src/HOL/Algebra/Lattice.thy

 text {* Introduction rule: the usual definition of total order *}
 
 lemma (in weak_partial_order) weak_total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "weak_total_order L"
-  by default (rule total)
+  by standard (rule total)
 
 text {* Total orders are lattices. *}
 
 sublocale weak_total_order < weak: weak_lattice
 proof

   assumes sup_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "weak_complete_lattice L"
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 definition
   top :: "_ => 'a" ("\<top>\<index>")
   where "\<top>\<^bsub>L\<^esub> = sup L (carrier L)"
 

 locale upper_semilattice = partial_order +
   assumes sup_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
 sublocale upper_semilattice < weak: weak_upper_semilattice
-  by default (rule sup_of_two_exists)
+  by standard (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
 sublocale lower_semilattice < weak: weak_lower_semilattice
-  by default (rule inf_of_two_exists)
+  by standard (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
 
 text {* Supremum *}

 
 locale total_order = partial_order +
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
 sublocale total_order < weak: weak_total_order
-  by default (rule total_order_total)
+  by standard (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
 
 lemma (in partial_order) total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "total_order L"
-  by default (rule total)
+  by standard (rule total)
 
 text {* Total orders are lattices. *}
 
 sublocale total_order < weak: lattice
-  by default (auto intro: sup_of_two_exists inf_of_two_exists)
+  by standard (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
 text {* Complete lattices *}
 
 locale complete_lattice = lattice +

     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
 sublocale complete_lattice < weak: weak_complete_lattice
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
 lemma (in partial_order) complete_latticeI:
   assumes sup_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
-  by default (auto intro: sup_exists inf_exists)
+  by standard (auto intro: sup_exists inf_exists)
 
 theorem (in partial_order) complete_lattice_criterion1:
   assumes top_exists: "EX g. greatest L g (carrier L)"
     and inf_exists:
       "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"

 theorem powerset_is_complete_lattice:
   "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
-    by default auto
+    by standard auto
 next
   fix B
   assume "B \<subseteq> carrier ?L"
   then have "least ?L (\<Union>B) (Upper ?L B)"
     by (fastforce intro!: least_UpperI simp: Upper_def)