# HG changeset patch
# User haftmann
# Date 1388151314 -3600
# Node ID bab6cade3cc52d99218a83a8439afbf7660e9aab
# Parent  c21a2465cac1875153e78afea017e3db414ee343
prefer target-style syntaxx for sublocale

diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- 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
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Groups.thy
--- 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"
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Lattices_Big.thy
--- 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
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Library/Boolean_Algebra.thy
--- 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
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Library/Multiset.thy
--- 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)
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/List.thy
--- 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) 
diff -r c21a2465cac1 -r bab6cade3cc5 src/HOL/Orderings.thy
--- 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)