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