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