src/HOL/Library/Groups_Big_Fun.thy
changeset 61776 57bb7da5c867
parent 61671 20d4cd2ceab2
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Dec 02 19:14:57 2015 +0100
     1.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Dec 02 19:14:57 2015 +0100
     1.3 @@ -220,19 +220,15 @@
     1.4  context comm_monoid_add
     1.5  begin
     1.6  
     1.7 -definition Sum_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     1.8 -where
     1.9 -  "Sum_any = comm_monoid_fun.G plus 0"
    1.10 -
    1.11 -permanent_interpretation Sum_any: comm_monoid_fun plus 0
    1.12 +sublocale Sum_any: comm_monoid_fun plus 0
    1.13 +defines
    1.14 +  Sum_any = Sum_any.G
    1.15  rewrites
    1.16 -  "comm_monoid_fun.G plus 0 = Sum_any" and
    1.17    "comm_monoid_set.F plus 0 = setsum"
    1.18  proof -
    1.19    show "comm_monoid_fun plus 0" ..
    1.20    then interpret Sum_any: comm_monoid_fun plus 0 .
    1.21 -  from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
    1.22 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    1.23 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
    1.24  qed
    1.25  
    1.26  end
    1.27 @@ -293,19 +289,15 @@
    1.28  context comm_monoid_mult
    1.29  begin
    1.30  
    1.31 -definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    1.32 -where
    1.33 -  "Prod_any = comm_monoid_fun.G times 1"
    1.34 -
    1.35 -permanent_interpretation Prod_any: comm_monoid_fun times 1
    1.36 +sublocale Prod_any: comm_monoid_fun times 1
    1.37 +defines
    1.38 +  Prod_any = Prod_any.G
    1.39  rewrites
    1.40 -  "comm_monoid_fun.G times 1 = Prod_any" and
    1.41    "comm_monoid_set.F times 1 = setprod"
    1.42  proof -
    1.43    show "comm_monoid_fun times 1" ..
    1.44    then interpret Prod_any: comm_monoid_fun times 1 .
    1.45 -  from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
    1.46 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.47 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
    1.48  qed
    1.49  
    1.50  end