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