src/HOL/Integ/Ring.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/Ring.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996 TU Muenchen
     5 
     6 Derives a few equational consequences about rings
     7 and defines cring_simpl, a simplification tactic for commutative rings.
     8 *)
     9 
    10 open Ring;
    11 
    12 (***
    13 It is not clear if all thsese rules, esp. distributivity, should be part
    14 of the default simpset. At the moment they are because they are used in the
    15 decision procedure.
    16 ***)   
    17 Addsimps [times_assoc,times_commute,distribL,distribR];
    18 
    19 goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
    20 br trans 1;
    21 br times_commute 1;
    22 br trans 1;
    23 br times_assoc 1;
    24 by(Simp_tac 1);
    25 qed "times_commuteL";
    26 Addsimps [times_commuteL];
    27 
    28 val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
    29 
    30 goal Ring.thy "!!x::'a::ring. zero*x = zero";
    31 br trans 1;
    32  br right_inv 2;
    33 br trans 1;
    34  br plus_cong 2;
    35   br refl 3;
    36  br trans 2;
    37   br times_cong 3;
    38    br zeroL 3;
    39   br refl 3;
    40  br (distribR RS sym) 2;
    41 br trans 1;
    42  br(plus_assoc RS sym) 2;
    43 br trans 1;
    44  br plus_cong 2;
    45   br refl 2;
    46  br (right_inv RS sym) 2;
    47 br (zeroR RS sym) 1;
    48 qed "mult_zeroL";
    49 
    50 goal Ring.thy "!!x::'a::ring. x*zero = zero";
    51 br trans 1;
    52  br right_inv 2;
    53 br trans 1;
    54  br plus_cong 2;
    55   br refl 3;
    56  br trans 2;
    57   br times_cong 3;
    58    br zeroL 4;
    59   br refl 3;
    60  br (distribL RS sym) 2;
    61 br trans 1;
    62  br(plus_assoc RS sym) 2;
    63 br trans 1;
    64  br plus_cong 2;
    65   br refl 2;
    66  br (right_inv RS sym) 2;
    67 br (zeroR RS sym) 1;
    68 qed "mult_zeroR";
    69 
    70 goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
    71 br trans 1;
    72  br zeroL 2;
    73 br trans 1;
    74  br plus_cong 2;
    75   br refl 3;
    76  br mult_zeroL 2;
    77 br trans 1;
    78  br plus_cong 2;
    79   br refl 3;
    80  br times_cong 2;
    81   br left_inv 2;
    82  br refl 2;
    83 br trans 1;
    84  br plus_cong 2;
    85   br refl 3;
    86  br (distribR RS sym) 2;
    87 br trans 1;
    88  br(plus_assoc RS sym) 2;
    89 br trans 1;
    90  br plus_cong 2;
    91   br refl 2;
    92  br (right_inv RS sym) 2;
    93 br (zeroR RS sym) 1;
    94 qed "mult_invL";
    95 
    96 goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
    97 br trans 1;
    98  br zeroL 2;
    99 br trans 1;
   100  br plus_cong 2;
   101   br refl 3;
   102  br mult_zeroR 2;
   103 br trans 1;
   104  br plus_cong 2;
   105   br refl 3;
   106  br times_cong 2;
   107   br refl 2;
   108  br left_inv 2;
   109 br trans 1;
   110  br plus_cong 2;
   111   br refl 3;
   112  br (distribL RS sym) 2;
   113 br trans 1;
   114  br(plus_assoc RS sym) 2;
   115 br trans 1;
   116  br plus_cong 2;
   117   br refl 2;
   118  br (right_inv RS sym) 2;
   119 br (zeroR RS sym) 1;
   120 qed "mult_invR";
   121 
   122 Addsimps[mult_invL,mult_invR];
   123 
   124 
   125 goal Ring.thy "!!x::'a::ring. x*(y-z) = x*y - x*z";
   126 by(stac minus_inv 1);
   127 br sym 1;
   128 by(stac minus_inv 1);
   129 by(Simp_tac 1);
   130 qed "minus_distribL";
   131 
   132 goal Ring.thy "!!x::'a::ring. (x-y)*z = x*z - y*z";
   133 by(stac minus_inv 1);
   134 br sym 1;
   135 by(stac minus_inv 1);
   136 by(Simp_tac 1);
   137 qed "minus_distribR";
   138 
   139 Addsimps [minus_distribL,minus_distribR];
   140 
   141 (*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
   142      MUST be tried first ***)
   143 val cring_simp =
   144   let val phase1 = !simpset addsimps
   145                    [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
   146       val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
   147                                     zeroL,zeroR,mult_zeroL,mult_zeroR]
   148   in simp_tac phase1 THEN' simp_tac phase2 end;