src/HOL/Lattices.thy
changeset 36635 080b755377c0
parent 36352 f71978e47cd5
child 36673 6d25e8dab1e3
     1.1 --- a/src/HOL/Lattices.thy	Tue May 04 08:55:39 2010 +0200
     1.2 +++ b/src/HOL/Lattices.thy	Tue May 04 08:55:43 2010 +0200
     1.3 @@ -67,8 +67,8 @@
     1.4  text {* Dual lattice *}
     1.5  
     1.6  lemma dual_semilattice:
     1.7 -  "semilattice_inf (op \<ge>) (op >) sup"
     1.8 -by (rule semilattice_inf.intro, rule dual_order)
     1.9 +  "class.semilattice_inf (op \<ge>) (op >) sup"
    1.10 +by (rule class.semilattice_inf.intro, rule dual_order)
    1.11    (unfold_locales, simp_all add: sup_least)
    1.12  
    1.13  end
    1.14 @@ -235,8 +235,8 @@
    1.15  begin
    1.16  
    1.17  lemma dual_lattice:
    1.18 -  "lattice (op \<ge>) (op >) sup inf"
    1.19 -  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
    1.20 +  "class.lattice (op \<ge>) (op >) sup inf"
    1.21 +  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
    1.22      (unfold_locales, auto)
    1.23  
    1.24  lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
    1.25 @@ -347,8 +347,8 @@
    1.26  by(simp add: inf_sup_aci inf_sup_distrib1)
    1.27  
    1.28  lemma dual_distrib_lattice:
    1.29 -  "distrib_lattice (op \<ge>) (op >) sup inf"
    1.30 -  by (rule distrib_lattice.intro, rule dual_lattice)
    1.31 +  "class.distrib_lattice (op \<ge>) (op >) sup inf"
    1.32 +  by (rule class.distrib_lattice.intro, rule dual_lattice)
    1.33      (unfold_locales, fact inf_sup_distrib1)
    1.34  
    1.35  lemmas sup_inf_distrib =
    1.36 @@ -419,7 +419,7 @@
    1.37  begin
    1.38  
    1.39  lemma dual_bounded_lattice:
    1.40 -  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.41 +  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.42    by unfold_locales (auto simp add: less_le_not_le)
    1.43  
    1.44  end
    1.45 @@ -431,8 +431,8 @@
    1.46  begin
    1.47  
    1.48  lemma dual_boolean_algebra:
    1.49 -  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.50 -  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.51 +  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
    1.52 +  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
    1.53      (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
    1.54  
    1.55  lemma compl_inf_bot: