src/HOL/Lattices.thy
changeset 63588 d0e2bad67bd4
parent 63322 bc1f17d45e91
child 63661 92e037803666
     1.1 --- a/src/HOL/Lattices.thy	Tue Aug 02 21:04:52 2016 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Aug 02 21:05:34 2016 +0200
     1.3 @@ -47,12 +47,10 @@
     1.4  
     1.5  sublocale ordering less_eq less
     1.6  proof
     1.7 -  fix a b
     1.8    show "a \<^bold>< b \<longleftrightarrow> a \<^bold>\<le> b \<and> a \<noteq> b" for a b
     1.9      by (simp add: order_iff strict_order_iff)
    1.10  next
    1.11 -  fix a
    1.12 -  show "a \<^bold>\<le> a"
    1.13 +  show "a \<^bold>\<le> a" for a
    1.14      by (simp add: order_iff)
    1.15  next
    1.16    fix a b
    1.17 @@ -83,8 +81,10 @@
    1.18    assumes "a \<^bold>\<le> b" and "a \<^bold>\<le> c"
    1.19    shows "a \<^bold>\<le> b \<^bold>* c"
    1.20  proof (rule orderI)
    1.21 -  from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a" by (auto elim!: orderE)
    1.22 -  then show "a = a \<^bold>* (b \<^bold>* c)" by (simp add: assoc [symmetric])
    1.23 +  from assms obtain "a \<^bold>* b = a" and "a \<^bold>* c = a"
    1.24 +    by (auto elim!: orderE)
    1.25 +  then show "a = a \<^bold>* (b \<^bold>* c)"
    1.26 +    by (simp add: assoc [symmetric])
    1.27  qed
    1.28  
    1.29  lemma boundedE:
    1.30 @@ -108,7 +108,8 @@
    1.31  
    1.32  lemma strict_coboundedI1: "a \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.33    using irrefl
    1.34 -    by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order elim: strict_boundedE)
    1.35 +  by (auto intro: not_eq_order_implies_strict coboundedI1 strict_implies_order
    1.36 +      elim: strict_boundedE)
    1.37  
    1.38  lemma strict_coboundedI2: "b \<^bold>< c \<Longrightarrow> a \<^bold>* b \<^bold>< c"
    1.39    using strict_coboundedI1 [of b c a] by (simp add: commute)
    1.40 @@ -117,10 +118,10 @@
    1.41    by (blast intro: boundedI coboundedI1 coboundedI2)
    1.42  
    1.43  lemma absorb1: "a \<^bold>\<le> b \<Longrightarrow> a \<^bold>* b = a"
    1.44 -  by (rule antisym) (auto simp add: refl)
    1.45 +  by (rule antisym) (auto simp: refl)
    1.46  
    1.47  lemma absorb2: "b \<^bold>\<le> a \<Longrightarrow> a \<^bold>* b = b"
    1.48 -  by (rule antisym) (auto simp add: refl)
    1.49 +  by (rule antisym) (auto simp: refl)
    1.50  
    1.51  lemma absorb_iff1: "a \<^bold>\<le> b \<longleftrightarrow> a \<^bold>* b = a"
    1.52    using order_iff by auto
    1.53 @@ -165,8 +166,7 @@
    1.54    and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
    1.55  begin
    1.56  
    1.57 -text \<open>Dual lattice\<close>
    1.58 -
    1.59 +text \<open>Dual lattice.\<close>
    1.60  lemma dual_semilattice: "class.semilattice_inf sup greater_eq greater"
    1.61    by (rule class.semilattice_inf.intro, rule dual_order)
    1.62      (unfold_locales, simp_all add: sup_least)
    1.63 @@ -330,7 +330,10 @@
    1.64  begin
    1.65  
    1.66  lemma dual_lattice: "class.lattice sup (op \<ge>) (op >) inf"
    1.67 -  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    1.68 +  by (rule class.lattice.intro,
    1.69 +      rule dual_semilattice,
    1.70 +      rule class.semilattice_sup.intro,
    1.71 +      rule dual_order)
    1.72      (unfold_locales, auto)
    1.73  
    1.74  lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
    1.75 @@ -343,7 +346,7 @@
    1.76  
    1.77  lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
    1.78  
    1.79 -text\<open>Towards distributivity\<close>
    1.80 +text \<open>Towards distributivity.\<close>
    1.81  
    1.82  lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.83    by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)
    1.84 @@ -533,7 +536,9 @@
    1.85  
    1.86  lemma dual_boolean_algebra:
    1.87    "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
    1.88 -  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.89 +  by (rule class.boolean_algebra.intro,
    1.90 +      rule dual_bounded_lattice,
    1.91 +      rule dual_distrib_lattice)
    1.92      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    1.93  
    1.94  lemma compl_inf_bot [simp]: "- x \<sqinter> x = \<bottom>"
    1.95 @@ -645,7 +650,8 @@
    1.96    assumes "- y \<sqsubset> x"
    1.97    shows "- x \<sqsubset> y"
    1.98  proof -
    1.99 -  from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)
   1.100 +  from assms have "- x \<sqsubset> - (- y)"
   1.101 +    by (simp only: compl_less_compl_iff)
   1.102    then show ?thesis by simp
   1.103  qed
   1.104  
   1.105 @@ -661,7 +667,8 @@
   1.106  lemma inf_cancel_left2: "inf (inf (- x) a) (inf x b) = bot"
   1.107    by (simp add: inf_sup_aci inf_compl_bot)
   1.108  
   1.109 -declare inf_compl_bot [simp] and sup_compl_top [simp]
   1.110 +declare inf_compl_bot [simp]
   1.111 +  and sup_compl_top [simp]
   1.112  
   1.113  lemma sup_compl_top_left1 [simp]: "sup (- x) (sup x y) = top"
   1.114    by (simp add: sup_assoc[symmetric])
   1.115 @@ -821,7 +828,8 @@
   1.116  lemma sup_apply [simp, code]: "(f \<squnion> g) x = f x \<squnion> g x"
   1.117    by (simp add: sup_fun_def)
   1.118  
   1.119 -instance by standard (simp_all add: le_fun_def)
   1.120 +instance
   1.121 +  by standard (simp_all add: le_fun_def)
   1.122  
   1.123  end
   1.124