more uniform style for interpretation and sublocale declarations
authorhaftmann
Tue Mar 26 21:53:56 2013 +0100 (2013-03-26)
changeset 515462e26df807dc7
parent 51545 6f6012f430fc
child 51547 604d73671fa7
more uniform style for interpretation and sublocale declarations
src/HOL/Big_Operators.thy
src/HOL/Finite_Set.thy
src/HOL/Groups.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
     1.1 --- a/src/HOL/Big_Operators.thy	Tue Mar 26 20:55:21 2013 +0100
     1.2 +++ b/src/HOL/Big_Operators.thy	Tue Mar 26 21:53:56 2013 +0100
     1.3 @@ -325,12 +325,11 @@
     1.4  
     1.5  sublocale comm_monoid_add < setsum!: comm_monoid_set plus 0
     1.6  where
     1.7 -  "setsum.F = setsum"
     1.8 +  "comm_monoid_set.F plus 0 = setsum"
     1.9  proof -
    1.10    show "comm_monoid_set plus 0" ..
    1.11    then interpret setsum!: comm_monoid_set plus 0 .
    1.12 -  show "setsum.F = setsum"
    1.13 -    by (simp only: setsum_def)
    1.14 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    1.15  qed
    1.16  
    1.17  abbreviation
    1.18 @@ -1048,12 +1047,11 @@
    1.19  
    1.20  sublocale comm_monoid_mult < setprod!: comm_monoid_set times 1
    1.21  where
    1.22 -  "setprod.F = setprod"
    1.23 +  "comm_monoid_set.F times 1 = setprod"
    1.24  proof -
    1.25    show "comm_monoid_set times 1" ..
    1.26    then interpret setprod!: comm_monoid_set times 1 .
    1.27 -  show "setprod.F = setprod"
    1.28 -    by (simp only: setprod_def)
    1.29 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.30  qed
    1.31  
    1.32  abbreviation
    1.33 @@ -1743,22 +1741,20 @@
    1.34  
    1.35  sublocale semilattice_inf < Inf_fin!: semilattice_order_set inf less_eq less
    1.36  where
    1.37 -  "Inf_fin.F = Inf_fin"
    1.38 +  "semilattice_set.F inf = Inf_fin"
    1.39  proof -
    1.40    show "semilattice_order_set inf less_eq less" ..
    1.41    then interpret Inf_fin!: semilattice_order_set inf less_eq less.
    1.42 -  show "Inf_fin.F = Inf_fin"
    1.43 -    by (fact Inf_fin_def [symmetric])
    1.44 +  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
    1.45  qed
    1.46  
    1.47  sublocale semilattice_sup < Sup_fin!: semilattice_order_set sup greater_eq greater
    1.48  where
    1.49 -  "Sup_fin.F = Sup_fin"
    1.50 +  "semilattice_set.F sup = Sup_fin"
    1.51  proof -
    1.52    show "semilattice_order_set sup greater_eq greater" ..
    1.53    then interpret Sup_fin!: semilattice_order_set sup greater_eq greater .
    1.54 -  show "Sup_fin.F = Sup_fin"
    1.55 -    by (fact Sup_fin_def [symmetric])
    1.56 +  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
    1.57  qed
    1.58  
    1.59  
    1.60 @@ -1910,12 +1906,6 @@
    1.61  
    1.62  subsection {* Minimum and Maximum over non-empty sets *}
    1.63  
    1.64 -text {*
    1.65 -  This case is already setup by the @{text min_max} sublocale dependency from above.  But note
    1.66 -  that this yields irregular prefixes, e.g.~@{text min_max.Inf_fin.insert} instead
    1.67 -  of @{text Max.insert}.
    1.68 -*}
    1.69 -
    1.70  context linorder
    1.71  begin
    1.72  
     2.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 26 20:55:21 2013 +0100
     2.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 26 21:53:56 2013 +0100
     2.3 @@ -1107,11 +1107,11 @@
     2.4  
     2.5  interpretation card!: folding "\<lambda>_. Suc" 0
     2.6  where
     2.7 -  "card.F = card"
     2.8 +  "folding.F (\<lambda>_. Suc) 0 = card"
     2.9  proof -
    2.10    show "folding (\<lambda>_. Suc)" by default rule
    2.11    then interpret card!: folding "\<lambda>_. Suc" 0 .
    2.12 -  show "card.F = card" by (simp only: card_def)
    2.13 +  from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
    2.14  qed
    2.15  
    2.16  lemma card_infinite:
     3.1 --- a/src/HOL/Groups.thy	Tue Mar 26 20:55:21 2013 +0100
     3.2 +++ b/src/HOL/Groups.thy	Tue Mar 26 21:53:56 2013 +0100
     3.3 @@ -91,8 +91,8 @@
     3.4    fixes z :: 'a ("1")
     3.5    assumes comm_neutral: "a * 1 = a"
     3.6  
     3.7 -sublocale comm_monoid < monoid proof
     3.8 -qed (simp_all add: commute comm_neutral)
     3.9 +sublocale comm_monoid < monoid
    3.10 +  by default (simp_all add: commute comm_neutral)
    3.11  
    3.12  
    3.13  subsection {* Generic operations *}
    3.14 @@ -151,14 +151,14 @@
    3.15  class semigroup_add = plus +
    3.16    assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)"
    3.17  
    3.18 -sublocale semigroup_add < add!: semigroup plus proof
    3.19 -qed (fact add_assoc)
    3.20 +sublocale semigroup_add < add!: semigroup plus
    3.21 +  by default (fact add_assoc)
    3.22  
    3.23  class ab_semigroup_add = semigroup_add +
    3.24    assumes add_commute [algebra_simps, field_simps]: "a + b = b + a"
    3.25  
    3.26 -sublocale ab_semigroup_add < add!: abel_semigroup plus proof
    3.27 -qed (fact add_commute)
    3.28 +sublocale ab_semigroup_add < add!: abel_semigroup plus
    3.29 +  by default (fact add_commute)
    3.30  
    3.31  context ab_semigroup_add
    3.32  begin
    3.33 @@ -174,14 +174,14 @@
    3.34  class semigroup_mult = times +
    3.35    assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)"
    3.36  
    3.37 -sublocale semigroup_mult < mult!: semigroup times proof
    3.38 -qed (fact mult_assoc)
    3.39 +sublocale semigroup_mult < mult!: semigroup times
    3.40 +  by default (fact mult_assoc)
    3.41  
    3.42  class ab_semigroup_mult = semigroup_mult +
    3.43    assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a"
    3.44  
    3.45 -sublocale ab_semigroup_mult < mult!: abel_semigroup times proof
    3.46 -qed (fact mult_commute)
    3.47 +sublocale ab_semigroup_mult < mult!: abel_semigroup times
    3.48 +  by default (fact mult_commute)
    3.49  
    3.50  context ab_semigroup_mult
    3.51  begin
    3.52 @@ -198,8 +198,8 @@
    3.53    assumes add_0_left: "0 + a = a"
    3.54      and add_0_right: "a + 0 = a"
    3.55  
    3.56 -sublocale monoid_add < add!: monoid plus 0 proof
    3.57 -qed (fact add_0_left add_0_right)+
    3.58 +sublocale monoid_add < add!: monoid plus 0
    3.59 +  by default (fact add_0_left add_0_right)+
    3.60  
    3.61  lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
    3.62  by (rule eq_commute)
    3.63 @@ -207,11 +207,11 @@
    3.64  class comm_monoid_add = zero + ab_semigroup_add +
    3.65    assumes add_0: "0 + a = a"
    3.66  
    3.67 -sublocale comm_monoid_add < add!: comm_monoid plus 0 proof
    3.68 -qed (insert add_0, simp add: ac_simps)
    3.69 +sublocale comm_monoid_add < add!: comm_monoid plus 0
    3.70 +  by default (insert add_0, simp add: ac_simps)
    3.71  
    3.72 -subclass (in comm_monoid_add) monoid_add proof
    3.73 -qed (fact add.left_neutral add.right_neutral)+
    3.74 +subclass (in comm_monoid_add) monoid_add
    3.75 +  by default (fact add.left_neutral add.right_neutral)+
    3.76  
    3.77  class comm_monoid_diff = comm_monoid_add + minus +
    3.78    assumes diff_zero [simp]: "a - 0 = a"
    3.79 @@ -268,8 +268,8 @@
    3.80    assumes mult_1_left: "1 * a  = a"
    3.81      and mult_1_right: "a * 1 = a"
    3.82  
    3.83 -sublocale monoid_mult < mult!: monoid times 1 proof
    3.84 -qed (fact mult_1_left mult_1_right)+
    3.85 +sublocale monoid_mult < mult!: monoid times 1
    3.86 +  by default (fact mult_1_left mult_1_right)+
    3.87  
    3.88  lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
    3.89  by (rule eq_commute)
    3.90 @@ -277,11 +277,11 @@
    3.91  class comm_monoid_mult = one + ab_semigroup_mult +
    3.92    assumes mult_1: "1 * a = a"
    3.93  
    3.94 -sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof
    3.95 -qed (insert mult_1, simp add: ac_simps)
    3.96 +sublocale comm_monoid_mult < mult!: comm_monoid times 1
    3.97 +  by default (insert mult_1, simp add: ac_simps)
    3.98  
    3.99 -subclass (in comm_monoid_mult) monoid_mult proof
   3.100 -qed (fact mult.left_neutral mult.right_neutral)+
   3.101 +subclass (in comm_monoid_mult) monoid_mult
   3.102 +  by default (fact mult.left_neutral mult.right_neutral)+
   3.103  
   3.104  class cancel_semigroup_add = semigroup_add +
   3.105    assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c"
     4.1 --- a/src/HOL/Lattices.thy	Tue Mar 26 20:55:21 2013 +0100
     4.2 +++ b/src/HOL/Lattices.thy	Tue Mar 26 21:53:56 2013 +0100
     4.3 @@ -471,25 +471,23 @@
     4.4  class bounded_semilattice_inf_top = semilattice_inf + top
     4.5  
     4.6  sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr inf top
     4.7 +  + inf_top!: semilattice_neutr_order inf top less_eq less
     4.8  proof
     4.9    fix x
    4.10    show "x \<sqinter> \<top> = x"
    4.11      by (rule inf_absorb1) simp
    4.12  qed
    4.13  
    4.14 -sublocale bounded_semilattice_inf_top < inf_top!: semilattice_neutr_order inf top less_eq less ..
    4.15 -
    4.16  class bounded_semilattice_sup_bot = semilattice_sup + bot
    4.17  
    4.18  sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr sup bot
    4.19 +  + sup_bot!: semilattice_neutr_order sup bot greater_eq greater
    4.20  proof
    4.21    fix x
    4.22    show "x \<squnion> \<bottom> = x"
    4.23      by (rule sup_absorb1) simp
    4.24  qed
    4.25  
    4.26 -sublocale bounded_semilattice_sup_bot < sup_bot!: semilattice_neutr_order sup bot greater_eq greater ..
    4.27 -
    4.28  class bounded_lattice_bot = lattice + bot
    4.29  begin
    4.30  
     5.1 --- a/src/HOL/Orderings.thy	Tue Mar 26 20:55:21 2013 +0100
     5.2 +++ b/src/HOL/Orderings.thy	Tue Mar 26 21:53:56 2013 +0100
     5.3 @@ -197,10 +197,7 @@
     5.4  
     5.5  end
     5.6  
     5.7 -sublocale order < order!: ordering less_eq less
     5.8 -  by default (auto intro: antisym order_trans simp add: less_le)
     5.9 -
    5.10 -sublocale order < dual_order!: ordering greater_eq greater
    5.11 +sublocale order < order!: ordering less_eq less +  dual_order!: ordering greater_eq greater
    5.12    by default (auto intro: antisym order_trans simp add: less_le)
    5.13  
    5.14  context order
    5.15 @@ -210,7 +207,7 @@
    5.16  
    5.17  lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
    5.18      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
    5.19 -by (simp add: less_le) blast
    5.20 +by (fact order.order_iff_strict)
    5.21  
    5.22  lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
    5.23  unfolding less_le by blast
    5.24 @@ -228,10 +225,10 @@
    5.25  text {* Transitivity rules for calculational reasoning *}
    5.26  
    5.27  lemma neq_le_trans: "a \<noteq> b \<Longrightarrow> a \<le> b \<Longrightarrow> a < b"
    5.28 -by (simp add: less_le)
    5.29 +by (fact order.not_eq_order_implies_strict)
    5.30  
    5.31  lemma le_neq_trans: "a \<le> b \<Longrightarrow> a \<noteq> b \<Longrightarrow> a < b"
    5.32 -by (simp add: less_le)
    5.33 +by (rule order.not_eq_order_implies_strict)
    5.34  
    5.35  
    5.36  text {* Asymmetry. *}
    5.37 @@ -243,7 +240,7 @@
    5.38  by (blast intro: antisym)
    5.39  
    5.40  lemma less_imp_neq: "x < y \<Longrightarrow> x \<noteq> y"
    5.41 -by (erule contrapos_pn, erule subst, rule less_irrefl)
    5.42 +by (fact order.strict_implies_not_eq)
    5.43  
    5.44  
    5.45  text {* Least value operator *}
    5.46 @@ -1168,7 +1165,6 @@
    5.47  by (simp add: max_def)
    5.48  
    5.49  
    5.50 -
    5.51  subsection {* (Unique) top and bottom elements *}
    5.52  
    5.53  class bot = order +
    5.54 @@ -1176,8 +1172,7 @@
    5.55    assumes bot_least: "\<bottom> \<le> a"
    5.56  
    5.57  sublocale bot < bot!: ordering_top greater_eq greater bot
    5.58 -proof
    5.59 -qed (fact bot_least)
    5.60 +  by default (fact bot_least)
    5.61  
    5.62  context bot
    5.63  begin
    5.64 @@ -1205,8 +1200,7 @@
    5.65    assumes top_greatest: "a \<le> \<top>"
    5.66  
    5.67  sublocale top < top!: ordering_top less_eq less top
    5.68 -proof
    5.69 -qed (fact top_greatest)
    5.70 +  by default (fact top_greatest)
    5.71  
    5.72  context top
    5.73  begin
    5.74 @@ -1316,6 +1310,7 @@
    5.75  
    5.76  class dense_linorder = inner_dense_linorder + no_top + no_bot
    5.77  
    5.78 +
    5.79  subsection {* Wellorders *}
    5.80  
    5.81  class wellorder = linorder +