src/HOL/Lattices.thy

 begin
 
 text {* Dual lattice *}
 
 lemma dual_semilattice:
-  "semilattice_inf (op \<ge>) (op >) sup"
-by (rule semilattice_inf.intro, rule dual_order)
+  "class.semilattice_inf (op \<ge>) (op >) sup"
+by (rule class.semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
 
 end
 
 class lattice = semilattice_inf + semilattice_sup

 
 context lattice
 begin
 
 lemma dual_lattice:
-  "lattice (op \<ge>) (op >) sup inf"
-  by (rule lattice.intro, rule dual_semilattice, rule semilattice_sup.intro, rule dual_order)
+  "class.lattice (op \<ge>) (op >) sup inf"
+  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
 lemma inf_sup_absorb: "x \<sqinter> (x \<squnion> y) = x"
   by (blast intro: antisym inf_le1 inf_greatest sup_ge1)
 

 lemma inf_sup_distrib2:
  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"
 by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
-  "distrib_lattice (op \<ge>) (op >) sup inf"
-  by (rule distrib_lattice.intro, rule dual_lattice)
+  "class.distrib_lattice (op \<ge>) (op >) sup inf"
+  by (rule class.distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
 lemmas sup_inf_distrib =
   sup_inf_distrib1 sup_inf_distrib2
 

 
 class bounded_lattice = bounded_lattice_bot + bounded_lattice_top
 begin
 
 lemma dual_bounded_lattice:
-  "bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  "class.bounded_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
 
 end
 
 class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +

     and sup_compl_top: "x \<squnion> - x = \<top>"
   assumes diff_eq: "x - y = x \<sqinter> - y"
 begin
 
 lemma dual_boolean_algebra:
-  "boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
-  by (rule boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
+  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
+  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
 lemma compl_inf_bot:
   "- x \<sqinter> x = \<bottom>"
   by (simp add: inf_commute inf_compl_bot)