src/HOL/Isar_Examples/Group_Notepad.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 55656 eb07b0acbebc
child 58614 7338eb25226c
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     1 (*  Title:      HOL/Isar_Examples/Group_Notepad.thy
     2     Author:     Makarius
     3 *)
     4 
     5 header {* Some algebraic identities derived from group axioms -- proof notepad version *}
     6 
     7 theory Group_Notepad
     8 imports Main
     9 begin
    10 
    11 notepad
    12 begin
    13   txt {* hypothetical group axiomatization *}
    14 
    15   fix prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "**" 70)
    16     and one :: "'a"
    17     and inverse :: "'a \<Rightarrow> 'a"
    18   assume assoc: "\<And>x y z. (x ** y) ** z = x ** (y ** z)"
    19     and left_one: "\<And>x. one ** x = x"
    20     and left_inverse: "\<And>x. inverse x ** x = one"
    21 
    22   txt {* some consequences *}
    23 
    24   have right_inverse: "\<And>x. x ** inverse x = one"
    25   proof -
    26     fix x
    27     have "x ** inverse x = one ** (x ** inverse x)"
    28       by (simp only: left_one)
    29     also have "\<dots> = one ** x ** inverse x"
    30       by (simp only: assoc)
    31     also have "\<dots> = inverse (inverse x) ** inverse x ** x ** inverse x"
    32       by (simp only: left_inverse)
    33     also have "\<dots> = inverse (inverse x) ** (inverse x ** x) ** inverse x"
    34       by (simp only: assoc)
    35     also have "\<dots> = inverse (inverse x) ** one ** inverse x"
    36       by (simp only: left_inverse)
    37     also have "\<dots> = inverse (inverse x) ** (one ** inverse x)"
    38       by (simp only: assoc)
    39     also have "\<dots> = inverse (inverse x) ** inverse x"
    40       by (simp only: left_one)
    41     also have "\<dots> = one"
    42       by (simp only: left_inverse)
    43     finally show "x ** inverse x = one" .
    44   qed
    45 
    46   have right_one: "\<And>x. x ** one = x"
    47   proof -
    48     fix x
    49     have "x ** one = x ** (inverse x ** x)"
    50       by (simp only: left_inverse)
    51     also have "\<dots> = x ** inverse x ** x"
    52       by (simp only: assoc)
    53     also have "\<dots> = one ** x"
    54       by (simp only: right_inverse)
    55     also have "\<dots> = x"
    56       by (simp only: left_one)
    57     finally show "x ** one = x" .
    58   qed
    59 
    60   have one_equality: "\<And>e x. e ** x = x \<Longrightarrow> one = e"
    61   proof -
    62     fix e x
    63     assume eq: "e ** x = x"
    64     have "one = x ** inverse x"
    65       by (simp only: right_inverse)
    66     also have "\<dots> = (e ** x) ** inverse x"
    67       by (simp only: eq)
    68     also have "\<dots> = e ** (x ** inverse x)"
    69       by (simp only: assoc)
    70     also have "\<dots> = e ** one"
    71       by (simp only: right_inverse)
    72     also have "\<dots> = e"
    73       by (simp only: right_one)
    74     finally show "one = e" .
    75   qed
    76 
    77   have inverse_equality: "\<And>x x'. x' ** x = one \<Longrightarrow> inverse x = x'"
    78   proof -
    79     fix x x'
    80     assume eq: "x' ** x = one"
    81     have "inverse x = one ** inverse x"
    82       by (simp only: left_one)
    83     also have "\<dots> = (x' ** x) ** inverse x"
    84       by (simp only: eq)
    85     also have "\<dots> = x' ** (x ** inverse x)"
    86       by (simp only: assoc)
    87     also have "\<dots> = x' ** one"
    88       by (simp only: right_inverse)
    89     also have "\<dots> = x'"
    90       by (simp only: right_one)
    91     finally show "inverse x = x'" .
    92   qed
    93 
    94 end
    95 
    96 end