src/HOL/ex/Ring.ML
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 8936 a1c426541757
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Integ/Ring.ML
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1996 TU Muenchen
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     5
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     6
Derives a few equational consequences about rings
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     7
and defines cring_simpl, a simplification tactic for commutative rings.
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     8
*)
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
     9
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    10
Goal "!!x::'a::cring. x*(y*z)=y*(x*z)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    11
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    12
by (rtac times_commute 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    13
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    14
by (rtac times_assoc 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    15
by (simp_tac (HOL_basic_ss addsimps [times_commute]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    16
qed "times_commuteL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    17
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    18
val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    19
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    20
Goal "!!x::'a::ring. 0*x = 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    21
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    22
 by (rtac right_inv 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    23
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    24
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    25
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    26
 by (rtac trans 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    27
  by (rtac times_cong 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    28
   by (rtac zeroL 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    29
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    30
 by (rtac (distribR RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    31
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    32
 by (rtac (plus_assoc RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    33
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    34
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    35
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    36
 by (rtac (right_inv RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    37
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    38
qed "mult_zeroL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    39
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    40
Goal "!!x::'a::ring. x*0 = 0";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    41
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    42
 by (rtac right_inv 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    43
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    44
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    45
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    46
 by (rtac trans 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    47
  by (rtac times_cong 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    48
   by (rtac zeroL 4);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    49
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    50
 by (rtac (distribL RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    51
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    52
 by (rtac (plus_assoc RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    53
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    54
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    55
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    56
 by (rtac (right_inv RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    57
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    58
qed "mult_zeroR";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    59
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    60
Goal "!!x::'a::ring. (0-x)*y = 0-(x*y)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    61
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    62
 by (rtac zeroL 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    63
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    64
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    65
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    66
 by (rtac mult_zeroL 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    67
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    68
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    69
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    70
 by (rtac times_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    71
  by (rtac left_inv 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    72
 by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    73
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    74
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    75
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    76
 by (rtac (distribR RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    77
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    78
 by (rtac (plus_assoc RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    79
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    80
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    81
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    82
 by (rtac (right_inv RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    83
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    84
qed "mult_invL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    85
8936
a1c426541757 Now that 0 is overloaded, constant "zero" and its type class "zero" are
paulson
parents: 5078
diff changeset
    86
Goal "!!x::'a::ring. x*(0-y) = 0-(x*y)";
5078
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    87
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    88
 by (rtac zeroL 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    89
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    90
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    91
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    92
 by (rtac mult_zeroR 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    93
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    94
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    95
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    96
 by (rtac times_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    97
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    98
 by (rtac left_inv 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
    99
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   100
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   101
  by (rtac refl 3);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   102
 by (rtac (distribL RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   103
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   104
 by (rtac (plus_assoc RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   105
by (rtac trans 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   106
 by (rtac plus_cong 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   107
  by (rtac refl 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   108
 by (rtac (right_inv RS sym) 2);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   109
by (rtac (zeroR RS sym) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   110
qed "mult_invR";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   111
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   112
Goal "x*(y-z) = (x*y - x*z::'a::ring)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   113
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   114
by (simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   115
qed "minus_distribL";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   116
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   117
Goal "(x-y)*z = (x*z - y*z::'a::ring)";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   118
by (mk_group1_tac 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   119
by (simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   120
qed "minus_distribR";
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   121
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   122
val cring_simps = [times_assoc,times_commute,times_commuteL,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   123
                   distribL,distribR,minus_distribL,minus_distribR]
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   124
                  @ agroup2_simps;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   125
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   126
val cring_tac =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   127
  let val ss = HOL_basic_ss addsimps cring_simps
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   128
  in simp_tac ss end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   129
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   130
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   131
(*** The order [minus_plusL3,minus_plusL2] is important because minus_plusL3
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   132
     MUST be tried first
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   133
val cring_simp =
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   134
  let val phase1 = simpset() addsimps
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   135
                   [plus_minusL,minus_plusR,minus_minusR,plus_minusR]
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   136
      val phase2 = HOL_ss addsimps [minus_plusL3,minus_plusL2,
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   137
                                    zeroL,zeroR,mult_zeroL,mult_zeroR]
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   138
  in simp_tac phase1 THEN' simp_tac phase2 end;
7b5ea59c0275 Installation of target HOL-Real
paulson
parents:
diff changeset
   139
***)