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;
wenzelm@47295
     1
(*  Title:      HOL/Isar_Examples/Group_Notepad.thy
wenzelm@47295
     2
    Author:     Makarius
wenzelm@47295
     3
*)
wenzelm@47295
     4
wenzelm@58882
     5
section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
wenzelm@47295
     6
wenzelm@47295
     7
theory Group_Notepad
wenzelm@63585
     8
  imports Main
wenzelm@47295
     9
begin
wenzelm@47295
    10
wenzelm@47295
    11
notepad
wenzelm@47295
    12
begin
wenzelm@58614
    13
  txt \<open>hypothetical group axiomatization\<close>
wenzelm@47295
    14
wenzelm@61797
    15
  fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<odot>" 70)
wenzelm@47295
    16
    and one :: "'a"
wenzelm@55656
    17
    and inverse :: "'a \<Rightarrow> 'a"
wenzelm@61797
    18
  assume assoc: "(x \<odot> y) \<odot> z = x \<odot> (y \<odot> z)"
wenzelm@61797
    19
    and left_one: "one \<odot> x = x"
wenzelm@61797
    20
    and left_inverse: "inverse x \<odot> x = one"
wenzelm@61797
    21
    for x y z
wenzelm@47295
    22
wenzelm@58614
    23
  txt \<open>some consequences\<close>
wenzelm@47295
    24
wenzelm@61797
    25
  have right_inverse: "x \<odot> inverse x = one" for x
wenzelm@47295
    26
  proof -
wenzelm@61797
    27
    have "x \<odot> inverse x = one \<odot> (x \<odot> inverse x)"
wenzelm@47295
    28
      by (simp only: left_one)
wenzelm@61797
    29
    also have "\<dots> = one \<odot> x \<odot> inverse x"
wenzelm@47295
    30
      by (simp only: assoc)
wenzelm@61797
    31
    also have "\<dots> = inverse (inverse x) \<odot> inverse x \<odot> x \<odot> inverse x"
wenzelm@47295
    32
      by (simp only: left_inverse)
wenzelm@61797
    33
    also have "\<dots> = inverse (inverse x) \<odot> (inverse x \<odot> x) \<odot> inverse x"
wenzelm@47295
    34
      by (simp only: assoc)
wenzelm@61797
    35
    also have "\<dots> = inverse (inverse x) \<odot> one \<odot> inverse x"
wenzelm@47295
    36
      by (simp only: left_inverse)
wenzelm@61797
    37
    also have "\<dots> = inverse (inverse x) \<odot> (one \<odot> inverse x)"
wenzelm@47295
    38
      by (simp only: assoc)
wenzelm@61797
    39
    also have "\<dots> = inverse (inverse x) \<odot> inverse x"
wenzelm@47295
    40
      by (simp only: left_one)
wenzelm@47295
    41
    also have "\<dots> = one"
wenzelm@47295
    42
      by (simp only: left_inverse)
wenzelm@61797
    43
    finally show ?thesis .
wenzelm@47295
    44
  qed
wenzelm@47295
    45
wenzelm@61797
    46
  have right_one: "x \<odot> one = x" for x
wenzelm@47295
    47
  proof -
wenzelm@61797
    48
    have "x \<odot> one = x \<odot> (inverse x \<odot> x)"
wenzelm@47295
    49
      by (simp only: left_inverse)
wenzelm@61797
    50
    also have "\<dots> = x \<odot> inverse x \<odot> x"
wenzelm@47295
    51
      by (simp only: assoc)
wenzelm@61797
    52
    also have "\<dots> = one \<odot> x"
wenzelm@47295
    53
      by (simp only: right_inverse)
wenzelm@47295
    54
    also have "\<dots> = x"
wenzelm@47295
    55
      by (simp only: left_one)
wenzelm@61797
    56
    finally show ?thesis .
wenzelm@47295
    57
  qed
wenzelm@47295
    58
wenzelm@61797
    59
  have one_equality: "one = e" if eq: "e \<odot> x = x" for e x
wenzelm@47295
    60
  proof -
wenzelm@61797
    61
    have "one = x \<odot> inverse x"
wenzelm@47295
    62
      by (simp only: right_inverse)
wenzelm@61797
    63
    also have "\<dots> = (e \<odot> x) \<odot> inverse x"
wenzelm@47295
    64
      by (simp only: eq)
wenzelm@61797
    65
    also have "\<dots> = e \<odot> (x \<odot> inverse x)"
wenzelm@47295
    66
      by (simp only: assoc)
wenzelm@61797
    67
    also have "\<dots> = e \<odot> one"
wenzelm@47295
    68
      by (simp only: right_inverse)
wenzelm@47295
    69
    also have "\<dots> = e"
wenzelm@47295
    70
      by (simp only: right_one)
wenzelm@61797
    71
    finally show ?thesis .
wenzelm@47295
    72
  qed
wenzelm@47295
    73
wenzelm@61797
    74
  have inverse_equality: "inverse x = x'" if eq: "x' \<odot> x = one" for x x'
wenzelm@47295
    75
  proof -
wenzelm@61797
    76
    have "inverse x = one \<odot> inverse x"
wenzelm@47295
    77
      by (simp only: left_one)
wenzelm@61797
    78
    also have "\<dots> = (x' \<odot> x) \<odot> inverse x"
wenzelm@47295
    79
      by (simp only: eq)
wenzelm@61797
    80
    also have "\<dots> = x' \<odot> (x \<odot> inverse x)"
wenzelm@47295
    81
      by (simp only: assoc)
wenzelm@61797
    82
    also have "\<dots> = x' \<odot> one"
wenzelm@47295
    83
      by (simp only: right_inverse)
wenzelm@47295
    84
    also have "\<dots> = x'"
wenzelm@47295
    85
      by (simp only: right_one)
wenzelm@61797
    86
    finally show ?thesis .
wenzelm@47295
    87
  qed
wenzelm@47295
    88
wenzelm@47295
    89
end
wenzelm@47295
    90
wenzelm@47295
    91
end