# HG changeset patch # User haftmann # Date 1449080097 -3600 # Node ID 57bb7da5c867c62b4b24fa8b9ba900792d7f63c2 # Parent ec11275fb26369a908f6cd4f37522da76e99f9a7 modernized diff -r ec11275fb263 -r 57bb7da5c867 src/HOL/Groups_Big.thy --- a/src/HOL/Groups_Big.thy Wed Dec 02 19:14:57 2015 +0100 +++ b/src/HOL/Groups_Big.thy Wed Dec 02 19:14:57 2015 +0100 @@ -467,18 +467,9 @@ context comm_monoid_add begin -definition setsum :: "('b \ 'a) \ 'b set \ 'a" -where - "setsum = comm_monoid_set.F plus 0" - sublocale setsum: comm_monoid_set plus 0 -rewrites - "comm_monoid_set.F plus 0 = setsum" -proof - - show "comm_monoid_set plus 0" .. - then interpret setsum: comm_monoid_set plus 0 . - from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule -qed +defines + setsum = setsum.F .. abbreviation Setsum ("\_" [1000] 999) where @@ -1058,18 +1049,9 @@ context comm_monoid_mult begin -definition setprod :: "('b \ 'a) \ 'b set \ 'a" -where - "setprod = comm_monoid_set.F times 1" - sublocale setprod: comm_monoid_set times 1 -rewrites - "comm_monoid_set.F times 1 = setprod" -proof - - show "comm_monoid_set times 1" .. - then interpret setprod: comm_monoid_set times 1 . - from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule -qed +defines + setprod = setprod.F .. abbreviation Setprod ("\_" [1000] 999) where diff -r ec11275fb263 -r 57bb7da5c867 src/HOL/Groups_List.thy --- a/src/HOL/Groups_List.thy Wed Dec 02 19:14:57 2015 +0100 +++ b/src/HOL/Groups_List.thy Wed Dec 02 19:14:57 2015 +0100 @@ -61,18 +61,9 @@ context monoid_add begin -definition listsum :: "'a list \ 'a" -where - "listsum = monoid_list.F plus 0" - sublocale listsum: monoid_list plus 0 -rewrites - "monoid_list.F plus 0 = listsum" -proof - - show "monoid_list plus 0" .. - then interpret listsum: monoid_list plus 0 . - from listsum_def show "monoid_list.F plus 0 = listsum" by rule -qed +defines + listsum = listsum.F .. end @@ -85,7 +76,7 @@ proof - show "comm_monoid_list plus 0" .. then interpret listsum: comm_monoid_list plus 0 . - from listsum_def show "monoid_list.F plus 0 = listsum" by rule + from listsum_def show "monoid_list.F plus 0 = listsum" by simp qed sublocale setsum: comm_monoid_list_set plus 0 @@ -95,8 +86,8 @@ proof - show "comm_monoid_list_set plus 0" .. then interpret setsum: comm_monoid_list_set plus 0 . - from listsum_def show "monoid_list.F plus 0 = listsum" by rule - from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule + from listsum_def show "monoid_list.F plus 0 = listsum" by simp + from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym) qed end @@ -328,18 +319,9 @@ context monoid_mult begin -definition listprod :: "'a list \ 'a" -where - "listprod = monoid_list.F times 1" - sublocale listprod: monoid_list times 1 -rewrites - "monoid_list.F times 1 = listprod" -proof - - show "monoid_list times 1" .. - then interpret listprod: monoid_list times 1 . - from listprod_def show "monoid_list.F times 1 = listprod" by rule -qed +defines + listprod = listprod.F .. end @@ -352,7 +334,7 @@ proof - show "comm_monoid_list times 1" .. then interpret listprod: comm_monoid_list times 1 . - from listprod_def show "monoid_list.F times 1 = listprod" by rule + from listprod_def show "monoid_list.F times 1 = listprod" by simp qed sublocale setprod: comm_monoid_list_set times 1 @@ -362,8 +344,8 @@ proof - show "comm_monoid_list_set times 1" .. then interpret setprod: comm_monoid_list_set times 1 . - from listprod_def show "monoid_list.F times 1 = listprod" by rule - from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule + from listprod_def show "monoid_list.F times 1 = listprod" by simp + from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym) qed end diff -r ec11275fb263 -r 57bb7da5c867 src/HOL/Lattices_Big.thy --- a/src/HOL/Lattices_Big.thy Wed Dec 02 19:14:57 2015 +0100 +++ b/src/HOL/Lattices_Big.thy Wed Dec 02 19:14:57 2015 +0100 @@ -314,36 +314,18 @@ context semilattice_inf begin -definition Inf_fin :: "'a set \ 'a" ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) -where - "Inf_fin = semilattice_set.F inf" - sublocale Inf_fin: semilattice_order_set inf less_eq less -rewrites - "semilattice_set.F inf = Inf_fin" -proof - - show "semilattice_order_set inf less_eq less" .. - then interpret Inf_fin: semilattice_order_set inf less_eq less . - from Inf_fin_def show "semilattice_set.F inf = Inf_fin" by rule -qed +defines + Inf_fin ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F .. end context semilattice_sup begin -definition Sup_fin :: "'a set \ 'a" ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) -where - "Sup_fin = semilattice_set.F sup" - sublocale Sup_fin: semilattice_order_set sup greater_eq greater -rewrites - "semilattice_set.F sup = Sup_fin" -proof - - show "semilattice_order_set sup greater_eq greater" .. - then interpret Sup_fin: semilattice_order_set sup greater_eq greater . - from Sup_fin_def show "semilattice_set.F sup = Sup_fin" by rule -qed +defines + Sup_fin ("\\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F .. end @@ -482,27 +464,10 @@ context linorder begin -definition Min :: "'a set \ 'a" -where - "Min = semilattice_set.F min" - -definition Max :: "'a set \ 'a" -where - "Max = semilattice_set.F max" - sublocale Min: semilattice_order_set min less_eq less + Max: semilattice_order_set max greater_eq greater -rewrites - "semilattice_set.F min = Min" - and "semilattice_set.F max = Max" -proof - - show "semilattice_order_set min less_eq less" by standard (auto simp add: min_def) - then interpret Min: semilattice_order_set min less_eq less . - show "semilattice_order_set max greater_eq greater" by standard (auto simp add: max_def) - then interpret Max: semilattice_order_set max greater_eq greater . - from Min_def show "semilattice_set.F min = Min" by rule - from Max_def show "semilattice_set.F max = Max" by rule -qed +defines + Min = Min.F and Max = Max.F .. end diff -r ec11275fb263 -r 57bb7da5c867 src/HOL/Library/Groups_Big_Fun.thy --- a/src/HOL/Library/Groups_Big_Fun.thy Wed Dec 02 19:14:57 2015 +0100 +++ b/src/HOL/Library/Groups_Big_Fun.thy Wed Dec 02 19:14:57 2015 +0100 @@ -220,19 +220,15 @@ context comm_monoid_add begin -definition Sum_any :: "('b \ 'a) \ 'a" -where - "Sum_any = comm_monoid_fun.G plus 0" - -permanent_interpretation Sum_any: comm_monoid_fun plus 0 +sublocale Sum_any: comm_monoid_fun plus 0 +defines + Sum_any = Sum_any.G rewrites - "comm_monoid_fun.G plus 0 = Sum_any" and "comm_monoid_set.F plus 0 = setsum" proof - show "comm_monoid_fun plus 0" .. then interpret Sum_any: comm_monoid_fun plus 0 . - from Sum_any_def show "comm_monoid_fun.G plus 0 = Sum_any" by rule - from setsum_def show "comm_monoid_set.F plus 0 = setsum" by rule + from setsum_def show "comm_monoid_set.F plus 0 = setsum" by (auto intro: sym) qed end @@ -293,19 +289,15 @@ context comm_monoid_mult begin -definition Prod_any :: "('b \ 'a) \ 'a" -where - "Prod_any = comm_monoid_fun.G times 1" - -permanent_interpretation Prod_any: comm_monoid_fun times 1 +sublocale Prod_any: comm_monoid_fun times 1 +defines + Prod_any = Prod_any.G rewrites - "comm_monoid_fun.G times 1 = Prod_any" and "comm_monoid_set.F times 1 = setprod" proof - show "comm_monoid_fun times 1" .. then interpret Prod_any: comm_monoid_fun times 1 . - from Prod_any_def show "comm_monoid_fun.G times 1 = Prod_any" by rule - from setprod_def show "comm_monoid_set.F times 1 = setprod" by rule + from setprod_def show "comm_monoid_set.F times 1 = setprod" by (auto intro: sym) qed end