src/HOL/Lattices.thy
changeset 44918 6a80fbc4e72c
parent 44845 5e51075cbd97
child 44919 482f1807976e
     1.1 --- a/src/HOL/Lattices.thy	Tue Sep 13 13:17:52 2011 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue Sep 13 16:21:48 2011 +0200
     1.3 @@ -180,10 +180,10 @@
     1.4  lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"
     1.5    by (fact inf.left_commute)
     1.6  
     1.7 -lemma inf_idem (*[simp]*): "x \<sqinter> x = x"
     1.8 +lemma inf_idem [simp]: "x \<sqinter> x = x"
     1.9    by (fact inf.idem)
    1.10  
    1.11 -lemma inf_left_idem (*[simp]*): "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    1.12 +lemma inf_left_idem [simp]: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"
    1.13    by (fact inf.left_idem)
    1.14  
    1.15  lemma inf_absorb1: "x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x"
    1.16 @@ -219,10 +219,10 @@
    1.17  lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"
    1.18    by (fact sup.left_commute)
    1.19  
    1.20 -lemma sup_idem (*[simp]*): "x \<squnion> x = x"
    1.21 +lemma sup_idem [simp]: "x \<squnion> x = x"
    1.22    by (fact sup.idem)
    1.23  
    1.24 -lemma sup_left_idem (*[simp]*): "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    1.25 +lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"
    1.26    by (fact sup.left_idem)
    1.27  
    1.28  lemma sup_absorb1: "y \<sqsubseteq> x \<Longrightarrow> x \<squnion> y = x"
    1.29 @@ -243,10 +243,10 @@
    1.30    by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    1.31      (unfold_locales, auto)
    1.32  
    1.33 -lemma inf_sup_absorb (*[simp]*): "x \<sqinter> (x \<squnion> y) = x"
    1.34 +lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"
    1.35    by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
    1.36  
    1.37 -lemma sup_inf_absorb (*[simp]*): "x \<squnion> (x \<sqinter> y) = x"
    1.38 +lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"
    1.39    by (blast intro: antisym sup_ge1 sup_least inf_le1)
    1.40  
    1.41  lemmas inf_sup_aci = inf_aci sup_aci
    1.42 @@ -267,8 +267,9 @@
    1.43  assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.44  shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.45  proof-
    1.46 -  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by(simp add:sup_inf_absorb)
    1.47 -  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))" by(simp add:D inf_commute sup_assoc)
    1.48 +  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp
    1.49 +  also have "\<dots> = x \<squnion> (z \<sqinter> (x \<squnion> y))"
    1.50 +    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)
    1.51    also have "\<dots> = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"
    1.52      by(simp add:inf_sup_absorb inf_commute)
    1.53    also have "\<dots> = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)
    1.54 @@ -279,8 +280,9 @@
    1.55  assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
    1.56  shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
    1.57  proof-
    1.58 -  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by(simp add:inf_sup_absorb)
    1.59 -  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))" by(simp add:D sup_commute inf_assoc)
    1.60 +  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp
    1.61 +  also have "\<dots> = x \<sqinter> (z \<squnion> (x \<sqinter> y))"
    1.62 +    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)
    1.63    also have "\<dots> = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"
    1.64      by(simp add:sup_inf_absorb sup_commute)
    1.65    also have "\<dots> = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)
    1.66 @@ -439,11 +441,11 @@
    1.67    by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.68      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    1.69  
    1.70 -lemma compl_inf_bot (*[simp]*):
    1.71 +lemma compl_inf_bot [simp]:
    1.72    "- x \<sqinter> x = \<bottom>"
    1.73    by (simp add: inf_commute inf_compl_bot)
    1.74  
    1.75 -lemma compl_sup_top (*[simp]*):
    1.76 +lemma compl_sup_top [simp]:
    1.77    "- x \<squnion> x = \<top>"
    1.78    by (simp add: sup_commute sup_compl_top)
    1.79  
    1.80 @@ -525,7 +527,7 @@
    1.81    then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)
    1.82  qed
    1.83  
    1.84 -lemma compl_le_compl_iff (*[simp]*):
    1.85 +lemma compl_le_compl_iff [simp]:
    1.86    "- x \<sqsubseteq> - y \<longleftrightarrow> y \<sqsubseteq> x"
    1.87    by (auto dest: compl_mono)
    1.88