--- a/src/HOL/IMP/Big_Step.thy Mon Mar 25 14:07:59 2013 +0100
+++ b/src/HOL/IMP/Big_Step.thy Mon Mar 25 15:09:41 2013 +0100
@@ -78,8 +78,8 @@
text{* What can we deduce from @{prop "(SKIP,s) \<Rightarrow> t"} ?
That @{prop "s = t"}. This is how we can automatically prove it: *}
-inductive_cases skipE[elim!]: "(SKIP,s) \<Rightarrow> t"
-thm skipE
+inductive_cases SkipE[elim!]: "(SKIP,s) \<Rightarrow> t"
+thm SkipE
text{* This is an \emph{elimination rule}. The [elim] attribute tells auto,
blast and friends (but not simp!) to use it automatically; [elim!] means that
@@ -216,6 +216,16 @@
(IF b2 THEN (IF b1 THEN c11 ELSE c2) ELSE (IF b1 THEN c12 ELSE c2))"
by blast
+lemma sim_while_cong_aux:
+ "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> c \<sim> c' \<Longrightarrow> (WHILE b DO c',s) \<Rightarrow> t"
+apply(induction "WHILE b DO c" s t arbitrary: b c rule: big_step_induct)
+ apply blast
+apply blast
+done
+
+lemma sim_while_cong: "c \<sim> c' \<Longrightarrow> WHILE b DO c \<sim> WHILE b DO c'"
+by (metis sim_while_cong_aux)
+
subsection "Execution is deterministic"