Time 
Nick 
Message 
00:11 
phimuemue_ 
is here anybody from tum semantics course? 
00:12 
* larsrh 

00:12 
phimuemue_ 
because I'm struggling with the current homework 
00:12 
larsrh 
sheet 6 or 7? 
00:12 
phimuemue_ 
sheet 6 (lastminuteworking) 
00:13 
phimuemue_ 
I'm not able to prove the second lemma (microsteps_imp_bigstep) 
00:13 
phimuemue_ 
I tried induction with rule: micro_steps_induct, arbitrary t, which leads to a subgoal I'm not able to solve 
00:14 
larsrh 
which one is that lemma? 
00:14 
phimuemue_ 
"micro_steps (cs, s) (cs', s') \<Longrightarrow> \<forall> t. (seq cs, s) \<Rightarrow> t \<longleftrightarrow> (seq cs', s') \<Rightarrow> t" 
00:15 
phimuemue_ 
which leaves me with the following subgoal 
00:15 
phimuemue_ 
⋀a b aa ba ab bb. 
00:15 
phimuemue_ 
⟦micro_step (a, b) (aa, ba); star micro_step (aa, ba) (ab, bb); ∀t. (seq aa, ba) ⇒ t = (seq ab, bb) ⇒ t⟧ 
00:15 
phimuemue_ 
⟹ ∀t. (seq a, b) ⇒ t = (seq ab, bb) ⇒ t 
00:16 
phimuemue_ 
do i have to connect seq and micro_step/micro_steps somehow? 
00:17 
larsrh 
I think it is easier if you first split the lemma into 'assumes' and 'shows' 
00:17 
phimuemue_ 
ah ok, I'll give this a try, but then I'll have to be familiar with isar, right? 
00:17 
larsrh 
because the proof itself should be fairly easy once you got the structure right 
00:17 
larsrh 
yep, I wrote it in Isar 
00:17 
phimuemue_ 
did you split the original lemma or just my subgoal? 
00:18 
larsrh 
the original lemma 
00:18 
phimuemue_ 
thank you, I'll try it 
00:19 
larsrh 
the actual proof is then a subproof which should go through with the induction rule you tried to use 
00:19 
phimuemue_ 
ah, ok 
00:25 
phimuemue_ 
but when i split it into assumption and show, i can seemingly not apply this induction rule, because it apparently disappered from the goal. 
00:25 
phimuemue_ 
how can i tell isar that i want the induction on the assumptions? 
00:34 
phimuemue_ 
thank you so far. 
00:34 
phimuemue_ 
good night 
00:34 

phimuemue_ left #isabelle 
01:51 

dschoepe joined #isabelle 
01:59 

dschoepe joined #isabelle 
07:59 

phimuemue_ joined #isabelle 
09:14 
phimuemue_ 
hi 
09:15 
phimuemue_ 
if i am trying to prove something in isar language (via induction) and i have a case where "this" refers to some things, and i want to do induction on the thigs in "this", how can this be acchieved? 
09:34 

phimuemue__ joined #isabelle 
09:45 

bwright joined #isabelle 
10:39 

dschoepe joined #isabelle 
10:46 

phimuemue_ joined #isabelle 
14:23 
larsrh 
phimuemue_: you can always start a subproof 
14:23 
larsrh 
assume foo hence bar proof (induction ...) 
23:51 

davidL joined #isabelle 