# HG changeset patch # User wenzelm # Date 1442177812 -7200 # Node ID 4de9ff3ea29a607b80101439885c5fd556fda6b2 # Parent dcdfb6355a056c357af9a6d0b413b10648062395 tuned proofs -- less legacy; diff -r dcdfb6355a05 -r 4de9ff3ea29a src/Doc/Codegen/Adaptation.thy --- a/src/Doc/Codegen/Adaptation.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/Doc/Codegen/Adaptation.thy Sun Sep 13 22:56:52 2015 +0200 @@ -346,7 +346,7 @@ definition %quote "HOL.equal (x::bar) y \ x = y" -instance %quote by default (simp add: equal_bar_def) +instance %quote by standard (simp add: equal_bar_def) end %quote (*<*) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/AbelCoset.thy --- a/src/HOL/Algebra/AbelCoset.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/AbelCoset.thy Sun Sep 13 22:56:52 2015 +0200 @@ -236,7 +236,7 @@ by (rule a_normal) show "abelian_subgroup H G" - by default (simp add: a_comm) + by standard (simp add: a_comm) qed lemma abelian_subgroupI2: diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/Divisibility.thy --- a/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/Divisibility.thy Sun Sep 13 22:56:52 2015 +0200 @@ -25,14 +25,14 @@ and r_cancel: "\a b c. \a \ c = b \ c; a \ carrier G; b \ carrier G; c \ carrier G\ \ a = b" shows "monoid_cancel G" - by default fact+ + by standard fact+ lemma (in monoid_cancel) is_monoid_cancel: "monoid_cancel G" .. sublocale group \ monoid_cancel - by default simp_all + by standard simp_all locale comm_monoid_cancel = monoid_cancel + comm_monoid @@ -3640,7 +3640,7 @@ done sublocale factorial_monoid \ primeness_condition_monoid - by default (rule irreducible_is_prime) + by standard (rule irreducible_is_prime) lemma (in factorial_monoid) primeness_condition: @@ -3649,10 +3649,10 @@ lemma (in factorial_monoid) gcd_condition [simp]: shows "gcd_condition_monoid G" - by default (rule gcdof_exists) + by standard (rule gcdof_exists) sublocale factorial_monoid \ gcd_condition_monoid - by default (rule gcdof_exists) + by standard (rule gcdof_exists) lemma (in factorial_monoid) division_weak_lattice [simp]: shows "weak_lattice (division_rel G)" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/Group.thy --- a/src/HOL/Algebra/Group.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/Group.thy Sun Sep 13 22:56:52 2015 +0200 @@ -286,7 +286,8 @@ qed then have carrier_subset_Units: "carrier G <= Units G" by (unfold Units_def) fast - show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units) + show ?thesis + by standard (auto simp: r_one m_assoc carrier_subset_Units) qed lemma (in monoid) group_l_invI: @@ -730,7 +731,7 @@ assumes m_comm: "!!x y. [| x \ carrier G; y \ carrier G |] ==> x \ y = y \ x" shows "comm_group G" - by default (simp_all add: m_comm) + by standard (simp_all add: m_comm) lemma comm_groupI: fixes G (structure) @@ -758,7 +759,7 @@ theorem (in group) subgroups_partial_order: "partial_order \carrier = {H. subgroup H G}, eq = op =, le = op \\" - by default simp_all + by standard simp_all lemma (in group) subgroup_self: "subgroup (carrier G) G" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/IntRing.thy Sun Sep 13 22:56:52 2015 +0200 @@ -60,7 +60,7 @@ and "pow \ x n = x^n" proof - -- "Specification" - show "monoid \" by default auto + show "monoid \" by standard auto then interpret int: monoid \ . -- "Carrier" @@ -76,7 +76,7 @@ where "finprod \ f A = setprod f A" proof - -- "Specification" - show "comm_monoid \" by default auto + show "comm_monoid \" by standard auto then interpret int: comm_monoid \ . -- "Operations" @@ -94,7 +94,7 @@ and int_finsum_eq: "finsum \ f A = setsum f A" proof - -- "Specification" - show "abelian_monoid \" by default auto + show "abelian_monoid \" by standard auto then interpret int: abelian_monoid \ . -- "Carrier" @@ -178,7 +178,7 @@ and "lless \carrier = UNIV::int set, eq = op =, le = op \\ x y = (x < y)" proof - show "partial_order \carrier = UNIV::int set, eq = op =, le = op \\" - by default simp_all + by standard simp_all show "carrier \carrier = UNIV::int set, eq = op =, le = op \\ = UNIV" by simp show "le \carrier = UNIV::int set, eq = op =, le = op \\ x y = (x \ y)" @@ -215,7 +215,7 @@ interpretation int (* [unfolded UNIV] *) : total_order "\carrier = UNIV::int set, eq = op =, le = op \\" - by default clarsimp + by standard clarsimp subsection {* Generated Ideals of @{text "\"} *} diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/Lattice.thy --- a/src/HOL/Algebra/Lattice.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/Lattice.thy Sun Sep 13 22:56:52 2015 +0200 @@ -921,7 +921,7 @@ lemma (in weak_partial_order) weak_total_orderI: assumes total: "!!x y. [| x \ carrier L; y \ carrier L |] ==> x \ y | y \ x" shows "weak_total_order L" - by default (rule total) + by standard (rule total) text {* Total orders are lattices. *} @@ -985,7 +985,7 @@ and inf_exists: "!!A. [| A \ 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" ("\\") @@ -1133,14 +1133,14 @@ "[| x \ carrier L; y \ 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 \ carrier L; y \ 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 @@ -1191,19 +1191,19 @@ assumes total_order_total: "[| x \ carrier L; y \ carrier L |] ==> x \ y | y \ 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 \ carrier L; y \ carrier L |] ==> x \ y | y \ 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 *} @@ -1215,7 +1215,7 @@ "[| A \ 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 *} @@ -1225,7 +1225,7 @@ and inf_exists: "!!A. [| A \ 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)" @@ -1282,7 +1282,7 @@ (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 \ carrier ?L" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/RingHom.thy --- a/src/HOL/Algebra/RingHom.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/RingHom.thy Sun Sep 13 22:56:52 2015 +0200 @@ -17,7 +17,7 @@ and hom_one [simp] = ring_hom_one [OF homh] sublocale ring_hom_cring \ ring: ring_hom_ring - by default (rule homh) + by standard (rule homh) sublocale ring_hom_ring \ abelian_group: abelian_group_hom R S apply (rule abelian_group_homI) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/UnivPoly.thy --- a/src/HOL/Algebra/UnivPoly.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Algebra/UnivPoly.thy Sun Sep 13 22:56:52 2015 +0200 @@ -1760,7 +1760,7 @@ and deg_r_0: "deg R r = 0" shows "r = monom P (eval R R id a f) 0" proof - - interpret UP_pre_univ_prop R R id P by default simp + interpret UP_pre_univ_prop R R id P by standard simp have eval_ring_hom: "eval R R id a \ ring_hom P R" using eval_ring_hom [OF a] by simp have "eval R R id a f = eval R R id a ?gq \\<^bsub>R\<^esub> eval R R id a r" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Sun Sep 13 22:56:52 2015 +0200 @@ -15,10 +15,10 @@ begin lemma False_imp_eq_True: "(False \ Q) \ Trueprop True" - by default simp_all + by standard simp_all lemma conj_imp_eq_imp_imp: "(P \ Q \ PROP R) \ (P \ Q \ PROP R)" - by default simp_all + by standard simp_all lemma mp_conj: "(P \ Q) \ R \ P \ R \ Q" by auto diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Basic_BNF_LFPs.thy --- a/src/HOL/Basic_BNF_LFPs.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Basic_BNF_LFPs.thy Sun Sep 13 22:56:52 2015 +0200 @@ -30,7 +30,7 @@ lemmas xtor_inject = xtor_rel[of "op ="] lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" - unfolding xtor_def vimage2p_def id_bnf_def by default + unfolding xtor_def vimage2p_def id_bnf_def .. lemma Inl_def_alt: "Inl \ (\a. xtor (id_bnf (Inl a)))" unfolding xtor_def id_bnf_def by (rule reflexive) @@ -60,10 +60,10 @@ by (cases p) auto lemma ex_neg_all_pos: "((\x. P x) \ Q) \ (\x. P x \ Q)" - by default blast+ + by standard blast+ lemma hypsubst_in_prems: "(\x. y = x \ z = f x \ P) \ (z = f y \ P)" - by default blast+ + by standard blast+ lemma isl_map_sum: "isl (map_sum f g s) = isl s" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Complete_Partial_Order.thy --- a/src/HOL/Complete_Partial_Order.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Complete_Partial_Order.thy Sun Sep 13 22:56:52 2015 +0200 @@ -293,7 +293,7 @@ end instance complete_lattice \ ccpo - by default (fast intro: Sup_upper Sup_least)+ + by standard (fast intro: Sup_upper Sup_least)+ lemma lfp_eq_fixp: assumes f: "mono f" shows "lfp f = fixp f" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Conditionally_Complete_Lattices.thy --- a/src/HOL/Conditionally_Complete_Lattices.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Conditionally_Complete_Lattices.thy Sun Sep 13 22:56:52 2015 +0200 @@ -371,7 +371,7 @@ end instance complete_lattice \ conditionally_complete_lattice - by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) + by standard (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest) lemma cSup_eq: fixes a :: "'a :: {conditionally_complete_lattice, no_bot}" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Enum.thy --- a/src/HOL/Enum.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Enum.thy Sun Sep 13 22:56:52 2015 +0200 @@ -446,9 +446,10 @@ "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))" -instance by default - (simp_all add: enum_prod_def distinct_product - enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def) +instance + by standard + (simp_all add: enum_prod_def distinct_product + enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Finite_Set.thy Sun Sep 13 22:56:52 2015 +0200 @@ -573,7 +573,7 @@ end instance prod :: (finite, finite) finite - by default (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) + by standard (simp only: UNIV_Times_UNIV [symmetric] finite_cartesian_product finite) lemma inj_graph: "inj (%f. {(x, y). y = f x})" by (rule inj_onI, auto simp add: set_eq_iff fun_eq_iff) @@ -593,16 +593,16 @@ qed instance bool :: finite - by default (simp add: UNIV_bool) + by standard (simp add: UNIV_bool) instance set :: (finite) finite - by default (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) + by standard (simp only: Pow_UNIV [symmetric] finite_Pow_iff finite) instance unit :: finite - by default (simp add: UNIV_unit) + by standard (simp add: UNIV_unit) instance sum :: (finite, finite) finite - by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) + by standard (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite) subsection \A basic fold functional for finite sets\ @@ -967,7 +967,7 @@ "comp_fun_commute (\x A'. if P x then Set.insert x A' else A')" proof - interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) - show ?thesis by default (auto simp: fun_eq_iff) + show ?thesis by standard (auto simp: fun_eq_iff) qed lemma Set_filter_fold: @@ -988,7 +988,7 @@ shows "image f A = fold (\k A. Set.insert (f k) A) {} A" using assms proof - - interpret comp_fun_commute "\k A. Set.insert (f k) A" by default auto + interpret comp_fun_commute "\k A. Set.insert (f k) A" by standard auto show ?thesis using assms by (induct A) auto qed @@ -997,7 +997,7 @@ shows "Ball A P = fold (\k s. s \ P k) True A" using assms proof - - interpret comp_fun_commute "\k s. s \ P k" by default auto + interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed @@ -1006,7 +1006,7 @@ shows "Bex A P = fold (\k s. s \ P k) False A" using assms proof - - interpret comp_fun_commute "\k s. s \ P k" by default auto + interpret comp_fun_commute "\k s. s \ P k" by standard auto show ?thesis using assms by (induct A) auto qed @@ -1027,14 +1027,14 @@ assumes "finite B" shows "(\y\B. {(x, y)}) \ A = fold (\y. Set.insert (x, y)) A B" proof - - interpret comp_fun_commute "\y. Set.insert (x, y)" by default auto + interpret comp_fun_commute "\y. Set.insert (x, y)" by standard auto show ?thesis using assms by (induct B arbitrary: A) simp_all qed lemma comp_fun_commute_product_fold: assumes "finite B" shows "comp_fun_commute (\x z. fold (\y. Set.insert (x, y)) z B)" -by default (auto simp: fold_union_pair[symmetric] assms) + by standard (auto simp: fold_union_pair[symmetric] assms) lemma product_fold: assumes "finite A" @@ -1122,18 +1122,16 @@ begin interpretation fold?: comp_fun_commute f - by default (insert comp_fun_commute, simp add: fun_eq_iff) + by standard (insert comp_fun_commute, simp add: fun_eq_iff) definition F :: "'a set \ 'b" where eq_fold: "F A = fold f z A" -lemma empty [simp]: - "F {} = z" +lemma empty [simp]:"F {} = z" by (simp add: eq_fold) -lemma infinite [simp]: - "\ finite A \ F A = z" +lemma infinite [simp]: "\ finite A \ F A = z" by (simp add: eq_fold) lemma insert [simp]: @@ -1172,7 +1170,7 @@ declare insert [simp del] interpretation fold?: comp_fun_idem f - by default (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) + by standard (insert comp_fun_commute comp_fun_idem, simp add: fun_eq_iff) lemma insert_idem [simp]: assumes "finite A" @@ -1202,7 +1200,7 @@ where "folding.F (\_. Suc) 0 = card" proof - - show "folding (\_. Suc)" by default rule + show "folding (\_. Suc)" by standard rule then interpret card!: folding "\_. Suc" 0 . from card_def show "folding.F (\_. Suc) 0 = card" by rule qed diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/GCD.thy --- a/src/HOL/GCD.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/GCD.thy Sun Sep 13 22:56:52 2015 +0200 @@ -1975,7 +1975,7 @@ and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" proof - show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\m n. m dvd n \ \ n dvd m) lcm 1 (0::nat)" - by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite) + by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite) then interpret gcd_lcm_complete_lattice_nat: complete_lattice Gcd Lcm gcd Rings.dvd "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" . from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" . diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Groups.thy --- a/src/HOL/Groups.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Groups.thy Sun Sep 13 22:56:52 2015 +0200 @@ -71,7 +71,7 @@ begin sublocale monoid - by default (simp_all add: commute comm_neutral) + by standard (simp_all add: commute comm_neutral) end @@ -132,7 +132,7 @@ begin sublocale add!: semigroup plus - by default (fact add_assoc) + by standard (fact add_assoc) end @@ -143,7 +143,7 @@ begin sublocale add!: abel_semigroup plus - by default (fact add_commute) + by standard (fact add_commute) declare add.left_commute [algebra_simps, field_simps] @@ -160,7 +160,7 @@ begin sublocale mult!: semigroup times - by default (fact mult_assoc) + by standard (fact mult_assoc) end @@ -171,7 +171,7 @@ begin sublocale mult!: abel_semigroup times - by default (fact mult_commute) + by standard (fact mult_commute) declare mult.left_commute [algebra_simps, field_simps] @@ -189,7 +189,7 @@ begin sublocale add!: monoid plus 0 - by default (fact add_0_left add_0_right)+ + by standard (fact add_0_left add_0_right)+ end @@ -201,10 +201,10 @@ begin subclass monoid_add - by default (simp_all add: add_0 add.commute [of _ 0]) + by standard (simp_all add: add_0 add.commute [of _ 0]) sublocale add!: comm_monoid plus 0 - by default (simp add: ac_simps) + by standard (simp add: ac_simps) end @@ -214,7 +214,7 @@ begin sublocale mult!: monoid times 1 - by default (fact mult_1_left mult_1_right)+ + by standard (fact mult_1_left mult_1_right)+ end @@ -226,10 +226,10 @@ begin subclass monoid_mult - by default (simp_all add: mult_1 mult.commute [of _ 1]) + by standard (simp_all add: mult_1 mult.commute [of _ 1]) sublocale mult!: comm_monoid times 1 - by default (simp add: ac_simps) + by standard (simp add: ac_simps) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Groups_Big.thy Sun Sep 13 22:56:52 2015 +0200 @@ -18,7 +18,7 @@ begin interpretation comp_fun_commute f - by default (simp add: fun_eq_iff left_commute) + by standard (simp add: fun_eq_iff left_commute) interpretation comp?: comp_fun_commute "f \ g" by (fact comp_comp_fun_commute) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOL.thy Sun Sep 13 22:56:52 2015 +0200 @@ -1254,10 +1254,10 @@ qed lemma implies_True_equals: "(PROP P \ True) \ Trueprop True" -by default (intro TrueI) + by standard (intro TrueI) lemma False_implies_equals: "(False \ P) \ Trueprop True" -by default simp_all + by standard simp_all (* This is not made a simp rule because it does not improve any proofs but slows some AFP entries down by 5% (cpu time). May 2015 *) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Bifinite.thy --- a/src/HOL/HOLCF/Bifinite.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Bifinite.thy Sun Sep 13 22:56:52 2015 +0200 @@ -162,7 +162,7 @@ qed instance u :: (profinite) bifinite - by default (rule profinite) + by standard (rule profinite) text {* Types @{typ "'a \ 'b"} and @{typ "'a u \! 'b"} are isomorphic. @@ -256,10 +256,10 @@ by (simp add: approx_chain_def cfun_eq_iff finite_deflation_bottom) instance unit :: bifinite - by default (fast intro!: approx_chain_unit) + by standard (fast intro!: approx_chain_unit) instance discr :: (countable) profinite - by default (fast intro!: discr_approx) + by standard (fast intro!: discr_approx) instance lift :: (countable) bifinite proof diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Completion.thy --- a/src/HOL/HOLCF/Completion.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Completion.thy Sun Sep 13 22:56:52 2015 +0200 @@ -116,7 +116,7 @@ assumes type: "type_definition Rep Abs {S. ideal S}" assumes below: "\x y. x \ y \ Rep x \ Rep y" shows "OFCLASS('b, cpo_class)" -by (default, rule exI, erule typedef_ideal_lub [OF type below]) + by standard (rule exI, erule typedef_ideal_lub [OF type below]) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/ConvexPD.thy Sun Sep 13 22:56:52 2015 +0200 @@ -414,14 +414,14 @@ by (simp add: convex_map_def convex_bind_bind) lemma ep_pair_convex_map: "ep_pair e p \ ep_pair (convex_map\e) (convex_map\p)" -apply default +apply standard apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse) apply (induct_tac y rule: convex_pd_induct) apply (simp_all add: ep_pair.e_p_below monofun_cfun) done lemma deflation_convex_map: "deflation d \ deflation (convex_map\d)" -apply default +apply standard apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem) apply (induct_tac x rule: convex_pd_induct) apply (simp_all add: deflation.below monofun_cfun) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Deflation.thy --- a/src/HOL/HOLCF/Deflation.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Deflation.thy Sun Sep 13 22:56:52 2015 +0200 @@ -161,7 +161,7 @@ unfolding finite_deflation_def by simp lemma finite_deflation_bottom: "finite_deflation \" -by default simp_all +by standard simp_all subsection {* Continuous embedding-projection pairs *} @@ -358,7 +358,7 @@ subsection {* Composing ep-pairs *} lemma ep_pair_ID_ID: "ep_pair ID ID" -by default simp_all +by standard simp_all lemma ep_pair_comp: assumes "ep_pair e1 p1" and "ep_pair e2 p2" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Discrete.thy --- a/src/HOL/HOLCF/Discrete.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Discrete.thy Sun Sep 13 22:56:52 2015 +0200 @@ -19,7 +19,7 @@ "(op \ :: 'a discr \ 'a discr \ bool) = (op =)" instance -by default (simp add: below_discr_def) + by standard (simp add: below_discr_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Domain.thy --- a/src/HOL/HOLCF/Domain.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Domain.thy Sun Sep 13 22:56:52 2015 +0200 @@ -125,7 +125,7 @@ unfolding prj_beta emb_beta by (simp add: type_definition.Abs_inverse [OF type]) show "ep_pair (emb :: 'a \ udom) prj" - apply default + apply standard apply (simp add: prj_emb) apply (simp add: emb_prj cast.below) done diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Fun_Cpo.thy --- a/src/HOL/HOLCF/Fun_Cpo.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Fun_Cpo.thy Sun Sep 13 22:56:52 2015 +0200 @@ -93,7 +93,7 @@ by (simp add: below_fun_def) instance "fun" :: (type, pcpo) pcpo -by default (fast intro: minimal_fun) +by standard (fast intro: minimal_fun) lemma inst_fun_pcpo: "\ = (\x. \)" by (rule minimal_fun [THEN bottomI, symmetric]) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Library/Defl_Bifinite.thy --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sun Sep 13 22:56:52 2015 +0200 @@ -490,7 +490,7 @@ by (fast intro: below_antisym meet_defl_below2 meet_defl_greatest) interpretation meet_defl: semilattice "\a b. meet_defl\a\b" -by default +by standard (fast intro: below_antisym meet_defl_greatest meet_defl_below1 [THEN below_trans] meet_defl_below2 [THEN below_trans])+ diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Library/List_Predomain.thy --- a/src/HOL/HOLCF/Library/List_Predomain.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Library/List_Predomain.thy Sun Sep 13 22:56:52 2015 +0200 @@ -143,7 +143,7 @@ lemma deflation_list_map [domain_deflation]: "deflation d \ deflation (list_map d)" -apply default +apply standard apply (induct_tac x, simp_all add: deflation.idem) apply (induct_tac x, simp_all add: deflation.below) done diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Library/Option_Cpo.thy --- a/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Library/Option_Cpo.thy Sun Sep 13 22:56:52 2015 +0200 @@ -269,7 +269,7 @@ lemma deflation_option_map [domain_deflation]: "deflation d \ deflation (option_map d)" -apply default +apply standard apply (induct_tac x, simp_all add: deflation.idem) apply (induct_tac x, simp_all add: deflation.below) done diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Library/Sum_Cpo.thy --- a/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Library/Sum_Cpo.thy Sun Sep 13 22:56:52 2015 +0200 @@ -342,7 +342,7 @@ lemma deflation_map_sum [domain_deflation]: "\deflation d1; deflation d2\ \ deflation (map_sum' d1 d2)" -apply default +apply standard apply (induct_tac x, simp_all add: deflation.idem) apply (induct_tac x, simp_all add: deflation.below) done diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/LowerPD.thy Sun Sep 13 22:56:52 2015 +0200 @@ -407,14 +407,14 @@ by (simp add: lower_map_def lower_bind_bind) lemma ep_pair_lower_map: "ep_pair e p \ ep_pair (lower_map\e) (lower_map\p)" -apply default +apply standard apply (induct_tac x rule: lower_pd_induct, simp_all add: ep_pair.e_inverse) apply (induct_tac y rule: lower_pd_induct) apply (simp_all add: ep_pair.e_p_below monofun_cfun del: lower_plus_below_iff) done lemma deflation_lower_map: "deflation d \ deflation (lower_map\d)" -apply default +apply standard apply (induct_tac x rule: lower_pd_induct, simp_all add: deflation.idem) apply (induct_tac x rule: lower_pd_induct) apply (simp_all add: deflation.below monofun_cfun del: lower_plus_below_iff) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Map_Functions.thy --- a/src/HOL/HOLCF/Map_Functions.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Map_Functions.thy Sun Sep 13 22:56:52 2015 +0200 @@ -195,13 +195,13 @@ by (simp add: cfcomp1 u_map_map eta_cfun) lemma ep_pair_u_map: "ep_pair e p \ ep_pair (u_map\e) (u_map\p)" -apply default +apply standard apply (case_tac x, simp, simp add: ep_pair.e_inverse) apply (case_tac y, simp, simp add: ep_pair.e_p_below) done lemma deflation_u_map: "deflation d \ deflation (u_map\d)" -apply default +apply standard apply (case_tac x, simp, simp add: deflation.idem) apply (case_tac x, simp, simp add: deflation.below) done diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Pcpo.thy --- a/src/HOL/HOLCF/Pcpo.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Pcpo.thy Sun Sep 13 22:56:52 2015 +0200 @@ -198,7 +198,7 @@ begin subclass cpo -apply default +apply standard apply (frule chfin) apply (blast intro: lub_finch1) done @@ -213,7 +213,7 @@ begin subclass chfin -apply default +apply standard apply (unfold max_in_chain_def) apply (case_tac "\i. Y i = \") apply simp diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Representable.thy --- a/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Representable.thy Sun Sep 13 22:56:52 2015 +0200 @@ -119,10 +119,10 @@ qed instance "domain" \ bifinite -by default (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL]) +by standard (rule approx_chain_ep_cast [OF ep_pair_emb_prj cast_DEFL]) instance predomain \ profinite -by default (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) +by standard (rule approx_chain_ep_cast [OF predomain_ep cast_liftdefl]) subsection {* Universal domain ep-pairs *} diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/Universal.thy Sun Sep 13 22:56:52 2015 +0200 @@ -98,7 +98,7 @@ done interpretation udom: preorder ubasis_le -apply default +apply standard apply (rule ubasis_le_refl) apply (erule (1) ubasis_le_trans) done @@ -879,7 +879,7 @@ done lemma ep_pair_udom: "ep_pair udom_emb udom_prj" - apply default + apply standard apply (rule compact_basis.principal_induct, simp) apply (simp add: udom_emb_principal udom_prj_principal) apply (simp add: basis_prj_basis_emb) @@ -986,7 +986,7 @@ qed instance udom :: bifinite - by default (fast intro: udom_approx) + by standard (fast intro: udom_approx) hide_const (open) node diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/HOLCF/UpperPD.thy Sun Sep 13 22:56:52 2015 +0200 @@ -400,14 +400,14 @@ by (simp add: upper_map_def upper_bind_bind) lemma ep_pair_upper_map: "ep_pair e p \ ep_pair (upper_map\e) (upper_map\p)" -apply default +apply standard apply (induct_tac x rule: upper_pd_induct, simp_all add: ep_pair.e_inverse) apply (induct_tac y rule: upper_pd_induct) apply (simp_all add: ep_pair.e_p_below monofun_cfun del: upper_below_plus_iff) done lemma deflation_upper_map: "deflation d \ deflation (upper_map\d)" -apply default +apply standard apply (induct_tac x rule: upper_pd_induct, simp_all add: deflation.idem) apply (induct_tac x rule: upper_pd_induct) apply (simp_all add: deflation.below monofun_cfun del: upper_below_plus_iff) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Int.thy --- a/src/HOL/Int.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Int.thy Sun Sep 13 22:56:52 2015 +0200 @@ -66,7 +66,7 @@ qed instance - by default (transfer, clarsimp simp: algebra_simps)+ + by standard (transfer, clarsimp simp: algebra_simps)+ end @@ -99,7 +99,7 @@ by auto instance - by default (transfer, force)+ + by standard (transfer, force)+ end @@ -305,13 +305,13 @@ instance int :: no_top - apply default + apply standard apply (rule_tac x="x + 1" in exI) apply simp done instance int :: no_bot - apply default + apply standard apply (rule_tac x="x - 1" in exI) apply simp done @@ -1526,7 +1526,8 @@ definition "HOL.equal k l \ k = (l::int)" -instance by default (rule equal_int_def) +instance + by standard (rule equal_int_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Lattices.thy Sun Sep 13 22:56:52 2015 +0200 @@ -145,7 +145,7 @@ begin sublocale ordering_top less_eq less 1 - by default (simp add: order_iff) + by standard (simp add: order_iff) end @@ -283,7 +283,7 @@ qed sublocale inf!: semilattice_order inf less_eq less - by default (auto simp add: le_iff_inf less_le) + by standard (auto simp add: le_iff_inf less_le) lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" by (fact inf.assoc) @@ -328,7 +328,7 @@ qed sublocale sup!: semilattice_order sup greater_eq greater - by default (auto simp add: le_iff_sup sup.commute less_le) + by standard (auto simp add: le_iff_sup sup.commute less_le) lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" by (fact sup.assoc) @@ -717,7 +717,7 @@ sublocale min!: semilattice_order min less_eq less + max!: semilattice_order max greater_eq greater - by default (auto simp add: min_def max_def) + by standard (auto simp add: min_def max_def) lemma min_le_iff_disj: "min x y \ z \ x \ z \ y \ z" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Lattices_Big.thy Sun Sep 13 22:56:52 2015 +0200 @@ -21,7 +21,7 @@ begin interpretation comp_fun_idem f - by default (simp_all add: fun_eq_iff left_commute) + by standard (simp_all add: fun_eq_iff left_commute) definition F :: "'a set \ 'a" where @@ -33,7 +33,7 @@ proof (rule sym) let ?f = "\x y. Some (case y of None \ x | Some z \ f x z)" interpret comp_fun_idem "?f" - by default (simp_all add: fun_eq_iff commute left_commute split: option.split) + by standard (simp_all add: fun_eq_iff commute left_commute split: option.split) from assms show "Finite_Set.fold f x A = F (insert x A)" proof induct case empty then show ?case by (simp add: eq_fold') @@ -189,7 +189,7 @@ begin interpretation comp_fun_idem f - by default (simp_all add: fun_eq_iff left_commute) + by standard (simp_all add: fun_eq_iff left_commute) definition F :: "'a set \ 'a" where @@ -496,9 +496,9 @@ "semilattice_set.F min = Min" and "semilattice_set.F max = Max" proof - - show "semilattice_order_set min less_eq less" by default (auto simp add: min_def) + show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def) then interpret Min!: semilattice_order_set min less_eq less . - show "semilattice_order_set max greater_eq greater" by default (auto simp add: max_def) + show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def) then interpret Max!: semilattice_order_set max greater_eq greater . from Min_def show "semilattice_set.F min = Min" by rule from Max_def show "semilattice_set.F max = Max" by rule diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Limits.thy --- a/src/HOL/Limits.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Limits.thy Sun Sep 13 22:56:52 2015 +0200 @@ -710,13 +710,15 @@ lemma (in bounded_bilinear) flip: "bounded_bilinear (\x y. y ** x)" - apply default + apply standard apply (rule add_right) apply (rule add_left) apply (rule scaleR_right) apply (rule scaleR_left) apply (subst mult.commute) - using bounded by fast + using bounded + apply fast + done lemma (in bounded_bilinear) Bfun_prod_Zfun: assumes f: "Bfun f F" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/List.thy --- a/src/HOL/List.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/List.thy Sun Sep 13 22:56:52 2015 +0200 @@ -2868,7 +2868,7 @@ "F (set (x # xs)) = fold f xs x" proof - interpret comp_fun_idem f - by default (simp_all add: fun_eq_iff left_commute) + by standard (simp_all add: fun_eq_iff left_commute) show ?thesis by (simp add: eq_fold fold_set_fold) qed @@ -5161,7 +5161,7 @@ "folding.F insort [] = sorted_list_of_set" proof - interpret comp_fun_commute insort by (fact comp_fun_commute_insort) - show "folding insort" by default (fact comp_fun_commute) + show "folding insort" by standard (fact comp_fun_commute) show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def) qed diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Matrix_LP/Matrix.thy --- a/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Matrix_LP/Matrix.thy Sun Sep 13 22:56:52 2015 +0200 @@ -1448,7 +1448,7 @@ definition "sup = combine_matrix sup" instance - by default (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def) + by standard (auto simp add: le_infI le_matrix_def inf_matrix_def sup_matrix_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Matrix_LP/SparseMatrix.thy --- a/src/HOL/Matrix_LP/SparseMatrix.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Matrix_LP/SparseMatrix.thy Sun Sep 13 22:56:52 2015 +0200 @@ -120,8 +120,11 @@ done instance matrix :: (lattice_ab_group_add_abs) lattice_ab_group_add_abs -apply default -unfolding abs_matrix_def .. (*FIXME move*) + apply standard + unfolding abs_matrix_def + apply rule + done + (*FIXME move*) lemma sparse_row_vector_abs: "sorted_spvec (v :: 'a::lattice_ring spvec) \ sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/MicroJava/J/State.thy --- a/src/HOL/MicroJava/J/State.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/MicroJava/J/State.thy Sun Sep 13 22:56:52 2015 +0200 @@ -191,7 +191,7 @@ begin definition "HOL.equal (l :: loc') l' \ l = l'" -instance by default (simp add: equal_loc'_def) +instance by standard (simp add: equal_loc'_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/MicroJava/J/Type.thy --- a/src/HOL/MicroJava/J/Type.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/MicroJava/J/Type.thy Sun Sep 13 22:56:52 2015 +0200 @@ -13,7 +13,7 @@ begin definition "HOL.equal (cn :: cnam) cn' \ cn = cn'" -instance by default (simp add: equal_cnam_def) +instance by standard (simp add: equal_cnam_def) end @@ -63,7 +63,7 @@ begin definition "HOL.equal (vn :: vnam) vn' \ vn = vn'" -instance by default (simp add: equal_vnam_def) +instance by standard (simp add: equal_vnam_def) end @@ -98,7 +98,7 @@ begin definition "HOL.equal (M :: mname) M' \ M = M'" -instance by default (simp add: equal_mname_def) +instance by standard (simp add: equal_mname_def) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sun Sep 13 22:56:52 2015 +0200 @@ -315,7 +315,7 @@ by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun) instance - by default + by standard (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps plus_cont const_bcontfun minus_cont scaleR_cont) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Sun Sep 13 22:56:52 2015 +0200 @@ -589,7 +589,7 @@ using enum_Suc[of 0] na[rule_format, OF \enum 1 \ s - {a}\] \a = enum 0\ by (auto simp: \upd 0 = n\) show ?thesis - proof (rule ksimplex.intros, default) + proof (rule ksimplex.intros, standard) show "bij_betw (upd\Suc) {..< n} {..< n}" by fact show "base(n := p) \ {.. {..i. n\i \ (base(n := p)) i = p" using base base_out by (auto simp: Pi_iff) @@ -620,7 +620,7 @@ def u \ "\i. case i of 0 \ n | Suc i \ upd i" have "ksimplex p (Suc n) (s' \ {b})" - proof (rule ksimplex.intros, default) + proof (rule ksimplex.intros, standard) show "b \ {.. {..0 < p\ unfolding lessThan_Suc b_def by (auto simp: PiE_iff) show "\i. Suc n \ i \ b i = p" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200 @@ -73,7 +73,7 @@ end instance vec:: (order, finite) order - by default (auto simp: less_eq_vec_def less_vec_def vec_eq_iff + by standard (auto simp: less_eq_vec_def less_vec_def vec_eq_iff intro: order.trans order.antisym order.strict_implies_order) instance vec :: (linorder, cart_one) linorder @@ -183,26 +183,26 @@ subsection \Some frequently useful arithmetic lemmas over vectors.\ instance vec :: (semigroup_mult, finite) semigroup_mult - by default (vector mult.assoc) + by standard (vector mult.assoc) instance vec :: (monoid_mult, finite) monoid_mult - by default vector+ + by standard vector+ instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult - by default (vector mult.commute) + by standard (vector mult.commute) instance vec :: (comm_monoid_mult, finite) comm_monoid_mult - by default vector + by standard vector instance vec :: (semiring, finite) semiring - by default (vector field_simps)+ + by standard (vector field_simps)+ instance vec :: (semiring_0, finite) semiring_0 - by default (vector field_simps)+ + by standard (vector field_simps)+ instance vec :: (semiring_1, finite) semiring_1 - by default vector + by standard vector instance vec :: (comm_semiring, finite) comm_semiring - by default (vector field_simps)+ + by standard (vector field_simps)+ instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. @@ -215,7 +215,7 @@ instance vec :: (ring_1, finite) ring_1 .. instance vec :: (real_algebra, finite) real_algebra - by default (simp_all add: vec_eq_iff) + by standard (simp_all add: vec_eq_iff) instance vec :: (real_algebra_1, finite) real_algebra_1 .. diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200 @@ -139,7 +139,7 @@ [simp]: "Basis = {1::real}" instance - by default auto + by standard auto end @@ -155,7 +155,7 @@ "Basis = {1, ii}" instance - by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm) + by standard (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Sun Sep 13 22:56:52 2015 +0200 @@ -53,7 +53,7 @@ qed instance ereal :: second_countable_topology -proof (default, intro exI conjI) +proof (standard, intro exI conjI) let ?B = "(\r\\. {{..< r}, {r <..}} :: ereal set set)" show "countable ?B" by (auto intro: countable_rat) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Sep 13 22:56:52 2015 +0200 @@ -95,30 +95,30 @@ unfolding uminus_vec_def by simp instance vec :: (semigroup_add, finite) semigroup_add - by default (simp add: vec_eq_iff add.assoc) + by standard (simp add: vec_eq_iff add.assoc) instance vec :: (ab_semigroup_add, finite) ab_semigroup_add - by default (simp add: vec_eq_iff add.commute) + by standard (simp add: vec_eq_iff add.commute) instance vec :: (monoid_add, finite) monoid_add - by default (simp_all add: vec_eq_iff) + by standard (simp_all add: vec_eq_iff) instance vec :: (comm_monoid_add, finite) comm_monoid_add - by default (simp add: vec_eq_iff) + by standard (simp add: vec_eq_iff) instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add - by default (simp_all add: vec_eq_iff) + by standard (simp_all add: vec_eq_iff) instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add - by default (simp_all add: vec_eq_iff diff_diff_eq) + by standard (simp_all add: vec_eq_iff diff_diff_eq) instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. instance vec :: (group_add, finite) group_add - by default (simp_all add: vec_eq_iff) + by standard (simp_all add: vec_eq_iff) instance vec :: (ab_group_add, finite) ab_group_add - by default (simp_all add: vec_eq_iff) + by standard (simp_all add: vec_eq_iff) subsection \Real vector space\ @@ -132,7 +132,7 @@ unfolding scaleR_vec_def by simp instance - by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib) + by standard (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib) end @@ -412,7 +412,7 @@ by (rule member_le_setL2) simp_all lemma bounded_linear_vec_nth: "bounded_linear (\x. x $ i)" -apply default +apply standard apply (rule vector_add_component) apply (rule vector_scaleR_component) apply (rule_tac x="1" in exI, simp add: norm_nth_le) diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Ordered_Euclidean_Space.thy Sun Sep 13 22:56:52 2015 +0200 @@ -17,20 +17,20 @@ begin subclass order - by default + by standard (auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) subclass ordered_ab_group_add_abs - by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI) + by standard (auto simp: eucl_le inner_add_left eucl_abs abs_leI) subclass ordered_real_vector - by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) + by standard (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) subclass lattice - by default (auto simp: eucl_inf eucl_sup eucl_le) + by standard (auto simp: eucl_inf eucl_sup eucl_le) subclass distrib_lattice - by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) + by standard (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) subclass conditionally_complete_lattice proof @@ -152,7 +152,7 @@ by (auto) instance real :: ordered_euclidean_space - by default (auto simp: INF_def SUP_def) + by standard (auto simp: INF_def SUP_def) lemma in_Basis_prod_iff: fixes i::"'a::euclidean_space*'b::euclidean_space" @@ -168,7 +168,7 @@ end instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space - by default + by standard (auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] @@ -281,7 +281,7 @@ definition "abs x = (\ i. abs (x $ i))" instance - apply default + apply standard unfolding euclidean_representation_setsum' apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Nat.thy Sun Sep 13 22:56:52 2015 +0200 @@ -529,7 +529,7 @@ end instance nat :: no_top - by default (auto intro: less_Suc_eq_le [THEN iffD2]) + by standard (auto intro: less_Suc_eq_le [THEN iffD2]) subsubsection \Introduction properties\ diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Nominal/Examples/Pattern.thy --- a/src/HOL/Nominal/Examples/Pattern.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Nominal/Examples/Pattern.thy Sun Sep 13 22:56:52 2015 +0200 @@ -62,7 +62,7 @@ by (simp add: supp_def Collect_disj_eq del: disj_not1) instance pat :: pt_name -proof (default, goal_cases) +proof (standard, goal_cases) case (1 x) show ?case by (induct x) simp_all next @@ -74,7 +74,7 @@ qed instance pat :: fs_name -proof (default, goal_cases) +proof (standard, goal_cases) case (1 x) show ?case by (induct x) (simp_all add: fin_supp) qed diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Num.thy --- a/src/HOL/Num.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Num.thy Sun Sep 13 22:56:52 2015 +0200 @@ -106,7 +106,7 @@ "m < n \ nat_of_num m < nat_of_num n" instance - by (default, auto simp add: less_num_def less_eq_num_def num_eq_iff) + by standard (auto simp add: less_num_def less_eq_num_def num_eq_iff) end diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Orderings.thy Sun Sep 13 22:56:52 2015 +0200 @@ -196,7 +196,7 @@ by (auto simp add: less_le_not_le intro: antisym) sublocale order!: ordering less_eq less + dual_order!: ordering greater_eq greater - by default (auto intro: antisym order_trans simp add: less_le) + by standard (auto intro: antisym order_trans simp add: less_le) text \Reflexivity.\ @@ -1197,7 +1197,7 @@ begin sublocale bot!: ordering_top greater_eq greater bot - by default (fact bot_least) + by standard (fact bot_least) lemma le_bot: "a \ \ \ a = \" @@ -1225,7 +1225,7 @@ begin sublocale top!: ordering_top less_eq less top - by default (fact top_greatest) + by standard (fact top_greatest) lemma top_le: "\ \ a \ a = \" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Sun Sep 13 22:56:52 2015 +0200 @@ -702,7 +702,7 @@ proof (rule measure_eqI) interpret A: finite_measure "count_space A" by (rule finite_measure_count_space) fact interpret B: finite_measure "count_space B" by (rule finite_measure_count_space) fact - interpret P: pair_sigma_finite "count_space A" "count_space B" by default + interpret P: pair_sigma_finite "count_space A" "count_space B" .. show eq: "sets ?P = sets ?C" by (simp add: sets_pair_measure sigma_sets_pair_measure_generator_finite A B) fix X assume X: "X \ sets ?P" @@ -890,7 +890,7 @@ proof - interpret M1: sigma_finite_measure M1 by fact interpret M2: sigma_finite_measure M2 by fact - interpret pair_sigma_finite M1 M2 by default + interpret pair_sigma_finite M1 M2 .. from sigma_finite_up_in_pair_measure_generator guess F :: "nat \ ('a \ 'b) set" .. note F = this let ?E = "{a \ b |a b. a \ sets M1 \ b \ sets M2}" let ?P = "M1 \\<^sub>M M2" diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Bochner_Integration.thy Sun Sep 13 22:56:52 2015 +0200 @@ -2549,7 +2549,7 @@ assumes "integrable (M1 \\<^sub>M M2) f" shows "integrable (M2 \\<^sub>M M1) (\(x,y). f (y,x))" proof - - interpret Q: pair_sigma_finite M2 M1 by default + interpret Q: pair_sigma_finite M2 M1 .. have *: "(\(x,y). f (y,x)) = (\x. f (case x of (x,y)\(y,x)))" by (auto simp: fun_eq_iff) show ?thesis unfolding * by (rule integrable_distr[OF measurable_pair_swap']) @@ -2560,7 +2560,7 @@ fixes f :: "_ \ _::{banach, second_countable_topology}" shows "integrable (M2 \\<^sub>M M1) (\(x,y). f (y,x)) \ integrable (M1 \\<^sub>M M2) f" proof - - interpret Q: pair_sigma_finite M2 M1 by default + interpret Q: pair_sigma_finite M2 M1 .. from Q.integrable_product_swap[of "\(x,y). f (y,x)"] integrable_product_swap[of f] show ?thesis by auto qed @@ -2751,7 +2751,7 @@ and integrable_snd: "integrable M2 (\y. \x. f x y \M1)" (is "?INT") and integral_snd: "(\y. (\x. f x y \M1) \M2) = integral\<^sup>L (M1 \\<^sub>M M2) (split f)" (is "?EQ") proof - - interpret Q: pair_sigma_finite M2 M1 by default + interpret Q: pair_sigma_finite M2 M1 .. have Q_int: "integrable (M2 \\<^sub>M M1) (\(x, y). f y x)" using f unfolding integrable_product_swap_iff[symmetric] by simp show ?AE using Q.AE_integrable_fst'[OF Q_int] by simp @@ -2780,11 +2780,11 @@ and f: "integrable (Pi\<^sub>M (I \ J) M) f" shows "integral\<^sup>L (Pi\<^sub>M (I \ J) M) f = (\x. (\y. f (merge I J (x, y)) \Pi\<^sub>M J M) \Pi\<^sub>M I M)" proof - - interpret I: finite_product_sigma_finite M I by default fact - interpret J: finite_product_sigma_finite M J by default fact + interpret I: finite_product_sigma_finite M I by standard fact + interpret J: finite_product_sigma_finite M J by standard fact have "finite (I \ J)" using fin by auto - interpret IJ: finite_product_sigma_finite M "I \ J" by default fact - interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default + interpret IJ: finite_product_sigma_finite M "I \ J" by standard fact + interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" .. let ?M = "merge I J" let ?f = "\x. f (?M x)" from f have f_borel: "f \ borel_measurable (Pi\<^sub>M (I \ J) M)" @@ -2830,7 +2830,7 @@ assumes [simp]: "finite I" and integrable: "\i. i \ I \ integrable (M i) (f i)" shows "integrable (Pi\<^sub>M I M) (\x. (\i\I. f i (x i)))" (is "integrable _ ?f") proof (unfold integrable_iff_bounded, intro conjI) - interpret finite_product_sigma_finite M I by default fact + interpret finite_product_sigma_finite M I by standard fact show "?f \ borel_measurable (Pi\<^sub>M I M)" using assms by simp @@ -2859,7 +2859,7 @@ then have prod: "\J. J \ insert i I \ integrable (Pi\<^sub>M J M) (\x. (\i\J. f i (x i)))" by (intro product_integrable_setprod insert(4)) (auto intro: finite_subset) - interpret I: finite_product_sigma_finite M I by default fact + interpret I: finite_product_sigma_finite M I by standard fact have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" using `i \ I` by (auto intro!: setprod.cong) show ?case diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Probability/Embed_Measure.thy --- a/src/HOL/Probability/Embed_Measure.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Embed_Measure.thy Sun Sep 13 22:56:52 2015 +0200 @@ -169,7 +169,7 @@ from A_props and inj have "\a\op ` f ` A. emeasure (embed_measure M f) a \ \" by (intro ballI, subst emeasure_embed_measure) (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure) - ultimately show ?thesis by - (default, blast) + ultimately show ?thesis by - (standard, blast) qed lemma embed_measure_count_space': diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Sun Sep 13 22:25:21 2015 +0200 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Sun Sep 13 22:56:52 2015 +0200 @@ -764,9 +764,9 @@ "finite I \ (\i. i\I \ A i \ sets (M i)) \ emeasure (PiM I M) (Pi\<^sub>E I A) = (\i\I. emeasure (M i) (A i))" proof (induct I arbitrary: A rule: finite_induct) case (insert i I) - interpret finite_product_sigma_finite M I by default fact + interpret finite_product_sigma_finite M I by standard fact have "finite (insert i I)" using `finite I` by auto - interpret I': finite_product_sigma_finite M "insert i I" by default fact + interpret I': finite_product_sigma_finite M "insert i I" by standard fact let ?h = "(\(f, y). f(i := y))" let ?P = "distr (Pi\<^sub>M I M \\<^sub>M M i) (Pi\<^sub>M (insert i I) M) ?h" @@ -821,7 +821,7 @@ assumes "finite I" shows "sigma_finite_measure (PiM I M)" proof - interpret finite_product_sigma_finite M I by default fact + interpret finite_product_sigma_finite M I by standard fact obtain F where F: "\j. countable (F j)" "\j f. f \ F j \ f \ sets (M j)" "\j f. f \ F j \ emeasure (M j) f \ \" and @@ -846,7 +846,7 @@ assumes pos: "0 \ f (\k. undefined)" shows "integral\<^sup>N (Pi\<^sub>M {} M) f = f (\k. undefined)" proof - - interpret finite_product_sigma_finite M "{}" by default (fact finite.emptyI) + interpret finite_product_sigma_finite M "{}" by standard (fact finite.emptyI) have "\A. emeasure (Pi\<^sub>M {} M) (Pi\<^sub>E {} A) = 1" using assms by (subst measure_times) auto then show ?thesis @@ -864,11 +864,11 @@ shows "distr (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M) (Pi\<^sub>M (I \ J) M) (merge I J) = Pi\<^sub>M (I \ J) M" (is "?D = ?P") proof - - interpret I: finite_product_sigma_finite M I by default fact - interpret J: finite_product_sigma_finite M J by default fact + interpret I: finite_product_sigma_finite M I by standard fact + interpret J: finite_product_sigma_finite M J by standard fact have "finite (I \ J)" using fin by auto - interpret IJ: finite_product_sigma_finite M "I \ J" by default fact - interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default + interpret IJ: finite_product_sigma_finite M "I \ J" by standard fact + interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard let ?g = "merge I J" from IJ.sigma_finite_pairs obtain F where @@ -928,9 +928,9 @@ shows "integral\<^sup>N (Pi\<^sub>M (I \ J) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (merge I J (x, y)) \(Pi\<^sub>M J M)) \(Pi\<^sub>M I M))" proof - - interpret I: finite_product_sigma_finite M I by default fact - interpret J: finite_product_sigma_finite M J by default fact - interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by default + interpret I: finite_product_sigma_finite M I by standard fact + interpret J: finite_product_sigma_finite M J by standard fact + interpret P: pair_sigma_finite "Pi\<^sub>M I M" "Pi\<^sub>M J M" by standard have P_borel: "(\x. f (merge I J x)) \ borel_measurable (Pi\<^sub>M I M \\<^sub>M Pi\<^sub>M J M)" using measurable_comp[OF measurable_merge f] by (simp add: comp_def) show ?thesis @@ -944,7 +944,7 @@ lemma (in product_sigma_finite) distr_singleton: "distr (Pi\<^sub>M {i} M) (M i) (\x. x i) = M i" (is "?D = _") proof (intro measure_eqI[symmetric]) - interpret I: finite_product_sigma_finite M "{i}" by default simp + interpret I: finite_product_sigma_finite M "{i}" by standard simp fix A assume A: "A \ sets (M i)" then have "(\x. x i) -` A \ space (Pi\<^sub>M {i} M) = (\\<^sub>E i\{i}. A)" using sets.sets_into_space by (auto simp: space_PiM) @@ -957,7 +957,7 @@ assumes f: "f \ borel_measurable (M i)" shows "integral\<^sup>N (Pi\<^sub>M {i} M) (\x. f (x i)) = integral\<^sup>N (M i) f" proof - - interpret I: finite_product_sigma_finite M "{i}" by default simp + interpret I: finite_product_sigma_finite M "{i}" by standard simp from f show ?thesis apply (subst distr_singleton[symmetric]) apply (subst nn_integral_distr[OF measurable_component_singleton]) @@ -970,8 +970,8 @@ and f: "f \ borel_measurable (Pi\<^sub>M (insert i I) M)" shows "integral\<^sup>N (Pi\<^sub>M (insert i I) M) f = (\\<^sup>+ x. (\\<^sup>+ y. f (x(i := y)) \(M i)) \(Pi\<^sub>M I M))" proof - - interpret I: finite_product_sigma_finite M I by default auto - interpret i: finite_product_sigma_finite M "{i}" by default auto + interpret I: finite_product_sigma_finite M I by standard auto + interpret i: finite_product_sigma_finite M "{i}" by standard auto have IJ: "I \ {i} = {}" and insert: "I \ {i} = insert i I" using f by auto show ?thesis @@ -1008,7 +1008,7 @@ using assms proof induct case (insert i I) note `finite I`[intro, simp] - interpret I: finite_product_sigma_finite M I by default auto + interpret I: finite_product_sigma_finite M I by standard auto have *: "\x y. (\j\I. f j (if j = i then y else x j)) = (\j\I. f j (x j))" using insert by (auto intro!: setprod.cong) have prod: "\J. J \ insert i I \ (\x. (\i\J. f i (x i))) \ borel_measurable (Pi\<^sub>M J M)" @@ -1044,7 +1044,7 @@ lemma (in product_sigma_finite) distr_component: "distr (M i) (Pi\<^sub>M {i} M) (\