src/HOL/Library/Saturated.thy

--- a/src/HOL/Library/Saturated.thy	Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Saturated.thy	Mon Jul 06 22:57:34 2015 +0200
@@ -61,7 +61,8 @@
   less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+  by standard
+    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
 
 end
 
@@ -106,8 +107,9 @@
   "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
   by (simp add: times_sat_def)
 
-instance proof
-  fix a b c :: "('a::len) sat"
+instance
+proof
+  fix a b c :: "'a::len sat"
   show "a * b * c = a * (b * c)"
   proof(cases "a = 0")
     case True thus ?thesis by (simp add: sat_eq_iff)
@@ -120,14 +122,10 @@
         by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
     qed
   qed
-next
-  fix a :: "('a::len) sat"
   show "1 * a = a"
     apply (simp add: sat_eq_iff)
     apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute)
     done
-next
-  fix a b c :: "('a::len) sat"
   show "(a + b) * c = a * c + b * c"
   proof(cases "c = 0")
     case True thus ?thesis by (simp add: sat_eq_iff)
@@ -143,7 +141,8 @@
 begin
 
 instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+  by standard
+    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
 
 end
 
@@ -183,43 +182,33 @@
 instantiation sat :: (len) equal
 begin
 
-definition
-  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
+definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
 
-instance proof
-qed (simp add: equal_sat_def nat_of_inject)
+instance
+  by standard (simp add: equal_sat_def nat_of_inject)
 
 end
 
 instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
 begin
 
-definition
-  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
-
-definition
-  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
+definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "bot = (0 :: 'a sat)"
+definition "top = Sat (len_of TYPE('a))"
 
-definition
-  "bot = (0 :: 'a sat)"
-
-definition
-  "top = Sat (len_of TYPE('a))"
-
-instance proof
-qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
-  simp_all add: less_eq_sat_def)
+instance
+  by standard
+    (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
+      simp_all add: less_eq_sat_def)
 
 end
 
 instantiation sat :: (len) "{Inf, Sup}"
 begin
 
-definition
-  "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
-
-definition
-  "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
 
 instance ..
 
@@ -229,16 +218,20 @@
 where
   "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
 proof -
-  show "semilattice_neutr_set min (top :: 'a sat)" by default (simp add: min_def)
-  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" by (simp add: Inf_sat_def)
+  show "semilattice_neutr_set min (top :: 'a sat)"
+    by standard (simp add: min_def)
+  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
+    by (simp add: Inf_sat_def)
 qed
 
 interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
 where
   "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
 proof -
-  show "semilattice_neutr_set max (bot :: 'a sat)" by default (simp add: max_def bot.extremum_unique)
-  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" by (simp add: Sup_sat_def)
+  show "semilattice_neutr_set max (bot :: 'a sat)"
+    by standard (simp add: max_def bot.extremum_unique)
+  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
+    by (simp add: Sup_sat_def)
 qed
 
 instance sat :: (len) complete_lattice
@@ -271,10 +264,8 @@
 next
   show "Inf {} = (top::'a sat)"
     by (auto simp: top_sat_def)
-next
   show "Sup {} = (bot::'a sat)"
     by (auto simp: bot_sat_def)
 qed
 
 end
-