# HG changeset patch
# User nipkow
# Date 1364220581 -3600
# Node ID 7a29122823916c61bd57621c52ee9cf1197080dd
# Parent  193ba70666bd65dd0db6ada0d21653ba073d4bdb
added lemmas

diff -r 193ba70666bd -r 7a2912282391 src/HOL/IMP/Big_Step.thy
--- 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"