tuned proofs;
authorwenzelm
Mon Jul 06 22:57:34 2015 +0200 (2015-07-06)
changeset 60679ade12ef2773c
parent 60678 17ba2df56dee
child 60680 589ed01b94fe
tuned proofs;
src/HOL/Library/Bit.thy
src/HOL/Library/Cardinality.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Countable_Set_Type.thy
src/HOL/Library/DAList.thy
src/HOL/Library/DAList_Multiset.thy
src/HOL/Library/Dlist.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Finite_Lattice.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Function_Algebras.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Lattice_Constructions.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset_Order.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Prefix_Order.thy
src/HOL/Library/Product_Lexorder.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Product_plus.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Library/Saturated.thy
src/HOL/Library/Set_Algebras.thy
src/HOL/Library/Sublist.thy
     1.1 --- a/src/HOL/Library/Bit.thy	Mon Jul 06 22:06:02 2015 +0200
     1.2 +++ b/src/HOL/Library/Bit.thy	Mon Jul 06 22:57:34 2015 +0200
     1.3 @@ -123,8 +123,8 @@
     1.4    plus_bit_def times_bit_def minus_bit_def uminus_bit_def
     1.5    divide_bit_def inverse_bit_def
     1.6  
     1.7 -instance proof
     1.8 -qed (unfold field_bit_defs, auto split: bit.split)
     1.9 +instance
    1.10 +  by standard (auto simp: field_bit_defs split: bit.split)
    1.11  
    1.12  end
    1.13  
     2.1 --- a/src/HOL/Library/Cardinality.thy	Mon Jul 06 22:06:02 2015 +0200
     2.2 +++ b/src/HOL/Library/Cardinality.thy	Mon Jul 06 22:57:34 2015 +0200
     2.3 @@ -228,19 +228,21 @@
     2.4  instantiation natural :: card_UNIV begin
     2.5  definition "finite_UNIV = Phantom(natural) False"
     2.6  definition "card_UNIV = Phantom(natural) 0"
     2.7 -instance proof
     2.8 -qed (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
     2.9 -  type_definition.univ [OF type_definition_natural] natural_eq_iff
    2.10 -  dest!: finite_imageD intro: inj_onI)
    2.11 +instance
    2.12 +  by standard
    2.13 +    (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
    2.14 +      type_definition.univ [OF type_definition_natural] natural_eq_iff
    2.15 +      dest!: finite_imageD intro: inj_onI)
    2.16  end
    2.17  
    2.18  instantiation integer :: card_UNIV begin
    2.19  definition "finite_UNIV = Phantom(integer) False"
    2.20  definition "card_UNIV = Phantom(integer) 0"
    2.21 -instance proof
    2.22 -qed (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
    2.23 -  type_definition.univ [OF type_definition_integer] infinite_UNIV_int
    2.24 -  dest!: finite_imageD intro: inj_onI)
    2.25 +instance
    2.26 +  by standard
    2.27 +    (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
    2.28 +      type_definition.univ [OF type_definition_integer] infinite_UNIV_int
    2.29 +      dest!: finite_imageD intro: inj_onI)
    2.30  end
    2.31  
    2.32  instantiation list :: (type) card_UNIV begin
     3.1 --- a/src/HOL/Library/Char_ord.thy	Mon Jul 06 22:06:02 2015 +0200
     3.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Jul 06 22:57:34 2015 +0200
     3.3 @@ -11,42 +11,33 @@
     3.4  instantiation nibble :: linorder
     3.5  begin
     3.6  
     3.7 -definition
     3.8 -  "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
     3.9 +definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
    3.10 +definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    3.11  
    3.12 -definition
    3.13 -  "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
    3.14 -
    3.15 -instance proof
    3.16 -qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    3.17 +instance
    3.18 +  by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
    3.19  
    3.20  end
    3.21  
    3.22  instantiation nibble :: distrib_lattice
    3.23  begin
    3.24  
    3.25 -definition
    3.26 -  "(inf \<Colon> nibble \<Rightarrow> _) = min"
    3.27 +definition "(inf \<Colon> nibble \<Rightarrow> _) = min"
    3.28 +definition "(sup \<Colon> nibble \<Rightarrow> _) = max"
    3.29  
    3.30 -definition
    3.31 -  "(sup \<Colon> nibble \<Rightarrow> _) = max"
    3.32 -
    3.33 -instance proof
    3.34 -qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    3.35 +instance
    3.36 +  by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
    3.37  
    3.38  end
    3.39  
    3.40  instantiation char :: linorder
    3.41  begin
    3.42  
    3.43 -definition
    3.44 -  "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    3.45 +definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
    3.46 +definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    3.47  
    3.48 -definition
    3.49 -  "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
    3.50 -
    3.51 -instance proof
    3.52 -qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    3.53 +instance
    3.54 +  by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
    3.55  
    3.56  end
    3.57  
    3.58 @@ -83,14 +74,11 @@
    3.59  instantiation char :: distrib_lattice
    3.60  begin
    3.61  
    3.62 -definition
    3.63 -  "(inf \<Colon> char \<Rightarrow> _) = min"
    3.64 +definition "(inf \<Colon> char \<Rightarrow> _) = min"
    3.65 +definition "(sup \<Colon> char \<Rightarrow> _) = max"
    3.66  
    3.67 -definition
    3.68 -  "(sup \<Colon> char \<Rightarrow> _) = max"
    3.69 -
    3.70 -instance proof
    3.71 -qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
    3.72 +instance
    3.73 +  by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
    3.74  
    3.75  end
    3.76  
     4.1 --- a/src/HOL/Library/Countable_Set_Type.thy	Mon Jul 06 22:06:02 2015 +0200
     4.2 +++ b/src/HOL/Library/Countable_Set_Type.thy	Mon Jul 06 22:57:34 2015 +0200
     4.3 @@ -94,7 +94,8 @@
     4.4  lift_definition minus_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
     4.5  is minus parametric Diff_transfer by simp
     4.6  
     4.7 -instance by default(transfer, fastforce)+
     4.8 +instance by standard (transfer; auto)+
     4.9 +
    4.10  end
    4.11  
    4.12  abbreviation cempty :: "'a cset" where "cempty \<equiv> bot"
    4.13 @@ -536,14 +537,15 @@
    4.14  
    4.15  lemma finite_countable_subset:
    4.16  "finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
    4.17 -apply default
    4.18 +apply (rule iffI)
    4.19   apply (erule contrapos_pp)
    4.20   apply (rule card_of_ordLeq_infinite)
    4.21   apply (rule ordLeq_countable_subsets)
    4.22   apply assumption
    4.23  apply (rule finite_Collect_conjI)
    4.24  apply (rule disjI1)
    4.25 -by (erule finite_Collect_subsets)
    4.26 +apply (erule finite_Collect_subsets)
    4.27 +done
    4.28  
    4.29  lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
    4.30    including cset.lifting
     5.1 --- a/src/HOL/Library/DAList.thy	Mon Jul 06 22:06:02 2015 +0200
     5.2 +++ b/src/HOL/Library/DAList.thy	Mon Jul 06 22:57:34 2015 +0200
     5.3 @@ -93,7 +93,7 @@
     5.4  definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
     5.5  
     5.6  instance
     5.7 -  by default (simp add: equal_alist_def impl_of_inject)
     5.8 +  by standard (simp add: equal_alist_def impl_of_inject)
     5.9  
    5.10  end
    5.11  
     6.1 --- a/src/HOL/Library/DAList_Multiset.thy	Mon Jul 06 22:06:02 2015 +0200
     6.2 +++ b/src/HOL/Library/DAList_Multiset.thy	Mon Jul 06 22:57:34 2015 +0200
     6.3 @@ -390,7 +390,7 @@
     6.4  
     6.5  lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
     6.6  proof -
     6.7 -  interpret comp_fun_commute ?f by default auto
     6.8 +  interpret comp_fun_commute ?f by standard auto
     6.9    show ?thesis by (induct A) auto
    6.10  qed
    6.11  
    6.12 @@ -405,7 +405,7 @@
    6.13  
    6.14  lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
    6.15  proof -
    6.16 -  interpret comp_fun_commute ?f by default auto
    6.17 +  interpret comp_fun_commute ?f by standard auto
    6.18    show ?thesis by (induct A) auto
    6.19  qed
    6.20  
     7.1 --- a/src/HOL/Library/Dlist.thy	Mon Jul 06 22:06:02 2015 +0200
     7.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jul 06 22:57:34 2015 +0200
     7.3 @@ -120,15 +120,14 @@
     7.4  
     7.5  definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
     7.6  
     7.7 -instance proof
     7.8 -qed (simp add: equal_dlist_def equal list_of_dlist_inject)
     7.9 +instance
    7.10 +  by standard (simp add: equal_dlist_def equal list_of_dlist_inject)
    7.11  
    7.12  end
    7.13  
    7.14  declare equal_dlist_def [code]
    7.15  
    7.16 -lemma [code nbe]:
    7.17 -  "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
    7.18 +lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
    7.19    by (fact equal_refl)
    7.20  
    7.21  
     8.1 --- a/src/HOL/Library/Extended_Nat.thy	Mon Jul 06 22:06:02 2015 +0200
     8.2 +++ b/src/HOL/Library/Extended_Nat.thy	Mon Jul 06 22:57:34 2015 +0200
     8.3 @@ -34,8 +34,10 @@
     8.4   
     8.5  instantiation enat :: infinity
     8.6  begin
     8.7 -  definition "\<infinity> = Abs_enat None"
     8.8 -  instance proof qed
     8.9 +
    8.10 +definition "\<infinity> = Abs_enat None"
    8.11 +instance ..
    8.12 +
    8.13  end
    8.14  
    8.15  instance enat :: countable
    8.16 @@ -156,7 +158,8 @@
    8.17      and "q + \<infinity> = \<infinity>"
    8.18    by (simp_all add: plus_enat_def split: enat.splits)
    8.19  
    8.20 -instance proof
    8.21 +instance
    8.22 +proof
    8.23    fix n m q :: enat
    8.24    show "n + m + q = n + (m + q)"
    8.25      by (cases n m q rule: enat3_cases) auto
    8.26 @@ -203,7 +206,8 @@
    8.27    unfolding times_enat_def zero_enat_def
    8.28    by (simp_all split: enat.split)
    8.29  
    8.30 -instance proof
    8.31 +instance
    8.32 +proof
    8.33    fix a b c :: enat
    8.34    show "(a * b) * c = a * (b * c)"
    8.35      unfolding times_enat_def zero_enat_def
    8.36 @@ -242,7 +246,8 @@
    8.37    apply (simp add: plus_1_eSuc eSuc_enat)
    8.38    done
    8.39  
    8.40 -instance enat :: semiring_char_0 proof
    8.41 +instance enat :: semiring_char_0
    8.42 +proof
    8.43    have "inj enat" by (rule injI) simp
    8.44    then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
    8.45  qed
    8.46 @@ -355,8 +360,8 @@
    8.47    "(\<infinity>::enat) < q \<longleftrightarrow> False"
    8.48    by simp_all
    8.49  
    8.50 -instance by default
    8.51 -  (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
    8.52 +instance
    8.53 +  by standard (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
    8.54  
    8.55  end
    8.56  
    8.57 @@ -486,14 +491,11 @@
    8.58  instantiation enat :: "{order_bot, order_top}"
    8.59  begin
    8.60  
    8.61 -definition bot_enat :: enat where
    8.62 -  "bot_enat = 0"
    8.63 +definition bot_enat :: enat where "bot_enat = 0"
    8.64 +definition top_enat :: enat where "top_enat = \<infinity>"
    8.65  
    8.66 -definition top_enat :: enat where
    8.67 -  "top_enat = \<infinity>"
    8.68 -
    8.69 -instance proof
    8.70 -qed (simp_all add: bot_enat_def top_enat_def)
    8.71 +instance
    8.72 +  by standard (simp_all add: bot_enat_def top_enat_def)
    8.73  
    8.74  end
    8.75  
    8.76 @@ -502,10 +504,11 @@
    8.77    shows "finite A"
    8.78  proof (rule finite_subset)
    8.79    show "finite (enat ` {..n})" by blast
    8.80 -
    8.81    have "A \<subseteq> {..enat n}" using le_fin by fastforce
    8.82    also have "\<dots> \<subseteq> enat ` {..n}"
    8.83 -    by (rule subsetI) (case_tac x, auto)
    8.84 +    apply (rule subsetI)
    8.85 +    subgoal for x by (cases x) auto
    8.86 +    done
    8.87    finally show "A \<subseteq> enat ` {..n}" .
    8.88  qed
    8.89  
     9.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Jul 06 22:06:02 2015 +0200
     9.2 +++ b/src/HOL/Library/Extended_Real.thy	Mon Jul 06 22:57:34 2015 +0200
     9.3 @@ -257,7 +257,7 @@
     9.4  | "real_ereal \<infinity> = 0"
     9.5  | "real_ereal (-\<infinity>) = 0"
     9.6    by (auto intro: ereal_cases)
     9.7 -termination by default (rule wf_empty)
     9.8 +termination by standard (rule wf_empty)
     9.9  
    9.10  instance ..
    9.11  end
    9.12 @@ -340,7 +340,7 @@
    9.13    with prems show P
    9.14     by (cases rule: ereal2_cases[of a b]) auto
    9.15  qed auto
    9.16 -termination by default (rule wf_empty)
    9.17 +termination by standard (rule wf_empty)
    9.18  
    9.19  lemma Infty_neq_0[simp]:
    9.20    "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
    9.21 @@ -509,7 +509,7 @@
    9.22    using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
    9.23  
    9.24  instance ereal :: dense_linorder
    9.25 -  by default (blast dest: ereal_dense2)
    9.26 +  by standard (blast dest: ereal_dense2)
    9.27  
    9.28  instance ereal :: ordered_ab_semigroup_add
    9.29  proof
    9.30 @@ -848,7 +848,7 @@
    9.31  | "sgn (\<infinity>::ereal) = 1"
    9.32  | "sgn (-\<infinity>::ereal) = -1"
    9.33  by (auto intro: ereal_cases)
    9.34 -termination by default (rule wf_empty)
    9.35 +termination by standard (rule wf_empty)
    9.36  
    9.37  function times_ereal where
    9.38    "ereal r * ereal p = ereal (r * p)"
    9.39 @@ -1602,7 +1602,7 @@
    9.40  
    9.41  definition [simp]: "sup x y = (max x y :: ereal)"
    9.42  definition [simp]: "inf x y = (min x y :: ereal)"
    9.43 -instance by default simp_all
    9.44 +instance by standard simp_all
    9.45  
    9.46  end
    9.47  
    9.48 @@ -1706,7 +1706,7 @@
    9.49    open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
    9.50  
    9.51  instance
    9.52 -  by default (simp add: open_ereal_generated)
    9.53 +  by standard (simp add: open_ereal_generated)
    9.54  
    9.55  end
    9.56  
    10.1 --- a/src/HOL/Library/FSet.thy	Mon Jul 06 22:06:02 2015 +0200
    10.2 +++ b/src/HOL/Library/FSet.thy	Mon Jul 06 22:57:34 2015 +0200
    10.3 @@ -23,7 +23,7 @@
    10.4  (* FIXME transfer and right_total vs. bi_total *)
    10.5  instantiation fset :: (finite) finite
    10.6  begin
    10.7 -instance by default (transfer, simp)
    10.8 +instance by (standard; transfer; simp)
    10.9  end
   10.10  
   10.11  instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
   10.12 @@ -54,7 +54,7 @@
   10.13    by simp
   10.14  
   10.15  instance
   10.16 -by default (transfer, auto)+
   10.17 +  by (standard; transfer; auto)+
   10.18  
   10.19  end
   10.20  
   10.21 @@ -132,9 +132,12 @@
   10.22  instantiation fset :: (finite) complete_lattice 
   10.23  begin
   10.24  
   10.25 -lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer by simp
   10.26 +lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
   10.27 +  by simp
   10.28  
   10.29 -instance by default (transfer, auto)+
   10.30 +instance
   10.31 +  by (standard; transfer; auto)
   10.32 +
   10.33  end
   10.34  
   10.35  instantiation fset :: (finite) complete_boolean_algebra
   10.36 @@ -143,7 +146,8 @@
   10.37  lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus 
   10.38    parametric right_total_Compl_transfer Compl_transfer by simp
   10.39  
   10.40 -instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
   10.41 +instance
   10.42 +  by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
   10.43  
   10.44  end
   10.45  
    11.1 --- a/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:06:02 2015 +0200
    11.2 +++ b/src/HOL/Library/Finite_Lattice.thy	Mon Jul 06 22:57:34 2015 +0200
    11.3 @@ -32,13 +32,13 @@
    11.4    by (auto simp: bot_def intro: Inf_fin.coboundedI)
    11.5  
    11.6  instance finite_lattice_complete \<subseteq> order_bot
    11.7 -  by default (auto simp: finite_lattice_complete_bot_least)
    11.8 +  by standard (auto simp: finite_lattice_complete_bot_least)
    11.9  
   11.10  lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
   11.11    by (auto simp: top_def Sup_fin.coboundedI)
   11.12  
   11.13  instance finite_lattice_complete \<subseteq> order_top
   11.14 -  by default (auto simp: finite_lattice_complete_top_greatest)
   11.15 +  by standard (auto simp: finite_lattice_complete_top_greatest)
   11.16  
   11.17  instance finite_lattice_complete \<subseteq> bounded_lattice ..
   11.18  
   11.19 @@ -124,7 +124,7 @@
   11.20    by (metis Sup_fold_sup finite_code)
   11.21  
   11.22  instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
   11.23 -  by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   11.24 +  by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
   11.25  
   11.26  text \<open>Functions with a finite domain and with a finite lattice as codomain
   11.27  already form a finite lattice.\<close>
   11.28 @@ -146,7 +146,7 @@
   11.29    by (metis Sup_fold_sup finite_code)
   11.30  
   11.31  instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
   11.32 -  by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   11.33 +  by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
   11.34  
   11.35  
   11.36  subsection \<open>Finite Distributive Lattices\<close>
    12.1 --- a/src/HOL/Library/Float.thy	Mon Jul 06 22:06:02 2015 +0200
    12.2 +++ b/src/HOL/Library/Float.thy	Mon Jul 06 22:57:34 2015 +0200
    12.3 @@ -237,8 +237,8 @@
    12.4  where "sup_float a b = max a b"
    12.5  
    12.6  instance
    12.7 -  by default
    12.8 -     (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
    12.9 +  by (standard; transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max)
   12.10 +
   12.11  end
   12.12  
   12.13  lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
    13.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:06:02 2015 +0200
    13.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Jul 06 22:57:34 2015 +0200
    13.3 @@ -218,7 +218,7 @@
    13.4  qed
    13.5  
    13.6  instance fps :: (zero_neq_one) zero_neq_one
    13.7 -  by default (simp add: expand_fps_eq)
    13.8 +  by standard (simp add: expand_fps_eq)
    13.9  
   13.10  instance fps :: (semiring_0) semiring
   13.11  proof
    14.1 --- a/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
    14.2 +++ b/src/HOL/Library/Function_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
    14.3 @@ -62,46 +62,45 @@
    14.4  text \<open>Additive structures\<close>
    14.5  
    14.6  instance "fun" :: (type, semigroup_add) semigroup_add
    14.7 -  by default (simp add: fun_eq_iff add.assoc)
    14.8 +  by standard (simp add: fun_eq_iff add.assoc)
    14.9  
   14.10  instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
   14.11 -  by default (simp_all add: fun_eq_iff)
   14.12 +  by standard (simp_all add: fun_eq_iff)
   14.13  
   14.14  instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
   14.15 -  by default (simp add: fun_eq_iff add.commute)
   14.16 +  by standard (simp add: fun_eq_iff add.commute)
   14.17  
   14.18  instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   14.19 -  by default (simp_all add: fun_eq_iff diff_diff_eq)
   14.20 +  by standard (simp_all add: fun_eq_iff diff_diff_eq)
   14.21  
   14.22  instance "fun" :: (type, monoid_add) monoid_add
   14.23 -  by default (simp_all add: fun_eq_iff)
   14.24 +  by standard (simp_all add: fun_eq_iff)
   14.25  
   14.26  instance "fun" :: (type, comm_monoid_add) comm_monoid_add
   14.27 -  by default simp
   14.28 +  by standard simp
   14.29  
   14.30  instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   14.31  
   14.32  instance "fun" :: (type, group_add) group_add
   14.33 -  by default
   14.34 -    (simp_all add: fun_eq_iff)
   14.35 +  by standard (simp_all add: fun_eq_iff)
   14.36  
   14.37  instance "fun" :: (type, ab_group_add) ab_group_add
   14.38 -  by default simp_all
   14.39 +  by standard simp_all
   14.40  
   14.41  
   14.42  text \<open>Multiplicative structures\<close>
   14.43  
   14.44  instance "fun" :: (type, semigroup_mult) semigroup_mult
   14.45 -  by default (simp add: fun_eq_iff mult.assoc)
   14.46 +  by standard (simp add: fun_eq_iff mult.assoc)
   14.47  
   14.48  instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
   14.49 -  by default (simp add: fun_eq_iff mult.commute)
   14.50 +  by standard (simp add: fun_eq_iff mult.commute)
   14.51  
   14.52  instance "fun" :: (type, monoid_mult) monoid_mult
   14.53 -  by default (simp_all add: fun_eq_iff)
   14.54 +  by standard (simp_all add: fun_eq_iff)
   14.55  
   14.56  instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
   14.57 -  by default simp
   14.58 +  by standard simp
   14.59  
   14.60  
   14.61  text \<open>Misc\<close>
   14.62 @@ -109,19 +108,19 @@
   14.63  instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
   14.64  
   14.65  instance "fun" :: (type, mult_zero) mult_zero
   14.66 -  by default (simp_all add: fun_eq_iff)
   14.67 +  by standard (simp_all add: fun_eq_iff)
   14.68  
   14.69  instance "fun" :: (type, zero_neq_one) zero_neq_one
   14.70 -  by default (simp add: fun_eq_iff)
   14.71 +  by standard (simp add: fun_eq_iff)
   14.72  
   14.73  
   14.74  text \<open>Ring structures\<close>
   14.75  
   14.76  instance "fun" :: (type, semiring) semiring
   14.77 -  by default (simp_all add: fun_eq_iff algebra_simps)
   14.78 +  by standard (simp_all add: fun_eq_iff algebra_simps)
   14.79  
   14.80  instance "fun" :: (type, comm_semiring) comm_semiring
   14.81 -  by default (simp add: fun_eq_iff  algebra_simps)
   14.82 +  by standard (simp add: fun_eq_iff  algebra_simps)
   14.83  
   14.84  instance "fun" :: (type, semiring_0) semiring_0 ..
   14.85  
   14.86 @@ -155,7 +154,7 @@
   14.87  instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
   14.88  
   14.89  instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel 
   14.90 -  by default (auto simp add: times_fun_def algebra_simps)
   14.91 +  by standard (auto simp add: times_fun_def algebra_simps)
   14.92  
   14.93  instance "fun" :: (type, semiring_char_0) semiring_char_0
   14.94  proof
   14.95 @@ -180,23 +179,22 @@
   14.96  text \<open>Ordered structures\<close>
   14.97  
   14.98  instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
   14.99 -  by default (auto simp add: le_fun_def intro: add_left_mono)
  14.100 +  by standard (auto simp add: le_fun_def intro: add_left_mono)
  14.101  
  14.102  instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
  14.103  
  14.104  instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
  14.105 -  by default (simp add: le_fun_def)
  14.106 +  by standard (simp add: le_fun_def)
  14.107  
  14.108  instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
  14.109  
  14.110  instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
  14.111  
  14.112  instance "fun" :: (type, ordered_semiring) ordered_semiring
  14.113 -  by default
  14.114 -    (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
  14.115 +  by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
  14.116  
  14.117  instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
  14.118 -  by default (fact mult_left_mono)
  14.119 +  by standard (fact mult_left_mono)
  14.120  
  14.121  instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
  14.122  
    15.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Jul 06 22:06:02 2015 +0200
    15.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Jul 06 22:57:34 2015 +0200
    15.3 @@ -199,6 +199,7 @@
    15.4    "f differentiable (at x within s) \<Longrightarrow> g differentiable at x within s \<Longrightarrow> (\<lambda>x. inner (f x) (g x)) differentiable at x within s"
    15.5    unfolding differentiable_def by (blast intro: has_derivative_inner)
    15.6  
    15.7 +
    15.8  subsection \<open>Class instances\<close>
    15.9  
   15.10  instantiation real :: real_inner
   15.11 @@ -206,7 +207,8 @@
   15.12  
   15.13  definition inner_real_def [simp]: "inner = op *"
   15.14  
   15.15 -instance proof
   15.16 +instance
   15.17 +proof
   15.18    fix x y z r :: real
   15.19    show "inner x y = inner y x"
   15.20      unfolding inner_real_def by (rule mult.commute)
   15.21 @@ -230,7 +232,8 @@
   15.22  definition inner_complex_def:
   15.23    "inner x y = Re x * Re y + Im x * Im y"
   15.24  
   15.25 -instance proof
   15.26 +instance
   15.27 +proof
   15.28    fix x y z :: complex and r :: real
   15.29    show "inner x y = inner y x"
   15.30      unfolding inner_complex_def by (simp add: mult.commute)
    16.1 --- a/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:06:02 2015 +0200
    16.2 +++ b/src/HOL/Library/Lattice_Constructions.thy	Mon Jul 06 22:57:34 2015 +0200
    16.3 @@ -51,16 +51,16 @@
    16.4    by (simp add: less_bot_def)
    16.5  
    16.6  instance
    16.7 -  by default
    16.8 +  by standard
    16.9      (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
   16.10  
   16.11  end
   16.12  
   16.13  instance bot :: (order) order
   16.14 -  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
   16.15 +  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
   16.16  
   16.17  instance bot :: (linorder) linorder
   16.18 -  by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
   16.19 +  by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
   16.20  
   16.21  instantiation bot :: (order) bot
   16.22  begin
   16.23 @@ -88,7 +88,7 @@
   16.24          | Value v' \<Rightarrow> Value (inf v v')))"
   16.25  
   16.26  instance
   16.27 -  by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
   16.28 +  by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
   16.29  
   16.30  end
   16.31  
   16.32 @@ -106,7 +106,7 @@
   16.33          | Value v' \<Rightarrow> Value (sup v v')))"
   16.34  
   16.35  instance
   16.36 -  by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   16.37 +  by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
   16.38  
   16.39  end
   16.40  
   16.41 @@ -158,16 +158,16 @@
   16.42    by (simp add: less_top_def)
   16.43  
   16.44  instance
   16.45 -  by default
   16.46 +  by standard
   16.47      (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
   16.48  
   16.49  end
   16.50  
   16.51  instance top :: (order) order
   16.52 -  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
   16.53 +  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
   16.54  
   16.55  instance top :: (linorder) linorder
   16.56 -  by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
   16.57 +  by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
   16.58  
   16.59  instantiation top :: (order) top
   16.60  begin
   16.61 @@ -195,7 +195,7 @@
   16.62          | Value v' \<Rightarrow> Value (inf v v')))"
   16.63  
   16.64  instance
   16.65 -  by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   16.66 +  by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
   16.67  
   16.68  end
   16.69  
   16.70 @@ -213,12 +213,12 @@
   16.71          | Value v' \<Rightarrow> Value (sup v v')))"
   16.72  
   16.73  instance
   16.74 -  by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   16.75 +  by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
   16.76  
   16.77  end
   16.78  
   16.79  instance top :: (lattice) bounded_lattice_top
   16.80 -  by default (simp add: top_top_def)
   16.81 +  by standard (simp add: top_top_def)
   16.82  
   16.83  
   16.84  subsection \<open>Values extended by a top and a bottom element\<close>
   16.85 @@ -267,7 +267,7 @@
   16.86    by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
   16.87  
   16.88  instance
   16.89 -  by default
   16.90 +  by standard
   16.91      (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
   16.92        split: flat_complete_lattice.splits)
   16.93  
   16.94 @@ -313,7 +313,7 @@
   16.95      | Top \<Rightarrow> Top)"
   16.96  
   16.97  instance
   16.98 -  by default
   16.99 +  by standard
  16.100      (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
  16.101        less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
  16.102  
    17.1 --- a/src/HOL/Library/List_lexord.thy	Mon Jul 06 22:06:02 2015 +0200
    17.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Jul 06 22:57:34 2015 +0200
    17.3 @@ -74,7 +74,7 @@
    17.4  definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
    17.5  
    17.6  instance
    17.7 -  by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
    17.8 +  by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
    17.9  
   17.10  end
   17.11  
   17.12 @@ -102,7 +102,7 @@
   17.13  definition "bot = []"
   17.14  
   17.15  instance
   17.16 -  by default (simp add: bot_list_def)
   17.17 +  by standard (simp add: bot_list_def)
   17.18  
   17.19  end
   17.20  
    18.1 --- a/src/HOL/Library/Mapping.thy	Mon Jul 06 22:06:02 2015 +0200
    18.2 +++ b/src/HOL/Library/Mapping.thy	Mon Jul 06 22:57:34 2015 +0200
    18.3 @@ -183,8 +183,8 @@
    18.4  definition
    18.5    "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
    18.6  
    18.7 -instance proof
    18.8 -qed (unfold equal_mapping_def, transfer, auto)
    18.9 +instance
   18.10 +  by standard (unfold equal_mapping_def, transfer, auto)
   18.11  
   18.12  end
   18.13  
    19.1 --- a/src/HOL/Library/Multiset_Order.thy	Mon Jul 06 22:06:02 2015 +0200
    19.2 +++ b/src/HOL/Library/Multiset_Order.thy	Mon Jul 06 22:57:34 2015 +0200
    19.3 @@ -62,7 +62,7 @@
    19.4    have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
    19.5      unfolding mult_def by (blast intro: trancl_trans)
    19.6    show "class.order ?le ?less"
    19.7 -    by default (auto simp add: le_multiset_def irrefl dest: trans)
    19.8 +    by standard (auto simp add: le_multiset_def irrefl dest: trans)
    19.9  qed
   19.10  
   19.11  text \<open>The Dershowitz--Manna ordering:\<close>
    20.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:06:02 2015 +0200
    20.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Jul 06 22:57:34 2015 +0200
    20.3 @@ -192,8 +192,8 @@
    20.4  lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
    20.5    by (induct x, induct y) simp
    20.6  
    20.7 -instance proof
    20.8 -qed (simp_all add: num1_eq_iff)
    20.9 +instance
   20.10 +  by standard (simp_all add: num1_eq_iff)
   20.11  
   20.12  end
   20.13  
    21.1 --- a/src/HOL/Library/Option_ord.thy	Mon Jul 06 22:06:02 2015 +0200
    21.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Jul 06 22:57:34 2015 +0200
    21.3 @@ -62,59 +62,61 @@
    21.4  lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
    21.5    by (simp add: less_option_def)
    21.6  
    21.7 -instance proof
    21.8 -qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
    21.9 -
   21.10 -end 
   21.11 +instance
   21.12 +  by standard
   21.13 +    (auto simp add: less_eq_option_def less_option_def less_le_not_le
   21.14 +      elim: order_trans split: option.splits)
   21.15  
   21.16 -instance option :: (order) order proof
   21.17 -qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
   21.18 +end
   21.19  
   21.20 -instance option :: (linorder) linorder proof
   21.21 -qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
   21.22 +instance option :: (order) order
   21.23 +  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
   21.24 +
   21.25 +instance option :: (linorder) linorder
   21.26 +  by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
   21.27  
   21.28  instantiation option :: (order) order_bot
   21.29  begin
   21.30  
   21.31 -definition bot_option where
   21.32 -  "\<bottom> = None"
   21.33 +definition bot_option where "\<bottom> = None"
   21.34  
   21.35 -instance proof
   21.36 -qed (simp add: bot_option_def)
   21.37 +instance
   21.38 +  by standard (simp add: bot_option_def)
   21.39  
   21.40  end
   21.41  
   21.42  instantiation option :: (order_top) order_top
   21.43  begin
   21.44  
   21.45 -definition top_option where
   21.46 -  "\<top> = Some \<top>"
   21.47 +definition top_option where "\<top> = Some \<top>"
   21.48  
   21.49 -instance proof
   21.50 -qed (simp add: top_option_def less_eq_option_def split: option.split)
   21.51 +instance
   21.52 +  by standard (simp add: top_option_def less_eq_option_def split: option.split)
   21.53  
   21.54  end
   21.55  
   21.56 -instance option :: (wellorder) wellorder proof
   21.57 -  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
   21.58 +instance option :: (wellorder) wellorder
   21.59 +proof
   21.60 +  fix P :: "'a option \<Rightarrow> bool"
   21.61 +  fix z :: "'a option"
   21.62    assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   21.63    have "P None" by (rule H) simp
   21.64 -  then have P_Some [case_names Some]:
   21.65 -    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
   21.66 -  proof -
   21.67 -    fix z
   21.68 -    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
   21.69 -    with \<open>P None\<close> show "P z" by (cases z) simp_all
   21.70 -  qed
   21.71 -  show "P z" proof (cases z rule: P_Some)
   21.72 +  then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P o Some) x" for z
   21.73 +    using \<open>P None\<close> that by (cases z) simp_all
   21.74 +  show "P z"
   21.75 +  proof (cases z rule: P_Some)
   21.76      case (Some w)
   21.77 -    show "(P o Some) w" proof (induct rule: less_induct)
   21.78 +    show "(P o Some) w"
   21.79 +    proof (induct rule: less_induct)
   21.80        case (less x)
   21.81 -      have "P (Some x)" proof (rule H)
   21.82 +      have "P (Some x)"
   21.83 +      proof (rule H)
   21.84          fix y :: "'a option"
   21.85          assume "y < Some x"
   21.86 -        show "P y" proof (cases y rule: P_Some)
   21.87 -          case (Some v) with \<open>y < Some x\<close> have "v < x" by simp
   21.88 +        show "P y"
   21.89 +        proof (cases y rule: P_Some)
   21.90 +          case (Some v)
   21.91 +          with \<open>y < Some x\<close> have "v < x" by simp
   21.92            with less show "(P o Some) v" .
   21.93          qed
   21.94        qed
   21.95 @@ -129,16 +131,13 @@
   21.96  definition inf_option where
   21.97    "x \<sqinter> y = (case x of None \<Rightarrow> None | Some x \<Rightarrow> (case y of None \<Rightarrow> None | Some y \<Rightarrow> Some (x \<sqinter> y)))"
   21.98  
   21.99 -lemma inf_None_1 [simp, code]:
  21.100 -  "None \<sqinter> y = None"
  21.101 +lemma inf_None_1 [simp, code]: "None \<sqinter> y = None"
  21.102    by (simp add: inf_option_def)
  21.103  
  21.104 -lemma inf_None_2 [simp, code]:
  21.105 -  "x \<sqinter> None = None"
  21.106 +lemma inf_None_2 [simp, code]: "x \<sqinter> None = None"
  21.107    by (cases x) (simp_all add: inf_option_def)
  21.108  
  21.109 -lemma inf_Some [simp, code]:
  21.110 -  "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
  21.111 +lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
  21.112    by (simp add: inf_option_def)
  21.113  
  21.114  instance ..
  21.115 @@ -151,53 +150,42 @@
  21.116  definition sup_option where
  21.117    "x \<squnion> y = (case x of None \<Rightarrow> y | Some x' \<Rightarrow> (case y of None \<Rightarrow> x | Some y \<Rightarrow> Some (x' \<squnion> y)))"
  21.118  
  21.119 -lemma sup_None_1 [simp, code]:
  21.120 -  "None \<squnion> y = y"
  21.121 +lemma sup_None_1 [simp, code]: "None \<squnion> y = y"
  21.122    by (simp add: sup_option_def)
  21.123  
  21.124 -lemma sup_None_2 [simp, code]:
  21.125 -  "x \<squnion> None = x"
  21.126 +lemma sup_None_2 [simp, code]: "x \<squnion> None = x"
  21.127    by (cases x) (simp_all add: sup_option_def)
  21.128  
  21.129 -lemma sup_Some [simp, code]:
  21.130 -  "Some x \<squnion> Some y = Some (x \<squnion> y)"
  21.131 +lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)"
  21.132    by (simp add: sup_option_def)
  21.133  
  21.134  instance ..
  21.135  
  21.136  end
  21.137  
  21.138 -instantiation option :: (semilattice_inf) semilattice_inf
  21.139 -begin
  21.140 -
  21.141 -instance proof
  21.142 +instance option :: (semilattice_inf) semilattice_inf
  21.143 +proof
  21.144    fix x y z :: "'a option"
  21.145    show "x \<sqinter> y \<le> x"
  21.146 -    by - (cases x, simp_all, cases y, simp_all)
  21.147 +    by (cases x, simp_all, cases y, simp_all)
  21.148    show "x \<sqinter> y \<le> y"
  21.149 -    by - (cases x, simp_all, cases y, simp_all)
  21.150 +    by (cases x, simp_all, cases y, simp_all)
  21.151    show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
  21.152 -    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
  21.153 +    by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
  21.154  qed
  21.155 -  
  21.156 -end
  21.157  
  21.158 -instantiation option :: (semilattice_sup) semilattice_sup
  21.159 -begin
  21.160 -
  21.161 -instance proof
  21.162 +instance option :: (semilattice_sup) semilattice_sup
  21.163 +proof
  21.164    fix x y z :: "'a option"
  21.165    show "x \<le> x \<squnion> y"
  21.166 -    by - (cases x, simp_all, cases y, simp_all)
  21.167 +    by (cases x, simp_all, cases y, simp_all)
  21.168    show "y \<le> x \<squnion> y"
  21.169 -    by - (cases x, simp_all, cases y, simp_all)
  21.170 +    by (cases x, simp_all, cases y, simp_all)
  21.171    fix x y z :: "'a option"
  21.172    show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
  21.173 -    by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
  21.174 +    by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
  21.175  qed
  21.176  
  21.177 -end
  21.178 -
  21.179  instance option :: (lattice) lattice ..
  21.180  
  21.181  instance option :: (lattice) bounded_lattice_bot ..
  21.182 @@ -210,8 +198,8 @@
  21.183  proof
  21.184    fix x y z :: "'a option"
  21.185    show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
  21.186 -    by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
  21.187 -qed 
  21.188 +    by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
  21.189 +qed
  21.190  
  21.191  instantiation option :: (complete_lattice) complete_lattice
  21.192  begin
  21.193 @@ -219,22 +207,20 @@
  21.194  definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
  21.195    "\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
  21.196  
  21.197 -lemma None_in_Inf [simp]:
  21.198 -  "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
  21.199 +lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
  21.200    by (simp add: Inf_option_def)
  21.201  
  21.202  definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
  21.203    "\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
  21.204  
  21.205 -lemma empty_Sup [simp]:
  21.206 -  "\<Squnion>{} = None"
  21.207 +lemma empty_Sup [simp]: "\<Squnion>{} = None"
  21.208    by (simp add: Sup_option_def)
  21.209  
  21.210 -lemma singleton_None_Sup [simp]:
  21.211 -  "\<Squnion>{None} = None"
  21.212 +lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None"
  21.213    by (simp add: Sup_option_def)
  21.214  
  21.215 -instance proof
  21.216 +instance
  21.217 +proof
  21.218    fix x :: "'a option" and A
  21.219    assume "x \<in> A"
  21.220    then show "\<Sqinter>A \<le> x"
  21.221 @@ -274,10 +260,9 @@
  21.222    qed
  21.223  next
  21.224    show "\<Squnion>{} = (\<bottom>::'a option)"
  21.225 -  by (auto simp: bot_option_def)
  21.226 -next
  21.227 +    by (auto simp: bot_option_def)
  21.228    show "\<Sqinter>{} = (\<top>::'a option)"
  21.229 -  by (auto simp: top_option_def Inf_option_def)
  21.230 +    by (auto simp: top_option_def Inf_option_def)
  21.231  qed
  21.232  
  21.233  end
  21.234 @@ -298,10 +283,8 @@
  21.235    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
  21.236    using Some_Sup [of "f ` A"] by (simp add: comp_def)
  21.237  
  21.238 -instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
  21.239 -begin
  21.240 -
  21.241 -instance proof
  21.242 +instance option :: (complete_distrib_lattice) complete_distrib_lattice
  21.243 +proof
  21.244    fix a :: "'a option" and B
  21.245    show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
  21.246    proof (cases a)
  21.247 @@ -354,14 +337,7 @@
  21.248    qed
  21.249  qed
  21.250  
  21.251 -end
  21.252 -
  21.253 -instantiation option :: (complete_linorder) complete_linorder
  21.254 -begin
  21.255 -
  21.256 -instance ..
  21.257 -
  21.258 -end
  21.259 +instance option :: (complete_linorder) complete_linorder ..
  21.260  
  21.261  
  21.262  no_notation
  21.263 @@ -379,4 +355,3 @@
  21.264    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
  21.265  
  21.266  end
  21.267 -
    22.1 --- a/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:06:02 2015 +0200
    22.2 +++ b/src/HOL/Library/Polynomial.thy	Mon Jul 06 22:57:34 2015 +0200
    22.3 @@ -392,13 +392,12 @@
    22.4  definition
    22.5    [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
    22.6  
    22.7 -instance proof
    22.8 -qed (simp add: equal equal_poly_def coeffs_eq_iff)
    22.9 +instance
   22.10 +  by standard (simp add: equal equal_poly_def coeffs_eq_iff)
   22.11  
   22.12  end
   22.13  
   22.14 -lemma [code nbe]:
   22.15 -  "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   22.16 +lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
   22.17    by (fact equal_refl)
   22.18  
   22.19  definition is_zero :: "'a::zero poly \<Rightarrow> bool"
   22.20 @@ -510,15 +509,16 @@
   22.21  lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   22.22    is "\<lambda>p q n. coeff p n + coeff q n"
   22.23  proof -
   22.24 -  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
   22.25 +  fix q p :: "'a poly"
   22.26 +  show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
   22.27      using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   22.28  qed
   22.29  
   22.30 -lemma coeff_add [simp]:
   22.31 -  "coeff (p + q) n = coeff p n + coeff q n"
   22.32 +lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
   22.33    by (simp add: plus_poly.rep_eq)
   22.34  
   22.35 -instance proof
   22.36 +instance
   22.37 +proof
   22.38    fix p q r :: "'a poly"
   22.39    show "(p + q) + r = p + (q + r)"
   22.40      by (simp add: poly_eq_iff add.assoc)
   22.41 @@ -536,15 +536,16 @@
   22.42  lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   22.43    is "\<lambda>p q n. coeff p n - coeff q n"
   22.44  proof -
   22.45 -  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
   22.46 +  fix q p :: "'a poly"
   22.47 +  show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
   22.48      using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
   22.49  qed
   22.50  
   22.51 -lemma coeff_diff [simp]:
   22.52 -  "coeff (p - q) n = coeff p n - coeff q n"
   22.53 +lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
   22.54    by (simp add: minus_poly.rep_eq)
   22.55  
   22.56 -instance proof
   22.57 +instance
   22.58 +proof
   22.59    fix p q r :: "'a poly"
   22.60    show "p + q - p = q"
   22.61      by (simp add: poly_eq_iff)
   22.62 @@ -560,14 +561,16 @@
   22.63  lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   22.64    is "\<lambda>p n. - coeff p n"
   22.65  proof -
   22.66 -  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
   22.67 +  fix p :: "'a poly"
   22.68 +  show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
   22.69      using MOST_coeff_eq_0 by simp
   22.70  qed
   22.71  
   22.72  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
   22.73    by (simp add: uminus_poly.rep_eq)
   22.74  
   22.75 -instance proof
   22.76 +instance
   22.77 +proof
   22.78    fix p q :: "'a poly"
   22.79    show "- p + p = 0"
   22.80      by (simp add: poly_eq_iff)
   22.81 @@ -663,7 +666,8 @@
   22.82    { fix xs ys :: "'a list" and n
   22.83      have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
   22.84      proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
   22.85 -      case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
   22.86 +      case (3 x xs y ys n)
   22.87 +      then show ?case by (cases n) (auto simp add: cCons_def)
   22.88      qed simp_all }
   22.89    note * = this
   22.90    { fix xs ys :: "'a list"
   22.91 @@ -825,7 +829,8 @@
   22.92    shows "(p + q) * r = p * r + q * r"
   22.93    by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
   22.94  
   22.95 -instance proof
   22.96 +instance
   22.97 +proof
   22.98    fix p q r :: "'a poly"
   22.99    show 0: "0 * p = 0"
  22.100      by (rule mult_poly_0_left)
  22.101 @@ -861,18 +866,17 @@
  22.102  done
  22.103  
  22.104  lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
  22.105 -  by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
  22.106 +  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
  22.107  
  22.108  instantiation poly :: (comm_semiring_1) comm_semiring_1
  22.109  begin
  22.110  
  22.111 -definition one_poly_def:
  22.112 -  "1 = pCons 1 0"
  22.113 +definition one_poly_def: "1 = pCons 1 0"
  22.114  
  22.115 -instance proof
  22.116 -  fix p :: "'a poly" show "1 * p = p"
  22.117 +instance
  22.118 +proof
  22.119 +  show "1 * p = p" for p :: "'a poly"
  22.120      unfolding one_poly_def by simp
  22.121 -next
  22.122    show "0 \<noteq> (1::'a poly)"
  22.123      unfolding one_poly_def by simp
  22.124  qed
  22.125 @@ -1063,8 +1067,9 @@
  22.126  definition
  22.127    "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  22.128  
  22.129 -instance proof
  22.130 -  fix x y :: "'a poly"
  22.131 +instance
  22.132 +proof
  22.133 +  fix x y z :: "'a poly"
  22.134    show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
  22.135      unfolding less_eq_poly_def less_poly_def
  22.136      apply safe
  22.137 @@ -1072,50 +1077,34 @@
  22.138      apply (drule (1) pos_poly_add)
  22.139      apply simp
  22.140      done
  22.141 -next
  22.142 -  fix x :: "'a poly" show "x \<le> x"
  22.143 +  show "x \<le> x"
  22.144      unfolding less_eq_poly_def by simp
  22.145 -next
  22.146 -  fix x y z :: "'a poly"
  22.147 -  assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
  22.148 +  show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
  22.149      unfolding less_eq_poly_def
  22.150      apply safe
  22.151      apply (drule (1) pos_poly_add)
  22.152      apply (simp add: algebra_simps)
  22.153      done
  22.154 -next
  22.155 -  fix x y :: "'a poly"
  22.156 -  assume "x \<le> y" and "y \<le> x" thus "x = y"
  22.157 +  show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
  22.158      unfolding less_eq_poly_def
  22.159      apply safe
  22.160      apply (drule (1) pos_poly_add)
  22.161      apply simp
  22.162      done
  22.163 -next
  22.164 -  fix x y z :: "'a poly"
  22.165 -  assume "x \<le> y" thus "z + x \<le> z + y"
  22.166 +  show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
  22.167      unfolding less_eq_poly_def
  22.168      apply safe
  22.169      apply (simp add: algebra_simps)
  22.170      done
  22.171 -next
  22.172 -  fix x y :: "'a poly"
  22.173    show "x \<le> y \<or> y \<le> x"
  22.174      unfolding less_eq_poly_def
  22.175      using pos_poly_total [of "x - y"]
  22.176      by auto
  22.177 -next
  22.178 -  fix x y z :: "'a poly"
  22.179 -  assume "x < y" and "0 < z"
  22.180 -  thus "z * x < z * y"
  22.181 +  show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
  22.182      unfolding less_poly_def
  22.183      by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
  22.184 -next
  22.185 -  fix x :: "'a poly"
  22.186    show "\<bar>x\<bar> = (if x < 0 then - x else x)"
  22.187      by (rule abs_poly_def)
  22.188 -next
  22.189 -  fix x :: "'a poly"
  22.190    show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
  22.191      by (rule sgn_poly_def)
  22.192  qed
  22.193 @@ -1410,7 +1399,8 @@
  22.194      by (simp add: div_poly_eq mod_poly_eq)
  22.195  qed
  22.196  
  22.197 -instance proof
  22.198 +instance
  22.199 +proof
  22.200    fix x y :: "'a poly"
  22.201    show "x div y * y + x mod y = x"
  22.202      using pdivmod_rel [of x y]
    23.1 --- a/src/HOL/Library/Prefix_Order.thy	Mon Jul 06 22:06:02 2015 +0200
    23.2 +++ b/src/HOL/Library/Prefix_Order.thy	Mon Jul 06 22:57:34 2015 +0200
    23.3 @@ -14,7 +14,8 @@
    23.4  definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
    23.5  definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
    23.6  
    23.7 -instance by (default, unfold less_eq_list_def less_list_def) auto
    23.8 +instance
    23.9 +  by standard (auto simp: less_eq_list_def less_list_def)
   23.10  
   23.11  end
   23.12  
    24.1 --- a/src/HOL/Library/Product_Lexorder.thy	Mon Jul 06 22:06:02 2015 +0200
    24.2 +++ b/src/HOL/Library/Product_Lexorder.thy	Mon Jul 06 22:57:34 2015 +0200
    24.3 @@ -37,13 +37,13 @@
    24.4    by (auto simp add: less_prod_def le_less)
    24.5  
    24.6  instance prod :: (preorder, preorder) preorder
    24.7 -  by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
    24.8 +  by standard (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
    24.9  
   24.10  instance prod :: (order, order) order
   24.11 -  by default (auto simp add: less_eq_prod_def)
   24.12 +  by standard (auto simp add: less_eq_prod_def)
   24.13  
   24.14  instance prod :: (linorder, linorder) linorder
   24.15 -  by default (auto simp: less_eq_prod_def)
   24.16 +  by standard (auto simp: less_eq_prod_def)
   24.17  
   24.18  instantiation prod :: (linorder, linorder) distrib_lattice
   24.19  begin
   24.20 @@ -55,7 +55,7 @@
   24.21    "(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
   24.22  
   24.23  instance
   24.24 -  by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
   24.25 +  by standard (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
   24.26  
   24.27  end
   24.28  
   24.29 @@ -70,7 +70,7 @@
   24.30  end
   24.31  
   24.32  instance prod :: (order_bot, order_bot) order_bot
   24.33 -  by default (auto simp add: bot_prod_def)
   24.34 +  by standard (auto simp add: bot_prod_def)
   24.35  
   24.36  instantiation prod :: (top, top) top
   24.37  begin
   24.38 @@ -83,7 +83,7 @@
   24.39  end
   24.40  
   24.41  instance prod :: (order_top, order_top) order_top
   24.42 -  by default (auto simp add: top_prod_def)
   24.43 +  by standard (auto simp add: top_prod_def)
   24.44  
   24.45  instance prod :: (wellorder, wellorder) wellorder
   24.46  proof
    25.1 --- a/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:06:02 2015 +0200
    25.2 +++ b/src/HOL/Library/Product_Order.thy	Mon Jul 06 22:57:34 2015 +0200
    25.3 @@ -49,7 +49,7 @@
    25.4  qed
    25.5  
    25.6  instance prod :: (order, order) order
    25.7 -  by default auto
    25.8 +  by standard auto
    25.9  
   25.10  
   25.11  subsection \<open>Binary infimum and supremum\<close>
   25.12 @@ -57,8 +57,7 @@
   25.13  instantiation prod :: (inf, inf) inf
   25.14  begin
   25.15  
   25.16 -definition
   25.17 -  "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
   25.18 +definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
   25.19  
   25.20  lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
   25.21    unfolding inf_prod_def by simp
   25.22 @@ -69,11 +68,12 @@
   25.23  lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
   25.24    unfolding inf_prod_def by simp
   25.25  
   25.26 -instance proof qed
   25.27 +instance ..
   25.28 +
   25.29  end
   25.30  
   25.31  instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
   25.32 -  by default auto
   25.33 +  by standard auto
   25.34  
   25.35  
   25.36  instantiation prod :: (sup, sup) sup
   25.37 @@ -91,16 +91,17 @@
   25.38  lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
   25.39    unfolding sup_prod_def by simp
   25.40  
   25.41 -instance proof qed
   25.42 +instance ..
   25.43 +
   25.44  end
   25.45  
   25.46  instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
   25.47 -  by default auto
   25.48 +  by standard auto
   25.49  
   25.50  instance prod :: (lattice, lattice) lattice ..
   25.51  
   25.52  instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
   25.53 -  by default (auto simp add: sup_inf_distrib1)
   25.54 +  by standard (auto simp add: sup_inf_distrib1)
   25.55  
   25.56  
   25.57  subsection \<open>Top and bottom elements\<close>
   25.58 @@ -125,7 +126,7 @@
   25.59    unfolding top_prod_def by simp
   25.60  
   25.61  instance prod :: (order_top, order_top) order_top
   25.62 -  by default (auto simp add: top_prod_def)
   25.63 +  by standard (auto simp add: top_prod_def)
   25.64  
   25.65  instantiation prod :: (bot, bot) bot
   25.66  begin
   25.67 @@ -147,12 +148,12 @@
   25.68    unfolding bot_prod_def by simp
   25.69  
   25.70  instance prod :: (order_bot, order_bot) order_bot
   25.71 -  by default (auto simp add: bot_prod_def)
   25.72 +  by standard (auto simp add: bot_prod_def)
   25.73  
   25.74  instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
   25.75  
   25.76  instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
   25.77 -  by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   25.78 +  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
   25.79  
   25.80  
   25.81  subsection \<open>Complete lattice operations\<close>
   25.82 @@ -160,28 +161,28 @@
   25.83  instantiation prod :: (Inf, Inf) Inf
   25.84  begin
   25.85  
   25.86 -definition
   25.87 -  "Inf A = (INF x:A. fst x, INF x:A. snd x)"
   25.88 +definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
   25.89  
   25.90 -instance proof qed
   25.91 +instance ..
   25.92 +
   25.93  end
   25.94  
   25.95  instantiation prod :: (Sup, Sup) Sup
   25.96  begin
   25.97  
   25.98 -definition
   25.99 -  "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
  25.100 +definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
  25.101  
  25.102 -instance proof qed
  25.103 +instance ..
  25.104 +
  25.105  end
  25.106  
  25.107  instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
  25.108      conditionally_complete_lattice
  25.109 -  by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
  25.110 +  by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
  25.111      INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
  25.112  
  25.113  instance prod :: (complete_lattice, complete_lattice) complete_lattice
  25.114 -  by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
  25.115 +  by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
  25.116      INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
  25.117  
  25.118  lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
  25.119 @@ -231,9 +232,8 @@
  25.120  
  25.121  (* Contribution: Alessandro Coglio *)
  25.122  
  25.123 -instance prod ::
  25.124 -  (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
  25.125 -proof (default, goals)
  25.126 +instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
  25.127 +proof (standard, goals)
  25.128    case 1
  25.129    then show ?case
  25.130      by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    26.1 --- a/src/HOL/Library/Product_Vector.thy	Mon Jul 06 22:06:02 2015 +0200
    26.2 +++ b/src/HOL/Library/Product_Vector.thy	Mon Jul 06 22:57:34 2015 +0200
    26.3 @@ -25,7 +25,8 @@
    26.4  lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
    26.5    unfolding scaleR_prod_def by simp
    26.6  
    26.7 -instance proof
    26.8 +instance
    26.9 +proof
   26.10    fix a b :: real and x y :: "'a \<times> 'b"
   26.11    show "scaleR a (x + y) = scaleR a x + scaleR a y"
   26.12      by (simp add: prod_eq_iff scaleR_right_distrib)
   26.13 @@ -58,7 +59,8 @@
   26.14    shows "open S"
   26.15  using assms unfolding open_prod_def by fast
   26.16  
   26.17 -instance proof
   26.18 +instance
   26.19 +proof
   26.20    show "open (UNIV :: ('a \<times> 'b) set)"
   26.21      unfolding open_prod_def by auto
   26.22  next
   26.23 @@ -277,7 +279,8 @@
   26.24  lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
   26.25    unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
   26.26  
   26.27 -instance proof
   26.28 +instance
   26.29 +proof
   26.30    fix x y :: "'a \<times> 'b"
   26.31    show "dist x y = 0 \<longleftrightarrow> x = y"
   26.32      unfolding dist_prod_def prod_eq_iff by simp
   26.33 @@ -406,7 +409,8 @@
   26.34  lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
   26.35    unfolding norm_prod_def by simp
   26.36  
   26.37 -instance proof
   26.38 +instance
   26.39 +proof
   26.40    fix r :: real and x y :: "'a \<times> 'b"
   26.41    show "norm x = 0 \<longleftrightarrow> x = 0"
   26.42      unfolding norm_prod_def
   26.43 @@ -510,7 +514,8 @@
   26.44  lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
   26.45    unfolding inner_prod_def by simp
   26.46  
   26.47 -instance proof
   26.48 +instance
   26.49 +proof
   26.50    fix r :: real
   26.51    fix x y z :: "'a::real_inner \<times> 'b::real_inner"
   26.52    show "inner x y = inner y x"
    27.1 --- a/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:06:02 2015 +0200
    27.2 +++ b/src/HOL/Library/Product_plus.thy	Mon Jul 06 22:57:34 2015 +0200
    27.3 @@ -81,41 +81,56 @@
    27.4  subsection \<open>Class instances\<close>
    27.5  
    27.6  instance prod :: (semigroup_add, semigroup_add) semigroup_add
    27.7 -  by default (simp add: prod_eq_iff add.assoc)
    27.8 +  by standard (simp add: prod_eq_iff add.assoc)
    27.9  
   27.10  instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
   27.11 -  by default (simp add: prod_eq_iff add.commute)
   27.12 +  by standard (simp add: prod_eq_iff add.commute)
   27.13  
   27.14  instance prod :: (monoid_add, monoid_add) monoid_add
   27.15 -  by default (simp_all add: prod_eq_iff)
   27.16 +  by standard (simp_all add: prod_eq_iff)
   27.17  
   27.18  instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
   27.19 -  by default (simp add: prod_eq_iff)
   27.20 +  by standard (simp add: prod_eq_iff)
   27.21  
   27.22 -instance prod ::
   27.23 -  (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   27.24 -    by default (simp_all add: prod_eq_iff)
   27.25 +instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
   27.26 +    by standard (simp_all add: prod_eq_iff)
   27.27  
   27.28 -instance prod ::
   27.29 -  (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   27.30 -    by default (simp_all add: prod_eq_iff diff_diff_eq)
   27.31 +instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
   27.32 +    by standard (simp_all add: prod_eq_iff diff_diff_eq)
   27.33  
   27.34 -instance prod ::
   27.35 -  (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   27.36 +instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
   27.37  
   27.38  instance prod :: (group_add, group_add) group_add
   27.39 -  by default (simp_all add: prod_eq_iff)
   27.40 +  by standard (simp_all add: prod_eq_iff)
   27.41  
   27.42  instance prod :: (ab_group_add, ab_group_add) ab_group_add
   27.43 -  by default (simp_all add: prod_eq_iff)
   27.44 +  by standard (simp_all add: prod_eq_iff)
   27.45  
   27.46  lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
   27.47 -by (cases "finite A", induct set: finite, simp_all)
   27.48 +proof (cases "finite A")
   27.49 +  case True
   27.50 +  then show ?thesis by induct simp_all
   27.51 +next
   27.52 +  case False
   27.53 +  then show ?thesis by simp
   27.54 +qed
   27.55  
   27.56  lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
   27.57 -by (cases "finite A", induct set: finite, simp_all)
   27.58 +proof (cases "finite A")
   27.59 +  case True
   27.60 +  then show ?thesis by induct simp_all
   27.61 +next
   27.62 +  case False
   27.63 +  then show ?thesis by simp
   27.64 +qed
   27.65  
   27.66  lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
   27.67 -by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
   27.68 +proof (cases "finite A")
   27.69 +  case True
   27.70 +  then show ?thesis by induct (simp_all add: zero_prod_def)
   27.71 +next
   27.72 +  case False
   27.73 +  then show ?thesis by (simp add: zero_prod_def)
   27.74 +qed
   27.75  
   27.76  end
    28.1 --- a/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:06:02 2015 +0200
    28.2 +++ b/src/HOL/Library/RBT_Set.thy	Mon Jul 06 22:57:34 2015 +0200
    28.3 @@ -621,14 +621,17 @@
    28.4  lemma image_Set [code]:
    28.5    "image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
    28.6  proof -
    28.7 -  have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
    28.8 -  then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
    28.9 +  have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
   28.10 +    by standard auto
   28.11 +  then show ?thesis
   28.12 +    by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
   28.13  qed
   28.14  
   28.15  lemma Ball_Set [code]:
   28.16    "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   28.17  proof -
   28.18 -  have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   28.19 +  have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
   28.20 +    by standard auto
   28.21    then show ?thesis 
   28.22      by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
   28.23  qed
   28.24 @@ -636,7 +639,8 @@
   28.25  lemma Bex_Set [code]:
   28.26    "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   28.27  proof -
   28.28 -  have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   28.29 +  have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
   28.30 +    by standard auto
   28.31    then show ?thesis 
   28.32      by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
   28.33  qed
   28.34 @@ -670,7 +674,8 @@
   28.35  lemma setsum_Set [code]:
   28.36    "setsum f (Set xs) = fold_keys (plus o f) xs 0"
   28.37  proof -
   28.38 -  have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
   28.39 +  have "comp_fun_commute (\<lambda>x. op + (f x))"
   28.40 +    by standard (auto simp: ac_simps)
   28.41    then show ?thesis 
   28.42      by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
   28.43  qed
   28.44 @@ -695,23 +700,23 @@
   28.45      by(auto split: rbt.split unit.split color.split)
   28.46  qed
   28.47  
   28.48 -lemma Pow_Set [code]:
   28.49 -  "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   28.50 -by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   28.51 +lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
   28.52 +  by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
   28.53  
   28.54  lemma product_Set [code]:
   28.55    "Product_Type.product (Set t1) (Set t2) = 
   28.56      fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
   28.57  proof -
   28.58 -  have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
   28.59 +  have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
   28.60 +    by standard auto
   28.61    show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]  
   28.62      by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
   28.63  qed
   28.64  
   28.65 -lemma Id_on_Set [code]:
   28.66 -  "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   28.67 +lemma Id_on_Set [code]: "Id_on (Set t) =  fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
   28.68  proof -
   28.69 -  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
   28.70 +  have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
   28.71 +    by standard auto
   28.72    then show ?thesis
   28.73      by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
   28.74  qed
   28.75 @@ -728,10 +733,12 @@
   28.76    "(Set t1) O (Set t2) = fold_keys 
   28.77      (\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
   28.78  proof -
   28.79 -  interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
   28.80 +  interpret comp_fun_idem Set.insert
   28.81 +    by (fact comp_fun_idem_insert)
   28.82    have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
   28.83 -    by default (auto simp add: fun_eq_iff)
   28.84 -  show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   28.85 +    by standard (auto simp add: fun_eq_iff)
   28.86 +  show ?thesis
   28.87 +    using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
   28.88      by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
   28.89  qed
   28.90  
   28.91 @@ -759,11 +766,13 @@
   28.92    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   28.93    shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   28.94  proof -
   28.95 -  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   28.96 +  have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
   28.97 +    by standard (simp add: fun_eq_iff ac_simps)
   28.98    then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   28.99      by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
  28.100    then show ?thesis 
  28.101 -    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
  28.102 +    by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
  28.103 +      r_min_eq_r_min_opt[symmetric] r_min_alt_def)
  28.104  qed
  28.105  
  28.106  definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
  28.107 @@ -775,7 +784,7 @@
  28.108    shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
  28.109  proof -
  28.110    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
  28.111 -    by default (auto simp add: fun_eq_iff ac_simps)
  28.112 +    by standard (auto simp add: fun_eq_iff ac_simps)
  28.113    then show ?thesis
  28.114      by (auto simp: INF_fold_inf finite_fold_fold_keys)
  28.115  qed
  28.116 @@ -800,14 +809,17 @@
  28.117    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
  28.118    shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
  28.119  proof -
  28.120 -  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
  28.121 +  have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
  28.122 +    by standard (simp add: fun_eq_iff ac_simps)
  28.123    then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
  28.124      by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
  28.125    then show ?thesis 
  28.126 -    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
  28.127 +    by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
  28.128 +      r_max_eq_r_max_opt[symmetric] r_max_alt_def)
  28.129  qed
  28.130  
  28.131 -definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
  28.132 +definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a"
  28.133 +  where [code del]: "Sup' x = Sup x"
  28.134  declare Sup'_def[symmetric, code_unfold]
  28.135  declare Sup_Set_fold[folded Sup'_def, code]
  28.136  
  28.137 @@ -816,30 +828,34 @@
  28.138    shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
  28.139  proof -
  28.140    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
  28.141 -    by default (auto simp add: fun_eq_iff ac_simps)
  28.142 +    by standard (auto simp add: fun_eq_iff ac_simps)
  28.143    then show ?thesis
  28.144      by (auto simp: SUP_fold_sup finite_fold_fold_keys)
  28.145  qed
  28.146  
  28.147 -lemma sorted_list_set[code]:
  28.148 -  "sorted_list_of_set (Set t) = RBT.keys t"
  28.149 -by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
  28.150 +lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
  28.151 +  by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
  28.152  
  28.153  lemma Bleast_code [code]:
  28.154 - "Bleast (Set t) P = (case filter P (RBT.keys t) of
  28.155 -    x#xs \<Rightarrow> x |
  28.156 -    [] \<Rightarrow> abort_Bleast (Set t) P)"
  28.157 +  "Bleast (Set t) P =
  28.158 +    (case filter P (RBT.keys t) of
  28.159 +      x # xs \<Rightarrow> x
  28.160 +    | [] \<Rightarrow> abort_Bleast (Set t) P)"
  28.161  proof (cases "filter P (RBT.keys t)")
  28.162 -  case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
  28.163 +  case Nil
  28.164 +  thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
  28.165  next
  28.166    case (Cons x ys)
  28.167    have "(LEAST x. x \<in> Set t \<and> P x) = x"
  28.168    proof (rule Least_equality)
  28.169 -    show "x \<in> Set t \<and> P x" using Cons[symmetric]
  28.170 -      by(auto simp add: set_keys Cons_eq_filter_iff)
  28.171 +    show "x \<in> Set t \<and> P x"
  28.172 +      using Cons[symmetric]
  28.173 +      by (auto simp add: set_keys Cons_eq_filter_iff)
  28.174      next
  28.175 -      fix y assume "y : Set t \<and> P y"
  28.176 -      then show "x \<le> y" using Cons[symmetric]
  28.177 +      fix y
  28.178 +      assume "y \<in> Set t \<and> P y"
  28.179 +      then show "x \<le> y"
  28.180 +        using Cons[symmetric]
  28.181          by(auto simp add: set_keys Cons_eq_filter_iff)
  28.182            (metis sorted_Cons sorted_append sorted_keys)
  28.183    qed
    29.1 --- a/src/HOL/Library/Saturated.thy	Mon Jul 06 22:06:02 2015 +0200
    29.2 +++ b/src/HOL/Library/Saturated.thy	Mon Jul 06 22:57:34 2015 +0200
    29.3 @@ -61,7 +61,8 @@
    29.4    less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
    29.5  
    29.6  instance
    29.7 -by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
    29.8 +  by standard
    29.9 +    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
   29.10  
   29.11  end
   29.12  
   29.13 @@ -106,8 +107,9 @@
   29.14    "nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
   29.15    by (simp add: times_sat_def)
   29.16  
   29.17 -instance proof
   29.18 -  fix a b c :: "('a::len) sat"
   29.19 +instance
   29.20 +proof
   29.21 +  fix a b c :: "'a::len sat"
   29.22    show "a * b * c = a * (b * c)"
   29.23    proof(cases "a = 0")
   29.24      case True thus ?thesis by (simp add: sat_eq_iff)
   29.25 @@ -120,14 +122,10 @@
   29.26          by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
   29.27      qed
   29.28    qed
   29.29 -next
   29.30 -  fix a :: "('a::len) sat"
   29.31    show "1 * a = a"
   29.32      apply (simp add: sat_eq_iff)
   29.33      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)
   29.34      done
   29.35 -next
   29.36 -  fix a b c :: "('a::len) sat"
   29.37    show "(a + b) * c = a * c + b * c"
   29.38    proof(cases "c = 0")
   29.39      case True thus ?thesis by (simp add: sat_eq_iff)
   29.40 @@ -143,7 +141,8 @@
   29.41  begin
   29.42  
   29.43  instance
   29.44 -by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
   29.45 +  by standard
   29.46 +    (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
   29.47  
   29.48  end
   29.49  
   29.50 @@ -183,43 +182,33 @@
   29.51  instantiation sat :: (len) equal
   29.52  begin
   29.53  
   29.54 -definition
   29.55 -  "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
   29.56 +definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
   29.57  
   29.58 -instance proof
   29.59 -qed (simp add: equal_sat_def nat_of_inject)
   29.60 +instance
   29.61 +  by standard (simp add: equal_sat_def nat_of_inject)
   29.62  
   29.63  end
   29.64  
   29.65  instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
   29.66  begin
   29.67  
   29.68 -definition
   29.69 -  "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
   29.70 -
   29.71 -definition
   29.72 -  "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
   29.73 +definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
   29.74 +definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
   29.75 +definition "bot = (0 :: 'a sat)"
   29.76 +definition "top = Sat (len_of TYPE('a))"
   29.77  
   29.78 -definition
   29.79 -  "bot = (0 :: 'a sat)"
   29.80 -
   29.81 -definition
   29.82 -  "top = Sat (len_of TYPE('a))"
   29.83 -
   29.84 -instance proof
   29.85 -qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
   29.86 -  simp_all add: less_eq_sat_def)
   29.87 +instance
   29.88 +  by standard
   29.89 +    (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
   29.90 +      simp_all add: less_eq_sat_def)
   29.91  
   29.92  end
   29.93  
   29.94  instantiation sat :: (len) "{Inf, Sup}"
   29.95  begin
   29.96  
   29.97 -definition
   29.98 -  "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
   29.99 -
  29.100 -definition
  29.101 -  "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
  29.102 +definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
  29.103 +definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
  29.104  
  29.105  instance ..
  29.106  
  29.107 @@ -229,16 +218,20 @@
  29.108  where
  29.109    "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
  29.110  proof -
  29.111 -  show "semilattice_neutr_set min (top :: 'a sat)" by default (simp add: min_def)
  29.112 -  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" by (simp add: Inf_sat_def)
  29.113 +  show "semilattice_neutr_set min (top :: 'a sat)"
  29.114 +    by standard (simp add: min_def)
  29.115 +  show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
  29.116 +    by (simp add: Inf_sat_def)
  29.117  qed
  29.118  
  29.119  interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
  29.120  where
  29.121    "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
  29.122  proof -
  29.123 -  show "semilattice_neutr_set max (bot :: 'a sat)" by default (simp add: max_def bot.extremum_unique)
  29.124 -  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" by (simp add: Sup_sat_def)
  29.125 +  show "semilattice_neutr_set max (bot :: 'a sat)"
  29.126 +    by standard (simp add: max_def bot.extremum_unique)
  29.127 +  show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
  29.128 +    by (simp add: Sup_sat_def)
  29.129  qed
  29.130  
  29.131  instance sat :: (len) complete_lattice
  29.132 @@ -271,10 +264,8 @@
  29.133  next
  29.134    show "Inf {} = (top::'a sat)"
  29.135      by (auto simp: top_sat_def)
  29.136 -next
  29.137    show "Sup {} = (bot::'a sat)"
  29.138      by (auto simp: bot_sat_def)
  29.139  qed
  29.140  
  29.141  end
  29.142 -
    30.1 --- a/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:06:02 2015 +0200
    30.2 +++ b/src/HOL/Library/Set_Algebras.thy	Mon Jul 06 22:57:34 2015 +0200
    30.3 @@ -64,28 +64,28 @@
    30.4    "x =o A \<equiv> x \<in> A"
    30.5  
    30.6  instance set :: (semigroup_add) semigroup_add
    30.7 -  by default (force simp add: set_plus_def add.assoc)
    30.8 +  by standard (force simp add: set_plus_def add.assoc)
    30.9  
   30.10  instance set :: (ab_semigroup_add) ab_semigroup_add
   30.11 -  by default (force simp add: set_plus_def add.commute)
   30.12 +  by standard (force simp add: set_plus_def add.commute)
   30.13  
   30.14  instance set :: (monoid_add) monoid_add
   30.15 -  by default (simp_all add: set_plus_def)
   30.16 +  by standard (simp_all add: set_plus_def)
   30.17  
   30.18  instance set :: (comm_monoid_add) comm_monoid_add
   30.19 -  by default (simp_all add: set_plus_def)
   30.20 +  by standard (simp_all add: set_plus_def)
   30.21  
   30.22  instance set :: (semigroup_mult) semigroup_mult
   30.23 -  by default (force simp add: set_times_def mult.assoc)
   30.24 +  by standard (force simp add: set_times_def mult.assoc)
   30.25  
   30.26  instance set :: (ab_semigroup_mult) ab_semigroup_mult
   30.27 -  by default (force simp add: set_times_def mult.commute)
   30.28 +  by standard (force simp add: set_times_def mult.commute)
   30.29  
   30.30  instance set :: (monoid_mult) monoid_mult
   30.31 -  by default (simp_all add: set_times_def)
   30.32 +  by standard (simp_all add: set_times_def)
   30.33  
   30.34  instance set :: (comm_monoid_mult) comm_monoid_mult
   30.35 -  by default (simp_all add: set_times_def)
   30.36 +  by standard (simp_all add: set_times_def)
   30.37  
   30.38  lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
   30.39    by (auto simp add: set_plus_def)
    31.1 --- a/src/HOL/Library/Sublist.thy	Mon Jul 06 22:06:02 2015 +0200
    31.2 +++ b/src/HOL/Library/Sublist.thy	Mon Jul 06 22:57:34 2015 +0200
    31.3 @@ -18,10 +18,10 @@
    31.4    where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
    31.5  
    31.6  interpretation prefix_order: order prefixeq prefix
    31.7 -  by default (auto simp: prefixeq_def prefix_def)
    31.8 +  by standard (auto simp: prefixeq_def prefix_def)
    31.9  
   31.10  interpretation prefix_bot: order_bot Nil prefixeq prefix
   31.11 -  by default (simp add: prefixeq_def)
   31.12 +  by standard (simp add: prefixeq_def)
   31.13  
   31.14  lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
   31.15    unfolding prefixeq_def by blast