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 *)
     4 
     5 section \<open>Some algebraic identities derived from group axioms -- proof notepad version\<close>
     6 
     7 theory Group_Notepad
     8   imports Main
     9 begin
    10 
    11 notepad
    12 begin
    13   txt \<open>hypothetical group axiomatization\<close>
    14 
    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
    22 
    23   txt \<open>some consequences\<close>
    24 
    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
    45 
    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
    58 
    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
    73 
    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
    88 
    89 end
    90 
    91 end