# HG changeset patch
# User nipkow
# Date 1366484269 -7200
# Node ID 3da99469cc1b33f51aee3535ac6a92d785c97eb5
# Parent  8417feab782efaa8412ec888b415797aeaa92b85
proved termination for fun-based AI

diff -r 8417feab782e -r 3da99469cc1b src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Sat Apr 20 19:30:04 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Sat Apr 20 20:57:49 2013 +0200
@@ -102,7 +102,7 @@
 by(simp add: bot_def)
 
 
-subsubsection "Post-fixed point iteration"
+subsubsection "Pre-fixpoint iteration"
 
 definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
 "pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
@@ -171,6 +171,9 @@
 
 definition "step' = Step fa (\<lambda>b S. S)"
 
+lemma strip_step'[simp]: "strip(step' S C) = strip C"
+by(simp add: step'_def)
+
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
 "AI c = pfp (step' \<top>) (bot c)"
 
@@ -257,6 +260,223 @@
 by(rule mono2_Step)
   (auto simp: mono_update mono_aval' fa_def split: option.split)
 
+lemma mono_step'_top: "C \<le> C' \<Longrightarrow> step' \<top> C \<le> step' \<top> C'"
+by (metis mono_step' order_refl)
+
+lemma AI_least_pfp: assumes "AI c = Some C" "step' \<top> C' \<le> C'" "strip C' = c"
+shows "C \<le> C'"
+by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
+  (simp_all add: mono_step'_top)
+
+end
+
+
+instantiation acom :: (type) vars
+begin
+
+definition "vars_acom = vars o strip"
+
+instance ..
+
+end
+
+lemma finite_Cvars: "finite(vars(C::'a acom))"
+by(simp add: vars_acom_def)
+
+
+subsubsection "Termination"
+
+lemma pfp_termination:
+fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
+assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
+and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
+and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
+shows "\<exists>x. pfp f x0 = Some x"
+proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
+  show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
+    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
+next
+  show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
+next
+  fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
+    by (blast intro: I mono)
+qed
+
+
+locale Measure1_fun =
+fixes m :: "'av::{order,top} \<Rightarrow> nat"
+fixes h :: "nat"
+assumes h: "m x \<le> h"
+begin
+
+definition m_s :: "vname set \<Rightarrow> 'av st \<Rightarrow> nat" ("m\<^isub>s") where
+"m_s X S = (\<Sum> x \<in> X. m(S x))"
+
+lemma m_s_h: "finite X \<Longrightarrow> m_s X S \<le> h * card X"
+by(simp add: m_s_def) (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
+
+definition m_o :: "vname set \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where
+"m_o X opt = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s X S)"
+
+lemma m_o_h: "finite X \<Longrightarrow> m_o X opt \<le> (h*card X + 1)"
+by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
+
+definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
+"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
+
+text{* Upper complexity bound: *}
+lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
+proof-
+  let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
+  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
+  also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
+    apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
+  also have "\<dots> = ?a * (h * ?n + 1)" by simp
+  finally show ?thesis .
+qed
+
+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)
+
+
+text{* The predicates @{text "top_on_ty X a"} that follow describe that @{text a} is some object
+that maps all variables in @{text X} to @{term \<top>}.
+This is an important invariant for the termination proof where we argue that only
+the finitely many variables in the program change. That the others do not change
+follows because they remain @{term \<top>}. *}
+
+fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
+"top_on_st X f = (\<forall>x\<in>X. f x = \<top>)"
+
+fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
+"top_on_opt X (Some F) = top_on_st X F" |
+"top_on_opt X None = True"
+
+definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
+"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
+
+lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
+by(auto simp: top_option_def)
+
+lemma top_on_bot: "top_on_acom X (bot c)"
+by(auto simp add: top_on_acom_def bot_def)
+
+lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
+by(simp add: top_on_acom_def post_in_annos)
+
+lemma top_on_acom_simps:
+  "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
+  "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
+  "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
+  "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+   (top_on_opt X P1 \<and> top_on_acom X C1 \<and> top_on_opt X P2 \<and> top_on_acom X C2 \<and> top_on_opt X Q)"
+  "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
+   (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
+by(auto simp add: top_on_acom_def)
+
+lemma top_on_sup:
+  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
+apply(induction o1 o2 rule: sup_option.induct)
+apply(auto)
+done
+
+lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
+assumes "!!x e S. \<lbrakk>top_on_opt X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (f x e S)"
+        "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
+shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt X S; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (Step f g S C)"
+proof(induction C arbitrary: S)
+qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
+
+
+locale Measure_fun = Measure1_fun +
+assumes m2: "x < y \<Longrightarrow> m x > m y"
+begin
+
+lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
+by(auto simp: le_less m2)
+
+lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "\<forall>x. S1 x \<le> S2 x" and "S1 \<noteq> S2"
+shows "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))"
+proof-
+  from assms(3) have 1: "\<forall>x\<in>X. m(S1 x) \<ge> m(S2 x)" by (simp add: m1)
+  from assms(2,3,4) have "EX x:X. S1 x < S2 x"
+    by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
+  hence 2: "\<exists>x\<in>X. m(S1 x) > m(S2 x)" by (metis m2)
+  from setsum_strict_mono_ex1[OF `finite X` 1 2]
+  show "(\<Sum>x\<in>X. m (S2 x)) < (\<Sum>x\<in>X. m (S1 x))" .
+qed
+
+lemma m_s2: "finite(X) \<Longrightarrow> S1 = S2 on -X \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s X S1 > m_s X S2"
+apply(auto simp add: less_fun_def m_s_def)
+apply(simp add: m_s2_rep le_fun_def)
+done
+
+lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
+  o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
+  case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
+next
+  case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
+next
+  case 3 thus ?case by (auto simp: less_option_def)
+qed
+
+lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
+  o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
+by(auto simp: le_less m_o2)
+
+
+lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
+  C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
+proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
+  let ?X = "vars(strip C2)"
+  assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
+  and strip_eq: "strip C1 = strip C2"
+  and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
+  hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
+    apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
+    by (metis (lifting, no_types) finite_cvars m_o1 size_annos_same2)
+  fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
+  have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
+    using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+  have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
+    using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
+  from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
+    by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
+  hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
+  show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
+         < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
+    apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
+qed
+
+end
+
+
+locale Abs_Int_fun_measure =
+  Abs_Int_fun_mono where \<gamma>=\<gamma> + Measure_fun where m=m
+  for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
+begin
+
+lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
+unfolding step'_def
+by(rule top_on_Step)
+  (auto simp add: top_option_def fa_def split: option.splits)
+
+lemma AI_Some_measure: "\<exists>C. AI c = Some C"
+unfolding AI_def
+apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
+apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
+apply(auto simp add: top_on_step' vars_acom_def)
+done
+
 end
 
 text{* Problem: not executable because of the comparison of abstract states,
diff -r 8417feab782e -r 3da99469cc1b src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Sat Apr 20 19:30:04 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Sat Apr 20 20:57:49 2013 +0200
@@ -4,28 +4,6 @@
 imports Abs_State
 begin
 
-instantiation acom :: (type) vars
-begin
-
-definition "vars_acom = vars o strip"
-
-instance ..
-
-end
-
-lemma finite_Cvars: "finite(vars(C::'a acom))"
-by(simp add: vars_acom_def)
-
-
-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)
-
-
 subsection "Computable Abstract Interpretation"
 
 text{* Abstract interpretation over type @{text st} instead of functions. *}
@@ -100,17 +78,6 @@
 
 subsubsection "Monotonicity"
 
-lemma le_sup_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> (z::_::semilattice_sup)"
-by (metis sup_ge1 sup_ge2 order_trans)
-
-theorem mono2_Step: fixes C1 :: "'a::semilattice acom"
-  assumes "!!x e S1 S2. S1 \<le> S2 \<Longrightarrow> f x e S1 \<le> f x e S2"
-          "!!b S1 S2. S1 \<le> S2 \<Longrightarrow> g b S1 \<le> g b S2"
-  shows "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> Step f g S1 C1 \<le> Step f g S2 C2"
-by(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
-  (auto simp: mono_post assms le_sup_disj)
-
-
 locale Abs_Int_mono = Abs_Int +
 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin
@@ -135,23 +102,6 @@
 
 subsubsection "Termination"
 
-lemma pfp_termination:
-fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
-assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
-and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
-and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
-shows "\<exists>x. pfp f x0 = Some x"
-proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
-  show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
-    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
-next
-  show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
-next
-  fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
-    by (blast intro: I mono)
-qed
-
-
 locale Measure1 =
 fixes m :: "'av::{order,top} \<Rightarrow> nat"
 fixes h :: "nat"
@@ -186,75 +136,45 @@
 
 end
 
-text{* The predicates @{text "top_on X a"} that follow describe that @{text a} is some object
-that maps all variables in @{text X} to @{term \<top>}.
-This is an important invariant for the termination proof where we argue that only
-the finitely many variables in the program change. That the others do not change
-follows because they remain @{term \<top>}. *}
-
-class top_on =
-fixes top_on :: "vname set \<Rightarrow> 'a \<Rightarrow> bool"
-
-instantiation st :: (top)top_on
-begin
-
-fun top_on_st :: "vname set \<Rightarrow> 'a st \<Rightarrow> bool" where
+fun top_on_st :: "vname set \<Rightarrow> 'a::top st \<Rightarrow> bool" where
 "top_on_st X F = (\<forall>x\<in>X. fun F x = \<top>)"
 
-instance ..
-
-end
-
-instantiation option :: (top_on)top_on
-begin
-
-fun top_on_option :: "vname set \<Rightarrow> 'a option \<Rightarrow> bool" where
-"top_on_option X (Some F) = top_on X F" |
-"top_on_option X None = True"
-
-instance ..
+fun top_on_opt :: "vname set \<Rightarrow> 'a::top st option \<Rightarrow> bool" where
+"top_on_opt X (Some F) = top_on_st X F" |
+"top_on_opt X None = True"
 
-end
-
-instantiation acom :: (top_on)top_on
-begin
+definition top_on_acom :: "vname set \<Rightarrow> 'a::top st option acom \<Rightarrow> bool" where
+"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on_opt X a)"
 
-definition top_on_acom :: "vname set \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"top_on_acom X C = (\<forall>a \<in> set(annos C). top_on X a)"
-
-instance ..
-
-end
-
-lemma top_on_top: "top_on X (\<top>::_ st option)"
+lemma top_on_top: "top_on_opt X (\<top>::_ st option)"
 by(auto simp: top_option_def fun_top)
 
-lemma top_on_bot: "top_on X (bot c)"
+lemma top_on_bot: "top_on_acom X (bot c)"
 by(auto simp add: top_on_acom_def bot_def)
 
-lemma top_on_post: "top_on X C \<Longrightarrow> top_on X (post C)"
+lemma top_on_post: "top_on_acom X C \<Longrightarrow> top_on_opt X (post C)"
 by(simp add: top_on_acom_def post_in_annos)
 
 lemma top_on_acom_simps:
-  "top_on X (SKIP {Q}) = top_on X Q"
-  "top_on X (x ::= e {Q}) = top_on X Q"
-  "top_on X (C1;C2) = (top_on X C1 \<and> top_on X C2)"
-  "top_on X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
-   (top_on X P1 \<and> top_on X C1 \<and> top_on X P2 \<and> top_on X C2 \<and> top_on X Q)"
-  "top_on X ({I} WHILE b DO {P} C {Q}) =
-   (top_on X I \<and> top_on X C \<and> top_on X P \<and> top_on X Q)"
+  "top_on_acom X (SKIP {Q}) = top_on_opt X Q"
+  "top_on_acom X (x ::= e {Q}) = top_on_opt X Q"
+  "top_on_acom X (C1;C2) = (top_on_acom X C1 \<and> top_on_acom X C2)"
+  "top_on_acom X (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
+   (top_on_opt X P1 \<and> top_on_acom X C1 \<and> top_on_opt X P2 \<and> top_on_acom X C2 \<and> top_on_opt X Q)"
+  "top_on_acom X ({I} WHILE b DO {P} C {Q}) =
+   (top_on_opt X I \<and> top_on_acom X C \<and> top_on_opt X P \<and> top_on_opt X Q)"
 by(auto simp add: top_on_acom_def)
 
 lemma top_on_sup:
-  "top_on X o1 \<Longrightarrow> top_on X o2 \<Longrightarrow> top_on X (o1 \<squnion> o2 :: _ st option)"
+  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2 \<Longrightarrow> top_on_opt X (o1 \<squnion> o2 :: _ st option)"
 apply(induction o1 o2 rule: sup_option.induct)
 apply(auto)
 by transfer simp
 
 lemma top_on_Step: fixes C :: "('a::semilattice)st option acom"
-assumes "!!x e S. \<lbrakk>top_on X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on X (f x e S)"
-        "!!b S. top_on X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on X (g b S)"
-shows "\<lbrakk> vars C \<subseteq> -X; top_on X S; top_on X C \<rbrakk> \<Longrightarrow> top_on X (Step f g S C)"
+assumes "!!x e S. \<lbrakk>top_on_opt X S; x \<notin> X; vars e \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (f x e S)"
+        "!!b S. top_on_opt X S \<Longrightarrow> vars b \<subseteq> -X \<Longrightarrow> top_on_opt X (g b S)"
+shows "\<lbrakk> vars C \<subseteq> -X; top_on_opt X S; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (Step f g S C)"
 proof(induction C arbitrary: S)
 qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)
 
@@ -283,7 +203,7 @@
 apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)
 done
 
-lemma m_o2: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+lemma m_o2: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
   o1 < o2 \<Longrightarrow> m_o X o1 > m_o X o2"
 proof(induction o1 o2 rule: less_eq_option.induct)
   case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
@@ -293,25 +213,25 @@
   case 3 thus ?case by (auto simp: less_option_def)
 qed
 
-lemma m_o1: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+lemma m_o1: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
   o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
 by(auto simp: le_less m_o2)
 
 
-lemma m_c2: "top_on (-vars C1) C1 \<Longrightarrow> top_on (-vars C2) C2 \<Longrightarrow>
+lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
   C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
 proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
   let ?X = "vars(strip C2)"
-  assume top: "top_on (- vars(strip C2)) C1"  "top_on (- vars(strip C2)) C2"
+  assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
   and strip_eq: "strip C1 = strip C2"
   and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
   hence 1: "\<forall>i<size(annos C2). m_o ?X (annos C1 ! i) \<ge> m_o ?X (annos C2 ! i)"
     apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
     by (metis finite_cvars m_o1 size_annos_same2)
   fix i assume i: "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
-  have topo1: "top_on (- ?X) (annos C1 ! i)"
+  have topo1: "top_on_opt (- ?X) (annos C1 ! i)"
     using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
-  have topo2: "top_on (- ?X) (annos C2 ! i)"
+  have topo2: "top_on_opt (- ?X) (annos C2 ! i)"
     using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
   from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
     by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
@@ -329,14 +249,14 @@
   for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
 begin
 
-lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on X C \<rbrakk> \<Longrightarrow> top_on X (step' \<top> C)"
+lemma top_on_step': "\<lbrakk> vars C \<subseteq> -X; top_on_acom X C \<rbrakk> \<Longrightarrow> top_on_acom X (step' \<top> C)"
 unfolding step'_def
 by(rule top_on_Step)
   (auto simp add: top_option_def fun_top split: option.splits)
 
 lemma AI_Some_measure: "\<exists>C. AI c = Some C"
 unfolding AI_def
-apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on (- vars C) C" and m="m_c"])
+apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
 apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
 apply(auto simp add: top_on_step' vars_acom_def)
 done
diff -r 8417feab782e -r 3da99469cc1b src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Sat Apr 20 19:30:04 2013 +0200
+++ b/src/HOL/IMP/Abs_Int2.thy	Sat Apr 20 20:57:49 2013 +0200
@@ -147,13 +147,13 @@
 lemma strip_step'[simp]: "strip(step' S c) = strip c"
 by(simp add: step'_def)
 
-lemma top_on_afilter: "\<lbrakk> top_on X S;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on X (afilter e a S)"
+lemma top_on_afilter: "\<lbrakk> top_on_opt X S;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt X (afilter e a S)"
 by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
 
-lemma top_on_bfilter: "\<lbrakk>top_on X S; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on X (bfilter b r S)"
+lemma top_on_bfilter: "\<lbrakk>top_on_opt X S; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt X (bfilter b r S)"
 by(induction b arbitrary: r S) (auto simp: top_on_afilter top_on_sup split: prod.split)
 
-lemma top_on_step': "top_on (- vars C) C \<Longrightarrow> top_on (- vars C) (step' \<top> C)"
+lemma top_on_step': "top_on_acom (- vars C) C \<Longrightarrow> top_on_acom (- vars C) (step' \<top> C)"
 unfolding step'_def
 by(rule top_on_Step)
   (auto simp add: top_on_top top_on_bfilter split: option.split)
diff -r 8417feab782e -r 3da99469cc1b src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Sat Apr 20 19:30:04 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Sat Apr 20 20:57:49 2013 +0200
@@ -311,22 +311,26 @@
 
 subsubsection "Generic Termination Proof"
 
-lemma top_on_opt_widen: "top_on X o1 \<Longrightarrow> top_on X o2  \<Longrightarrow> top_on X (o1 \<nabla> o2 :: _ st option)"
+lemma top_on_opt_widen:
+  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2  \<Longrightarrow> top_on_opt X (o1 \<nabla> o2 :: _ st option)"
 apply(induct o1 o2 rule: widen_option.induct)
 apply (auto)
 by transfer simp
 
-lemma top_on_opt_narrow: "top_on X o1 \<Longrightarrow> top_on X o2  \<Longrightarrow> top_on X (o1 \<triangle> o2 :: _ st option)"
+lemma top_on_opt_narrow:
+  "top_on_opt X o1 \<Longrightarrow> top_on_opt X o2  \<Longrightarrow> top_on_opt X (o1 \<triangle> o2 :: _ st option)"
 apply(induct o1 o2 rule: narrow_option.induct)
 apply (auto)
 by transfer simp
 
 lemma top_on_acom_widen:
-  "\<lbrakk>top_on X C1; strip C1 = strip C2; top_on X C2\<rbrakk> \<Longrightarrow> top_on X (C1 \<nabla> C2 :: _ st option acom)"
+  "\<lbrakk>top_on_acom X C1; strip C1 = strip C2; top_on_acom X C2\<rbrakk>
+  \<Longrightarrow> top_on_acom X (C1 \<nabla> C2 :: _ st option acom)"
 by(auto simp add: widen_acom_def top_on_acom_def)(metis top_on_opt_widen in_set_zipE)
 
 lemma top_on_acom_narrow:
-  "\<lbrakk>top_on X C1; strip C1 = strip C2; top_on X C2\<rbrakk> \<Longrightarrow> top_on X (C1 \<triangle> C2 :: _ st option acom)"
+  "\<lbrakk>top_on_acom X C1; strip C1 = strip C2; top_on_acom X C2\<rbrakk>
+  \<Longrightarrow> top_on_acom X (C1 \<triangle> C2 :: _ st option acom)"
 by(auto simp add: narrow_acom_def top_on_acom_def)(metis top_on_opt_narrow in_set_zipE)
 
 text{* The assumptions for widening and narrowing differ because during
@@ -376,7 +380,7 @@
 apply(auto simp add: less_eq_st_rep_iff m_s_widen_rep)
 done
 
-lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on (-X) o1 \<Longrightarrow> top_on (-X) o2 \<Longrightarrow>
+lemma m_o_anti_mono: "finite X \<Longrightarrow> top_on_opt (-X) o1 \<Longrightarrow> top_on_opt (-X) o2 \<Longrightarrow>
   o1 \<le> o2 \<Longrightarrow> m_o X o1 \<ge> m_o X o2"
 proof(induction o1 o2 rule: less_eq_option.induct)
   case 1 thus ?case by (simp add: m_o_def)(metis m_s_anti_mono)
@@ -387,12 +391,12 @@
   case 3 thus ?case by simp
 qed
 
-lemma m_o_widen: "\<lbrakk> finite X; top_on (-X) S1; top_on (-X) S2; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
+lemma m_o_widen: "\<lbrakk> finite X; top_on_opt (-X) S1; top_on_opt (-X) S2; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   m_o X (S1 \<nabla> S2) < m_o X S1"
 by(auto simp: m_o_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
 
 lemma m_c_widen:
-  "strip C1 = strip C2  \<Longrightarrow> top_on (-vars C1) C1 \<Longrightarrow> top_on (-vars C2) C2
+  "strip C1 = strip C2  \<Longrightarrow> top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2
    \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
 apply(auto simp: m_c_def widen_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
@@ -433,7 +437,7 @@
 "n\<^isub>o X opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s X S + 1)"
 
 lemma n_o_narrow:
-  "top_on (-X) S1 \<Longrightarrow> top_on (-X) S2 \<Longrightarrow> finite X
+  "top_on_opt (-X) S1 \<Longrightarrow> top_on_opt (-X) S2 \<Longrightarrow> finite X
   \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> S1 \<triangle> S2 < S1 \<Longrightarrow> n\<^isub>o X (S1 \<triangle> S2) < n\<^isub>o X S1"
 apply(induction S1 S2 rule: narrow_option.induct)
 apply(auto simp: n_o_def n_s_narrow)
@@ -448,7 +452,7 @@
 by(metis (hide_lams, no_types) less_le_not_le le_iff_le_annos size_annos_same2)
 
 lemma n_c_narrow: "strip C1 = strip C2
-  \<Longrightarrow> top_on (- vars C1) C1 \<Longrightarrow> top_on (- vars C2) C2
+  \<Longrightarrow> top_on_acom (- vars C1) C1 \<Longrightarrow> top_on_acom (- vars C2) C2
   \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> C1 \<triangle> C2 < C1 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
 apply(auto simp: n_c_def Let_def narrow_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
@@ -564,15 +568,15 @@
 
 lemma iter_winden_step_ivl_termination:
   "\<exists>C. iter_widen (step_ivl \<top>) (bot c) = Some C"
-apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on (- vars C) C"])
+apply(rule iter_widen_termination[where m = "m_c" and P = "%C. strip C = c \<and> top_on_acom (- vars C) C"])
 apply (auto simp add: m_c_widen top_on_bot top_on_step'[simplified comp_def vars_acom_def]
   vars_acom_def top_on_acom_widen)
 done
 
 lemma iter_narrow_step_ivl_termination:
-  "top_on (- vars C0) C0 \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
+  "top_on_acom (- vars C0) C0 \<Longrightarrow> step_ivl \<top> C0 \<le> C0 \<Longrightarrow>
   \<exists>C. iter_narrow (step_ivl \<top>) C0 = Some C"
-apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on (-vars C) C"])
+apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. strip C0 = strip C \<and> top_on_acom (-vars C) C"])
 apply(auto simp: top_on_step'[simplified comp_def vars_acom_def]
         mono_step'_top n_c_narrow vars_acom_def top_on_acom_narrow)
 done
@@ -583,7 +587,7 @@
            split: option.split)
 apply(rule iter_narrow_step_ivl_termination)
 apply(rule conjunct2)
-apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on (- vars C) C"])
+apply(rule iter_widen_inv[where f = "step' \<top>" and P = "%C. c = strip C & top_on_acom (- vars C) C"])
 apply(auto simp: top_on_acom_widen top_on_step'[simplified comp_def vars_acom_def]
   iter_widen_pfp top_on_bot vars_acom_def)
 done