author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 55656 eb07b0acbebc child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Isar_Examples/Group_Notepad.thy
2     Author:     Makarius
3 *)
5 header {* Some algebraic identities derived from group axioms -- proof notepad version *}
8 imports Main
9 begin
12 begin
13   txt {* hypothetical group axiomatization *}
15   fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
16     and one :: "'a"
17     and inverse :: "'a \<Rightarrow> 'a"
18   assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
19     and left_one: "\<And>x. one ** x = x"
20     and left_inverse: "\<And>x. inverse x ** x = one"
22   txt {* some consequences *}
24   have right_inverse: "\<And>x. x ** inverse x = one"
25   proof -
26     fix x
27     have "x ** inverse x = one ** (x ** inverse x)"
28       by (simp only: left_one)
29     also have "\<dots> = one ** x ** inverse x"
30       by (simp only: assoc)
31     also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
32       by (simp only: left_inverse)
33     also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
34       by (simp only: assoc)
35     also have "\<dots> = inverse (inverse x) ** one ** inverse x"
36       by (simp only: left_inverse)
37     also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
38       by (simp only: assoc)
39     also have "\<dots> = inverse (inverse x) ** inverse x"
40       by (simp only: left_one)
41     also have "\<dots> = one"
42       by (simp only: left_inverse)
43     finally show "x ** inverse x = one" .
44   qed
46   have right_one: "\<And>x. x ** one = x"
47   proof -
48     fix x
49     have "x ** one = x ** (inverse x ** x)"
50       by (simp only: left_inverse)
51     also have "\<dots> = x ** inverse x ** x"
52       by (simp only: assoc)
53     also have "\<dots> = one ** x"
54       by (simp only: right_inverse)
55     also have "\<dots> = x"
56       by (simp only: left_one)
57     finally show "x ** one = x" .
58   qed
60   have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
61   proof -
62     fix e x
63     assume eq: "e ** x = x"
64     have "one = x ** inverse x"
65       by (simp only: right_inverse)
66     also have "\<dots> = (e ** x) ** inverse x"
67       by (simp only: eq)
68     also have "\<dots> = e ** (x ** inverse x)"
69       by (simp only: assoc)
70     also have "\<dots> = e ** one"
71       by (simp only: right_inverse)
72     also have "\<dots> = e"
73       by (simp only: right_one)
74     finally show "one = e" .
75   qed
77   have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"
78   proof -
79     fix x x'
80     assume eq: "x' ** x = one"
81     have "inverse x = one ** inverse x"
82       by (simp only: left_one)
83     also have "\<dots> = (x' ** x) ** inverse x"
84       by (simp only: eq)
85     also have "\<dots> = x' ** (x ** inverse x)"
86       by (simp only: assoc)
87     also have "\<dots> = x' ** one"
88       by (simp only: right_inverse)
89     also have "\<dots> = x'"
90       by (simp only: right_one)
91     finally show "inverse x = x'" .
92   qed
94 end
96 end