equal
deleted
inserted
replaced
4 |
4 |
5 theory Groups_List |
5 theory Groups_List |
6 imports List |
6 imports List |
7 begin |
7 begin |
8 |
8 |
9 no_notation times (infixl "*" 70) |
|
10 no_notation Groups.one ("1") |
|
11 |
|
12 locale monoid_list = monoid |
9 locale monoid_list = monoid |
13 begin |
10 begin |
14 |
11 |
15 definition F :: "'a list \<Rightarrow> 'a" |
12 definition F :: "'a list \<Rightarrow> 'a" |
16 where |
13 where |
17 eq_foldr [code]: "F xs = foldr f xs 1" |
14 eq_foldr [code]: "F xs = foldr f xs \<^bold>1" |
18 |
15 |
19 lemma Nil [simp]: |
16 lemma Nil [simp]: |
20 "F [] = 1" |
17 "F [] = \<^bold>1" |
21 by (simp add: eq_foldr) |
18 by (simp add: eq_foldr) |
22 |
19 |
23 lemma Cons [simp]: |
20 lemma Cons [simp]: |
24 "F (x # xs) = x * F xs" |
21 "F (x # xs) = x \<^bold>* F xs" |
25 by (simp add: eq_foldr) |
22 by (simp add: eq_foldr) |
26 |
23 |
27 lemma append [simp]: |
24 lemma append [simp]: |
28 "F (xs @ ys) = F xs * F ys" |
25 "F (xs @ ys) = F xs \<^bold>* F ys" |
29 by (induct xs) (simp_all add: assoc) |
26 by (induct xs) (simp_all add: assoc) |
30 |
27 |
31 end |
28 end |
32 |
29 |
33 locale comm_monoid_list = comm_monoid + monoid_list |
30 locale comm_monoid_list = comm_monoid + monoid_list |
49 lemma set_conv_list [code]: |
46 lemma set_conv_list [code]: |
50 "set.F g (set xs) = list.F (map g (remdups xs))" |
47 "set.F g (set xs) = list.F (map g (remdups xs))" |
51 by (simp add: distinct_set_conv_list [symmetric]) |
48 by (simp add: distinct_set_conv_list [symmetric]) |
52 |
49 |
53 end |
50 end |
54 |
|
55 notation times (infixl "*" 70) |
|
56 notation Groups.one ("1") |
|
57 |
51 |
58 |
52 |
59 subsection \<open>List summation\<close> |
53 subsection \<open>List summation\<close> |
60 |
54 |
61 context monoid_add |
55 context monoid_add |