author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47311  1addbe2a7458 
child 47872  1f6f519cdb32 
permissions  rwrr 
47295  1 
(* Title: HOL/Isar_Examples/Group_Context.thy 
2 
Author: Makarius 

3 
*) 

4 

5 
header {* Some algebraic identities derived from group axioms  theory context version *} 

6 

7 
theory Group_Context 

8 
imports Main 

9 
begin 

10 

11 
text {* hypothetical group axiomatization *} 

12 

13 
context 

14 
fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "**" 70) 

15 
and one :: "'a" 

16 
and inverse :: "'a => 'a" 

47311
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset

17 
assumes assoc: "(x ** y) ** z = x ** (y ** z)" 
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset

18 
and left_one: "one ** x = x" 
1addbe2a7458
close context elements via Expression.cert/read_declaration;
wenzelm
parents:
47295
diff
changeset

19 
and left_inverse: "inverse x ** x = one" 
47295  20 
begin 
21 

22 
text {* some consequences *} 

23 

24 
lemma right_inverse: "x ** inverse x = one" 

25 
proof  

26 
have "x ** inverse x = one ** (x ** inverse x)" 

27 
by (simp only: left_one) 

28 
also have "\<dots> = one ** x ** inverse x" 

29 
by (simp only: assoc) 

30 
also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x" 

31 
by (simp only: left_inverse) 

32 
also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x" 

33 
by (simp only: assoc) 

34 
also have "\<dots> = inverse (inverse x) ** one ** inverse x" 

35 
by (simp only: left_inverse) 

36 
also have "\<dots> = inverse (inverse x) ** (one ** inverse x)" 

37 
by (simp only: assoc) 

38 
also have "\<dots> = inverse (inverse x) ** inverse x" 

39 
by (simp only: left_one) 

40 
also have "\<dots> = one" 

41 
by (simp only: left_inverse) 

42 
finally show "x ** inverse x = one" . 

43 
qed 

44 

45 
lemma right_one: "x ** one = x" 

46 
proof  

47 
have "x ** one = x ** (inverse x ** x)" 

48 
by (simp only: left_inverse) 

49 
also have "\<dots> = x ** inverse x ** x" 

50 
by (simp only: assoc) 

51 
also have "\<dots> = one ** x" 

52 
by (simp only: right_inverse) 

53 
also have "\<dots> = x" 

54 
by (simp only: left_one) 

55 
finally show "x ** one = x" . 

56 
qed 

57 

58 
lemma one_equality: "e ** x = x \<Longrightarrow> one = e" 

59 
proof  

60 
fix e x 

61 
assume eq: "e ** x = x" 

62 
have "one = x ** inverse x" 

63 
by (simp only: right_inverse) 

64 
also have "\<dots> = (e ** x) ** inverse x" 

65 
by (simp only: eq) 

66 
also have "\<dots> = e ** (x ** inverse x)" 

67 
by (simp only: assoc) 

68 
also have "\<dots> = e ** one" 

69 
by (simp only: right_inverse) 

70 
also have "\<dots> = e" 

71 
by (simp only: right_one) 

72 
finally show "one = e" . 

73 
qed 

74 

75 
lemma inverse_equality: "x' ** x = one \<Longrightarrow> inverse x = x'" 

76 
proof  

77 
fix x x' 

78 
assume eq: "x' ** x = one" 

79 
have "inverse x = one ** inverse x" 

80 
by (simp only: left_one) 

81 
also have "\<dots> = (x' ** x) ** inverse x" 

82 
by (simp only: eq) 

83 
also have "\<dots> = x' ** (x ** inverse x)" 

84 
by (simp only: assoc) 

85 
also have "\<dots> = x' ** one" 

86 
by (simp only: right_inverse) 

87 
also have "\<dots> = x'" 

88 
by (simp only: right_one) 

89 
finally show "inverse x = x'" . 

90 
qed 

91 

92 
end 

93 

94 
end 