src/HOL/IMP/Abs_Int3.thy
changeset 51359 00b45c7e831f
parent 51245 311fe56541ea
child 51372 d315e9a9ee72
     1.1 --- a/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 14:10:07 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int3.thy	Wed Mar 06 16:10:56 2013 +0100
     1.3 @@ -65,17 +65,17 @@
     1.4  class narrow =
     1.5  fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
     1.6  
     1.7 -class WN = widen + narrow + preord +
     1.8 -assumes widen1: "x \<sqsubseteq> x \<nabla> y"
     1.9 -assumes widen2: "y \<sqsubseteq> x \<nabla> y"
    1.10 -assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    1.11 -assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    1.12 +class WN = widen + narrow + order +
    1.13 +assumes widen1: "x \<le> x \<nabla> y"
    1.14 +assumes widen2: "y \<le> x \<nabla> y"
    1.15 +assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
    1.16 +assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
    1.17  
    1.18 -class WN_Lc = widen + narrow + preord + Lc +
    1.19 -assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<sqsubseteq> x \<nabla> y"
    1.20 -assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<sqsubseteq> x \<nabla> y"
    1.21 -assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
    1.22 -assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
    1.23 +class WN_Lc = widen + narrow + order + Lc +
    1.24 +assumes widen1: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<le> x \<nabla> y"
    1.25 +assumes widen2: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> y \<le> x \<nabla> y"
    1.26 +assumes narrow1: "y \<le> x \<Longrightarrow> y \<le> x \<triangle> y"
    1.27 +assumes narrow2: "y \<le> x \<Longrightarrow> x \<triangle> y \<le> x"
    1.28  assumes Lc_widen[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<nabla> y \<in> Lc c"
    1.29  assumes Lc_narrow[simp]: "x \<in> Lc c \<Longrightarrow> y \<in> Lc c \<Longrightarrow> x \<triangle> y \<in> Lc c"
    1.30  
    1.31 @@ -83,22 +83,25 @@
    1.32  instantiation ivl :: WN
    1.33  begin
    1.34  
    1.35 -definition "widen_ivl ivl1 ivl2 =
    1.36 -  ((*if is_empty ivl1 then ivl2 else
    1.37 -   if is_empty ivl2 then ivl1 else*)
    1.38 -     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    1.39 -       Ivl (if l2 \<le> l1 \<and> l2 \<noteq> l1 then Minf else l1)
    1.40 -           (if h1 \<le> h2 \<and> h1 \<noteq> h2 then Pinf else h1))"
    1.41 +definition "widen_rep p1 p2 =
    1.42 +  (if is_empty_rep p1 then p2 else if is_empty_rep p2 then p1 else
    1.43 +   let (l1,h1) = p1; (l2,h2) = p2
    1.44 +   in (if l2 < l1 then Minf else l1, if h1 < h2 then Pinf else h1))"
    1.45 +
    1.46 +lift_definition widen_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is widen_rep
    1.47 +by(auto simp: widen_rep_def eq_ivl_iff)
    1.48  
    1.49 -definition "narrow_ivl ivl1 ivl2 =
    1.50 -  ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
    1.51 -     case (ivl1,ivl2) of (Ivl l1 h1, Ivl l2 h2) \<Rightarrow>
    1.52 -       Ivl (if l1 = Minf then l2 else l1)
    1.53 -           (if h1 = Pinf then h2 else h1))"
    1.54 +definition "narrow_rep p1 p2 =
    1.55 +  (if is_empty_rep p1 \<or> is_empty_rep p2 then empty_rep else
    1.56 +   let (l1,h1) = p1; (l2,h2) = p2
    1.57 +   in (if l1 = Minf then l2 else l1, if h1 = Pinf then h2 else h1))"
    1.58 +
    1.59 +lift_definition narrow_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> ivl" is narrow_rep
    1.60 +by(auto simp: narrow_rep_def eq_ivl_iff)
    1.61  
    1.62  instance
    1.63 -proof qed
    1.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)
    1.65 +proof
    1.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)+
    1.67  
    1.68  end
    1.69  
    1.70 @@ -106,23 +109,20 @@
    1.71  instantiation st :: (WN)WN_Lc
    1.72  begin
    1.73  
    1.74 -definition "widen_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
    1.75 +definition "widen_st F1 F2 = St (\<lambda>x. fun F1 x \<nabla> fun F2 x) (dom F1)"
    1.76  
    1.77 -definition "narrow_st F1 F2 = FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
    1.78 +definition "narrow_st F1 F2 = St (\<lambda>x. fun F1 x \<triangle> fun F2 x) (dom F1)"
    1.79  
    1.80  instance
    1.81  proof
    1.82 -  case goal1 thus ?case
    1.83 -    by(simp add: widen_st_def le_st_def WN_class.widen1)
    1.84 +  case goal1 thus ?case by(simp add: widen_st_def less_eq_st_def WN_class.widen1)
    1.85  next
    1.86    case goal2 thus ?case
    1.87 -    by(simp add: widen_st_def le_st_def WN_class.widen2 Lc_st_def L_st_def)
    1.88 +    by(simp add: widen_st_def less_eq_st_def WN_class.widen2 Lc_st_def L_st_def)
    1.89  next
    1.90 -  case goal3 thus ?case
    1.91 -    by(auto simp: narrow_st_def le_st_def WN_class.narrow1)
    1.92 +  case goal3 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow1)
    1.93  next
    1.94 -  case goal4 thus ?case
    1.95 -    by(auto simp: narrow_st_def le_st_def WN_class.narrow2)
    1.96 +  case goal4 thus ?case by(auto simp: narrow_st_def less_eq_st_def WN_class.narrow2)
    1.97  next
    1.98    case goal5 thus ?case by(auto simp: widen_st_def Lc_st_def L_st_def)
    1.99  next
   1.100 @@ -196,14 +196,14 @@
   1.101  
   1.102  lemma widen_acom1: fixes C1 :: "'a acom" shows
   1.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>
   1.104 -   \<Longrightarrow> C1 \<sqsubseteq> C1 \<nabla> C2"
   1.105 -by(induct C1 C2 rule: le_acom.induct)
   1.106 +   \<Longrightarrow> C1 \<le> C1 \<nabla> C2"
   1.107 +by(induct C1 C2 rule: less_eq_acom.induct)
   1.108    (auto simp: widen_acom_def widen1 Lc_acom_def)
   1.109  
   1.110  lemma widen_acom2: fixes C1 :: "'a acom" shows
   1.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>
   1.112 -   \<Longrightarrow> C2 \<sqsubseteq> C1 \<nabla> C2"
   1.113 -by(induct C1 C2 rule: le_acom.induct)
   1.114 +   \<Longrightarrow> C2 \<le> C1 \<nabla> C2"
   1.115 +by(induct C1 C2 rule: less_eq_acom.induct)
   1.116    (auto simp: widen_acom_def widen2 Lc_acom_def)
   1.117  
   1.118  lemma strip_map2_acom[simp]:
   1.119 @@ -229,10 +229,10 @@
   1.120    case goal2 thus ?case by(auto simp: Lc_acom_def widen_acom2)
   1.121  next
   1.122    case goal3 thus ?case
   1.123 -    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow1)
   1.124 +    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow1)
   1.125  next
   1.126    case goal4 thus ?case
   1.127 -    by(induct x y rule: le_acom.induct)(simp_all add: narrow_acom_def narrow2)
   1.128 +    by(induct x y rule: less_eq_acom.induct)(simp_all add: narrow_acom_def narrow2)
   1.129  next
   1.130    case goal5 thus ?case
   1.131      by(auto simp: Lc_acom_def widen_acom_def split_conv elim!: in_set_zipE)
   1.132 @@ -255,12 +255,12 @@
   1.133  
   1.134  lemma widen_c_in_L: fixes C1 C2 :: "_ st option acom"
   1.135  shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<nabla> C2 \<in> L X"
   1.136 -by(induction C1 C2 rule: le_acom.induct)
   1.137 +by(induction C1 C2 rule: less_eq_acom.induct)
   1.138    (auto simp: widen_acom_def)
   1.139  
   1.140  lemma narrow_c_in_L: fixes C1 C2 :: "_ st option acom"
   1.141  shows "strip C1 = strip C2 \<Longrightarrow> C1 \<in> L X \<Longrightarrow> C2 \<in> L X \<Longrightarrow> C1 \<triangle> C2 \<in> L X"
   1.142 -by(induction C1 C2 rule: le_acom.induct)
   1.143 +by(induction C1 C2 rule: less_eq_acom.induct)
   1.144    (auto simp: narrow_acom_def)
   1.145  
   1.146  lemma bot_in_Lc[simp]: "bot c \<in> Lc c"
   1.147 @@ -269,18 +269,18 @@
   1.148  
   1.149  subsubsection "Post-fixed point computation"
   1.150  
   1.151 -definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,widen})option"
   1.152 -where "iter_widen f = while_option (\<lambda>x. \<not> f x \<sqsubseteq> x) (\<lambda>x. x \<nabla> f x)"
   1.153 +definition iter_widen :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,widen})option"
   1.154 +where "iter_widen f = while_option (\<lambda>x. \<not> f x \<le> x) (\<lambda>x. x \<nabla> f x)"
   1.155  
   1.156 -definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{preord,narrow})option"
   1.157 -where "iter_narrow f = while_option (\<lambda>x. \<not> x \<sqsubseteq> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
   1.158 +definition iter_narrow :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> ('a::{order,narrow})option"
   1.159 +where "iter_narrow f = while_option (\<lambda>x. \<not> x \<le> x \<triangle> f x) (\<lambda>x. x \<triangle> f x)"
   1.160  
   1.161 -definition pfp_wn :: "('a::{preord,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   1.162 +definition pfp_wn :: "('a::{order,widen,narrow} \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a option"
   1.163  where "pfp_wn f x =
   1.164    (case iter_widen f x of None \<Rightarrow> None | Some p \<Rightarrow> iter_narrow f p)"
   1.165  
   1.166  
   1.167 -lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<sqsubseteq> p"
   1.168 +lemma iter_widen_pfp: "iter_widen f x = Some p \<Longrightarrow> f p \<le> p"
   1.169  by(auto simp add: iter_widen_def dest: while_option_stop)
   1.170  
   1.171  lemma iter_widen_inv:
   1.172 @@ -295,7 +295,7 @@
   1.173  using while_option_rule[where P = "\<lambda>C'. strip C' = strip C", OF _ assms(2)]
   1.174  by (metis assms(1))
   1.175  
   1.176 -lemma strip_iter_widen: fixes f :: "'a::{preord,widen} acom \<Rightarrow> 'a acom"
   1.177 +lemma strip_iter_widen: fixes f :: "'a::{order,widen} acom \<Rightarrow> 'a acom"
   1.178  assumes "\<forall>C. strip (f C) = strip C" and "iter_widen f C = Some C'"
   1.179  shows "strip C' = strip C"
   1.180  proof-
   1.181 @@ -305,12 +305,12 @@
   1.182  qed
   1.183  
   1.184  lemma iter_narrow_pfp:
   1.185 -assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   1.186 +assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   1.187  and Pinv: "!!x. P x \<Longrightarrow> P(f x)" "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   1.188 -and "P p0" and "f p0 \<sqsubseteq> p0" and "iter_narrow f p0 = Some p"
   1.189 -shows "P p \<and> f p \<sqsubseteq> p"
   1.190 +and "P p0" and "f p0 \<le> p0" and "iter_narrow f p0 = Some p"
   1.191 +shows "P p \<and> f p \<le> p"
   1.192  proof-
   1.193 -  let ?Q = "%p. P p \<and> f p \<sqsubseteq> p \<and> p \<sqsubseteq> p0"
   1.194 +  let ?Q = "%p. P p \<and> f p \<le> p \<and> p \<le> p0"
   1.195    { fix p assume "?Q p"
   1.196      note P = conjunct1[OF this] and 12 = conjunct2[OF this]
   1.197      note 1 = conjunct1[OF 12] and 2 = conjunct2[OF 12]
   1.198 @@ -318,12 +318,12 @@
   1.199      have "?Q ?p'"
   1.200      proof auto
   1.201        show "P ?p'" by (blast intro: P Pinv)
   1.202 -      have "f ?p' \<sqsubseteq> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
   1.203 -      also have "\<dots> \<sqsubseteq> ?p'" by(rule narrow1[OF 1])
   1.204 -      finally show "f ?p' \<sqsubseteq> ?p'" .
   1.205 -      have "?p' \<sqsubseteq> p" by (rule narrow2[OF 1])
   1.206 -      also have "p \<sqsubseteq> p0" by(rule 2)
   1.207 -      finally show "?p' \<sqsubseteq> p0" .
   1.208 +      have "f ?p' \<le> f p" by(rule mono[OF `P (p \<triangle> f p)`  P narrow2[OF 1]])
   1.209 +      also have "\<dots> \<le> ?p'" by(rule narrow1[OF 1])
   1.210 +      finally show "f ?p' \<le> ?p'" .
   1.211 +      have "?p' \<le> p" by (rule narrow2[OF 1])
   1.212 +      also have "p \<le> p0" by(rule 2)
   1.213 +      finally show "?p' \<le> p0" .
   1.214      qed
   1.215    }
   1.216    thus ?thesis
   1.217 @@ -332,11 +332,11 @@
   1.218  qed
   1.219  
   1.220  lemma pfp_wn_pfp:
   1.221 -assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<sqsubseteq> x2 \<Longrightarrow> f x1 \<sqsubseteq> f x2"
   1.222 +assumes mono: "!!x1 x2::_::WN_Lc. P x1 \<Longrightarrow> P x2 \<Longrightarrow> x1 \<le> x2 \<Longrightarrow> f x1 \<le> f x2"
   1.223  and Pinv: "P x"  "!!x. P x \<Longrightarrow> P(f x)"
   1.224    "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<nabla> x2)"
   1.225    "!!x1 x2. P x1 \<Longrightarrow> P x2 \<Longrightarrow> P(x1 \<triangle> x2)"
   1.226 -and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<sqsubseteq> p"
   1.227 +and pfp_wn: "pfp_wn f x = Some p" shows "P p \<and> f p \<le> p"
   1.228  proof-
   1.229    from pfp_wn obtain p0
   1.230      where its: "iter_widen f x = Some p0" "iter_narrow f p0 = Some p"
   1.231 @@ -358,24 +358,24 @@
   1.232  begin
   1.233  
   1.234  definition AI_wn :: "com \<Rightarrow> 'av st option acom option" where
   1.235 -"AI_wn c = pfp_wn (step' (top(vars c))) (bot c)"
   1.236 +"AI_wn c = pfp_wn (step' (Top(vars c))) (bot c)"
   1.237  
   1.238  lemma AI_wn_sound: "AI_wn c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^isub>c C"
   1.239  proof(simp add: CS_def AI_wn_def)
   1.240 -  assume 1: "pfp_wn (step' (top(vars c))) (bot c) = Some C"
   1.241 -  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<sqsubseteq> C"
   1.242 +  assume 1: "pfp_wn (step' (Top(vars c))) (bot c) = Some C"
   1.243 +  have 2: "(strip C = c & C \<in> L(vars c)) \<and> step' \<top>\<^bsub>vars c\<^esub> C \<le> C"
   1.244      by(rule pfp_wn_pfp[where x="bot c"])
   1.245        (simp_all add: 1 mono_step'_top widen_c_in_L narrow_c_in_L)
   1.246 -  have pfp: "step (\<gamma>\<^isub>o(top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   1.247 +  have pfp: "step (\<gamma>\<^isub>o(Top(vars c))) (\<gamma>\<^isub>c C) \<le> \<gamma>\<^isub>c C"
   1.248    proof(rule order_trans)
   1.249 -    show "step (\<gamma>\<^isub>o (top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (top(vars c)) C)"
   1.250 -      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] top_in_L])
   1.251 +    show "step (\<gamma>\<^isub>o (Top(vars c))) (\<gamma>\<^isub>c C) \<le>  \<gamma>\<^isub>c (step' (Top(vars c)) C)"
   1.252 +      by(rule step_step'[OF conjunct2[OF conjunct1[OF 2]] Top_in_L])
   1.253      show "... \<le> \<gamma>\<^isub>c C"
   1.254        by(rule mono_gamma_c[OF conjunct2[OF 2]])
   1.255    qed
   1.256    have 3: "strip (\<gamma>\<^isub>c C) = c" by(simp add: strip_pfp_wn[OF _ 1])
   1.257 -  have "lfp c (step (\<gamma>\<^isub>o (top(vars c)))) \<le> \<gamma>\<^isub>c C"
   1.258 -    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(top(vars c)))", OF 3 pfp])
   1.259 +  have "lfp c (step (\<gamma>\<^isub>o (Top(vars c)))) \<le> \<gamma>\<^isub>c C"
   1.260 +    by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^isub>o(Top(vars c)))", OF 3 pfp])
   1.261    thus "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C" by simp
   1.262  qed
   1.263  
   1.264 @@ -391,14 +391,10 @@
   1.265  
   1.266  subsubsection "Tests"
   1.267  
   1.268 -(* Trick to make the code generator happy. *)
   1.269 -lemma [code]: "equal_class.equal (x::'a st) y = equal_class.equal x y"
   1.270 -by(rule refl)
   1.271 -
   1.272  definition "step_up_ivl n =
   1.273 -  ((\<lambda>C. C \<nabla> step_ivl (top(vars(strip C))) C)^^n)"
   1.274 +  ((\<lambda>C. C \<nabla> step_ivl (Top(vars(strip C))) C)^^n)"
   1.275  definition "step_down_ivl n =
   1.276 -  ((\<lambda>C. C \<triangle> step_ivl (top(vars(strip C))) C)^^n)"
   1.277 +  ((\<lambda>C. C \<triangle> step_ivl (Top(vars(strip C))) C)^^n)"
   1.278  
   1.279  text{* For @{const test3_ivl}, @{const AI_ivl} needed as many iterations as
   1.280  the loop took to execute. In contrast, @{const AI_ivl'} converges in a
   1.281 @@ -430,32 +426,31 @@
   1.282  
   1.283  locale Measure_WN = Measure1 where m=m for m :: "'av::WN \<Rightarrow> nat" +
   1.284  fixes n :: "'av \<Rightarrow> nat"
   1.285 -assumes m_widen: "~ y \<sqsubseteq> x \<Longrightarrow> m(x \<nabla> y) < m x"
   1.286 -assumes n_mono: "x \<sqsubseteq> y \<Longrightarrow> n x \<le> n y"
   1.287 -assumes n_narrow: "y \<sqsubseteq> x \<Longrightarrow> ~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
   1.288 +assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
   1.289 +assumes n_mono: "x \<le> y \<Longrightarrow> n x \<le> n y"
   1.290 +assumes n_narrow: "y \<le> x \<Longrightarrow> ~ x \<le> x \<triangle> y \<Longrightarrow> n(x \<triangle> y) < n x"
   1.291  
   1.292  begin
   1.293  
   1.294  lemma m_s_widen: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
   1.295 -  ~ S2 \<sqsubseteq> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
   1.296 -proof(auto simp add: le_st_def m_s_def L_st_def widen_st_def)
   1.297 +  ~ S2 \<le> S1 \<Longrightarrow> m_s(S1 \<nabla> S2) < m_s S1"
   1.298 +proof(auto simp add: less_eq_st_def m_s_def L_st_def widen_st_def)
   1.299    assume "finite(dom S1)"
   1.300    have 1: "\<forall>x\<in>dom S1. m(fun S1 x) \<ge> m(fun S1 x \<nabla> fun S2 x)"
   1.301      by (metis m1 WN_class.widen1)
   1.302 -  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<sqsubseteq> fun S1 x"
   1.303 +  fix x assume "x \<in> dom S1" "\<not> fun S2 x \<le> fun S1 x"
   1.304    hence 2: "EX x : dom S1. m(fun S1 x) > m(fun S1 x \<nabla> fun S2 x)"
   1.305      using m_widen by blast
   1.306    from setsum_strict_mono_ex1[OF `finite(dom S1)` 1 2]
   1.307    show "(\<Sum>x\<in>dom S1. m (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>dom S1. m (fun S1 x))" .
   1.308  qed
   1.309  
   1.310 -lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
   1.311 +lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<le> S1 \<rbrakk> \<Longrightarrow>
   1.312    m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
   1.313 -by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen
   1.314 -        split: option.split)
   1.315 +by(auto simp: m_o_def L_st_def m_s_h less_Suc_eq_le m_s_widen split: option.split)
   1.316  
   1.317  lemma m_c_widen:
   1.318 -  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   1.319 +  "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
   1.320  apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
   1.321  apply(subgoal_tac "length(annos C2) = length(annos C1)")
   1.322  prefer 2 apply (simp add: size_annos_same2)
   1.323 @@ -475,25 +470,25 @@
   1.324  definition n_s :: "'av st \<Rightarrow> nat" ("n\<^isub>s") where
   1.325  "n\<^isub>s S = (\<Sum>x\<in>dom S. n(fun S x))"
   1.326  
   1.327 -lemma n_s_mono: assumes "S1 \<sqsubseteq> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
   1.328 +lemma n_s_mono: assumes "S1 \<le> S2" shows "n\<^isub>s S1 \<le> n\<^isub>s S2"
   1.329  proof-
   1.330 -  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<sqsubseteq> fun S2 x"
   1.331 -    by(simp_all add: le_st_def)
   1.332 +  from assms have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S1 x \<le> fun S2 x"
   1.333 +    by(simp_all add: less_eq_st_def)
   1.334    have "(\<Sum>x\<in>dom S1. n(fun S1 x)) \<le> (\<Sum>x\<in>dom S1. n(fun S2 x))"
   1.335 -    by(rule setsum_mono)(simp add: le_st_def n_mono)
   1.336 +    by(rule setsum_mono)(simp add: less_eq_st_def n_mono)
   1.337    thus ?thesis by(simp add: n_s_def)
   1.338  qed
   1.339  
   1.340  lemma n_s_narrow:
   1.341 -assumes "finite(dom S1)" and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
   1.342 +assumes "finite(dom S1)" and "S2 \<le> S1" "\<not> S1 \<le> S1 \<triangle> S2"
   1.343  shows "n\<^isub>s (S1 \<triangle> S2) < n\<^isub>s S1"
   1.344  proof-
   1.345 -  from `S2\<sqsubseteq>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<sqsubseteq> fun S1 x"
   1.346 -    by(simp_all add: le_st_def)
   1.347 +  from `S2\<le>S1` have [simp]: "dom S1 = dom S2" "\<forall>x\<in>dom S1. fun S2 x \<le> fun S1 x"
   1.348 +    by(simp_all add: less_eq_st_def)
   1.349    have 1: "\<forall>x\<in>dom S1. n(fun (S1 \<triangle> S2) x) \<le> n(fun S1 x)"
   1.350 -    by(auto simp: le_st_def narrow_st_def n_mono WN_class.narrow2)
   1.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`
   1.352 -    by(force simp: le_st_def narrow_st_def intro: n_narrow)
   1.353 +    by(auto simp: less_eq_st_def narrow_st_def n_mono WN_class.narrow2)
   1.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`
   1.355 +    by(force simp: less_eq_st_def narrow_st_def intro: n_narrow)
   1.356    have "(\<Sum>x\<in>dom S1. n(fun (S1 \<triangle> S2) x)) < (\<Sum>x\<in>dom S1. n(fun S1 x))"
   1.357      apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   1.358    moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
   1.359 @@ -504,12 +499,12 @@
   1.360  definition n_o :: "'av st option \<Rightarrow> nat" ("n\<^isub>o") where
   1.361  "n\<^isub>o opt = (case opt of None \<Rightarrow> 0 | Some S \<Rightarrow> n\<^isub>s S + 1)"
   1.362  
   1.363 -lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
   1.364 -by(induction S1 S2 rule: le_option.induct)(auto simp: n_o_def n_s_mono)
   1.365 +lemma n_o_mono: "S1 \<le> S2 \<Longrightarrow> n\<^isub>o S1 \<le> n\<^isub>o S2"
   1.366 +by(induction S1 S2 rule: less_eq_option.induct)(auto simp: n_o_def n_s_mono)
   1.367  
   1.368  lemma n_o_narrow:
   1.369    "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X
   1.370 -  \<Longrightarrow> S2 \<sqsubseteq> S1 \<Longrightarrow> \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
   1.371 +  \<Longrightarrow> S2 \<le> S1 \<Longrightarrow> \<not> S1 \<le> S1 \<triangle> S2 \<Longrightarrow> n\<^isub>o (S1 \<triangle> S2) < n\<^isub>o S1"
   1.372  apply(induction S1 S2 rule: narrow_option.induct)
   1.373  apply(auto simp: n_o_def L_st_def n_s_narrow)
   1.374  done
   1.375 @@ -519,7 +514,7 @@
   1.376  "n\<^isub>c C = (let as = annos C in \<Sum>i<size as. n\<^isub>o (as!i))"
   1.377  
   1.378  lemma n_c_narrow: "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow>
   1.379 -  C2 \<sqsubseteq> C1 \<Longrightarrow> \<not> C1 \<sqsubseteq> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
   1.380 +  C2 \<le> C1 \<Longrightarrow> \<not> C1 \<le> C1 \<triangle> C2 \<Longrightarrow> n\<^isub>c (C1 \<triangle> C2) < n\<^isub>c C1"
   1.381  apply(auto simp: n_c_def Let_def Lc_acom_def narrow_acom_def)
   1.382  apply(subgoal_tac "length(annos C2) = length(annos C1)")
   1.383  prefer 2 apply (simp add: size_annos_same2)
   1.384 @@ -544,13 +539,13 @@
   1.385  fixes m :: "'a::WN_Lc \<Rightarrow> nat"
   1.386  assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   1.387  and P_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<nabla> C2)"
   1.388 -and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<sqsubseteq> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   1.389 +and m_widen: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> ~ C2 \<le> C1 \<Longrightarrow> m(C1 \<nabla> C2) < m C1"
   1.390  and "P C" shows "EX C'. iter_widen f C = Some C'"
   1.391  proof(simp add: iter_widen_def,
   1.392        rule measure_while_option_Some[where P = P and f=m])
   1.393    show "P C" by(rule `P C`)
   1.394  next
   1.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"
   1.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"
   1.397      by(simp add: P_f P_widen m_widen)
   1.398  qed
   1.399  
   1.400 @@ -558,19 +553,19 @@
   1.401  fixes n :: "'a::WN_Lc \<Rightarrow> nat"
   1.402  assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
   1.403  and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
   1.404 -and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"
   1.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"
   1.406 -and init: "P C" "f C \<sqsubseteq> C" shows "EX C'. iter_narrow f C = Some C'"
   1.407 +and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> f C1 \<le> f C2"
   1.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"
   1.409 +and init: "P C" "f C \<le> C" shows "EX C'. iter_narrow f C = Some C'"
   1.410  proof(simp add: iter_narrow_def,
   1.411 -      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<sqsubseteq> C"])
   1.412 -  show "P C \<and> f C \<sqsubseteq> C" using init by blast
   1.413 +      rule measure_while_option_Some[where f=n and P = "%C. P C \<and> f C \<le> C"])
   1.414 +  show "P C \<and> f C \<le> C" using init by blast
   1.415  next
   1.416 -  fix C assume 1: "P C \<and> f C \<sqsubseteq> C" and 2: "\<not> C \<sqsubseteq> C \<triangle> f C"
   1.417 +  fix C assume 1: "P C \<and> f C \<le> C" and 2: "\<not> C \<le> C \<triangle> f C"
   1.418    hence "P (C \<triangle> f C)" by(simp add: P_f P_narrow)
   1.419 -  moreover then have "f (C \<triangle> f C) \<sqsubseteq> C \<triangle> f C"
   1.420 -    by (metis narrow1 narrow2 1 mono preord_class.le_trans)
   1.421 +  moreover then have "f (C \<triangle> f C) \<le> C \<triangle> f C"
   1.422 +    by (metis narrow1 narrow2 1 mono order_trans)
   1.423    moreover have "n (C \<triangle> f C) < n C" using 1 2 by(simp add: n_narrow P_f)
   1.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"
   1.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"
   1.426      by blast
   1.427  qed
   1.428  
   1.429 @@ -581,39 +576,51 @@
   1.430  
   1.431  subsubsection "Termination: Intervals"
   1.432  
   1.433 -definition m_ivl :: "ivl \<Rightarrow> nat" where
   1.434 -"m_ivl ivl = (case ivl of Ivl l h \<Rightarrow>
   1.435 -     (case l of Minf \<Rightarrow> 0 | Lb _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | Ub _ \<Rightarrow> 1))"
   1.436 +definition m_rep :: "eint2 \<Rightarrow> nat" where
   1.437 +"m_rep p = (if is_empty_rep p then 3 else
   1.438 +  let (l,h) = p in (case l of Minf \<Rightarrow> 0 | _ \<Rightarrow> 1) + (case h of Pinf \<Rightarrow> 0 | _ \<Rightarrow> 1))"
   1.439 +
   1.440 +lift_definition m_ivl :: "ivl \<Rightarrow> nat" is m_rep
   1.441 +by(auto simp: m_rep_def eq_ivl_iff)
   1.442  
   1.443 -lemma m_ivl_height: "m_ivl ivl \<le> 2"
   1.444 -by(simp add: m_ivl_def split: ivl.split lub_splits)
   1.445 +lemma m_ivl_nice: "m_ivl[l\<dots>h] = (if [l\<dots>h] = \<bottom> then 3 else
   1.446 +   (if l = Minf then 0 else 1) + (if h = Pinf then 0 else 1))"
   1.447 +unfolding bot_ivl_def
   1.448 +by transfer (auto simp: m_rep_def eq_ivl_empty split: extended.split)
   1.449  
   1.450 -lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   1.451 -by(auto simp: m_ivl_def le_lub_defs le_ivl_def
   1.452 -        split: ivl.split lub_splits if_splits)
   1.453 +lemma m_ivl_height: "m_ivl iv \<le> 3"
   1.454 +by transfer (simp add: m_rep_def split: prod.split extended.split)
   1.455 +
   1.456 +lemma m_ivl_anti_mono: "y \<le> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
   1.457 +by transfer
   1.458 +   (auto simp: m_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   1.459 +         split: prod.split extended.splits if_splits)
   1.460  
   1.461  lemma m_ivl_widen:
   1.462 -  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   1.463 -by(auto simp: m_ivl_def widen_ivl_def le_lub_defs le_ivl_def
   1.464 -        split: ivl.splits lub_splits if_splits)
   1.465 +  "~ y \<le> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
   1.466 +by transfer
   1.467 +   (auto simp: m_rep_def widen_rep_def is_empty_rep_def \<gamma>_rep_cases le_iff_subset
   1.468 +         split: prod.split extended.splits if_splits)
   1.469  
   1.470  definition n_ivl :: "ivl \<Rightarrow> nat" where
   1.471 -"n_ivl ivl = 2 - m_ivl ivl"
   1.472 +"n_ivl ivl = 3 - m_ivl ivl"
   1.473  
   1.474 -lemma n_ivl_mono: "(x::ivl) \<sqsubseteq> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
   1.475 +lemma n_ivl_mono: "x \<le> y \<Longrightarrow> n_ivl x \<le> n_ivl y"
   1.476  unfolding n_ivl_def by (metis diff_le_mono2 m_ivl_anti_mono)
   1.477  
   1.478  lemma n_ivl_narrow:
   1.479 -  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   1.480 -by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_lub_defs le_ivl_def
   1.481 -        split: ivl.splits lub_splits if_splits)
   1.482 +  "~ x \<le> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
   1.483 +unfolding n_ivl_def
   1.484 +by transfer
   1.485 +   (auto simp add: m_rep_def narrow_rep_def is_empty_rep_def empty_rep_def \<gamma>_rep_cases le_iff_subset
   1.486 +         split: prod.splits if_splits extended.splits)
   1.487  
   1.488  
   1.489  interpretation Abs_Int2_measure
   1.490  where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
   1.491  and test_num' = in_ivl
   1.492  and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
   1.493 -and m = m_ivl and n = n_ivl and h = 2
   1.494 +and m = m_ivl and n = n_ivl and h = 3
   1.495  proof
   1.496    case goal1 thus ?case by(rule m_ivl_anti_mono)
   1.497  next
   1.498 @@ -629,14 +636,14 @@
   1.499  
   1.500  
   1.501  lemma iter_winden_step_ivl_termination:
   1.502 -  "\<exists>C. iter_widen (step_ivl (top(vars c))) (bot c) = Some C"
   1.503 +  "\<exists>C. iter_widen (step_ivl (Top(vars c))) (bot c) = Some C"
   1.504  apply(rule iter_widen_termination[where m = "m_c" and P = "%C. C \<in> Lc c"])
   1.505  apply (simp_all add: step'_in_Lc m_c_widen)
   1.506  done
   1.507  
   1.508  lemma iter_narrow_step_ivl_termination:
   1.509 -  "C0 \<in> Lc c \<Longrightarrow> step_ivl (top(vars c)) C0 \<sqsubseteq> C0 \<Longrightarrow>
   1.510 -  \<exists>C. iter_narrow (step_ivl (top(vars c))) C0 = Some C"
   1.511 +  "C0 \<in> Lc c \<Longrightarrow> step_ivl (Top(vars c)) C0 \<le> C0 \<Longrightarrow>
   1.512 +  \<exists>C. iter_narrow (step_ivl (Top(vars c))) C0 = Some C"
   1.513  apply(rule iter_narrow_termination[where n = "n_c" and P = "%C. C \<in> Lc c"])
   1.514  apply (simp add: step'_in_Lc)
   1.515  apply (simp)
   1.516 @@ -662,12 +669,11 @@
   1.517  
   1.518  subsubsection "Counterexamples"
   1.519  
   1.520 -text{* Widening is increasing by assumption,
   1.521 -but @{prop"x \<sqsubseteq> f x"} is not an invariant of widening. It can already
   1.522 -be lost after the first step: *}
   1.523 +text{* Widening is increasing by assumption, but @{prop"x \<le> f x"} is not an invariant of widening.
   1.524 +It can already be lost after the first step: *}
   1.525  
   1.526 -lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   1.527 -and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" shows "x \<nabla> f x \<sqsubseteq> f(x \<nabla> f x)"
   1.528 +lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
   1.529 +and "x \<le> f x" and "\<not> f x \<le> x" shows "x \<nabla> f x \<le> f(x \<nabla> f x)"
   1.530  nitpick[card = 3, expect = genuine, show_consts]
   1.531  (*
   1.532  1 < 2 < 3,
   1.533 @@ -682,9 +688,9 @@
   1.534  text{* Widening terminates but may converge more slowly than Kleene iteration.
   1.535  In the following model, Kleene iteration goes from 0 to the least pfp
   1.536  in one step but widening takes 2 steps to reach a strictly larger pfp: *}
   1.537 -lemma assumes "!!x y::'a::WN. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
   1.538 -and "x \<sqsubseteq> f x" and "\<not> f x \<sqsubseteq> x" and "f(f x) \<sqsubseteq> f x"
   1.539 -shows "f(x \<nabla> f x) \<sqsubseteq> x \<nabla> f x"
   1.540 +lemma assumes "!!x y::'a::WN. x \<le> y \<Longrightarrow> f x \<le> f y"
   1.541 +and "x \<le> f x" and "\<not> f x \<le> x" and "f(f x) \<le> f x"
   1.542 +shows "f(x \<nabla> f x) \<le> x \<nabla> f x"
   1.543  nitpick[card = 4, expect = genuine, show_consts]
   1.544  (*
   1.545