src/HOL/Groups_List.thy
changeset 61776 57bb7da5c867
parent 61605 1bf7b186542e
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Groups_List.thy	Wed Dec 02 19:14:57 2015 +0100
     1.2 +++ b/src/HOL/Groups_List.thy	Wed Dec 02 19:14:57 2015 +0100
     1.3 @@ -61,18 +61,9 @@
     1.4  context monoid_add
     1.5  begin
     1.6  
     1.7 -definition listsum :: "'a list \<Rightarrow> 'a"
     1.8 -where
     1.9 -  "listsum  = monoid_list.F plus 0"
    1.10 -
    1.11  sublocale listsum: monoid_list plus 0
    1.12 -rewrites
    1.13 - "monoid_list.F plus 0 = listsum"
    1.14 -proof -
    1.15 -  show "monoid_list plus 0" ..
    1.16 -  then interpret listsum: monoid_list plus 0 .
    1.17 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.18 -qed
    1.19 +defines
    1.20 +  listsum = listsum.F ..
    1.21   
    1.22  end
    1.23  
    1.24 @@ -85,7 +76,7 @@
    1.25  proof -
    1.26    show "comm_monoid_list plus 0" ..
    1.27    then interpret listsum: comm_monoid_list plus 0 .
    1.28 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.29 +  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    1.30  qed
    1.31  
    1.32  sublocale setsum: comm_monoid_list_set plus 0
    1.33 @@ -95,8 +86,8 @@
    1.34  proof -
    1.35    show "comm_monoid_list_set plus 0" ..
    1.36    then interpret setsum: comm_monoid_list_set plus 0 .
    1.37 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    1.38 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    1.39 +  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    1.40 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
    1.41  qed
    1.42  
    1.43  end
    1.44 @@ -328,18 +319,9 @@
    1.45  context monoid_mult
    1.46  begin
    1.47  
    1.48 -definition listprod :: "'a list \<Rightarrow> 'a"
    1.49 -where
    1.50 -  "listprod  = monoid_list.F times 1"
    1.51 -
    1.52  sublocale listprod: monoid_list times 1
    1.53 -rewrites
    1.54 -  "monoid_list.F times 1 = listprod"
    1.55 -proof -
    1.56 -  show "monoid_list times 1" ..
    1.57 -  then interpret listprod: monoid_list times 1 .
    1.58 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.59 -qed
    1.60 +defines
    1.61 +  listprod = listprod.F ..
    1.62  
    1.63  end
    1.64  
    1.65 @@ -352,7 +334,7 @@
    1.66  proof -
    1.67    show "comm_monoid_list times 1" ..
    1.68    then interpret listprod: comm_monoid_list times 1 .
    1.69 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.70 +  from listprod_def show "monoid_list.F times 1 = listprod" by simp
    1.71  qed
    1.72  
    1.73  sublocale setprod: comm_monoid_list_set times 1
    1.74 @@ -362,8 +344,8 @@
    1.75  proof -
    1.76    show "comm_monoid_list_set times 1" ..
    1.77    then interpret setprod: comm_monoid_list_set times 1 .
    1.78 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    1.79 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.80 +  from listprod_def show "monoid_list.F times 1 = listprod" by simp
    1.81 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
    1.82  qed
    1.83  
    1.84  end