--- a/src/HOL/IMP/Abs_Int1.thy Thu Sep 13 17:20:44 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Fri Sep 14 10:01:42 2012 +0200
@@ -28,8 +28,11 @@
wt I X \<and> vars b \<subseteq> X \<and> wt P X \<and> wt C X \<and> wt Q X"
by(auto simp add: wt_acom_def)
-lemma wt_post[simp]: "wt c X \<Longrightarrow> wt (post c) X"
-by(induction c)(auto simp: wt_acom_def)
+lemma post_in_annos: "post C : set(annos C)"
+by(induction C) auto
+
+lemma wt_post[simp]: "wt C X \<Longrightarrow> wt (post C) X"
+by(simp add: wt_acom_def post_in_annos)
lemma lpfp_inv:
assumes "lpfp f x0 = Some x" and "\<And>x. P x \<Longrightarrow> P(f x)" and "P(bot x0)"
--- a/src/HOL/IMP/Abs_State.thy Thu Sep 13 17:20:44 2012 +0200
+++ b/src/HOL/IMP/Abs_State.thy Fri Sep 14 10:01:42 2012 +0200
@@ -52,7 +52,7 @@
definition wt_option where
"wt opt X = (case opt of None \<Rightarrow> True | Some x \<Rightarrow> wt x X)"
-lemma wt_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
+lemma wt_option_simps[simp]: "wt None X" "wt (Some x) X = wt x X"
by(simp_all add: wt_option_def)
instance ..