src/HOL/Lattices.thy
changeset 43753 fe5e846c0839
parent 41082 9ff94e7cc3b3
child 43873 8a2f339641c1
     1.1 --- a/src/HOL/Lattices.thy	Sun Jul 10 21:39:03 2011 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Sun Jul 10 21:56:39 2011 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4  text {* Dual lattice *}
     1.5  
     1.6  lemma dual_semilattice:
     1.7 -  "class.semilattice_inf (op \<ge>) (op >) sup"
     1.8 +  "class.semilattice_inf greater_eq greater sup"
     1.9  by (rule class.semilattice_inf.intro, rule dual_order)
    1.10    (unfold_locales, simp_all add: sup_least)
    1.11  
    1.12 @@ -104,7 +104,7 @@
    1.13    "x \<sqsubseteq> y \<longleftrightarrow> x \<sqinter> y = x"
    1.14    by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])
    1.15  
    1.16 -lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    1.17 +lemma inf_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"
    1.18    by (fast intro: inf_greatest le_infI1 le_infI2)
    1.19  
    1.20  lemma mono_inf:
    1.21 @@ -141,7 +141,7 @@
    1.22    "x \<sqsubseteq> y \<longleftrightarrow> x \<squnion> y = y"
    1.23    by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])
    1.24  
    1.25 -lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<le> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    1.26 +lemma sup_mono: "a \<sqsubseteq> c \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> a \<squnion> b \<sqsubseteq> c \<squnion> d"
    1.27    by (fast intro: sup_least le_supI1 le_supI2)
    1.28  
    1.29  lemma mono_sup:
    1.30 @@ -420,7 +420,7 @@
    1.31  begin
    1.32  
    1.33  lemma dual_bounded_lattice:
    1.34 -  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.35 +  "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
    1.36    by unfold_locales (auto simp add: less_le_not_le)
    1.37  
    1.38  end
    1.39 @@ -432,7 +432,7 @@
    1.40  begin
    1.41  
    1.42  lemma dual_boolean_algebra:
    1.43 -  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.44 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
    1.45    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.46      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    1.47  
    1.48 @@ -506,7 +506,7 @@
    1.49  lemma compl_sup [simp]:
    1.50    "- (x \<squnion> y) = - x \<sqinter> - y"
    1.51  proof -
    1.52 -  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus "op \<ge>" "op >" "op \<squnion>" "op \<sqinter>" \<top> \<bottom>
    1.53 +  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
    1.54      by (rule dual_boolean_algebra)
    1.55    then show ?thesis by simp
    1.56  qed
    1.57 @@ -523,7 +523,7 @@
    1.58  qed
    1.59  
    1.60  lemma compl_le_compl_iff: (* TODO: declare [simp] ? *)
    1.61 -  "- x \<le> - y \<longleftrightarrow> y \<le> x"
    1.62 +  "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
    1.63  by (auto dest: compl_mono)
    1.64  
    1.65  end