src/HOL/AxClasses/Tutorial/Group.ML
author nipkow
Mon Oct 21 09:50:50 1996 +0200 (1996-10-21)
changeset 2115 9709f9188549
parent 1465 5d7a7e439cec
child 2907 0e272e4c7cb2
permissions -rw-r--r--
Added trans_tac (see Provers/nat_transitive.ML)
wenzelm@1247
     1
(*  Title:      HOL/AxClasses/Tutorial/Group.ML
wenzelm@1247
     2
    ID:         $Id$
wenzelm@1247
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@1247
     4
wenzelm@1247
     5
Some basic theorems of group theory.
wenzelm@1247
     6
*)
wenzelm@1247
     7
wenzelm@1247
     8
open Group;
wenzelm@1247
     9
wenzelm@1247
    10
fun sub r = standard (r RS subst);
wenzelm@1247
    11
fun ssub r = standard (r RS ssubst);
wenzelm@1247
    12
wenzelm@1247
    13
wenzelm@1247
    14
goal Group.thy "x <*> inv x = (1::'a::group)";
clasohm@1465
    15
by (rtac (sub left_unit) 1);
wenzelm@1247
    16
back();
clasohm@1465
    17
by (rtac (sub assoc) 1);
clasohm@1465
    18
by (rtac (sub left_inv) 1);
wenzelm@1247
    19
back();
wenzelm@1247
    20
back();
clasohm@1465
    21
by (rtac (ssub assoc) 1);
wenzelm@1247
    22
back();
clasohm@1465
    23
by (rtac (ssub left_inv) 1);
clasohm@1465
    24
by (rtac (ssub assoc) 1);
clasohm@1465
    25
by (rtac (ssub left_unit) 1);
clasohm@1465
    26
by (rtac (ssub left_inv) 1);
clasohm@1465
    27
by (rtac refl 1);
wenzelm@1247
    28
qed "right_inv";
wenzelm@1247
    29
wenzelm@1247
    30
wenzelm@1247
    31
goal Group.thy "x <*> 1 = (x::'a::group)";
clasohm@1465
    32
by (rtac (sub left_inv) 1);
clasohm@1465
    33
by (rtac (sub assoc) 1);
clasohm@1465
    34
by (rtac (ssub right_inv) 1);
clasohm@1465
    35
by (rtac (ssub left_unit) 1);
clasohm@1465
    36
by (rtac refl 1);
wenzelm@1247
    37
qed "right_unit";
wenzelm@1247
    38
wenzelm@1247
    39
wenzelm@1247
    40
goal Group.thy "e <*> x = x --> e = (1::'a::group)";
clasohm@1465
    41
by (rtac impI 1);
clasohm@1465
    42
by (rtac (sub right_unit) 1);
wenzelm@1247
    43
back();
wenzelm@1247
    44
by (res_inst_tac [("x", "x")] (sub right_inv) 1);
clasohm@1465
    45
by (rtac (sub assoc) 1);
clasohm@1465
    46
by (rtac arg_cong 1);
wenzelm@1247
    47
back();
clasohm@1465
    48
by (assume_tac 1);
wenzelm@1247
    49
qed "strong_one_unit";
wenzelm@1247
    50
wenzelm@1247
    51
wenzelm@1247
    52
goal Group.thy "EX! e. ALL x. e <*> x = (x::'a::group)";
clasohm@1465
    53
by (rtac ex1I 1);
clasohm@1465
    54
by (rtac allI 1);
clasohm@1465
    55
by (rtac left_unit 1);
clasohm@1465
    56
by (rtac mp 1);
clasohm@1465
    57
by (rtac strong_one_unit 1);
clasohm@1465
    58
by (etac allE 1);
clasohm@1465
    59
by (assume_tac 1);
wenzelm@1247
    60
qed "ex1_unit";
wenzelm@1247
    61
wenzelm@1247
    62
wenzelm@1247
    63
goal Group.thy "ALL x. EX! e. e <*> x = (x::'a::group)";
clasohm@1465
    64
by (rtac allI 1);
clasohm@1465
    65
by (rtac ex1I 1);
clasohm@1465
    66
by (rtac left_unit 1);
clasohm@1465
    67
by (rtac (strong_one_unit RS mp) 1);
clasohm@1465
    68
by (assume_tac 1);
wenzelm@1247
    69
qed "ex1_unit'";
wenzelm@1247
    70
wenzelm@1247
    71
wenzelm@1247
    72
goal Group.thy "y <*> x = 1 --> y = inv (x::'a::group)";
clasohm@1465
    73
by (rtac impI 1);
clasohm@1465
    74
by (rtac (sub right_unit) 1);
wenzelm@1247
    75
back();
wenzelm@1247
    76
back();
clasohm@1465
    77
by (rtac (sub right_unit) 1);
wenzelm@1247
    78
by (res_inst_tac [("x", "x")] (sub right_inv) 1);
clasohm@1465
    79
by (rtac (sub assoc) 1);
clasohm@1465
    80
by (rtac (sub assoc) 1);
clasohm@1465
    81
by (rtac arg_cong 1);
wenzelm@1247
    82
back();
clasohm@1465
    83
by (rtac (ssub left_inv) 1);
clasohm@1465
    84
by (assume_tac 1);
wenzelm@1247
    85
qed "one_inv";
wenzelm@1247
    86
wenzelm@1247
    87
wenzelm@1247
    88
goal Group.thy "ALL x. EX! y. y <*> x = (1::'a::group)";
clasohm@1465
    89
by (rtac allI 1);
clasohm@1465
    90
by (rtac ex1I 1);
clasohm@1465
    91
by (rtac left_inv 1);
clasohm@1465
    92
by (rtac mp 1);
clasohm@1465
    93
by (rtac one_inv 1);
clasohm@1465
    94
by (assume_tac 1);
wenzelm@1247
    95
qed "ex1_inv";
wenzelm@1247
    96
wenzelm@1247
    97
wenzelm@1247
    98
goal Group.thy "inv (x <*> y) = inv y <*> inv (x::'a::group)";
clasohm@1465
    99
by (rtac sym 1);
clasohm@1465
   100
by (rtac mp 1);
clasohm@1465
   101
by (rtac one_inv 1);
clasohm@1465
   102
by (rtac (ssub assoc) 1);
clasohm@1465
   103
by (rtac (sub assoc) 1);
wenzelm@1247
   104
back();
clasohm@1465
   105
by (rtac (ssub left_inv) 1);
clasohm@1465
   106
by (rtac (ssub left_unit) 1);
clasohm@1465
   107
by (rtac (ssub left_inv) 1);
clasohm@1465
   108
by (rtac refl 1);
wenzelm@1247
   109
qed "inv_product";
wenzelm@1247
   110
wenzelm@1247
   111
wenzelm@1247
   112
goal Group.thy "inv (inv x) = (x::'a::group)";
clasohm@1465
   113
by (rtac sym 1);
clasohm@1465
   114
by (rtac (one_inv RS mp) 1);
clasohm@1465
   115
by (rtac (ssub right_inv) 1);
clasohm@1465
   116
by (rtac refl 1);
wenzelm@1247
   117
qed "inv_inv";
wenzelm@1247
   118