src/HOL/Isar_Examples/Group_Notepad.thy
author wenzelm
Tue Oct 07 20:59:46 2014 +0200 (2014-10-07)
changeset 58614 7338eb25226c
parent 55656 eb07b0acbebc
child 58882 6e2010ab8bd9
permissions -rw-r--r--
more cartouches;
more antiquotations;
wenzelm@47295
     1
(*  Title:      HOL/Isar_Examples/Group_Notepad.thy
wenzelm@47295
     2
    Author:     Makarius
wenzelm@47295
     3
*)
wenzelm@47295
     4
wenzelm@58614
     5
header \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
wenzelm@47295
     6
wenzelm@47295
     7
theory Group_Notepad
wenzelm@47295
     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@47295
    15
  fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
wenzelm@47295
    16
    and one :: "'a"
wenzelm@55656
    17
    and inverse :: "'a \<Rightarrow> 'a"
wenzelm@47295
    18
  assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
wenzelm@47295
    19
    and left_one: "\<And>x. one ** x = x"
wenzelm@47295
    20
    and left_inverse: "\<And>x. inverse x ** x = one"
wenzelm@47295
    21
wenzelm@58614
    22
  txt \<open>some consequences\<close>
wenzelm@47295
    23
wenzelm@47295
    24
  have right_inverse: "\<And>x. x ** inverse x = one"
wenzelm@47295
    25
  proof -
wenzelm@47295
    26
    fix x
wenzelm@47295
    27
    have "x ** inverse x = one ** (x ** inverse x)"
wenzelm@47295
    28
      by (simp only: left_one)
wenzelm@47295
    29
    also have "\<dots> = one ** x ** inverse x"
wenzelm@47295
    30
      by (simp only: assoc)
wenzelm@47295
    31
    also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
wenzelm@47295
    32
      by (simp only: left_inverse)
wenzelm@47295
    33
    also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
wenzelm@47295
    34
      by (simp only: assoc)
wenzelm@47295
    35
    also have "\<dots> = inverse (inverse x) ** one ** inverse x"
wenzelm@47295
    36
      by (simp only: left_inverse)
wenzelm@47295
    37
    also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
wenzelm@47295
    38
      by (simp only: assoc)
wenzelm@47295
    39
    also have "\<dots> = inverse (inverse x) ** 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@47295
    43
    finally show "x ** inverse x = one" .
wenzelm@47295
    44
  qed
wenzelm@47295
    45
wenzelm@47295
    46
  have right_one: "\<And>x. x ** one = x"
wenzelm@47295
    47
  proof -
wenzelm@47295
    48
    fix x
wenzelm@47295
    49
    have "x ** one = x ** (inverse x ** x)"
wenzelm@47295
    50
      by (simp only: left_inverse)
wenzelm@47295
    51
    also have "\<dots> = x ** inverse x ** x"
wenzelm@47295
    52
      by (simp only: assoc)
wenzelm@47295
    53
    also have "\<dots> = one ** x"
wenzelm@47295
    54
      by (simp only: right_inverse)
wenzelm@47295
    55
    also have "\<dots> = x"
wenzelm@47295
    56
      by (simp only: left_one)
wenzelm@47295
    57
    finally show "x ** one = x" .
wenzelm@47295
    58
  qed
wenzelm@47295
    59
wenzelm@47295
    60
  have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
wenzelm@47295
    61
  proof -
wenzelm@47295
    62
    fix e x
wenzelm@47295
    63
    assume eq: "e ** x = x"
wenzelm@47295
    64
    have "one = x ** inverse x"
wenzelm@47295
    65
      by (simp only: right_inverse)
wenzelm@47295
    66
    also have "\<dots> = (e ** x) ** inverse x"
wenzelm@47295
    67
      by (simp only: eq)
wenzelm@47295
    68
    also have "\<dots> = e ** (x ** inverse x)"
wenzelm@47295
    69
      by (simp only: assoc)
wenzelm@47295
    70
    also have "\<dots> = e ** one"
wenzelm@47295
    71
      by (simp only: right_inverse)
wenzelm@47295
    72
    also have "\<dots> = e"
wenzelm@47295
    73
      by (simp only: right_one)
wenzelm@47295
    74
    finally show "one = e" .
wenzelm@47295
    75
  qed
wenzelm@47295
    76
wenzelm@47295
    77
  have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"
wenzelm@47295
    78
  proof -
wenzelm@47295
    79
    fix x x'
wenzelm@47295
    80
    assume eq: "x' ** x = one"
wenzelm@47295
    81
    have "inverse x = one ** inverse x"
wenzelm@47295
    82
      by (simp only: left_one)
wenzelm@47295
    83
    also have "\<dots> = (x' ** x) ** inverse x"
wenzelm@47295
    84
      by (simp only: eq)
wenzelm@47295
    85
    also have "\<dots> = x' ** (x ** inverse x)"
wenzelm@47295
    86
      by (simp only: assoc)
wenzelm@47295
    87
    also have "\<dots> = x' ** one"
wenzelm@47295
    88
      by (simp only: right_inverse)
wenzelm@47295
    89
    also have "\<dots> = x'"
wenzelm@47295
    90
      by (simp only: right_one)
wenzelm@47295
    91
    finally show "inverse x = x'" .
wenzelm@47295
    92
  qed
wenzelm@47295
    93
wenzelm@47295
    94
end
wenzelm@47295
    95
wenzelm@47295
    96
end