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

src/HOL/Isar_Examples/Group_Notepad.thy

author | wenzelm |

Tue Sep 26 20:54:40 2017 +0200 (23 months ago) | |

changeset 66695 | 91500c024c7f |

parent 63585 | f4a308fdf664 |

permissions | -rw-r--r-- |

tuned;

1 (* Title: HOL/Isar_Examples/Group_Notepad.thy

2 Author: Makarius

3 *)

5 section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>

7 theory Group_Notepad

8 imports Main

9 begin

11 notepad

12 begin

13 txt \<open>hypothetical group axiomatization\<close>

15 fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<odot>" 70)

16 and one :: "'a"

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

18 assume assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"

19 and left_one: "one \<odot> x = x"

20 and left_inverse: "inverse x \<odot> x = one"

21 for x y z

23 txt \<open>some consequences\<close>

25 have right_inverse: "x \<odot> inverse x = one" for x

26 proof -

27 have "x \<odot> inverse x = one \<odot> (x \<odot> inverse x)"

28 by (simp only: left_one)

29 also have "\<dots> = one \<odot> x \<odot> inverse x"

30 by (simp only: assoc)

31 also have "\<dots> = inverse (inverse x) \<odot> inverse x \<odot> x \<odot> inverse x"

32 by (simp only: left_inverse)

33 also have "\<dots> = inverse (inverse x) \<odot> (inverse x \<odot> x) \<odot> inverse x"

34 by (simp only: assoc)

35 also have "\<dots> = inverse (inverse x) \<odot> one \<odot> inverse x"

36 by (simp only: left_inverse)

37 also have "\<dots> = inverse (inverse x) \<odot> (one \<odot> inverse x)"

38 by (simp only: assoc)

39 also have "\<dots> = inverse (inverse x) \<odot> inverse x"

40 by (simp only: left_one)

41 also have "\<dots> = one"

42 by (simp only: left_inverse)

43 finally show ?thesis .

44 qed

46 have right_one: "x \<odot> one = x" for x

47 proof -

48 have "x \<odot> one = x \<odot> (inverse x \<odot> x)"

49 by (simp only: left_inverse)

50 also have "\<dots> = x \<odot> inverse x \<odot> x"

51 by (simp only: assoc)

52 also have "\<dots> = one \<odot> x"

53 by (simp only: right_inverse)

54 also have "\<dots> = x"

55 by (simp only: left_one)

56 finally show ?thesis .

57 qed

59 have one_equality: "one = e" if eq: "e \<odot> x = x" for e x

60 proof -

61 have "one = x \<odot> inverse x"

62 by (simp only: right_inverse)

63 also have "\<dots> = (e \<odot> x) \<odot> inverse x"

64 by (simp only: eq)

65 also have "\<dots> = e \<odot> (x \<odot> inverse x)"

66 by (simp only: assoc)

67 also have "\<dots> = e \<odot> one"

68 by (simp only: right_inverse)

69 also have "\<dots> = e"

70 by (simp only: right_one)

71 finally show ?thesis .

72 qed

74 have inverse_equality: "inverse x = x'" if eq: "x' \<odot> x = one" for x x'

75 proof -

76 have "inverse x = one \<odot> inverse x"

77 by (simp only: left_one)

78 also have "\<dots> = (x' \<odot> x) \<odot> inverse x"

79 by (simp only: eq)

80 also have "\<dots> = x' \<odot> (x \<odot> inverse x)"

81 by (simp only: assoc)

82 also have "\<dots> = x' \<odot> one"

83 by (simp only: right_inverse)

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

85 by (simp only: right_one)

86 finally show ?thesis .

87 qed

89 end

91 end