prefer target-style syntaxx for sublocale
authorhaftmann
Fri Dec 27 14:35:14 2013 +0100 (2013-12-27)
changeset 54868bab6cade3cc5
parent 54867 c21a2465cac1
child 54869 0046711700c8
prefer target-style syntaxx for sublocale
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Groups.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Multiset.thy
src/HOL/List.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Dec 26 22:47:49 2013 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Dec 27 14:35:14 2013 +0100
     1.3 @@ -452,8 +452,9 @@
     1.4    fixes between
     1.5    assumes between_less: "less x y \<Longrightarrow> less x (between x y) \<and> less (between x y) y"
     1.6      and between_same: "between x x = x"
     1.7 +begin
     1.8  
     1.9 -sublocale  constr_dense_linorder < dlo: unbounded_dense_linorder 
    1.10 +sublocale dlo: unbounded_dense_linorder 
    1.11    apply unfold_locales
    1.12    using gt_ex lt_ex between_less
    1.13    apply auto
    1.14 @@ -461,9 +462,6 @@
    1.15    apply simp
    1.16    done
    1.17  
    1.18 -context constr_dense_linorder
    1.19 -begin
    1.20 -
    1.21  lemma rinf_U[no_atp]:
    1.22    assumes fU: "finite U"
    1.23      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
     2.1 --- a/src/HOL/Groups.thy	Thu Dec 26 22:47:49 2013 +0100
     2.2 +++ b/src/HOL/Groups.thy	Fri Dec 27 14:35:14 2013 +0100
     2.3 @@ -90,10 +90,13 @@
     2.4  locale comm_monoid = abel_semigroup +
     2.5    fixes z :: 'a ("1")
     2.6    assumes comm_neutral: "a * 1 = a"
     2.7 +begin
     2.8  
     2.9 -sublocale comm_monoid < monoid
    2.10 +sublocale monoid
    2.11    by default (simp_all add: commute comm_neutral)
    2.12  
    2.13 +end
    2.14 +
    2.15  
    2.16  subsection {* Generic operations *}
    2.17  
    2.18 @@ -148,19 +151,20 @@
    2.19  
    2.20  class semigroup_add = plus +
    2.21    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
    2.22 +begin
    2.23  
    2.24 -sublocale semigroup_add < add!: semigroup plus
    2.25 +sublocale add!: semigroup plus
    2.26    by default (fact add_assoc)
    2.27  
    2.28 +end
    2.29 +
    2.30  class ab_semigroup_add = semigroup_add +
    2.31    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    2.32 +begin
    2.33  
    2.34 -sublocale ab_semigroup_add < add!: abel_semigroup plus
    2.35 +sublocale add!: abel_semigroup plus
    2.36    by default (fact add_commute)
    2.37  
    2.38 -context ab_semigroup_add
    2.39 -begin
    2.40 -
    2.41  lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute
    2.42  
    2.43  theorems add_ac = add_assoc add_commute add_left_commute
    2.44 @@ -171,19 +175,20 @@
    2.45  
    2.46  class semigroup_mult = times +
    2.47    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    2.48 +begin
    2.49  
    2.50 -sublocale semigroup_mult < mult!: semigroup times
    2.51 +sublocale mult!: semigroup times
    2.52    by default (fact mult_assoc)
    2.53  
    2.54 +end
    2.55 +
    2.56  class ab_semigroup_mult = semigroup_mult +
    2.57    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    2.58 +begin
    2.59  
    2.60 -sublocale ab_semigroup_mult < mult!: abel_semigroup times
    2.61 +sublocale mult!: abel_semigroup times
    2.62    by default (fact mult_commute)
    2.63  
    2.64 -context ab_semigroup_mult
    2.65 -begin
    2.66 -
    2.67  lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute
    2.68  
    2.69  theorems mult_ac = mult_assoc mult_commute mult_left_commute
    2.70 @@ -195,22 +200,28 @@
    2.71  class monoid_add = zero + semigroup_add +
    2.72    assumes add_0_left: "0 + a = a"
    2.73      and add_0_right: "a + 0 = a"
    2.74 +begin
    2.75  
    2.76 -sublocale monoid_add < add!: monoid plus 0
    2.77 +sublocale add!: monoid plus 0
    2.78    by default (fact add_0_left add_0_right)+
    2.79  
    2.80 +end
    2.81 +
    2.82  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    2.83 -by (rule eq_commute)
    2.84 +  by (fact eq_commute)
    2.85  
    2.86  class comm_monoid_add = zero + ab_semigroup_add +
    2.87    assumes add_0: "0 + a = a"
    2.88 +begin
    2.89  
    2.90 -sublocale comm_monoid_add < add!: comm_monoid plus 0
    2.91 +sublocale add!: comm_monoid plus 0
    2.92    by default (insert add_0, simp add: ac_simps)
    2.93  
    2.94 -subclass (in comm_monoid_add) monoid_add
    2.95 +subclass monoid_add
    2.96    by default (fact add.left_neutral add.right_neutral)+
    2.97  
    2.98 +end
    2.99 +
   2.100  class comm_monoid_diff = comm_monoid_add + minus +
   2.101    assumes diff_zero [simp]: "a - 0 = a"
   2.102      and zero_diff [simp]: "0 - a = 0"
   2.103 @@ -265,22 +276,28 @@
   2.104  class monoid_mult = one + semigroup_mult +
   2.105    assumes mult_1_left: "1 * a  = a"
   2.106      and mult_1_right: "a * 1 = a"
   2.107 +begin
   2.108  
   2.109 -sublocale monoid_mult < mult!: monoid times 1
   2.110 +sublocale mult!: monoid times 1
   2.111    by default (fact mult_1_left mult_1_right)+
   2.112  
   2.113 +end
   2.114 +
   2.115  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
   2.116 -by (rule eq_commute)
   2.117 +  by (fact eq_commute)
   2.118  
   2.119  class comm_monoid_mult = one + ab_semigroup_mult +
   2.120    assumes mult_1: "1 * a = a"
   2.121 +begin
   2.122  
   2.123 -sublocale comm_monoid_mult < mult!: comm_monoid times 1
   2.124 +sublocale mult!: comm_monoid times 1
   2.125    by default (insert mult_1, simp add: ac_simps)
   2.126  
   2.127 -subclass (in comm_monoid_mult) monoid_mult
   2.128 +subclass monoid_mult
   2.129    by default (fact mult.left_neutral mult.right_neutral)+
   2.130  
   2.131 +end
   2.132 +
   2.133  class cancel_semigroup_add = semigroup_add +
   2.134    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
   2.135    assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c"
     3.1 --- a/src/HOL/Lattices_Big.thy	Thu Dec 26 22:47:49 2013 +0100
     3.2 +++ b/src/HOL/Lattices_Big.thy	Fri Dec 27 14:35:14 2013 +0100
     3.3 @@ -308,15 +308,14 @@
     3.4  
     3.5  subsection {* Lattice operations on finite sets *}
     3.6  
     3.7 -definition (in semilattice_inf) Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
     3.8 +context semilattice_inf
     3.9 +begin
    3.10 +
    3.11 +definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
    3.12  where
    3.13    "Inf_fin = semilattice_set.F inf"
    3.14  
    3.15 -definition (in semilattice_sup) Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
    3.16 -where
    3.17 -  "Sup_fin = semilattice_set.F sup"
    3.18 -
    3.19 -sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
    3.20 +sublocale Inf_fin!: semilattice_order_set inf less_eq less
    3.21  where
    3.22    "semilattice_set.F inf = Inf_fin"
    3.23  proof -
    3.24 @@ -325,7 +324,16 @@
    3.25    from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
    3.26  qed
    3.27  
    3.28 -sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
    3.29 +end
    3.30 +
    3.31 +context semilattice_sup
    3.32 +begin
    3.33 +
    3.34 +definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
    3.35 +where
    3.36 +  "Sup_fin = semilattice_set.F sup"
    3.37 +
    3.38 +sublocale Sup_fin!: semilattice_order_set sup greater_eq greater
    3.39  where
    3.40    "semilattice_set.F sup = Sup_fin"
    3.41  proof -
    3.42 @@ -334,13 +342,11 @@
    3.43    from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
    3.44  qed
    3.45  
    3.46 +end
    3.47 +
    3.48  
    3.49  subsection {* Infimum and Supremum over non-empty sets *}
    3.50  
    3.51 -text {*
    3.52 -  After this non-regular bootstrap, things continue canonically.
    3.53 -*}
    3.54 -
    3.55  context lattice
    3.56  begin
    3.57  
    3.58 @@ -449,7 +455,7 @@
    3.59  
    3.60  lemma Inf_fin_Inf:
    3.61    assumes "finite A" and "A \<noteq> {}"
    3.62 -  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = Inf A"
    3.63 +  shows "\<Sqinter>\<^sub>f\<^sub>i\<^sub>nA = \<Sqinter>A"
    3.64  proof -
    3.65    from assms obtain b B where "A = insert b B" and "finite B" by auto
    3.66    then show ?thesis
    3.67 @@ -458,7 +464,7 @@
    3.68  
    3.69  lemma Sup_fin_Sup:
    3.70    assumes "finite A" and "A \<noteq> {}"
    3.71 -  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = Sup A"
    3.72 +  shows "\<Squnion>\<^sub>f\<^sub>i\<^sub>nA = \<Squnion>A"
    3.73  proof -
    3.74    from assms obtain b B where "A = insert b B" and "finite B" by auto
    3.75    then show ?thesis
     4.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Thu Dec 26 22:47:49 2013 +0100
     4.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Fri Dec 27 14:35:14 2013 +0100
     4.3 @@ -24,16 +24,14 @@
     4.4    assumes disj_zero_right [simp]: "x \<squnion> \<zero> = x"
     4.5    assumes conj_cancel_right [simp]: "x \<sqinter> \<sim> x = \<zero>"
     4.6    assumes disj_cancel_right [simp]: "x \<squnion> \<sim> x = \<one>"
     4.7 +begin
     4.8  
     4.9 -sublocale boolean < conj!: abel_semigroup conj proof
    4.10 +sublocale conj!: abel_semigroup conj proof
    4.11  qed (fact conj_assoc conj_commute)+
    4.12  
    4.13 -sublocale boolean < disj!: abel_semigroup disj proof
    4.14 +sublocale disj!: abel_semigroup disj proof
    4.15  qed (fact disj_assoc disj_commute)+
    4.16  
    4.17 -context boolean
    4.18 -begin
    4.19 -
    4.20  lemmas conj_left_commute = conj.left_commute
    4.21  
    4.22  lemmas disj_left_commute = disj.left_commute
    4.23 @@ -185,8 +183,9 @@
    4.24  locale boolean_xor = boolean +
    4.25    fixes xor :: "'a => 'a => 'a"  (infixr "\<oplus>" 65)
    4.26    assumes xor_def: "x \<oplus> y = (x \<sqinter> \<sim> y) \<squnion> (\<sim> x \<sqinter> y)"
    4.27 +begin
    4.28  
    4.29 -sublocale boolean_xor < xor!: abel_semigroup xor proof
    4.30 +sublocale xor!: abel_semigroup xor proof
    4.31    fix x y z :: 'a
    4.32    let ?t = "(x \<sqinter> y \<sqinter> z) \<squnion> (x \<sqinter> \<sim> y \<sqinter> \<sim> z) \<squnion>
    4.33              (\<sim> x \<sqinter> y \<sqinter> \<sim> z) \<squnion> (\<sim> x \<sqinter> \<sim> y \<sqinter> z)"
    4.34 @@ -201,9 +200,6 @@
    4.35      by (simp only: xor_def conj_commute disj_commute)
    4.36  qed
    4.37  
    4.38 -context boolean_xor
    4.39 -begin
    4.40 -
    4.41  lemmas xor_assoc = xor.assoc
    4.42  lemmas xor_commute = xor.commute
    4.43  lemmas xor_left_commute = xor.left_commute
     5.1 --- a/src/HOL/Library/Multiset.thy	Thu Dec 26 22:47:49 2013 +0100
     5.2 +++ b/src/HOL/Library/Multiset.thy	Fri Dec 27 14:35:14 2013 +0100
     5.3 @@ -1159,15 +1159,14 @@
     5.4  notation times (infixl "*" 70)
     5.5  notation Groups.one ("1")
     5.6  
     5.7 -definition (in comm_monoid_add) msetsum :: "'a multiset \<Rightarrow> 'a"
     5.8 +context comm_monoid_add
     5.9 +begin
    5.10 +
    5.11 +definition msetsum :: "'a multiset \<Rightarrow> 'a"
    5.12  where
    5.13    "msetsum = comm_monoid_mset.F plus 0"
    5.14  
    5.15 -definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
    5.16 -where
    5.17 -  "msetprod = comm_monoid_mset.F times 1"
    5.18 -
    5.19 -sublocale comm_monoid_add < msetsum!: comm_monoid_mset plus 0
    5.20 +sublocale msetsum!: comm_monoid_mset plus 0
    5.21  where
    5.22    "comm_monoid_mset.F plus 0 = msetsum"
    5.23  proof -
    5.24 @@ -1175,9 +1174,6 @@
    5.25    from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
    5.26  qed
    5.27  
    5.28 -context comm_monoid_add
    5.29 -begin
    5.30 -
    5.31  lemma setsum_unfold_msetsum:
    5.32    "setsum f A = msetsum (image_mset f (multiset_of_set A))"
    5.33    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    5.34 @@ -1203,7 +1199,14 @@
    5.35  translations
    5.36    "SUM i :# A. b" == "CONST msetsum_image (\<lambda>i. b) A"
    5.37  
    5.38 -sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1
    5.39 +context comm_monoid_mult
    5.40 +begin
    5.41 +
    5.42 +definition msetprod :: "'a multiset \<Rightarrow> 'a"
    5.43 +where
    5.44 +  "msetprod = comm_monoid_mset.F times 1"
    5.45 +
    5.46 +sublocale msetprod!: comm_monoid_mset times 1
    5.47  where
    5.48    "comm_monoid_mset.F times 1 = msetprod"
    5.49  proof -
    5.50 @@ -1211,9 +1214,6 @@
    5.51    from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" ..
    5.52  qed
    5.53  
    5.54 -context comm_monoid_mult
    5.55 -begin
    5.56 -
    5.57  lemma msetprod_empty:
    5.58    "msetprod {#} = 1"
    5.59    by (fact msetprod.empty)
     6.1 --- a/src/HOL/List.thy	Thu Dec 26 22:47:49 2013 +0100
     6.2 +++ b/src/HOL/List.thy	Fri Dec 27 14:35:14 2013 +0100
     6.3 @@ -5018,10 +5018,13 @@
     6.4  sets to lists but one should convert in the other direction (via
     6.5  @{const set}). *}
     6.6  
     6.7 -definition (in linorder) sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
     6.8 +context linorder
     6.9 +begin
    6.10 +
    6.11 +definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
    6.12    "sorted_list_of_set = folding.F insort []"
    6.13  
    6.14 -sublocale linorder < sorted_list_of_set!: folding insort Nil
    6.15 +sublocale sorted_list_of_set!: folding insort Nil
    6.16  where
    6.17    "folding.F insort [] = sorted_list_of_set"
    6.18  proof -
    6.19 @@ -5030,21 +5033,17 @@
    6.20    show "folding.F insort [] = sorted_list_of_set" by (simp only: sorted_list_of_set_def)
    6.21  qed
    6.22  
    6.23 -context linorder
    6.24 -begin
    6.25 -
    6.26  lemma sorted_list_of_set_empty:
    6.27    "sorted_list_of_set {} = []"
    6.28    by (fact sorted_list_of_set.empty)
    6.29  
    6.30  lemma sorted_list_of_set_insert [simp]:
    6.31 -  assumes "finite A"
    6.32 -  shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
    6.33 -  using assms by (fact sorted_list_of_set.insert_remove)
    6.34 +  "finite A \<Longrightarrow> sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
    6.35 +  by (fact sorted_list_of_set.insert_remove)
    6.36  
    6.37  lemma sorted_list_of_set_eq_Nil_iff [simp]:
    6.38    "finite A \<Longrightarrow> sorted_list_of_set A = [] \<longleftrightarrow> A = {}"
    6.39 -  using assms by (auto simp: sorted_list_of_set.remove)
    6.40 +  by (auto simp: sorted_list_of_set.remove)
    6.41  
    6.42  lemma sorted_list_of_set [simp]:
    6.43    "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
     7.1 --- a/src/HOL/Orderings.thy	Thu Dec 26 22:47:49 2013 +0100
     7.2 +++ b/src/HOL/Orderings.thy	Fri Dec 27 14:35:14 2013 +0100
     7.3 @@ -195,13 +195,9 @@
     7.4  lemma less_le: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> y"
     7.5    by (auto simp add: less_le_not_le intro: antisym)
     7.6  
     7.7 -end
     7.8 -
     7.9 -sublocale order < order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    7.10 +sublocale order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    7.11    by default (auto intro: antisym order_trans simp add: less_le)
    7.12  
    7.13 -context order
    7.14 -begin
    7.15  
    7.16  text {* Reflexivity. *}
    7.17  
    7.18 @@ -1130,13 +1126,11 @@
    7.19  
    7.20  class order_bot = order + bot +
    7.21    assumes bot_least: "\<bottom> \<le> a"
    7.22 +begin
    7.23  
    7.24 -sublocale order_bot < bot!: ordering_top greater_eq greater bot
    7.25 +sublocale bot!: ordering_top greater_eq greater bot
    7.26    by default (fact bot_least)
    7.27  
    7.28 -context order_bot
    7.29 -begin
    7.30 -
    7.31  lemma le_bot:
    7.32    "a \<le> \<bottom> \<Longrightarrow> a = \<bottom>"
    7.33    by (fact bot.extremum_uniqueI)
    7.34 @@ -1160,13 +1154,11 @@
    7.35  
    7.36  class order_top = order + top +
    7.37    assumes top_greatest: "a \<le> \<top>"
    7.38 +begin
    7.39  
    7.40 -sublocale order_top < top!: ordering_top less_eq less top
    7.41 +sublocale top!: ordering_top less_eq less top
    7.42    by default (fact top_greatest)
    7.43  
    7.44 -context order_top
    7.45 -begin
    7.46 -
    7.47  lemma top_le:
    7.48    "\<top> \<le> a \<Longrightarrow> a = \<top>"
    7.49    by (fact top.extremum_uniqueI)