modernized
authorhaftmann
Wed Dec 02 19:14:57 2015 +0100 (2015-12-02)
changeset 6177657bb7da5c867
parent 61775 ec11275fb263
child 61777 f9e05eab6e3c
modernized
src/HOL/Groups_Big.thy
src/HOL/Groups_List.thy
src/HOL/Lattices_Big.thy
src/HOL/Library/Groups_Big_Fun.thy
     1.1 --- a/src/HOL/Groups_Big.thy	Wed Dec 02 19:14:57 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Wed Dec 02 19:14:57 2015 +0100
     1.3 @@ -467,18 +467,9 @@
     1.4  context comm_monoid_add
     1.5  begin
     1.6  
     1.7 -definition setsum :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
     1.8 -where
     1.9 -  "setsum = comm_monoid_set.F plus 0"
    1.10 -
    1.11  sublocale setsum: comm_monoid_set plus 0
    1.12 -rewrites
    1.13 -  "comm_monoid_set.F plus 0 = setsum"
    1.14 -proof -
    1.15 -  show "comm_monoid_set plus 0" ..
    1.16 -  then interpret setsum: comm_monoid_set plus 0 .
    1.17 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    1.18 -qed
    1.19 +defines
    1.20 +  setsum = setsum.F ..
    1.21  
    1.22  abbreviation
    1.23    Setsum ("\<Sum>_" [1000] 999) where
    1.24 @@ -1058,18 +1049,9 @@
    1.25  context comm_monoid_mult
    1.26  begin
    1.27  
    1.28 -definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> 'a"
    1.29 -where
    1.30 -  "setprod = comm_monoid_set.F times 1"
    1.31 -
    1.32  sublocale setprod: comm_monoid_set times 1
    1.33 -rewrites
    1.34 -  "comm_monoid_set.F times 1 = setprod"
    1.35 -proof -
    1.36 -  show "comm_monoid_set times 1" ..
    1.37 -  then interpret setprod: comm_monoid_set times 1 .
    1.38 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    1.39 -qed
    1.40 +defines
    1.41 +  setprod = setprod.F ..
    1.42  
    1.43  abbreviation
    1.44    Setprod ("\<Prod>_" [1000] 999) where
     2.1 --- a/src/HOL/Groups_List.thy	Wed Dec 02 19:14:57 2015 +0100
     2.2 +++ b/src/HOL/Groups_List.thy	Wed Dec 02 19:14:57 2015 +0100
     2.3 @@ -61,18 +61,9 @@
     2.4  context monoid_add
     2.5  begin
     2.6  
     2.7 -definition listsum :: "'a list \<Rightarrow> 'a"
     2.8 -where
     2.9 -  "listsum  = monoid_list.F plus 0"
    2.10 -
    2.11  sublocale listsum: monoid_list plus 0
    2.12 -rewrites
    2.13 - "monoid_list.F plus 0 = listsum"
    2.14 -proof -
    2.15 -  show "monoid_list plus 0" ..
    2.16 -  then interpret listsum: monoid_list plus 0 .
    2.17 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    2.18 -qed
    2.19 +defines
    2.20 +  listsum = listsum.F ..
    2.21   
    2.22  end
    2.23  
    2.24 @@ -85,7 +76,7 @@
    2.25  proof -
    2.26    show "comm_monoid_list plus 0" ..
    2.27    then interpret listsum: comm_monoid_list plus 0 .
    2.28 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    2.29 +  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    2.30  qed
    2.31  
    2.32  sublocale setsum: comm_monoid_list_set plus 0
    2.33 @@ -95,8 +86,8 @@
    2.34  proof -
    2.35    show "comm_monoid_list_set plus 0" ..
    2.36    then interpret setsum: comm_monoid_list_set plus 0 .
    2.37 -  from listsum_def show "monoid_list.F plus 0 = listsum" by rule
    2.38 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    2.39 +  from listsum_def show "monoid_list.F plus 0 = listsum" by simp
    2.40 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
    2.41  qed
    2.42  
    2.43  end
    2.44 @@ -328,18 +319,9 @@
    2.45  context monoid_mult
    2.46  begin
    2.47  
    2.48 -definition listprod :: "'a list \<Rightarrow> 'a"
    2.49 -where
    2.50 -  "listprod  = monoid_list.F times 1"
    2.51 -
    2.52  sublocale listprod: monoid_list times 1
    2.53 -rewrites
    2.54 -  "monoid_list.F times 1 = listprod"
    2.55 -proof -
    2.56 -  show "monoid_list times 1" ..
    2.57 -  then interpret listprod: monoid_list times 1 .
    2.58 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.59 -qed
    2.60 +defines
    2.61 +  listprod = listprod.F ..
    2.62  
    2.63  end
    2.64  
    2.65 @@ -352,7 +334,7 @@
    2.66  proof -
    2.67    show "comm_monoid_list times 1" ..
    2.68    then interpret listprod: comm_monoid_list times 1 .
    2.69 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.70 +  from listprod_def show "monoid_list.F times 1 = listprod" by simp
    2.71  qed
    2.72  
    2.73  sublocale setprod: comm_monoid_list_set times 1
    2.74 @@ -362,8 +344,8 @@
    2.75  proof -
    2.76    show "comm_monoid_list_set times 1" ..
    2.77    then interpret setprod: comm_monoid_list_set times 1 .
    2.78 -  from listprod_def show "monoid_list.F times 1 = listprod" by rule
    2.79 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    2.80 +  from listprod_def show "monoid_list.F times 1 = listprod" by simp
    2.81 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
    2.82  qed
    2.83  
    2.84  end
     3.1 --- a/src/HOL/Lattices_Big.thy	Wed Dec 02 19:14:57 2015 +0100
     3.2 +++ b/src/HOL/Lattices_Big.thy	Wed Dec 02 19:14:57 2015 +0100
     3.3 @@ -314,36 +314,18 @@
     3.4  context semilattice_inf
     3.5  begin
     3.6  
     3.7 -definition Inf_fin :: "'a set \<Rightarrow> 'a" ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
     3.8 -where
     3.9 -  "Inf_fin = semilattice_set.F inf"
    3.10 -
    3.11  sublocale Inf_fin: semilattice_order_set inf less_eq less
    3.12 -rewrites
    3.13 -  "semilattice_set.F inf = Inf_fin"
    3.14 -proof -
    3.15 -  show "semilattice_order_set inf less_eq less" ..
    3.16 -  then interpret Inf_fin: semilattice_order_set inf less_eq less .
    3.17 -  from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule
    3.18 -qed
    3.19 +defines
    3.20 +  Inf_fin ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
    3.21  
    3.22  end
    3.23  
    3.24  context semilattice_sup
    3.25  begin
    3.26  
    3.27 -definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900)
    3.28 -where
    3.29 -  "Sup_fin = semilattice_set.F sup"
    3.30 -
    3.31  sublocale Sup_fin: semilattice_order_set sup greater_eq greater
    3.32 -rewrites
    3.33 -  "semilattice_set.F sup = Sup_fin"
    3.34 -proof -
    3.35 -  show "semilattice_order_set sup greater_eq greater" ..
    3.36 -  then interpret Sup_fin: semilattice_order_set sup greater_eq greater .
    3.37 -  from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule
    3.38 -qed
    3.39 +defines
    3.40 +  Sup_fin ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
    3.41  
    3.42  end
    3.43  
    3.44 @@ -482,27 +464,10 @@
    3.45  context linorder
    3.46  begin
    3.47  
    3.48 -definition Min :: "'a set \<Rightarrow> 'a"
    3.49 -where
    3.50 -  "Min = semilattice_set.F min"
    3.51 -
    3.52 -definition Max :: "'a set \<Rightarrow> 'a"
    3.53 -where
    3.54 -  "Max = semilattice_set.F max"
    3.55 -
    3.56  sublocale Min: semilattice_order_set min less_eq less
    3.57    + Max: semilattice_order_set max greater_eq greater
    3.58 -rewrites
    3.59 -  "semilattice_set.F min = Min"
    3.60 -  and "semilattice_set.F max = Max"
    3.61 -proof -
    3.62 -  show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def)
    3.63 -  then interpret Min: semilattice_order_set min less_eq less .
    3.64 -  show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def)
    3.65 -  then interpret Max: semilattice_order_set max greater_eq greater .
    3.66 -  from Min_def show "semilattice_set.F min = Min" by rule
    3.67 -  from Max_def show "semilattice_set.F max = Max" by rule
    3.68 -qed
    3.69 +defines
    3.70 +  Min = Min.F and Max = Max.F ..
    3.71  
    3.72  end
    3.73  
     4.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Wed Dec 02 19:14:57 2015 +0100
     4.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Wed Dec 02 19:14:57 2015 +0100
     4.3 @@ -220,19 +220,15 @@
     4.4  context comm_monoid_add
     4.5  begin
     4.6  
     4.7 -definition Sum_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     4.8 -where
     4.9 -  "Sum_any = comm_monoid_fun.G plus 0"
    4.10 -
    4.11 -permanent_interpretation Sum_any: comm_monoid_fun plus 0
    4.12 +sublocale Sum_any: comm_monoid_fun plus 0
    4.13 +defines
    4.14 +  Sum_any = Sum_any.G
    4.15  rewrites
    4.16 -  "comm_monoid_fun.G plus 0 = Sum_any" and
    4.17    "comm_monoid_set.F plus 0 = setsum"
    4.18  proof -
    4.19    show "comm_monoid_fun plus 0" ..
    4.20    then interpret Sum_any: comm_monoid_fun plus 0 .
    4.21 -  from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule
    4.22 -  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule
    4.23 +  from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym)
    4.24  qed
    4.25  
    4.26  end
    4.27 @@ -293,19 +289,15 @@
    4.28  context comm_monoid_mult
    4.29  begin
    4.30  
    4.31 -definition Prod_any :: "('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    4.32 -where
    4.33 -  "Prod_any = comm_monoid_fun.G times 1"
    4.34 -
    4.35 -permanent_interpretation Prod_any: comm_monoid_fun times 1
    4.36 +sublocale Prod_any: comm_monoid_fun times 1
    4.37 +defines
    4.38 +  Prod_any = Prod_any.G
    4.39  rewrites
    4.40 -  "comm_monoid_fun.G times 1 = Prod_any" and
    4.41    "comm_monoid_set.F times 1 = setprod"
    4.42  proof -
    4.43    show "comm_monoid_fun times 1" ..
    4.44    then interpret Prod_any: comm_monoid_fun times 1 .
    4.45 -  from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule
    4.46 -  from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule
    4.47 +  from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym)
    4.48  qed
    4.49  
    4.50  end