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