src/HOL/Lattices.thy
changeset 63322 bc1f17d45e91
parent 63290 9ac558ab0906
child 63588 d0e2bad67bd4
     1.1 --- a/src/HOL/Lattices.thy	Sun Jun 19 22:51:42 2016 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Mon Jun 20 17:03:50 2016 +0200
     1.3 @@ -21,24 +21,23 @@
     1.4  begin
     1.5  
     1.6  lemma left_idem [simp]: "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
     1.7 -by (simp add: assoc [symmetric])
     1.8 +  by (simp add: assoc [symmetric])
     1.9  
    1.10  lemma right_idem [simp]: "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
    1.11 -by (simp add: assoc)
    1.12 +  by (simp add: assoc)
    1.13  
    1.14  end
    1.15  
    1.16  locale semilattice_neutr = semilattice + comm_monoid
    1.17  
    1.18  locale semilattice_order = semilattice +
    1.19 -  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold>\<le>" 50)
    1.20 -    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<^bold><" 50)
    1.21 +  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold>\<le>" 50)
    1.22 +    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<^bold><" 50)
    1.23    assumes order_iff: "a \<^bold>\<le> b \<longleftrightarrow> a = a \<^bold>* b"
    1.24      and strict_order_iff: "a \<^bold>< b \<longleftrightarrow> a = a \<^bold>* b \<and> a \<noteq> b"
    1.25  begin
    1.26  
    1.27 -lemma orderI:
    1.28 -  "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
    1.29 +lemma orderI: "a = a \<^bold>* b \<Longrightarrow> a \<^bold>\<le> b"
    1.30    by (simp add: order_iff)
    1.31  
    1.32  lemma orderE:
    1.33 @@ -49,7 +48,7 @@
    1.34  sublocale ordering less_eq less
    1.35  proof
    1.36    fix a b
    1.37 -  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b"
    1.38 +  show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b
    1.39      by (simp add: order_iff strict_order_iff)
    1.40  next
    1.41    fix a
    1.42 @@ -74,12 +73,10 @@
    1.43    then show "a \<^bold>\<le> c" by (rule orderI)
    1.44  qed
    1.45  
    1.46 -lemma cobounded1 [simp]:
    1.47 -  "a \<^bold>* b \<^bold>\<le> a"
    1.48 -  by (simp add: order_iff commute)  
    1.49 +lemma cobounded1 [simp]: "a \<^bold>* b \<^bold>\<le> a"
    1.50 +  by (simp add: order_iff commute)
    1.51  
    1.52 -lemma cobounded2 [simp]:
    1.53 -  "a \<^bold>* b \<^bold>\<le> b"
    1.54 +lemma cobounded2 [simp]: "a \<^bold>* b \<^bold>\<le> b"
    1.55    by (simp add: order_iff)
    1.56  
    1.57  lemma boundedI:
    1.58 @@ -95,8 +92,7 @@
    1.59    obtains "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
    1.60    using assms by (blast intro: trans cobounded1 cobounded2)
    1.61  
    1.62 -lemma bounded_iff [simp]:
    1.63 -  "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
    1.64 +lemma bounded_iff [simp]: "a \<^bold>\<le> b \<^bold>* c \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<^bold>\<le> c"
    1.65    by (blast intro: boundedI elim: boundedE)
    1.66  
    1.67  lemma strict_boundedE:
    1.68 @@ -104,21 +100,17 @@
    1.69    obtains "a \<^bold>< b" and "a \<^bold>< c"
    1.70    using assms by (auto simp add: commute strict_iff_order elim: orderE intro!: that)+
    1.71  
    1.72 -lemma coboundedI1:
    1.73 -  "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    1.74 +lemma coboundedI1: "a \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    1.75    by (rule trans) auto
    1.76  
    1.77 -lemma coboundedI2:
    1.78 -  "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    1.79 +lemma coboundedI2: "b \<^bold>\<le> c \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c"
    1.80    by (rule trans) auto
    1.81  
    1.82 -lemma strict_coboundedI1:
    1.83 -  "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.84 +lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.85    using irrefl
    1.86      by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
    1.87  
    1.88 -lemma strict_coboundedI2:
    1.89 -  "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.90 +lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.91    using strict_coboundedI1 [of b c a] by (simp add: commute)
    1.92  
    1.93  lemma mono: "a \<^bold>\<le> c \<Longrightarrow> b \<^bold>\<le> d \<Longrightarrow> a \<^bold>* b \<^bold>\<le> c \<^bold>* d"
    1.94 @@ -152,7 +144,7 @@
    1.95  class inf =
    1.96    fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
    1.97  
    1.98 -class sup = 
    1.99 +class sup =
   1.100    fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
   1.101  
   1.102  
   1.103 @@ -175,10 +167,9 @@
   1.104  
   1.105  text \<open>Dual lattice\<close>
   1.106  
   1.107 -lemma dual_semilattice:
   1.108 -  "class.semilattice_inf sup greater_eq greater"
   1.109 -by (rule class.semilattice_inf.intro, rule dual_order)
   1.110 -  (unfold_locales, simp_all add: sup_least)
   1.111 +lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
   1.112 +  by (rule class.semilattice_inf.intro, rule dual_order)
   1.113 +    (unfold_locales, simp_all add: sup_least)
   1.114  
   1.115  end
   1.116  
   1.117 @@ -190,12 +181,10 @@
   1.118  context semilattice_inf
   1.119  begin
   1.120  
   1.121 -lemma le_infI1:
   1.122 -  "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   1.123 +lemma le_infI1: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   1.124    by (rule order_trans) auto
   1.125  
   1.126 -lemma le_infI2:
   1.127 -  "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   1.128 +lemma le_infI2: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
   1.129    by (rule order_trans) auto
   1.130  
   1.131  lemma le_infI: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
   1.132 @@ -204,20 +193,16 @@
   1.133  lemma le_infE: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
   1.134    by (blast intro: order_trans inf_le1 inf_le2)
   1.135  
   1.136 -lemma le_inf_iff:
   1.137 -  "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   1.138 +lemma le_inf_iff: "x \<sqsubseteq> y \<sqinter> z \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<sqsubseteq> z"
   1.139    by (blast intro: le_infI elim: le_infE)
   1.140  
   1.141 -lemma le_iff_inf:
   1.142 -  "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   1.143 +lemma le_iff_inf: "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
   1.144    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1] simp add: le_inf_iff)
   1.145  
   1.146  lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
   1.147    by (fast intro: inf_greatest le_infI1 le_infI2)
   1.148  
   1.149 -lemma mono_inf:
   1.150 -  fixes f :: "'a \<Rightarrow> 'b::semilattice_inf"
   1.151 -  shows "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"
   1.152 +lemma mono_inf: "mono f \<Longrightarrow> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B" for f :: "'a \<Rightarrow> 'b::semilattice_inf"
   1.153    by (auto simp add: mono_def intro: Lattices.inf_greatest)
   1.154  
   1.155  end
   1.156 @@ -225,36 +210,28 @@
   1.157  context semilattice_sup
   1.158  begin
   1.159  
   1.160 -lemma le_supI1:
   1.161 -  "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   1.162 +lemma le_supI1: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   1.163 +  by (rule order_trans) auto
   1.164 +
   1.165 +lemma le_supI2: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   1.166    by (rule order_trans) auto
   1.167  
   1.168 -lemma le_supI2:
   1.169 -  "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
   1.170 -  by (rule order_trans) auto 
   1.171 -
   1.172 -lemma le_supI:
   1.173 -  "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   1.174 +lemma le_supI: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
   1.175    by (fact sup_least) (* FIXME: duplicate lemma *)
   1.176  
   1.177 -lemma le_supE:
   1.178 -  "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   1.179 +lemma le_supE: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
   1.180    by (blast intro: order_trans sup_ge1 sup_ge2)
   1.181  
   1.182 -lemma le_sup_iff:
   1.183 -  "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   1.184 +lemma le_sup_iff: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
   1.185    by (blast intro: le_supI elim: le_supE)
   1.186  
   1.187 -lemma le_iff_sup:
   1.188 -  "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   1.189 +lemma le_iff_sup: "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
   1.190    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1] simp add: le_sup_iff)
   1.191  
   1.192  lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
   1.193    by (fast intro: sup_least le_supI1 le_supI2)
   1.194  
   1.195 -lemma mono_sup:
   1.196 -  fixes f :: "'a \<Rightarrow> 'b::semilattice_sup"
   1.197 -  shows "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"
   1.198 +lemma mono_sup: "mono f \<Longrightarrow> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)" for f :: "'a \<Rightarrow> 'b::semilattice_sup"
   1.199    by (auto simp add: mono_def intro: Lattices.sup_least)
   1.200  
   1.201  end
   1.202 @@ -302,7 +279,7 @@
   1.203  
   1.204  lemma inf_absorb2: "y \<sqsubseteq> x \<Longrightarrow> x \<sqinter> y = y"
   1.205    by (rule antisym) auto
   1.206 - 
   1.207 +
   1.208  lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem
   1.209  
   1.210  end
   1.211 @@ -352,8 +329,7 @@
   1.212  context lattice
   1.213  begin
   1.214  
   1.215 -lemma dual_lattice:
   1.216 -  "class.lattice sup (op \<ge>) (op >) inf"
   1.217 +lemma dual_lattice: "class.lattice sup (op \<ge>) (op >) inf"
   1.218    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
   1.219      (unfold_locales, auto)
   1.220  
   1.221 @@ -375,47 +351,48 @@
   1.222  lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
   1.223    by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
   1.224  
   1.225 -text\<open>If you have one of them, you have them all.\<close>
   1.226 +text \<open>If you have one of them, you have them all.\<close>
   1.227  
   1.228  lemma distrib_imp1:
   1.229 -assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.230 -shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   1.231 +  assumes distrib: "\<And>x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.232 +  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   1.233  proof-
   1.234 -  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
   1.235 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)"
   1.236 +    by simp
   1.237    also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
   1.238 -    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
   1.239 +    by (simp add: distrib inf_commute sup_assoc del: sup_inf_absorb)
   1.240    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
   1.241 -    by(simp add: inf_commute)
   1.242 -  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
   1.243 +    by (simp add: inf_commute)
   1.244 +  also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:distrib)
   1.245    finally show ?thesis .
   1.246  qed
   1.247  
   1.248  lemma distrib_imp2:
   1.249 -assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   1.250 -shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.251 +  assumes distrib: "\<And>x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
   1.252 +  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.253  proof-
   1.254 -  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
   1.255 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)"
   1.256 +    by simp
   1.257    also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
   1.258 -    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
   1.259 +    by (simp add: distrib sup_commute inf_assoc del: inf_sup_absorb)
   1.260    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
   1.261 -    by(simp add: sup_commute)
   1.262 -  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
   1.263 +    by (simp add: sup_commute)
   1.264 +  also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by (simp add:distrib)
   1.265    finally show ?thesis .
   1.266  qed
   1.267  
   1.268  end
   1.269  
   1.270 +
   1.271  subsubsection \<open>Strict order\<close>
   1.272  
   1.273  context semilattice_inf
   1.274  begin
   1.275  
   1.276 -lemma less_infI1:
   1.277 -  "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   1.278 +lemma less_infI1: "a \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   1.279    by (auto simp add: less_le inf_absorb1 intro: le_infI1)
   1.280  
   1.281 -lemma less_infI2:
   1.282 -  "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   1.283 +lemma less_infI2: "b \<sqsubset> x \<Longrightarrow> a \<sqinter> b \<sqsubset> x"
   1.284    by (auto simp add: less_le inf_absorb2 intro: le_infI2)
   1.285  
   1.286  end
   1.287 @@ -423,13 +400,11 @@
   1.288  context semilattice_sup
   1.289  begin
   1.290  
   1.291 -lemma less_supI1:
   1.292 -  "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.293 +lemma less_supI1: "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.294    using dual_semilattice
   1.295    by (rule semilattice_inf.less_infI1)
   1.296  
   1.297 -lemma less_supI2:
   1.298 -  "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.299 +lemma less_supI2: "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
   1.300    using dual_semilattice
   1.301    by (rule semilattice_inf.less_infI2)
   1.302  
   1.303 @@ -444,31 +419,24 @@
   1.304  context distrib_lattice
   1.305  begin
   1.306  
   1.307 -lemma sup_inf_distrib2:
   1.308 -  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   1.309 +lemma sup_inf_distrib2: "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
   1.310    by (simp add: sup_commute sup_inf_distrib1)
   1.311  
   1.312 -lemma inf_sup_distrib1:
   1.313 -  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.314 +lemma inf_sup_distrib1: "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
   1.315    by (rule distrib_imp2 [OF sup_inf_distrib1])
   1.316  
   1.317 -lemma inf_sup_distrib2:
   1.318 -  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   1.319 +lemma inf_sup_distrib2: "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
   1.320    by (simp add: inf_commute inf_sup_distrib1)
   1.321  
   1.322 -lemma dual_distrib_lattice:
   1.323 -  "class.distrib_lattice sup (op \<ge>) (op >) inf"
   1.324 +lemma dual_distrib_lattice: "class.distrib_lattice sup (op \<ge>) (op >) inf"
   1.325    by (rule class.distrib_lattice.intro, rule dual_lattice)
   1.326      (unfold_locales, fact inf_sup_distrib1)
   1.327  
   1.328 -lemmas sup_inf_distrib =
   1.329 -  sup_inf_distrib1 sup_inf_distrib2
   1.330 +lemmas sup_inf_distrib = sup_inf_distrib1 sup_inf_distrib2
   1.331  
   1.332 -lemmas inf_sup_distrib =
   1.333 -  inf_sup_distrib1 inf_sup_distrib2
   1.334 +lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2
   1.335  
   1.336 -lemmas distrib =
   1.337 -  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   1.338 +lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2
   1.339  
   1.340  end
   1.341  
   1.342 @@ -481,8 +449,7 @@
   1.343  sublocale inf_top: semilattice_neutr inf top
   1.344    + inf_top: semilattice_neutr_order inf top less_eq less
   1.345  proof
   1.346 -  fix x
   1.347 -  show "x \<sqinter> \<top> = x"
   1.348 +  show "x \<sqinter> \<top> = x" for x
   1.349      by (rule inf_absorb1) simp
   1.350  qed
   1.351  
   1.352 @@ -494,8 +461,7 @@
   1.353  sublocale sup_bot: semilattice_neutr sup bot
   1.354    + sup_bot: semilattice_neutr_order sup bot greater_eq greater
   1.355  proof
   1.356 -  fix x
   1.357 -  show "x \<squnion> \<bottom> = x"
   1.358 +  show "x \<squnion> \<bottom> = x" for x
   1.359      by (rule sup_absorb1) simp
   1.360  qed
   1.361  
   1.362 @@ -506,28 +472,22 @@
   1.363  
   1.364  subclass bounded_semilattice_sup_bot ..
   1.365  
   1.366 -lemma inf_bot_left [simp]:
   1.367 -  "\<bottom> \<sqinter> x = \<bottom>"
   1.368 +lemma inf_bot_left [simp]: "\<bottom> \<sqinter> x = \<bottom>"
   1.369    by (rule inf_absorb1) simp
   1.370  
   1.371 -lemma inf_bot_right [simp]:
   1.372 -  "x \<sqinter> \<bottom> = \<bottom>"
   1.373 +lemma inf_bot_right [simp]: "x \<sqinter> \<bottom> = \<bottom>"
   1.374    by (rule inf_absorb2) simp
   1.375  
   1.376 -lemma sup_bot_left:
   1.377 -  "\<bottom> \<squnion> x = x"
   1.378 +lemma sup_bot_left: "\<bottom> \<squnion> x = x"
   1.379    by (fact sup_bot.left_neutral)
   1.380  
   1.381 -lemma sup_bot_right:
   1.382 -  "x \<squnion> \<bottom> = x"
   1.383 +lemma sup_bot_right: "x \<squnion> \<bottom> = x"
   1.384    by (fact sup_bot.right_neutral)
   1.385  
   1.386 -lemma sup_eq_bot_iff [simp]:
   1.387 -  "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.388 +lemma sup_eq_bot_iff [simp]: "x \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.389    by (simp add: eq_iff)
   1.390  
   1.391 -lemma bot_eq_sup_iff [simp]:
   1.392 -  "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.393 +lemma bot_eq_sup_iff [simp]: "\<bottom> = x \<squnion> y \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
   1.394    by (simp add: eq_iff)
   1.395  
   1.396  end
   1.397 @@ -537,24 +497,19 @@
   1.398  
   1.399  subclass bounded_semilattice_inf_top ..
   1.400  
   1.401 -lemma sup_top_left [simp]:
   1.402 -  "\<top> \<squnion> x = \<top>"
   1.403 +lemma sup_top_left [simp]: "\<top> \<squnion> x = \<top>"
   1.404    by (rule sup_absorb1) simp
   1.405  
   1.406 -lemma sup_top_right [simp]:
   1.407 -  "x \<squnion> \<top> = \<top>"
   1.408 +lemma sup_top_right [simp]: "x \<squnion> \<top> = \<top>"
   1.409    by (rule sup_absorb2) simp
   1.410  
   1.411 -lemma inf_top_left:
   1.412 -  "\<top> \<sqinter> x = x"
   1.413 +lemma inf_top_left: "\<top> \<sqinter> x = x"
   1.414    by (fact inf_top.left_neutral)
   1.415  
   1.416 -lemma inf_top_right:
   1.417 -  "x \<sqinter> \<top> = x"
   1.418 +lemma inf_top_right: "x \<sqinter> \<top> = x"
   1.419    by (fact inf_top.right_neutral)
   1.420  
   1.421 -lemma inf_eq_top_iff [simp]:
   1.422 -  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   1.423 +lemma inf_eq_top_iff [simp]: "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   1.424    by (simp add: eq_iff)
   1.425  
   1.426  end
   1.427 @@ -565,8 +520,7 @@
   1.428  subclass bounded_lattice_bot ..
   1.429  subclass bounded_lattice_top ..
   1.430  
   1.431 -lemma dual_bounded_lattice:
   1.432 -  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   1.433 +lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   1.434    by unfold_locales (auto simp add: less_le_not_le)
   1.435  
   1.436  end
   1.437 @@ -582,12 +536,10 @@
   1.438    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
   1.439      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
   1.440  
   1.441 -lemma compl_inf_bot [simp]:
   1.442 -  "- x \<sqinter> x = \<bottom>"
   1.443 +lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>"
   1.444    by (simp add: inf_commute inf_compl_bot)
   1.445  
   1.446 -lemma compl_sup_top [simp]:
   1.447 -  "- x \<squnion> x = \<top>"
   1.448 +lemma compl_sup_top [simp]: "- x \<squnion> x = \<top>"
   1.449    by (simp add: sup_commute sup_compl_top)
   1.450  
   1.451  lemma compl_unique:
   1.452 @@ -606,12 +558,10 @@
   1.453    then show "- x = y" by simp
   1.454  qed
   1.455  
   1.456 -lemma double_compl [simp]:
   1.457 -  "- (- x) = x"
   1.458 +lemma double_compl [simp]: "- (- x) = x"
   1.459    using compl_inf_bot compl_sup_top by (rule compl_unique)
   1.460  
   1.461 -lemma compl_eq_compl_iff [simp]:
   1.462 -  "- x = - y \<longleftrightarrow> x = y"
   1.463 +lemma compl_eq_compl_iff [simp]: "- x = - y \<longleftrightarrow> x = y"
   1.464  proof
   1.465    assume "- x = - y"
   1.466    then have "- (- x) = - (- y)" by (rule arg_cong)
   1.467 @@ -621,22 +571,19 @@
   1.468    then show "- x = - y" by simp
   1.469  qed
   1.470  
   1.471 -lemma compl_bot_eq [simp]:
   1.472 -  "- \<bottom> = \<top>"
   1.473 +lemma compl_bot_eq [simp]: "- \<bottom> = \<top>"
   1.474  proof -
   1.475    from sup_compl_top have "\<bottom> \<squnion> - \<bottom> = \<top>" .
   1.476    then show ?thesis by simp
   1.477  qed
   1.478  
   1.479 -lemma compl_top_eq [simp]:
   1.480 -  "- \<top> = \<bottom>"
   1.481 +lemma compl_top_eq [simp]: "- \<top> = \<bottom>"
   1.482  proof -
   1.483    from inf_compl_bot have "\<top> \<sqinter> - \<top> = \<bottom>" .
   1.484    then show ?thesis by simp
   1.485  qed
   1.486  
   1.487 -lemma compl_inf [simp]:
   1.488 -  "- (x \<sqinter> y) = - x \<squnion> - y"
   1.489 +lemma compl_inf [simp]: "- (x \<sqinter> y) = - x \<squnion> - y"
   1.490  proof (rule compl_unique)
   1.491    have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"
   1.492      by (simp only: inf_sup_distrib inf_aci)
   1.493 @@ -649,86 +596,87 @@
   1.494      by (simp add: sup_compl_top)
   1.495  qed
   1.496  
   1.497 -lemma compl_sup [simp]:
   1.498 -  "- (x \<squnion> y) = - x \<sqinter> - y"
   1.499 +lemma compl_sup [simp]: "- (x \<squnion> y) = - x \<sqinter> - y"
   1.500    using dual_boolean_algebra
   1.501    by (rule boolean_algebra.compl_inf)
   1.502  
   1.503  lemma compl_mono:
   1.504 -  "x \<sqsubseteq> y \<Longrightarrow> - y \<sqsubseteq> - x"
   1.505 +  assumes "x \<sqsubseteq> y"
   1.506 +  shows "- y \<sqsubseteq> - x"
   1.507  proof -
   1.508 -  assume "x \<sqsubseteq> y"
   1.509 -  then have "x \<squnion> y = y" by (simp only: le_iff_sup)
   1.510 +  from assms have "x \<squnion> y = y" by (simp only: le_iff_sup)
   1.511    then have "- (x \<squnion> y) = - y" by simp
   1.512    then have "- x \<sqinter> - y = - y" by simp
   1.513    then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)
   1.514 -  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
   1.515 +  then show ?thesis by (simp only: le_iff_inf)
   1.516  qed
   1.517  
   1.518 -lemma compl_le_compl_iff [simp]:
   1.519 -  "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   1.520 +lemma compl_le_compl_iff [simp]: "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
   1.521    by (auto dest: compl_mono)
   1.522  
   1.523  lemma compl_le_swap1:
   1.524 -  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"
   1.525 +  assumes "y \<sqsubseteq> - x"
   1.526 +  shows "x \<sqsubseteq> -y"
   1.527  proof -
   1.528    from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)
   1.529    then show ?thesis by simp
   1.530  qed
   1.531  
   1.532  lemma compl_le_swap2:
   1.533 -  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"
   1.534 +  assumes "- y \<sqsubseteq> x"
   1.535 +  shows "- x \<sqsubseteq> y"
   1.536  proof -
   1.537    from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)
   1.538    then show ?thesis by simp
   1.539  qed
   1.540  
   1.541 -lemma compl_less_compl_iff: (* TODO: declare [simp] ? *)
   1.542 -  "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"
   1.543 +lemma compl_less_compl_iff: "- x \<sqsubset> - y \<longleftrightarrow> y \<sqsubset> x"  (* TODO: declare [simp] ? *)
   1.544    by (auto simp add: less_le)
   1.545  
   1.546  lemma compl_less_swap1:
   1.547 -  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"
   1.548 +  assumes "y \<sqsubset> - x"
   1.549 +  shows "x \<sqsubset> - y"
   1.550  proof -
   1.551    from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)
   1.552    then show ?thesis by simp
   1.553  qed
   1.554  
   1.555  lemma compl_less_swap2:
   1.556 -  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"
   1.557 +  assumes "- y \<sqsubset> x"
   1.558 +  shows "- x \<sqsubset> y"
   1.559  proof -
   1.560    from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
   1.561    then show ?thesis by simp
   1.562  qed
   1.563  
   1.564  lemma sup_cancel_left1: "sup (sup x a) (sup (- x) b) = top"
   1.565 -by(simp add: inf_sup_aci sup_compl_top)
   1.566 +  by (simp add: inf_sup_aci sup_compl_top)
   1.567  
   1.568  lemma sup_cancel_left2: "sup (sup (- x) a) (sup x b) = top"
   1.569 -by(simp add: inf_sup_aci sup_compl_top)
   1.570 +  by (simp add: inf_sup_aci sup_compl_top)
   1.571  
   1.572  lemma inf_cancel_left1: "inf (inf x a) (inf (- x) b) = bot"
   1.573 -by(simp add: inf_sup_aci inf_compl_bot)
   1.574 +  by (simp add: inf_sup_aci inf_compl_bot)
   1.575  
   1.576  lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
   1.577 -by(simp add: inf_sup_aci inf_compl_bot)
   1.578 +  by (simp add: inf_sup_aci inf_compl_bot)
   1.579  
   1.580 -declare inf_compl_bot [simp] sup_compl_top [simp]
   1.581 +declare inf_compl_bot [simp] and sup_compl_top [simp]
   1.582  
   1.583  lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
   1.584 -by(simp add: sup_assoc[symmetric])
   1.585 +  by (simp add: sup_assoc[symmetric])
   1.586  
   1.587  lemma sup_compl_top_left2 [simp]: "sup x (sup (- x) y) = top"
   1.588 -using sup_compl_top_left1[of "- x" y] by simp
   1.589 +  using sup_compl_top_left1[of "- x" y] by simp
   1.590  
   1.591  lemma inf_compl_bot_left1 [simp]: "inf (- x) (inf x y) = bot"
   1.592 -by(simp add: inf_assoc[symmetric])
   1.593 +  by (simp add: inf_assoc[symmetric])
   1.594  
   1.595  lemma inf_compl_bot_left2 [simp]: "inf x (inf (- x) y) = bot"
   1.596 -using inf_compl_bot_left1[of "- x" y] by simp
   1.597 +  using inf_compl_bot_left1[of "- x" y] by simp
   1.598  
   1.599  lemma inf_compl_bot_right [simp]: "inf x (inf y (- x)) = bot"
   1.600 -by(subst inf_left_commute) simp
   1.601 +  by (subst inf_left_commute) simp
   1.602  
   1.603  end
   1.604  
   1.605 @@ -740,6 +688,7 @@
   1.606  simproc_setup boolean_algebra_cancel_inf ("inf a b::'a::boolean_algebra") =
   1.607    \<open>fn phi => fn ss => try Boolean_Algebra_Cancel.cancel_inf_conv\<close>
   1.608  
   1.609 +
   1.610  subsection \<open>\<open>min/max\<close> as special case of lattice\<close>
   1.611  
   1.612  context linorder
   1.613 @@ -749,64 +698,48 @@
   1.614    + max: semilattice_order max greater_eq greater
   1.615    by standard (auto simp add: min_def max_def)
   1.616  
   1.617 -lemma min_le_iff_disj:
   1.618 -  "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   1.619 +lemma min_le_iff_disj: "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
   1.620    unfolding min_def using linear by (auto intro: order_trans)
   1.621  
   1.622 -lemma le_max_iff_disj:
   1.623 -  "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   1.624 +lemma le_max_iff_disj: "z \<le> max x y \<longleftrightarrow> z \<le> x \<or> z \<le> y"
   1.625    unfolding max_def using linear by (auto intro: order_trans)
   1.626  
   1.627 -lemma min_less_iff_disj:
   1.628 -  "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   1.629 +lemma min_less_iff_disj: "min x y < z \<longleftrightarrow> x < z \<or> y < z"
   1.630    unfolding min_def le_less using less_linear by (auto intro: less_trans)
   1.631  
   1.632 -lemma less_max_iff_disj:
   1.633 -  "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   1.634 +lemma less_max_iff_disj: "z < max x y \<longleftrightarrow> z < x \<or> z < y"
   1.635    unfolding max_def le_less using less_linear by (auto intro: less_trans)
   1.636  
   1.637 -lemma min_less_iff_conj [simp]:
   1.638 -  "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   1.639 +lemma min_less_iff_conj [simp]: "z < min x y \<longleftrightarrow> z < x \<and> z < y"
   1.640    unfolding min_def le_less using less_linear by (auto intro: less_trans)
   1.641  
   1.642 -lemma max_less_iff_conj [simp]:
   1.643 -  "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   1.644 +lemma max_less_iff_conj [simp]: "max x y < z \<longleftrightarrow> x < z \<and> y < z"
   1.645    unfolding max_def le_less using less_linear by (auto intro: less_trans)
   1.646  
   1.647 -lemma min_max_distrib1:
   1.648 -  "min (max b c) a = max (min b a) (min c a)"
   1.649 +lemma min_max_distrib1: "min (max b c) a = max (min b a) (min c a)"
   1.650    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   1.651  
   1.652 -lemma min_max_distrib2:
   1.653 -  "min a (max b c) = max (min a b) (min a c)"
   1.654 +lemma min_max_distrib2: "min a (max b c) = max (min a b) (min a c)"
   1.655    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   1.656  
   1.657 -lemma max_min_distrib1:
   1.658 -  "max (min b c) a = min (max b a) (max c a)"
   1.659 +lemma max_min_distrib1: "max (min b c) a = min (max b a) (max c a)"
   1.660    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   1.661  
   1.662 -lemma max_min_distrib2:
   1.663 -  "max a (min b c) = min (max a b) (max a c)"
   1.664 +lemma max_min_distrib2: "max a (min b c) = min (max a b) (max a c)"
   1.665    by (auto simp add: min_def max_def not_le dest: le_less_trans less_trans intro: antisym)
   1.666  
   1.667  lemmas min_max_distribs = min_max_distrib1 min_max_distrib2 max_min_distrib1 max_min_distrib2
   1.668  
   1.669 -lemma split_min [no_atp]:
   1.670 -  "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   1.671 +lemma split_min [no_atp]: "P (min i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P i) \<and> (\<not> i \<le> j \<longrightarrow> P j)"
   1.672    by (simp add: min_def)
   1.673  
   1.674 -lemma split_max [no_atp]:
   1.675 -  "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   1.676 +lemma split_max [no_atp]: "P (max i j) \<longleftrightarrow> (i \<le> j \<longrightarrow> P j) \<and> (\<not> i \<le> j \<longrightarrow> P i)"
   1.677    by (simp add: max_def)
   1.678  
   1.679 -lemma min_of_mono:
   1.680 -  fixes f :: "'a \<Rightarrow> 'b::linorder"
   1.681 -  shows "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)"
   1.682 +lemma min_of_mono: "mono f \<Longrightarrow> min (f m) (f n) = f (min m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   1.683    by (auto simp: mono_def Orderings.min_def min_def intro: Orderings.antisym)
   1.684  
   1.685 -lemma max_of_mono:
   1.686 -  fixes f :: "'a \<Rightarrow> 'b::linorder"
   1.687 -  shows "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)"
   1.688 +lemma max_of_mono: "mono f \<Longrightarrow> max (f m) (f n) = f (max m n)" for f :: "'a \<Rightarrow> 'b::linorder"
   1.689    by (auto simp: mono_def Orderings.max_def max_def intro: Orderings.antisym)
   1.690  
   1.691  end
   1.692 @@ -821,27 +754,33 @@
   1.693  subsection \<open>Uniqueness of inf and sup\<close>
   1.694  
   1.695  lemma (in semilattice_inf) inf_unique:
   1.696 -  fixes f (infixl "\<triangle>" 70)
   1.697 -  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x" and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   1.698 -  and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   1.699 +  fixes f  (infixl "\<triangle>" 70)
   1.700 +  assumes le1: "\<And>x y. x \<triangle> y \<sqsubseteq> x"
   1.701 +    and le2: "\<And>x y. x \<triangle> y \<sqsubseteq> y"
   1.702 +    and greatest: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   1.703    shows "x \<sqinter> y = x \<triangle> y"
   1.704  proof (rule antisym)
   1.705 -  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)
   1.706 -next
   1.707 -  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)
   1.708 -  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_all
   1.709 +  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y"
   1.710 +    by (rule le_infI) (rule le1, rule le2)
   1.711 +  have leI: "\<And>x y z. x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<triangle> z"
   1.712 +    by (blast intro: greatest)
   1.713 +  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y"
   1.714 +    by (rule leI) simp_all
   1.715  qed
   1.716  
   1.717  lemma (in semilattice_sup) sup_unique:
   1.718 -  fixes f (infixl "\<nabla>" 70)
   1.719 -  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y" and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   1.720 -  and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   1.721 +  fixes f  (infixl "\<nabla>" 70)
   1.722 +  assumes ge1 [simp]: "\<And>x y. x \<sqsubseteq> x \<nabla> y"
   1.723 +    and ge2: "\<And>x y. y \<sqsubseteq> x \<nabla> y"
   1.724 +    and least: "\<And>x y z. y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<nabla> z \<sqsubseteq> x"
   1.725    shows "x \<squnion> y = x \<nabla> y"
   1.726  proof (rule antisym)
   1.727 -  show "x \<squnion> y \<sqsubseteq> x \<nabla> y" by (rule le_supI) (rule ge1, rule ge2)
   1.728 -next
   1.729 -  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z" by (blast intro: least)
   1.730 -  show "x \<nabla> y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_all
   1.731 +  show "x \<squnion> y \<sqsubseteq> x \<nabla> y"
   1.732 +    by (rule le_supI) (rule ge1, rule ge2)
   1.733 +  have leI: "\<And>x y z. x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<nabla> y \<sqsubseteq> z"
   1.734 +    by (blast intro: least)
   1.735 +  show "x \<nabla> y \<sqsubseteq> x \<squnion> y"
   1.736 +    by (rule leI) simp_all
   1.737  qed
   1.738  
   1.739  
   1.740 @@ -850,33 +789,25 @@
   1.741  instantiation bool :: boolean_algebra
   1.742  begin
   1.743  
   1.744 -definition
   1.745 -  bool_Compl_def [simp]: "uminus = Not"
   1.746 +definition bool_Compl_def [simp]: "uminus = Not"
   1.747  
   1.748 -definition
   1.749 -  bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   1.750 +definition bool_diff_def [simp]: "A - B \<longleftrightarrow> A \<and> \<not> B"
   1.751  
   1.752 -definition
   1.753 -  [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   1.754 +definition [simp]: "P \<sqinter> Q \<longleftrightarrow> P \<and> Q"
   1.755  
   1.756 -definition
   1.757 -  [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   1.758 +definition [simp]: "P \<squnion> Q \<longleftrightarrow> P \<or> Q"
   1.759  
   1.760 -instance proof
   1.761 -qed auto
   1.762 +instance by standard auto
   1.763  
   1.764  end
   1.765  
   1.766 -lemma sup_boolI1:
   1.767 -  "P \<Longrightarrow> P \<squnion> Q"
   1.768 +lemma sup_boolI1: "P \<Longrightarrow> P \<squnion> Q"
   1.769    by simp
   1.770  
   1.771 -lemma sup_boolI2:
   1.772 -  "Q \<Longrightarrow> P \<squnion> Q"
   1.773 +lemma sup_boolI2: "Q \<Longrightarrow> P \<squnion> Q"
   1.774    by simp
   1.775  
   1.776 -lemma sup_boolE:
   1.777 -  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   1.778 +lemma sup_boolE: "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
   1.779    by auto
   1.780  
   1.781  
   1.782 @@ -885,48 +816,40 @@
   1.783  instantiation "fun" :: (type, semilattice_sup) semilattice_sup
   1.784  begin
   1.785  
   1.786 -definition
   1.787 -  "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   1.788 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   1.789  
   1.790 -lemma sup_apply [simp, code]:
   1.791 -  "(f \<squnion> g) x = f x \<squnion> g x"
   1.792 +lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x"
   1.793    by (simp add: sup_fun_def)
   1.794  
   1.795 -instance proof
   1.796 -qed (simp_all add: le_fun_def)
   1.797 +instance by standard (simp_all add: le_fun_def)
   1.798  
   1.799  end
   1.800  
   1.801  instantiation "fun" :: (type, semilattice_inf) semilattice_inf
   1.802  begin
   1.803  
   1.804 -definition
   1.805 -  "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   1.806 +definition "f \<sqinter> g = (\<lambda>x. f x \<sqinter> g x)"
   1.807  
   1.808 -lemma inf_apply [simp, code]:
   1.809 -  "(f \<sqinter> g) x = f x \<sqinter> g x"
   1.810 +lemma inf_apply [simp, code]: "(f \<sqinter> g) x = f x \<sqinter> g x"
   1.811    by (simp add: inf_fun_def)
   1.812  
   1.813 -instance proof
   1.814 -qed (simp_all add: le_fun_def)
   1.815 +instance by standard (simp_all add: le_fun_def)
   1.816  
   1.817  end
   1.818  
   1.819  instance "fun" :: (type, lattice) lattice ..
   1.820  
   1.821 -instance "fun" :: (type, distrib_lattice) distrib_lattice proof
   1.822 -qed (rule ext, simp add: sup_inf_distrib1)
   1.823 +instance "fun" :: (type, distrib_lattice) distrib_lattice
   1.824 +  by standard (rule ext, simp add: sup_inf_distrib1)
   1.825  
   1.826  instance "fun" :: (type, bounded_lattice) bounded_lattice ..
   1.827  
   1.828  instantiation "fun" :: (type, uminus) uminus
   1.829  begin
   1.830  
   1.831 -definition
   1.832 -  fun_Compl_def: "- A = (\<lambda>x. - A x)"
   1.833 +definition fun_Compl_def: "- A = (\<lambda>x. - A x)"
   1.834  
   1.835 -lemma uminus_apply [simp, code]:
   1.836 -  "(- A) x = - (A x)"
   1.837 +lemma uminus_apply [simp, code]: "(- A) x = - (A x)"
   1.838    by (simp add: fun_Compl_def)
   1.839  
   1.840  instance ..
   1.841 @@ -936,19 +859,17 @@
   1.842  instantiation "fun" :: (type, minus) minus
   1.843  begin
   1.844  
   1.845 -definition
   1.846 -  fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   1.847 +definition fun_diff_def: "A - B = (\<lambda>x. A x - B x)"
   1.848  
   1.849 -lemma minus_apply [simp, code]:
   1.850 -  "(A - B) x = A x - B x"
   1.851 +lemma minus_apply [simp, code]: "(A - B) x = A x - B x"
   1.852    by (simp add: fun_diff_def)
   1.853  
   1.854  instance ..
   1.855  
   1.856  end
   1.857  
   1.858 -instance "fun" :: (type, boolean_algebra) boolean_algebra proof
   1.859 -qed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   1.860 +instance "fun" :: (type, boolean_algebra) boolean_algebra
   1.861 +  by standard (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+
   1.862  
   1.863  
   1.864  subsection \<open>Lattice on unary and binary predicates\<close>
   1.865 @@ -995,10 +916,7 @@
   1.866  lemma sup2E: "(A \<squnion> B) x y \<Longrightarrow> (A x y \<Longrightarrow> P) \<Longrightarrow> (B x y \<Longrightarrow> P) \<Longrightarrow> P"
   1.867    by (simp add: sup_fun_def) iprover
   1.868  
   1.869 -text \<open>
   1.870 -  \medskip Classical introduction rule: no commitment to \<open>A\<close> vs
   1.871 -  \<open>B\<close>.
   1.872 -\<close>
   1.873 +text \<open> \<^medskip> Classical introduction rule: no commitment to \<open>A\<close> vs \<open>B\<close>.\<close>
   1.874  
   1.875  lemma sup1CI: "(\<not> B x \<Longrightarrow> A x) \<Longrightarrow> (A \<squnion> B) x"
   1.876    by (auto simp add: sup_fun_def)
   1.877 @@ -1012,4 +930,3 @@
   1.878    less (infix "\<sqsubset>" 50)
   1.879  
   1.880  end
   1.881 -