src/HOL/Big_Operators.thy
changeset 51546 2e26df807dc7
parent 51540 eea5c4ca4a0e
child 51586 7c59fe17f495
     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