10 |
10 |
11 notepad |
11 notepad |
12 begin |
12 begin |
13 txt \<open>hypothetical group axiomatization\<close> |
13 txt \<open>hypothetical group axiomatization\<close> |
14 |
14 |
15 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) |
15 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70) |
16 and one :: "'a" |
16 and one :: "'a" |
17 and inverse :: "'a \<Rightarrow> 'a" |
17 and inverse :: "'a \<Rightarrow> 'a" |
18 assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)" |
18 assume assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)" |
19 and left_one: "\<And>x. one ** x = x" |
19 and left_one: "one \<odot> x = x" |
20 and left_inverse: "\<And>x. inverse x ** x = one" |
20 and left_inverse: "inverse x \<odot> x = one" |
|
21 for x y z |
21 |
22 |
22 txt \<open>some consequences\<close> |
23 txt \<open>some consequences\<close> |
23 |
24 |
24 have right_inverse: "\<And>x. x ** inverse x = one" |
25 have right_inverse: "x \<odot> inverse x = one" for x |
25 proof - |
26 proof - |
26 fix x |
27 have "x \<odot> inverse x = one \<odot> (x \<odot> inverse x)" |
27 have "x ** inverse x = one ** (x ** inverse x)" |
|
28 by (simp only: left_one) |
28 by (simp only: left_one) |
29 also have "\<dots> = one ** x ** inverse x" |
29 also have "\<dots> = one \<odot> x \<odot> inverse x" |
30 by (simp only: assoc) |
30 by (simp only: assoc) |
31 also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x" |
31 also have "\<dots> = inverse (inverse x) \<odot> inverse x \<odot> x \<odot> inverse x" |
32 by (simp only: left_inverse) |
32 by (simp only: left_inverse) |
33 also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x" |
33 also have "\<dots> = inverse (inverse x) \<odot> (inverse x \<odot> x) \<odot> inverse x" |
34 by (simp only: assoc) |
34 by (simp only: assoc) |
35 also have "\<dots> = inverse (inverse x) ** one ** inverse x" |
35 also have "\<dots> = inverse (inverse x) \<odot> one \<odot> inverse x" |
36 by (simp only: left_inverse) |
36 by (simp only: left_inverse) |
37 also have "\<dots> = inverse (inverse x) ** (one ** inverse x)" |
37 also have "\<dots> = inverse (inverse x) \<odot> (one \<odot> inverse x)" |
38 by (simp only: assoc) |
38 by (simp only: assoc) |
39 also have "\<dots> = inverse (inverse x) ** inverse x" |
39 also have "\<dots> = inverse (inverse x) \<odot> inverse x" |
40 by (simp only: left_one) |
40 by (simp only: left_one) |
41 also have "\<dots> = one" |
41 also have "\<dots> = one" |
42 by (simp only: left_inverse) |
42 by (simp only: left_inverse) |
43 finally show "x ** inverse x = one" . |
43 finally show ?thesis . |
44 qed |
44 qed |
45 |
45 |
46 have right_one: "\<And>x. x ** one = x" |
46 have right_one: "x \<odot> one = x" for x |
47 proof - |
47 proof - |
48 fix x |
48 have "x \<odot> one = x \<odot> (inverse x \<odot> x)" |
49 have "x ** one = x ** (inverse x ** x)" |
|
50 by (simp only: left_inverse) |
49 by (simp only: left_inverse) |
51 also have "\<dots> = x ** inverse x ** x" |
50 also have "\<dots> = x \<odot> inverse x \<odot> x" |
52 by (simp only: assoc) |
51 by (simp only: assoc) |
53 also have "\<dots> = one ** x" |
52 also have "\<dots> = one \<odot> x" |
54 by (simp only: right_inverse) |
53 by (simp only: right_inverse) |
55 also have "\<dots> = x" |
54 also have "\<dots> = x" |
56 by (simp only: left_one) |
55 by (simp only: left_one) |
57 finally show "x ** one = x" . |
56 finally show ?thesis . |
58 qed |
57 qed |
59 |
58 |
60 have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e" |
59 have one_equality: "one = e" if eq: "e \<odot> x = x" for e x |
61 proof - |
60 proof - |
62 fix e x |
61 have "one = x \<odot> inverse x" |
63 assume eq: "e ** x = x" |
|
64 have "one = x ** inverse x" |
|
65 by (simp only: right_inverse) |
62 by (simp only: right_inverse) |
66 also have "\<dots> = (e ** x) ** inverse x" |
63 also have "\<dots> = (e \<odot> x) \<odot> inverse x" |
67 by (simp only: eq) |
64 by (simp only: eq) |
68 also have "\<dots> = e ** (x ** inverse x)" |
65 also have "\<dots> = e \<odot> (x \<odot> inverse x)" |
69 by (simp only: assoc) |
66 by (simp only: assoc) |
70 also have "\<dots> = e ** one" |
67 also have "\<dots> = e \<odot> one" |
71 by (simp only: right_inverse) |
68 by (simp only: right_inverse) |
72 also have "\<dots> = e" |
69 also have "\<dots> = e" |
73 by (simp only: right_one) |
70 by (simp only: right_one) |
74 finally show "one = e" . |
71 finally show ?thesis . |
75 qed |
72 qed |
76 |
73 |
77 have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'" |
74 have inverse_equality: "inverse x = x'" if eq: "x' \<odot> x = one" for x x' |
78 proof - |
75 proof - |
79 fix x x' |
76 have "inverse x = one \<odot> inverse x" |
80 assume eq: "x' ** x = one" |
|
81 have "inverse x = one ** inverse x" |
|
82 by (simp only: left_one) |
77 by (simp only: left_one) |
83 also have "\<dots> = (x' ** x) ** inverse x" |
78 also have "\<dots> = (x' \<odot> x) \<odot> inverse x" |
84 by (simp only: eq) |
79 by (simp only: eq) |
85 also have "\<dots> = x' ** (x ** inverse x)" |
80 also have "\<dots> = x' \<odot> (x \<odot> inverse x)" |
86 by (simp only: assoc) |
81 by (simp only: assoc) |
87 also have "\<dots> = x' ** one" |
82 also have "\<dots> = x' \<odot> one" |
88 by (simp only: right_inverse) |
83 by (simp only: right_inverse) |
89 also have "\<dots> = x'" |
84 also have "\<dots> = x'" |
90 by (simp only: right_one) |
85 by (simp only: right_one) |
91 finally show "inverse x = x'" . |
86 finally show ?thesis . |
92 qed |
87 qed |
93 |
88 |
94 end |
89 end |
95 |
90 |
96 end |
91 end |