# HG changeset patch
# User kleing
# Date 1312814875 -7200
# Node ID cebb7abb54b18bcac5705320cbd11e5d70b80a74
# Parent  d7c7ec248ef044fd037af64808a1fcdcc44c1c1e
import constant folding theory into IMP

diff -r d7c7ec248ef0 -r cebb7abb54b1 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Sat Aug 06 15:48:08 2011 +0200
+++ b/src/HOL/IMP/Big_Step.thy	Mon Aug 08 16:47:55 2011 +0200
@@ -113,6 +113,10 @@
   qed
 qed
 
+(* Using rule inversion to prove simplification rules: *)
+lemma assign_simp:
+  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
+  by auto
 
 subsection "Command Equivalence"
 
diff -r d7c7ec248ef0 -r cebb7abb54b1 src/HOL/IMP/Comp_Rev.thy
--- a/src/HOL/IMP/Comp_Rev.thy	Sat Aug 06 15:48:08 2011 +0200
+++ b/src/HOL/IMP/Comp_Rev.thy	Mon Aug 08 16:47:55 2011 +0200
@@ -479,9 +479,7 @@
   "ccomp c = [] \<Longrightarrow> (c,s) \<Rightarrow> s"
   by (induct c) auto
 
-lemma assign [simp]:
-  "(x ::= a,s) \<Rightarrow> s' \<longleftrightarrow> (s' = s(x := aval a s))"
-  by auto
+declare assign_simp [simp]
 
 lemma ccomp_exec_n:
   "ccomp c \<turnstile> (0,s,stk) \<rightarrow>^n (isize(ccomp c),t,stk')
diff -r d7c7ec248ef0 -r cebb7abb54b1 src/HOL/IMP/Fold.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Fold.thy	Mon Aug 08 16:47:55 2011 +0200
@@ -0,0 +1,413 @@
+header "Constant Folding"
+
+theory Fold imports Sem_Equiv begin
+
+section "Simple folding of arithmetic expressions"
+
+types
+  tab = "name \<Rightarrow> val option"
+
+(* maybe better as the composition of substitution and the existing simp_const(0) *)
+fun simp_const :: "aexp \<Rightarrow> tab \<Rightarrow> aexp" where
+"simp_const (N n) _ = N n" |
+"simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
+"simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
+  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')" 
+
+definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
+
+theorem aval_simp_const[simp]:
+assumes "approx t s"
+shows "aval (simp_const a t) s = aval a s"
+  using assms 
+  by (induct a) (auto simp: approx_def split: aexp.split option.split)
+
+theorem aval_simp_const_N:
+assumes "approx t s"
+shows "simp_const a t = N n \<Longrightarrow> aval a s = n"
+  using assms
+  by (induct a arbitrary: n)
+     (auto simp: approx_def split: aexp.splits option.splits)
+
+definition
+  "merge t1 t2 = (\<lambda>m. if t1 m = t2 m then t1 m else None)"
+
+primrec lnames :: "com \<Rightarrow> name set" where
+"lnames SKIP = {}" |
+"lnames (x ::= a) = {x}" |
+"lnames (c1; c2) = lnames c1 \<union> lnames c2" |
+"lnames (IF b THEN c1 ELSE c2) = lnames c1 \<union> lnames c2" |
+"lnames (WHILE b DO c) = lnames c"
+
+primrec "defs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"defs SKIP t = t" |
+"defs (x ::= a) t =
+  (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"defs (c1;c2) t = (defs c2 o defs c1) t" |
+"defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
+"defs (WHILE b DO c) t = t |` (-lnames c)" 
+
+primrec fold where
+"fold SKIP _ = SKIP" |
+"fold (x ::= a) t = (x ::= (simp_const a t))" |
+"fold (c1;c2) t = (fold c1 t; fold c2 (defs c1 t))" |
+"fold (IF b THEN c1 ELSE c2) t = IF b THEN fold c1 t ELSE fold c2 t" |
+"fold (WHILE b DO c) t = WHILE b DO fold c (t |` (-lnames c))"
+
+lemma approx_merge:
+  "approx t1 s \<or> approx t2 s \<Longrightarrow> approx (merge t1 t2) s"
+  by (fastsimp simp: merge_def approx_def)
+
+lemma approx_map_le:
+  "approx t2 s \<Longrightarrow> t1 \<subseteq>\<^sub>m t2 \<Longrightarrow> approx t1 s"
+  by (clarsimp simp: approx_def map_le_def dom_def)
+
+lemma restrict_map_le [intro!, simp]: "t |` S \<subseteq>\<^sub>m t"
+  by (clarsimp simp: restrict_map_def map_le_def)
+
+lemma merge_restrict:
+  assumes "t1 |` S = t |` S"
+  assumes "t2 |` S = t |` S"
+  shows "merge t1 t2 |` S = t |` S"
+proof -
+  from assms
+  have "\<forall>x. (t1 |` S) x = (t |` S) x" 
+   and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
+  thus ?thesis
+    by (auto simp: merge_def restrict_map_def 
+             split: if_splits intro: ext)
+qed
+
+
+lemma defs_restrict:
+  "defs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+  case (Semi c1 c2)
+  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
+    by simp
+  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
+         t |` (- lnames c1) |` (-lnames c2)" by simp
+  moreover
+  from Semi
+  have "defs c2 (defs c1 t) |` (- lnames c2) = 
+        defs c1 t |` (- lnames c2)"
+    by simp
+  hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
+         defs c1 t |` (- lnames c2) |` (- lnames c1)"
+    by simp
+  ultimately
+  show ?case by (clarsimp simp: Int_commute)
+next
+  case (If b c1 c2)
+  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
+         t |` (- lnames c1) |` (-lnames c2)" by simp
+  moreover
+  from If
+  have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) = 
+         t |` (- lnames c2) |` (-lnames c1)" by simp
+  ultimately
+  show ?case by (auto simp: Int_commute intro: merge_restrict)
+qed (auto split: aexp.split)
+
+
+lemma big_step_pres_approx:
+  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (defs c t) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+  case Skip thus ?case by simp
+next
+  case Assign
+  thus ?case
+    by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+  case (Semi c1 s1 s2 c2 s3)
+  have "approx (defs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+  hence "approx (defs c2 (defs c1 t)) s3" by (rule Semi(4))
+  thus ?case by simp
+next
+  case (IfTrue b s c1 s')
+  hence "approx (defs c1 t) s'" by simp
+  thus ?case by (simp add: approx_merge)
+next
+  case (IfFalse b s c2 s')
+  hence "approx (defs c2 t) s'" by simp
+  thus ?case by (simp add: approx_merge)
+next
+  case WhileFalse
+  thus ?case by (simp add: approx_def restrict_map_def)
+next
+  case (WhileTrue b s1 c s2 s3)
+  hence "approx (defs c t) s2" by simp
+  with WhileTrue
+  have "approx (defs c t |` (-lnames c)) s3" by simp
+  thus ?case by (simp add: defs_restrict)
+qed
+
+corollary approx_defs_inv [simp]:
+  "\<Turnstile> {approx t} c {approx (defs c t)}"
+  by (simp add: hoare_valid_def big_step_pres_approx)
+
+
+lemma big_step_pres_approx_restrict:
+  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
+proof (induct arbitrary: t rule: big_step_induct)
+  case Assign
+  thus ?case by (clarsimp simp: approx_def)
+next
+  case (Semi c1 s1 s2 c2 s3)
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
+    by (simp add: Int_commute)
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
+    by (rule Semi)
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s2"
+    by (simp add: Int_commute)
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s3"
+    by (rule Semi)
+  thus ?case by simp
+next
+  case (IfTrue b s c1 s' c2)
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" 
+    by (simp add: Int_commute)
+  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'" 
+    by (rule IfTrue)
+  thus ?case by (simp add: Int_commute) 
+next
+  case (IfFalse b s c2 s' c1)
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s" 
+    by simp
+  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'" 
+    by (rule IfFalse)
+  thus ?case by simp
+qed auto
+
+
+lemma approx_restrict_inv:
+  "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
+  by (simp add: hoare_valid_def big_step_pres_approx_restrict)
+
+declare assign_simp [simp]
+
+lemma approx_eq:
+  "approx t \<Turnstile> c \<sim> fold c t"
+proof (induct c arbitrary: t)
+  case SKIP show ?case by simp
+next
+  case Assign
+  show ?case by (simp add: equiv_up_to_def)
+next
+  case Semi 
+  thus ?case by (auto intro!: equiv_up_to_semi)
+next
+  case If
+  thus ?case by (auto intro!: equiv_up_to_if_weak)
+next
+  case (While b c)
+  hence "approx (t |` (- lnames c)) \<Turnstile> 
+         WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
+    by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
+  thus ?case 
+    by (auto intro: equiv_up_to_weaken approx_map_le)
+qed
+  
+
+lemma approx_empty [simp]: 
+  "approx empty = (\<lambda>_. True)"
+  by (auto intro!: ext simp: approx_def)
+
+lemma equiv_sym:
+  "c \<sim> c' \<longleftrightarrow> c' \<sim> c"
+  by (auto simp add: equiv_def)
+
+theorem constant_folding_equiv:
+  "fold c empty \<sim> c"
+  using approx_eq [of empty c]
+  by (simp add: equiv_up_to_True equiv_sym)
+
+
+
+section {* More ambitious folding including boolean expressions *}
+
+
+fun bsimp_const :: "bexp \<Rightarrow> tab \<Rightarrow> bexp" where
+"bsimp_const (Less a1 a2) t = less (simp_const a1 t) (simp_const a2 t)" |
+"bsimp_const (And b1 b2) t = and (bsimp_const b1 t) (bsimp_const b2 t)" |
+"bsimp_const (Not b) t = not(bsimp_const b t)" |
+"bsimp_const (B bv) _ = B bv"
+
+theorem bvalsimp_const [simp]:
+  assumes "approx t s"
+  shows "bval (bsimp_const b t) s = bval b s"
+  using assms by (induct b) auto
+
+lemma not_B [simp]: "not (B v) = B (\<not>v)"
+  by (cases v) auto
+
+lemma not_B_eq [simp]: "(not b = B v) = (b = B (\<not>v))"
+  by (cases b) auto
+
+lemma and_B_eq: 
+  "(and a b = B v) = (a = B False \<and> \<not>v \<or> 
+                      b = B False \<and> \<not>v \<or> 
+                      (\<exists>v1 v2. a = B v1 \<and> b = B v2 \<and> v = v1 \<and> v2))"
+  by (rule and.induct) auto
+
+lemma less_B_eq [simp]:
+  "(less a b = B v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
+  by (rule less.induct) auto
+    
+theorem bvalsimp_const_B:
+assumes "approx t s"
+shows "bsimp_const b t = B v \<Longrightarrow> bval b s = v"
+  using assms
+  by (induct b arbitrary: v)
+     (auto simp: approx_def and_B_eq aval_simp_const_N 
+           split: bexp.splits bool.splits)
+
+
+primrec "bdefs" :: "com \<Rightarrow> tab \<Rightarrow> tab" where
+"bdefs SKIP t = t" |
+"bdefs (x ::= a) t =
+  (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
+"bdefs (c1;c2) t = (bdefs c2 o bdefs c1) t" |
+"bdefs (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+    B True \<Rightarrow> bdefs c1 t
+  | B False \<Rightarrow> bdefs c2 t
+  | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
+"bdefs (WHILE b DO c) t = t |` (-lnames c)" 
+
+
+primrec bfold where
+"bfold SKIP _ = SKIP" |
+"bfold (x ::= a) t = (x ::= (simp_const a t))" |
+"bfold (c1;c2) t = (bfold c1 t; bfold c2 (bdefs c1 t))" |
+"bfold (IF b THEN c1 ELSE c2) t = (case bsimp_const b t of
+    B True \<Rightarrow> bfold c1 t
+  | B False \<Rightarrow> bfold c2 t
+  | _ \<Rightarrow> IF bsimp_const b t THEN bfold c1 t ELSE bfold c2 t)" |
+"bfold (WHILE b DO c) t = (case bsimp_const b t of
+    B False \<Rightarrow> SKIP
+  | _ \<Rightarrow> WHILE bsimp_const b (t |` (-lnames c)) DO bfold c (t |` (-lnames c)))"
+
+
+lemma bdefs_restrict:
+  "bdefs c t |` (- lnames c) = t |` (- lnames c)"
+proof (induct c arbitrary: t)
+  case (Semi c1 c2)
+  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
+    by simp
+  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
+         t |` (- lnames c1) |` (-lnames c2)" by simp
+  moreover
+  from Semi
+  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
+        bdefs c1 t |` (- lnames c2)"
+    by simp
+  hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
+         bdefs c1 t |` (- lnames c2) |` (- lnames c1)"
+    by simp
+  ultimately
+  show ?case by (clarsimp simp: Int_commute)
+next
+  case (If b c1 c2)
+  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
+  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
+         t |` (- lnames c1) |` (-lnames c2)" by simp
+  moreover
+  from If
+  have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
+  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) = 
+         t |` (- lnames c2) |` (-lnames c1)" by simp
+  ultimately
+  show ?case 
+    by (auto simp: Int_commute intro: merge_restrict 
+             split: bexp.splits bool.splits)
+qed (auto split: aexp.split bexp.split bool.split)
+
+
+lemma big_step_pres_approx_b:
+  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
+proof (induct arbitrary: t rule: big_step_induct)
+  case Skip thus ?case by simp
+next
+  case Assign
+  thus ?case
+    by (clarsimp simp: aval_simp_const_N approx_def split: aexp.split)
+next
+  case (Semi c1 s1 s2 c2 s3)
+  have "approx (bdefs c1 t) s2" by (rule Semi(2) [OF Semi.prems])
+  hence "approx (bdefs c2 (bdefs c1 t)) s3" by (rule Semi(4))
+  thus ?case by simp
+next
+  case (IfTrue b s c1 s')
+  hence "approx (bdefs c1 t) s'" by simp
+  thus ?case using `bval b s` `approx t s`
+    by (clarsimp simp: approx_merge bvalsimp_const_B 
+                 split: bexp.splits bool.splits)
+next
+  case (IfFalse b s c2 s')
+  hence "approx (bdefs c2 t) s'" by simp
+  thus ?case using `\<not>bval b s` `approx t s`
+    by (clarsimp simp: approx_merge bvalsimp_const_B 
+                 split: bexp.splits bool.splits)
+next
+  case WhileFalse
+  thus ?case 
+    by (clarsimp simp: bvalsimp_const_B approx_def restrict_map_def
+                 split: bexp.splits bool.splits)
+next
+  case (WhileTrue b s1 c s2 s3)
+  hence "approx (bdefs c t) s2" by simp
+  with WhileTrue
+  have "approx (bdefs c t |` (- lnames c)) s3"
+    by simp
+  thus ?case 
+    by (simp add: bdefs_restrict)
+qed
+
+corollary approx_bdefs_inv [simp]:
+  "\<Turnstile> {approx t} c {approx (bdefs c t)}"
+  by (simp add: hoare_valid_def big_step_pres_approx_b)
+
+lemma bfold_equiv: 
+  "approx t \<Turnstile> c \<sim> bfold c t"
+proof (induct c arbitrary: t)
+  case SKIP show ?case by simp
+next
+  case Assign
+  thus ?case by (simp add: equiv_up_to_def)
+next
+  case Semi
+  thus ?case by (auto intro!: equiv_up_to_semi)           
+next
+  case (If b c1 c2)
+  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
+                   IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
+    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
+  thus ?case using If
+    by (fastsimp simp: bvalsimp_const_B split: bexp.splits bool.splits 
+                 intro: equiv_up_to_trans)
+  next
+  case (While b c)
+  hence "approx (t |` (- lnames c)) \<Turnstile> 
+                   WHILE b DO c \<sim>
+                   WHILE bsimp_const b (t |` (- lnames c)) 
+                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'") 
+    by (auto intro: equiv_up_to_while_weak approx_restrict_inv 
+             simp: bequiv_up_to_def)
+  hence "approx t \<Turnstile> ?W \<sim> ?W'"
+    by (auto intro: equiv_up_to_weaken approx_map_le)
+  thus ?case
+    by (auto split: bexp.splits bool.splits 
+             intro: equiv_up_to_while_False 
+             simp: bvalsimp_const_B)
+qed
+
+
+theorem constant_bfolding_equiv:
+  "bfold c empty \<sim> c"
+  using bfold_equiv [of empty c]
+  by (simp add: equiv_up_to_True equiv_sym)
+
+
+end
diff -r d7c7ec248ef0 -r cebb7abb54b1 src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Sat Aug 06 15:48:08 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML	Mon Aug 08 16:47:55 2011 +0200
@@ -17,5 +17,6 @@
  "Procs_Stat_Vars_Dyn",
  "Procs_Stat_Vars_Stat",
  "C_like",
- "OO"
+ "OO",
+ "Fold"
 ];
diff -r d7c7ec248ef0 -r cebb7abb54b1 src/HOL/IMP/Sem_Equiv.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/Sem_Equiv.thy	Mon Aug 08 16:47:55 2011 +0200
@@ -0,0 +1,165 @@
+header "Semantic Equivalence up to a Condition"
+
+theory Sem_Equiv
+imports Hoare_Sound_Complete
+begin
+
+definition
+  equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
+where
+  "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
+
+definition 
+  bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
+where 
+  "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
+
+lemma equiv_up_to_True:
+  "((\<lambda>_. True) \<Turnstile> c \<sim> c') = (c \<sim> c')"
+  by (simp add: equiv_def equiv_up_to_def)
+
+lemma equiv_up_to_weaken:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P' s \<Longrightarrow> P s) \<Longrightarrow> P' \<Turnstile> c \<sim> c'"
+  by (simp add: equiv_up_to_def)
+
+lemma equiv_up_toI:
+  "(\<And>s s'. P s \<Longrightarrow> (c, s) \<Rightarrow> s' = (c', s) \<Rightarrow> s') \<Longrightarrow> P \<Turnstile> c \<sim> c'"
+  by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD1:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
+  by (unfold equiv_up_to_def) blast
+
+lemma equiv_up_toD2:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
+  by (unfold equiv_up_to_def) blast
+
+
+lemma equiv_up_to_refl [simp, intro!]:
+  "P \<Turnstile> c \<sim> c"
+  by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_sym:
+  "(P \<Turnstile> c \<sim> c') = (P \<Turnstile> c' \<sim> c)"
+  by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_trans [trans]:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> c' \<sim> c'' \<Longrightarrow> P \<Turnstile> c \<sim> c''"
+  by (auto simp: equiv_up_to_def)
+
+
+lemma bequiv_up_to_refl [simp, intro!]:
+  "P \<Turnstile> b <\<sim>> b"
+  by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_sym:
+  "(P \<Turnstile> b <\<sim>> b') = (P \<Turnstile> b' <\<sim>> b)"
+  by (auto simp: bequiv_up_to_def)
+
+lemma bequiv_up_to_trans [trans]:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
+  by (auto simp: bequiv_up_to_def)
+
+
+lemma equiv_up_to_hoare:
+  "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+  unfolding hoare_valid_def equiv_up_to_def by blast
+
+lemma equiv_up_to_hoare_eq:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
+  by (rule equiv_up_to_hoare)
+
+
+lemma equiv_up_to_semi:
+  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
+  P \<Turnstile> (c; d) \<sim> (c'; d')"
+  by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
+
+lemma equiv_up_to_while_lemma:
+  shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 
+         P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
+         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
+         \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
+         P s \<Longrightarrow> 
+         d = WHILE b DO c \<Longrightarrow> 
+         (WHILE b' DO c', s) \<Rightarrow> s'"  
+proof (induct rule: big_step_induct)
+  case (WhileTrue b s1 c s2 s3)
+  note IH = WhileTrue.hyps(5) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
+  
+  from WhileTrue.prems
+  have "P \<Turnstile> b <\<sim>> b'" by simp
+  with `bval b s1` `P s1`
+  have "bval b' s1" by (simp add: bequiv_up_to_def)
+  moreover
+  from WhileTrue.prems
+  have "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'" by simp
+  with `bval b s1` `P s1` `(c, s1) \<Rightarrow> s2`
+  have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
+  moreover
+  from WhileTrue.prems
+  have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
+  with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
+  have "P s2" by (simp add: hoare_valid_def)
+  hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
+  ultimately 
+  show ?case by blast
+next
+  case WhileFalse
+  thus ?case by (auto simp: bequiv_up_to_def)
+qed (fastsimp simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
+
+lemma bequiv_context_subst:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
+  by (auto simp: bequiv_up_to_def)
+
+lemma equiv_up_to_while:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
+   \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
+   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+  apply (safe intro!: equiv_up_toI)
+   apply (auto intro: equiv_up_to_while_lemma)[1]
+  apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
+  apply (drule equiv_up_to_sym [THEN iffD1])
+  apply (drule bequiv_up_to_sym [THEN iffD1])
+  apply (auto intro: equiv_up_to_while_lemma)[1]
+  done
+
+lemma equiv_up_to_while_weak:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
+   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
+  by (fastsimp elim!: equiv_up_to_while equiv_up_to_weaken 
+               simp: hoare_valid_def)
+
+lemma equiv_up_to_if:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<inter> bval b \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
+   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+  by (auto simp: bequiv_up_to_def equiv_up_to_def)
+
+lemma equiv_up_to_if_weak:
+  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> P \<Turnstile> d \<sim> d' \<Longrightarrow>
+   P \<Turnstile> IF b THEN c ELSE d \<sim> IF b' THEN c' ELSE d'"
+  by (fastsimp elim!: equiv_up_to_if equiv_up_to_weaken)
+
+lemma equiv_up_to_if_True [intro!]:
+  "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
+  by (auto simp: equiv_up_to_def) 
+
+lemma equiv_up_to_if_False [intro!]:
+  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
+  by (auto simp: equiv_up_to_def)
+
+lemma equiv_up_to_while_False [intro!]:
+  "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
+  by (auto simp: equiv_up_to_def)
+
+lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
+ by (induct rule: big_step_induct) auto
+  
+lemma equiv_up_to_while_True [intro!,simp]:
+  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
+  unfolding equiv_up_to_def
+  by (blast dest: while_never)
+
+
+end
\ No newline at end of file