summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_Examples/Group_Notepad.thy

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 *}

7 theory Group_Notepad

8 imports Main

9 begin

11 notepad

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