--- a/src/HOL/Library/Bit.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Bit.thy Mon Jul 06 22:57:34 2015 +0200
@@ -123,8 +123,8 @@
plus_bit_def times_bit_def minus_bit_def uminus_bit_def
divide_bit_def inverse_bit_def
-instance proof
-qed (unfold field_bit_defs, auto split: bit.split)
+instance
+ by standard (auto simp: field_bit_defs split: bit.split)
end
--- a/src/HOL/Library/Cardinality.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Cardinality.thy Mon Jul 06 22:57:34 2015 +0200
@@ -228,19 +228,21 @@
instantiation natural :: card_UNIV begin
definition "finite_UNIV = Phantom(natural) False"
definition "card_UNIV = Phantom(natural) 0"
-instance proof
-qed (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
- type_definition.univ [OF type_definition_natural] natural_eq_iff
- dest!: finite_imageD intro: inj_onI)
+instance
+ by standard
+ (auto simp add: finite_UNIV_natural_def card_UNIV_natural_def card_eq_0_iff
+ type_definition.univ [OF type_definition_natural] natural_eq_iff
+ dest!: finite_imageD intro: inj_onI)
end
instantiation integer :: card_UNIV begin
definition "finite_UNIV = Phantom(integer) False"
definition "card_UNIV = Phantom(integer) 0"
-instance proof
-qed (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
- type_definition.univ [OF type_definition_integer] infinite_UNIV_int
- dest!: finite_imageD intro: inj_onI)
+instance
+ by standard
+ (auto simp add: finite_UNIV_integer_def card_UNIV_integer_def card_eq_0_iff
+ type_definition.univ [OF type_definition_integer] infinite_UNIV_int
+ dest!: finite_imageD intro: inj_onI)
end
instantiation list :: (type) card_UNIV begin
--- a/src/HOL/Library/Char_ord.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Char_ord.thy Mon Jul 06 22:57:34 2015 +0200
@@ -11,42 +11,33 @@
instantiation nibble :: linorder
begin
-definition
- "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+definition "n \<le> m \<longleftrightarrow> nat_of_nibble n \<le> nat_of_nibble m"
+definition "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
-definition
- "n < m \<longleftrightarrow> nat_of_nibble n < nat_of_nibble m"
-
-instance proof
-qed (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
+instance
+ by standard (auto simp add: less_eq_nibble_def less_nibble_def not_le nat_of_nibble_eq_iff)
end
instantiation nibble :: distrib_lattice
begin
-definition
- "(inf \<Colon> nibble \<Rightarrow> _) = min"
+definition "(inf \<Colon> nibble \<Rightarrow> _) = min"
+definition "(sup \<Colon> nibble \<Rightarrow> _) = max"
-definition
- "(sup \<Colon> nibble \<Rightarrow> _) = max"
-
-instance proof
-qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
+instance
+ by standard (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2)
end
instantiation char :: linorder
begin
-definition
- "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
+definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
+definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
-definition
- "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
-
-instance proof
-qed (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
+instance
+ by standard (auto simp add: less_eq_char_def less_char_def nat_of_char_eq_iff)
end
@@ -83,14 +74,11 @@
instantiation char :: distrib_lattice
begin
-definition
- "(inf \<Colon> char \<Rightarrow> _) = min"
+definition "(inf \<Colon> char \<Rightarrow> _) = min"
+definition "(sup \<Colon> char \<Rightarrow> _) = max"
-definition
- "(sup \<Colon> char \<Rightarrow> _) = max"
-
-instance proof
-qed (auto simp add: inf_char_def sup_char_def max_min_distrib2)
+instance
+ by standard (auto simp add: inf_char_def sup_char_def max_min_distrib2)
end
--- a/src/HOL/Library/Countable_Set_Type.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy Mon Jul 06 22:57:34 2015 +0200
@@ -94,7 +94,8 @@
lift_definition minus_cset :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset"
is minus parametric Diff_transfer by simp
-instance by default(transfer, fastforce)+
+instance by standard (transfer; auto)+
+
end
abbreviation cempty :: "'a cset" where "cempty \<equiv> bot"
@@ -536,14 +537,15 @@
lemma finite_countable_subset:
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
-apply default
+apply (rule iffI)
apply (erule contrapos_pp)
apply (rule card_of_ordLeq_infinite)
apply (rule ordLeq_countable_subsets)
apply assumption
apply (rule finite_Collect_conjI)
apply (rule disjI1)
-by (erule finite_Collect_subsets)
+apply (erule finite_Collect_subsets)
+done
lemma rcset_to_rcset: "countable A \<Longrightarrow> rcset (the_inv rcset A) = A"
including cset.lifting
--- a/src/HOL/Library/DAList.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/DAList.thy Mon Jul 06 22:57:34 2015 +0200
@@ -93,7 +93,7 @@
definition "HOL.equal (xs :: ('a, 'b) alist) ys == impl_of xs = impl_of ys"
instance
- by default (simp add: equal_alist_def impl_of_inject)
+ by standard (simp add: equal_alist_def impl_of_inject)
end
--- a/src/HOL/Library/DAList_Multiset.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/DAList_Multiset.thy Mon Jul 06 22:57:34 2015 +0200
@@ -390,7 +390,7 @@
lemma size_fold: "size A = fold_mset (\<lambda>_. Suc) 0 A" (is "_ = fold_mset ?f _ _")
proof -
- interpret comp_fun_commute ?f by default auto
+ interpret comp_fun_commute ?f by standard auto
show ?thesis by (induct A) auto
qed
@@ -405,7 +405,7 @@
lemma set_mset_fold: "set_mset A = fold_mset insert {} A" (is "_ = fold_mset ?f _ _")
proof -
- interpret comp_fun_commute ?f by default auto
+ interpret comp_fun_commute ?f by standard auto
show ?thesis by (induct A) auto
qed
--- a/src/HOL/Library/Dlist.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Dlist.thy Mon Jul 06 22:57:34 2015 +0200
@@ -120,15 +120,14 @@
definition "HOL.equal dxs dys \<longleftrightarrow> HOL.equal (list_of_dlist dxs) (list_of_dlist dys)"
-instance proof
-qed (simp add: equal_dlist_def equal list_of_dlist_inject)
+instance
+ by standard (simp add: equal_dlist_def equal list_of_dlist_inject)
end
declare equal_dlist_def [code]
-lemma [code nbe]:
- "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
+lemma [code nbe]: "HOL.equal (dxs :: 'a::equal dlist) dxs \<longleftrightarrow> True"
by (fact equal_refl)
--- a/src/HOL/Library/Extended_Nat.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Mon Jul 06 22:57:34 2015 +0200
@@ -34,8 +34,10 @@
instantiation enat :: infinity
begin
- definition "\<infinity> = Abs_enat None"
- instance proof qed
+
+definition "\<infinity> = Abs_enat None"
+instance ..
+
end
instance enat :: countable
@@ -156,7 +158,8 @@
and "q + \<infinity> = \<infinity>"
by (simp_all add: plus_enat_def split: enat.splits)
-instance proof
+instance
+proof
fix n m q :: enat
show "n + m + q = n + (m + q)"
by (cases n m q rule: enat3_cases) auto
@@ -203,7 +206,8 @@
unfolding times_enat_def zero_enat_def
by (simp_all split: enat.split)
-instance proof
+instance
+proof
fix a b c :: enat
show "(a * b) * c = a * (b * c)"
unfolding times_enat_def zero_enat_def
@@ -242,7 +246,8 @@
apply (simp add: plus_1_eSuc eSuc_enat)
done
-instance enat :: semiring_char_0 proof
+instance enat :: semiring_char_0
+proof
have "inj enat" by (rule injI) simp
then show "inj (\<lambda>n. of_nat n :: enat)" by (simp add: of_nat_eq_enat)
qed
@@ -355,8 +360,8 @@
"(\<infinity>::enat) < q \<longleftrightarrow> False"
by simp_all
-instance by default
- (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
+instance
+ by standard (auto simp add: less_eq_enat_def less_enat_def plus_enat_def split: enat.splits)
end
@@ -486,14 +491,11 @@
instantiation enat :: "{order_bot, order_top}"
begin
-definition bot_enat :: enat where
- "bot_enat = 0"
+definition bot_enat :: enat where "bot_enat = 0"
+definition top_enat :: enat where "top_enat = \<infinity>"
-definition top_enat :: enat where
- "top_enat = \<infinity>"
-
-instance proof
-qed (simp_all add: bot_enat_def top_enat_def)
+instance
+ by standard (simp_all add: bot_enat_def top_enat_def)
end
@@ -502,10 +504,11 @@
shows "finite A"
proof (rule finite_subset)
show "finite (enat ` {..n})" by blast
-
have "A \<subseteq> {..enat n}" using le_fin by fastforce
also have "\<dots> \<subseteq> enat ` {..n}"
- by (rule subsetI) (case_tac x, auto)
+ apply (rule subsetI)
+ subgoal for x by (cases x) auto
+ done
finally show "A \<subseteq> enat ` {..n}" .
qed
--- a/src/HOL/Library/Extended_Real.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Jul 06 22:57:34 2015 +0200
@@ -257,7 +257,7 @@
| "real_ereal \<infinity> = 0"
| "real_ereal (-\<infinity>) = 0"
by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
instance ..
end
@@ -340,7 +340,7 @@
with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
lemma Infty_neq_0[simp]:
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -509,7 +509,7 @@
using lt_ex gt_ex dense by (cases x y rule: ereal2_cases) auto
instance ereal :: dense_linorder
- by default (blast dest: ereal_dense2)
+ by standard (blast dest: ereal_dense2)
instance ereal :: ordered_ab_semigroup_add
proof
@@ -848,7 +848,7 @@
| "sgn (\<infinity>::ereal) = 1"
| "sgn (-\<infinity>::ereal) = -1"
by (auto intro: ereal_cases)
-termination by default (rule wf_empty)
+termination by standard (rule wf_empty)
function times_ereal where
"ereal r * ereal p = ereal (r * p)"
@@ -1602,7 +1602,7 @@
definition [simp]: "sup x y = (max x y :: ereal)"
definition [simp]: "inf x y = (min x y :: ereal)"
-instance by default simp_all
+instance by standard simp_all
end
@@ -1706,7 +1706,7 @@
open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
instance
- by default (simp add: open_ereal_generated)
+ by standard (simp add: open_ereal_generated)
end
--- a/src/HOL/Library/FSet.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/FSet.thy Mon Jul 06 22:57:34 2015 +0200
@@ -23,7 +23,7 @@
(* FIXME transfer and right_total vs. bi_total *)
instantiation fset :: (finite) finite
begin
-instance by default (transfer, simp)
+instance by (standard; transfer; simp)
end
instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}"
@@ -54,7 +54,7 @@
by simp
instance
-by default (transfer, auto)+
+ by (standard; transfer; auto)+
end
@@ -132,9 +132,12 @@
instantiation fset :: (finite) complete_lattice
begin
-lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer by simp
+lift_definition top_fset :: "'a fset" is UNIV parametric right_total_UNIV_transfer UNIV_transfer
+ by simp
-instance by default (transfer, auto)+
+instance
+ by (standard; transfer; auto)
+
end
instantiation fset :: (finite) complete_boolean_algebra
@@ -143,7 +146,8 @@
lift_definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" is uminus
parametric right_total_Compl_transfer Compl_transfer by simp
-instance by (default, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
+instance
+ by (standard, simp_all only: INF_def SUP_def) (transfer, simp add: Compl_partition Diff_eq)+
end
--- a/src/HOL/Library/Finite_Lattice.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Mon Jul 06 22:57:34 2015 +0200
@@ -32,13 +32,13 @@
by (auto simp: bot_def intro: Inf_fin.coboundedI)
instance finite_lattice_complete \<subseteq> order_bot
- by default (auto simp: finite_lattice_complete_bot_least)
+ by standard (auto simp: finite_lattice_complete_bot_least)
lemma finite_lattice_complete_top_greatest: "(top::'a::finite_lattice_complete) \<ge> x"
by (auto simp: top_def Sup_fin.coboundedI)
instance finite_lattice_complete \<subseteq> order_top
- by default (auto simp: finite_lattice_complete_top_greatest)
+ by standard (auto simp: finite_lattice_complete_top_greatest)
instance finite_lattice_complete \<subseteq> bounded_lattice ..
@@ -124,7 +124,7 @@
by (metis Sup_fold_sup finite_code)
instance prod :: (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
- by default (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
+ by standard (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
text \<open>Functions with a finite domain and with a finite lattice as codomain
already form a finite lattice.\<close>
@@ -146,7 +146,7 @@
by (metis Sup_fold_sup finite_code)
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
- by default (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
+ by standard (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
subsection \<open>Finite Distributive Lattices\<close>
--- a/src/HOL/Library/Float.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Float.thy Mon Jul 06 22:57:34 2015 +0200
@@ -237,8 +237,8 @@
where "sup_float a b = max a b"
instance
- by default
- (transfer, simp_all add: inf_float_def sup_float_def real_of_float_min real_of_float_max)+
+ by (standard; transfer; simp add: inf_float_def sup_float_def real_of_float_min real_of_float_max)
+
end
lemma float_numeral[simp]: "real (numeral x :: float) = numeral x"
--- a/src/HOL/Library/Formal_Power_Series.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Mon Jul 06 22:57:34 2015 +0200
@@ -218,7 +218,7 @@
qed
instance fps :: (zero_neq_one) zero_neq_one
- by default (simp add: expand_fps_eq)
+ by standard (simp add: expand_fps_eq)
instance fps :: (semiring_0) semiring
proof
--- a/src/HOL/Library/Function_Algebras.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Function_Algebras.thy Mon Jul 06 22:57:34 2015 +0200
@@ -62,46 +62,45 @@
text \<open>Additive structures\<close>
instance "fun" :: (type, semigroup_add) semigroup_add
- by default (simp add: fun_eq_iff add.assoc)
+ by standard (simp add: fun_eq_iff add.assoc)
instance "fun" :: (type, cancel_semigroup_add) cancel_semigroup_add
- by default (simp_all add: fun_eq_iff)
+ by standard (simp_all add: fun_eq_iff)
instance "fun" :: (type, ab_semigroup_add) ab_semigroup_add
- by default (simp add: fun_eq_iff add.commute)
+ by standard (simp add: fun_eq_iff add.commute)
instance "fun" :: (type, cancel_ab_semigroup_add) cancel_ab_semigroup_add
- by default (simp_all add: fun_eq_iff diff_diff_eq)
+ by standard (simp_all add: fun_eq_iff diff_diff_eq)
instance "fun" :: (type, monoid_add) monoid_add
- by default (simp_all add: fun_eq_iff)
+ by standard (simp_all add: fun_eq_iff)
instance "fun" :: (type, comm_monoid_add) comm_monoid_add
- by default simp
+ by standard simp
instance "fun" :: (type, cancel_comm_monoid_add) cancel_comm_monoid_add ..
instance "fun" :: (type, group_add) group_add
- by default
- (simp_all add: fun_eq_iff)
+ by standard (simp_all add: fun_eq_iff)
instance "fun" :: (type, ab_group_add) ab_group_add
- by default simp_all
+ by standard simp_all
text \<open>Multiplicative structures\<close>
instance "fun" :: (type, semigroup_mult) semigroup_mult
- by default (simp add: fun_eq_iff mult.assoc)
+ by standard (simp add: fun_eq_iff mult.assoc)
instance "fun" :: (type, ab_semigroup_mult) ab_semigroup_mult
- by default (simp add: fun_eq_iff mult.commute)
+ by standard (simp add: fun_eq_iff mult.commute)
instance "fun" :: (type, monoid_mult) monoid_mult
- by default (simp_all add: fun_eq_iff)
+ by standard (simp_all add: fun_eq_iff)
instance "fun" :: (type, comm_monoid_mult) comm_monoid_mult
- by default simp
+ by standard simp
text \<open>Misc\<close>
@@ -109,19 +108,19 @@
instance "fun" :: (type, "Rings.dvd") "Rings.dvd" ..
instance "fun" :: (type, mult_zero) mult_zero
- by default (simp_all add: fun_eq_iff)
+ by standard (simp_all add: fun_eq_iff)
instance "fun" :: (type, zero_neq_one) zero_neq_one
- by default (simp add: fun_eq_iff)
+ by standard (simp add: fun_eq_iff)
text \<open>Ring structures\<close>
instance "fun" :: (type, semiring) semiring
- by default (simp_all add: fun_eq_iff algebra_simps)
+ by standard (simp_all add: fun_eq_iff algebra_simps)
instance "fun" :: (type, comm_semiring) comm_semiring
- by default (simp add: fun_eq_iff algebra_simps)
+ by standard (simp add: fun_eq_iff algebra_simps)
instance "fun" :: (type, semiring_0) semiring_0 ..
@@ -155,7 +154,7 @@
instance "fun" :: (type, semiring_1_cancel) semiring_1_cancel ..
instance "fun" :: (type, comm_semiring_1_cancel) comm_semiring_1_cancel
- by default (auto simp add: times_fun_def algebra_simps)
+ by standard (auto simp add: times_fun_def algebra_simps)
instance "fun" :: (type, semiring_char_0) semiring_char_0
proof
@@ -180,23 +179,22 @@
text \<open>Ordered structures\<close>
instance "fun" :: (type, ordered_ab_semigroup_add) ordered_ab_semigroup_add
- by default (auto simp add: le_fun_def intro: add_left_mono)
+ by standard (auto simp add: le_fun_def intro: add_left_mono)
instance "fun" :: (type, ordered_cancel_ab_semigroup_add) ordered_cancel_ab_semigroup_add ..
instance "fun" :: (type, ordered_ab_semigroup_add_imp_le) ordered_ab_semigroup_add_imp_le
- by default (simp add: le_fun_def)
+ by standard (simp add: le_fun_def)
instance "fun" :: (type, ordered_comm_monoid_add) ordered_comm_monoid_add ..
instance "fun" :: (type, ordered_ab_group_add) ordered_ab_group_add ..
instance "fun" :: (type, ordered_semiring) ordered_semiring
- by default
- (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
+ by standard (auto simp add: le_fun_def intro: mult_left_mono mult_right_mono)
instance "fun" :: (type, ordered_comm_semiring) ordered_comm_semiring
- by default (fact mult_left_mono)
+ by standard (fact mult_left_mono)
instance "fun" :: (type, ordered_cancel_semiring) ordered_cancel_semiring ..
--- a/src/HOL/Library/Inner_Product.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Inner_Product.thy Mon Jul 06 22:57:34 2015 +0200
@@ -199,6 +199,7 @@
"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"
unfolding differentiable_def by (blast intro: has_derivative_inner)
+
subsection \<open>Class instances\<close>
instantiation real :: real_inner
@@ -206,7 +207,8 @@
definition inner_real_def [simp]: "inner = op *"
-instance proof
+instance
+proof
fix x y z r :: real
show "inner x y = inner y x"
unfolding inner_real_def by (rule mult.commute)
@@ -230,7 +232,8 @@
definition inner_complex_def:
"inner x y = Re x * Re y + Im x * Im y"
-instance proof
+instance
+proof
fix x y z :: complex and r :: real
show "inner x y = inner y x"
unfolding inner_complex_def by (simp add: mult.commute)
--- a/src/HOL/Library/Lattice_Constructions.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Mon Jul 06 22:57:34 2015 +0200
@@ -51,16 +51,16 @@
by (simp add: less_bot_def)
instance
- by default
+ by standard
(auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
end
instance bot :: (order) order
- by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+ by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
instance bot :: (linorder) linorder
- by default (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+ by standard (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
instantiation bot :: (order) bot
begin
@@ -88,7 +88,7 @@
| Value v' \<Rightarrow> Value (inf v v')))"
instance
- by default (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
+ by standard (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
end
@@ -106,7 +106,7 @@
| Value v' \<Rightarrow> Value (sup v v')))"
instance
- by default (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
+ by standard (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
end
@@ -158,16 +158,16 @@
by (simp add: less_top_def)
instance
- by default
+ by standard
(auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
end
instance top :: (order) order
- by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
+ by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
instance top :: (linorder) linorder
- by default (auto simp add: less_eq_top_def less_top_def split: top.splits)
+ by standard (auto simp add: less_eq_top_def less_top_def split: top.splits)
instantiation top :: (order) top
begin
@@ -195,7 +195,7 @@
| Value v' \<Rightarrow> Value (inf v v')))"
instance
- by default (auto simp add: inf_top_def less_eq_top_def split: top.splits)
+ by standard (auto simp add: inf_top_def less_eq_top_def split: top.splits)
end
@@ -213,12 +213,12 @@
| Value v' \<Rightarrow> Value (sup v v')))"
instance
- by default (auto simp add: sup_top_def less_eq_top_def split: top.splits)
+ by standard (auto simp add: sup_top_def less_eq_top_def split: top.splits)
end
instance top :: (lattice) bounded_lattice_top
- by default (simp add: top_top_def)
+ by standard (simp add: top_top_def)
subsection \<open>Values extended by a top and a bottom element\<close>
@@ -267,7 +267,7 @@
by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
instance
- by default
+ by standard
(auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def
split: flat_complete_lattice.splits)
@@ -313,7 +313,7 @@
| Top \<Rightarrow> Top)"
instance
- by default
+ by standard
(auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def
less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
--- a/src/HOL/Library/List_lexord.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/List_lexord.thy Mon Jul 06 22:57:34 2015 +0200
@@ -74,7 +74,7 @@
definition "(sup \<Colon> 'a list \<Rightarrow> _) = max"
instance
- by default (auto simp add: inf_list_def sup_list_def max_min_distrib2)
+ by standard (auto simp add: inf_list_def sup_list_def max_min_distrib2)
end
@@ -102,7 +102,7 @@
definition "bot = []"
instance
- by default (simp add: bot_list_def)
+ by standard (simp add: bot_list_def)
end
--- a/src/HOL/Library/Mapping.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Mapping.thy Mon Jul 06 22:57:34 2015 +0200
@@ -183,8 +183,8 @@
definition
"HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
-instance proof
-qed (unfold equal_mapping_def, transfer, auto)
+instance
+ by standard (unfold equal_mapping_def, transfer, auto)
end
--- a/src/HOL/Library/Multiset_Order.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Multiset_Order.thy Mon Jul 06 22:57:34 2015 +0200
@@ -62,7 +62,7 @@
have trans: "\<And>K M N :: 'a multiset. ?less K M \<Longrightarrow> ?less M N \<Longrightarrow> ?less K N"
unfolding mult_def by (blast intro: trancl_trans)
show "class.order ?le ?less"
- by default (auto simp add: le_multiset_def irrefl dest: trans)
+ by standard (auto simp add: le_multiset_def irrefl dest: trans)
qed
text \<open>The Dershowitz--Manna ordering:\<close>
--- a/src/HOL/Library/Numeral_Type.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Mon Jul 06 22:57:34 2015 +0200
@@ -192,8 +192,8 @@
lemma num1_eq_iff: "(x::num1) = (y::num1) \<longleftrightarrow> True"
by (induct x, induct y) simp
-instance proof
-qed (simp_all add: num1_eq_iff)
+instance
+ by standard (simp_all add: num1_eq_iff)
end
--- a/src/HOL/Library/Option_ord.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Option_ord.thy Mon Jul 06 22:57:34 2015 +0200
@@ -62,59 +62,61 @@
lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
by (simp add: less_option_def)
-instance proof
-qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
-
-end
+instance
+ by standard
+ (auto simp add: less_eq_option_def less_option_def less_le_not_le
+ elim: order_trans split: option.splits)
-instance option :: (order) order proof
-qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+end
-instance option :: (linorder) linorder proof
-qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order
+ by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder
+ by standard (auto simp add: less_eq_option_def less_option_def split: option.splits)
instantiation option :: (order) order_bot
begin
-definition bot_option where
- "\<bottom> = None"
+definition bot_option where "\<bottom> = None"
-instance proof
-qed (simp add: bot_option_def)
+instance
+ by standard (simp add: bot_option_def)
end
instantiation option :: (order_top) order_top
begin
-definition top_option where
- "\<top> = Some \<top>"
+definition top_option where "\<top> = Some \<top>"
-instance proof
-qed (simp add: top_option_def less_eq_option_def split: option.split)
+instance
+ by standard (simp add: top_option_def less_eq_option_def split: option.split)
end
-instance option :: (wellorder) wellorder proof
- fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+instance option :: (wellorder) wellorder
+proof
+ fix P :: "'a option \<Rightarrow> bool"
+ fix z :: "'a option"
assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
have "P None" by (rule H) simp
- then have P_Some [case_names Some]:
- "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
- proof -
- fix z
- assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
- with \<open>P None\<close> show "P z" by (cases z) simp_all
- qed
- show "P z" proof (cases z rule: P_Some)
+ then have P_Some [case_names Some]: "P z" if "\<And>x. z = Some x \<Longrightarrow> (P o Some) x" for z
+ using \<open>P None\<close> that by (cases z) simp_all
+ show "P z"
+ proof (cases z rule: P_Some)
case (Some w)
- show "(P o Some) w" proof (induct rule: less_induct)
+ show "(P o Some) w"
+ proof (induct rule: less_induct)
case (less x)
- have "P (Some x)" proof (rule H)
+ have "P (Some x)"
+ proof (rule H)
fix y :: "'a option"
assume "y < Some x"
- show "P y" proof (cases y rule: P_Some)
- case (Some v) with \<open>y < Some x\<close> have "v < x" by simp
+ show "P y"
+ proof (cases y rule: P_Some)
+ case (Some v)
+ with \<open>y < Some x\<close> have "v < x" by simp
with less show "(P o Some) v" .
qed
qed
@@ -129,16 +131,13 @@
definition inf_option where
"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)))"
-lemma inf_None_1 [simp, code]:
- "None \<sqinter> y = None"
+lemma inf_None_1 [simp, code]: "None \<sqinter> y = None"
by (simp add: inf_option_def)
-lemma inf_None_2 [simp, code]:
- "x \<sqinter> None = None"
+lemma inf_None_2 [simp, code]: "x \<sqinter> None = None"
by (cases x) (simp_all add: inf_option_def)
-lemma inf_Some [simp, code]:
- "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
+lemma inf_Some [simp, code]: "Some x \<sqinter> Some y = Some (x \<sqinter> y)"
by (simp add: inf_option_def)
instance ..
@@ -151,53 +150,42 @@
definition sup_option where
"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)))"
-lemma sup_None_1 [simp, code]:
- "None \<squnion> y = y"
+lemma sup_None_1 [simp, code]: "None \<squnion> y = y"
by (simp add: sup_option_def)
-lemma sup_None_2 [simp, code]:
- "x \<squnion> None = x"
+lemma sup_None_2 [simp, code]: "x \<squnion> None = x"
by (cases x) (simp_all add: sup_option_def)
-lemma sup_Some [simp, code]:
- "Some x \<squnion> Some y = Some (x \<squnion> y)"
+lemma sup_Some [simp, code]: "Some x \<squnion> Some y = Some (x \<squnion> y)"
by (simp add: sup_option_def)
instance ..
end
-instantiation option :: (semilattice_inf) semilattice_inf
-begin
-
-instance proof
+instance option :: (semilattice_inf) semilattice_inf
+proof
fix x y z :: "'a option"
show "x \<sqinter> y \<le> x"
- by - (cases x, simp_all, cases y, simp_all)
+ by (cases x, simp_all, cases y, simp_all)
show "x \<sqinter> y \<le> y"
- by - (cases x, simp_all, cases y, simp_all)
+ by (cases x, simp_all, cases y, simp_all)
show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<sqinter> z"
- by - (cases x, simp_all, cases y, simp_all, cases z, simp_all)
+ by (cases x, simp_all, cases y, simp_all, cases z, simp_all)
qed
-
-end
-instantiation option :: (semilattice_sup) semilattice_sup
-begin
-
-instance proof
+instance option :: (semilattice_sup) semilattice_sup
+proof
fix x y z :: "'a option"
show "x \<le> x \<squnion> y"
- by - (cases x, simp_all, cases y, simp_all)
+ by (cases x, simp_all, cases y, simp_all)
show "y \<le> x \<squnion> y"
- by - (cases x, simp_all, cases y, simp_all)
+ by (cases x, simp_all, cases y, simp_all)
fix x y z :: "'a option"
show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<squnion> z \<le> x"
- by - (cases y, simp_all, cases z, simp_all, cases x, simp_all)
+ by (cases y, simp_all, cases z, simp_all, cases x, simp_all)
qed
-end
-
instance option :: (lattice) lattice ..
instance option :: (lattice) bounded_lattice_bot ..
@@ -210,8 +198,8 @@
proof
fix x y z :: "'a option"
show "x \<squnion> y \<sqinter> z = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
- by - (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
-qed
+ by (cases x, simp_all, cases y, simp_all, cases z, simp_all add: sup_inf_distrib1 inf_commute)
+qed
instantiation option :: (complete_lattice) complete_lattice
begin
@@ -219,22 +207,20 @@
definition Inf_option :: "'a option set \<Rightarrow> 'a option" where
"\<Sqinter>A = (if None \<in> A then None else Some (\<Sqinter>Option.these A))"
-lemma None_in_Inf [simp]:
- "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
+lemma None_in_Inf [simp]: "None \<in> A \<Longrightarrow> \<Sqinter>A = None"
by (simp add: Inf_option_def)
definition Sup_option :: "'a option set \<Rightarrow> 'a option" where
"\<Squnion>A = (if A = {} \<or> A = {None} then None else Some (\<Squnion>Option.these A))"
-lemma empty_Sup [simp]:
- "\<Squnion>{} = None"
+lemma empty_Sup [simp]: "\<Squnion>{} = None"
by (simp add: Sup_option_def)
-lemma singleton_None_Sup [simp]:
- "\<Squnion>{None} = None"
+lemma singleton_None_Sup [simp]: "\<Squnion>{None} = None"
by (simp add: Sup_option_def)
-instance proof
+instance
+proof
fix x :: "'a option" and A
assume "x \<in> A"
then show "\<Sqinter>A \<le> x"
@@ -274,10 +260,9 @@
qed
next
show "\<Squnion>{} = (\<bottom>::'a option)"
- by (auto simp: bot_option_def)
-next
+ by (auto simp: bot_option_def)
show "\<Sqinter>{} = (\<top>::'a option)"
- by (auto simp: top_option_def Inf_option_def)
+ by (auto simp: top_option_def Inf_option_def)
qed
end
@@ -298,10 +283,8 @@
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
using Some_Sup [of "f ` A"] by (simp add: comp_def)
-instantiation option :: (complete_distrib_lattice) complete_distrib_lattice
-begin
-
-instance proof
+instance option :: (complete_distrib_lattice) complete_distrib_lattice
+proof
fix a :: "'a option" and B
show "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
proof (cases a)
@@ -354,14 +337,7 @@
qed
qed
-end
-
-instantiation option :: (complete_linorder) complete_linorder
-begin
-
-instance ..
-
-end
+instance option :: (complete_linorder) complete_linorder ..
no_notation
@@ -379,4 +355,3 @@
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
end
-
--- a/src/HOL/Library/Polynomial.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy Mon Jul 06 22:57:34 2015 +0200
@@ -392,13 +392,12 @@
definition
[code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)"
-instance proof
-qed (simp add: equal equal_poly_def coeffs_eq_iff)
+instance
+ by standard (simp add: equal equal_poly_def coeffs_eq_iff)
end
-lemma [code nbe]:
- "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
+lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True"
by (fact equal_refl)
definition is_zero :: "'a::zero poly \<Rightarrow> bool"
@@ -510,15 +509,16 @@
lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
is "\<lambda>p q n. coeff p n + coeff q n"
proof -
- fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
+ fix q p :: "'a poly"
+ show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed
-lemma coeff_add [simp]:
- "coeff (p + q) n = coeff p n + coeff q n"
+lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
by (simp add: plus_poly.rep_eq)
-instance proof
+instance
+proof
fix p q r :: "'a poly"
show "(p + q) + r = p + (q + r)"
by (simp add: poly_eq_iff add.assoc)
@@ -536,15 +536,16 @@
lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
is "\<lambda>p q n. coeff p n - coeff q n"
proof -
- fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
+ fix q p :: "'a poly"
+ show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed
-lemma coeff_diff [simp]:
- "coeff (p - q) n = coeff p n - coeff q n"
+lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
by (simp add: minus_poly.rep_eq)
-instance proof
+instance
+proof
fix p q r :: "'a poly"
show "p + q - p = q"
by (simp add: poly_eq_iff)
@@ -560,14 +561,16 @@
lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
is "\<lambda>p n. - coeff p n"
proof -
- fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
+ fix p :: "'a poly"
+ show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
using MOST_coeff_eq_0 by simp
qed
lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
by (simp add: uminus_poly.rep_eq)
-instance proof
+instance
+proof
fix p q :: "'a poly"
show "- p + p = 0"
by (simp add: poly_eq_iff)
@@ -663,7 +666,8 @@
{ fix xs ys :: "'a list" and n
have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
- case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def)
+ case (3 x xs y ys n)
+ then show ?case by (cases n) (auto simp add: cCons_def)
qed simp_all }
note * = this
{ fix xs ys :: "'a list"
@@ -825,7 +829,8 @@
shows "(p + q) * r = p * r + q * r"
by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps)
-instance proof
+instance
+proof
fix p q r :: "'a poly"
show 0: "0 * p = 0"
by (rule mult_poly_0_left)
@@ -861,18 +866,17 @@
done
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
- by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc)
+ by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)
instantiation poly :: (comm_semiring_1) comm_semiring_1
begin
-definition one_poly_def:
- "1 = pCons 1 0"
+definition one_poly_def: "1 = pCons 1 0"
-instance proof
- fix p :: "'a poly" show "1 * p = p"
+instance
+proof
+ show "1 * p = p" for p :: "'a poly"
unfolding one_poly_def by simp
-next
show "0 \<noteq> (1::'a poly)"
unfolding one_poly_def by simp
qed
@@ -1063,8 +1067,9 @@
definition
"sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
-instance proof
- fix x y :: "'a poly"
+instance
+proof
+ fix x y z :: "'a poly"
show "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
unfolding less_eq_poly_def less_poly_def
apply safe
@@ -1072,50 +1077,34 @@
apply (drule (1) pos_poly_add)
apply simp
done
-next
- fix x :: "'a poly" show "x \<le> x"
+ show "x \<le> x"
unfolding less_eq_poly_def by simp
-next
- fix x y z :: "'a poly"
- assume "x \<le> y" and "y \<le> z" thus "x \<le> z"
+ show "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
unfolding less_eq_poly_def
apply safe
apply (drule (1) pos_poly_add)
apply (simp add: algebra_simps)
done
-next
- fix x y :: "'a poly"
- assume "x \<le> y" and "y \<le> x" thus "x = y"
+ show "x \<le> y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
unfolding less_eq_poly_def
apply safe
apply (drule (1) pos_poly_add)
apply simp
done
-next
- fix x y z :: "'a poly"
- assume "x \<le> y" thus "z + x \<le> z + y"
+ show "x \<le> y \<Longrightarrow> z + x \<le> z + y"
unfolding less_eq_poly_def
apply safe
apply (simp add: algebra_simps)
done
-next
- fix x y :: "'a poly"
show "x \<le> y \<or> y \<le> x"
unfolding less_eq_poly_def
using pos_poly_total [of "x - y"]
by auto
-next
- fix x y z :: "'a poly"
- assume "x < y" and "0 < z"
- thus "z * x < z * y"
+ show "x < y \<Longrightarrow> 0 < z \<Longrightarrow> z * x < z * y"
unfolding less_poly_def
by (simp add: right_diff_distrib [symmetric] pos_poly_mult)
-next
- fix x :: "'a poly"
show "\<bar>x\<bar> = (if x < 0 then - x else x)"
by (rule abs_poly_def)
-next
- fix x :: "'a poly"
show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
by (rule sgn_poly_def)
qed
@@ -1410,7 +1399,8 @@
by (simp add: div_poly_eq mod_poly_eq)
qed
-instance proof
+instance
+proof
fix x y :: "'a poly"
show "x div y * y + x mod y = x"
using pdivmod_rel [of x y]
--- a/src/HOL/Library/Prefix_Order.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Prefix_Order.thy Mon Jul 06 22:57:34 2015 +0200
@@ -14,7 +14,8 @@
definition "(xs::'a list) \<le> ys \<equiv> prefixeq xs ys"
definition "(xs::'a list) < ys \<equiv> xs \<le> ys \<and> \<not> (ys \<le> xs)"
-instance by (default, unfold less_eq_list_def less_list_def) auto
+instance
+ by standard (auto simp: less_eq_list_def less_list_def)
end
--- a/src/HOL/Library/Product_Lexorder.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Lexorder.thy Mon Jul 06 22:57:34 2015 +0200
@@ -37,13 +37,13 @@
by (auto simp add: less_prod_def le_less)
instance prod :: (preorder, preorder) preorder
- by default (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
+ by standard (auto simp: less_eq_prod_def less_prod_def less_le_not_le intro: order_trans)
instance prod :: (order, order) order
- by default (auto simp add: less_eq_prod_def)
+ by standard (auto simp add: less_eq_prod_def)
instance prod :: (linorder, linorder) linorder
- by default (auto simp: less_eq_prod_def)
+ by standard (auto simp: less_eq_prod_def)
instantiation prod :: (linorder, linorder) distrib_lattice
begin
@@ -55,7 +55,7 @@
"(sup :: 'a \<times> 'b \<Rightarrow> _ \<Rightarrow> _) = max"
instance
- by default (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
+ by standard (auto simp add: inf_prod_def sup_prod_def max_min_distrib2)
end
@@ -70,7 +70,7 @@
end
instance prod :: (order_bot, order_bot) order_bot
- by default (auto simp add: bot_prod_def)
+ by standard (auto simp add: bot_prod_def)
instantiation prod :: (top, top) top
begin
@@ -83,7 +83,7 @@
end
instance prod :: (order_top, order_top) order_top
- by default (auto simp add: top_prod_def)
+ by standard (auto simp add: top_prod_def)
instance prod :: (wellorder, wellorder) wellorder
proof
--- a/src/HOL/Library/Product_Order.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy Mon Jul 06 22:57:34 2015 +0200
@@ -49,7 +49,7 @@
qed
instance prod :: (order, order) order
- by default auto
+ by standard auto
subsection \<open>Binary infimum and supremum\<close>
@@ -57,8 +57,7 @@
instantiation prod :: (inf, inf) inf
begin
-definition
- "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
+definition "inf x y = (inf (fst x) (fst y), inf (snd x) (snd y))"
lemma inf_Pair_Pair [simp]: "inf (a, b) (c, d) = (inf a c, inf b d)"
unfolding inf_prod_def by simp
@@ -69,11 +68,12 @@
lemma snd_inf [simp]: "snd (inf x y) = inf (snd x) (snd y)"
unfolding inf_prod_def by simp
-instance proof qed
+instance ..
+
end
instance prod :: (semilattice_inf, semilattice_inf) semilattice_inf
- by default auto
+ by standard auto
instantiation prod :: (sup, sup) sup
@@ -91,16 +91,17 @@
lemma snd_sup [simp]: "snd (sup x y) = sup (snd x) (snd y)"
unfolding sup_prod_def by simp
-instance proof qed
+instance ..
+
end
instance prod :: (semilattice_sup, semilattice_sup) semilattice_sup
- by default auto
+ by standard auto
instance prod :: (lattice, lattice) lattice ..
instance prod :: (distrib_lattice, distrib_lattice) distrib_lattice
- by default (auto simp add: sup_inf_distrib1)
+ by standard (auto simp add: sup_inf_distrib1)
subsection \<open>Top and bottom elements\<close>
@@ -125,7 +126,7 @@
unfolding top_prod_def by simp
instance prod :: (order_top, order_top) order_top
- by default (auto simp add: top_prod_def)
+ by standard (auto simp add: top_prod_def)
instantiation prod :: (bot, bot) bot
begin
@@ -147,12 +148,12 @@
unfolding bot_prod_def by simp
instance prod :: (order_bot, order_bot) order_bot
- by default (auto simp add: bot_prod_def)
+ by standard (auto simp add: bot_prod_def)
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
- by default (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+ by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
subsection \<open>Complete lattice operations\<close>
@@ -160,28 +161,28 @@
instantiation prod :: (Inf, Inf) Inf
begin
-definition
- "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
-instance proof qed
+instance ..
+
end
instantiation prod :: (Sup, Sup) Sup
begin
-definition
- "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
-instance proof qed
+instance ..
+
end
instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
conditionally_complete_lattice
- by default (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
+ by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
instance prod :: (complete_lattice, complete_lattice) complete_lattice
- by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
+ by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
@@ -231,9 +232,8 @@
(* Contribution: Alessandro Coglio *)
-instance prod ::
- (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof (default, goals)
+instance prod :: (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
+proof (standard, goals)
case 1
then show ?case
by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
--- a/src/HOL/Library/Product_Vector.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_Vector.thy Mon Jul 06 22:57:34 2015 +0200
@@ -25,7 +25,8 @@
lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)"
unfolding scaleR_prod_def by simp
-instance proof
+instance
+proof
fix a b :: real and x y :: "'a \<times> 'b"
show "scaleR a (x + y) = scaleR a x + scaleR a y"
by (simp add: prod_eq_iff scaleR_right_distrib)
@@ -58,7 +59,8 @@
shows "open S"
using assms unfolding open_prod_def by fast
-instance proof
+instance
+proof
show "open (UNIV :: ('a \<times> 'b) set)"
unfolding open_prod_def by auto
next
@@ -277,7 +279,8 @@
lemma dist_snd_le: "dist (snd x) (snd y) \<le> dist x y"
unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2)
-instance proof
+instance
+proof
fix x y :: "'a \<times> 'b"
show "dist x y = 0 \<longleftrightarrow> x = y"
unfolding dist_prod_def prod_eq_iff by simp
@@ -406,7 +409,8 @@
lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)"
unfolding norm_prod_def by simp
-instance proof
+instance
+proof
fix r :: real and x y :: "'a \<times> 'b"
show "norm x = 0 \<longleftrightarrow> x = 0"
unfolding norm_prod_def
@@ -510,7 +514,8 @@
lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
unfolding inner_prod_def by simp
-instance proof
+instance
+proof
fix r :: real
fix x y z :: "'a::real_inner \<times> 'b::real_inner"
show "inner x y = inner y x"
--- a/src/HOL/Library/Product_plus.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Product_plus.thy Mon Jul 06 22:57:34 2015 +0200
@@ -81,41 +81,56 @@
subsection \<open>Class instances\<close>
instance prod :: (semigroup_add, semigroup_add) semigroup_add
- by default (simp add: prod_eq_iff add.assoc)
+ by standard (simp add: prod_eq_iff add.assoc)
instance prod :: (ab_semigroup_add, ab_semigroup_add) ab_semigroup_add
- by default (simp add: prod_eq_iff add.commute)
+ by standard (simp add: prod_eq_iff add.commute)
instance prod :: (monoid_add, monoid_add) monoid_add
- by default (simp_all add: prod_eq_iff)
+ by standard (simp_all add: prod_eq_iff)
instance prod :: (comm_monoid_add, comm_monoid_add) comm_monoid_add
- by default (simp add: prod_eq_iff)
+ by standard (simp add: prod_eq_iff)
-instance prod ::
- (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
- by default (simp_all add: prod_eq_iff)
+instance prod :: (cancel_semigroup_add, cancel_semigroup_add) cancel_semigroup_add
+ by standard (simp_all add: prod_eq_iff)
-instance prod ::
- (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
- by default (simp_all add: prod_eq_iff diff_diff_eq)
+instance prod :: (cancel_ab_semigroup_add, cancel_ab_semigroup_add) cancel_ab_semigroup_add
+ by standard (simp_all add: prod_eq_iff diff_diff_eq)
-instance prod ::
- (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
+instance prod :: (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add ..
instance prod :: (group_add, group_add) group_add
- by default (simp_all add: prod_eq_iff)
+ by standard (simp_all add: prod_eq_iff)
instance prod :: (ab_group_add, ab_group_add) ab_group_add
- by default (simp_all add: prod_eq_iff)
+ by standard (simp_all add: prod_eq_iff)
lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))"
-by (cases "finite A", induct set: finite, simp_all)
+proof (cases "finite A")
+ case True
+ then show ?thesis by induct simp_all
+next
+ case False
+ then show ?thesis by simp
+qed
lemma snd_setsum: "snd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. snd (f x))"
-by (cases "finite A", induct set: finite, simp_all)
+proof (cases "finite A")
+ case True
+ then show ?thesis by induct simp_all
+next
+ case False
+ then show ?thesis by simp
+qed
lemma setsum_prod: "(\<Sum>x\<in>A. (f x, g x)) = (\<Sum>x\<in>A. f x, \<Sum>x\<in>A. g x)"
-by (cases "finite A", induct set: finite) (simp_all add: zero_prod_def)
+proof (cases "finite A")
+ case True
+ then show ?thesis by induct (simp_all add: zero_prod_def)
+next
+ case False
+ then show ?thesis by (simp add: zero_prod_def)
+qed
end
--- a/src/HOL/Library/RBT_Set.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy Mon Jul 06 22:57:34 2015 +0200
@@ -621,14 +621,17 @@
lemma image_Set [code]:
"image f (Set t) = fold_keys (\<lambda>k A. Set.insert (f k) A) t {}"
proof -
- have "comp_fun_commute (\<lambda>k. Set.insert (f k))" by default auto
- then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
+ have "comp_fun_commute (\<lambda>k. Set.insert (f k))"
+ by standard auto
+ then show ?thesis
+ by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys)
qed
lemma Ball_Set [code]:
"Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
proof -
- have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
+ have "comp_fun_commute (\<lambda>k s. s \<and> P k)"
+ by standard auto
then show ?thesis
by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys)
qed
@@ -636,7 +639,8 @@
lemma Bex_Set [code]:
"Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
proof -
- have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
+ have "comp_fun_commute (\<lambda>k s. s \<or> P k)"
+ by standard auto
then show ?thesis
by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys)
qed
@@ -670,7 +674,8 @@
lemma setsum_Set [code]:
"setsum f (Set xs) = fold_keys (plus o f) xs 0"
proof -
- have "comp_fun_commute (\<lambda>x. op + (f x))" by default (auto simp: ac_simps)
+ have "comp_fun_commute (\<lambda>x. op + (f x))"
+ by standard (auto simp: ac_simps)
then show ?thesis
by (auto simp add: setsum.eq_fold finite_fold_fold_keys o_def)
qed
@@ -695,23 +700,23 @@
by(auto split: rbt.split unit.split color.split)
qed
-lemma Pow_Set [code]:
- "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
-by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
+lemma Pow_Set [code]: "Pow (Set t) = fold_keys (\<lambda>x A. A \<union> Set.insert x ` A) t {{}}"
+ by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold])
lemma product_Set [code]:
"Product_Type.product (Set t1) (Set t2) =
fold_keys (\<lambda>x A. fold_keys (\<lambda>y. Set.insert (x, y)) t2 A) t1 {}"
proof -
- have *:"\<And>x. comp_fun_commute (\<lambda>y. Set.insert (x, y))" by default auto
+ have *: "comp_fun_commute (\<lambda>y. Set.insert (x, y))" for x
+ by standard auto
show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"]
by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *])
qed
-lemma Id_on_Set [code]:
- "Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
+lemma Id_on_Set [code]: "Id_on (Set t) = fold_keys (\<lambda>x. Set.insert (x, x)) t {}"
proof -
- have "comp_fun_commute (\<lambda>x. Set.insert (x, x))" by default auto
+ have "comp_fun_commute (\<lambda>x. Set.insert (x, x))"
+ by standard auto
then show ?thesis
by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys)
qed
@@ -728,10 +733,12 @@
"(Set t1) O (Set t2) = fold_keys
(\<lambda>(x,y) A. fold_keys (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}"
proof -
- interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert)
+ interpret comp_fun_idem Set.insert
+ by (fact comp_fun_idem_insert)
have *: "\<And>x y. comp_fun_commute (\<lambda>(w, z) A'. if y = w then Set.insert (x, z) A' else A')"
- by default (auto simp add: fun_eq_iff)
- show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
+ by standard (auto simp add: fun_eq_iff)
+ show ?thesis
+ using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1]
by (simp add: relcomp_fold finite_fold_fold_keys[OF *])
qed
@@ -759,11 +766,13 @@
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
proof -
- have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+ have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
+ by standard (simp add: fun_eq_iff ac_simps)
then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
then show ?thesis
- by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
+ by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric]
+ r_min_eq_r_min_opt[symmetric] r_min_alt_def)
qed
definition Inf' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Inf' x = Inf x"
@@ -775,7 +784,7 @@
shows "INFIMUM (Set t) f = fold_keys (inf \<circ> f) t top"
proof -
have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
- by default (auto simp add: fun_eq_iff ac_simps)
+ by standard (auto simp add: fun_eq_iff ac_simps)
then show ?thesis
by (auto simp: INF_fold_inf finite_fold_fold_keys)
qed
@@ -800,14 +809,17 @@
fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
proof -
- have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
+ have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)"
+ by standard (simp add: fun_eq_iff ac_simps)
then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
then show ?thesis
- by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
+ by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric]
+ r_max_eq_r_max_opt[symmetric] r_max_alt_def)
qed
-definition Sup' :: "'a :: {linorder, complete_lattice} set \<Rightarrow> 'a" where [code del]: "Sup' x = Sup x"
+definition Sup' :: "'a :: {linorder,complete_lattice} set \<Rightarrow> 'a"
+ where [code del]: "Sup' x = Sup x"
declare Sup'_def[symmetric, code_unfold]
declare Sup_Set_fold[folded Sup'_def, code]
@@ -816,30 +828,34 @@
shows "SUPREMUM (Set t) f = fold_keys (sup \<circ> f) t bot"
proof -
have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)"
- by default (auto simp add: fun_eq_iff ac_simps)
+ by standard (auto simp add: fun_eq_iff ac_simps)
then show ?thesis
by (auto simp: SUP_fold_sup finite_fold_fold_keys)
qed
-lemma sorted_list_set[code]:
- "sorted_list_of_set (Set t) = RBT.keys t"
-by (auto simp add: set_keys intro: sorted_distinct_set_unique)
+lemma sorted_list_set[code]: "sorted_list_of_set (Set t) = RBT.keys t"
+ by (auto simp add: set_keys intro: sorted_distinct_set_unique)
lemma Bleast_code [code]:
- "Bleast (Set t) P = (case filter P (RBT.keys t) of
- x#xs \<Rightarrow> x |
- [] \<Rightarrow> abort_Bleast (Set t) P)"
+ "Bleast (Set t) P =
+ (case filter P (RBT.keys t) of
+ x # xs \<Rightarrow> x
+ | [] \<Rightarrow> abort_Bleast (Set t) P)"
proof (cases "filter P (RBT.keys t)")
- case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
+ case Nil
+ thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
next
case (Cons x ys)
have "(LEAST x. x \<in> Set t \<and> P x) = x"
proof (rule Least_equality)
- show "x \<in> Set t \<and> P x" using Cons[symmetric]
- by(auto simp add: set_keys Cons_eq_filter_iff)
+ show "x \<in> Set t \<and> P x"
+ using Cons[symmetric]
+ by (auto simp add: set_keys Cons_eq_filter_iff)
next
- fix y assume "y : Set t \<and> P y"
- then show "x \<le> y" using Cons[symmetric]
+ fix y
+ assume "y \<in> Set t \<and> P y"
+ then show "x \<le> y"
+ using Cons[symmetric]
by(auto simp add: set_keys Cons_eq_filter_iff)
(metis sorted_Cons sorted_append sorted_keys)
qed
--- a/src/HOL/Library/Saturated.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Saturated.thy Mon Jul 06 22:57:34 2015 +0200
@@ -61,7 +61,8 @@
less_sat_def: "x < y \<longleftrightarrow> nat_of x < nat_of y"
instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+ by standard
+ (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
end
@@ -106,8 +107,9 @@
"nat_of (x * y) = min (nat_of x * nat_of y) (len_of TYPE('a))"
by (simp add: times_sat_def)
-instance proof
- fix a b c :: "('a::len) sat"
+instance
+proof
+ fix a b c :: "'a::len sat"
show "a * b * c = a * (b * c)"
proof(cases "a = 0")
case True thus ?thesis by (simp add: sat_eq_iff)
@@ -120,14 +122,10 @@
by (simp add: sat_eq_iff nat_mult_min_left nat_mult_min_right mult.assoc min.assoc min.absorb2)
qed
qed
-next
- fix a :: "('a::len) sat"
show "1 * a = a"
apply (simp add: sat_eq_iff)
apply (metis One_nat_def len_gt_0 less_Suc0 less_zeroE linorder_not_less min.absorb_iff1 min_nat_of_len_of nat_mult_1_right mult.commute)
done
-next
- fix a b c :: "('a::len) sat"
show "(a + b) * c = a * c + b * c"
proof(cases "c = 0")
case True thus ?thesis by (simp add: sat_eq_iff)
@@ -143,7 +141,8 @@
begin
instance
-by default (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
+ by standard
+ (auto simp add: less_eq_sat_def less_sat_def not_le sat_eq_iff min.coboundedI1 mult.commute)
end
@@ -183,43 +182,33 @@
instantiation sat :: (len) equal
begin
-definition
- "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
+definition "HOL.equal A B \<longleftrightarrow> nat_of A = nat_of B"
-instance proof
-qed (simp add: equal_sat_def nat_of_inject)
+instance
+ by standard (simp add: equal_sat_def nat_of_inject)
end
instantiation sat :: (len) "{bounded_lattice, distrib_lattice}"
begin
-definition
- "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
-
-definition
- "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "(inf :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = min"
+definition "(sup :: 'a sat \<Rightarrow> 'a sat \<Rightarrow> 'a sat) = max"
+definition "bot = (0 :: 'a sat)"
+definition "top = Sat (len_of TYPE('a))"
-definition
- "bot = (0 :: 'a sat)"
-
-definition
- "top = Sat (len_of TYPE('a))"
-
-instance proof
-qed (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
- simp_all add: less_eq_sat_def)
+instance
+ by standard
+ (simp_all add: inf_sat_def sup_sat_def bot_sat_def top_sat_def max_min_distrib2,
+ simp_all add: less_eq_sat_def)
end
instantiation sat :: (len) "{Inf, Sup}"
begin
-definition
- "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
-
-definition
- "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Inf = (semilattice_neutr_set.F min top :: 'a sat set \<Rightarrow> 'a sat)"
+definition "Sup = (semilattice_neutr_set.F max bot :: 'a sat set \<Rightarrow> 'a sat)"
instance ..
@@ -229,16 +218,20 @@
where
"semilattice_neutr_set.F min (top :: 'a sat) = Inf"
proof -
- show "semilattice_neutr_set min (top :: 'a sat)" by default (simp add: min_def)
- show "semilattice_neutr_set.F min (top :: 'a sat) = Inf" by (simp add: Inf_sat_def)
+ show "semilattice_neutr_set min (top :: 'a sat)"
+ by standard (simp add: min_def)
+ show "semilattice_neutr_set.F min (top :: 'a sat) = Inf"
+ by (simp add: Inf_sat_def)
qed
interpretation Sup_sat!: semilattice_neutr_set max "bot :: 'a::len sat"
where
"semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
proof -
- show "semilattice_neutr_set max (bot :: 'a sat)" by default (simp add: max_def bot.extremum_unique)
- show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup" by (simp add: Sup_sat_def)
+ show "semilattice_neutr_set max (bot :: 'a sat)"
+ by standard (simp add: max_def bot.extremum_unique)
+ show "semilattice_neutr_set.F max (bot :: 'a sat) = Sup"
+ by (simp add: Sup_sat_def)
qed
instance sat :: (len) complete_lattice
@@ -271,10 +264,8 @@
next
show "Inf {} = (top::'a sat)"
by (auto simp: top_sat_def)
-next
show "Sup {} = (bot::'a sat)"
by (auto simp: bot_sat_def)
qed
end
-
--- a/src/HOL/Library/Set_Algebras.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Mon Jul 06 22:57:34 2015 +0200
@@ -64,28 +64,28 @@
"x =o A \<equiv> x \<in> A"
instance set :: (semigroup_add) semigroup_add
- by default (force simp add: set_plus_def add.assoc)
+ by standard (force simp add: set_plus_def add.assoc)
instance set :: (ab_semigroup_add) ab_semigroup_add
- by default (force simp add: set_plus_def add.commute)
+ by standard (force simp add: set_plus_def add.commute)
instance set :: (monoid_add) monoid_add
- by default (simp_all add: set_plus_def)
+ by standard (simp_all add: set_plus_def)
instance set :: (comm_monoid_add) comm_monoid_add
- by default (simp_all add: set_plus_def)
+ by standard (simp_all add: set_plus_def)
instance set :: (semigroup_mult) semigroup_mult
- by default (force simp add: set_times_def mult.assoc)
+ by standard (force simp add: set_times_def mult.assoc)
instance set :: (ab_semigroup_mult) ab_semigroup_mult
- by default (force simp add: set_times_def mult.commute)
+ by standard (force simp add: set_times_def mult.commute)
instance set :: (monoid_mult) monoid_mult
- by default (simp_all add: set_times_def)
+ by standard (simp_all add: set_times_def)
instance set :: (comm_monoid_mult) comm_monoid_mult
- by default (simp_all add: set_times_def)
+ by standard (simp_all add: set_times_def)
lemma set_plus_intro [intro]: "a \<in> C \<Longrightarrow> b \<in> D \<Longrightarrow> a + b \<in> C + D"
by (auto simp add: set_plus_def)
--- a/src/HOL/Library/Sublist.thy Mon Jul 06 22:06:02 2015 +0200
+++ b/src/HOL/Library/Sublist.thy Mon Jul 06 22:57:34 2015 +0200
@@ -18,10 +18,10 @@
where "prefix xs ys \<longleftrightarrow> prefixeq xs ys \<and> xs \<noteq> ys"
interpretation prefix_order: order prefixeq prefix
- by default (auto simp: prefixeq_def prefix_def)
+ by standard (auto simp: prefixeq_def prefix_def)
interpretation prefix_bot: order_bot Nil prefixeq prefix
- by default (simp add: prefixeq_def)
+ by standard (simp add: prefixeq_def)
lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
unfolding prefixeq_def by blast