--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Fri Dec 27 14:35:14 2013 +0100
@@ -452,8 +452,9 @@
fixes between
assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
and between_same: "between x x = x"
+begin
-sublocale constr_dense_linorder < dlo: unbounded_dense_linorder
+sublocale dlo: unbounded_dense_linorder
apply unfold_locales
using gt_ex lt_ex between_less
apply auto
@@ -461,9 +462,6 @@
apply simp
done
-context constr_dense_linorder
-begin
-
lemma rinf_U[no_atp]:
assumes fU: "finite U"
and lin_dense: "\<forall>x l u. (\<forall> t. l \<sqsubset> t \<and> t\<sqsubset> u \<longrightarrow> t \<notin> U) \<and> l\<sqsubset> x \<and> x \<sqsubset> u \<and> P x
--- a/src/HOL/Groups.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Groups.thy Fri Dec 27 14:35:14 2013 +0100
@@ -90,10 +90,13 @@
locale comm_monoid = abel_semigroup +
fixes z :: 'a ("1")
assumes comm_neutral: "a * 1 = a"
+begin
-sublocale comm_monoid < monoid
+sublocale monoid
by default (simp_all add: commute comm_neutral)
+end
+
subsection {* Generic operations *}
@@ -148,19 +151,20 @@
class semigroup_add = plus +
assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
+begin
-sublocale semigroup_add < add!: semigroup plus
+sublocale add!: semigroup plus
by default (fact add_assoc)
+end
+
class ab_semigroup_add = semigroup_add +
assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
+begin
-sublocale ab_semigroup_add < add!: abel_semigroup plus
+sublocale add!: abel_semigroup plus
by default (fact add_commute)
-context ab_semigroup_add
-begin
-
lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
theorems add_ac = add_assoc add_commute add_left_commute
@@ -171,19 +175,20 @@
class semigroup_mult = times +
assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
+begin
-sublocale semigroup_mult < mult!: semigroup times
+sublocale mult!: semigroup times
by default (fact mult_assoc)
+end
+
class ab_semigroup_mult = semigroup_mult +
assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
+begin
-sublocale ab_semigroup_mult < mult!: abel_semigroup times
+sublocale mult!: abel_semigroup times
by default (fact mult_commute)
-context ab_semigroup_mult
-begin
-
lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
theorems mult_ac = mult_assoc mult_commute mult_left_commute
@@ -195,22 +200,28 @@
class monoid_add = zero + semigroup_add +
assumes add_0_left: "0 + a = a"
and add_0_right: "a + 0 = a"
+begin
-sublocale monoid_add < add!: monoid plus 0
+sublocale add!: monoid plus 0
by default (fact add_0_left add_0_right)+
+end
+
lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
-by (rule eq_commute)
+ by (fact eq_commute)
class comm_monoid_add = zero + ab_semigroup_add +
assumes add_0: "0 + a = a"
+begin
-sublocale comm_monoid_add < add!: comm_monoid plus 0
+sublocale add!: comm_monoid plus 0
by default (insert add_0, simp add: ac_simps)
-subclass (in comm_monoid_add) monoid_add
+subclass monoid_add
by default (fact add.left_neutral add.right_neutral)+
+end
+
class comm_monoid_diff = comm_monoid_add + minus +
assumes diff_zero [simp]: "a - 0 = a"
and zero_diff [simp]: "0 - a = 0"
@@ -265,22 +276,28 @@
class monoid_mult = one + semigroup_mult +
assumes mult_1_left: "1 * a = a"
and mult_1_right: "a * 1 = a"
+begin
-sublocale monoid_mult < mult!: monoid times 1
+sublocale mult!: monoid times 1
by default (fact mult_1_left mult_1_right)+
+end
+
lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
-by (rule eq_commute)
+ by (fact eq_commute)
class comm_monoid_mult = one + ab_semigroup_mult +
assumes mult_1: "1 * a = a"
+begin
-sublocale comm_monoid_mult < mult!: comm_monoid times 1
+sublocale mult!: comm_monoid times 1
by default (insert mult_1, simp add: ac_simps)
-subclass (in comm_monoid_mult) monoid_mult
+subclass monoid_mult
by default (fact mult.left_neutral mult.right_neutral)+
+end
+
class cancel_semigroup_add = semigroup_add +
assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
--- a/src/HOL/Lattices_Big.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Lattices_Big.thy Fri Dec 27 14:35:14 2013 +0100
@@ -308,15 +308,14 @@
subsection {* Lattice operations on finite sets *}
-definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
+context semilattice_inf
+begin
+
+definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
where
"Inf_fin = semilattice_set.F inf"
-definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
-where
- "Sup_fin = semilattice_set.F sup"
-
-sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
+sublocale Inf_fin!: semilattice_order_set inf less_eq less
where
"semilattice_set.F inf = Inf_fin"
proof -
@@ -325,7 +324,16 @@
from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
qed
-sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
+end
+
+context semilattice_sup
+begin
+
+definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
+where
+ "Sup_fin = semilattice_set.F sup"
+
+sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
where
"semilattice_set.F sup = Sup_fin"
proof -
@@ -334,13 +342,11 @@
from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
qed
+end
+
subsection {* Infimum and Supremum over non-empty sets *}
-text {*
- After this non-regular bootstrap, things continue canonically.
-*}
-
context lattice
begin
@@ -449,7 +455,7 @@
lemma Inf_fin_Inf:
assumes "finite A" and "A \<noteq> {}"
- shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
+ shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
@@ -458,7 +464,7 @@
lemma Sup_fin_Sup:
assumes "finite A" and "A \<noteq> {}"
- shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
+ shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
proof -
from assms obtain b B where "A = insert b B" and "finite B" by auto
then show ?thesis
--- a/src/HOL/Library/Boolean_Algebra.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy Fri Dec 27 14:35:14 2013 +0100
@@ -24,16 +24,14 @@
assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
+begin
-sublocale boolean < conj!: abel_semigroup conj proof
+sublocale conj!: abel_semigroup conj proof
qed (fact conj_assoc conj_commute)+
-sublocale boolean < disj!: abel_semigroup disj proof
+sublocale disj!: abel_semigroup disj proof
qed (fact disj_assoc disj_commute)+
-context boolean
-begin
-
lemmas conj_left_commute = conj.left_commute
lemmas disj_left_commute = disj.left_commute
@@ -185,8 +183,9 @@
locale boolean_xor = boolean +
fixes xor :: "'a => 'a => 'a" (infixr "\<oplus>" 65)
assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
+begin
-sublocale boolean_xor < xor!: abel_semigroup xor proof
+sublocale xor!: abel_semigroup xor proof
fix x y z :: 'a
let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
(\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
@@ -201,9 +200,6 @@
by (simp only: xor_def conj_commute disj_commute)
qed
-context boolean_xor
-begin
-
lemmas xor_assoc = xor.assoc
lemmas xor_commute = xor.commute
lemmas xor_left_commute = xor.left_commute
--- a/src/HOL/Library/Multiset.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Library/Multiset.thy Fri Dec 27 14:35:14 2013 +0100
@@ -1159,15 +1159,14 @@
notation times (infixl "*" 70)
notation Groups.one ("1")
-definition (in comm_monoid_add) msetsum :: "'a multiset \<Rightarrow> 'a"
+context comm_monoid_add
+begin
+
+definition msetsum :: "'a multiset \<Rightarrow> 'a"
where
"msetsum = comm_monoid_mset.F plus 0"
-definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
-where
- "msetprod = comm_monoid_mset.F times 1"
-
-sublocale comm_monoid_add < msetsum!: comm_monoid_mset plus 0
+sublocale msetsum!: comm_monoid_mset plus 0
where
"comm_monoid_mset.F plus 0 = msetsum"
proof -
@@ -1175,9 +1174,6 @@
from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
qed
-context comm_monoid_add
-begin
-
lemma setsum_unfold_msetsum:
"setsum f A = msetsum (image_mset f (multiset_of_set A))"
by (cases "finite A") (induct A rule: finite_induct, simp_all)
@@ -1203,7 +1199,14 @@
translations
"SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
-sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1
+context comm_monoid_mult
+begin
+
+definition msetprod :: "'a multiset \<Rightarrow> 'a"
+where
+ "msetprod = comm_monoid_mset.F times 1"
+
+sublocale msetprod!: comm_monoid_mset times 1
where
"comm_monoid_mset.F times 1 = msetprod"
proof -
@@ -1211,9 +1214,6 @@
from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" ..
qed
-context comm_monoid_mult
-begin
-
lemma msetprod_empty:
"msetprod {#} = 1"
by (fact msetprod.empty)
--- a/src/HOL/List.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/List.thy Fri Dec 27 14:35:14 2013 +0100
@@ -5018,10 +5018,13 @@
sets to lists but one should convert in the other direction (via
@{const set}). *}
-definition (in linorder) sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
+context linorder
+begin
+
+definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
"sorted_list_of_set = folding.F insort []"
-sublocale linorder < sorted_list_of_set!: folding insort Nil
+sublocale sorted_list_of_set!: folding insort Nil
where
"folding.F insort [] = sorted_list_of_set"
proof -
@@ -5030,21 +5033,17 @@
show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
qed
-context linorder
-begin
-
lemma sorted_list_of_set_empty:
"sorted_list_of_set {} = []"
by (fact sorted_list_of_set.empty)
lemma sorted_list_of_set_insert [simp]:
- assumes "finite A"
- shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
- using assms by (fact sorted_list_of_set.insert_remove)
+ "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
+ by (fact sorted_list_of_set.insert_remove)
lemma sorted_list_of_set_eq_Nil_iff [simp]:
"finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
- using assms by (auto simp: sorted_list_of_set.remove)
+ by (auto simp: sorted_list_of_set.remove)
lemma sorted_list_of_set [simp]:
"finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)
--- a/src/HOL/Orderings.thy Thu Dec 26 22:47:49 2013 +0100
+++ b/src/HOL/Orderings.thy Fri Dec 27 14:35:14 2013 +0100
@@ -195,13 +195,9 @@
lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
by (auto simp add: less_le_not_le intro: antisym)
-end
-
-sublocale order < order!: ordering less_eq less + dual_order!: ordering greater_eq greater
+sublocale order!: ordering less_eq less + dual_order!: ordering greater_eq greater
by default (auto intro: antisym order_trans simp add: less_le)
-context order
-begin
text {* Reflexivity. *}
@@ -1130,13 +1126,11 @@
class order_bot = order + bot +
assumes bot_least: "\<bottom> \<le> a"
+begin
-sublocale order_bot < bot!: ordering_top greater_eq greater bot
+sublocale bot!: ordering_top greater_eq greater bot
by default (fact bot_least)
-context order_bot
-begin
-
lemma le_bot:
"a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
by (fact bot.extremum_uniqueI)
@@ -1160,13 +1154,11 @@
class order_top = order + top +
assumes top_greatest: "a \<le> \<top>"
+begin
-sublocale order_top < top!: ordering_top less_eq less top
+sublocale top!: ordering_top less_eq less top
by default (fact top_greatest)
-context order_top
-begin
-
lemma top_le:
"\<top> \<le> a \<Longrightarrow> a = \<top>"
by (fact top.extremum_uniqueI)