# HG changeset patch
# User nipkow
# Date 1362582656 -3600
# Node ID 00b45c7e831f038b581cb0db0038418db7f767d0
# Parent  0c376ef98559a035a94cde93759c3445710d2cc9
major redesign: order instead of preorder, new definition of intervals as quotients

diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -6,52 +6,26 @@
 
 subsection "Orderings"
 
-class preord =
-fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
-assumes le_refl[simp]: "x \<sqsubseteq> x"
-and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
-begin
-
-definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
-
-declare le_trans[trans]
+notation
+  Orderings.bot ("\<bottom>") and
+  Orderings.top ("\<top>")
 
-end
+declare order_trans[trans]
 
-text{* Note: no antisymmetry. Allows implementations where some abstract
-element is implemented by two different values @{prop "x \<noteq> y"}
-such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
-needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
-*}
-
-class join = preord +
+class join = order +
 fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
 
-class semilattice = join +
-fixes Top :: "'a" ("\<top>")
-assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
-and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<sqsubseteq> \<top>"
+class semilattice = join + top +
+assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
+and join_ge2 [simp]: "y \<le> x \<squnion> y"
+and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
 begin
 
-lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
-by (metis join_ge1 join_ge2 join_least le_trans)
-
-lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
-by (metis join_ge1 join_ge2 le_trans)
-
-end
+lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
+by (metis join_ge1 join_ge2 join_least order_trans)
 
-instantiation "fun" :: (type, preord) preord
-begin
-
-definition "f \<sqsubseteq> g = (\<forall>x. f x \<sqsubseteq> g x)"
-
-instance
-proof
-  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
-qed (simp_all add: le_fun_def)
+lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
+by (metis join_ge1 join_ge2 order_trans)
 
 end
 
@@ -60,81 +34,41 @@
 begin
 
 definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
-definition "\<top> = (\<lambda>x. \<top>)"
 
 lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
 by (simp add: join_fun_def)
 
 instance
 proof
-qed (simp_all add: le_fun_def Top_fun_def)
+qed (simp_all add: le_fun_def)
 
 end
 
 
-instantiation acom :: (preord) preord
+instantiation option :: (order)order
 begin
 
-fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
-"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
-"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
-"le_acom (C1;C2) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
-"le_acom (IF b THEN {p1} C1 ELSE {p2} C2 {S}) (IF b' THEN {q1} D1 ELSE {q2} D2 {S'}) =
-  (b=b' \<and> p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
-"le_acom ({I} WHILE b DO {p} C {P}) ({I'} WHILE b' DO {p'} C' {P'}) =
-  (b=b' \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
-"le_acom _ _ = False"
-
-lemma [simp]: "SKIP {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = SKIP {S'} \<and> S \<sqsubseteq> S')"
-by (cases C) auto
-
-lemma [simp]: "x ::= e {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = x ::= e {S'} \<and> S \<sqsubseteq> S')"
-by (cases C) auto
-
-lemma [simp]: "C1;C2 \<sqsubseteq> C \<longleftrightarrow> (\<exists>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)"
-by (cases C) auto
-
-lemma [simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<sqsubseteq> C \<longleftrightarrow>
-  (\<exists>q1 q2 D1 D2 S'. C = IF b THEN {q1} D1 ELSE {q2} D2 {S'} \<and>
-     p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
-by (cases C) auto
+fun less_eq_option where
+"Some x \<le> Some y = (x \<le> y)" |
+"None \<le> y = True" |
+"Some _ \<le> None = False"
 
-lemma [simp]: "{I} WHILE b DO {p} C {P} \<sqsubseteq> W \<longleftrightarrow>
-  (\<exists>I' p' C' P'. W = {I'} WHILE b DO {p'} C' {P'} \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')"
-by (cases W) auto
+definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
 
-instance
-proof
-  case goal1 thus ?case by (induct x) auto
-next
-  case goal2 thus ?case
-  apply(induct x y arbitrary: z rule: le_acom.induct)
-  apply (auto intro: le_trans)
-  done
-qed
-
-end
-
-
-instantiation option :: (preord)preord
-begin
-
-fun le_option where
-"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
-"None \<sqsubseteq> y = True" |
-"Some _ \<sqsubseteq> None = False"
-
-lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
+lemma [simp]: "(x \<le> None) = (x = None)"
 by (cases x) simp_all
 
-lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y \<and> x \<sqsubseteq> y)"
+lemma [simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
 by (cases u) auto
 
 instance proof
-  case goal1 show ?case by(cases x, simp_all)
+  case goal1 show ?case by(rule less_option_def)
+next
+  case goal2 show ?case by(cases x, simp_all)
 next
-  case goal2 thus ?case
-    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
+  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
+next
+  case goal4 thus ?case by(cases y, simp, cases x, auto)
 qed
 
 end
@@ -157,25 +91,21 @@
 instantiation option :: (semilattice)semilattice
 begin
 
-definition "\<top> = Some \<top>"
+definition top_option where "\<top> = Some \<top>"
 
 instance proof
-  case goal1 thus ?case by(cases x, simp, cases y, simp_all)
+  case goal1 show ?case by(cases a, simp_all add: top_option_def)
 next
-  case goal2 thus ?case by(cases y, simp, cases x, simp_all)
+  case goal2 thus ?case by(cases x, simp, cases y, simp_all)
 next
-  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
+  case goal3 thus ?case by(cases y, simp, cases x, simp_all)
 next
-  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
+  case goal4 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 qed
 
 end
 
-class bot = preord +
-fixes bot :: "'a" ("\<bottom>")
-assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
-
-instantiation option :: (preord)bot
+instantiation option :: (order)bot
 begin
 
 definition bot_option :: "'a option" where
@@ -192,7 +122,7 @@
 definition bot :: "com \<Rightarrow> 'a option acom" where
 "bot c = anno None c"
 
-lemma bot_least: "strip C = c \<Longrightarrow> bot c \<sqsubseteq> C"
+lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
 by(induct C arbitrary: c)(auto simp: bot_def)
 
 lemma strip_bot[simp]: "strip(bot c) = c"
@@ -201,20 +131,21 @@
 
 subsubsection "Post-fixed point iteration"
 
-definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
-"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
+definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
+"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
 
-lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
+lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
 using while_option_stop[OF assms[simplified pfp_def]] by simp
 
 lemma while_least:
-assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
-and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L"
+fixes q :: "'a::order"
+assumes "\<forall>x\<in>L.\<forall>y\<in>L. x \<le> y \<longrightarrow> f x \<le> f y" and "\<forall>x. x \<in> L \<longrightarrow> f x \<in> L"
+and "\<forall>x \<in> L. b \<le> x" and "b \<in> L" and "f q \<le> q" and "q \<in> L"
 and "while_option P f b = Some p"
-shows "p \<sqsubseteq> q"
+shows "p \<le> q"
 using while_option_rule[OF _  assms(7)[unfolded pfp_def],
-                        where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"]
-by (metis assms(1-6) le_trans)
+                        where P = "%x. x \<in> L \<and> x \<le> q"]
+by (metis assms(1-6) order_trans)
 
 lemma pfp_inv:
   "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
@@ -238,7 +169,7 @@
 
 locale Val_abs =
 fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set"
-  assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
+  assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
   and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
 fixes num' :: "val \<Rightarrow> 'av"
 and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
@@ -284,21 +215,21 @@
 abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s Top = UNIV"
-by(simp add: Top_fun_def \<gamma>_fun_def)
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
+by(simp add: top_fun_def \<gamma>_fun_def)
 
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
-by (simp add: Top_option_def)
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o \<top> = UNIV"
+by (simp add: top_option_def)
 
-lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
+lemma mono_gamma_s: "f1 \<le> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
 by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
 
 lemma mono_gamma_o:
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
+  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
 
-lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
+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)
 
 text{* Soundness: *}
 
@@ -326,7 +257,7 @@
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
   assume 1: "pfp (step' \<top>) (bot c) = Some C"
-  have pfp': "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
+  have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
   have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
   proof(rule order_trans)
     show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
@@ -343,21 +274,21 @@
 
 subsubsection "Monotonicity"
 
-lemma mono_post: "C1 \<sqsubseteq> C2 \<Longrightarrow> post C1 \<sqsubseteq> post C2"
-by(induction C1 C2 rule: le_acom.induct) (auto)
+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 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin
 
-lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
+lemma mono_aval': "S \<le> S' \<Longrightarrow> aval' e S \<le> aval' e S'"
 by(induction e)(auto simp: le_fun_def mono_plus')
 
-lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
+lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
 by(simp add: le_fun_def)
 
-lemma mono_step': "S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
 apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
             split: option.split)
 done
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -4,16 +4,16 @@
 imports Abs_State
 begin
 
-lemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
- (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) \<and> strip C1 = strip C2"
-by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)
+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 \<sqsubseteq> C2 \<longleftrightarrow>
-  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"
+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)
 
 
-lemma mono_fun_L[simp]: "F \<in> L X \<Longrightarrow> F \<sqsubseteq> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
+lemma mono_fun_L[simp]: "F \<in> L X \<Longrightarrow> F \<le> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<le> fun G x"
 by(simp add: mono_fun L_st_def)
 
 lemma bot_in_L[simp]: "bot c \<in> L(vars c)"
@@ -71,7 +71,7 @@
    {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
 
 definition AI :: "com \<Rightarrow> 'av st option acom option" where
-"AI c = pfp (step' (top(vars c))) (bot c)"
+"AI c = pfp (step' (Top(vars c))) (bot c)"
 
 
 lemma strip_step'[simp]: "strip(step' S C) = strip C"
@@ -94,7 +94,7 @@
   case Seq thus ?case by auto
 next
   case (If b p1 C1 p2 C2 P)
-  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+  hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
     by(simp, metis post_in_L join_ge1 join_ge2)
   thus ?case using If by (auto simp: mono_gamma_o)
 next
@@ -105,26 +105,26 @@
   "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> (step' S C) \<in> L X"
 proof(induction C arbitrary: S)
   case Assign thus ?case
-    by(auto simp: L_st_def update_def split: option.splits)
+    by(auto simp: L_st_def split: option.splits)
 qed auto
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
+  assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
-      (erule step'_in_L[OF _ top_in_L])
-  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+      (erule step'_in_L[OF _ Top_in_L])
+  have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
-      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
-    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
+    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
+      by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
+    show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF pfp'])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
+  have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -134,41 +134,41 @@
 subsubsection "Monotonicity"
 
 lemma le_join_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
-  x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
-by (metis join_ge1 join_ge2 preord_class.le_trans)
+  x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
+by (metis join_ge1 join_ge2 order_trans)
 
 locale Abs_Int_mono = Abs_Int +
-assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
 begin
 
 lemma mono_aval':
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
-by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
+  "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
+by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
 
 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
-  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+  S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
 apply (auto simp: Let_def mono_aval' mono_post
   le_join_disj le_join_disj[OF  post_in_L post_in_L]
             split: option.split)
 done
 
 lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
-  C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
-by (metis top_in_L mono_step' preord_class.le_refl)
+  C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
+by (metis Top_in_L mono_step' order_refl)
 
 lemma pfp_bot_least:
 assumes "\<forall>x\<in>L(vars c)\<inter>{C. strip C = c}.\<forall>y\<in>L(vars c)\<inter>{C. strip C = c}.
-  x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
+  x \<le> y \<longrightarrow> f x \<le> f y"
 and "\<forall>C. C \<in> L(vars c)\<inter>{C. strip C = c} \<longrightarrow> f C \<in> L(vars c)\<inter>{C. strip C = c}"
-and "f C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
-shows "C \<sqsubseteq> C'"
+and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
+shows "C \<le> C'"
 apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
 by (simp_all add: assms(4,5) bot_least)
 
 lemma AI_least_pfp: assumes "AI c = Some C"
-and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
-shows "C \<sqsubseteq> C'"
+and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
+shows "C \<le> C'"
 apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
 by (simp_all add: mono_step'_top)
 
@@ -177,30 +177,27 @@
 
 subsubsection "Termination"
 
-abbreviation sqless (infix "\<sqsubset>" 50) where
-"x \<sqsubset> y == x \<sqsubseteq> y \<and> \<not> y \<sqsubseteq> x"
-
 lemma pfp_termination:
-fixes x0 :: "'a::preord" and m :: "'a \<Rightarrow> nat"
-assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
-and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
+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 \<sqsubseteq> f x"])
-  show "wf {(y,x). ((I x \<and> x \<sqsubseteq> f x) \<and> \<not> f x \<sqsubseteq> x) \<and> y = f 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 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blast
+  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 \<sqsubseteq> f x" thus "I(f x) \<and> f x \<sqsubseteq> f(f x)"
+  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::preord \<Rightarrow> nat"
+fixes m :: "'av::order \<Rightarrow> nat"
 fixes h :: "nat"
-assumes m1: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
+assumes m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
 assumes h: "m x \<le> h"
 begin
 
@@ -211,9 +208,9 @@
 by(simp add: L_st_def m_s_def)
   (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
 
-lemma m_s1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
-proof(auto simp add: le_st_def m_s_def)
-  assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+lemma m_s1: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
+proof(auto simp add: less_eq_st_def m_s_def)
+  assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
   hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
   thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
     by (metis setsum_mono)
@@ -226,8 +223,8 @@
 by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)
 
 lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
-  o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
-proof(induction o1 o2 rule: le_option.induct)
+  o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
   case 1 thus ?case by (simp add: m_o_def)(metis m_s1)
 next
   case 2 thus ?case
@@ -257,46 +254,45 @@
 end
 
 locale Measure = Measure1 +
-assumes m2: "x \<sqsubset> y \<Longrightarrow> m x > m y"
+assumes m2: "x < y \<Longrightarrow> m x > m y"
 begin
 
-lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 \<sqsubset> S2 \<Longrightarrow> m_s S1 > m_s S2"
-proof(auto simp add: le_st_def m_s_def)
-  assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
+lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2"
+proof(auto simp add: less_st_def less_eq_st_def m_s_def)
+  assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
   hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
-  fix x assume "x \<in> dom S2" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
-  hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast
+  fix x assume "x \<in> dom S2" "\<not> fun S2 x \<le> fun S1 x"
+  hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" by (metis 0 m2 less_le_not_le)
   from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]
   show "(\<Sum>x\<in>dom S2. m (fun S2 x)) < (\<Sum>x\<in>dom S2. m (fun S1 x))" .
 qed
 
 lemma m_o2: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
-  o1 \<sqsubset> o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
-proof(induction o1 o2 rule: le_option.induct)
-  case 1 thus ?case by (simp add: m_o_def L_st_def m_s2)
+  o1 < o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
+proof(induction o1 o2 rule: less_eq_option.induct)
+  case 1 thus ?case by (auto simp: m_o_def L_st_def m_s2 less_option_def)
 next
-  case 2 thus ?case
-    by(auto simp add: m_o_def le_imp_less_Suc m_s_h)
+  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 simp
+  case 3 thus ?case by (auto simp: less_option_def)
 qed
 
-
+find_theorems "(_<_) = _"
 lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
-  C1 \<sqsubset> 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] L_acom_def)
+  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] less_acom_def L_acom_def)
   let ?X = "vars(strip C2)"
   let ?n = "card ?X"
   assume V1: "\<forall>a\<in>set(annos C1). a \<in> L ?X"
     and V2: "\<forall>a\<in>set(annos C2). a \<in> L ?X"
     and strip_eq: "strip C1 = strip C2"
-    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<sqsubseteq> annos C2 ! i"
+    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
   hence 1: "\<forall>i<size(annos C2). m_o ?n (annos C1 ! i) \<ge> m_o ?n (annos C2 ! i)"
     by (auto simp: all_set_conv_all_nth)
        (metis finite_cvars m_o1 size_annos_same2)
-  fix i assume "i < size(annos C2)" "\<not> annos C2 ! i \<sqsubseteq> annos C1 ! i"
+  fix i assume "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
   hence "m_o ?n (annos C1 ! i) > m_o ?n (annos C2 ! i)" (is "?P i")
-    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0)
+    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0 less_option_def)
   hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
   show "(\<Sum>i<size(annos C2). m_o ?n (annos C2 ! i))
          < (\<Sum>i<size(annos C2). m_o ?n (annos C1 ! i))"
@@ -312,8 +308,7 @@
 
 lemma AI_Some_measure: "\<exists>C. AI c = Some C"
 unfolding AI_def
-apply(rule pfp_termination[where I = "%C. strip C = c \<and> C \<in> L(vars c)"
-  and m="m_c"])
+apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> C \<in> L(vars c)" and m="m_c"])
 apply(simp_all add: m_c2 mono_step'_top bot_least)
 done
 
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -23,10 +23,12 @@
 instantiation const :: semilattice
 begin
 
-fun le_const where
-"_ \<sqsubseteq> Any = True" |
-"Const n \<sqsubseteq> Const m = (n=m)" |
-"Any \<sqsubseteq> Const _ = False"
+fun less_eq_const where
+"_ \<le> Any = True" |
+"Const n \<le> Const m = (n=m)" |
+"Any \<le> Const _ = False"
+
+definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
 
 fun join_const where
 "Const m \<squnion> Const n = (if n=m then Const m else Any)" |
@@ -36,17 +38,21 @@
 
 instance
 proof
-  case goal1 thus ?case by (cases x) simp_all
+  case goal1 thus ?case by (rule less_const_def)
+next
+  case goal2 show ?case by (cases x) simp_all
 next
-  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
+  case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal3 thus ?case by(cases x, cases y, simp_all)
+  case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
 next
-  case goal4 thus ?case by(cases y, cases x, simp_all)
+  case goal6 thus ?case by(cases x, cases y, simp_all)
+next
+  case goal7 thus ?case by(cases y, cases x, simp_all)
 next
-  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
+  case goal8 thus ?case by(cases z, cases y, cases x, simp_all)
 next
-  case goal6 thus ?case by(simp add: Top_const_def)
+  case goal5 thus ?case by(simp add: top_const_def)
 qed
 
 end
@@ -58,7 +64,7 @@
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 next
-  case goal2 show ?case by(simp add: Top_const_def)
+  case goal2 show ?case by(simp add: top_const_def)
 next
   case goal3 show ?case by simp
 next
@@ -74,7 +80,7 @@
 
 subsubsection "Tests"
 
-definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)"
 
 value "show_acom (steps test1_const 0)"
 value "show_acom (steps test1_const 1)"
@@ -139,7 +145,7 @@
 next
   case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
 next
-  case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
+  case goal3 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
 qed
 
 thm AI_Some_measure
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -1,3 +1,5 @@
+(* Author: Tobias Nipkow *)
+
 theory Abs_Int1_parity
 imports Abs_Int1
 begin
@@ -6,29 +8,41 @@
 
 datatype parity = Even | Odd | Either
 
-text{* Instantiation of class @{class preord} with type @{typ parity}: *}
+text{* Instantiation of class @{class order} with type @{typ parity}: *}
 
-instantiation parity :: preord
+instantiation parity :: order
 begin
 
-text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
-the header of the definition must refer to the ascii name @{const le} of the
-constants as @{text le_parity} and the definition is named @{text
-le_parity_def}.  Inside the definition the symbolic names can be used. *}
+text{* First the definition of the interface function @{text"\<le>"}. Note that
+the header of the definition must refer to the ascii name @{const less_eq} of the
+constants as @{text less_eq_parity} and the definition is named @{text
+less_eq_parity_def}.  Inside the definition the symbolic names can be used. *}
+
+definition less_eq_parity where
+"x \<le> y = (y = Either \<or> x=y)"
 
-definition le_parity where
-"x \<sqsubseteq> y = (y = Either \<or> x=y)"
+text{* We also need @{text"<"}, which is defined canonically: *}
 
-text{* Now the instance proof, i.e.\ the proof that the definition fulfills
+definition less_parity where
+"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
+
+text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.)
+
+Now the instance proof, i.e.\ the proof that the definition fulfills
 the axioms (assumptions) of the class. The initial proof-step generates the
 necessary proof obligations. *}
 
 instance
 proof
-  fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
+  fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
+next
+  fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
+    by(auto simp: less_eq_parity_def)
 next
-  fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
-    by(auto simp: le_parity_def)
+  fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
+    by(auto simp: less_eq_parity_def)
+next
+  fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
 qed
 
 end
@@ -39,9 +53,9 @@
 begin
 
 definition join_parity where
-"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
+"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
 
-definition Top_parity where
+definition top_parity where
 "\<top> = Either"
 
 text{* Now the instance proof. This time we take a lazy shortcut: we do not
@@ -52,13 +66,13 @@
 
 instance
 proof
-  case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
+  case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
 next
-  case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
+  case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
 next
-  case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
+  case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
 next
-  case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
+  case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def)
 qed
 
 end
@@ -92,10 +106,10 @@
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof txt{* of the locale axioms *}
   fix a b :: parity
-  assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
-    by(auto simp: le_parity_def)
+  assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
+    by(auto simp: less_eq_parity_def)
 next txt{* The rest in the lazy, implicit way *}
-  case goal2 show ?case by(auto simp: Top_parity_def)
+  case goal2 show ?case by(auto simp: top_parity_def)
 next
   case goal3 show ?case by auto
 next
@@ -127,7 +141,7 @@
   ''x'' ::= N 1;
   WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
 
-definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)"
 
 value "show_acom (steps test2_parity 0)"
 value "show_acom (steps test2_parity 1)"
@@ -147,7 +161,7 @@
   case goal1 thus ?case
   proof(cases a1 a2 b1 b2
    rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
-  qed (auto simp add:le_parity_def)
+  qed (auto simp add:less_eq_parity_def)
 qed
 
 definition m_parity :: "parity \<Rightarrow> nat" where
@@ -157,11 +171,11 @@
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 and m = m_parity and h = "1"
 proof
-  case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
+  case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
 next
-  case goal2 thus ?case by(auto simp add: m_parity_def le_parity_def)
+  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
 next
-  case goal3 thus ?case by(auto simp add: m_parity_def le_parity_def)
+  case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
 qed
 
 thm AI_Some_measure
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int2.thy
--- a/src/HOL/IMP/Abs_Int2.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -4,16 +4,21 @@
 imports Abs_Int1
 begin
 
-instantiation prod :: (preord,preord) preord
+instantiation prod :: (order,order) order
 begin
 
-definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
+definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
+definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
 
 instance
 proof
-  case goal1 show ?case by(simp add: le_prod_def)
+  case goal1 show ?case by(rule less_prod_def)
+next
+  case goal2 show ?case by(simp add: less_eq_prod_def)
 next
-  case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
+  case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
+next
+  case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
 qed
 
 end
@@ -23,13 +28,13 @@
 
 class lattice = semilattice + bot +
 fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
-assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
-and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
-and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
+assumes meet_le1 [simp]: "x \<sqinter> y \<le> x"
+and meet_le2 [simp]: "x \<sqinter> y \<le> y"
+and meet_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
 begin
 
-lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
-by (metis meet_greatest meet_le1 meet_le2 le_trans)
+lemma mono_meet: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> x \<sqinter> y \<le> x' \<sqinter> y'"
+by (metis meet_greatest meet_le1 meet_le2 order_trans)
 
 end
 
@@ -83,7 +88,7 @@
 "afilter (N n) a S = (if test_num' n a then S else None)" |
 "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
   let a' = fun S x \<sqinter> a in
-  if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
+  if a' = \<bottom> then None else Some(update S x a'))" |
 "afilter (Plus e1 e2) a S =
  (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
   in afilter e1 a1 (afilter e2 a2 S))"
@@ -110,8 +115,7 @@
 
 lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
 by(induction e arbitrary: a S)
-  (auto simp: Let_def update_def L_st_def
-           split: option.splits prod.split)
+  (auto simp: Let_def L_st_def split: option.splits prod.split)
 
 lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
@@ -189,7 +193,7 @@
   case Seq thus ?case by auto
 next
   case (If b _ C1 _ C2)
-  hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
+  hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
     by(simp, metis post_in_L join_ge1 join_ge2)
   have "vars b \<subseteq> X" using If.prems by simp
   note vars = `S \<in> L X` `vars b \<subseteq> X`
@@ -204,26 +208,26 @@
 
 lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
 proof(induction C arbitrary: S)
-  case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
+  case Assign thus ?case by(auto simp add: L_option_def L_st_def split: option.splits)
 qed (auto simp add: bfilter_in_L)
 
 lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_def)
-  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
+  assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
   have "C \<in> L(vars c)"
     by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
-      (erule step'_in_L[OF _ top_in_L])
-  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
-  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+      (erule step'_in_L[OF _ Top_in_L])
+  have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
+  have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
-      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
-    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
+    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
+      by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
+    show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF pfp'])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
+  have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -233,19 +237,19 @@
 subsubsection "Monotonicity"
 
 locale Abs_Int1_mono = Abs_Int1 +
-assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
-and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
-  filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
-and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
-  filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
+assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
+and mono_filter_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
+  filter_plus' r a1 a2 \<le> filter_plus' r' b1 b2"
+and mono_filter_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
+  filter_less' bv a1 a2 \<le> filter_less' bv b1 b2"
 begin
 
 lemma mono_aval':
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
-by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
+  "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
+by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
 
 lemma mono_aval'':
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"
+  "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
 apply(cases S1)
  apply simp
 apply(cases S2)
@@ -253,37 +257,37 @@
 by (simp add: mono_aval')
 
 lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
-  r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"
+  r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
 apply(induction e arbitrary: r1 r2 S1 S2)
 apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)
 apply (metis mono_gamma subsetD)
 apply(drule (2) mono_fun_L)
-apply (metis mono_meet le_trans)
-apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
+apply (metis mono_meet le_bot)
+apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
 done
 
 lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
-  S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"
+  S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
 apply(induction b arbitrary: bv S1 S2)
 apply(simp)
 apply(simp)
 apply simp
-apply(metis join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] bfilter_in_L)
+apply(metis join_least order_trans[OF _ join_ge1] order_trans[OF _ join_ge2] bfilter_in_L)
 apply (simp split: prod.splits)
-apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
+apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
 done
 
 theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
-  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
-apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
+  S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
+apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
 apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
   le_join_disj le_join_disj[OF  post_in_L post_in_L] bfilter_in_L
             split: option.split)
 done
 
 lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
-  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
-by (metis top_in_L mono_step' preord_class.le_refl)
+  C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
+by (metis Top_in_L mono_step' order_refl)
 
 end
 
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -1,297 +1,341 @@
 (* Author: Tobias Nipkow *)
 
 theory Abs_Int2_ivl
-imports Abs_Int2
+imports "~~/src/HOL/Library/Quotient_List"
+        "~~/src/HOL/Library/Extended"
+        Abs_Int2
 begin
 
 subsection "Interval Analysis"
 
-datatype lb = Minf | Lb int
-datatype ub = Pinf | Ub int
+type_synonym eint = "int extended"
+type_synonym eint2 = "eint * eint"
 
-datatype ivl = Ivl lb ub
+definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
+"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
 
-definition "\<gamma>_ivl i = (case i of
-  Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} |
-  Ivl (Lb l) Pinf \<Rightarrow> {l..} |
-  Ivl Minf (Ub h) \<Rightarrow> {..h} |
-  Ivl Minf Pinf \<Rightarrow> UNIV)"
+definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
+"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
 
-abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
-"{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)"
-abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
-"{lo\<dots>} == Ivl (Lb lo) Pinf"
-abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
-"{\<dots>hi} == Ivl Minf (Ub hi)"
-abbreviation Ivl_Minf_Pinf :: "ivl"  ("{\<dots>}") where
-"{\<dots>} == Ivl Minf Pinf"
+lemma refl_eq_ivl[simp]: "eq_ivl p p"
+by(auto simp: eq_ivl_def)
 
-lemmas lub_splits = lb.splits ub.splits
-
-definition "num_ivl n = {n\<dots>n}"
+quotient_type ivl = eint2 / eq_ivl
+by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
 
-fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
-"in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
-"in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" |
-"in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" |
-"in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
+lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
+by(simp add: eq_ivl_def)
 
-
-instantiation lb :: linorder
-begin
+abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
+"[l\<dots>h] == abs_ivl(l,h)"
 
-definition less_eq_lb where
-"l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))"
+lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
+by(auto simp: eq_ivl_def)
 
-definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where
-"((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)"
+fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where
+"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h"
 
-instance
-proof
-  case goal1 show ?case by(rule less_lb_def)
-next
-  case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
-  case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
-  case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-next
-  case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
-qed
+lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep
+by(auto simp: eq_ivl_def \<gamma>_rep_def)
+
+definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
+"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
 
-end
-
-instantiation ub :: linorder
-begin
+lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
+  (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
+by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
 
-definition less_eq_ub where
-"u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))"
-
-definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where
-"((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)"
+lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
+apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
+apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
+done
 
-instance
-proof
-  case goal1 show ?case by(rule less_ub_def)
-next
-  case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
-  case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
-  case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-next
-  case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
-qed
+lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
+by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
 
-end
+definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
 
-lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
+lift_definition empty_ivl :: ivl is empty_rep
+by simp
 
-lemma le_lub_simps[simp]:
-  "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf"
-  "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j"
-by(auto simp: le_lub_defs split: lub_splits)
-
-definition empty where "empty = {1\<dots>0}"
+lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
+by(auto simp add: is_empty_rep_def empty_rep_def)
 
-fun is_empty where
-"is_empty {l\<dots>h} = (h<l)" |
-"is_empty _ = False"
+lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
+by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
 
-lemma [simp]: "is_empty(Ivl l h) =
-  (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)"
-by(auto split: lub_splits)
-
-lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
-by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
+declare is_empty_rep_iff[THEN iffD1, simp]
 
 
 instantiation ivl :: semilattice
 begin
 
-fun le_aux where
-"le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)"
+definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
+"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
+  if is_empty_rep(l1,h1) then True else
+  if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
+
+lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
+apply rule
+apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
+apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
+apply(auto simp: not_less split: extended.splits)
+done
+
+lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
+by(auto simp: eq_ivl_def le_iff_subset)
 
-definition le_ivl where
-"i1 \<sqsubseteq> i2 =
- (if is_empty i1 then True else
-  if is_empty i2 then False else le_aux i1 i2)"
+definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
+
+definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
+  else let (l1,h1) = p1; (l2,h2) = p2 in  (min l1 l2, max h1 h2))"
 
-definition "i1 \<squnion> i2 =
- (if is_empty i1 then i2 else if is_empty i2 then i1
-  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))"
+lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep
+by(auto simp: eq_ivl_iff join_rep_def)
 
-definition "\<top> = {\<dots>}"
+lift_definition top_ivl :: ivl is "(Minf,Pinf)"
+by(auto simp: eq_ivl_def)
+
+lemma is_empty_min_max:
+  "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
+by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
 
 instance
 proof
-  case goal1 thus ?case
-    by(cases x, simp add: le_ivl_def)
+  case goal1 show ?case by (rule less_ivl_def)
+next
+  case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
 next
-  case goal2 thus ?case
-    by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits)
+  case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
 next
-  case goal3 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
+  case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
 next
-  case goal4 thus ?case
-    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
+  case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
+next
+  case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
 next
-  case goal5 thus ?case
-    by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits if_splits)
+  case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def)
 next
-  case goal6 thus ?case
-    by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits)
+  case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
 qed
 
 end
 
+text{* Implement (naive) executable equality: *}
+instantiation ivl :: equal
+begin
+
+definition equal_ivl where
+"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
+
+instance
+proof
+  case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
+qed
+
+end
+
+lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
+by(simp add: not_less)
+lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
+by(simp add: not_less)
 
 instantiation ivl :: lattice
 begin
 
-definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))"
+definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
 
-definition "\<bottom> = empty"
+lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
+by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
+
+lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep
+by(auto simp: \<gamma>_meet_rep eq_ivl_def)
+
+definition "\<bottom> = empty_ivl"
 
 instance
 proof
   case goal2 thus ?case
-    by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
+    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
 next
   case goal3 thus ?case
-    by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
+    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
 next
   case goal4 thus ?case
-    by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_lub_defs max_def min_def split: lub_splits if_splits)
+    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
 next
-  case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
+  case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
 qed
 
 end
 
 
-instantiation lb :: plus
+lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
+by (metis eq_ivl_iff is_empty_empty_rep)
+
+lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow>
+  (if [l1\<dots>h1] = \<bottom> then True else
+   if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
+unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
+
+lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
+  (if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else
+   if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
+unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty)
+
+lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
+by transfer (simp add: meet_rep_def)
+
+
+instantiation ivl :: plus
 begin
 
-fun plus_lb where
-"Lb x + Lb y = Lb(x+y)" |
-"_ + _ = Minf"
+definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
+"plus_rep p1 p2 =
+  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
+   let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
+
+lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
+by(auto simp: plus_rep_def eq_ivl_iff)
 
 instance ..
 end
 
-instantiation ub :: plus
-begin
-
-fun plus_ub where
-"Ub x + Ub y = Ub(x+y)" |
-"_ + _ = Pinf"
-
-instance ..
-end
-
-instantiation ivl :: plus
-begin
+lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] =
+  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])"
+unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
 
-definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
-
-instance ..
-end
+lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
+by(cases x) auto
+lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
+by(cases x) auto
 
-fun uminus_ub :: "ub \<Rightarrow> lb" where
-"uminus_ub(Ub( x)) = Lb(-x)" |
-"uminus_ub Pinf = Minf"
-
-fun uminus_lb :: "lb \<Rightarrow> ub" where
-"uminus_lb(Lb( x)) = Ub(-x)" |
-"uminus_lb Minf = Pinf"
+lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
+by(cases x) auto
+lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
+by(cases x) auto
 
 instantiation ivl :: uminus
 begin
 
-fun uminus_ivl where
-"-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)"
-
-instance ..
-end
+definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
+"uminus_rep p = (let (l,h) = p in (-h, -l))"
 
-instantiation ivl :: minus
-begin
+lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
+by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
+        split: prod.split)
 
-definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
-"(i1::ivl) - i2 = i1 + -i2"
+lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
+by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
+   (auto simp: Icc_eq_Icc split: extended.splits)
 
 instance ..
 end
 
-lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
-  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
-by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
+lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]"
+by transfer (simp add: uminus_rep_def)
+
+instantiation ivl :: minus
+begin
+definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2"
+instance ..
+end
+
 
-lemma gamma_minus_ivl:
-  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
-by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
+definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
+"filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
+
+definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where
+"filter_less_rep res p1 p2 =
+  (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else
+   let (l1,h1) = p1; (l2,h2) = p2 in
+   if res
+   then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2))
+   else ((max l1 l2, h1), (l2, min h1 h2)))"
 
-definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
-  i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
+lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep
+by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff)
+declare filter_less_ivl.abs_eq[code] (* bug in lifting *)
+
+lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] =
+  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else
+   if b
+   then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2])
+   else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))"
+unfolding prod_rel_eq[symmetric] bot_ivl_def
+by transfer (auto simp: filter_less_rep_def eq_ivl_empty)
 
-fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
-"filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
-  (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
-   if res
-   then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2)
-   else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))"
+lemma add_mono_le_Fin:
+  "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
+by(drule (1) add_mono) simp
+
+lemma add_mono_Fin_le:
+  "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
+by(drule (1) add_mono) simp
+
+lemma plus_rep_plus:
+  "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)"
+by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin)
 
 interpretation Val_abs
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 proof
-  case goal1 thus ?case
-    by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits)
+  case goal1 thus ?case by transfer (simp add: le_iff_subset)
 next
-  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
+  case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
 next
-  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
+  case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
 next
   case goal4 thus ?case
-    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits)
+    apply transfer
+    apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
+    by(auto simp: empty_rep_def is_empty_rep_def)
 qed
 
+
 interpretation Val_abs1_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defines aval_ivl is aval'
 proof
-  case goal1 thus ?case
-    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits)
+  case goal1 show ?case
+    by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split)
 next
-  case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
+  case goal2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
-lemma mono_minus_ivl: fixes i1 :: ivl
-shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
-apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits)
-  apply(simp split: lub_splits)
- apply(simp split: lub_splits)
-apply(simp split: lub_splits)
-done
+lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)"
+by(auto simp: plus_rep_def plus_rep_plus split: prod.splits)
 
+lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
+     \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))"
+by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
+   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus)
+
+lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
+       eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2;
+        n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk>
+       \<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2"
+by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac)
+   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+
 
 interpretation Val_abs1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
-  case goal1 thus ?case
-    by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
+  case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
 next
-  case goal2 thus ?case
-    by(auto simp add: filter_plus_ivl_def)
-      (metis gamma_minus_ivl add_diff_cancel add_commute)+
+  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric]
+    by transfer (simp add: filter_plus)
 next
   case goal3 thus ?case
-    by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits)
+    unfolding prod_rel_eq[symmetric]
+    apply transfer
+    apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits)
+    apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits)
+    done
 qed
 
 interpretation Abs_Int1
@@ -308,25 +352,41 @@
 
 text{* Monotonicity: *}
 
+lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)"
+by(auto simp add: le_iff_subset \<gamma>_meet_rep)
+
+lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)"
+apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
+by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
+
+lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)"
+apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
+by(auto simp: \<gamma>_rep_cases split: extended.splits)
+
 interpretation Abs_Int1_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
 proof
-  case goal1 thus ?case
-    by(auto simp: plus_ivl_def le_ivl_def le_lub_defs empty_def split: if_splits ivl.splits lub_splits)
+  case goal1 thus ?case by transfer (rule mono_plus_rep)
+next
+  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def
+    by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep)
 next
-  case goal2 thus ?case
-    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
-next
-  case goal3 thus ?case
-    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
-    by(auto simp add: empty_def le_ivl_def le_lub_defs min_def max_def split: lub_splits)
+  case goal3 thus ?case unfolding less_eq_prod_def
+    apply transfer
+    apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits)
+    by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
 qed
 
 
 subsubsection "Tests"
 
+(* Hide Fin in numerals on output *)
+declare
+Fin_numeral [code_post] Fin_neg_numeral [code_post]
+zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
+
 value "show_acom_opt (AI_ivl test1_ivl)"
 
 text{* Better than @{text AI_const}: *}
@@ -334,7 +394,7 @@
 value "show_acom_opt (AI_ivl test4_const)"
 value "show_acom_opt (AI_ivl test6_const)"
 
-definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
+definition "steps c i = (step_ivl(Top(vars c)) ^^ i) (bot c)"
 
 value "show_acom_opt (AI_ivl test2_ivl)"
 value "show_acom (steps test2_ivl 0)"
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -65,17 +65,17 @@
 class narrow =
 fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
 
-class WN = widen + narrow + preord +
-assumes widen1: "x \<sqsubseteq> x \<nabla> y"
-assumes widen2: "y \<sqsubseteq> x \<nabla> y"
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+class WN = widen + narrow + order +
+assumes widen1: "x \<le> x \<nabla> y"
+assumes widen2: "y \<le> x \<nabla> y"
+assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
+assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
 
-class WN_Lc = widen + narrow + preord + Lc +
-assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
-assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
-assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
-assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+class WN_Lc = widen + narrow + order + Lc +
+assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<le> x \<nabla> y"
+assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<le> x \<nabla> y"
+assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
+assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
 assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c"
 assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c"
 
@@ -83,22 +83,25 @@
 instantiation ivl :: WN
 begin
 
-definition "widen_ivl ivl1 ivl2 =
-  ((*if is_empty ivl1 then ivl2 else
-   if is_empty ivl2 then ivl1 else*)
-     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-       Ivl (if l2 \<le> l1 \<and> l2 \<noteq> l1 then Minf else l1)
-           (if h1 \<le> h2 \<and> h1 \<noteq> h2 then Pinf else h1))"
+definition "widen_rep p1 p2 =
+  (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
+   let (l1,h1) = p1; (l2,h2) = p2
+   in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
+
+lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
+by(auto simp: widen_rep_def eq_ivl_iff)
 
-definition "narrow_ivl ivl1 ivl2 =
-  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
-     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
-       Ivl (if l1 = Minf then l2 else l1)
-           (if h1 = Pinf then h2 else h1))"
+definition "narrow_rep p1 p2 =
+  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
+   let (l1,h1) = p1; (l2,h2) = p2
+   in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
+
+lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
+by(auto simp: narrow_rep_def eq_ivl_iff)
 
 instance
-proof qed
-  (auto simp add: widen_ivl_def narrow_ivl_def le_lub_defs le_ivl_def empty_def split: ivl.split lub_splits if_splits)
+proof
+qed (transfer, auto simp: widen_rep_def narrow_rep_def le_iff_subset \<gamma>_rep_def subset_eq is_empty_rep_def empty_rep_def split: if_splits extended.splits)+
 
 end
 
@@ -106,23 +109,20 @@
 instantiation st :: (WN)WN_Lc
 begin
 
-definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
+definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
 
-definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
+definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
 
 instance
 proof
-  case goal1 thus ?case
-    by(simp add: widen_st_def le_st_def WN_class.widen1)
+  case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1)
 next
   case goal2 thus ?case
-    by(simp add: widen_st_def le_st_def WN_class.widen2 Lc_st_def L_st_def)
+    by(simp add: widen_st_def less_eq_st_def WN_class.widen2 Lc_st_def L_st_def)
 next
-  case goal3 thus ?case
-    by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
+  case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1)
 next
-  case goal4 thus ?case
-    by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
+  case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2)
 next
   case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
 next
@@ -196,14 +196,14 @@
 
 lemma widen_acom1: fixes C1 :: "'a acom" shows
   "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
-   \<Longrightarrow> C1 \<sqsubseteq> C1 \<nabla> C2"
-by(induct C1 C2 rule: le_acom.induct)
+   \<Longrightarrow> C1 \<le> C1 \<nabla> C2"
+by(induct C1 C2 rule: less_eq_acom.induct)
   (auto simp: widen_acom_def widen1 Lc_acom_def)
 
 lemma widen_acom2: fixes C1 :: "'a acom" shows
   "\<lbrakk>\<forall>a\<in>set(annos C1). a \<in> Lc c; \<forall>a\<in>set (annos C2). a \<in> Lc c; strip C1 = strip C2\<rbrakk>
-   \<Longrightarrow> C2 \<sqsubseteq> C1 \<nabla> C2"
-by(induct C1 C2 rule: le_acom.induct)
+   \<Longrightarrow> C2 \<le> C1 \<nabla> C2"
+by(induct C1 C2 rule: less_eq_acom.induct)
   (auto simp: widen_acom_def widen2 Lc_acom_def)
 
 lemma strip_map2_acom[simp]:
@@ -229,10 +229,10 @@
   case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
 next
   case goal3 thus ?case
-    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
+    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
 next
   case goal4 thus ?case
-    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
+    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
 next
   case goal5 thus ?case
     by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE)
@@ -255,12 +255,12 @@
 
 lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom"
 shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X"
-by(induction C1 C2 rule: le_acom.induct)
+by(induction C1 C2 rule: less_eq_acom.induct)
   (auto simp: widen_acom_def)
 
 lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom"
 shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X"
-by(induction C1 C2 rule: le_acom.induct)
+by(induction C1 C2 rule: less_eq_acom.induct)
   (auto simp: narrow_acom_def)
 
 lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
@@ -269,18 +269,18 @@
 
 subsubsection "Post-fixed point computation"
 
-definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
-where "iter_widen f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) (\<lambda>x. x \<nabla> f x)"
+definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
+where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
 
-definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
-where "iter_narrow f = while_option (\<lambda>x. \<not> x \<sqsubseteq> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
+definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
+where "iter_narrow f = while_option (\<lambda>x. \<not> x \<le> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
 
-definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
+definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
 where "pfp_wn f x =
   (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
 
 
-lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
+lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
 by(auto simp add: iter_widen_def dest: while_option_stop)
 
 lemma iter_widen_inv:
@@ -295,7 +295,7 @@
 using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
 by (metis assms(1))
 
-lemma strip_iter_widen: fixes f :: "'a::{preord,widen} acom \<Rightarrow> 'a acom"
+lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
 assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
 shows "strip C' = strip C"
 proof-
@@ -305,12 +305,12 @@
 qed
 
 lemma iter_narrow_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
+assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
 and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
-and "P p0" and "f p0 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
-shows "P p \<and> f p \<sqsubseteq> p"
+and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
+shows "P p \<and> f p \<le> p"
 proof-
-  let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
+  let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
   { fix p assume "?Q p"
     note P = conjunct1[OF this] and 12 = conjunct2[OF this]
     note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
@@ -318,12 +318,12 @@
     have "?Q ?p'"
     proof auto
       show "P ?p'" by (blast intro: P Pinv)
-      have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
-      also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
-      finally show "f ?p' \<sqsubseteq> ?p'" .
-      have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
-      also have "p \<sqsubseteq> p0" by(rule 2)
-      finally show "?p' \<sqsubseteq> p0" .
+      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
+      also have "\<dots> \<le> ?p'" by(rule narrow1[OF 1])
+      finally show "f ?p' \<le> ?p'" .
+      have "?p' \<le> p" by (rule narrow2[OF 1])
+      also have "p \<le> p0" by(rule 2)
+      finally show "?p' \<le> p0" .
     qed
   }
   thus ?thesis
@@ -332,11 +332,11 @@
 qed
 
 lemma pfp_wn_pfp:
-assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
+assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
 and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
-and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
+and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
 proof-
   from pfp_wn obtain p0
     where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
@@ -358,24 +358,24 @@
 begin
 
 definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
-"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
+"AI_wn c = pfp_wn (step' (Top(vars c))) (bot c)"
 
 lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
 proof(simp add: CS_def AI_wn_def)
-  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
-  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
+  assume 1: "pfp_wn (step' (Top(vars c))) (bot c) = Some C"
+  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<le> C"
     by(rule pfp_wn_pfp[where x="bot c"])
       (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
-  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
+  have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   proof(rule order_trans)
-    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
-      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
+    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
+      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] Top_in_L])
     show "... \<le> \<gamma>\<^isub>c C"
       by(rule mono_gamma_c[OF conjunct2[OF 2]])
   qed
   have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
-  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
-    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
+  have "lfp c (step (\<gamma>\<^isub>o (Top(vars c)))) \<le> \<gamma>\<^isub>c C"
+    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp])
   thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
 qed
 
@@ -391,14 +391,10 @@
 
 subsubsection "Tests"
 
-(* Trick to make the code generator happy. *)
-lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
-by(rule refl)
-
 definition "step_up_ivl n =
-  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
+  ((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) C)^^n)"
 definition "step_down_ivl n =
-  ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
+  ((\<lambda>C. C \<triangle> step_ivl (Top(vars(strip C))) C)^^n)"
 
 text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
 the loop took to execute. In contrast, @{const AI_ivl'} converges in a
@@ -430,32 +426,31 @@
 
 locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
 fixes n :: "'av \<Rightarrow> nat"
-assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
-assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
-assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
+assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
+assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y"
+assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
 
 begin
 
 lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
-  ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
-proof(auto simp add: le_st_def m_s_def L_st_def widen_st_def)
+  ~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
+proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def)
   assume "finite(dom S1)"
   have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
     by (metis m1 WN_class.widen1)
-  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
+  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x"
   hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
     using m_widen by blast
   from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
   show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
 qed
 
-lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
+lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
-by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen
-        split: option.split)
+by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
 
 lemma m_c_widen:
-  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
+  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
 prefer 2 apply (simp add: size_annos_same2)
@@ -475,25 +470,25 @@
 definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
 "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
 
-lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
+lemma n_s_mono: assumes "S1 \<le> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
 proof-
-  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
-    by(simp_all add: le_st_def)
+  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<le> fun S2 x"
+    by(simp_all add: less_eq_st_def)
   have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
-    by(rule setsum_mono)(simp add: le_st_def n_mono)
+    by(rule setsum_mono)(simp add: less_eq_st_def n_mono)
   thus ?thesis by(simp add: n_s_def)
 qed
 
 lemma n_s_narrow:
-assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
+assumes "finite(dom S1)" and "S2 \<le> S1" "\<not> S1 \<le> S1 \<triangle> S2"
 shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
 proof-
-  from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
-    by(simp_all add: le_st_def)
+  from `S2\<le>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x"
+    by(simp_all add: less_eq_st_def)
   have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
-    by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
-  have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
-    by(force simp: le_st_def narrow_st_def intro: n_narrow)
+    by(auto simp: less_eq_st_def narrow_st_def n_mono WN_class.narrow2)
+  have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<le> S1 \<triangle> S2`
+    by(force simp: less_eq_st_def narrow_st_def intro: n_narrow)
   have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
     apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
@@ -504,12 +499,12 @@
 definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
 "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
 
-lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
+lemma n_o_mono: "S1 \<le> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(auto simp: n_o_def n_s_mono)
 
 lemma n_o_narrow:
   "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
-  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
+  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> \<not> S1 \<le> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
 apply(induction S1 S2 rule: narrow_option.induct)
 apply(auto simp: n_o_def L_st_def n_s_narrow)
 done
@@ -519,7 +514,7 @@
 "n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
 
 lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
-  C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
+  C2 \<le> C1 \<Longrightarrow> \<not> C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
 apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
 prefer 2 apply (simp add: size_annos_same2)
@@ -544,13 +539,13 @@
 fixes m :: "'a::WN_Lc \<Rightarrow> nat"
 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
 and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
-and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
+and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
 and "P C" shows "EX C'. iter_widen f C = Some C'"
 proof(simp add: iter_widen_def,
       rule measure_while_option_Some[where P = P and f=m])
   show "P C" by(rule `P C`)
 next
-  fix C assume "P C" "\<not> f C \<sqsubseteq> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
+  fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
     by(simp add: P_f P_widen m_widen)
 qed
 
@@ -558,19 +553,19 @@
 fixes n :: "'a::WN_Lc \<Rightarrow> nat"
 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
 and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
-and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
-and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<sqsubseteq> C1 \<Longrightarrow> ~ C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
-and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
+and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
+and n_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C2 \<le> C1 \<Longrightarrow> ~ C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n(C1 \<triangle> C2) < n C1"
+and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
 proof(simp add: iter_narrow_def,
-      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<sqsubseteq> C"])
-  show "P C \<and> f C \<sqsubseteq> C" using init by blast
+      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
+  show "P C \<and> f C \<le> C" using init by blast
 next
-  fix C assume 1: "P C \<and> f C \<sqsubseteq> C" and 2: "\<not> C \<sqsubseteq> C \<triangle> f C"
+  fix C assume 1: "P C \<and> f C \<le> C" and 2: "\<not> C \<le> C \<triangle> f C"
   hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
-  moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
-    by (metis narrow1 narrow2 1 mono preord_class.le_trans)
+  moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
+    by (metis narrow1 narrow2 1 mono order_trans)
   moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
-  ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
+  ultimately show "(P (C \<triangle> f C) \<and> f (C \<triangle> f C) \<le> C \<triangle> f C) \<and> n(C \<triangle> f C) < n C"
     by blast
 qed
 
@@ -581,39 +576,51 @@
 
 subsubsection "Termination: Intervals"
 
-definition m_ivl :: "ivl \<Rightarrow> nat" where
-"m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
-     (case l of Minf \<Rightarrow> 0 | Lb _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | Ub _ \<Rightarrow> 1))"
+definition m_rep :: "eint2 \<Rightarrow> nat" where
+"m_rep p = (if is_empty_rep p then 3 else
+  let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
+
+lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
+by(auto simp: m_rep_def eq_ivl_iff)
 
-lemma m_ivl_height: "m_ivl ivl \<le> 2"
-by(simp add: m_ivl_def split: ivl.split lub_splits)
+lemma m_ivl_nice: "m_ivl[l\<dots>h] = (if [l\<dots>h] = \<bottom> then 3 else
+   (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
+unfolding bot_ivl_def
+by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
 
-lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
-by(auto simp: m_ivl_def le_lub_defs le_ivl_def
-        split: ivl.split lub_splits if_splits)
+lemma m_ivl_height: "m_ivl iv \<le> 3"
+by transfer (simp add: m_rep_def split: prod.split extended.split)
+
+lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
+by transfer
+   (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
+         split: prod.split extended.splits if_splits)
 
 lemma m_ivl_widen:
-  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
-by(auto simp: m_ivl_def widen_ivl_def le_lub_defs le_ivl_def
-        split: ivl.splits lub_splits if_splits)
+  "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
+by transfer
+   (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
+         split: prod.split extended.splits if_splits)
 
 definition n_ivl :: "ivl \<Rightarrow> nat" where
-"n_ivl ivl = 2 - m_ivl ivl"
+"n_ivl ivl = 3 - m_ivl ivl"
 
-lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
+lemma n_ivl_mono: "x \<le> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
 unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
 
 lemma n_ivl_narrow:
-  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
-by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_lub_defs le_ivl_def
-        split: ivl.splits lub_splits if_splits)
+  "~ x \<le> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
+unfolding n_ivl_def
+by transfer
+   (auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
+         split: prod.splits if_splits extended.splits)
 
 
 interpretation Abs_Int2_measure
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
-and m = m_ivl and n = n_ivl and h = 2
+and m = m_ivl and n = n_ivl and h = 3
 proof
   case goal1 thus ?case by(rule m_ivl_anti_mono)
 next
@@ -629,14 +636,14 @@
 
 
 lemma iter_winden_step_ivl_termination:
-  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
+  "\<exists>C. iter_widen (step_ivl (Top(vars c))) (bot c) = Some C"
 apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
 apply (simp_all add: step'_in_Lc m_c_widen)
 done
 
 lemma iter_narrow_step_ivl_termination:
-  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
-  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
+  "C0 \<in> Lc c \<Longrightarrow> step_ivl (Top(vars c)) C0 \<le> C0 \<Longrightarrow>
+  \<exists>C. iter_narrow (step_ivl (Top(vars c))) C0 = Some C"
 apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
 apply (simp add: step'_in_Lc)
 apply (simp)
@@ -662,12 +669,11 @@
 
 subsubsection "Counterexamples"
 
-text{* Widening is increasing by assumption,
-but @{prop"x \<sqsubseteq> f x"} is not an invariant of widening. It can already
-be lost after the first step: *}
+text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
+It can already be lost after the first step: *}
 
-lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" shows "x \<nabla> f x \<sqsubseteq> f(x \<nabla> f x)"
+lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
+and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
 nitpick[card = 3, expect = genuine, show_consts]
 (*
 1 < 2 < 3,
@@ -682,9 +688,9 @@
 text{* Widening terminates but may converge more slowly than Kleene iteration.
 In the following model, Kleene iteration goes from 0 to the least pfp
 in one step but widening takes 2 steps to reach a strictly larger pfp: *}
-lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" and "f(f x) \<sqsubseteq> f x"
-shows "f(x \<nabla> f x) \<sqsubseteq> x \<nabla> f x"
+lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
+and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
+shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
 nitpick[card = 4, expect = genuine, show_consts]
 (*
 
diff -r 0c376ef98559 -r 00b45c7e831f src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Wed Mar 06 14:10:07 2013 +0100
+++ b/src/HOL/IMP/Abs_State.thy	Wed Mar 06 16:10:56 2013 +0100
@@ -60,21 +60,21 @@
 end
 
 class semilatticeL = join + L +
-fixes top :: "vname set \<Rightarrow> 'a"
-assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
-and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
-and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
-and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
-and top_in_L[simp]: "top X \<in> L X"
+fixes Top :: "vname set \<Rightarrow> 'a"
+assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
+and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
+and join_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
+and Top[simp]: "x \<in> L X \<Longrightarrow> x \<le> Top X"
+and Top_in_L[simp]: "Top X \<in> L X"
 and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
 
-notation (input) top ("\<top>\<^bsub>_\<^esub>")
-notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
+notation (input) Top ("\<top>\<^bsub>_\<^esub>")
+notation (latex output) Top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
 
 instantiation option :: (semilatticeL)semilatticeL
 begin
 
-definition top_option where "top c = Some(top c)"
+definition Top_option where "Top c = Some(Top c)"
 
 instance proof
   case goal1 thus ?case by(cases x, simp, cases y, simp_all)
@@ -83,9 +83,9 @@
 next
   case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
 next
-  case goal4 thus ?case by(cases x, simp_all add: top_option_def)
+  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
 next
-  case goal5 thus ?case by(simp add: top_option_def)
+  case goal5 thus ?case by(simp add: Top_option_def)
 next
   case goal6 thus ?case by(simp add: L_option_def split: option.splits)
 qed
@@ -97,41 +97,77 @@
 
 hide_type  st  --"to avoid long names"
 
-text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
+text{* A concrete type of state with computable @{text"\<le>"}: *}
+
+fun st :: "(vname \<Rightarrow> 'a) * vname set \<Rightarrow> bool" where
+"st (f,X) = (\<forall>x. x \<notin> X \<longrightarrow> f x = undefined)"
 
-datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
+typedef 'a st = "{p :: (vname \<Rightarrow> 'a) * vname set. st p}"
+proof
+  show "(\<lambda>x. undefined,{}) \<in> {p. st p}" by simp
+qed
+
+setup_lifting type_definition_st
+
+lift_definition St :: "(vname \<Rightarrow> 'a) \<Rightarrow> vname set \<Rightarrow> 'a st" is
+  "\<lambda>f X. (\<lambda>x. if x \<in> X then f x else undefined, X)"
+by(simp)
 
-fun "fun" where "fun (FunDom f X) = f"
-fun dom where "dom (FunDom f X) = X"
+lift_definition update :: "'a st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st" is
+  "\<lambda>(f,X) x a. (f(x := a), insert x X)"
+by(auto)
+
+lift_definition "fun" :: "'a st \<Rightarrow> vname \<Rightarrow> 'a" is fst ..
+
+lift_definition dom :: "'a st \<Rightarrow> vname set" is snd ..
 
-definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
+lemma dom_St[simp]: "dom(St f X) = X"
+by(simp add: St.rep_eq dom.rep_eq)
 
-value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
+lemma fun_St[simp]: "fun(St f X) = (\<lambda>x. if x \<in> X then f x else undefined)"
+by(simp add: St.rep_eq fun.rep_eq)
+
+definition show_st :: "'a st \<Rightarrow> (vname * 'a)set" where
+"show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
 
 definition "show_acom = map_acom (Option.map show_st)"
 definition "show_acom_opt = Option.map show_acom"
 
-definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
+lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
+by transfer auto
 
-lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
-by(rule ext)(auto simp: update_def)
+lemma dom_update[simp]: "dom (update S x y) = insert x (dom S)"
+by transfer auto
+
+definition \<gamma>_st :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
+"\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom  F. f x \<in> \<gamma>(fun F x)}"
 
-lemma dom_update[simp]: "dom (update S x y) = dom S"
-by(simp add: update_def)
+lemma ext_st: "dom F = dom G \<Longrightarrow> \<forall>x \<in> dom G. fun F x = fun G x \<Longrightarrow> F=G"
+apply(induct F rule:Abs_st_induct)
+apply(induct G rule:Abs_st_induct)
+apply (auto simp:Abs_st_inject fun_def dom_def Abs_st_inverse simp del: st.simps)
+apply(rule ext)
+apply auto
+done
 
-definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
-
-
-instantiation st :: (preord) preord
+instantiation st :: (order) order
 begin
 
-definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
-"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"
+definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
+"F \<le> (G::'a st) = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<le> fun G x))"
+
+definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
 
 instance
 proof
-  case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)
-qed (auto simp: le_st_def)
+  case goal1 show ?case by(rule less_st_def)
+next
+  case goal2 show ?case by(auto simp: less_eq_st_def)
+next
+  case goal3 thus ?case by(fastforce simp: less_eq_st_def)
+next
+  case goal4 thus ?case by (metis less_eq_st_def antisym ext_st)
+qed
 
 end
 
@@ -139,7 +175,7 @@
 begin
 
 definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
-"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
+"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
 
 instance ..
 
@@ -149,7 +185,7 @@
 begin
 
 definition L_st :: "vname set \<Rightarrow> 'a st set" where
-"L X = {F. dom F = X}"
+"L(X::vname set) = {F. dom F = X}"
 
 instance ..
 
@@ -158,11 +194,10 @@
 instantiation st :: (semilattice) semilatticeL
 begin
 
-definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
+definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
 
 instance
-proof
-qed (auto simp: le_st_def join_st_def top_st_def L_st_def)
+proof qed(auto simp add: less_eq_st_def join_st_def Top_st_def L_st_def)
 
 end
 
@@ -175,12 +210,12 @@
    But L is not executable. This looping defn makes it look as if it were. *)
 
 
-lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
-by(auto simp: le_st_def)
+lemma mono_fun: "F \<le> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<le> fun G x"
+by(auto simp: less_eq_st_def)
 
 lemma mono_update[simp]:
-  "a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"
-by(auto simp add: le_st_def update_def)
+  "a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
+by(auto simp add: less_eq_st_def)
 
 
 locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
@@ -195,22 +230,22 @@
 abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
 where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
 
-lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
-by(auto simp: top_st_def \<gamma>_st_def)
+lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (Top X) = UNIV"
+by(auto simp: Top_st_def \<gamma>_st_def)
 
-lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
-by (simp add: top_option_def)
+lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (Top X) = UNIV"
+by (simp add: Top_option_def)
 
-lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
-apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
+lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
+apply(simp add:\<gamma>_st_def subset_iff less_eq_st_def split: if_splits)
 by (metis mono_gamma subsetD)
 
 lemma mono_gamma_o:
-  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
-by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
+  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
+by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
 
-lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
-by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
+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)
 
 lemma in_gamma_option_iff:
   "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"