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

src/HOL/Isar_Examples/Group_Context.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_Context.thy

2 Author: Makarius

3 *)

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

7 theory Group_Context

8 imports Main

9 begin

11 text {* hypothetical group axiomatization *}

13 context

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

15 and one :: "'a"

16 and inverse :: "'a \<Rightarrow> 'a"

17 assumes assoc: "(x ** y) ** z = x ** (y ** z)"

18 and left_one: "one ** x = x"

19 and left_inverse: "inverse x ** x = one"

20 begin

22 text {* some consequences *}

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

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

58 lemma one_equality:

59 assumes eq: "e ** x = x"

60 shows "one = e"

61 proof -

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

75 lemma inverse_equality:

76 assumes eq: "x' ** x = one"

77 shows "inverse x = x'"

78 proof -

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

92 end

94 end