src/HOL/Integ/IntDef.ML
author paulson
Thu, 15 Jul 1999 10:34:37 +0200
changeset 7010 63120b6dca50
parent 6991 500038b6063b
child 7127 48e235179ffb
permissions -rw-r--r--
more renaming of theorems from _nat to _int (corresponding to a function that was similarly renamed some time ago Also new theorem zmult_int
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
     1
(*  Title:      IntDef.ML
691c70898518 new files in Integ
paulson
parents:
diff changeset
     2
    ID:         $Id$
691c70898518 new files in Integ
paulson
parents:
diff changeset
     3
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
691c70898518 new files in Integ
paulson
parents:
diff changeset
     4
    Copyright   1993  University of Cambridge
691c70898518 new files in Integ
paulson
parents:
diff changeset
     5
691c70898518 new files in Integ
paulson
parents:
diff changeset
     6
The integers as equivalence classes over nat*nat.
691c70898518 new files in Integ
paulson
parents:
diff changeset
     7
*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
     8
691c70898518 new files in Integ
paulson
parents:
diff changeset
     9
691c70898518 new files in Integ
paulson
parents:
diff changeset
    10
(*** Proving that intrel is an equivalence relation ***)
691c70898518 new files in Integ
paulson
parents:
diff changeset
    11
691c70898518 new files in Integ
paulson
parents:
diff changeset
    12
val eqa::eqb::prems = goal Arith.thy 
691c70898518 new files in Integ
paulson
parents:
diff changeset
    13
    "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
691c70898518 new files in Integ
paulson
parents:
diff changeset
    14
\       x1 + y3 = x3 + y1";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    15
by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    16
by (rtac (add_left_commute RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    17
by (stac eqb 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    18
by (rtac (add_left_commute RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    19
by (stac eqa 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    20
by (rtac (add_left_commute) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    21
qed "integ_trans_lemma";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    22
691c70898518 new files in Integ
paulson
parents:
diff changeset
    23
(** Natural deduction for intrel **)
691c70898518 new files in Integ
paulson
parents:
diff changeset
    24
691c70898518 new files in Integ
paulson
parents:
diff changeset
    25
Goalw  [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    26
by (Fast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    27
qed "intrelI";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    28
691c70898518 new files in Integ
paulson
parents:
diff changeset
    29
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
    30
Goalw [intrel_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
    31
  "p: intrel --> (EX x1 y1 x2 y2. \
691c70898518 new files in Integ
paulson
parents:
diff changeset
    32
\                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    33
by (Fast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    34
qed "intrelE_lemma";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    35
691c70898518 new files in Integ
paulson
parents:
diff changeset
    36
val [major,minor] = Goal
691c70898518 new files in Integ
paulson
parents:
diff changeset
    37
  "[| p: intrel;  \
691c70898518 new files in Integ
paulson
parents:
diff changeset
    38
\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
691c70898518 new files in Integ
paulson
parents:
diff changeset
    39
\  ==> Q";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    40
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    41
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
691c70898518 new files in Integ
paulson
parents:
diff changeset
    42
qed "intrelE";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    43
691c70898518 new files in Integ
paulson
parents:
diff changeset
    44
AddSIs [intrelI];
691c70898518 new files in Integ
paulson
parents:
diff changeset
    45
AddSEs [intrelE];
691c70898518 new files in Integ
paulson
parents:
diff changeset
    46
691c70898518 new files in Integ
paulson
parents:
diff changeset
    47
Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    48
by (Fast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    49
qed "intrel_iff";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    50
691c70898518 new files in Integ
paulson
parents:
diff changeset
    51
Goal "(x,x): intrel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    52
by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    53
qed "intrel_refl";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    54
691c70898518 new files in Integ
paulson
parents:
diff changeset
    55
Goalw [equiv_def, refl_def, sym_def, trans_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
    56
    "equiv {x::(nat*nat).True} intrel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    57
by (fast_tac (claset() addSIs [intrel_refl] 
691c70898518 new files in Integ
paulson
parents:
diff changeset
    58
                        addSEs [sym, integ_trans_lemma]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    59
qed "equiv_intrel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    60
691c70898518 new files in Integ
paulson
parents:
diff changeset
    61
val equiv_intrel_iff =
691c70898518 new files in Integ
paulson
parents:
diff changeset
    62
    [TrueI, TrueI] MRS 
691c70898518 new files in Integ
paulson
parents:
diff changeset
    63
    ([CollectI, CollectI] MRS 
691c70898518 new files in Integ
paulson
parents:
diff changeset
    64
    (equiv_intrel RS eq_equiv_class_iff));
691c70898518 new files in Integ
paulson
parents:
diff changeset
    65
691c70898518 new files in Integ
paulson
parents:
diff changeset
    66
Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    67
by (Fast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    68
qed "intrel_in_integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    69
691c70898518 new files in Integ
paulson
parents:
diff changeset
    70
Goal "inj_on Abs_Integ Integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    71
by (rtac inj_on_inverseI 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    72
by (etac Abs_Integ_inverse 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    73
qed "inj_on_Abs_Integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    74
691c70898518 new files in Integ
paulson
parents:
diff changeset
    75
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
691c70898518 new files in Integ
paulson
parents:
diff changeset
    76
          intrel_iff, intrel_in_integ, Abs_Integ_inverse];
691c70898518 new files in Integ
paulson
parents:
diff changeset
    77
691c70898518 new files in Integ
paulson
parents:
diff changeset
    78
Goal "inj(Rep_Integ)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    79
by (rtac inj_inverseI 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    80
by (rtac Rep_Integ_inverse 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    81
qed "inj_Rep_Integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
    82
691c70898518 new files in Integ
paulson
parents:
diff changeset
    83
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
    84
(** int: the injection from "nat" to "int" **)
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    85
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
    86
Goal "inj int";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    87
by (rtac injI 1);
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
    88
by (rewtac int_def);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    89
by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    90
by (REPEAT (rtac intrel_in_integ 1));
691c70898518 new files in Integ
paulson
parents:
diff changeset
    91
by (dtac eq_equiv_class 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    92
by (rtac equiv_intrel 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    93
by (Fast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
    94
by Safe_tac;
691c70898518 new files in Integ
paulson
parents:
diff changeset
    95
by (Asm_full_simp_tac 1);
6991
500038b6063b renamed inj_nat to inj_int
paulson
parents: 6917
diff changeset
    96
qed "inj_int";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
    97
691c70898518 new files in Integ
paulson
parents:
diff changeset
    98
691c70898518 new files in Integ
paulson
parents:
diff changeset
    99
(**** zminus: unary negation on Integ ****)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   100
691c70898518 new files in Integ
paulson
parents:
diff changeset
   101
Goalw [congruent_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   102
  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   103
by Safe_tac;
691c70898518 new files in Integ
paulson
parents:
diff changeset
   104
by (asm_simp_tac (simpset() addsimps add_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   105
qed "zminus_congruent";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   106
691c70898518 new files in Integ
paulson
parents:
diff changeset
   107
691c70898518 new files in Integ
paulson
parents:
diff changeset
   108
(*Resolve th against the corresponding facts for zminus*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   109
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   110
691c70898518 new files in Integ
paulson
parents:
diff changeset
   111
Goalw [zminus_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   112
      "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   113
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   114
by (simp_tac (simpset() addsimps 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   115
   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   116
qed "zminus";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   117
691c70898518 new files in Integ
paulson
parents:
diff changeset
   118
(*by lcp*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   119
val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   120
by (res_inst_tac [("x1","z")] 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   121
    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   122
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   123
by (res_inst_tac [("p","x")] PairE 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   124
by (rtac prem 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   125
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   126
qed "eq_Abs_Integ";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   127
691c70898518 new files in Integ
paulson
parents:
diff changeset
   128
Goal "- (- z) = (z::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   129
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   130
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   131
qed "zminus_zminus";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   132
Addsimps [zminus_zminus];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   133
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   134
Goal "inj(%z::int. -z)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   135
by (rtac injI 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   136
by (dres_inst_tac [("f","uminus")] arg_cong 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   137
by (Asm_full_simp_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   138
qed "inj_zminus";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   139
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   140
Goalw [int_def] "- (int 0) = int 0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   141
by (simp_tac (simpset() addsimps [zminus]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   142
qed "zminus_int0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   143
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   144
Addsimps [zminus_int0];
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   145
691c70898518 new files in Integ
paulson
parents:
diff changeset
   146
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   147
(**** neg: the test for negative integers ****)
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   148
691c70898518 new files in Integ
paulson
parents:
diff changeset
   149
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   150
Goalw [neg_def, int_def] "~ neg(int n)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   151
by (Simp_tac 1);
7010
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   152
qed "not_neg_int";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   153
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   154
Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   155
by (simp_tac (simpset() addsimps [zminus]) 1);
7010
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   156
qed "neg_zminus_int";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   157
7010
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   158
Addsimps [neg_zminus_int, not_neg_int]; 
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   159
691c70898518 new files in Integ
paulson
parents:
diff changeset
   160
691c70898518 new files in Integ
paulson
parents:
diff changeset
   161
(**** zadd: addition on Integ ****)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   162
691c70898518 new files in Integ
paulson
parents:
diff changeset
   163
(** Congruence property for addition **)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   164
691c70898518 new files in Integ
paulson
parents:
diff changeset
   165
Goalw [congruent2_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   166
    "congruent2 intrel (%p1 p2.                  \
691c70898518 new files in Integ
paulson
parents:
diff changeset
   167
\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   168
(*Proof via congruent2_commuteI seems longer*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   169
by Safe_tac;
5983
79e301a6a51b At last: linear arithmetic for nat!
nipkow
parents: 5758
diff changeset
   170
by (Asm_simp_tac 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   171
qed "zadd_congruent2";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   172
691c70898518 new files in Integ
paulson
parents:
diff changeset
   173
(*Resolve th against the corresponding facts for zadd*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   174
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   175
691c70898518 new files in Integ
paulson
parents:
diff changeset
   176
Goalw [zadd_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   177
  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
691c70898518 new files in Integ
paulson
parents:
diff changeset
   178
\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   179
by (asm_simp_tac
691c70898518 new files in Integ
paulson
parents:
diff changeset
   180
    (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   181
qed "zadd";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   182
691c70898518 new files in Integ
paulson
parents:
diff changeset
   183
Goal "- (z + w) = - z + - (w::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   184
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   185
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   186
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   187
qed "zminus_zadd_distrib";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   188
Addsimps [zminus_zadd_distrib];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   189
691c70898518 new files in Integ
paulson
parents:
diff changeset
   190
Goal "(z::int) + w = w + z";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   191
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   192
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   193
by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   194
qed "zadd_commute";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   195
691c70898518 new files in Integ
paulson
parents:
diff changeset
   196
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   197
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   198
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   199
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   200
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   201
qed "zadd_assoc";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   202
691c70898518 new files in Integ
paulson
parents:
diff changeset
   203
(*For AC rewriting*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   204
Goal "(x::int)+(y+z)=y+(x+z)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   205
by (rtac (zadd_commute RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   206
by (rtac (zadd_assoc RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   207
by (rtac (zadd_commute RS arg_cong) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   208
qed "zadd_left_commute";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   209
691c70898518 new files in Integ
paulson
parents:
diff changeset
   210
(*Integer addition is an AC operator*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   211
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   212
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   213
Goalw [int_def] "(int m) + (int n) = int (m + n)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   214
by (simp_tac (simpset() addsimps [zadd]) 1);
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   215
qed "zadd_int";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   216
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   217
Goal "(int m) + (int n + z) = int (m + n) + z";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   218
by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   219
qed "zadd_int_left";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   220
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   221
Goal "int (Suc m) = int 1 + (int m)";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   222
by (simp_tac (simpset() addsimps [zadd_int]) 1);
6717
70b251dc7055 int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc
paulson
parents: 6674
diff changeset
   223
qed "int_Suc_int_1";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   224
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   225
Goalw [int_def] "int 0 + z = z";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   226
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   227
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   228
qed "zadd_int0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   229
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   230
Goal "z + int 0 = z";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   231
by (rtac (zadd_commute RS trans) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   232
by (rtac zadd_int0 1);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   233
qed "zadd_int0_right";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   234
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   235
Goalw [int_def] "z + (- z) = int 0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   236
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   237
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   238
qed "zadd_zminus_inverse";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   239
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   240
Goal "(- z) + z = int 0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   241
by (rtac (zadd_commute RS trans) 1);
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   242
by (rtac zadd_zminus_inverse 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   243
qed "zadd_zminus_inverse2";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   244
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   245
Addsimps [zadd_int0, zadd_int0_right,
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   246
	  zadd_zminus_inverse, zadd_zminus_inverse2];
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   247
691c70898518 new files in Integ
paulson
parents:
diff changeset
   248
Goal "z + (- z + w) = (w::int)";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   249
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   250
qed "zadd_zminus_cancel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   251
691c70898518 new files in Integ
paulson
parents:
diff changeset
   252
Goal "(-z) + (z + w) = (w::int)";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   253
by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   254
qed "zminus_zadd_cancel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   255
691c70898518 new files in Integ
paulson
parents:
diff changeset
   256
Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   257
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   258
Goal "int 0 - x = -x";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   259
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   260
qed "zdiff_int0";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   261
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   262
Goal "x - int 0 = x";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   263
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   264
qed "zdiff_int0_right";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   265
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   266
Goal "x - x = int 0";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   267
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   268
qed "zdiff_self";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   269
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   270
Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   271
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   272
691c70898518 new files in Integ
paulson
parents:
diff changeset
   273
(** Lemmas **)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   274
691c70898518 new files in Integ
paulson
parents:
diff changeset
   275
Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   276
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   277
qed "zadd_assoc_cong";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   278
691c70898518 new files in Integ
paulson
parents:
diff changeset
   279
Goal "(z::int) + (v + w) = v + (z + w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   280
by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   281
qed "zadd_assoc_swap";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   282
691c70898518 new files in Integ
paulson
parents:
diff changeset
   283
691c70898518 new files in Integ
paulson
parents:
diff changeset
   284
(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   285
691c70898518 new files in Integ
paulson
parents:
diff changeset
   286
(**** zmult: multiplication on Integ ****)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   287
691c70898518 new files in Integ
paulson
parents:
diff changeset
   288
(** Congruence property for multiplication **)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   289
691c70898518 new files in Integ
paulson
parents:
diff changeset
   290
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   291
by (simp_tac (simpset() addsimps add_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   292
qed "zmult_congruent_lemma";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   293
691c70898518 new files in Integ
paulson
parents:
diff changeset
   294
Goal "congruent2 intrel (%p1 p2.                 \
691c70898518 new files in Integ
paulson
parents:
diff changeset
   295
\               split (%x1 y1. split (%x2 y2.   \
691c70898518 new files in Integ
paulson
parents:
diff changeset
   296
\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   297
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   298
by (pair_tac "w" 2);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   299
by (rename_tac "z1 z2" 2);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   300
by Safe_tac;
691c70898518 new files in Integ
paulson
parents:
diff changeset
   301
by (rewtac split_def);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   302
by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   303
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   304
                           addsimps add_ac@mult_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   305
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   306
by (rtac (zmult_congruent_lemma RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   307
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   308
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   309
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   310
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   311
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   312
qed "zmult_congruent2";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   313
691c70898518 new files in Integ
paulson
parents:
diff changeset
   314
(*Resolve th against the corresponding facts for zmult*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   315
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   316
691c70898518 new files in Integ
paulson
parents:
diff changeset
   317
Goalw [zmult_def]
691c70898518 new files in Integ
paulson
parents:
diff changeset
   318
   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
691c70898518 new files in Integ
paulson
parents:
diff changeset
   319
\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   320
by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   321
qed "zmult";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   322
691c70898518 new files in Integ
paulson
parents:
diff changeset
   323
Goal "(- z) * w = - (z * (w::int))";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   324
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   325
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   326
by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   327
qed "zmult_zminus";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   328
691c70898518 new files in Integ
paulson
parents:
diff changeset
   329
Goal "(z::int) * w = w * z";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   330
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   331
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   332
by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   333
qed "zmult_commute";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   334
691c70898518 new files in Integ
paulson
parents:
diff changeset
   335
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   336
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   337
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   338
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   339
by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @ 
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   340
                                     add_ac @ mult_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   341
qed "zmult_assoc";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   342
691c70898518 new files in Integ
paulson
parents:
diff changeset
   343
(*For AC rewriting*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   344
Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   345
by (rtac (zmult_commute RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   346
by (rtac (zmult_assoc RS trans) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   347
by (rtac (zmult_commute RS arg_cong) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   348
qed "zmult_left_commute";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   349
691c70898518 new files in Integ
paulson
parents:
diff changeset
   350
(*Integer multiplication is an AC operator*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   351
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   352
691c70898518 new files in Integ
paulson
parents:
diff changeset
   353
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   354
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   355
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   356
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   357
by (asm_simp_tac 
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   358
    (simpset() addsimps [add_mult_distrib2, zadd, zmult] @ 
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   359
                        add_ac @ mult_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   360
qed "zadd_zmult_distrib";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   361
691c70898518 new files in Integ
paulson
parents:
diff changeset
   362
val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
691c70898518 new files in Integ
paulson
parents:
diff changeset
   363
691c70898518 new files in Integ
paulson
parents:
diff changeset
   364
Goal "w * (- z) = - (w * (z::int))";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   365
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   366
qed "zmult_zminus_right";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   367
691c70898518 new files in Integ
paulson
parents:
diff changeset
   368
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   369
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   370
qed "zadd_zmult_distrib2";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   371
6839
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   372
Goalw [zdiff_def] "((z1::int) - z2) * w = (z1 * w) - (z2 * w)";
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   373
by (stac zadd_zmult_distrib 1);
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   374
by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   375
qed "zdiff_zmult_distrib";
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   376
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   377
Goal "(w::int) * (z1 - z2) = (w * z1) - (w * z2)";
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   378
by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   379
qed "zdiff_zmult_distrib2";
da8a39302686 new distributive laws involving * and -
paulson
parents: 6717
diff changeset
   380
7010
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   381
Goalw [int_def] "(int m) * (int n) = int (m * n)";
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   382
by (simp_tac (simpset() addsimps [zmult]) 1);
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   383
qed "zmult_int";
63120b6dca50 more renaming of theorems from _nat to _int (corresponding to a function that
paulson
parents: 6991
diff changeset
   384
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   385
Goalw [int_def] "int 0 * z = int 0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   386
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   387
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   388
qed "zmult_int0";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   389
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   390
Goalw [int_def] "int 1 * z = z";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   391
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   392
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   393
qed "zmult_int1";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   394
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   395
Goal "z * int 0 = int 0";
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   396
by (rtac ([zmult_commute, zmult_int0] MRS trans) 1);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   397
qed "zmult_int0_right";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   398
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   399
Goal "z * int 1 = z";
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   400
by (rtac ([zmult_commute, zmult_int1] MRS trans) 1);
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   401
qed "zmult_int1_right";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   402
6917
eba301caceea Introduction of integer division algorithm
paulson
parents: 6839
diff changeset
   403
Addsimps [zmult_int0, zmult_int0_right, zmult_int1, zmult_int1_right];
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   404
691c70898518 new files in Integ
paulson
parents:
diff changeset
   405
691c70898518 new files in Integ
paulson
parents:
diff changeset
   406
(* Theorems about less and less_equal *)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   407
691c70898518 new files in Integ
paulson
parents:
diff changeset
   408
(*This lemma allows direct proofs of other <-properties*)
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
   409
Goalw [zless_def, neg_def, zdiff_def, int_def] 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   410
    "(w < z) = (EX n. z = w + int(Suc n))";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   411
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   412
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   413
by (Clarify_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   414
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   415
by (safe_tac (claset() addSDs [less_eq_Suc_add]));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   416
by (res_inst_tac [("x","k")] exI 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   417
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   418
qed "zless_iff_Suc_zadd";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   419
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   420
Goal "z < z + int (Suc n)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   421
by (auto_tac (claset(),
691c70898518 new files in Integ
paulson
parents:
diff changeset
   422
	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   423
				  zadd_int]));
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   424
qed "zless_zadd_Suc";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   425
691c70898518 new files in Integ
paulson
parents:
diff changeset
   426
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   427
by (auto_tac (claset(),
691c70898518 new files in Integ
paulson
parents:
diff changeset
   428
	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   429
				  zadd_int]));
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   430
qed "zless_trans";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   431
691c70898518 new files in Integ
paulson
parents:
diff changeset
   432
Goal "!!w::int. z<w ==> ~w<z";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   433
by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   434
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   435
by Safe_tac;
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
   436
by (asm_full_simp_tac (simpset() addsimps [int_def, zadd]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   437
qed "zless_not_sym";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   438
691c70898518 new files in Integ
paulson
parents:
diff changeset
   439
(* [| n<m;  ~P ==> m<n |] ==> P *)
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   440
bind_thm ("zless_asym", zless_not_sym RS swap);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   441
691c70898518 new files in Integ
paulson
parents:
diff changeset
   442
Goal "!!z::int. ~ z<z";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   443
by (resolve_tac [zless_asym RS notI] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   444
by (REPEAT (assume_tac 1));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   445
qed "zless_not_refl";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   446
691c70898518 new files in Integ
paulson
parents:
diff changeset
   447
(* z<z ==> R *)
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   448
bind_thm ("zless_irrefl", zless_not_refl RS notE);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   449
AddSEs [zless_irrefl];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   450
691c70898518 new files in Integ
paulson
parents:
diff changeset
   451
Goal "z<w ==> w ~= (z::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   452
by (Blast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   453
qed "zless_not_refl2";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   454
691c70898518 new files in Integ
paulson
parents:
diff changeset
   455
(* s < t ==> s ~= t *)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   456
bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   457
691c70898518 new files in Integ
paulson
parents:
diff changeset
   458
691c70898518 new files in Integ
paulson
parents:
diff changeset
   459
(*"Less than" is a linear ordering*)
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   460
Goalw [zless_def, neg_def, zdiff_def] 
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   461
    "z<w | z=w | w<(z::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   462
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   463
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   464
by Safe_tac;
691c70898518 new files in Integ
paulson
parents:
diff changeset
   465
by (asm_full_simp_tac
691c70898518 new files in Integ
paulson
parents:
diff changeset
   466
    (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   467
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
5758
27a2b36efd95 corrected auto_tac (applications of unsafe wrappers)
oheimb
parents: 5594
diff changeset
   468
by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac)));
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   469
qed "zless_linear";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   470
691c70898518 new files in Integ
paulson
parents:
diff changeset
   471
Goal "!!w::int. (w ~= z) = (w<z | z<w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   472
by (cut_facts_tac [zless_linear] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   473
by (Blast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   474
qed "int_neq_iff";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   475
691c70898518 new files in Integ
paulson
parents:
diff changeset
   476
(*** eliminates ~= in premises ***)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   477
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   478
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   479
Goal "(int m = int n) = (m = n)"; 
6991
500038b6063b renamed inj_nat to inj_int
paulson
parents: 6917
diff changeset
   480
by (fast_tac (claset() addSEs [inj_int RS injD]) 1); 
5562
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
   481
qed "int_int_eq"; 
02261e6880d1 Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
paulson
parents: 5540
diff changeset
   482
AddIffs [int_int_eq]; 
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   483
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   484
Goal "(int m < int n) = (m<n)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   485
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   486
				  zadd_int]) 1);
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   487
qed "zless_int";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   488
Addsimps [zless_int];
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   489
691c70898518 new files in Integ
paulson
parents:
diff changeset
   490
691c70898518 new files in Integ
paulson
parents:
diff changeset
   491
(*** Properties of <= ***)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   492
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   493
Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   494
by (Simp_tac 1);
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   495
qed "zle_int";
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   496
Addsimps [zle_int];
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   497
691c70898518 new files in Integ
paulson
parents:
diff changeset
   498
Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   499
by (cut_facts_tac [zless_linear] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   500
by (blast_tac (claset() addEs [zless_asym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   501
qed "zle_imp_zless_or_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   502
691c70898518 new files in Integ
paulson
parents:
diff changeset
   503
Goalw [zle_def] "z<w | z=w ==> z <= (w::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   504
by (cut_facts_tac [zless_linear] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   505
by (blast_tac (claset() addEs [zless_asym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   506
qed "zless_or_eq_imp_zle";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   507
691c70898518 new files in Integ
paulson
parents:
diff changeset
   508
Goal "(x <= (y::int)) = (x < y | x=y)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   509
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   510
qed "integ_le_less";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   511
691c70898518 new files in Integ
paulson
parents:
diff changeset
   512
Goal "w <= (w::int)";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   513
by (simp_tac (simpset() addsimps [integ_le_less]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   514
qed "zle_refl";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   515
691c70898518 new files in Integ
paulson
parents:
diff changeset
   516
Goalw [zle_def] "z < w ==> z <= (w::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   517
by (blast_tac (claset() addEs [zless_asym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   518
qed "zless_imp_zle";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   519
691c70898518 new files in Integ
paulson
parents:
diff changeset
   520
(* Axiom 'linorder_linear' of class 'linorder': *)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   521
Goal "(z::int) <= w | w <= z";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   522
by (simp_tac (simpset() addsimps [integ_le_less]) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   523
by (cut_facts_tac [zless_linear] 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   524
by (Blast_tac 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   525
qed "zle_linear";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   526
691c70898518 new files in Integ
paulson
parents:
diff changeset
   527
Goal "[| i <= j; j < k |] ==> i < (k::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   528
by (dtac zle_imp_zless_or_eq 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   529
by (blast_tac (claset() addIs [zless_trans]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   530
qed "zle_zless_trans";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   531
691c70898518 new files in Integ
paulson
parents:
diff changeset
   532
Goal "[| i < j; j <= k |] ==> i < (k::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   533
by (dtac zle_imp_zless_or_eq 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   534
by (blast_tac (claset() addIs [zless_trans]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   535
qed "zless_zle_trans";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   536
691c70898518 new files in Integ
paulson
parents:
diff changeset
   537
Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   538
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
691c70898518 new files in Integ
paulson
parents:
diff changeset
   539
            rtac zless_or_eq_imp_zle, 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   540
	    blast_tac (claset() addIs [zless_trans])]);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   541
qed "zle_trans";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   542
691c70898518 new files in Integ
paulson
parents:
diff changeset
   543
Goal "[| z <= w; w <= z |] ==> z = (w::int)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   544
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
691c70898518 new files in Integ
paulson
parents:
diff changeset
   545
            blast_tac (claset() addEs [zless_asym])]);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   546
qed "zle_anti_sym";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   547
691c70898518 new files in Integ
paulson
parents:
diff changeset
   548
(* Axiom 'order_less_le' of class 'order': *)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   549
Goal "(w::int) < z = (w <= z & w ~= z)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   550
by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   551
by (blast_tac (claset() addSEs [zless_asym]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   552
qed "int_less_le";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   553
691c70898518 new files in Integ
paulson
parents:
diff changeset
   554
(* [| w <= z; w ~= z |] ==> w < z *)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   555
bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   556
691c70898518 new files in Integ
paulson
parents:
diff changeset
   557
691c70898518 new files in Integ
paulson
parents:
diff changeset
   558
691c70898518 new files in Integ
paulson
parents:
diff changeset
   559
(*** Subtraction laws ***)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   560
691c70898518 new files in Integ
paulson
parents:
diff changeset
   561
Goal "x + (y - z) = (x + y) - (z::int)";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   562
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   563
qed "zadd_zdiff_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   564
691c70898518 new files in Integ
paulson
parents:
diff changeset
   565
Goal "(x - y) + z = (x + z) - (y::int)";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   566
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   567
qed "zdiff_zadd_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   568
691c70898518 new files in Integ
paulson
parents:
diff changeset
   569
Goal "(x - y) - z = x - (y + (z::int))";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   570
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   571
qed "zdiff_zdiff_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   572
691c70898518 new files in Integ
paulson
parents:
diff changeset
   573
Goal "x - (y - z) = (x + z) - (y::int)";
5540
0f16c3b66ab4 much renaming and reorganization
paulson
parents: 5508
diff changeset
   574
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   575
qed "zdiff_zdiff_eq2";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   576
691c70898518 new files in Integ
paulson
parents:
diff changeset
   577
Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   578
by (simp_tac (simpset() addsimps zadd_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   579
qed "zdiff_zless_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   580
691c70898518 new files in Integ
paulson
parents:
diff changeset
   581
Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   582
by (simp_tac (simpset() addsimps zadd_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   583
qed "zless_zdiff_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   584
691c70898518 new files in Integ
paulson
parents:
diff changeset
   585
Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   586
by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   587
qed "zdiff_zle_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   588
691c70898518 new files in Integ
paulson
parents:
diff changeset
   589
Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   590
by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   591
qed "zle_zdiff_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   592
691c70898518 new files in Integ
paulson
parents:
diff changeset
   593
Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   594
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   595
qed "zdiff_eq_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   596
691c70898518 new files in Integ
paulson
parents:
diff changeset
   597
Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   598
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
691c70898518 new files in Integ
paulson
parents:
diff changeset
   599
qed "eq_zdiff_eq";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   600
691c70898518 new files in Integ
paulson
parents:
diff changeset
   601
(*This list of rewrites simplifies (in)equalities by bringing subtractions
691c70898518 new files in Integ
paulson
parents:
diff changeset
   602
  to the top and then moving negative terms to the other side.  
691c70898518 new files in Integ
paulson
parents:
diff changeset
   603
  Use with zadd_ac*)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   604
val zcompare_rls = 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   605
    [symmetric zdiff_def,
691c70898518 new files in Integ
paulson
parents:
diff changeset
   606
     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   607
     zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 
691c70898518 new files in Integ
paulson
parents:
diff changeset
   608
     zdiff_eq_eq, eq_zdiff_eq];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   609
691c70898518 new files in Integ
paulson
parents:
diff changeset
   610
691c70898518 new files in Integ
paulson
parents:
diff changeset
   611
(** Cancellation laws **)
691c70898518 new files in Integ
paulson
parents:
diff changeset
   612
691c70898518 new files in Integ
paulson
parents:
diff changeset
   613
Goal "!!w::int. (z + w' = z + w) = (w' = w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   614
by Safe_tac;
691c70898518 new files in Integ
paulson
parents:
diff changeset
   615
by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   616
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   617
qed "zadd_left_cancel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   618
691c70898518 new files in Integ
paulson
parents:
diff changeset
   619
Addsimps [zadd_left_cancel];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   620
691c70898518 new files in Integ
paulson
parents:
diff changeset
   621
Goal "!!z::int. (w' + z = w + z) = (w' = w)";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   622
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
691c70898518 new files in Integ
paulson
parents:
diff changeset
   623
qed "zadd_right_cancel";
691c70898518 new files in Integ
paulson
parents:
diff changeset
   624
691c70898518 new files in Integ
paulson
parents:
diff changeset
   625
Addsimps [zadd_right_cancel];
691c70898518 new files in Integ
paulson
parents:
diff changeset
   626
691c70898518 new files in Integ
paulson
parents:
diff changeset
   627
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   628
(** For the cancellation simproc.
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   629
    The idea is to cancel like terms on opposite sides by subtraction **)
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   630
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   631
Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   632
by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   633
qed "zless_eqI";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   634
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   635
Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   636
by (dtac zless_eqI 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   637
by (asm_simp_tac (simpset() addsimps [zle_def]) 1);
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   638
qed "zle_eqI";
5508
691c70898518 new files in Integ
paulson
parents:
diff changeset
   639
5594
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   640
Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')";
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   641
by Safe_tac;
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   642
by (ALLGOALS
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   643
    (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq, zdiff_eq_eq])));
e4439230af67 much tidying
paulson
parents: 5582
diff changeset
   644
qed "zeq_eqI";
5582
a356fb49e69e many renamings and changes. Simproc for cancelling common terms in relations
paulson
parents: 5562
diff changeset
   645