remove Hoare dependency from Fold.thy
authorGerwin Klein <gerwin.klein@nicta.com.au>
Thu Aug 23 15:32:22 2012 +0200 (2012-08-23)
changeset 48909b2dea007e55e
parent 48895 4cd4ef1ef4a4
child 48910 1c8c15c30356
remove Hoare dependency from Fold.thy
src/HOL/IMP/Fold.thy
src/HOL/IMP/Sem_Equiv.thy
     1.1 --- a/src/HOL/IMP/Fold.thy	Wed Aug 22 23:45:49 2012 +0200
     1.2 +++ b/src/HOL/IMP/Fold.thy	Thu Aug 23 15:32:22 2012 +0200
     1.3 @@ -12,14 +12,14 @@
     1.4  "simp_const (N n) _ = N n" |
     1.5  "simp_const (V x) t = (case t x of None \<Rightarrow> V x | Some k \<Rightarrow> N k)" |
     1.6  "simp_const (Plus e1 e2) t = (case (simp_const e1 t, simp_const e2 t) of
     1.7 -  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')" 
     1.8 +  (N n1, N n2) \<Rightarrow> N(n1+n2) | (e1',e2') \<Rightarrow> Plus e1' e2')"
     1.9  
    1.10  definition "approx t s \<longleftrightarrow> (ALL x k. t x = Some k \<longrightarrow> s x = k)"
    1.11  
    1.12  theorem aval_simp_const[simp]:
    1.13  assumes "approx t s"
    1.14  shows "aval (simp_const a t) s = aval a s"
    1.15 -  using assms 
    1.16 +  using assms
    1.17    by (induct a) (auto simp: approx_def split: aexp.split option.split)
    1.18  
    1.19  theorem aval_simp_const_N:
    1.20 @@ -45,7 +45,7 @@
    1.21    (case simp_const a t of N k \<Rightarrow> t(x \<mapsto> k) | _ \<Rightarrow> t(x:=None))" |
    1.22  "defs (c1;c2) t = (defs c2 o defs c1) t" |
    1.23  "defs (IF b THEN c1 ELSE c2) t = merge (defs c1 t) (defs c2 t)" |
    1.24 -"defs (WHILE b DO c) t = t |` (-lnames c)" 
    1.25 +"defs (WHILE b DO c) t = t |` (-lnames c)"
    1.26  
    1.27  primrec fold where
    1.28  "fold SKIP _ = SKIP" |
    1.29 @@ -71,10 +71,10 @@
    1.30    shows "merge t1 t2 |` S = t |` S"
    1.31  proof -
    1.32    from assms
    1.33 -  have "\<forall>x. (t1 |` S) x = (t |` S) x" 
    1.34 +  have "\<forall>x. (t1 |` S) x = (t |` S) x"
    1.35     and "\<forall>x. (t2 |` S) x = (t |` S) x" by auto
    1.36    thus ?thesis
    1.37 -    by (auto simp: merge_def restrict_map_def 
    1.38 +    by (auto simp: merge_def restrict_map_def
    1.39               split: if_splits intro: ext)
    1.40  qed
    1.41  
    1.42 @@ -83,13 +83,13 @@
    1.43    "defs c t |` (- lnames c) = t |` (- lnames c)"
    1.44  proof (induction c arbitrary: t)
    1.45    case (Seq c1 c2)
    1.46 -  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
    1.47 +  hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)"
    1.48      by simp
    1.49 -  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
    1.50 +  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
    1.51           t |` (- lnames c1) |` (-lnames c2)" by simp
    1.52    moreover
    1.53    from Seq
    1.54 -  have "defs c2 (defs c1 t) |` (- lnames c2) = 
    1.55 +  have "defs c2 (defs c1 t) |` (- lnames c2) =
    1.56          defs c1 t |` (- lnames c2)"
    1.57      by simp
    1.58    hence "defs c2 (defs c1 t) |` (- lnames c2) |` (- lnames c1) =
    1.59 @@ -100,12 +100,12 @@
    1.60  next
    1.61    case (If b c1 c2)
    1.62    hence "defs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
    1.63 -  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) = 
    1.64 +  hence "defs c1 t |` (- lnames c1) |` (-lnames c2) =
    1.65           t |` (- lnames c1) |` (-lnames c2)" by simp
    1.66    moreover
    1.67    from If
    1.68    have "defs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
    1.69 -  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) = 
    1.70 +  hence "defs c2 t |` (- lnames c2) |` (-lnames c1) =
    1.71           t |` (- lnames c2) |` (-lnames c1)" by simp
    1.72    ultimately
    1.73    show ?case by (auto simp: Int_commute intro: merge_restrict)
    1.74 @@ -144,10 +144,6 @@
    1.75    thus ?case by (simp add: defs_restrict)
    1.76  qed
    1.77  
    1.78 -corollary approx_defs_inv [simp]:
    1.79 -  "\<Turnstile> {approx t} c {approx (defs c t)}"
    1.80 -  by (simp add: hoare_valid_def big_step_pres_approx)
    1.81 -
    1.82  
    1.83  lemma big_step_pres_approx_restrict:
    1.84    "(c,s) \<Rightarrow> s' \<Longrightarrow> approx (t |` (-lnames c)) s \<Longrightarrow> approx (t |` (-lnames c)) s'"
    1.85 @@ -156,7 +152,7 @@
    1.86    thus ?case by (clarsimp simp: approx_def)
    1.87  next
    1.88    case (Seq c1 s1 s2 c2 s3)
    1.89 -  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1" 
    1.90 +  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s1"
    1.91      by (simp add: Int_commute)
    1.92    hence "approx (t |` (-lnames c2) |` (-lnames c1)) s2"
    1.93      by (rule Seq)
    1.94 @@ -167,25 +163,21 @@
    1.95    thus ?case by simp
    1.96  next
    1.97    case (IfTrue b s c1 s' c2)
    1.98 -  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s" 
    1.99 +  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s"
   1.100      by (simp add: Int_commute)
   1.101 -  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'" 
   1.102 +  hence "approx (t |` (-lnames c2) |` (-lnames c1)) s'"
   1.103      by (rule IfTrue)
   1.104 -  thus ?case by (simp add: Int_commute) 
   1.105 +  thus ?case by (simp add: Int_commute)
   1.106  next
   1.107    case (IfFalse b s c2 s' c1)
   1.108 -  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s" 
   1.109 +  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s"
   1.110      by simp
   1.111 -  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'" 
   1.112 +  hence "approx (t |` (-lnames c1) |` (-lnames c2)) s'"
   1.113      by (rule IfFalse)
   1.114    thus ?case by simp
   1.115  qed auto
   1.116  
   1.117  
   1.118 -lemma approx_restrict_inv:
   1.119 -  "\<Turnstile> {approx (t |` (-lnames c))} c {approx (t |` (-lnames c))}"
   1.120 -  by (simp add: hoare_valid_def big_step_pres_approx_restrict)
   1.121 -
   1.122  declare assign_simp [simp]
   1.123  
   1.124  lemma approx_eq:
   1.125 @@ -196,22 +188,22 @@
   1.126    case Assign
   1.127    show ?case by (simp add: equiv_up_to_def)
   1.128  next
   1.129 -  case Seq 
   1.130 -  thus ?case by (auto intro!: equiv_up_to_seq)
   1.131 +  case Seq
   1.132 +  thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx)
   1.133  next
   1.134    case If
   1.135    thus ?case by (auto intro!: equiv_up_to_if_weak)
   1.136  next
   1.137    case (While b c)
   1.138 -  hence "approx (t |` (- lnames c)) \<Turnstile> 
   1.139 +  hence "approx (t |` (- lnames c)) \<Turnstile>
   1.140           WHILE b DO c \<sim> WHILE b DO fold c (t |` (- lnames c))"
   1.141 -    by (auto intro: equiv_up_to_while_weak approx_restrict_inv)
   1.142 -  thus ?case 
   1.143 +    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict)
   1.144 +  thus ?case
   1.145      by (auto intro: equiv_up_to_weaken approx_map_le)
   1.146  qed
   1.147 -  
   1.148 +
   1.149  
   1.150 -lemma approx_empty [simp]: 
   1.151 +lemma approx_empty [simp]:
   1.152    "approx empty = (\<lambda>_. True)"
   1.153    by (auto intro!: ext simp: approx_def)
   1.154  
   1.155 @@ -246,22 +238,22 @@
   1.156  lemma not_Bc_eq [simp]: "(not b = Bc v) = (b = Bc (\<not>v))"
   1.157    by (cases b) auto
   1.158  
   1.159 -lemma and_Bc_eq: 
   1.160 +lemma and_Bc_eq:
   1.161    "(and a b = Bc v) =
   1.162 -   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or> 
   1.163 +   (a = Bc False \<and> \<not>v  \<or>  b = Bc False \<and> \<not>v \<or>
   1.164      (\<exists>v1 v2. a = Bc v1 \<and> b = Bc v2 \<and> v = v1 \<and> v2))"
   1.165    by (rule and.induct) auto
   1.166  
   1.167  lemma less_Bc_eq [simp]:
   1.168    "(less a b = Bc v) = (\<exists>n1 n2. a = N n1 \<and> b = N n2 \<and> v = (n1 < n2))"
   1.169    by (rule less.induct) auto
   1.170 -    
   1.171 +
   1.172  theorem bvalsimp_const_Bc:
   1.173  assumes "approx t s"
   1.174  shows "bsimp_const b t = Bc v \<Longrightarrow> bval b s = v"
   1.175    using assms
   1.176    by (induct b arbitrary: v)
   1.177 -     (auto simp: approx_def and_Bc_eq aval_simp_const_N 
   1.178 +     (auto simp: approx_def and_Bc_eq aval_simp_const_N
   1.179             split: bexp.splits bool.splits)
   1.180  
   1.181  
   1.182 @@ -274,7 +266,7 @@
   1.183      Bc True \<Rightarrow> bdefs c1 t
   1.184    | Bc False \<Rightarrow> bdefs c2 t
   1.185    | _ \<Rightarrow> merge (bdefs c1 t) (bdefs c2 t))" |
   1.186 -"bdefs (WHILE b DO c) t = t |` (-lnames c)" 
   1.187 +"bdefs (WHILE b DO c) t = t |` (-lnames c)"
   1.188  
   1.189  
   1.190  primrec bfold where
   1.191 @@ -294,13 +286,13 @@
   1.192    "bdefs c t |` (- lnames c) = t |` (- lnames c)"
   1.193  proof (induction c arbitrary: t)
   1.194    case (Seq c1 c2)
   1.195 -  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" 
   1.196 +  hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)"
   1.197      by simp
   1.198 -  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
   1.199 +  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
   1.200           t |` (- lnames c1) |` (-lnames c2)" by simp
   1.201    moreover
   1.202    from Seq
   1.203 -  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) = 
   1.204 +  have "bdefs c2 (bdefs c1 t) |` (- lnames c2) =
   1.205          bdefs c1 t |` (- lnames c2)"
   1.206      by simp
   1.207    hence "bdefs c2 (bdefs c1 t) |` (- lnames c2) |` (- lnames c1) =
   1.208 @@ -311,22 +303,22 @@
   1.209  next
   1.210    case (If b c1 c2)
   1.211    hence "bdefs c1 t |` (- lnames c1) = t |` (- lnames c1)" by simp
   1.212 -  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) = 
   1.213 +  hence "bdefs c1 t |` (- lnames c1) |` (-lnames c2) =
   1.214           t |` (- lnames c1) |` (-lnames c2)" by simp
   1.215    moreover
   1.216    from If
   1.217    have "bdefs c2 t |` (- lnames c2) = t |` (- lnames c2)" by simp
   1.218 -  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) = 
   1.219 +  hence "bdefs c2 t |` (- lnames c2) |` (-lnames c1) =
   1.220           t |` (- lnames c2) |` (-lnames c1)" by simp
   1.221    ultimately
   1.222 -  show ?case 
   1.223 -    by (auto simp: Int_commute intro: merge_restrict 
   1.224 +  show ?case
   1.225 +    by (auto simp: Int_commute intro: merge_restrict
   1.226               split: bexp.splits bool.splits)
   1.227  qed (auto split: aexp.split bexp.split bool.split)
   1.228  
   1.229  
   1.230  lemma big_step_pres_approx_b:
   1.231 -  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'" 
   1.232 +  "(c,s) \<Rightarrow> s' \<Longrightarrow> approx t s \<Longrightarrow> approx (bdefs c t) s'"
   1.233  proof (induction arbitrary: t rule: big_step_induct)
   1.234    case Skip thus ?case by simp
   1.235  next
   1.236 @@ -352,7 +344,7 @@
   1.237                   split: bexp.splits bool.splits)
   1.238  next
   1.239    case WhileFalse
   1.240 -  thus ?case 
   1.241 +  thus ?case
   1.242      by (clarsimp simp: bvalsimp_const_Bc approx_def restrict_map_def
   1.243                   split: bexp.splits bool.splits)
   1.244  next
   1.245 @@ -361,15 +353,11 @@
   1.246    with WhileTrue
   1.247    have "approx (bdefs c t |` (- lnames c)) s3"
   1.248      by simp
   1.249 -  thus ?case 
   1.250 +  thus ?case
   1.251      by (simp add: bdefs_restrict)
   1.252  qed
   1.253  
   1.254 -corollary approx_bdefs_inv [simp]:
   1.255 -  "\<Turnstile> {approx t} c {approx (bdefs c t)}"
   1.256 -  by (simp add: hoare_valid_def big_step_pres_approx_b)
   1.257 -
   1.258 -lemma bfold_equiv: 
   1.259 +lemma bfold_equiv:
   1.260    "approx t \<Turnstile> c \<sim> bfold c t"
   1.261  proof (induction c arbitrary: t)
   1.262    case SKIP show ?case by simp
   1.263 @@ -378,28 +366,28 @@
   1.264    thus ?case by (simp add: equiv_up_to_def)
   1.265  next
   1.266    case Seq
   1.267 -  thus ?case by (auto intro!: equiv_up_to_seq)           
   1.268 +  thus ?case by (auto intro!: equiv_up_to_seq big_step_pres_approx_b)
   1.269  next
   1.270    case (If b c1 c2)
   1.271 -  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim> 
   1.272 +  hence "approx t \<Turnstile> IF b THEN c1 ELSE c2 \<sim>
   1.273                     IF Fold.bsimp_const b t THEN bfold c1 t ELSE bfold c2 t"
   1.274 -    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def) 
   1.275 +    by (auto intro: equiv_up_to_if_weak simp: bequiv_up_to_def)
   1.276    thus ?case using If
   1.277 -    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits 
   1.278 +    by (fastforce simp: bvalsimp_const_Bc split: bexp.splits bool.splits
   1.279                   intro: equiv_up_to_trans)
   1.280    next
   1.281    case (While b c)
   1.282 -  hence "approx (t |` (- lnames c)) \<Turnstile> 
   1.283 +  hence "approx (t |` (- lnames c)) \<Turnstile>
   1.284                     WHILE b DO c \<sim>
   1.285 -                   WHILE bsimp_const b (t |` (- lnames c)) 
   1.286 -                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'") 
   1.287 -    by (auto intro: equiv_up_to_while_weak approx_restrict_inv 
   1.288 +                   WHILE bsimp_const b (t |` (- lnames c))
   1.289 +                      DO bfold c (t |` (- lnames c))" (is "_ \<Turnstile> ?W \<sim> ?W'")
   1.290 +    by (auto intro: equiv_up_to_while_weak big_step_pres_approx_restrict
   1.291               simp: bequiv_up_to_def)
   1.292    hence "approx t \<Turnstile> ?W \<sim> ?W'"
   1.293      by (auto intro: equiv_up_to_weaken approx_map_le)
   1.294    thus ?case
   1.295 -    by (auto split: bexp.splits bool.splits 
   1.296 -             intro: equiv_up_to_while_False 
   1.297 +    by (auto split: bexp.splits bool.splits
   1.298 +             intro: equiv_up_to_while_False
   1.299               simp: bvalsimp_const_Bc)
   1.300  qed
   1.301  
     2.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Wed Aug 22 23:45:49 2012 +0200
     2.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Thu Aug 23 15:32:22 2012 +0200
     2.3 @@ -1,17 +1,19 @@
     2.4  header "Semantic Equivalence up to a Condition"
     2.5  
     2.6  theory Sem_Equiv
     2.7 -imports Hoare_Sound_Complete
     2.8 +imports Big_Step
     2.9  begin
    2.10  
    2.11 +type_synonym assn = "state \<Rightarrow> bool"
    2.12 +
    2.13  definition
    2.14    equiv_up_to :: "assn \<Rightarrow> com \<Rightarrow> com \<Rightarrow> bool" ("_ \<Turnstile> _ \<sim> _" [60,0,10] 60)
    2.15  where
    2.16    "P \<Turnstile> c \<sim> c' \<equiv> \<forall>s s'. P s \<longrightarrow> (c,s) \<Rightarrow> s' \<longleftrightarrow> (c',s) \<Rightarrow> s'"
    2.17  
    2.18 -definition 
    2.19 +definition
    2.20    bequiv_up_to :: "assn \<Rightarrow> bexp \<Rightarrow> bexp \<Rightarrow> bool" ("_ \<Turnstile> _ <\<sim>> _" [60,0,10] 60)
    2.21 -where 
    2.22 +where
    2.23    "P \<Turnstile> b <\<sim>> b' \<equiv> \<forall>s. P s \<longrightarrow> bval b s = bval b' s"
    2.24  
    2.25  lemma equiv_up_to_True:
    2.26 @@ -27,11 +29,11 @@
    2.27    by (unfold equiv_up_to_def) blast
    2.28  
    2.29  lemma equiv_up_toD1:
    2.30 -  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> (c', s) \<Rightarrow> s'"
    2.31 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s'"
    2.32    by (unfold equiv_up_to_def) blast
    2.33  
    2.34  lemma equiv_up_toD2:
    2.35 -  "P \<Turnstile> c \<sim> c' \<Longrightarrow> P s \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> (c, s) \<Rightarrow> s'"
    2.36 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> (c, s) \<Rightarrow> s'"
    2.37    by (unfold equiv_up_to_def) blast
    2.38  
    2.39  
    2.40 @@ -60,32 +62,28 @@
    2.41    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> b' <\<sim>> b'' \<Longrightarrow> P \<Turnstile> b <\<sim>> b''"
    2.42    by (auto simp: bequiv_up_to_def)
    2.43  
    2.44 -
    2.45 -lemma equiv_up_to_hoare:
    2.46 -  "P' \<Turnstile> c \<sim> c' \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
    2.47 -  unfolding hoare_valid_def equiv_up_to_def by blast
    2.48 -
    2.49 -lemma equiv_up_to_hoare_eq:
    2.50 -  "P \<Turnstile> c \<sim> c' \<Longrightarrow> (\<Turnstile> {P} c {Q}) = (\<Turnstile> {P} c' {Q})"
    2.51 -  by (rule equiv_up_to_hoare)
    2.52 +lemma bequiv_up_to_subst:
    2.53 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P s \<Longrightarrow> bval b s = bval b' s"
    2.54 +  by (simp add: bequiv_up_to_def)
    2.55  
    2.56  
    2.57  lemma equiv_up_to_seq:
    2.58 -  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow> \<Turnstile> {P} c {Q} \<Longrightarrow>
    2.59 +  "P \<Turnstile> c \<sim> c' \<Longrightarrow> Q \<Turnstile> d \<sim> d' \<Longrightarrow>
    2.60 +  (\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
    2.61    P \<Turnstile> (c; d) \<sim> (c'; d')"
    2.62 -  by (clarsimp simp: equiv_up_to_def hoare_valid_def) blast
    2.63 +  by (clarsimp simp: equiv_up_to_def) blast
    2.64  
    2.65  lemma equiv_up_to_while_lemma:
    2.66 -  shows "(d,s) \<Rightarrow> s' \<Longrightarrow> 
    2.67 +  shows "(d,s) \<Rightarrow> s' \<Longrightarrow>
    2.68           P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
    2.69 -         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
    2.70 -         \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
    2.71 -         P s \<Longrightarrow> 
    2.72 -         d = WHILE b DO c \<Longrightarrow> 
    2.73 -         (WHILE b' DO c', s) \<Rightarrow> s'"  
    2.74 +         (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow>
    2.75 +         (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
    2.76 +         P s \<Longrightarrow>
    2.77 +         d = WHILE b DO c \<Longrightarrow>
    2.78 +         (WHILE b' DO c', s) \<Rightarrow> s'"
    2.79  proof (induction rule: big_step_induct)
    2.80    case (WhileTrue b s1 c s2 s3)
    2.81 -  note IH = WhileTrue.IH(2) [OF WhileTrue.prems(1-3) _ WhileTrue.prems(5)]
    2.82 +  hence IH: "P s2 \<Longrightarrow> (WHILE b' DO c', s2) \<Rightarrow> s3" by auto
    2.83    from WhileTrue.prems
    2.84    have "P \<Turnstile> b <\<sim>> b'" by simp
    2.85    with `bval b s1` `P s1`
    2.86 @@ -97,38 +95,46 @@
    2.87    have "(c', s1) \<Rightarrow> s2" by (simp add: equiv_up_to_def)
    2.88    moreover
    2.89    from WhileTrue.prems
    2.90 -  have "\<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P}" by simp
    2.91 +  have "\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'" by simp
    2.92    with `P s1` `bval b s1` `(c, s1) \<Rightarrow> s2`
    2.93 -  have "P s2" by (simp add: hoare_valid_def)
    2.94 +  have "P s2" by simp
    2.95    hence "(WHILE b' DO c', s2) \<Rightarrow> s3" by (rule IH)
    2.96 -  ultimately 
    2.97 +  ultimately
    2.98    show ?case by blast
    2.99  next
   2.100    case WhileFalse
   2.101    thus ?case by (auto simp: bequiv_up_to_def)
   2.102 -qed (fastforce simp: equiv_up_to_def bequiv_up_to_def hoare_valid_def)+
   2.103 +qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+
   2.104  
   2.105  lemma bequiv_context_subst:
   2.106    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (P s \<and> bval b s) = (P s \<and> bval b' s)"
   2.107    by (auto simp: bequiv_up_to_def)
   2.108  
   2.109  lemma equiv_up_to_while:
   2.110 -  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> 
   2.111 -   \<Turnstile> {\<lambda>s. P s \<and> bval b s} c {P} \<Longrightarrow> 
   2.112 -   P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   2.113 -  apply (safe intro!: equiv_up_toI)
   2.114 -   apply (auto intro: equiv_up_to_while_lemma)[1]
   2.115 -  apply (simp add: equiv_up_to_hoare_eq bequiv_context_subst)
   2.116 -  apply (drule equiv_up_to_sym [THEN iffD1])
   2.117 -  apply (drule bequiv_up_to_sym [THEN iffD1])
   2.118 -  apply (auto intro: equiv_up_to_while_lemma)[1]
   2.119 -  done
   2.120 +  assumes b: "P \<Turnstile> b <\<sim>> b'"
   2.121 +  assumes c: "(\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c'"
   2.122 +  assumes I: "\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s'"
   2.123 +  shows "P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   2.124 +proof -
   2.125 +  from b have b': "P \<Turnstile> b' <\<sim>> b" by (simp add: bequiv_up_to_sym)
   2.126 +
   2.127 +  from c b have c': "(\<lambda>s. P s \<and> bval b' s) \<Turnstile> c' \<sim> c"
   2.128 +    by (simp add: equiv_up_to_sym bequiv_context_subst)
   2.129 +
   2.130 +  from I
   2.131 +  have I': "\<And>s s'. (c', s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b' s \<Longrightarrow> P s'"
   2.132 +    by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])
   2.133 +
   2.134 +  note equiv_up_to_while_lemma [OF _ b c]
   2.135 +       equiv_up_to_while_lemma [OF _ b' c']
   2.136 +  thus ?thesis using I I' by (auto intro!: equiv_up_toI)
   2.137 +qed
   2.138  
   2.139  lemma equiv_up_to_while_weak:
   2.140 -  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow> \<Turnstile> {P} c {P} \<Longrightarrow> 
   2.141 +  "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> P \<Turnstile> c \<sim> c' \<Longrightarrow>
   2.142 +   (\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
   2.143     P \<Turnstile> WHILE b DO c \<sim> WHILE b' DO c'"
   2.144 -  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken 
   2.145 -               simp: hoare_valid_def)
   2.146 +  by (fastforce elim!: equiv_up_to_while equiv_up_to_weaken)
   2.147  
   2.148  lemma equiv_up_to_if:
   2.149    "P \<Turnstile> b <\<sim>> b' \<Longrightarrow> (\<lambda>s. P s \<and> bval b s) \<Turnstile> c \<sim> c' \<Longrightarrow> (\<lambda>s. P s \<and> \<not>bval b s) \<Turnstile> d \<sim> d' \<Longrightarrow>
   2.150 @@ -142,7 +148,7 @@
   2.151  
   2.152  lemma equiv_up_to_if_True [intro!]:
   2.153    "(\<And>s. P s \<Longrightarrow> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c1"
   2.154 -  by (auto simp: equiv_up_to_def) 
   2.155 +  by (auto simp: equiv_up_to_def)
   2.156  
   2.157  lemma equiv_up_to_if_False [intro!]:
   2.158    "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> IF b THEN c1 ELSE c2 \<sim> c2"
   2.159 @@ -154,7 +160,7 @@
   2.160  
   2.161  lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
   2.162   by (induct rule: big_step_induct) auto
   2.163 -  
   2.164 +
   2.165  lemma equiv_up_to_while_True [intro!,simp]:
   2.166    "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
   2.167    unfolding equiv_up_to_def