src/HOL/Integ/Group.ML
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2281 e00c13a29eda
child 3018 e65b60b28341
permissions -rw-r--r--
added AxClasses test;
     1 (*  Title:      HOL/Integ/Group.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TU Muenchen
     5 *)
     6 
     7 open Group;
     8 
     9 Addsimps [zeroL,zeroR,plus_assoc,plus_commute];
    10 
    11 goal Group.thy "!!x::'a::add_group. (zero-x)+(x+y) = y";
    12 br trans 1;
    13 br (plus_assoc RS sym) 1;
    14 by(stac left_inv 1);
    15 br zeroL 1;
    16 qed "left_inv2";
    17 
    18 goal Group.thy "!!x::'a::add_group. (zero-(zero-x)) = x";
    19 br trans 1;
    20 by(res_inst_tac [("x","zero-x")] left_inv2 2);
    21 by(stac left_inv 1);
    22 br (zeroR RS sym) 1;
    23 qed "inv_inv";
    24 
    25 goal Group.thy "zero-zero = (zero::'a::add_group)";
    26 br trans 1;
    27 br (zeroR RS sym) 1;
    28 br trans 1;
    29 by(res_inst_tac [("x","zero")] left_inv2 2);
    30 by(Simp_tac 1);
    31 qed "inv_zero";
    32 
    33 goal Group.thy "!!x::'a::add_group. x+(zero-x) = zero";
    34 br trans 1;
    35 by(res_inst_tac [("x","zero-x")] left_inv 2);
    36 by(stac inv_inv 1);
    37 br refl 1;
    38 qed "right_inv";
    39 
    40 goal Group.thy "!!x::'a::add_group. x+((zero-x)+y) = y";
    41 br trans 1;
    42 by(res_inst_tac [("x","zero-x")] left_inv2 2);
    43 by(stac inv_inv 1);
    44 br refl 1;
    45 qed "right_inv2";
    46 
    47 goal Group.thy "!!x::'a::add_group. x-x = zero";
    48 by(stac minus_inv 1);
    49 br right_inv 1;
    50 qed "minus_self_zero";
    51 Addsimps [minus_self_zero];
    52 
    53 goal Group.thy "!!x::'a::add_group. x-zero = x";
    54 by(stac minus_inv 1);
    55 by(stac inv_zero 1);
    56 br zeroR 1;
    57 qed "minus_zero";
    58 Addsimps [minus_zero];
    59 
    60 val plus_cong = read_instantiate [("f1","op +")] (arg_cong RS cong);
    61 
    62 goal Group.thy "!!x::'a::add_group. zero-(x+y) = (zero-y)+(zero-x)";
    63 br trans 1;
    64  br zeroR 2;
    65 br trans 1;
    66  br plus_cong 2;
    67   br refl 2;
    68  by(res_inst_tac [("x","x+y")] right_inv 2);
    69 br trans 1;
    70  br plus_assoc 2;
    71 br trans 1;
    72  br plus_cong 2;
    73   by(simp_tac (!simpset addsimps [left_inv,left_inv2,right_inv,right_inv2]) 2);
    74  br refl 2;
    75 br (zeroL RS sym) 1;
    76 qed "inv_plus";
    77 
    78 goal Group.thy "x+(y+z)=y+(x+z::'a::add_agroup)";
    79 br trans 1;
    80 br plus_commute 1;
    81 br trans 1;
    82 br plus_assoc 1;
    83 by(Simp_tac 1);
    84 qed "plus_commuteL";
    85 Addsimps [plus_commuteL];
    86 
    87 Addsimps [inv_inv,inv_plus];
    88 
    89 (* Phase 1 *)
    90 
    91 goal Group.thy "!!x::'a::add_agroup. (x+(zero-y))+z = (x+z)+(zero-y)";
    92 by(Simp_tac 1);
    93 val lemma = result();
    94 bind_thm("plus_minusL",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
    95 
    96 goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+z)) = (x+(zero-y))+(zero-z)";
    97 by(Simp_tac 1);
    98 val lemma = result();
    99 bind_thm("minus_plusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   100 
   101 goal Group.thy "!!x::'a::add_agroup. x+(zero-(y+(zero-z))) = (x+z)+(zero-y)";
   102 by(Simp_tac 1);
   103 val lemma = result();
   104 bind_thm("minus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   105 
   106 goal Group.thy "!!x::'a::add_agroup. x+(y+(zero-z)) = (x+y)+(zero-z)";
   107 by(Simp_tac 1);
   108 val lemma = result();
   109 bind_thm("plus_minusR",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   110 
   111 (* Phase 2 *)
   112 
   113 goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-z) = x+(y+(zero-z))";
   114 by(Simp_tac 1);
   115 val lemma = result();
   116 bind_thm("minus_plusL2",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   117 
   118 goal Group.thy "!!x::'a::add_agroup. (x+y)+(zero-x) = y";
   119 br (plus_assoc RS trans) 1;
   120 br trans 1;
   121  br plus_cong 1;
   122   br refl 1;
   123  br right_inv2 2;
   124 br plus_commute 1;
   125 val lemma = result();
   126 bind_thm("minus_plusL3",rewrite_rule[minus_inv RS sym RS eq_reflection]lemma);
   127