equal
deleted
inserted
replaced
151 "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto |
151 "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto |
152 from WhileTrue(5)[OF this(2)] obtain t3 |
152 from WhileTrue(5)[OF this(2)] obtain t3 |
153 where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X" |
153 where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X" |
154 by auto |
154 by auto |
155 with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto |
155 with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto |
156 (* FIXME why does s/h fail here? *) |
|
157 qed |
156 qed |
158 |
157 |
159 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'" |
158 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'" |
160 using bury_sound[of c s s' UNIV] |
159 using bury_sound[of c s s' UNIV] |
161 by (auto simp: fun_eq_iff[symmetric]) |
160 by (auto simp: fun_eq_iff[symmetric]) |