src/HOL/Isar_Examples/Group_Context.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 47872 1f6f519cdb32
child 55656 eb07b0acbebc
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
wenzelm@47295
     1
(*  Title:      HOL/Isar_Examples/Group_Context.thy
wenzelm@47295
     2
    Author:     Makarius
wenzelm@47295
     3
*)
wenzelm@47295
     4
wenzelm@47295
     5
header {* Some algebraic identities derived from group axioms -- theory context version *}
wenzelm@47295
     6
wenzelm@47295
     7
theory Group_Context
wenzelm@47295
     8
imports Main
wenzelm@47295
     9
begin
wenzelm@47295
    10
wenzelm@47295
    11
text {* hypothetical group axiomatization *}
wenzelm@47295
    12
wenzelm@47295
    13
context
wenzelm@47295
    14
  fixes prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
wenzelm@47295
    15
    and one :: "'a"
wenzelm@47295
    16
    and inverse :: "'a => 'a"
wenzelm@47311
    17
  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
wenzelm@47311
    18
    and left_one: "one ** x = x"
wenzelm@47311
    19
    and left_inverse: "inverse x ** x = one"
wenzelm@47295
    20
begin
wenzelm@47295
    21
wenzelm@47295
    22
text {* some consequences *}
wenzelm@47295
    23
wenzelm@47295
    24
lemma right_inverse: "x ** inverse x = one"
wenzelm@47295
    25
proof -
wenzelm@47295
    26
  have "x ** inverse x = one ** (x ** inverse x)"
wenzelm@47295
    27
    by (simp only: left_one)
wenzelm@47295
    28
  also have "\<dots> = one ** x ** inverse x"
wenzelm@47295
    29
    by (simp only: assoc)
wenzelm@47295
    30
  also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
wenzelm@47295
    31
    by (simp only: left_inverse)
wenzelm@47295
    32
  also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
wenzelm@47295
    33
    by (simp only: assoc)
wenzelm@47295
    34
  also have "\<dots> = inverse (inverse x) ** one ** inverse x"
wenzelm@47295
    35
    by (simp only: left_inverse)
wenzelm@47295
    36
  also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
wenzelm@47295
    37
    by (simp only: assoc)
wenzelm@47295
    38
  also have "\<dots> = inverse (inverse x) ** inverse x"
wenzelm@47295
    39
    by (simp only: left_one)
wenzelm@47295
    40
  also have "\<dots> = one"
wenzelm@47295
    41
    by (simp only: left_inverse)
wenzelm@47295
    42
  finally show "x ** inverse x = one" .
wenzelm@47295
    43
qed
wenzelm@47295
    44
wenzelm@47295
    45
lemma right_one: "x ** one = x"
wenzelm@47295
    46
proof -
wenzelm@47295
    47
  have "x ** one = x ** (inverse x ** x)"
wenzelm@47295
    48
    by (simp only: left_inverse)
wenzelm@47295
    49
  also have "\<dots> = x ** inverse x ** x"
wenzelm@47295
    50
    by (simp only: assoc)
wenzelm@47295
    51
  also have "\<dots> = one ** x"
wenzelm@47295
    52
    by (simp only: right_inverse)
wenzelm@47295
    53
  also have "\<dots> = x"
wenzelm@47295
    54
    by (simp only: left_one)
wenzelm@47295
    55
  finally show "x ** one = x" .
wenzelm@47295
    56
qed
wenzelm@47295
    57
wenzelm@47872
    58
lemma one_equality:
wenzelm@47872
    59
  assumes eq: "e ** x = x"
wenzelm@47872
    60
  shows "one = e"
wenzelm@47295
    61
proof -
wenzelm@47295
    62
  have "one = x ** inverse x"
wenzelm@47295
    63
    by (simp only: right_inverse)
wenzelm@47295
    64
  also have "\<dots> = (e ** x) ** inverse x"
wenzelm@47295
    65
    by (simp only: eq)
wenzelm@47295
    66
  also have "\<dots> = e ** (x ** inverse x)"
wenzelm@47295
    67
    by (simp only: assoc)
wenzelm@47295
    68
  also have "\<dots> = e ** one"
wenzelm@47295
    69
    by (simp only: right_inverse)
wenzelm@47295
    70
  also have "\<dots> = e"
wenzelm@47295
    71
    by (simp only: right_one)
wenzelm@47295
    72
  finally show "one = e" .
wenzelm@47295
    73
qed
wenzelm@47295
    74
wenzelm@47872
    75
lemma inverse_equality:
wenzelm@47872
    76
  assumes eq: "x' ** x = one"
wenzelm@47872
    77
  shows "inverse x = x'"
wenzelm@47295
    78
proof -
wenzelm@47295
    79
  have "inverse x = one ** inverse x"
wenzelm@47295
    80
    by (simp only: left_one)
wenzelm@47295
    81
  also have "\<dots> = (x' ** x) ** inverse x"
wenzelm@47295
    82
    by (simp only: eq)
wenzelm@47295
    83
  also have "\<dots> = x' ** (x ** inverse x)"
wenzelm@47295
    84
    by (simp only: assoc)
wenzelm@47295
    85
  also have "\<dots> = x' ** one"
wenzelm@47295
    86
    by (simp only: right_inverse)
wenzelm@47295
    87
  also have "\<dots> = x'"
wenzelm@47295
    88
    by (simp only: right_one)
wenzelm@47295
    89
  finally show "inverse x = x'" .
wenzelm@47295
    90
qed
wenzelm@47295
    91
wenzelm@47295
    92
end
wenzelm@47295
    93
wenzelm@47295
    94
end