# IRC log for #isabelle, 2011-12-07

All times shown according to UTC.

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 (last-minute-working)
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 sub-proof 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