--- a/src/HOL/IMP/Abs_Int0.thy Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Thu May 16 02:13:23 2013 +0200
@@ -93,10 +93,10 @@
definition bot :: "com \<Rightarrow> 'a option acom" where
-"bot c = anno None c"
+"bot c = annotate (\<lambda>p. None) c"
lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
-by(induct C arbitrary: c)(auto simp: bot_def)
+by(auto simp: bot_def less_eq_acom_def)
lemma strip_bot[simp]: "strip(bot c) = c"
by(simp add: bot_def)
@@ -206,7 +206,7 @@
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
+by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])
text{* Correctness: *}
@@ -247,9 +247,6 @@
subsubsection "Monotonicity"
-lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
-by(induction C1 C2 rule: less_eq_acom.induct) (auto)
-
locale Abs_Int_fun_mono = Abs_Int_fun +
assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
begin
@@ -307,6 +304,9 @@
by (blast intro: I mono)
qed
+lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
+ strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
+by(simp add: less_eq_acom_def anno_def)
locale Measure1_fun =
fixes m :: "'av::top \<Rightarrow> nat"
@@ -345,15 +345,6 @@
end
-lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
- (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
-by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
-
-lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
- strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
-by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
-
-
locale Measure_fun = Measure1_fun where m=m
for m :: "'av::semilattice_sup_top \<Rightarrow> nat" +
assumes m2: "x < y \<Longrightarrow> m x > m y"