[STATEMENT]
lemma inf_Seq:
  "inf \<Gamma> (Seq c1 c2#cs) css (Normal s) = inf \<Gamma> (c1#c2#cs) css (Normal s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s) = AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = (Seq c1 c2#cs,css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (Seq c1 c2 # cs, css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (Seq c1 c2 # cs, css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
from f_step [rule_format, of 0] f_0
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (Seq c1 c2 # cs, css, Normal s)
[PROOF STEP]
have "f 1 = (c1#c2#cs,css,Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (Seq c1 c2 # cs, css, Normal s)

goal (1 subgoal):
 1. f 1 = (c1 # c2 # cs, css, Normal s)
[PROOF STEP]
by (auto elim: step_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
f 1 = (c1 # c2 # cs, css, Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
with f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = (c1 # c2 # cs, css, Normal s)
[PROOF STEP]
show "inf \<Gamma> (c1#c2#cs) css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = (c1 # c2 # cs, css, Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (c1 # c2 # cs, css, Normal s)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (c1 # c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (Suc i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (c1 # c2 # cs, css, Normal s)\<rbrakk> \<Longrightarrow> f (Suc 0) = (c1 # c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f (Suc i) \<rightarrow> f (Suc (Suc i)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> (c1 # c2 # cs) css (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = (c1# c2#cs,css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (c1 # c2 # cs, css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (c1 # c2 # cs, css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
define g where "g i = (case i of 0 \<Rightarrow> (Seq c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j)" for i
[PROOF STATE]
proof (state)
this:
g ?i = (case ?i of 0 \<Rightarrow> (Seq c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
with f_0
[PROOF STATE]
proof (chain)
picking this:
f 0 = (c1 # c2 # cs, css, Normal s)
g ?i = (case ?i of 0 \<Rightarrow> (Seq c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)
[PROOF STEP]
have
    "\<Gamma>\<turnstile>g 0 \<rightarrow> g (Suc 0)"
[PROOF STATE]
proof (prove)
using this:
f 0 = (c1 # c2 # cs, css, Normal s)
g ?i = (case ?i of 0 \<Rightarrow> (Seq c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0)
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
from f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<forall>i. i\<noteq>0 \<longrightarrow> \<Gamma>\<turnstile>g i \<rightarrow> g (Suc i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. \<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)
[PROOF STEP]
by (auto simp add: g_def split: nat.splits)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c1 # c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)
[PROOF STEP]
show "inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (Seq c1 c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x=g in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> g 0 \<rightarrow> g (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i)\<rbrakk> \<Longrightarrow> g 0 = (Seq c1 c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> g i \<rightarrow> g (Suc i))
[PROOF STEP]
apply (simp add: g_def split: nat.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (Seq c1 c2 # cs) css (Normal s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_WhileTrue:
  assumes b: "s \<in> b"
  shows "inf \<Gamma> (While b c#cs) css (Normal s) =
          inf \<Gamma> (c#While b c#cs) css (Normal s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s) = AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> (While b c # cs) css (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = (While b c#cs,css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (While b c # cs, css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (While b c # cs, css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
from b f_step [rule_format, of 0] f_0
[PROOF STATE]
proof (chain)
picking this:
s \<in> b
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (While b c # cs, css, Normal s)
[PROOF STEP]
have "f 1 = (c#While b c#cs,css,Normal s)"
[PROOF STATE]
proof (prove)
using this:
s \<in> b
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (While b c # cs, css, Normal s)

goal (1 subgoal):
 1. f 1 = (c # While b c # cs, css, Normal s)
[PROOF STEP]
by (auto elim: step_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
f 1 = (c # While b c # cs, css, Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
with f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = (c # While b c # cs, css, Normal s)
[PROOF STEP]
show "inf \<Gamma> (c # While b c # cs) css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = (c # While b c # cs, css, Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (c # While b c # cs, css, Normal s)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (c # While b c # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (Suc i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = (c # While b c # cs, css, Normal s)\<rbrakk> \<Longrightarrow> f (Suc 0) = (c # While b c # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f (Suc i) \<rightarrow> f (Suc (Suc i)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> (c # While b c # cs) css (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = (c # While b c #cs,css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (c # While b c # cs, css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (c # While b c # cs, css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
define h where "h i = (case i of 0 \<Rightarrow> (While b c#cs,css,Normal s) | Suc j \<Rightarrow> f j)"  for i
[PROOF STATE]
proof (state)
this:
h ?i = (case ?i of 0 \<Rightarrow> (While b c # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
with b f_0
[PROOF STATE]
proof (chain)
picking this:
s \<in> b
f 0 = (c # While b c # cs, css, Normal s)
h ?i = (case ?i of 0 \<Rightarrow> (While b c # cs, css, Normal s) | Suc j \<Rightarrow> f j)
[PROOF STEP]
have
    "\<Gamma>\<turnstile>h 0 \<rightarrow> h (Suc 0)"
[PROOF STATE]
proof (prove)
using this:
s \<in> b
f 0 = (c # While b c # cs, css, Normal s)
h ?i = (case ?i of 0 \<Rightarrow> (While b c # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
from f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<forall>i. i\<noteq>0 \<longrightarrow> \<Gamma>\<turnstile>h i \<rightarrow> h (Suc i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. \<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)
[PROOF STEP]
by (auto simp add: h_def split: nat.splits)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (c # While b c # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)
[PROOF STEP]
show "inf \<Gamma> (While b c # cs) css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (While b c # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x=h in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)\<rbrakk> \<Longrightarrow> h 0 = (While b c # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i))
[PROOF STEP]
apply (simp add: h_def split: nat.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (While b c # cs) css (Normal s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_Catch:
"inf \<Gamma> (Catch c1 c2#cs) css (Normal s) = inf \<Gamma> [c1] ((cs,c2#cs)#css) (Normal s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s) = AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> (Catch c1 c2#cs) css (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = (Catch c1 c2#cs,css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = (Catch c1 c2 # cs, css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = (Catch c1 c2 # cs, css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
from f_step [rule_format, of 0] f_0
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (Catch c1 c2 # cs, css, Normal s)
[PROOF STEP]
have "f 1 = ([c1],(cs,c2#cs)#css,Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> f 0 \<rightarrow> f (Suc 0)
f 0 = (Catch c1 c2 # cs, css, Normal s)

goal (1 subgoal):
 1. f 1 = ([c1], (cs, c2 # cs) # css, Normal s)
[PROOF STEP]
by (auto elim: step_Normal_elim_cases)
[PROOF STATE]
proof (state)
this:
f 1 = ([c1], (cs, c2 # cs) # css, Normal s)

goal (2 subgoals):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
 2. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
with f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = ([c1], (cs, c2 # cs) # css, Normal s)
[PROOF STEP]
show "inf \<Gamma> [c1] ((cs,c2#cs)#css) (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
f 1 = ([c1], (cs, c2 # cs) # css, Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = ([c1], (cs, c2 # cs) # css, Normal s)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = ([c1], (cs, c2 # cs) # css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x="\<lambda>i. f (Suc i)" in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i); f (Suc 0) = ([c1], (cs, c2 # cs) # css, Normal s)\<rbrakk> \<Longrightarrow> f (Suc 0) = ([c1], (cs, c2 # cs) # css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f (Suc i) \<rightarrow> f (Suc (Suc i)))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
assume "inf \<Gamma> [c1] ((cs,c2#cs)#css) (Normal s)"
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)
[PROOF STEP]
obtain f where
    f_0: "f 0 = ([c1],(cs,c2#cs)#css,Normal s)" and
    f_step: "\<forall>i. \<Gamma>\<turnstile>f i \<rightarrow> f (Suc i)"
[PROOF STATE]
proof (prove)
using this:
AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s)

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f 0 = ([c1], (cs, c2 # cs) # css, Normal s); \<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: inf_def)
[PROOF STATE]
proof (state)
this:
f 0 = ([c1], (cs, c2 # cs) # css, Normal s)
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
define h where "h i = (case i of 0 \<Rightarrow> (Catch c1 c2#cs,css,Normal s) | Suc j \<Rightarrow> f j)"  for i
[PROOF STATE]
proof (state)
this:
h ?i = (case ?i of 0 \<Rightarrow> (Catch c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
with f_0
[PROOF STATE]
proof (chain)
picking this:
f 0 = ([c1], (cs, c2 # cs) # css, Normal s)
h ?i = (case ?i of 0 \<Rightarrow> (Catch c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)
[PROOF STEP]
have
    "\<Gamma>\<turnstile>h 0 \<rightarrow> h (Suc 0)"
[PROOF STATE]
proof (prove)
using this:
f 0 = ([c1], (cs, c2 # cs) # css, Normal s)
h ?i = (case ?i of 0 \<Rightarrow> (Catch c1 c2 # cs, css, Normal s) | Suc j \<Rightarrow> f j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
[PROOF STEP]
by (auto intro: step.intros)
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
from f_step
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)
[PROOF STEP]
have "\<forall>i. i\<noteq>0 \<longrightarrow> \<Gamma>\<turnstile>h i \<rightarrow> h (Suc i)"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i)

goal (1 subgoal):
 1. \<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)
[PROOF STEP]
by (auto simp add: h_def split: nat.splits)
[PROOF STATE]
proof (state)
this:
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> [c1] ((cs, c2 # cs) # css) (Normal s) \<Longrightarrow> AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)
[PROOF STEP]
show "inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0)
\<forall>i. i \<noteq> 0 \<longrightarrow> \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)

goal (1 subgoal):
 1. AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)
[PROOF STEP]
apply (simp add: inf_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)\<rbrakk> \<Longrightarrow> \<exists>f. f 0 = (Catch c1 c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow> f (Suc i))
[PROOF STEP]
apply (rule_tac x=h in exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> h 0 \<rightarrow> h (Suc 0); \<forall>i>0. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i)\<rbrakk> \<Longrightarrow> h 0 = (Catch c1 c2 # cs, css, Normal s) \<and> (\<forall>i. \<Gamma>\<turnstile> h i \<rightarrow> h (Suc i))
[PROOF STEP]
apply (simp add: h_def split: nat.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
AlternativeSmallStep.inf \<Gamma> (Catch c1 c2 # cs) css (Normal s)

goal:
No subgoals!
[PROOF STEP]
qed