src/HOL/Isar_examples/Group.thy
author wenzelm
Sat Jun 05 20:28:45 1999 +0200 (1999-06-05)
changeset 6784 687ddcad8581
parent 6763 df12aef00932
child 6793 88aba7f486cb
permissions -rw-r--r--
proper calculation;
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
wenzelm@6763
     6
theory Group = Main:;
wenzelm@6763
     7
wenzelm@6784
     8
title {* Basic group theory -- demonstrating calculational proofs *};
wenzelm@6763
     9
wenzelm@6784
    10
section {* Groups *}; 
wenzelm@6784
    11
wenzelm@6784
    12
text {*
wenzelm@6784
    13
 We define an axiomatic type class of general groupes over signature
wenzelm@6784
    14
 (op *, one, inv).
wenzelm@6784
    15
*};
wenzelm@6763
    16
wenzelm@6763
    17
consts
wenzelm@6784
    18
  one :: "'a"
wenzelm@6784
    19
  inv :: "'a => 'a";
wenzelm@6763
    20
wenzelm@6763
    21
axclass
wenzelm@6763
    22
  group < times
wenzelm@6763
    23
  assoc:         "(x * y) * z = x * (y * z)"
wenzelm@6763
    24
  left_unit:     "one * x = x"
wenzelm@6784
    25
  left_inverse:  "inv x * x = one";
wenzelm@6763
    26
wenzelm@6784
    27
text {*
wenzelm@6784
    28
 The group axioms only state the properties of left unit and inverse, the
wenzelm@6784
    29
 right versions are derivable as follows.  The calculational proof style below
wenzelm@6784
    30
 closely follows a typical presentation given in any basic course on
wenzelm@6784
    31
 algebra.
wenzelm@6784
    32
*};
wenzelm@6763
    33
wenzelm@6784
    34
theorem right_inverse: "x * inv x = (one::'a::group)";
wenzelm@6763
    35
proof same;
wenzelm@6784
    36
  have "x * inv x = one * (x * inv x)";
wenzelm@6763
    37
    by (simp add: left_unit);
wenzelm@6784
    38
  also; have "... = (one * x) * inv x";
wenzelm@6784
    39
    by (simp add: assoc);
wenzelm@6784
    40
  also; have "... = inv (inv x) * inv x * x * inv x";
wenzelm@6784
    41
    by (simp add: left_inverse);
wenzelm@6784
    42
  also; have "... = inv (inv x) * (inv x * x) * inv x";
wenzelm@6784
    43
    by (simp add: assoc);
wenzelm@6784
    44
  also; have "... = inv (inv x) * one * inv x";
wenzelm@6784
    45
    by (simp add: left_inverse);
wenzelm@6784
    46
  also; have "... = inv (inv x) * (one * inv x)";
wenzelm@6763
    47
    by (simp add: assoc);
wenzelm@6784
    48
  also; have "... = inv (inv x) * inv x";
wenzelm@6784
    49
    by (simp add: left_unit);
wenzelm@6784
    50
  also; have "... = one";
wenzelm@6784
    51
    by (simp add: left_inverse);
wenzelm@6784
    52
  finally; show ??thesis; .;
wenzelm@6784
    53
qed;
wenzelm@6763
    54
wenzelm@6784
    55
text {*
wenzelm@6784
    56
  With right_inverse already at our disposel, right_unit is now
wenzelm@6784
    57
  obtained much simpler.
wenzelm@6784
    58
*};
wenzelm@6763
    59
wenzelm@6784
    60
theorem right_unit: "x * one = (x::'a::group)";
wenzelm@6784
    61
proof same;
wenzelm@6784
    62
  have "x * one = x * (inv x * x)";
wenzelm@6784
    63
    by (simp add: left_inverse);
wenzelm@6784
    64
  also; have "... = x * inv x * x";
wenzelm@6763
    65
    by (simp add: assoc);
wenzelm@6784
    66
  also; have "... = one * x";
wenzelm@6784
    67
    by (simp add: right_inverse);
wenzelm@6784
    68
  also; have "... = x";
wenzelm@6784
    69
    by (simp add: left_unit);
wenzelm@6784
    70
  finally; show ??thesis; .;
wenzelm@6784
    71
qed;
wenzelm@6763
    72
wenzelm@6784
    73
text {*
wenzelm@6784
    74
 There are only two language elements 'also' (for initial or
wenzelm@6784
    75
 intermediate calculational steps), and 'finally' (for picking up the
wenzelm@6784
    76
 result of a calculation).  These constructs are not hardwired into
wenzelm@6784
    77
 Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
wenzelm@6784
    78
wenzelm@6784
    79
 Without referring to 'also' or 'finally', calculations may be
wenzelm@6784
    80
 simulated as follows.  This can be also understood as an expansion of these
wenzelm@6784
    81
 two derived language elements.
wenzelm@6763
    82
wenzelm@6784
    83
 Also note that "..." is just a special term binding that happens to
wenzelm@6784
    84
 be bound automatically to the argument of the last fact established by
wenzelm@6784
    85
 assume or any local goal.  Unlike ??thesis, "..." is bound after the
wenzelm@6784
    86
 proof is finished.
wenzelm@6784
    87
*};
wenzelm@6784
    88
wenzelm@6784
    89
theorem right_unit': "x * one = (x::'a::group)";
wenzelm@6784
    90
proof same;
wenzelm@6784
    91
wenzelm@6784
    92
  have "x * one = x * (inv x * x)";
wenzelm@6763
    93
    by (simp add: left_inverse);
wenzelm@6763
    94
wenzelm@6784
    95
  note calculation = facts
wenzelm@6784
    96
    -- {* first calculational step: init register *};
wenzelm@6763
    97
wenzelm@6784
    98
  have "... = x * inv x * x";
wenzelm@6763
    99
    by (simp add: assoc);
wenzelm@6763
   100
wenzelm@6784
   101
  note calculation = trans[APP calculation facts]
wenzelm@6784
   102
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   103
wenzelm@6763
   104
  have "... = one * x";
wenzelm@6763
   105
    by (simp add: right_inverse);
wenzelm@6763
   106
wenzelm@6784
   107
  note calculation = trans[APP calculation facts]
wenzelm@6784
   108
    -- {* general calculational step: compose with transitivity rule *};
wenzelm@6763
   109
wenzelm@6763
   110
  have "... = x";
wenzelm@6763
   111
    by (simp add: left_unit);
wenzelm@6763
   112
wenzelm@6784
   113
  note calculation = trans[APP calculation facts]
wenzelm@6784
   114
    -- {* final calculational step: compose with transitivity rule ... *};
wenzelm@6784
   115
  from calculation
wenzelm@6784
   116
    -- {* ... and pick up final result *};
wenzelm@6763
   117
wenzelm@6763
   118
  show ??thesis; .;
wenzelm@6784
   119
wenzelm@6763
   120
qed;
wenzelm@6763
   121
wenzelm@6763
   122
wenzelm@6763
   123
end;