src/HOL/Isar_examples/Group.thy
author wenzelm
Fri Jun 04 16:16:31 1999 +0200 (1999-06-04)
changeset 6763 df12aef00932
child 6784 687ddcad8581
permissions -rw-r--r--
Some bits of group theory. Demonstrate calculational proofs.
wenzelm@6763
     1
(*  Title:      HOL/Isar_examples/Group.thy
wenzelm@6763
     2
    ID:         $Id$
wenzelm@6763
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6763
     4
wenzelm@6763
     5
Some bits of group theory.  Demonstrate calculational proofs.
wenzelm@6763
     6
*)
wenzelm@6763
     7
wenzelm@6763
     8
theory Group = Main:;
wenzelm@6763
     9
wenzelm@6763
    10
wenzelm@6763
    11
subsection {* axiomatic type class of groups over signature (*, inv, one) *};
wenzelm@6763
    12
wenzelm@6763
    13
consts
wenzelm@6763
    14
  inv :: "'a => 'a"
wenzelm@6763
    15
  one :: "'a";
wenzelm@6763
    16
wenzelm@6763
    17
axclass
wenzelm@6763
    18
  group < times
wenzelm@6763
    19
  assoc:         "(x * y) * z = x * (y * z)"
wenzelm@6763
    20
  left_unit:     "one * x = x"
wenzelm@6763
    21
  left_inverse:  "inverse x * x = one";
wenzelm@6763
    22
wenzelm@6763
    23
wenzelm@6763
    24
subsection {* some basic theorems of group theory *};
wenzelm@6763
    25
wenzelm@6763
    26
text {* We simulate *};
wenzelm@6763
    27
wenzelm@6763
    28
theorem right_inverse: "x * inverse x = (one::'a::group)";
wenzelm@6763
    29
proof same;
wenzelm@6763
    30
  have "x * inverse x = one * (x * inverse x)";
wenzelm@6763
    31
    by (simp add: left_unit);
wenzelm@6763
    32
wenzelm@6763
    33
  note calculation = facts;
wenzelm@6763
    34
  let "_ = ..." = ??facts;
wenzelm@6763
    35
wenzelm@6763
    36
  have "... = (one * x) * inverse x";
wenzelm@6763
    37
    by (simp add: assoc);
wenzelm@6763
    38
wenzelm@6763
    39
  note calculation = trans[APP calculation facts];
wenzelm@6763
    40
  let "_ = ..." = ??facts;
wenzelm@6763
    41
wenzelm@6763
    42
  have "... = inverse (inverse x) * inverse x * x * inverse x";
wenzelm@6763
    43
    by (simp add: left_inverse);
wenzelm@6763
    44
wenzelm@6763
    45
  note calculation = trans[APP calculation facts];
wenzelm@6763
    46
  let "_ = ..." = ??facts;
wenzelm@6763
    47
wenzelm@6763
    48
  have "... = inverse (inverse x) * (inverse x * x) * inverse x";
wenzelm@6763
    49
    by (simp add: assoc);
wenzelm@6763
    50
wenzelm@6763
    51
  note calculation = trans[APP calculation facts];
wenzelm@6763
    52
  let "_ = ..." = ??facts;
wenzelm@6763
    53
wenzelm@6763
    54
  have "... = inverse (inverse x) * one * inverse x";
wenzelm@6763
    55
    by (simp add: left_inverse);
wenzelm@6763
    56
wenzelm@6763
    57
  note calculation = trans[APP calculation facts];
wenzelm@6763
    58
  let "_ = ..." = ??facts;
wenzelm@6763
    59
wenzelm@6763
    60
  have "... = inverse (inverse x) * (one * inverse x)";
wenzelm@6763
    61
    by (simp add: assoc);
wenzelm@6763
    62
wenzelm@6763
    63
  note calculation = trans[APP calculation facts];
wenzelm@6763
    64
  let "_ = ..." = ??facts;
wenzelm@6763
    65
wenzelm@6763
    66
  have "... = inverse (inverse x) * inverse x";
wenzelm@6763
    67
    by (simp add: left_unit);
wenzelm@6763
    68
wenzelm@6763
    69
  note calculation = trans[APP calculation facts];
wenzelm@6763
    70
  let "_ = ..." = ??facts;
wenzelm@6763
    71
wenzelm@6763
    72
  have "... = one";
wenzelm@6763
    73
    by (simp add: left_inverse);
wenzelm@6763
    74
wenzelm@6763
    75
  note calculation = trans[APP calculation facts];
wenzelm@6763
    76
  let "_ = ..." = ??facts;
wenzelm@6763
    77
  from calculation;
wenzelm@6763
    78
wenzelm@6763
    79
  show ??thesis; .;
wenzelm@6763
    80
qed;
wenzelm@6763
    81
wenzelm@6763
    82
wenzelm@6763
    83
theorem right_inverse: "x * one = (x::'a::group)";
wenzelm@6763
    84
proof same;
wenzelm@6763
    85
wenzelm@6763
    86
  have "x * one = x * (inverse x * x)";
wenzelm@6763
    87
    by (simp add: left_inverse);
wenzelm@6763
    88
wenzelm@6763
    89
  note calculation = facts;
wenzelm@6763
    90
  let "_ = ..." = ??facts;
wenzelm@6763
    91
wenzelm@6763
    92
  have "... = x * inverse x * x";
wenzelm@6763
    93
    by (simp add: assoc);
wenzelm@6763
    94
wenzelm@6763
    95
  note calculation = trans[APP calculation facts];
wenzelm@6763
    96
  let "_ = ..." = ??facts;
wenzelm@6763
    97
wenzelm@6763
    98
  have "... = one * x";
wenzelm@6763
    99
    by (simp add: right_inverse);
wenzelm@6763
   100
wenzelm@6763
   101
  note calculation = trans[APP calculation facts];
wenzelm@6763
   102
  let "_ = ..." = ??facts;
wenzelm@6763
   103
wenzelm@6763
   104
  have "... = x";
wenzelm@6763
   105
    by (simp add: left_unit);
wenzelm@6763
   106
wenzelm@6763
   107
  note calculation = trans[APP calculation facts];
wenzelm@6763
   108
  let "_ = ..." = ??facts;
wenzelm@6763
   109
  from calculation;
wenzelm@6763
   110
wenzelm@6763
   111
  show ??thesis; .;
wenzelm@6763
   112
qed;
wenzelm@6763
   113
wenzelm@6763
   114
wenzelm@6763
   115
end;