major redesign: order instead of preorder, new definition of intervals as quotients
authornipkow
Wed Mar 06 16:10:56 2013 +0100 (2013-03-06)
changeset 5135900b45c7e831f
parent 51358 0c376ef98559
child 51360 c4367ed99b5e
major redesign: order instead of preorder, new definition of intervals as quotients
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int1_const.thy
src/HOL/IMP/Abs_Int1_parity.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int2_ivl.thy
src/HOL/IMP/Abs_Int3.thy
src/HOL/IMP/Abs_State.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Wed Mar 06 14:10:07 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Wed Mar 06 16:10:56 2013 +0100
     1.3 @@ -6,52 +6,26 @@
     1.4  
     1.5  subsection "Orderings"
     1.6  
     1.7 -class preord =
     1.8 -fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
     1.9 -assumes le_refl[simp]: "x \<sqsubseteq> x"
    1.10 -and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    1.11 -begin
    1.12 -
    1.13 -definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
    1.14 -
    1.15 -declare le_trans[trans]
    1.16 +notation
    1.17 +  Orderings.bot ("\<bottom>") and
    1.18 +  Orderings.top ("\<top>")
    1.19  
    1.20 -end
    1.21 +declare order_trans[trans]
    1.22  
    1.23 -text{* Note: no antisymmetry. Allows implementations where some abstract
    1.24 -element is implemented by two different values @{prop "x \<noteq> y"}
    1.25 -such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
    1.26 -needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
    1.27 -*}
    1.28 -
    1.29 -class join = preord +
    1.30 +class join = order +
    1.31  fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    1.32  
    1.33 -class semilattice = join +
    1.34 -fixes Top :: "'a" ("\<top>")
    1.35 -assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    1.36 -and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    1.37 -and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    1.38 -and top[simp]: "x \<sqsubseteq> \<top>"
    1.39 +class semilattice = join + top +
    1.40 +assumes join_ge1 [simp]: "x \<le> x \<squnion> y"
    1.41 +and join_ge2 [simp]: "y \<le> x \<squnion> y"
    1.42 +and join_least: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
    1.43  begin
    1.44  
    1.45 -lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    1.46 -by (metis join_ge1 join_ge2 join_least le_trans)
    1.47 -
    1.48 -lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
    1.49 -by (metis join_ge1 join_ge2 le_trans)
    1.50 -
    1.51 -end
    1.52 +lemma join_le_iff[simp]: "x \<squnion> y \<le> z \<longleftrightarrow> x \<le> z \<and> y \<le> z"
    1.53 +by (metis join_ge1 join_ge2 join_least order_trans)
    1.54  
    1.55 -instantiation "fun" :: (type, preord) preord
    1.56 -begin
    1.57 -
    1.58 -definition "f \<sqsubseteq> g = (\<forall>x. f x \<sqsubseteq> g x)"
    1.59 -
    1.60 -instance
    1.61 -proof
    1.62 -  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
    1.63 -qed (simp_all add: le_fun_def)
    1.64 +lemma le_join_disj: "x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
    1.65 +by (metis join_ge1 join_ge2 order_trans)
    1.66  
    1.67  end
    1.68  
    1.69 @@ -60,81 +34,41 @@
    1.70  begin
    1.71  
    1.72  definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
    1.73 -definition "\<top> = (\<lambda>x. \<top>)"
    1.74  
    1.75  lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
    1.76  by (simp add: join_fun_def)
    1.77  
    1.78  instance
    1.79  proof
    1.80 -qed (simp_all add: le_fun_def Top_fun_def)
    1.81 +qed (simp_all add: le_fun_def)
    1.82  
    1.83  end
    1.84  
    1.85  
    1.86 -instantiation acom :: (preord) preord
    1.87 +instantiation option :: (order)order
    1.88  begin
    1.89  
    1.90 -fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
    1.91 -"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
    1.92 -"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
    1.93 -"le_acom (C1;C2) (D1;D2) = (C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)" |
    1.94 -"le_acom (IF b THEN {p1} C1 ELSE {p2} C2 {S}) (IF b' THEN {q1} D1 ELSE {q2} D2 {S'}) =
    1.95 -  (b=b' \<and> p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')" |
    1.96 -"le_acom ({I} WHILE b DO {p} C {P}) ({I'} WHILE b' DO {p'} C' {P'}) =
    1.97 -  (b=b' \<and> p \<sqsubseteq> p' \<and> C \<sqsubseteq> C' \<and> I \<sqsubseteq> I' \<and> P \<sqsubseteq> P')" |
    1.98 -"le_acom _ _ = False"
    1.99 -
   1.100 -lemma [simp]: "SKIP {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = SKIP {S'} \<and> S \<sqsubseteq> S')"
   1.101 -by (cases C) auto
   1.102 -
   1.103 -lemma [simp]: "x ::= e {S} \<sqsubseteq> C \<longleftrightarrow> (\<exists>S'. C = x ::= e {S'} \<and> S \<sqsubseteq> S')"
   1.104 -by (cases C) auto
   1.105 -
   1.106 -lemma [simp]: "C1;C2 \<sqsubseteq> C \<longleftrightarrow> (\<exists>D1 D2. C = D1;D2 \<and> C1 \<sqsubseteq> D1 \<and> C2 \<sqsubseteq> D2)"
   1.107 -by (cases C) auto
   1.108 -
   1.109 -lemma [simp]: "IF b THEN {p1} C1 ELSE {p2} C2 {S} \<sqsubseteq> C \<longleftrightarrow>
   1.110 -  (\<exists>q1 q2 D1 D2 S'. C = IF b THEN {q1} D1 ELSE {q2} D2 {S'} \<and>
   1.111 -     p1 \<sqsubseteq> q1 \<and> C1 \<sqsubseteq> D1 \<and> p2 \<sqsubseteq> q2 \<and> C2 \<sqsubseteq> D2 \<and> S \<sqsubseteq> S')"
   1.112 -by (cases C) auto
   1.113 +fun less_eq_option where
   1.114 +"Some x \<le> Some y = (x \<le> y)" |
   1.115 +"None \<le> y = True" |
   1.116 +"Some _ \<le> None = False"
   1.117  
   1.118 -lemma [simp]: "{I} WHILE b DO {p} C {P} \<sqsubseteq> W \<longleftrightarrow>
   1.119 -  (\<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')"
   1.120 -by (cases W) auto
   1.121 +definition less_option where "x < (y::'a option) = (x \<le> y \<and> \<not> y \<le> x)"
   1.122  
   1.123 -instance
   1.124 -proof
   1.125 -  case goal1 thus ?case by (induct x) auto
   1.126 -next
   1.127 -  case goal2 thus ?case
   1.128 -  apply(induct x y arbitrary: z rule: le_acom.induct)
   1.129 -  apply (auto intro: le_trans)
   1.130 -  done
   1.131 -qed
   1.132 -
   1.133 -end
   1.134 -
   1.135 -
   1.136 -instantiation option :: (preord)preord
   1.137 -begin
   1.138 -
   1.139 -fun le_option where
   1.140 -"Some x \<sqsubseteq> Some y = (x \<sqsubseteq> y)" |
   1.141 -"None \<sqsubseteq> y = True" |
   1.142 -"Some _ \<sqsubseteq> None = False"
   1.143 -
   1.144 -lemma [simp]: "(x \<sqsubseteq> None) = (x = None)"
   1.145 +lemma [simp]: "(x \<le> None) = (x = None)"
   1.146  by (cases x) simp_all
   1.147  
   1.148 -lemma [simp]: "(Some x \<sqsubseteq> u) = (\<exists>y. u = Some y \<and> x \<sqsubseteq> y)"
   1.149 +lemma [simp]: "(Some x \<le> u) = (\<exists>y. u = Some y \<and> x \<le> y)"
   1.150  by (cases u) auto
   1.151  
   1.152  instance proof
   1.153 -  case goal1 show ?case by(cases x, simp_all)
   1.154 +  case goal1 show ?case by(rule less_option_def)
   1.155 +next
   1.156 +  case goal2 show ?case by(cases x, simp_all)
   1.157  next
   1.158 -  case goal2 thus ?case
   1.159 -    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
   1.160 +  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, auto)
   1.161 +next
   1.162 +  case goal4 thus ?case by(cases y, simp, cases x, auto)
   1.163  qed
   1.164  
   1.165  end
   1.166 @@ -157,25 +91,21 @@
   1.167  instantiation option :: (semilattice)semilattice
   1.168  begin
   1.169  
   1.170 -definition "\<top> = Some \<top>"
   1.171 +definition top_option where "\<top> = Some \<top>"
   1.172  
   1.173  instance proof
   1.174 -  case goal1 thus ?case by(cases x, simp, cases y, simp_all)
   1.175 +  case goal1 show ?case by(cases a, simp_all add: top_option_def)
   1.176  next
   1.177 -  case goal2 thus ?case by(cases y, simp, cases x, simp_all)
   1.178 +  case goal2 thus ?case by(cases x, simp, cases y, simp_all)
   1.179  next
   1.180 -  case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
   1.181 +  case goal3 thus ?case by(cases y, simp, cases x, simp_all)
   1.182  next
   1.183 -  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
   1.184 +  case goal4 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
   1.185  qed
   1.186  
   1.187  end
   1.188  
   1.189 -class bot = preord +
   1.190 -fixes bot :: "'a" ("\<bottom>")
   1.191 -assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
   1.192 -
   1.193 -instantiation option :: (preord)bot
   1.194 +instantiation option :: (order)bot
   1.195  begin
   1.196  
   1.197  definition bot_option :: "'a option" where
   1.198 @@ -192,7 +122,7 @@
   1.199  definition bot :: "com \<Rightarrow> 'a option acom" where
   1.200  "bot c = anno None c"
   1.201  
   1.202 -lemma bot_least: "strip C = c \<Longrightarrow> bot c \<sqsubseteq> C"
   1.203 +lemma bot_least: "strip C = c \<Longrightarrow> bot c \<le> C"
   1.204  by(induct C arbitrary: c)(auto simp: bot_def)
   1.205  
   1.206  lemma strip_bot[simp]: "strip(bot c) = c"
   1.207 @@ -201,20 +131,21 @@
   1.208  
   1.209  subsubsection "Post-fixed point iteration"
   1.210  
   1.211 -definition pfp :: "(('a::preord) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
   1.212 -"pfp f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) f"
   1.213 +definition pfp :: "(('a::order) \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option" where
   1.214 +"pfp f = while_option (\<lambda>x. \<not> f x \<le> x) f"
   1.215  
   1.216 -lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<sqsubseteq> x"
   1.217 +lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x \<le> x"
   1.218  using while_option_stop[OF assms[simplified pfp_def]] by simp
   1.219  
   1.220  lemma while_least:
   1.221 -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"
   1.222 -and "\<forall>x \<in> L. b \<sqsubseteq> x" and "b \<in> L" and "f q \<sqsubseteq> q" and "q \<in> L"
   1.223 +fixes q :: "'a::order"
   1.224 +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"
   1.225 +and "\<forall>x \<in> L. b \<le> x" and "b \<in> L" and "f q \<le> q" and "q \<in> L"
   1.226  and "while_option P f b = Some p"
   1.227 -shows "p \<sqsubseteq> q"
   1.228 +shows "p \<le> q"
   1.229  using while_option_rule[OF _  assms(7)[unfolded pfp_def],
   1.230 -                        where P = "%x. x \<in> L \<and> x \<sqsubseteq> q"]
   1.231 -by (metis assms(1-6) le_trans)
   1.232 +                        where P = "%x. x \<in> L \<and> x \<le> q"]
   1.233 +by (metis assms(1-6) order_trans)
   1.234  
   1.235  lemma pfp_inv:
   1.236    "pfp f x = Some y \<Longrightarrow> (\<And>x. P x \<Longrightarrow> P(f x)) \<Longrightarrow> P x \<Longrightarrow> P y"
   1.237 @@ -238,7 +169,7 @@
   1.238  
   1.239  locale Val_abs =
   1.240  fixes \<gamma> :: "'av::semilattice \<Rightarrow> val set"
   1.241 -  assumes mono_gamma: "a \<sqsubseteq> b \<Longrightarrow> \<gamma> a \<subseteq> \<gamma> b"
   1.242 +  assumes mono_gamma: "a \<le> b \<Longrightarrow> \<gamma> a \<le> \<gamma> b"
   1.243    and gamma_Top[simp]: "\<gamma> \<top> = UNIV"
   1.244  fixes num' :: "val \<Rightarrow> 'av"
   1.245  and plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av"
   1.246 @@ -284,21 +215,21 @@
   1.247  abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
   1.248  where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
   1.249  
   1.250 -lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s Top = UNIV"
   1.251 -by(simp add: Top_fun_def \<gamma>_fun_def)
   1.252 +lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s \<top> = UNIV"
   1.253 +by(simp add: top_fun_def \<gamma>_fun_def)
   1.254  
   1.255 -lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o Top = UNIV"
   1.256 -by (simp add: Top_option_def)
   1.257 +lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o \<top> = UNIV"
   1.258 +by (simp add: top_option_def)
   1.259  
   1.260 -lemma mono_gamma_s: "f1 \<sqsubseteq> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
   1.261 +lemma mono_gamma_s: "f1 \<le> f2 \<Longrightarrow> \<gamma>\<^isub>s f1 \<subseteq> \<gamma>\<^isub>s f2"
   1.262  by(auto simp: le_fun_def \<gamma>_fun_def dest: mono_gamma)
   1.263  
   1.264  lemma mono_gamma_o:
   1.265 -  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   1.266 -by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
   1.267 +  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   1.268 +by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
   1.269  
   1.270 -lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   1.271 -by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
   1.272 +lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   1.273 +by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
   1.274  
   1.275  text{* Soundness: *}
   1.276  
   1.277 @@ -326,7 +257,7 @@
   1.278  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   1.279  proof(simp add: CS_def AI_def)
   1.280    assume 1: "pfp (step' \<top>) (bot c) = Some C"
   1.281 -  have pfp': "step' \<top> C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
   1.282 +  have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
   1.283    have 2: "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"  --"transfer the pfp'"
   1.284    proof(rule order_trans)
   1.285      show "step (\<gamma>\<^isub>o \<top>) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c (step' \<top> C)" by(rule step_step')
   1.286 @@ -343,21 +274,21 @@
   1.287  
   1.288  subsubsection "Monotonicity"
   1.289  
   1.290 -lemma mono_post: "C1 \<sqsubseteq> C2 \<Longrightarrow> post C1 \<sqsubseteq> post C2"
   1.291 -by(induction C1 C2 rule: le_acom.induct) (auto)
   1.292 +lemma mono_post: "C1 \<le> C2 \<Longrightarrow> post C1 \<le> post C2"
   1.293 +by(induction C1 C2 rule: less_eq_acom.induct) (auto)
   1.294  
   1.295  locale Abs_Int_Fun_mono = Abs_Int_Fun +
   1.296 -assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   1.297 +assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
   1.298  begin
   1.299  
   1.300 -lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
   1.301 +lemma mono_aval': "S \<le> S' \<Longrightarrow> aval' e S \<le> aval' e S'"
   1.302  by(induction e)(auto simp: le_fun_def mono_plus')
   1.303  
   1.304 -lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
   1.305 +lemma mono_update: "a \<le> a' \<Longrightarrow> S \<le> S' \<Longrightarrow> S(x := a) \<le> S'(x := a')"
   1.306  by(simp add: le_fun_def)
   1.307  
   1.308 -lemma mono_step': "S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
   1.309 -apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
   1.310 +lemma mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
   1.311 +apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
   1.312  apply (auto simp: Let_def mono_update mono_aval' mono_post le_join_disj
   1.313              split: option.split)
   1.314  done
     2.1 --- a/src/HOL/IMP/Abs_Int1.thy	Wed Mar 06 14:10:07 2013 +0100
     2.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Wed Mar 06 16:10:56 2013 +0100
     2.3 @@ -4,16 +4,16 @@
     2.4  imports Abs_State
     2.5  begin
     2.6  
     2.7 -lemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
     2.8 - (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) \<and> strip C1 = strip C2"
     2.9 -by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)
    2.10 +lemma le_iff_le_annos_zip: "C1 \<le> C2 \<longleftrightarrow>
    2.11 + (\<forall> (a1,a2) \<in> set(zip (annos C1) (annos C2)). a1 \<le> a2) \<and> strip C1 = strip C2"
    2.12 +by(induct C1 C2 rule: less_eq_acom.induct) (auto simp: size_annos_same2)
    2.13  
    2.14 -lemma le_iff_le_annos: "C1 \<sqsubseteq> C2 \<longleftrightarrow>
    2.15 -  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"
    2.16 +lemma le_iff_le_annos: "C1 \<le> C2 \<longleftrightarrow>
    2.17 +  strip C1 = strip C2 \<and> (\<forall> i<size(annos C1). annos C1 ! i \<le> annos C2 ! i)"
    2.18  by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)
    2.19  
    2.20  
    2.21 -lemma mono_fun_L[simp]: "F \<in> L X \<Longrightarrow> F \<sqsubseteq> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
    2.22 +lemma mono_fun_L[simp]: "F \<in> L X \<Longrightarrow> F \<le> G \<Longrightarrow> x : X \<Longrightarrow> fun F x \<le> fun G x"
    2.23  by(simp add: mono_fun L_st_def)
    2.24  
    2.25  lemma bot_in_L[simp]: "bot c \<in> L(vars c)"
    2.26 @@ -71,7 +71,7 @@
    2.27     {S \<squnion> post C} WHILE b DO {I} step' P C {I}"
    2.28  
    2.29  definition AI :: "com \<Rightarrow> 'av st option acom option" where
    2.30 -"AI c = pfp (step' (top(vars c))) (bot c)"
    2.31 +"AI c = pfp (step' (Top(vars c))) (bot c)"
    2.32  
    2.33  
    2.34  lemma strip_step'[simp]: "strip(step' S C) = strip C"
    2.35 @@ -94,7 +94,7 @@
    2.36    case Seq thus ?case by auto
    2.37  next
    2.38    case (If b p1 C1 p2 C2 P)
    2.39 -  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
    2.40 +  hence "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
    2.41      by(simp, metis post_in_L join_ge1 join_ge2)
    2.42    thus ?case using If by (auto simp: mono_gamma_o)
    2.43  next
    2.44 @@ -105,26 +105,26 @@
    2.45    "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> (step' S C) \<in> L X"
    2.46  proof(induction C arbitrary: S)
    2.47    case Assign thus ?case
    2.48 -    by(auto simp: L_st_def update_def split: option.splits)
    2.49 +    by(auto simp: L_st_def split: option.splits)
    2.50  qed auto
    2.51  
    2.52  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    2.53  proof(simp add: CS_def AI_def)
    2.54 -  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
    2.55 +  assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
    2.56    have "C \<in> L(vars c)"
    2.57      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    2.58 -      (erule step'_in_L[OF _ top_in_L])
    2.59 -  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    2.60 -  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    2.61 +      (erule step'_in_L[OF _ Top_in_L])
    2.62 +  have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
    2.63 +  have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    2.64    proof(rule order_trans)
    2.65 -    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    2.66 -      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    2.67 -    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
    2.68 +    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
    2.69 +      by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
    2.70 +    show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
    2.71        by(rule mono_gamma_c[OF pfp'])
    2.72    qed
    2.73    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
    2.74 -  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
    2.75 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
    2.76 +  have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
    2.77 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
    2.78    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
    2.79  qed
    2.80  
    2.81 @@ -134,41 +134,41 @@
    2.82  subsubsection "Monotonicity"
    2.83  
    2.84  lemma le_join_disj: "y \<in> L X \<Longrightarrow> (z::_::semilatticeL) \<in> L X \<Longrightarrow>
    2.85 -  x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
    2.86 -by (metis join_ge1 join_ge2 preord_class.le_trans)
    2.87 +  x \<le> y \<or> x \<le> z \<Longrightarrow> x \<le> y \<squnion> z"
    2.88 +by (metis join_ge1 join_ge2 order_trans)
    2.89  
    2.90  locale Abs_Int_mono = Abs_Int +
    2.91 -assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
    2.92 +assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
    2.93  begin
    2.94  
    2.95  lemma mono_aval':
    2.96 -  "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"
    2.97 -by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
    2.98 +  "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"
    2.99 +by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
   2.100  
   2.101  theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   2.102 -  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
   2.103 -apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
   2.104 +  S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
   2.105 +apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
   2.106  apply (auto simp: Let_def mono_aval' mono_post
   2.107    le_join_disj le_join_disj[OF  post_in_L post_in_L]
   2.108              split: option.split)
   2.109  done
   2.110  
   2.111  lemma mono_step'_top: "C \<in> L X \<Longrightarrow> C' \<in> L X \<Longrightarrow>
   2.112 -  C \<sqsubseteq> C' \<Longrightarrow> step' (top X) C \<sqsubseteq> step' (top X) C'"
   2.113 -by (metis top_in_L mono_step' preord_class.le_refl)
   2.114 +  C \<le> C' \<Longrightarrow> step' (Top X) C \<le> step' (Top X) C'"
   2.115 +by (metis Top_in_L mono_step' order_refl)
   2.116  
   2.117  lemma pfp_bot_least:
   2.118  assumes "\<forall>x\<in>L(vars c)\<inter>{C. strip C = c}.\<forall>y\<in>L(vars c)\<inter>{C. strip C = c}.
   2.119 -  x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y"
   2.120 +  x \<le> y \<longrightarrow> f x \<le> f y"
   2.121  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}"
   2.122 -and "f C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
   2.123 -shows "C \<sqsubseteq> C'"
   2.124 +and "f C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)" "pfp f (bot c) = Some C"
   2.125 +shows "C \<le> C'"
   2.126  apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
   2.127  by (simp_all add: assms(4,5) bot_least)
   2.128  
   2.129  lemma AI_least_pfp: assumes "AI c = Some C"
   2.130 -and "step' (top(vars c)) C' \<sqsubseteq> C'" "strip C' = c" "C' \<in> L(vars c)"
   2.131 -shows "C \<sqsubseteq> C'"
   2.132 +and "step' (Top(vars c)) C' \<le> C'" "strip C' = c" "C' \<in> L(vars c)"
   2.133 +shows "C \<le> C'"
   2.134  apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
   2.135  by (simp_all add: mono_step'_top)
   2.136  
   2.137 @@ -177,30 +177,27 @@
   2.138  
   2.139  subsubsection "Termination"
   2.140  
   2.141 -abbreviation sqless (infix "\<sqsubset>" 50) where
   2.142 -"x \<sqsubset> y == x \<sqsubseteq> y \<and> \<not> y \<sqsubseteq> x"
   2.143 -
   2.144  lemma pfp_termination:
   2.145 -fixes x0 :: "'a::preord" and m :: "'a \<Rightarrow> nat"
   2.146 -assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   2.147 -and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<sqsubset> y \<Longrightarrow> m x > m y"
   2.148 -and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
   2.149 +fixes x0 :: "'a::order" and m :: "'a \<Rightarrow> nat"
   2.150 +assumes mono: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
   2.151 +and m: "\<And>x y. I x \<Longrightarrow> I y \<Longrightarrow> x < y \<Longrightarrow> m x > m y"
   2.152 +and I: "\<And>x y. I x \<Longrightarrow> I(f x)" and "I x0" and "x0 \<le> f x0"
   2.153  shows "\<exists>x. pfp f x0 = Some x"
   2.154 -proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])
   2.155 -  show "wf {(y,x). ((I x \<and> x \<sqsubseteq> f x) \<and> \<not> f x \<sqsubseteq> x) \<and> y = f x}"
   2.156 +proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<le> f x"])
   2.157 +  show "wf {(y,x). ((I x \<and> x \<le> f x) \<and> \<not> f x \<le> x) \<and> y = f x}"
   2.158      by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
   2.159  next
   2.160 -  show "I x0 \<and> x0 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blast
   2.161 +  show "I x0 \<and> x0 \<le> f x0" using `I x0` `x0 \<le> f x0` by blast
   2.162  next
   2.163 -  fix x assume "I x \<and> x \<sqsubseteq> f x" thus "I(f x) \<and> f x \<sqsubseteq> f(f x)"
   2.164 +  fix x assume "I x \<and> x \<le> f x" thus "I(f x) \<and> f x \<le> f(f x)"
   2.165      by (blast intro: I mono)
   2.166  qed
   2.167  
   2.168  
   2.169  locale Measure1 =
   2.170 -fixes m :: "'av::preord \<Rightarrow> nat"
   2.171 +fixes m :: "'av::order \<Rightarrow> nat"
   2.172  fixes h :: "nat"
   2.173 -assumes m1: "x \<sqsubseteq> y \<Longrightarrow> m x \<ge> m y"
   2.174 +assumes m1: "x \<le> y \<Longrightarrow> m x \<ge> m y"
   2.175  assumes h: "m x \<le> h"
   2.176  begin
   2.177  
   2.178 @@ -211,9 +208,9 @@
   2.179  by(simp add: L_st_def m_s_def)
   2.180    (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
   2.181  
   2.182 -lemma m_s1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
   2.183 -proof(auto simp add: le_st_def m_s_def)
   2.184 -  assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
   2.185 +lemma m_s1: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2"
   2.186 +proof(auto simp add: less_eq_st_def m_s_def)
   2.187 +  assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
   2.188    hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
   2.189    thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"
   2.190      by (metis setsum_mono)
   2.191 @@ -226,8 +223,8 @@
   2.192  by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)
   2.193  
   2.194  lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
   2.195 -  o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
   2.196 -proof(induction o1 o2 rule: le_option.induct)
   2.197 +  o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
   2.198 +proof(induction o1 o2 rule: less_eq_option.induct)
   2.199    case 1 thus ?case by (simp add: m_o_def)(metis m_s1)
   2.200  next
   2.201    case 2 thus ?case
   2.202 @@ -257,46 +254,45 @@
   2.203  end
   2.204  
   2.205  locale Measure = Measure1 +
   2.206 -assumes m2: "x \<sqsubset> y \<Longrightarrow> m x > m y"
   2.207 +assumes m2: "x < y \<Longrightarrow> m x > m y"
   2.208  begin
   2.209  
   2.210 -lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 \<sqsubset> S2 \<Longrightarrow> m_s S1 > m_s S2"
   2.211 -proof(auto simp add: le_st_def m_s_def)
   2.212 -  assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
   2.213 +lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2"
   2.214 +proof(auto simp add: less_st_def less_eq_st_def m_s_def)
   2.215 +  assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x"
   2.216    hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1)
   2.217 -  fix x assume "x \<in> dom S2" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
   2.218 -  hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast
   2.219 +  fix x assume "x \<in> dom S2" "\<not> fun S2 x \<le> fun S1 x"
   2.220 +  hence 2: "\<exists>x\<in>dom S2. m(fun S1 x) > m(fun S2 x)" by (metis 0 m2 less_le_not_le)
   2.221    from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]
   2.222    show "(\<Sum>x\<in>dom S2. m (fun S2 x)) < (\<Sum>x\<in>dom S2. m (fun S1 x))" .
   2.223  qed
   2.224  
   2.225  lemma m_o2: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
   2.226 -  o1 \<sqsubset> o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
   2.227 -proof(induction o1 o2 rule: le_option.induct)
   2.228 -  case 1 thus ?case by (simp add: m_o_def L_st_def m_s2)
   2.229 +  o1 < o2 \<Longrightarrow> m_o (card X) o1 > m_o (card X) o2"
   2.230 +proof(induction o1 o2 rule: less_eq_option.induct)
   2.231 +  case 1 thus ?case by (auto simp: m_o_def L_st_def m_s2 less_option_def)
   2.232  next
   2.233 -  case 2 thus ?case
   2.234 -    by(auto simp add: m_o_def le_imp_less_Suc m_s_h)
   2.235 +  case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
   2.236  next
   2.237 -  case 3 thus ?case by simp
   2.238 +  case 3 thus ?case by (auto simp: less_option_def)
   2.239  qed
   2.240  
   2.241 -
   2.242 +find_theorems "(_<_) = _"
   2.243  lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
   2.244 -  C1 \<sqsubset> C2 \<Longrightarrow> m_c C1 > m_c C2"
   2.245 -proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] L_acom_def)
   2.246 +  C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
   2.247 +proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] less_acom_def L_acom_def)
   2.248    let ?X = "vars(strip C2)"
   2.249    let ?n = "card ?X"
   2.250    assume V1: "\<forall>a\<in>set(annos C1). a \<in> L ?X"
   2.251      and V2: "\<forall>a\<in>set(annos C2). a \<in> L ?X"
   2.252      and strip_eq: "strip C1 = strip C2"
   2.253 -    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<sqsubseteq> annos C2 ! i"
   2.254 +    and 0: "\<forall>i<size(annos C2). annos C1 ! i \<le> annos C2 ! i"
   2.255    hence 1: "\<forall>i<size(annos C2). m_o ?n (annos C1 ! i) \<ge> m_o ?n (annos C2 ! i)"
   2.256      by (auto simp: all_set_conv_all_nth)
   2.257         (metis finite_cvars m_o1 size_annos_same2)
   2.258 -  fix i assume "i < size(annos C2)" "\<not> annos C2 ! i \<sqsubseteq> annos C1 ! i"
   2.259 +  fix i assume "i < size(annos C2)" "\<not> annos C2 ! i \<le> annos C1 ! i"
   2.260    hence "m_o ?n (annos C1 ! i) > m_o ?n (annos C2 ! i)" (is "?P i")
   2.261 -    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0)
   2.262 +    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0 less_option_def)
   2.263    hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
   2.264    show "(\<Sum>i<size(annos C2). m_o ?n (annos C2 ! i))
   2.265           < (\<Sum>i<size(annos C2). m_o ?n (annos C1 ! i))"
   2.266 @@ -312,8 +308,7 @@
   2.267  
   2.268  lemma AI_Some_measure: "\<exists>C. AI c = Some C"
   2.269  unfolding AI_def
   2.270 -apply(rule pfp_termination[where I = "%C. strip C = c \<and> C \<in> L(vars c)"
   2.271 -  and m="m_c"])
   2.272 +apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> C \<in> L(vars c)" and m="m_c"])
   2.273  apply(simp_all add: m_c2 mono_step'_top bot_least)
   2.274  done
   2.275  
     3.1 --- a/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 14:10:07 2013 +0100
     3.2 +++ b/src/HOL/IMP/Abs_Int1_const.thy	Wed Mar 06 16:10:56 2013 +0100
     3.3 @@ -23,10 +23,12 @@
     3.4  instantiation const :: semilattice
     3.5  begin
     3.6  
     3.7 -fun le_const where
     3.8 -"_ \<sqsubseteq> Any = True" |
     3.9 -"Const n \<sqsubseteq> Const m = (n=m)" |
    3.10 -"Any \<sqsubseteq> Const _ = False"
    3.11 +fun less_eq_const where
    3.12 +"_ \<le> Any = True" |
    3.13 +"Const n \<le> Const m = (n=m)" |
    3.14 +"Any \<le> Const _ = False"
    3.15 +
    3.16 +definition "a < (b::const) = (a \<le> b & ~ b \<le> a)"
    3.17  
    3.18  fun join_const where
    3.19  "Const m \<squnion> Const n = (if n=m then Const m else Any)" |
    3.20 @@ -36,17 +38,21 @@
    3.21  
    3.22  instance
    3.23  proof
    3.24 -  case goal1 thus ?case by (cases x) simp_all
    3.25 +  case goal1 thus ?case by (rule less_const_def)
    3.26 +next
    3.27 +  case goal2 show ?case by (cases x) simp_all
    3.28  next
    3.29 -  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
    3.30 +  case goal3 thus ?case by(cases z, cases y, cases x, simp_all)
    3.31  next
    3.32 -  case goal3 thus ?case by(cases x, cases y, simp_all)
    3.33 +  case goal4 thus ?case by(cases x, cases y, simp_all, cases y, simp_all)
    3.34  next
    3.35 -  case goal4 thus ?case by(cases y, cases x, simp_all)
    3.36 +  case goal6 thus ?case by(cases x, cases y, simp_all)
    3.37 +next
    3.38 +  case goal7 thus ?case by(cases y, cases x, simp_all)
    3.39  next
    3.40 -  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
    3.41 +  case goal8 thus ?case by(cases z, cases y, cases x, simp_all)
    3.42  next
    3.43 -  case goal6 thus ?case by(simp add: Top_const_def)
    3.44 +  case goal5 thus ?case by(simp add: top_const_def)
    3.45  qed
    3.46  
    3.47  end
    3.48 @@ -58,7 +64,7 @@
    3.49    case goal1 thus ?case
    3.50      by(cases a, cases b, simp, simp, cases b, simp, simp)
    3.51  next
    3.52 -  case goal2 show ?case by(simp add: Top_const_def)
    3.53 +  case goal2 show ?case by(simp add: top_const_def)
    3.54  next
    3.55    case goal3 show ?case by simp
    3.56  next
    3.57 @@ -74,7 +80,7 @@
    3.58  
    3.59  subsubsection "Tests"
    3.60  
    3.61 -definition "steps c i = (step_const(top(vars c)) ^^ i) (bot c)"
    3.62 +definition "steps c i = (step_const(Top(vars c)) ^^ i) (bot c)"
    3.63  
    3.64  value "show_acom (steps test1_const 0)"
    3.65  value "show_acom (steps test1_const 1)"
    3.66 @@ -139,7 +145,7 @@
    3.67  next
    3.68    case goal2 thus ?case by(auto simp: m_const_def split: const.splits)
    3.69  next
    3.70 -  case goal3 thus ?case by(auto simp: m_const_def split: const.splits)
    3.71 +  case goal3 thus ?case by(auto simp: m_const_def less_const_def split: const.splits)
    3.72  qed
    3.73  
    3.74  thm AI_Some_measure
     4.1 --- a/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 14:10:07 2013 +0100
     4.2 +++ b/src/HOL/IMP/Abs_Int1_parity.thy	Wed Mar 06 16:10:56 2013 +0100
     4.3 @@ -1,3 +1,5 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6  theory Abs_Int1_parity
     4.7  imports Abs_Int1
     4.8  begin
     4.9 @@ -6,29 +8,41 @@
    4.10  
    4.11  datatype parity = Even | Odd | Either
    4.12  
    4.13 -text{* Instantiation of class @{class preord} with type @{typ parity}: *}
    4.14 +text{* Instantiation of class @{class order} with type @{typ parity}: *}
    4.15  
    4.16 -instantiation parity :: preord
    4.17 +instantiation parity :: order
    4.18  begin
    4.19  
    4.20 -text{* First the definition of the interface function @{text"\<sqsubseteq>"}. Note that
    4.21 -the header of the definition must refer to the ascii name @{const le} of the
    4.22 -constants as @{text le_parity} and the definition is named @{text
    4.23 -le_parity_def}.  Inside the definition the symbolic names can be used. *}
    4.24 +text{* First the definition of the interface function @{text"\<le>"}. Note that
    4.25 +the header of the definition must refer to the ascii name @{const less_eq} of the
    4.26 +constants as @{text less_eq_parity} and the definition is named @{text
    4.27 +less_eq_parity_def}.  Inside the definition the symbolic names can be used. *}
    4.28 +
    4.29 +definition less_eq_parity where
    4.30 +"x \<le> y = (y = Either \<or> x=y)"
    4.31  
    4.32 -definition le_parity where
    4.33 -"x \<sqsubseteq> y = (y = Either \<or> x=y)"
    4.34 +text{* We also need @{text"<"}, which is defined canonically: *}
    4.35  
    4.36 -text{* Now the instance proof, i.e.\ the proof that the definition fulfills
    4.37 +definition less_parity where
    4.38 +"x < y = (x \<le> y \<and> \<not> y \<le> (x::parity))"
    4.39 +
    4.40 +text{*\noindent (The type annotation is necessary to fix the type of the polymorphic predicates.)
    4.41 +
    4.42 +Now the instance proof, i.e.\ the proof that the definition fulfills
    4.43  the axioms (assumptions) of the class. The initial proof-step generates the
    4.44  necessary proof obligations. *}
    4.45  
    4.46  instance
    4.47  proof
    4.48 -  fix x::parity show "x \<sqsubseteq> x" by(auto simp: le_parity_def)
    4.49 +  fix x::parity show "x \<le> x" by(auto simp: less_eq_parity_def)
    4.50 +next
    4.51 +  fix x y z :: parity assume "x \<le> y" "y \<le> z" thus "x \<le> z"
    4.52 +    by(auto simp: less_eq_parity_def)
    4.53  next
    4.54 -  fix x y z :: parity assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    4.55 -    by(auto simp: le_parity_def)
    4.56 +  fix x y :: parity assume "x \<le> y" "y \<le> x" thus "x = y"
    4.57 +    by(auto simp: less_eq_parity_def)
    4.58 +next
    4.59 +  fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def)
    4.60  qed
    4.61  
    4.62  end
    4.63 @@ -39,9 +53,9 @@
    4.64  begin
    4.65  
    4.66  definition join_parity where
    4.67 -"x \<squnion> y = (if x \<sqsubseteq> y then y else if y \<sqsubseteq> x then x else Either)"
    4.68 +"x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)"
    4.69  
    4.70 -definition Top_parity where
    4.71 +definition top_parity where
    4.72  "\<top> = Either"
    4.73  
    4.74  text{* Now the instance proof. This time we take a lazy shortcut: we do not
    4.75 @@ -52,13 +66,13 @@
    4.76  
    4.77  instance
    4.78  proof
    4.79 -  case goal1 (*join1*) show ?case by(auto simp: le_parity_def join_parity_def)
    4.80 +  case goal1 (*top*) show ?case by(auto simp: less_eq_parity_def top_parity_def)
    4.81  next
    4.82 -  case goal2 (*join2*) show ?case by(auto simp: le_parity_def join_parity_def)
    4.83 +  case goal2 (*join1*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
    4.84  next
    4.85 -  case goal3 (*join least*) thus ?case by(auto simp: le_parity_def join_parity_def)
    4.86 +  case goal3 (*join2*) show ?case by(auto simp: less_eq_parity_def join_parity_def)
    4.87  next
    4.88 -  case goal4 (*Top*) show ?case by(auto simp: le_parity_def Top_parity_def)
    4.89 +  case goal4 (*join least*) thus ?case by(auto simp: less_eq_parity_def join_parity_def)
    4.90  qed
    4.91  
    4.92  end
    4.93 @@ -92,10 +106,10 @@
    4.94  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
    4.95  proof txt{* of the locale axioms *}
    4.96    fix a b :: parity
    4.97 -  assume "a \<sqsubseteq> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
    4.98 -    by(auto simp: le_parity_def)
    4.99 +  assume "a \<le> b" thus "\<gamma>_parity a \<subseteq> \<gamma>_parity b"
   4.100 +    by(auto simp: less_eq_parity_def)
   4.101  next txt{* The rest in the lazy, implicit way *}
   4.102 -  case goal2 show ?case by(auto simp: Top_parity_def)
   4.103 +  case goal2 show ?case by(auto simp: top_parity_def)
   4.104  next
   4.105    case goal3 show ?case by auto
   4.106  next
   4.107 @@ -127,7 +141,7 @@
   4.108    ''x'' ::= N 1;
   4.109    WHILE Less (V ''x'') (N 100) DO ''x'' ::= Plus (V ''x'') (N 3)"
   4.110  
   4.111 -definition "steps c i = (step_parity(top(vars c)) ^^ i) (bot c)"
   4.112 +definition "steps c i = (step_parity(Top(vars c)) ^^ i) (bot c)"
   4.113  
   4.114  value "show_acom (steps test2_parity 0)"
   4.115  value "show_acom (steps test2_parity 1)"
   4.116 @@ -147,7 +161,7 @@
   4.117    case goal1 thus ?case
   4.118    proof(cases a1 a2 b1 b2
   4.119     rule: parity.exhaust[case_product parity.exhaust[case_product parity.exhaust[case_product parity.exhaust]]]) (* FIXME - UGLY! *)
   4.120 -  qed (auto simp add:le_parity_def)
   4.121 +  qed (auto simp add:less_eq_parity_def)
   4.122  qed
   4.123  
   4.124  definition m_parity :: "parity \<Rightarrow> nat" where
   4.125 @@ -157,11 +171,11 @@
   4.126  where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
   4.127  and m = m_parity and h = "1"
   4.128  proof
   4.129 -  case goal1 thus ?case by(auto simp add: m_parity_def le_parity_def)
   4.130 +  case goal1 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
   4.131  next
   4.132 -  case goal2 thus ?case by(auto simp add: m_parity_def le_parity_def)
   4.133 +  case goal2 thus ?case by(auto simp add: m_parity_def less_eq_parity_def)
   4.134  next
   4.135 -  case goal3 thus ?case by(auto simp add: m_parity_def le_parity_def)
   4.136 +  case goal3 thus ?case by(auto simp add: m_parity_def less_eq_parity_def less_parity_def)
   4.137  qed
   4.138  
   4.139  thm AI_Some_measure
     5.1 --- a/src/HOL/IMP/Abs_Int2.thy	Wed Mar 06 14:10:07 2013 +0100
     5.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Wed Mar 06 16:10:56 2013 +0100
     5.3 @@ -4,16 +4,21 @@
     5.4  imports Abs_Int1
     5.5  begin
     5.6  
     5.7 -instantiation prod :: (preord,preord) preord
     5.8 +instantiation prod :: (order,order) order
     5.9  begin
    5.10  
    5.11 -definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    5.12 +definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
    5.13 +definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
    5.14  
    5.15  instance
    5.16  proof
    5.17 -  case goal1 show ?case by(simp add: le_prod_def)
    5.18 +  case goal1 show ?case by(rule less_prod_def)
    5.19 +next
    5.20 +  case goal2 show ?case by(simp add: less_eq_prod_def)
    5.21  next
    5.22 -  case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
    5.23 +  case goal3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
    5.24 +next
    5.25 +  case goal4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
    5.26  qed
    5.27  
    5.28  end
    5.29 @@ -23,13 +28,13 @@
    5.30  
    5.31  class lattice = semilattice + bot +
    5.32  fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
    5.33 -assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    5.34 -and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    5.35 -and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    5.36 +assumes meet_le1 [simp]: "x \<sqinter> y \<le> x"
    5.37 +and meet_le2 [simp]: "x \<sqinter> y \<le> y"
    5.38 +and meet_greatest: "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
    5.39  begin
    5.40  
    5.41 -lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
    5.42 -by (metis meet_greatest meet_le1 meet_le2 le_trans)
    5.43 +lemma mono_meet: "x \<le> x' \<Longrightarrow> y \<le> y' \<Longrightarrow> x \<sqinter> y \<le> x' \<sqinter> y'"
    5.44 +by (metis meet_greatest meet_le1 meet_le2 order_trans)
    5.45  
    5.46  end
    5.47  
    5.48 @@ -83,7 +88,7 @@
    5.49  "afilter (N n) a S = (if test_num' n a then S else None)" |
    5.50  "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    5.51    let a' = fun S x \<sqinter> a in
    5.52 -  if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
    5.53 +  if a' = \<bottom> then None else Some(update S x a'))" |
    5.54  "afilter (Plus e1 e2) a S =
    5.55   (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    5.56    in afilter e1 a1 (afilter e2 a2 S))"
    5.57 @@ -110,8 +115,7 @@
    5.58  
    5.59  lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
    5.60  by(induction e arbitrary: a S)
    5.61 -  (auto simp: Let_def update_def L_st_def
    5.62 -           split: option.splits prod.split)
    5.63 +  (auto simp: Let_def L_st_def split: option.splits prod.split)
    5.64  
    5.65  lemma afilter_sound: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
    5.66    s : \<gamma>\<^isub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^isub>o (afilter e a S)"
    5.67 @@ -189,7 +193,7 @@
    5.68    case Seq thus ?case by auto
    5.69  next
    5.70    case (If b _ C1 _ C2)
    5.71 -  hence 0: "post C1 \<sqsubseteq> post C1 \<squnion> post C2 \<and> post C2 \<sqsubseteq> post C1 \<squnion> post C2"
    5.72 +  hence 0: "post C1 \<le> post C1 \<squnion> post C2 \<and> post C2 \<le> post C1 \<squnion> post C2"
    5.73      by(simp, metis post_in_L join_ge1 join_ge2)
    5.74    have "vars b \<subseteq> X" using If.prems by simp
    5.75    note vars = `S \<in> L X` `vars b \<subseteq> X`
    5.76 @@ -204,26 +208,26 @@
    5.77  
    5.78  lemma step'_in_L[simp]: "\<lbrakk> C \<in> L X; S \<in> L X \<rbrakk> \<Longrightarrow> step' S C \<in> L X"
    5.79  proof(induction C arbitrary: S)
    5.80 -  case Assign thus ?case by(simp add: L_option_def L_st_def update_def split: option.splits)
    5.81 +  case Assign thus ?case by(auto simp add: L_option_def L_st_def split: option.splits)
    5.82  qed (auto simp add: bfilter_in_L)
    5.83  
    5.84  lemma AI_sound: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
    5.85  proof(simp add: CS_def AI_def)
    5.86 -  assume 1: "pfp (step' (top(vars c))) (bot c) = Some C"
    5.87 +  assume 1: "pfp (step' (Top(vars c))) (bot c) = Some C"
    5.88    have "C \<in> L(vars c)"
    5.89      by(rule pfp_inv[where P = "%C. C \<in> L(vars c)", OF 1 _ bot_in_L])
    5.90 -      (erule step'_in_L[OF _ top_in_L])
    5.91 -  have pfp': "step' (top(vars c)) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
    5.92 -  have 2: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    5.93 +      (erule step'_in_L[OF _ Top_in_L])
    5.94 +  have pfp': "step' (Top(vars c)) C \<le> C" by(rule pfp_pfp[OF 1])
    5.95 +  have 2: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
    5.96    proof(rule order_trans)
    5.97 -    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
    5.98 -      by(rule step_step'[OF `C \<in> L(vars c)` top_in_L])
    5.99 -    show "\<gamma>\<^isub>c (step' (top(vars c)) C) \<le> \<gamma>\<^isub>c C"
   5.100 +    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
   5.101 +      by(rule step_step'[OF `C \<in> L(vars c)` Top_in_L])
   5.102 +    show "\<gamma>\<^isub>c (step' (Top(vars c)) C) \<le> \<gamma>\<^isub>c C"
   5.103        by(rule mono_gamma_c[OF pfp'])
   5.104    qed
   5.105    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp[OF _ 1])
   5.106 -  have "lfp c (step (\<gamma>\<^isub>o(top(vars c)))) \<le> \<gamma>\<^isub>c C"
   5.107 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 2])
   5.108 +  have "lfp c (step (\<gamma>\<^isub>o(Top(vars c)))) \<le> \<gamma>\<^isub>c C"
   5.109 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 2])
   5.110    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   5.111  qed
   5.112  
   5.113 @@ -233,19 +237,19 @@
   5.114  subsubsection "Monotonicity"
   5.115  
   5.116  locale Abs_Int1_mono = Abs_Int1 +
   5.117 -assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
   5.118 -and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
   5.119 -  filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
   5.120 -and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
   5.121 -  filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
   5.122 +assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
   5.123 +and mono_filter_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
   5.124 +  filter_plus' r a1 a2 \<le> filter_plus' r' b1 b2"
   5.125 +and mono_filter_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
   5.126 +  filter_less' bv a1 a2 \<le> filter_less' bv b1 b2"
   5.127  begin
   5.128  
   5.129  lemma mono_aval':
   5.130 -  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<sqsubseteq> aval' e S2"
   5.131 -by(induction e) (auto simp: le_st_def mono_plus' L_st_def)
   5.132 +  "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval' e S1 \<le> aval' e S2"
   5.133 +by(induction e) (auto simp: less_eq_st_def mono_plus' L_st_def)
   5.134  
   5.135  lemma mono_aval'':
   5.136 -  "S1 \<sqsubseteq> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<sqsubseteq> aval'' e S2"
   5.137 +  "S1 \<le> S2 \<Longrightarrow> S1 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
   5.138  apply(cases S1)
   5.139   apply simp
   5.140  apply(cases S2)
   5.141 @@ -253,37 +257,37 @@
   5.142  by (simp add: mono_aval')
   5.143  
   5.144  lemma mono_afilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow>
   5.145 -  r1 \<sqsubseteq> r2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> afilter e r1 S1 \<sqsubseteq> afilter e r2 S2"
   5.146 +  r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> afilter e r1 S1 \<le> afilter e r2 S2"
   5.147  apply(induction e arbitrary: r1 r2 S1 S2)
   5.148  apply(auto simp: test_num' Let_def mono_meet split: option.splits prod.splits)
   5.149  apply (metis mono_gamma subsetD)
   5.150  apply(drule (2) mono_fun_L)
   5.151 -apply (metis mono_meet le_trans)
   5.152 -apply(metis mono_aval'' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
   5.153 +apply (metis mono_meet le_bot)
   5.154 +apply(metis mono_aval'' mono_filter_plus'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
   5.155  done
   5.156  
   5.157  lemma mono_bfilter: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> vars b \<subseteq> X \<Longrightarrow>
   5.158 -  S1 \<sqsubseteq> S2 \<Longrightarrow> bfilter b bv S1 \<sqsubseteq> bfilter b bv S2"
   5.159 +  S1 \<le> S2 \<Longrightarrow> bfilter b bv S1 \<le> bfilter b bv S2"
   5.160  apply(induction b arbitrary: bv S1 S2)
   5.161  apply(simp)
   5.162  apply(simp)
   5.163  apply simp
   5.164 -apply(metis join_least le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] bfilter_in_L)
   5.165 +apply(metis join_least order_trans[OF _ join_ge1] order_trans[OF _ join_ge2] bfilter_in_L)
   5.166  apply (simp split: prod.splits)
   5.167 -apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv afilter_in_L)
   5.168 +apply(metis mono_aval'' mono_afilter mono_filter_less'[simplified less_eq_prod_def] fst_conv snd_conv afilter_in_L)
   5.169  done
   5.170  
   5.171  theorem mono_step': "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   5.172 -  S1 \<sqsubseteq> S2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> step' S1 C1 \<sqsubseteq> step' S2 C2"
   5.173 -apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
   5.174 +  S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
   5.175 +apply(induction C1 C2 arbitrary: S1 S2 rule: less_eq_acom.induct)
   5.176  apply (auto simp: Let_def mono_bfilter mono_aval' mono_post
   5.177    le_join_disj le_join_disj[OF  post_in_L post_in_L] bfilter_in_L
   5.178              split: option.split)
   5.179  done
   5.180  
   5.181  lemma mono_step'_top: "C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow>
   5.182 -  C1 \<sqsubseteq> C2 \<Longrightarrow> step' (top X) C1 \<sqsubseteq> step' (top X) C2"
   5.183 -by (metis top_in_L mono_step' preord_class.le_refl)
   5.184 +  C1 \<le> C2 \<Longrightarrow> step' (Top X) C1 \<le> step' (Top X) C2"
   5.185 +by (metis Top_in_L mono_step' order_refl)
   5.186  
   5.187  end
   5.188  
     6.1 --- a/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 14:10:07 2013 +0100
     6.2 +++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Wed Mar 06 16:10:56 2013 +0100
     6.3 @@ -1,297 +1,341 @@
     6.4  (* Author: Tobias Nipkow *)
     6.5  
     6.6  theory Abs_Int2_ivl
     6.7 -imports Abs_Int2
     6.8 +imports "~~/src/HOL/Library/Quotient_List"
     6.9 +        "~~/src/HOL/Library/Extended"
    6.10 +        Abs_Int2
    6.11  begin
    6.12  
    6.13  subsection "Interval Analysis"
    6.14  
    6.15 -datatype lb = Minf | Lb int
    6.16 -datatype ub = Pinf | Ub int
    6.17 +type_synonym eint = "int extended"
    6.18 +type_synonym eint2 = "eint * eint"
    6.19  
    6.20 -datatype ivl = Ivl lb ub
    6.21 +definition \<gamma>_rep :: "eint2 \<Rightarrow> int set" where
    6.22 +"\<gamma>_rep p = (let (l,h) = p in {i. l \<le> Fin i \<and> Fin i \<le> h})"
    6.23  
    6.24 -definition "\<gamma>_ivl i = (case i of
    6.25 -  Ivl (Lb l) (Ub h) \<Rightarrow> {l..h} |
    6.26 -  Ivl (Lb l) Pinf \<Rightarrow> {l..} |
    6.27 -  Ivl Minf (Ub h) \<Rightarrow> {..h} |
    6.28 -  Ivl Minf Pinf \<Rightarrow> UNIV)"
    6.29 +definition eq_ivl :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
    6.30 +"eq_ivl p1 p2 = (\<gamma>_rep p1 = \<gamma>_rep p2)"
    6.31  
    6.32 -abbreviation Ivl_Lb_Ub :: "int \<Rightarrow> int \<Rightarrow> ivl"  ("{_\<dots>_}") where
    6.33 -"{lo\<dots>hi} == Ivl (Lb lo) (Ub hi)"
    6.34 -abbreviation Ivl_Lb_Pinf :: "int \<Rightarrow> ivl"  ("{_\<dots>}") where
    6.35 -"{lo\<dots>} == Ivl (Lb lo) Pinf"
    6.36 -abbreviation Ivl_Minf_Ub :: "int \<Rightarrow> ivl"  ("{\<dots>_}") where
    6.37 -"{\<dots>hi} == Ivl Minf (Ub hi)"
    6.38 -abbreviation Ivl_Minf_Pinf :: "ivl"  ("{\<dots>}") where
    6.39 -"{\<dots>} == Ivl Minf Pinf"
    6.40 +lemma refl_eq_ivl[simp]: "eq_ivl p p"
    6.41 +by(auto simp: eq_ivl_def)
    6.42  
    6.43 -lemmas lub_splits = lb.splits ub.splits
    6.44 -
    6.45 -definition "num_ivl n = {n\<dots>n}"
    6.46 +quotient_type ivl = eint2 / eq_ivl
    6.47 +by(rule equivpI)(auto simp: reflp_def symp_def transp_def eq_ivl_def)
    6.48  
    6.49 -fun in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" where
    6.50 -"in_ivl k (Ivl (Lb l) (Ub h)) \<longleftrightarrow> l \<le> k \<and> k \<le> h" |
    6.51 -"in_ivl k (Ivl (Lb l) Pinf) \<longleftrightarrow> l \<le> k" |
    6.52 -"in_ivl k (Ivl Minf (Ub h)) \<longleftrightarrow> k \<le> h" |
    6.53 -"in_ivl k (Ivl Minf Pinf) \<longleftrightarrow> True"
    6.54 +lift_definition \<gamma>_ivl :: "ivl \<Rightarrow> int set" is \<gamma>_rep
    6.55 +by(simp add: eq_ivl_def)
    6.56  
    6.57 -
    6.58 -instantiation lb :: linorder
    6.59 -begin
    6.60 +abbreviation ivl_abbr :: "eint \<Rightarrow> eint \<Rightarrow> ivl" ("[_\<dots>_]") where
    6.61 +"[l\<dots>h] == abs_ivl(l,h)"
    6.62  
    6.63 -definition less_eq_lb where
    6.64 -"l1 \<le> l2 = (case l1 of Minf \<Rightarrow> True | Lb i1 \<Rightarrow> (case l2 of Minf \<Rightarrow> False | Lb i2 \<Rightarrow> i1 \<le> i2))"
    6.65 +lift_definition num_ivl :: "int \<Rightarrow> ivl" is "\<lambda>i. (Fin i, Fin i)"
    6.66 +by(auto simp: eq_ivl_def)
    6.67  
    6.68 -definition less_lb :: "lb \<Rightarrow> lb \<Rightarrow> bool" where
    6.69 -"((l1::lb) < l2) = (l1 \<le> l2 & ~ l1 \<ge> l2)"
    6.70 +fun in_ivl_rep :: "int \<Rightarrow> eint2 \<Rightarrow> bool" where
    6.71 +"in_ivl_rep k (l,h) \<longleftrightarrow> l \<le> Fin k \<and> Fin k \<le> h"
    6.72  
    6.73 -instance
    6.74 -proof
    6.75 -  case goal1 show ?case by(rule less_lb_def)
    6.76 -next
    6.77 -  case goal2 show ?case by(auto simp: less_eq_lb_def split:lub_splits)
    6.78 -next
    6.79 -  case goal3 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    6.80 -next
    6.81 -  case goal4 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    6.82 -next
    6.83 -  case goal5 thus ?case by(auto simp: less_eq_lb_def split:lub_splits)
    6.84 -qed
    6.85 +lift_definition in_ivl :: "int \<Rightarrow> ivl \<Rightarrow> bool" is in_ivl_rep
    6.86 +by(auto simp: eq_ivl_def \<gamma>_rep_def)
    6.87 +
    6.88 +definition is_empty_rep :: "eint2 \<Rightarrow> bool" where
    6.89 +"is_empty_rep p = (let (l,h) = p in l>h | l=Pinf & h=Pinf | l=Minf & h=Minf)"
    6.90  
    6.91 -end
    6.92 -
    6.93 -instantiation ub :: linorder
    6.94 -begin
    6.95 +lemma \<gamma>_rep_cases: "\<gamma>_rep p = (case p of (Fin i,Fin j) => {i..j} | (Fin i,Pinf) => {i..} |
    6.96 +  (Minf,Fin i) \<Rightarrow> {..i} | (Minf,Pinf) \<Rightarrow> UNIV | _ \<Rightarrow> {})"
    6.97 +by(auto simp add: \<gamma>_rep_def split: prod.splits extended.splits)
    6.98  
    6.99 -definition less_eq_ub where
   6.100 -"u1 \<le> u2 = (case u2 of Pinf \<Rightarrow> True | Ub i2 \<Rightarrow> (case u1 of Pinf \<Rightarrow> False | Ub i1 \<Rightarrow> i1 \<le> i2))"
   6.101 -
   6.102 -definition less_ub :: "ub \<Rightarrow> ub \<Rightarrow> bool" where
   6.103 -"((u1::ub) < u2) = (u1 \<le> u2 & ~ u1 \<ge> u2)"
   6.104 +lift_definition  is_empty_ivl :: "ivl \<Rightarrow> bool" is is_empty_rep
   6.105 +apply(auto simp: eq_ivl_def \<gamma>_rep_cases is_empty_rep_def)
   6.106 +apply(auto simp: not_less less_eq_extended_cases split: extended.splits)
   6.107 +done
   6.108  
   6.109 -instance
   6.110 -proof
   6.111 -  case goal1 show ?case by(rule less_ub_def)
   6.112 -next
   6.113 -  case goal2 show ?case by(auto simp: less_eq_ub_def split:lub_splits)
   6.114 -next
   6.115 -  case goal3 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   6.116 -next
   6.117 -  case goal4 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   6.118 -next
   6.119 -  case goal5 thus ?case by(auto simp: less_eq_ub_def split:lub_splits)
   6.120 -qed
   6.121 +lemma eq_ivl_iff: "eq_ivl p1 p2 = (is_empty_rep p1 & is_empty_rep p2 | p1 = p2)"
   6.122 +by(auto simp: eq_ivl_def is_empty_rep_def \<gamma>_rep_cases Icc_eq_Icc split: prod.splits extended.splits)
   6.123  
   6.124 -end
   6.125 +definition empty_rep :: eint2 where "empty_rep = (Pinf,Minf)"
   6.126  
   6.127 -lemmas le_lub_defs = less_eq_lb_def less_eq_ub_def
   6.128 +lift_definition empty_ivl :: ivl is empty_rep
   6.129 +by simp
   6.130  
   6.131 -lemma le_lub_simps[simp]:
   6.132 -  "Minf \<le> l" "Lb i \<le> Lb j = (i \<le> j)" "~ Lb i \<le> Minf"
   6.133 -  "h \<le> Pinf" "Ub i \<le> Ub j = (i \<le> j)" "~ Pinf \<le> Ub j"
   6.134 -by(auto simp: le_lub_defs split: lub_splits)
   6.135 -
   6.136 -definition empty where "empty = {1\<dots>0}"
   6.137 +lemma is_empty_empty_rep[simp]: "is_empty_rep empty_rep"
   6.138 +by(auto simp add: is_empty_rep_def empty_rep_def)
   6.139  
   6.140 -fun is_empty where
   6.141 -"is_empty {l\<dots>h} = (h<l)" |
   6.142 -"is_empty _ = False"
   6.143 +lemma is_empty_rep_iff: "is_empty_rep p = (\<gamma>_rep p = {})"
   6.144 +by(auto simp add: \<gamma>_rep_cases is_empty_rep_def split: prod.splits extended.splits)
   6.145  
   6.146 -lemma [simp]: "is_empty(Ivl l h) =
   6.147 -  (case l of Lb l \<Rightarrow> (case h of Ub h \<Rightarrow> h<l | Pinf \<Rightarrow> False) | Minf \<Rightarrow> False)"
   6.148 -by(auto split: lub_splits)
   6.149 -
   6.150 -lemma [simp]: "is_empty i \<Longrightarrow> \<gamma>_ivl i = {}"
   6.151 -by(auto simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
   6.152 +declare is_empty_rep_iff[THEN iffD1, simp]
   6.153  
   6.154  
   6.155  instantiation ivl :: semilattice
   6.156  begin
   6.157  
   6.158 -fun le_aux where
   6.159 -"le_aux (Ivl l1 h1) (Ivl l2 h2) = (l2 \<le> l1 & h1 \<le> h2)"
   6.160 +definition le_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> bool" where
   6.161 +"le_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in
   6.162 +  if is_empty_rep(l1,h1) then True else
   6.163 +  if is_empty_rep(l2,h2) then False else l1 \<ge> l2 & h1 \<le> h2)"
   6.164 +
   6.165 +lemma le_iff_subset: "le_rep p1 p2 \<longleftrightarrow> \<gamma>_rep p1 \<subseteq> \<gamma>_rep p2"
   6.166 +apply rule
   6.167 +apply(auto simp: is_empty_rep_def le_rep_def \<gamma>_rep_def split: if_splits prod.splits)[1]
   6.168 +apply(auto simp: is_empty_rep_def \<gamma>_rep_cases le_rep_def)
   6.169 +apply(auto simp: not_less split: extended.splits)
   6.170 +done
   6.171 +
   6.172 +lift_definition less_eq_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool" is le_rep
   6.173 +by(auto simp: eq_ivl_def le_iff_subset)
   6.174  
   6.175 -definition le_ivl where
   6.176 -"i1 \<sqsubseteq> i2 =
   6.177 - (if is_empty i1 then True else
   6.178 -  if is_empty i2 then False else le_aux i1 i2)"
   6.179 +definition less_ivl where "i1 < i2 = (i1 \<le> i2 \<and> \<not> i2 \<le> (i1::ivl))"
   6.180 +
   6.181 +definition join_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   6.182 +"join_rep p1 p2 = (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1
   6.183 +  else let (l1,h1) = p1; (l2,h2) = p2 in  (min l1 l2, max h1 h2))"
   6.184  
   6.185 -definition "i1 \<squnion> i2 =
   6.186 - (if is_empty i1 then i2 else if is_empty i2 then i1
   6.187 -  else case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (min l1 l2) (max h1 h2))"
   6.188 +lift_definition join_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is join_rep
   6.189 +by(auto simp: eq_ivl_iff join_rep_def)
   6.190  
   6.191 -definition "\<top> = {\<dots>}"
   6.192 +lift_definition top_ivl :: ivl is "(Minf,Pinf)"
   6.193 +by(auto simp: eq_ivl_def)
   6.194 +
   6.195 +lemma is_empty_min_max:
   6.196 +  "\<not> is_empty_rep (l1,h1) \<Longrightarrow> \<not> is_empty_rep (l2, h2) \<Longrightarrow> \<not> is_empty_rep (min l1 l2, max h1 h2)"
   6.197 +by(auto simp add: is_empty_rep_def max_def min_def split: if_splits)
   6.198  
   6.199  instance
   6.200  proof
   6.201 -  case goal1 thus ?case
   6.202 -    by(cases x, simp add: le_ivl_def)
   6.203 +  case goal1 show ?case by (rule less_ivl_def)
   6.204 +next
   6.205 +  case goal2 show ?case by transfer (simp add: le_rep_def split: prod.splits)
   6.206  next
   6.207 -  case goal2 thus ?case
   6.208 -    by(cases x, cases y, cases z, auto simp: le_ivl_def split: if_splits)
   6.209 +  case goal3 thus ?case by transfer (auto simp: le_rep_def split: if_splits)
   6.210  next
   6.211 -  case goal3 thus ?case
   6.212 -    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
   6.213 +  case goal4 thus ?case by transfer (auto simp: le_rep_def eq_ivl_iff split: if_splits)
   6.214  next
   6.215 -  case goal4 thus ?case
   6.216 -    by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_lub_defs min_def max_def split: lub_splits)
   6.217 +  case goal6 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
   6.218 +next
   6.219 +  case goal7 thus ?case by transfer (auto simp add: le_rep_def join_rep_def is_empty_min_max)
   6.220  next
   6.221 -  case goal5 thus ?case
   6.222 -    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)
   6.223 +  case goal8 thus ?case by transfer (auto simp add: le_rep_def join_rep_def)
   6.224  next
   6.225 -  case goal6 thus ?case
   6.226 -    by(cases x, simp add: Top_ivl_def le_ivl_def le_lub_defs split: lub_splits)
   6.227 +  case goal5 show ?case by transfer (simp add: le_rep_def is_empty_rep_def)
   6.228  qed
   6.229  
   6.230  end
   6.231  
   6.232 +text{* Implement (naive) executable equality: *}
   6.233 +instantiation ivl :: equal
   6.234 +begin
   6.235 +
   6.236 +definition equal_ivl where
   6.237 +"equal_ivl i1 (i2::ivl) = (i1\<le>i2 \<and> i2 \<le> i1)"
   6.238 +
   6.239 +instance
   6.240 +proof
   6.241 +  case goal1 show ?case by(simp add: equal_ivl_def eq_iff)
   6.242 +qed
   6.243 +
   6.244 +end
   6.245 +
   6.246 +lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> x < Pinf) = (x = Pinf)"
   6.247 +by(simp add: not_less)
   6.248 +lemma [simp]: fixes x :: "'a::linorder extended" shows "(\<not> Minf < x) = (x = Minf)"
   6.249 +by(simp add: not_less)
   6.250  
   6.251  instantiation ivl :: lattice
   6.252  begin
   6.253  
   6.254 -definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
   6.255 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (max l1 l2) (min h1 h2))"
   6.256 +definition meet_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   6.257 +"meet_rep p1 p2 = (let (l1,h1) = p1; (l2,h2) = p2 in (max l1 l2, min h1 h2))"
   6.258  
   6.259 -definition "\<bottom> = empty"
   6.260 +lemma \<gamma>_meet_rep: "\<gamma>_rep(meet_rep p1 p2) = \<gamma>_rep p1 \<inter> \<gamma>_rep p2"
   6.261 +by(auto simp:meet_rep_def \<gamma>_rep_cases split: prod.splits extended.splits)
   6.262 +
   6.263 +lift_definition meet_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is meet_rep
   6.264 +by(auto simp: \<gamma>_meet_rep eq_ivl_def)
   6.265 +
   6.266 +definition "\<bottom> = empty_ivl"
   6.267  
   6.268  instance
   6.269  proof
   6.270    case goal2 thus ?case
   6.271 -    by (simp add:meet_ivl_def empty_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
   6.272 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   6.273  next
   6.274    case goal3 thus ?case
   6.275 -    by (simp add: empty_def meet_ivl_def le_ivl_def le_lub_defs max_def min_def split: ivl.splits lub_splits)
   6.276 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   6.277  next
   6.278    case goal4 thus ?case
   6.279 -    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)
   6.280 +    unfolding meet_rep_def by transfer (auto simp: le_iff_subset \<gamma>_meet_rep)
   6.281  next
   6.282 -  case goal1 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
   6.283 +  case goal1 show ?case unfolding bot_ivl_def by transfer (auto simp: le_iff_subset)
   6.284  qed
   6.285  
   6.286  end
   6.287  
   6.288  
   6.289 -instantiation lb :: plus
   6.290 +lemma eq_ivl_empty: "eq_ivl p empty_rep = is_empty_rep p"
   6.291 +by (metis eq_ivl_iff is_empty_empty_rep)
   6.292 +
   6.293 +lemma le_ivl_nice: "[l1\<dots>h1] \<le> [l2\<dots>h2] \<longleftrightarrow>
   6.294 +  (if [l1\<dots>h1] = \<bottom> then True else
   6.295 +   if [l2\<dots>h2] = \<bottom> then False else l1 \<ge> l2 & h1 \<le> h2)"
   6.296 +unfolding bot_ivl_def by transfer (simp add: le_rep_def eq_ivl_empty)
   6.297 +
   6.298 +lemma join_ivl_nice: "[l1\<dots>h1] \<squnion> [l2\<dots>h2] =
   6.299 +  (if [l1\<dots>h1] = \<bottom> then [l2\<dots>h2] else
   6.300 +   if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
   6.301 +unfolding bot_ivl_def by transfer (simp add: join_rep_def eq_ivl_empty)
   6.302 +
   6.303 +lemma meet_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
   6.304 +by transfer (simp add: meet_rep_def)
   6.305 +
   6.306 +
   6.307 +instantiation ivl :: plus
   6.308  begin
   6.309  
   6.310 -fun plus_lb where
   6.311 -"Lb x + Lb y = Lb(x+y)" |
   6.312 -"_ + _ = Minf"
   6.313 +definition plus_rep :: "eint2 \<Rightarrow> eint2 \<Rightarrow> eint2" where
   6.314 +"plus_rep p1 p2 =
   6.315 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
   6.316 +   let (l1,h1) = p1; (l2,h2) = p2 in (l1+l2, h1+h2))"
   6.317 +
   6.318 +lift_definition plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is plus_rep
   6.319 +by(auto simp: plus_rep_def eq_ivl_iff)
   6.320  
   6.321  instance ..
   6.322  end
   6.323  
   6.324 -instantiation ub :: plus
   6.325 -begin
   6.326 -
   6.327 -fun plus_ub where
   6.328 -"Ub x + Ub y = Ub(x+y)" |
   6.329 -"_ + _ = Pinf"
   6.330 -
   6.331 -instance ..
   6.332 -end
   6.333 -
   6.334 -instantiation ivl :: plus
   6.335 -begin
   6.336 +lemma plus_ivl_nice: "[l1\<dots>h1] + [l2\<dots>h2] =
   6.337 +  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then \<bottom> else [l1+l2 \<dots> h1+h2])"
   6.338 +unfolding bot_ivl_def by transfer (auto simp: plus_rep_def eq_ivl_empty)
   6.339  
   6.340 -definition "i1+i2 = (if is_empty i1 | is_empty i2 then empty else
   6.341 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1+l2) (h1+h2))"
   6.342 -
   6.343 -instance ..
   6.344 -end
   6.345 +lemma uminus_eq_Minf[simp]: "-x = Minf \<longleftrightarrow> x = Pinf"
   6.346 +by(cases x) auto
   6.347 +lemma uminus_eq_Pinf[simp]: "-x = Pinf \<longleftrightarrow> x = Minf"
   6.348 +by(cases x) auto
   6.349  
   6.350 -fun uminus_ub :: "ub \<Rightarrow> lb" where
   6.351 -"uminus_ub(Ub( x)) = Lb(-x)" |
   6.352 -"uminus_ub Pinf = Minf"
   6.353 -
   6.354 -fun uminus_lb :: "lb \<Rightarrow> ub" where
   6.355 -"uminus_lb(Lb( x)) = Ub(-x)" |
   6.356 -"uminus_lb Minf = Pinf"
   6.357 +lemma uminus_le_Fin_iff: "- x \<le> Fin(-y) \<longleftrightarrow> Fin y \<le> (x::'a::ordered_ab_group_add extended)"
   6.358 +by(cases x) auto
   6.359 +lemma Fin_uminus_le_iff: "Fin(-y) \<le> -x \<longleftrightarrow> x \<le> ((Fin y)::'a::ordered_ab_group_add extended)"
   6.360 +by(cases x) auto
   6.361  
   6.362  instantiation ivl :: uminus
   6.363  begin
   6.364  
   6.365 -fun uminus_ivl where
   6.366 -"-(Ivl l h) = Ivl (uminus_ub h) (uminus_lb l)"
   6.367 -
   6.368 -instance ..
   6.369 -end
   6.370 +definition uminus_rep :: "eint2 \<Rightarrow> eint2" where
   6.371 +"uminus_rep p = (let (l,h) = p in (-h, -l))"
   6.372  
   6.373 -instantiation ivl :: minus
   6.374 -begin
   6.375 +lemma \<gamma>_uminus_rep: "i : \<gamma>_rep p \<Longrightarrow> -i \<in> \<gamma>_rep(uminus_rep p)"
   6.376 +by(auto simp: uminus_rep_def \<gamma>_rep_def image_def uminus_le_Fin_iff Fin_uminus_le_iff
   6.377 +        split: prod.split)
   6.378  
   6.379 -definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where
   6.380 -"(i1::ivl) - i2 = i1 + -i2"
   6.381 +lift_definition uminus_ivl :: "ivl \<Rightarrow> ivl" is uminus_rep
   6.382 +by (auto simp: uminus_rep_def eq_ivl_def \<gamma>_rep_cases)
   6.383 +   (auto simp: Icc_eq_Icc split: extended.splits)
   6.384  
   6.385  instance ..
   6.386  end
   6.387  
   6.388 -lemma minus_ivl_cases: "i1 - i2 = (if is_empty i1 | is_empty i2 then empty else
   6.389 -  case (i1,i2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow> Ivl (l1 + uminus_ub h2) (h1 + uminus_lb l2))"
   6.390 -by(auto simp: plus_ivl_def minus_ivl_def split: ivl.split lub_splits)
   6.391 +lemma uminus_nice: "-[l\<dots>h] = [-h\<dots>-l]"
   6.392 +by transfer (simp add: uminus_rep_def)
   6.393 +
   6.394 +instantiation ivl :: minus
   6.395 +begin
   6.396 +definition minus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" where "(iv1::ivl) - iv2 = iv1 + -iv2"
   6.397 +instance ..
   6.398 +end
   6.399 +
   6.400  
   6.401 -lemma gamma_minus_ivl:
   6.402 -  "n1 : \<gamma>_ivl i1 \<Longrightarrow> n2 : \<gamma>_ivl i2 \<Longrightarrow> n1-n2 : \<gamma>_ivl(i1 - i2)"
   6.403 -by(auto simp add: minus_ivl_def plus_ivl_def \<gamma>_ivl_def split: ivl.splits lub_splits)
   6.404 +definition filter_plus_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl*ivl" where
   6.405 +"filter_plus_ivl iv iv1 iv2 = (iv1 \<sqinter> (iv - iv2), iv2 \<sqinter> (iv - iv1))"
   6.406 +
   6.407 +definition filter_less_rep :: "bool \<Rightarrow> eint2 \<Rightarrow> eint2 \<Rightarrow> eint2 * eint2" where
   6.408 +"filter_less_rep res p1 p2 =
   6.409 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then (empty_rep,empty_rep) else
   6.410 +   let (l1,h1) = p1; (l2,h2) = p2 in
   6.411 +   if res
   6.412 +   then ((l1, min h1 (h2 + Fin -1)), (max (l1 + Fin 1) l2, h2))
   6.413 +   else ((max l1 l2, h1), (l2, min h1 h2)))"
   6.414  
   6.415 -definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   6.416 -  i1 \<sqinter> (i - i2), i2 \<sqinter> (i - i1))"
   6.417 +lift_definition filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" is filter_less_rep
   6.418 +by(auto simp: prod_pred_def filter_less_rep_def eq_ivl_iff)
   6.419 +declare filter_less_ivl.abs_eq[code] (* bug in lifting *)
   6.420 +
   6.421 +lemma filter_less_ivl_nice: "filter_less_ivl b [l1\<dots>h1] [l2\<dots>h2] =
   6.422 +  (if [l1\<dots>h1] = \<bottom> \<or> [l2\<dots>h2] = \<bottom> then (\<bottom>,\<bottom>) else
   6.423 +   if b
   6.424 +   then ([l1 \<dots> min h1 (h2 + Fin -1)], [max (l1 + Fin 1) l2 \<dots> h2])
   6.425 +   else ([max l1 l2 \<dots> h1], [l2 \<dots> min h1 h2]))"
   6.426 +unfolding prod_rel_eq[symmetric] bot_ivl_def
   6.427 +by transfer (auto simp: filter_less_rep_def eq_ivl_empty)
   6.428  
   6.429 -fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
   6.430 -"filter_less_ivl res (Ivl l1 h1) (Ivl l2 h2) =
   6.431 -  (if is_empty(Ivl l1 h1) \<or> is_empty(Ivl l2 h2) then (empty, empty) else
   6.432 -   if res
   6.433 -   then (Ivl l1 (min h1 (h2 + Ub -1)), Ivl (max (l1 + Lb 1) l2) h2)
   6.434 -   else (Ivl (max l1 l2) h1, Ivl l2 (min h1 h2)))"
   6.435 +lemma add_mono_le_Fin:
   6.436 +  "\<lbrakk>x1 \<le> Fin y1; x2 \<le> Fin y2\<rbrakk> \<Longrightarrow> x1 + x2 \<le> Fin (y1 + (y2::'a::ordered_ab_group_add))"
   6.437 +by(drule (1) add_mono) simp
   6.438 +
   6.439 +lemma add_mono_Fin_le:
   6.440 +  "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
   6.441 +by(drule (1) add_mono) simp
   6.442 +
   6.443 +lemma plus_rep_plus:
   6.444 +  "\<lbrakk> i1 \<in> \<gamma>_rep (l1,h1); i2 \<in> \<gamma>_rep (l2, h2)\<rbrakk> \<Longrightarrow> i1 + i2 \<in> \<gamma>_rep (l1 + l2, h1 + h2)"
   6.445 +by(simp add: \<gamma>_rep_def add_mono_Fin_le add_mono_le_Fin)
   6.446  
   6.447  interpretation Val_abs
   6.448  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   6.449  proof
   6.450 -  case goal1 thus ?case
   6.451 -    by(auto simp: \<gamma>_ivl_def le_ivl_def le_lub_defs split: ivl.split lub_splits if_splits)
   6.452 +  case goal1 thus ?case by transfer (simp add: le_iff_subset)
   6.453  next
   6.454 -  case goal2 show ?case by(simp add: \<gamma>_ivl_def Top_ivl_def)
   6.455 +  case goal2 show ?case by transfer (simp add: \<gamma>_rep_def)
   6.456  next
   6.457 -  case goal3 thus ?case by(simp add: \<gamma>_ivl_def num_ivl_def)
   6.458 +  case goal3 show ?case by transfer (simp add: \<gamma>_rep_def)
   6.459  next
   6.460    case goal4 thus ?case
   6.461 -    by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split lub_splits)
   6.462 +    apply transfer
   6.463 +    apply(auto simp: \<gamma>_rep_def plus_rep_def add_mono_le_Fin add_mono_Fin_le)
   6.464 +    by(auto simp: empty_rep_def is_empty_rep_def)
   6.465  qed
   6.466  
   6.467 +
   6.468  interpretation Val_abs1_gamma
   6.469  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   6.470  defines aval_ivl is aval'
   6.471  proof
   6.472 -  case goal1 thus ?case
   6.473 -    by(auto simp add: \<gamma>_ivl_def meet_ivl_def empty_def min_def max_def split: ivl.split lub_splits)
   6.474 +  case goal1 show ?case
   6.475 +    by transfer (auto simp add:meet_rep_def \<gamma>_rep_cases split: prod.split extended.split)
   6.476  next
   6.477 -  case goal2 show ?case by(auto simp add: bot_ivl_def \<gamma>_ivl_def empty_def)
   6.478 +  case goal2 show ?case unfolding bot_ivl_def by transfer simp
   6.479  qed
   6.480  
   6.481 -lemma mono_minus_ivl: fixes i1 :: ivl
   6.482 -shows "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> i1 - i2 \<sqsubseteq> i1' - i2'"
   6.483 -apply(auto simp add: minus_ivl_cases empty_def le_ivl_def le_lub_defs split: ivl.splits)
   6.484 -  apply(simp split: lub_splits)
   6.485 - apply(simp split: lub_splits)
   6.486 -apply(simp split: lub_splits)
   6.487 -done
   6.488 +lemma \<gamma>_plus_rep: "i1 : \<gamma>_rep p1 \<Longrightarrow> i2 : \<gamma>_rep p2 \<Longrightarrow> i1+i2 \<in> \<gamma>_rep(plus_rep p1 p2)"
   6.489 +by(auto simp: plus_rep_def plus_rep_plus split: prod.splits)
   6.490  
   6.491 +lemma non_empty_meet: "\<lbrakk>n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a \<rbrakk> \<Longrightarrow>
   6.492 +     \<not> is_empty_rep (meet_rep a1 (plus_rep a (uminus_rep a2)))"
   6.493 +by (auto simp add: \<gamma>_meet_rep set_eq_iff is_empty_rep_iff simp del: all_not_in_conv)
   6.494 +   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_minus)
   6.495 +
   6.496 +lemma filter_plus: "\<lbrakk>eq_ivl (meet_rep a1 (plus_rep a (uminus_rep a2))) b1 \<and>
   6.497 +       eq_ivl (meet_rep a2 (plus_rep a (uminus_rep a1))) b2;
   6.498 +        n1 \<in> \<gamma>_rep a1; n2 \<in> \<gamma>_rep a2; n1 + n2 \<in> \<gamma>_rep a\<rbrakk>
   6.499 +       \<Longrightarrow> n1 \<in> \<gamma>_rep b1 \<and> n2 \<in> \<gamma>_rep b2"
   6.500 +by (auto simp: eq_ivl_iff \<gamma>_meet_rep non_empty_meet add_ac)
   6.501 +   (metis \<gamma>_plus_rep \<gamma>_uminus_rep add_diff_cancel diff_def add_commute)+
   6.502  
   6.503  interpretation Val_abs1
   6.504  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   6.505  and test_num' = in_ivl
   6.506  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   6.507  proof
   6.508 -  case goal1 thus ?case
   6.509 -    by (simp add: \<gamma>_ivl_def split: ivl.split lub_splits)
   6.510 +  case goal1 thus ?case by transfer (auto simp: \<gamma>_rep_def)
   6.511  next
   6.512 -  case goal2 thus ?case
   6.513 -    by(auto simp add: filter_plus_ivl_def)
   6.514 -      (metis gamma_minus_ivl add_diff_cancel add_commute)+
   6.515 +  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def prod_rel_eq[symmetric]
   6.516 +    by transfer (simp add: filter_plus)
   6.517  next
   6.518    case goal3 thus ?case
   6.519 -    by(cases a1, cases a2, auto simp: \<gamma>_ivl_def min_def max_def split: if_splits lub_splits)
   6.520 +    unfolding prod_rel_eq[symmetric]
   6.521 +    apply transfer
   6.522 +    apply (auto simp add: filter_less_rep_def eq_ivl_iff max_def min_def split: if_splits)
   6.523 +    apply(auto simp: \<gamma>_rep_cases is_empty_rep_def split: extended.splits)
   6.524 +    done
   6.525  qed
   6.526  
   6.527  interpretation Abs_Int1
   6.528 @@ -308,25 +352,41 @@
   6.529  
   6.530  text{* Monotonicity: *}
   6.531  
   6.532 +lemma mono_meet_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (meet_rep p1 q1) (meet_rep p2 q2)"
   6.533 +by(auto simp add: le_iff_subset \<gamma>_meet_rep)
   6.534 +
   6.535 +lemma mono_plus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep q1 q2 \<Longrightarrow> le_rep (plus_rep p1 q1) (plus_rep p2 q2)"
   6.536 +apply(auto simp: plus_rep_def le_iff_subset split: if_splits)
   6.537 +by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   6.538 +
   6.539 +lemma mono_minus_rep: "le_rep p1 p2 \<Longrightarrow> le_rep (uminus_rep p1) (uminus_rep p2)"
   6.540 +apply(auto simp: uminus_rep_def le_iff_subset split: if_splits prod.split)
   6.541 +by(auto simp: \<gamma>_rep_cases split: extended.splits)
   6.542 +
   6.543  interpretation Abs_Int1_mono
   6.544  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   6.545  and test_num' = in_ivl
   6.546  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   6.547  proof
   6.548 -  case goal1 thus ?case
   6.549 -    by(auto simp: plus_ivl_def le_ivl_def le_lub_defs empty_def split: if_splits ivl.splits lub_splits)
   6.550 +  case goal1 thus ?case by transfer (rule mono_plus_rep)
   6.551 +next
   6.552 +  case goal2 thus ?case unfolding filter_plus_ivl_def minus_ivl_def less_eq_prod_def
   6.553 +    by transfer (auto simp: mono_meet_rep mono_plus_rep mono_minus_rep)
   6.554  next
   6.555 -  case goal2 thus ?case
   6.556 -    by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
   6.557 -next
   6.558 -  case goal3 thus ?case
   6.559 -    apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
   6.560 -    by(auto simp add: empty_def le_ivl_def le_lub_defs min_def max_def split: lub_splits)
   6.561 +  case goal3 thus ?case unfolding less_eq_prod_def
   6.562 +    apply transfer
   6.563 +    apply(auto simp:filter_less_rep_def le_iff_subset min_def max_def split: if_splits)
   6.564 +    by(auto simp:is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
   6.565  qed
   6.566  
   6.567  
   6.568  subsubsection "Tests"
   6.569  
   6.570 +(* Hide Fin in numerals on output *)
   6.571 +declare
   6.572 +Fin_numeral [code_post] Fin_neg_numeral [code_post]
   6.573 +zero_extended_def[symmetric, code_post] one_extended_def[symmetric, code_post]
   6.574 +
   6.575  value "show_acom_opt (AI_ivl test1_ivl)"
   6.576  
   6.577  text{* Better than @{text AI_const}: *}
   6.578 @@ -334,7 +394,7 @@
   6.579  value "show_acom_opt (AI_ivl test4_const)"
   6.580  value "show_acom_opt (AI_ivl test6_const)"
   6.581  
   6.582 -definition "steps c i = (step_ivl(top(vars c)) ^^ i) (bot c)"
   6.583 +definition "steps c i = (step_ivl(Top(vars c)) ^^ i) (bot c)"
   6.584  
   6.585  value "show_acom_opt (AI_ivl test2_ivl)"
   6.586  value "show_acom (steps test2_ivl 0)"
     7.1 --- a/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 14:10:07 2013 +0100
     7.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 16:10:56 2013 +0100
     7.3 @@ -65,17 +65,17 @@
     7.4  class narrow =
     7.5  fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
     7.6  
     7.7 -class WN = widen + narrow + preord +
     7.8 -assumes widen1: "x \<sqsubseteq> x \<nabla> y"
     7.9 -assumes widen2: "y \<sqsubseteq> x \<nabla> y"
    7.10 -assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    7.11 -assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    7.12 +class WN = widen + narrow + order +
    7.13 +assumes widen1: "x \<le> x \<nabla> y"
    7.14 +assumes widen2: "y \<le> x \<nabla> y"
    7.15 +assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
    7.16 +assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
    7.17  
    7.18 -class WN_Lc = widen + narrow + preord + Lc +
    7.19 -assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
    7.20 -assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
    7.21 -assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    7.22 -assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    7.23 +class WN_Lc = widen + narrow + order + Lc +
    7.24 +assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<le> x \<nabla> y"
    7.25 +assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<le> x \<nabla> y"
    7.26 +assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
    7.27 +assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
    7.28  assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c"
    7.29  assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c"
    7.30  
    7.31 @@ -83,22 +83,25 @@
    7.32  instantiation ivl :: WN
    7.33  begin
    7.34  
    7.35 -definition "widen_ivl ivl1 ivl2 =
    7.36 -  ((*if is_empty ivl1 then ivl2 else
    7.37 -   if is_empty ivl2 then ivl1 else*)
    7.38 -     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    7.39 -       Ivl (if l2 \<le> l1 \<and> l2 \<noteq> l1 then Minf else l1)
    7.40 -           (if h1 \<le> h2 \<and> h1 \<noteq> h2 then Pinf else h1))"
    7.41 +definition "widen_rep p1 p2 =
    7.42 +  (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
    7.43 +   let (l1,h1) = p1; (l2,h2) = p2
    7.44 +   in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
    7.45 +
    7.46 +lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
    7.47 +by(auto simp: widen_rep_def eq_ivl_iff)
    7.48  
    7.49 -definition "narrow_ivl ivl1 ivl2 =
    7.50 -  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
    7.51 -     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    7.52 -       Ivl (if l1 = Minf then l2 else l1)
    7.53 -           (if h1 = Pinf then h2 else h1))"
    7.54 +definition "narrow_rep p1 p2 =
    7.55 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
    7.56 +   let (l1,h1) = p1; (l2,h2) = p2
    7.57 +   in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
    7.58 +
    7.59 +lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
    7.60 +by(auto simp: narrow_rep_def eq_ivl_iff)
    7.61  
    7.62  instance
    7.63 -proof qed
    7.64 -  (auto simp add: widen_ivl_def narrow_ivl_def le_lub_defs le_ivl_def empty_def split: ivl.split lub_splits if_splits)
    7.65 +proof
    7.66 +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)+
    7.67  
    7.68  end
    7.69  
    7.70 @@ -106,23 +109,20 @@
    7.71  instantiation st :: (WN)WN_Lc
    7.72  begin
    7.73  
    7.74 -definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
    7.75 +definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
    7.76  
    7.77 -definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
    7.78 +definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
    7.79  
    7.80  instance
    7.81  proof
    7.82 -  case goal1 thus ?case
    7.83 -    by(simp add: widen_st_def le_st_def WN_class.widen1)
    7.84 +  case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1)
    7.85  next
    7.86    case goal2 thus ?case
    7.87 -    by(simp add: widen_st_def le_st_def WN_class.widen2 Lc_st_def L_st_def)
    7.88 +    by(simp add: widen_st_def less_eq_st_def WN_class.widen2 Lc_st_def L_st_def)
    7.89  next
    7.90 -  case goal3 thus ?case
    7.91 -    by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
    7.92 +  case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1)
    7.93  next
    7.94 -  case goal4 thus ?case
    7.95 -    by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
    7.96 +  case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2)
    7.97  next
    7.98    case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
    7.99  next
   7.100 @@ -196,14 +196,14 @@
   7.101  
   7.102  lemma widen_acom1: fixes C1 :: "'a acom" shows
   7.103    "\<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>
   7.104 -   \<Longrightarrow> C1 \<sqsubseteq> C1 \<nabla> C2"
   7.105 -by(induct C1 C2 rule: le_acom.induct)
   7.106 +   \<Longrightarrow> C1 \<le> C1 \<nabla> C2"
   7.107 +by(induct C1 C2 rule: less_eq_acom.induct)
   7.108    (auto simp: widen_acom_def widen1 Lc_acom_def)
   7.109  
   7.110  lemma widen_acom2: fixes C1 :: "'a acom" shows
   7.111    "\<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>
   7.112 -   \<Longrightarrow> C2 \<sqsubseteq> C1 \<nabla> C2"
   7.113 -by(induct C1 C2 rule: le_acom.induct)
   7.114 +   \<Longrightarrow> C2 \<le> C1 \<nabla> C2"
   7.115 +by(induct C1 C2 rule: less_eq_acom.induct)
   7.116    (auto simp: widen_acom_def widen2 Lc_acom_def)
   7.117  
   7.118  lemma strip_map2_acom[simp]:
   7.119 @@ -229,10 +229,10 @@
   7.120    case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
   7.121  next
   7.122    case goal3 thus ?case
   7.123 -    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
   7.124 +    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
   7.125  next
   7.126    case goal4 thus ?case
   7.127 -    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
   7.128 +    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
   7.129  next
   7.130    case goal5 thus ?case
   7.131      by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE)
   7.132 @@ -255,12 +255,12 @@
   7.133  
   7.134  lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom"
   7.135  shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X"
   7.136 -by(induction C1 C2 rule: le_acom.induct)
   7.137 +by(induction C1 C2 rule: less_eq_acom.induct)
   7.138    (auto simp: widen_acom_def)
   7.139  
   7.140  lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom"
   7.141  shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X"
   7.142 -by(induction C1 C2 rule: le_acom.induct)
   7.143 +by(induction C1 C2 rule: less_eq_acom.induct)
   7.144    (auto simp: narrow_acom_def)
   7.145  
   7.146  lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
   7.147 @@ -269,18 +269,18 @@
   7.148  
   7.149  subsubsection "Post-fixed point computation"
   7.150  
   7.151 -definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
   7.152 -where "iter_widen f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) (\<lambda>x. x \<nabla> f x)"
   7.153 +definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
   7.154 +where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
   7.155  
   7.156 -definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
   7.157 -where "iter_narrow f = while_option (\<lambda>x. \<not> x \<sqsubseteq> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
   7.158 +definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
   7.159 +where "iter_narrow f = while_option (\<lambda>x. \<not> x \<le> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
   7.160  
   7.161 -definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   7.162 +definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   7.163  where "pfp_wn f x =
   7.164    (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
   7.165  
   7.166  
   7.167 -lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
   7.168 +lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
   7.169  by(auto simp add: iter_widen_def dest: while_option_stop)
   7.170  
   7.171  lemma iter_widen_inv:
   7.172 @@ -295,7 +295,7 @@
   7.173  using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
   7.174  by (metis assms(1))
   7.175  
   7.176 -lemma strip_iter_widen: fixes f :: "'a::{preord,widen} acom \<Rightarrow> 'a acom"
   7.177 +lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
   7.178  assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
   7.179  shows "strip C' = strip C"
   7.180  proof-
   7.181 @@ -305,12 +305,12 @@
   7.182  qed
   7.183  
   7.184  lemma iter_narrow_pfp:
   7.185 -assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   7.186 +assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   7.187  and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   7.188 -and "P p0" and "f p0 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
   7.189 -shows "P p \<and> f p \<sqsubseteq> p"
   7.190 +and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
   7.191 +shows "P p \<and> f p \<le> p"
   7.192  proof-
   7.193 -  let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
   7.194 +  let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
   7.195    { fix p assume "?Q p"
   7.196      note P = conjunct1[OF this] and 12 = conjunct2[OF this]
   7.197      note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
   7.198 @@ -318,12 +318,12 @@
   7.199      have "?Q ?p'"
   7.200      proof auto
   7.201        show "P ?p'" by (blast intro: P Pinv)
   7.202 -      have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
   7.203 -      also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
   7.204 -      finally show "f ?p' \<sqsubseteq> ?p'" .
   7.205 -      have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
   7.206 -      also have "p \<sqsubseteq> p0" by(rule 2)
   7.207 -      finally show "?p' \<sqsubseteq> p0" .
   7.208 +      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
   7.209 +      also have "\<dots> \<le> ?p'" by(rule narrow1[OF 1])
   7.210 +      finally show "f ?p' \<le> ?p'" .
   7.211 +      have "?p' \<le> p" by (rule narrow2[OF 1])
   7.212 +      also have "p \<le> p0" by(rule 2)
   7.213 +      finally show "?p' \<le> p0" .
   7.214      qed
   7.215    }
   7.216    thus ?thesis
   7.217 @@ -332,11 +332,11 @@
   7.218  qed
   7.219  
   7.220  lemma pfp_wn_pfp:
   7.221 -assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   7.222 +assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   7.223  and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   7.224    "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   7.225    "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   7.226 -and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
   7.227 +and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
   7.228  proof-
   7.229    from pfp_wn obtain p0
   7.230      where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
   7.231 @@ -358,24 +358,24 @@
   7.232  begin
   7.233  
   7.234  definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
   7.235 -"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
   7.236 +"AI_wn c = pfp_wn (step' (Top(vars c))) (bot c)"
   7.237  
   7.238  lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   7.239  proof(simp add: CS_def AI_wn_def)
   7.240 -  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
   7.241 -  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
   7.242 +  assume 1: "pfp_wn (step' (Top(vars c))) (bot c) = Some C"
   7.243 +  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<le> C"
   7.244      by(rule pfp_wn_pfp[where x="bot c"])
   7.245        (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
   7.246 -  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   7.247 +  have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   7.248    proof(rule order_trans)
   7.249 -    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
   7.250 -      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
   7.251 +    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
   7.252 +      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] Top_in_L])
   7.253      show "... \<le> \<gamma>\<^isub>c C"
   7.254        by(rule mono_gamma_c[OF conjunct2[OF 2]])
   7.255    qed
   7.256    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
   7.257 -  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
   7.258 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
   7.259 +  have "lfp c (step (\<gamma>\<^isub>o (Top(vars c)))) \<le> \<gamma>\<^isub>c C"
   7.260 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp])
   7.261    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   7.262  qed
   7.263  
   7.264 @@ -391,14 +391,10 @@
   7.265  
   7.266  subsubsection "Tests"
   7.267  
   7.268 -(* Trick to make the code generator happy. *)
   7.269 -lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
   7.270 -by(rule refl)
   7.271 -
   7.272  definition "step_up_ivl n =
   7.273 -  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
   7.274 +  ((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) C)^^n)"
   7.275  definition "step_down_ivl n =
   7.276 -  ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
   7.277 +  ((\<lambda>C. C \<triangle> step_ivl (Top(vars(strip C))) C)^^n)"
   7.278  
   7.279  text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
   7.280  the loop took to execute. In contrast, @{const AI_ivl'} converges in a
   7.281 @@ -430,32 +426,31 @@
   7.282  
   7.283  locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
   7.284  fixes n :: "'av \<Rightarrow> nat"
   7.285 -assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
   7.286 -assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
   7.287 -assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
   7.288 +assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
   7.289 +assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y"
   7.290 +assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
   7.291  
   7.292  begin
   7.293  
   7.294  lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
   7.295 -  ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
   7.296 -proof(auto simp add: le_st_def m_s_def L_st_def widen_st_def)
   7.297 +  ~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
   7.298 +proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def)
   7.299    assume "finite(dom S1)"
   7.300    have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
   7.301      by (metis m1 WN_class.widen1)
   7.302 -  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
   7.303 +  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x"
   7.304    hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
   7.305      using m_widen by blast
   7.306    from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
   7.307    show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
   7.308  qed
   7.309  
   7.310 -lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
   7.311 +lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   7.312    m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
   7.313 -by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen
   7.314 -        split: option.split)
   7.315 +by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
   7.316  
   7.317  lemma m_c_widen:
   7.318 -  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   7.319 +  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   7.320  apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
   7.321  apply(subgoal_tac "length(annos C2) = length(annos C1)")
   7.322  prefer 2 apply (simp add: size_annos_same2)
   7.323 @@ -475,25 +470,25 @@
   7.324  definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
   7.325  "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
   7.326  
   7.327 -lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
   7.328 +lemma n_s_mono: assumes "S1 \<le> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
   7.329  proof-
   7.330 -  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
   7.331 -    by(simp_all add: le_st_def)
   7.332 +  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<le> fun S2 x"
   7.333 +    by(simp_all add: less_eq_st_def)
   7.334    have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
   7.335 -    by(rule setsum_mono)(simp add: le_st_def n_mono)
   7.336 +    by(rule setsum_mono)(simp add: less_eq_st_def n_mono)
   7.337    thus ?thesis by(simp add: n_s_def)
   7.338  qed
   7.339  
   7.340  lemma n_s_narrow:
   7.341 -assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
   7.342 +assumes "finite(dom S1)" and "S2 \<le> S1" "\<not> S1 \<le> S1 \<triangle> S2"
   7.343  shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
   7.344  proof-
   7.345 -  from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
   7.346 -    by(simp_all add: le_st_def)
   7.347 +  from `S2\<le>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x"
   7.348 +    by(simp_all add: less_eq_st_def)
   7.349    have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
   7.350 -    by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
   7.351 -  have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<sqsubseteq> S1 \<triangle> S2`
   7.352 -    by(force simp: le_st_def narrow_st_def intro: n_narrow)
   7.353 +    by(auto simp: less_eq_st_def narrow_st_def n_mono WN_class.narrow2)
   7.354 +  have 2: "\<exists>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) < n(fun S1 x)" using `\<not> S1 \<le> S1 \<triangle> S2`
   7.355 +    by(force simp: less_eq_st_def narrow_st_def intro: n_narrow)
   7.356    have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
   7.357      apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   7.358    moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
   7.359 @@ -504,12 +499,12 @@
   7.360  definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
   7.361  "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
   7.362  
   7.363 -lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
   7.364 -by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
   7.365 +lemma n_o_mono: "S1 \<le> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
   7.366 +by(induction S1 S2 rule: less_eq_option.induct)(auto simp: n_o_def n_s_mono)
   7.367  
   7.368  lemma n_o_narrow:
   7.369    "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
   7.370 -  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
   7.371 +  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> \<not> S1 \<le> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
   7.372  apply(induction S1 S2 rule: narrow_option.induct)
   7.373  apply(auto simp: n_o_def L_st_def n_s_narrow)
   7.374  done
   7.375 @@ -519,7 +514,7 @@
   7.376  "n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
   7.377  
   7.378  lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
   7.379 -  C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
   7.380 +  C2 \<le> C1 \<Longrightarrow> \<not> C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
   7.381  apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
   7.382  apply(subgoal_tac "length(annos C2) = length(annos C1)")
   7.383  prefer 2 apply (simp add: size_annos_same2)
   7.384 @@ -544,13 +539,13 @@
   7.385  fixes m :: "'a::WN_Lc \<Rightarrow> nat"
   7.386  assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   7.387  and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
   7.388 -and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   7.389 +and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   7.390  and "P C" shows "EX C'. iter_widen f C = Some C'"
   7.391  proof(simp add: iter_widen_def,
   7.392        rule measure_while_option_Some[where P = P and f=m])
   7.393    show "P C" by(rule `P C`)
   7.394  next
   7.395 -  fix C assume "P C" "\<not> f C \<sqsubseteq> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
   7.396 +  fix C assume "P C" "\<not> f C \<le> C" thus "P (C \<nabla> f C) \<and> m (C \<nabla> f C) < m C"
   7.397      by(simp add: P_f P_widen m_widen)
   7.398  qed
   7.399  
   7.400 @@ -558,19 +553,19 @@
   7.401  fixes n :: "'a::WN_Lc \<Rightarrow> nat"
   7.402  assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   7.403  and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
   7.404 -and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
   7.405 -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"
   7.406 -and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
   7.407 +and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
   7.408 +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"
   7.409 +and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
   7.410  proof(simp add: iter_narrow_def,
   7.411 -      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<sqsubseteq> C"])
   7.412 -  show "P C \<and> f C \<sqsubseteq> C" using init by blast
   7.413 +      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
   7.414 +  show "P C \<and> f C \<le> C" using init by blast
   7.415  next
   7.416 -  fix C assume 1: "P C \<and> f C \<sqsubseteq> C" and 2: "\<not> C \<sqsubseteq> C \<triangle> f C"
   7.417 +  fix C assume 1: "P C \<and> f C \<le> C" and 2: "\<not> C \<le> C \<triangle> f C"
   7.418    hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
   7.419 -  moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
   7.420 -    by (metis narrow1 narrow2 1 mono preord_class.le_trans)
   7.421 +  moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
   7.422 +    by (metis narrow1 narrow2 1 mono order_trans)
   7.423    moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
   7.424 -  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"
   7.425 +  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"
   7.426      by blast
   7.427  qed
   7.428  
   7.429 @@ -581,39 +576,51 @@
   7.430  
   7.431  subsubsection "Termination: Intervals"
   7.432  
   7.433 -definition m_ivl :: "ivl \<Rightarrow> nat" where
   7.434 -"m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
   7.435 -     (case l of Minf \<Rightarrow> 0 | Lb _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | Ub _ \<Rightarrow> 1))"
   7.436 +definition m_rep :: "eint2 \<Rightarrow> nat" where
   7.437 +"m_rep p = (if is_empty_rep p then 3 else
   7.438 +  let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
   7.439 +
   7.440 +lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
   7.441 +by(auto simp: m_rep_def eq_ivl_iff)
   7.442  
   7.443 -lemma m_ivl_height: "m_ivl ivl \<le> 2"
   7.444 -by(simp add: m_ivl_def split: ivl.split lub_splits)
   7.445 +lemma m_ivl_nice: "m_ivl[l\<dots>h] = (if [l\<dots>h] = \<bottom> then 3 else
   7.446 +   (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
   7.447 +unfolding bot_ivl_def
   7.448 +by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
   7.449  
   7.450 -lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   7.451 -by(auto simp: m_ivl_def le_lub_defs le_ivl_def
   7.452 -        split: ivl.split lub_splits if_splits)
   7.453 +lemma m_ivl_height: "m_ivl iv \<le> 3"
   7.454 +by transfer (simp add: m_rep_def split: prod.split extended.split)
   7.455 +
   7.456 +lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   7.457 +by transfer
   7.458 +   (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   7.459 +         split: prod.split extended.splits if_splits)
   7.460  
   7.461  lemma m_ivl_widen:
   7.462 -  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   7.463 -by(auto simp: m_ivl_def widen_ivl_def le_lub_defs le_ivl_def
   7.464 -        split: ivl.splits lub_splits if_splits)
   7.465 +  "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   7.466 +by transfer
   7.467 +   (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   7.468 +         split: prod.split extended.splits if_splits)
   7.469  
   7.470  definition n_ivl :: "ivl \<Rightarrow> nat" where
   7.471 -"n_ivl ivl = 2 - m_ivl ivl"
   7.472 +"n_ivl ivl = 3 - m_ivl ivl"
   7.473  
   7.474 -lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
   7.475 +lemma n_ivl_mono: "x \<le> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
   7.476  unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
   7.477  
   7.478  lemma n_ivl_narrow:
   7.479 -  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   7.480 -by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_lub_defs le_ivl_def
   7.481 -        split: ivl.splits lub_splits if_splits)
   7.482 +  "~ x \<le> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   7.483 +unfolding n_ivl_def
   7.484 +by transfer
   7.485 +   (auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
   7.486 +         split: prod.splits if_splits extended.splits)
   7.487  
   7.488  
   7.489  interpretation Abs_Int2_measure
   7.490  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   7.491  and test_num' = in_ivl
   7.492  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   7.493 -and m = m_ivl and n = n_ivl and h = 2
   7.494 +and m = m_ivl and n = n_ivl and h = 3
   7.495  proof
   7.496    case goal1 thus ?case by(rule m_ivl_anti_mono)
   7.497  next
   7.498 @@ -629,14 +636,14 @@
   7.499  
   7.500  
   7.501  lemma iter_winden_step_ivl_termination:
   7.502 -  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
   7.503 +  "\<exists>C. iter_widen (step_ivl (Top(vars c))) (bot c) = Some C"
   7.504  apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
   7.505  apply (simp_all add: step'_in_Lc m_c_widen)
   7.506  done
   7.507  
   7.508  lemma iter_narrow_step_ivl_termination:
   7.509 -  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
   7.510 -  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
   7.511 +  "C0 \<in> Lc c \<Longrightarrow> step_ivl (Top(vars c)) C0 \<le> C0 \<Longrightarrow>
   7.512 +  \<exists>C. iter_narrow (step_ivl (Top(vars c))) C0 = Some C"
   7.513  apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
   7.514  apply (simp add: step'_in_Lc)
   7.515  apply (simp)
   7.516 @@ -662,12 +669,11 @@
   7.517  
   7.518  subsubsection "Counterexamples"
   7.519  
   7.520 -text{* Widening is increasing by assumption,
   7.521 -but @{prop"x \<sqsubseteq> f x"} is not an invariant of widening. It can already
   7.522 -be lost after the first step: *}
   7.523 +text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
   7.524 +It can already be lost after the first step: *}
   7.525  
   7.526 -lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   7.527 -and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" shows "x \<nabla> f x \<sqsubseteq> f(x \<nabla> f x)"
   7.528 +lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
   7.529 +and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
   7.530  nitpick[card = 3, expect = genuine, show_consts]
   7.531  (*
   7.532  1 < 2 < 3,
   7.533 @@ -682,9 +688,9 @@
   7.534  text{* Widening terminates but may converge more slowly than Kleene iteration.
   7.535  In the following model, Kleene iteration goes from 0 to the least pfp
   7.536  in one step but widening takes 2 steps to reach a strictly larger pfp: *}
   7.537 -lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   7.538 -and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" and "f(f x) \<sqsubseteq> f x"
   7.539 -shows "f(x \<nabla> f x) \<sqsubseteq> x \<nabla> f x"
   7.540 +lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
   7.541 +and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
   7.542 +shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
   7.543  nitpick[card = 4, expect = genuine, show_consts]
   7.544  (*
   7.545  
     8.1 --- a/src/HOL/IMP/Abs_State.thy	Wed Mar 06 14:10:07 2013 +0100
     8.2 +++ b/src/HOL/IMP/Abs_State.thy	Wed Mar 06 16:10:56 2013 +0100
     8.3 @@ -60,21 +60,21 @@
     8.4  end
     8.5  
     8.6  class semilatticeL = join + L +
     8.7 -fixes top :: "vname set \<Rightarrow> 'a"
     8.8 -assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<sqsubseteq> x \<squnion> y"
     8.9 -and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<sqsubseteq> x \<squnion> y"
    8.10 -and join_least[simp]: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    8.11 -and top[simp]: "x \<in> L X \<Longrightarrow> x \<sqsubseteq> top X"
    8.12 -and top_in_L[simp]: "top X \<in> L X"
    8.13 +fixes Top :: "vname set \<Rightarrow> 'a"
    8.14 +assumes join_ge1 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<le> x \<squnion> y"
    8.15 +and join_ge2 [simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> y \<le> x \<squnion> y"
    8.16 +and join_least[simp]: "x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<squnion> y \<le> z"
    8.17 +and Top[simp]: "x \<in> L X \<Longrightarrow> x \<le> Top X"
    8.18 +and Top_in_L[simp]: "Top X \<in> L X"
    8.19  and join_in_L[simp]: "x \<in> L X \<Longrightarrow> y \<in> L X \<Longrightarrow> x \<squnion> y \<in> L X"
    8.20  
    8.21 -notation (input) top ("\<top>\<^bsub>_\<^esub>")
    8.22 -notation (latex output) top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
    8.23 +notation (input) Top ("\<top>\<^bsub>_\<^esub>")
    8.24 +notation (latex output) Top ("\<top>\<^bsub>\<^raw:\isa{>_\<^raw:}>\<^esub>")
    8.25  
    8.26  instantiation option :: (semilatticeL)semilatticeL
    8.27  begin
    8.28  
    8.29 -definition top_option where "top c = Some(top c)"
    8.30 +definition Top_option where "Top c = Some(Top c)"
    8.31  
    8.32  instance proof
    8.33    case goal1 thus ?case by(cases x, simp, cases y, simp_all)
    8.34 @@ -83,9 +83,9 @@
    8.35  next
    8.36    case goal3 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
    8.37  next
    8.38 -  case goal4 thus ?case by(cases x, simp_all add: top_option_def)
    8.39 +  case goal4 thus ?case by(cases x, simp_all add: Top_option_def)
    8.40  next
    8.41 -  case goal5 thus ?case by(simp add: top_option_def)
    8.42 +  case goal5 thus ?case by(simp add: Top_option_def)
    8.43  next
    8.44    case goal6 thus ?case by(simp add: L_option_def split: option.splits)
    8.45  qed
    8.46 @@ -97,41 +97,77 @@
    8.47  
    8.48  hide_type  st  --"to avoid long names"
    8.49  
    8.50 -text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    8.51 +text{* A concrete type of state with computable @{text"\<le>"}: *}
    8.52 +
    8.53 +fun st :: "(vname \<Rightarrow> 'a) * vname set \<Rightarrow> bool" where
    8.54 +"st (f,X) = (\<forall>x. x \<notin> X \<longrightarrow> f x = undefined)"
    8.55  
    8.56 -datatype 'a st = FunDom "vname \<Rightarrow> 'a" "vname set"
    8.57 +typedef 'a st = "{p :: (vname \<Rightarrow> 'a) * vname set. st p}"
    8.58 +proof
    8.59 +  show "(\<lambda>x. undefined,{}) \<in> {p. st p}" by simp
    8.60 +qed
    8.61 +
    8.62 +setup_lifting type_definition_st
    8.63 +
    8.64 +lift_definition St :: "(vname \<Rightarrow> 'a) \<Rightarrow> vname set \<Rightarrow> 'a st" is
    8.65 +  "\<lambda>f X. (\<lambda>x. if x \<in> X then f x else undefined, X)"
    8.66 +by(simp)
    8.67  
    8.68 -fun "fun" where "fun (FunDom f X) = f"
    8.69 -fun dom where "dom (FunDom f X) = X"
    8.70 +lift_definition update :: "'a st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st" is
    8.71 +  "\<lambda>(f,X) x a. (f(x := a), insert x X)"
    8.72 +by(auto)
    8.73 +
    8.74 +lift_definition "fun" :: "'a st \<Rightarrow> vname \<Rightarrow> 'a" is fst ..
    8.75 +
    8.76 +lift_definition dom :: "'a st \<Rightarrow> vname set" is snd ..
    8.77  
    8.78 -definition "show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
    8.79 +lemma dom_St[simp]: "dom(St f X) = X"
    8.80 +by(simp add: St.rep_eq dom.rep_eq)
    8.81  
    8.82 -value [code] "show_st (FunDom (\<lambda>x. 1::int) {''a'',''b''})"
    8.83 +lemma fun_St[simp]: "fun(St f X) = (\<lambda>x. if x \<in> X then f x else undefined)"
    8.84 +by(simp add: St.rep_eq fun.rep_eq)
    8.85 +
    8.86 +definition show_st :: "'a st \<Rightarrow> (vname * 'a)set" where
    8.87 +"show_st S = (\<lambda>x. (x, fun S x)) ` dom S"
    8.88  
    8.89  definition "show_acom = map_acom (Option.map show_st)"
    8.90  definition "show_acom_opt = Option.map show_acom"
    8.91  
    8.92 -definition "update F x y = FunDom ((fun F)(x:=y)) (dom F)"
    8.93 +lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    8.94 +by transfer auto
    8.95  
    8.96 -lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
    8.97 -by(rule ext)(auto simp: update_def)
    8.98 +lemma dom_update[simp]: "dom (update S x y) = insert x (dom S)"
    8.99 +by transfer auto
   8.100 +
   8.101 +definition \<gamma>_st :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
   8.102 +"\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom  F. f x \<in> \<gamma>(fun F x)}"
   8.103  
   8.104 -lemma dom_update[simp]: "dom (update S x y) = dom S"
   8.105 -by(simp add: update_def)
   8.106 +lemma ext_st: "dom F = dom G \<Longrightarrow> \<forall>x \<in> dom G. fun F x = fun G x \<Longrightarrow> F=G"
   8.107 +apply(induct F rule:Abs_st_induct)
   8.108 +apply(induct G rule:Abs_st_induct)
   8.109 +apply (auto simp:Abs_st_inject fun_def dom_def Abs_st_inverse simp del: st.simps)
   8.110 +apply(rule ext)
   8.111 +apply auto
   8.112 +done
   8.113  
   8.114 -definition "\<gamma>_st \<gamma> F = {f. \<forall>x\<in>dom F. f x \<in> \<gamma>(fun F x)}"
   8.115 -
   8.116 -
   8.117 -instantiation st :: (preord) preord
   8.118 +instantiation st :: (order) order
   8.119  begin
   8.120  
   8.121 -definition le_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
   8.122 -"F \<sqsubseteq> G = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<sqsubseteq> fun G x))"
   8.123 +definition less_eq_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> bool" where
   8.124 +"F \<le> (G::'a st) = (dom F = dom G \<and> (\<forall>x \<in> dom F. fun F x \<le> fun G x))"
   8.125 +
   8.126 +definition less_st where "F < (G::'a st) = (F \<le> G \<and> \<not> G \<le> F)"
   8.127  
   8.128  instance
   8.129  proof
   8.130 -  case goal2 thus ?case by(auto simp: le_st_def)(metis preord_class.le_trans)
   8.131 -qed (auto simp: le_st_def)
   8.132 +  case goal1 show ?case by(rule less_st_def)
   8.133 +next
   8.134 +  case goal2 show ?case by(auto simp: less_eq_st_def)
   8.135 +next
   8.136 +  case goal3 thus ?case by(fastforce simp: less_eq_st_def)
   8.137 +next
   8.138 +  case goal4 thus ?case by (metis less_eq_st_def antisym ext_st)
   8.139 +qed
   8.140  
   8.141  end
   8.142  
   8.143 @@ -139,7 +175,7 @@
   8.144  begin
   8.145  
   8.146  definition join_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" where
   8.147 -"F \<squnion> G = FunDom (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
   8.148 +"F \<squnion> (G::'a st) = St (\<lambda>x. fun F x \<squnion> fun G x) (dom F)"
   8.149  
   8.150  instance ..
   8.151  
   8.152 @@ -149,7 +185,7 @@
   8.153  begin
   8.154  
   8.155  definition L_st :: "vname set \<Rightarrow> 'a st set" where
   8.156 -"L X = {F. dom F = X}"
   8.157 +"L(X::vname set) = {F. dom F = X}"
   8.158  
   8.159  instance ..
   8.160  
   8.161 @@ -158,11 +194,10 @@
   8.162  instantiation st :: (semilattice) semilatticeL
   8.163  begin
   8.164  
   8.165 -definition top_st where "top X = FunDom (\<lambda>x. \<top>) X"
   8.166 +definition Top_st :: "vname set \<Rightarrow> 'a st" where "Top(X) = St (\<lambda>x. \<top>) X"
   8.167  
   8.168  instance
   8.169 -proof
   8.170 -qed (auto simp: le_st_def join_st_def top_st_def L_st_def)
   8.171 +proof qed(auto simp add: less_eq_st_def join_st_def Top_st_def L_st_def)
   8.172  
   8.173  end
   8.174  
   8.175 @@ -175,12 +210,12 @@
   8.176     But L is not executable. This looping defn makes it look as if it were. *)
   8.177  
   8.178  
   8.179 -lemma mono_fun: "F \<sqsubseteq> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<sqsubseteq> fun G x"
   8.180 -by(auto simp: le_st_def)
   8.181 +lemma mono_fun: "F \<le> G \<Longrightarrow> x : dom F \<Longrightarrow> fun F x \<le> fun G x"
   8.182 +by(auto simp: less_eq_st_def)
   8.183  
   8.184  lemma mono_update[simp]:
   8.185 -  "a1 \<sqsubseteq> a2 \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow> update S1 x a1 \<sqsubseteq> update S2 x a2"
   8.186 -by(auto simp add: le_st_def update_def)
   8.187 +  "a1 \<le> a2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> update S1 x a1 \<le> update S2 x a2"
   8.188 +by(auto simp add: less_eq_st_def)
   8.189  
   8.190  
   8.191  locale Gamma = Val_abs where \<gamma>=\<gamma> for \<gamma> :: "'av::semilattice \<Rightarrow> val set"
   8.192 @@ -195,22 +230,22 @@
   8.193  abbreviation \<gamma>\<^isub>c :: "'av st option acom \<Rightarrow> state set acom"
   8.194  where "\<gamma>\<^isub>c == map_acom \<gamma>\<^isub>o"
   8.195  
   8.196 -lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (top c) = UNIV"
   8.197 -by(auto simp: top_st_def \<gamma>_st_def)
   8.198 +lemma gamma_s_Top[simp]: "\<gamma>\<^isub>s (Top X) = UNIV"
   8.199 +by(auto simp: Top_st_def \<gamma>_st_def)
   8.200  
   8.201 -lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (top c) = UNIV"
   8.202 -by (simp add: top_option_def)
   8.203 +lemma gamma_o_Top[simp]: "\<gamma>\<^isub>o (Top X) = UNIV"
   8.204 +by (simp add: Top_option_def)
   8.205  
   8.206 -lemma mono_gamma_s: "f \<sqsubseteq> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
   8.207 -apply(simp add:\<gamma>_st_def subset_iff le_st_def split: if_splits)
   8.208 +lemma mono_gamma_s: "f \<le> g \<Longrightarrow> \<gamma>\<^isub>s f \<subseteq> \<gamma>\<^isub>s g"
   8.209 +apply(simp add:\<gamma>_st_def subset_iff less_eq_st_def split: if_splits)
   8.210  by (metis mono_gamma subsetD)
   8.211  
   8.212  lemma mono_gamma_o:
   8.213 -  "S1 \<sqsubseteq> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   8.214 -by(induction S1 S2 rule: le_option.induct)(simp_all add: mono_gamma_s)
   8.215 +  "S1 \<le> S2 \<Longrightarrow> \<gamma>\<^isub>o S1 \<subseteq> \<gamma>\<^isub>o S2"
   8.216 +by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)
   8.217  
   8.218 -lemma mono_gamma_c: "C1 \<sqsubseteq> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   8.219 -by (induction C1 C2 rule: le_acom.induct) (simp_all add:mono_gamma_o)
   8.220 +lemma mono_gamma_c: "C1 \<le> C2 \<Longrightarrow> \<gamma>\<^isub>c C1 \<le> \<gamma>\<^isub>c C2"
   8.221 +by (induction C1 C2 rule: less_eq_acom.induct) (simp_all add:mono_gamma_o)
   8.222  
   8.223  lemma in_gamma_option_iff:
   8.224    "x : \<gamma>_option r u \<longleftrightarrow> (\<exists>u'. u = Some u' \<and> x : r u')"