equal
deleted
inserted
replaced
11 |
11 |
12 definition sym_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid" |
12 definition sym_group :: "nat \<Rightarrow> (nat \<Rightarrow> nat) monoid" |
13 where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>" |
13 where "sym_group n = \<lparr> carrier = { p. p permutes {1..n} }, mult = (\<circ>), one = id \<rparr>" |
14 |
14 |
15 definition sign_img :: "int monoid" |
15 definition sign_img :: "int monoid" |
16 where "sign_img = \<lparr> carrier = { -1, 1 }, mult = ( * ), one = 1 \<rparr>" |
16 where "sign_img = \<lparr> carrier = { -1, 1 }, mult = (*), one = 1 \<rparr>" |
17 |
17 |
18 |
18 |
19 lemma sym_group_is_group: "group (sym_group n)" |
19 lemma sym_group_is_group: "group (sym_group n)" |
20 apply (rule groupI) |
20 apply (rule groupI) |
21 apply (simp_all add: sym_group_def permutes_compose permutes_id comp_assoc) |
21 apply (simp_all add: sym_group_def permutes_compose permutes_id comp_assoc) |