--- 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 \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> '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 ("\<Sum>_" [1000] 999) where
@@ -1058,18 +1049,9 @@
context comm_monoid_mult
begin
-definition setprod :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b set \<Rightarrow> '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 ("\<Prod>_" [1000] 999) where
--- 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 \<Rightarrow> '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 \<Rightarrow> '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
--- 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 \<Rightarrow> 'a" ("\<Sqinter>\<^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 ("\<Sqinter>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Inf_fin.F ..
end
context semilattice_sup
begin
-definition Sup_fin :: "'a set \<Rightarrow> 'a" ("\<Squnion>\<^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 ("\<Squnion>\<^sub>f\<^sub>i\<^sub>n_" [900] 900) = Sup_fin.F ..
end
@@ -482,27 +464,10 @@
context linorder
begin
-definition Min :: "'a set \<Rightarrow> 'a"
-where
- "Min = semilattice_set.F min"
-
-definition Max :: "'a set \<Rightarrow> '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
--- 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 \<Rightarrow> 'a) \<Rightarrow> '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 \<Rightarrow> 'a) \<Rightarrow> '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