src/HOL/Integ/Integ.ML
author paulson
Thu Aug 06 15:48:13 1998 +0200 (1998-08-06)
changeset 5278 a903b66822e2
parent 5184 9b8547a9496a
child 5316 7a8975451a89
permissions -rw-r--r--
even more tidying of Goal commands
clasohm@1465
     1
(*  Title:      Integ.ML
clasohm@925
     2
    ID:         $Id$
paulson@2215
     3
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@925
     4
    Copyright   1993  University of Cambridge
clasohm@925
     5
clasohm@925
     6
The integers as equivalence classes over nat*nat.
clasohm@925
     7
clasohm@925
     8
Could also prove...
clasohm@925
     9
"znegative(z) ==> $# zmagnitude(z) = $~ z"
clasohm@925
    10
"~ znegative(z) ==> $# zmagnitude(z) = z"
clasohm@925
    11
< is a linear ordering
clasohm@925
    12
+ and * are monotonic wrt <
clasohm@925
    13
*)
clasohm@925
    14
clasohm@925
    15
open Integ;
clasohm@925
    16
berghofe@1894
    17
Delrules [equalityI];
berghofe@1894
    18
clasohm@925
    19
clasohm@925
    20
(*** Proving that intrel is an equivalence relation ***)
clasohm@925
    21
clasohm@925
    22
val eqa::eqb::prems = goal Arith.thy 
clasohm@925
    23
    "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
clasohm@925
    24
\       x1 + y3 = x3 + y1";
paulson@4473
    25
by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
clasohm@925
    26
by (rtac (add_left_commute RS trans) 1);
paulson@2036
    27
by (stac eqb 1);
clasohm@925
    28
by (rtac (add_left_commute RS trans) 1);
paulson@2036
    29
by (stac eqa 1);
clasohm@925
    30
by (rtac (add_left_commute) 1);
clasohm@925
    31
qed "integ_trans_lemma";
clasohm@925
    32
clasohm@925
    33
(** Natural deduction for intrel **)
clasohm@925
    34
clasohm@925
    35
val prems = goalw Integ.thy [intrel_def]
clasohm@925
    36
    "[| x1+y2 = x2+y1|] ==> \
clasohm@972
    37
\    ((x1,y1),(x2,y2)): intrel";
wenzelm@4089
    38
by (fast_tac (claset() addIs prems) 1);
clasohm@925
    39
qed "intrelI";
clasohm@925
    40
clasohm@925
    41
(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
wenzelm@5069
    42
Goalw [intrel_def]
clasohm@925
    43
  "p: intrel --> (EX x1 y1 x2 y2. \
clasohm@972
    44
\                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
berghofe@1894
    45
by (Fast_tac 1);
clasohm@925
    46
qed "intrelE_lemma";
clasohm@925
    47
clasohm@925
    48
val [major,minor] = goal Integ.thy
clasohm@925
    49
  "[| p: intrel;  \
clasohm@972
    50
\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
clasohm@925
    51
\  ==> Q";
clasohm@925
    52
by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
clasohm@925
    53
by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
clasohm@925
    54
qed "intrelE";
clasohm@925
    55
berghofe@1894
    56
AddSIs [intrelI];
berghofe@1894
    57
AddSEs [intrelE];
clasohm@925
    58
wenzelm@5069
    59
Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
berghofe@1894
    60
by (Fast_tac 1);
clasohm@925
    61
qed "intrel_iff";
clasohm@925
    62
wenzelm@5069
    63
Goal "(x,x): intrel";
paulson@2036
    64
by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
clasohm@925
    65
qed "intrel_refl";
clasohm@925
    66
wenzelm@5069
    67
Goalw [equiv_def, refl_def, sym_def, trans_def]
clasohm@925
    68
    "equiv {x::(nat*nat).True} intrel";
wenzelm@4089
    69
by (fast_tac (claset() addSIs [intrel_refl] 
clasohm@925
    70
                        addSEs [sym, integ_trans_lemma]) 1);
clasohm@925
    71
qed "equiv_intrel";
clasohm@925
    72
clasohm@925
    73
val equiv_intrel_iff =
clasohm@925
    74
    [TrueI, TrueI] MRS 
clasohm@925
    75
    ([CollectI, CollectI] MRS 
clasohm@925
    76
    (equiv_intrel RS eq_equiv_class_iff));
clasohm@925
    77
wenzelm@5069
    78
Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
berghofe@1894
    79
by (Fast_tac 1);
clasohm@925
    80
qed "intrel_in_integ";
clasohm@925
    81
wenzelm@5069
    82
Goal "inj_on Abs_Integ Integ";
nipkow@4831
    83
by (rtac inj_on_inverseI 1);
clasohm@925
    84
by (etac Abs_Integ_inverse 1);
nipkow@4831
    85
qed "inj_on_Abs_Integ";
clasohm@925
    86
nipkow@4831
    87
Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
clasohm@1465
    88
          intrel_iff, intrel_in_integ, Abs_Integ_inverse];
clasohm@925
    89
wenzelm@5069
    90
Goal "inj(Rep_Integ)";
clasohm@925
    91
by (rtac inj_inverseI 1);
clasohm@925
    92
by (rtac Rep_Integ_inverse 1);
clasohm@925
    93
qed "inj_Rep_Integ";
clasohm@925
    94
clasohm@925
    95
clasohm@925
    96
clasohm@925
    97
clasohm@925
    98
(** znat: the injection from nat to Integ **)
clasohm@925
    99
wenzelm@5069
   100
Goal "inj(znat)";
clasohm@925
   101
by (rtac injI 1);
clasohm@925
   102
by (rewtac znat_def);
nipkow@4831
   103
by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
clasohm@925
   104
by (REPEAT (rtac intrel_in_integ 1));
clasohm@925
   105
by (dtac eq_equiv_class 1);
clasohm@925
   106
by (rtac equiv_intrel 1);
berghofe@1894
   107
by (Fast_tac 1);
paulson@4162
   108
by Safe_tac;
clasohm@1266
   109
by (Asm_full_simp_tac 1);
clasohm@925
   110
qed "inj_znat";
clasohm@925
   111
clasohm@925
   112
clasohm@925
   113
(**** zminus: unary negation on Integ ****)
clasohm@925
   114
wenzelm@5069
   115
Goalw [congruent_def]
clasohm@972
   116
  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
paulson@4162
   117
by Safe_tac;
wenzelm@4089
   118
by (asm_simp_tac (simpset() addsimps add_ac) 1);
clasohm@925
   119
qed "zminus_congruent";
clasohm@925
   120
clasohm@925
   121
clasohm@925
   122
(*Resolve th against the corresponding facts for zminus*)
clasohm@925
   123
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
clasohm@925
   124
wenzelm@5069
   125
Goalw [zminus_def]
clasohm@972
   126
      "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
clasohm@925
   127
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
wenzelm@4089
   128
by (simp_tac (simpset() addsimps 
clasohm@925
   129
   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
clasohm@925
   130
qed "zminus";
clasohm@925
   131
clasohm@925
   132
(*by lcp*)
clasohm@925
   133
val [prem] = goal Integ.thy
clasohm@972
   134
    "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
clasohm@925
   135
by (res_inst_tac [("x1","z")] 
clasohm@925
   136
    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
clasohm@925
   137
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
clasohm@925
   138
by (res_inst_tac [("p","x")] PairE 1);
clasohm@925
   139
by (rtac prem 1);
wenzelm@4089
   140
by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
clasohm@925
   141
qed "eq_Abs_Integ";
clasohm@925
   142
wenzelm@5069
   143
Goal "$~ ($~ z) = z";
clasohm@925
   144
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
wenzelm@4089
   145
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
clasohm@925
   146
qed "zminus_zminus";
clasohm@925
   147
wenzelm@5069
   148
Goal "inj(zminus)";
clasohm@925
   149
by (rtac injI 1);
clasohm@925
   150
by (dres_inst_tac [("f","zminus")] arg_cong 1);
wenzelm@4089
   151
by (asm_full_simp_tac (simpset() addsimps [zminus_zminus]) 1);
clasohm@925
   152
qed "inj_zminus";
clasohm@925
   153
wenzelm@5069
   154
Goalw [znat_def] "$~ ($#0) = $#0";
wenzelm@4089
   155
by (simp_tac (simpset() addsimps [zminus]) 1);
clasohm@925
   156
qed "zminus_0";
clasohm@925
   157
clasohm@925
   158
clasohm@925
   159
(**** znegative: the test for negative integers ****)
clasohm@925
   160
clasohm@925
   161
wenzelm@5069
   162
Goalw [znegative_def, znat_def]
clasohm@925
   163
    "~ znegative($# n)";
clasohm@1266
   164
by (Simp_tac 1);
paulson@4162
   165
by Safe_tac;
clasohm@925
   166
qed "not_znegative_znat";
clasohm@925
   167
wenzelm@5069
   168
Goalw [znegative_def, znat_def] "znegative($~ $# Suc(n))";
wenzelm@4089
   169
by (simp_tac (simpset() addsimps [zminus]) 1);
clasohm@925
   170
qed "znegative_zminus_znat";
clasohm@925
   171
clasohm@925
   172
clasohm@925
   173
(**** zmagnitude: magnitide of an integer, as a natural number ****)
clasohm@925
   174
clasohm@925
   175
goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
berghofe@5184
   176
by (induct_tac "n" 1);
clasohm@1266
   177
by (ALLGOALS Asm_simp_tac);
clasohm@925
   178
qed "diff_Suc_add_0";
clasohm@925
   179
clasohm@925
   180
goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
berghofe@5184
   181
by (induct_tac "n" 1);
clasohm@1266
   182
by (ALLGOALS Asm_simp_tac);
clasohm@925
   183
qed "diff_Suc_add_inverse";
clasohm@925
   184
wenzelm@5069
   185
Goalw [congruent_def]
clasohm@972
   186
    "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
paulson@4162
   187
by Safe_tac;
clasohm@1266
   188
by (Asm_simp_tac 1);
clasohm@925
   189
by (etac rev_mp 1);
clasohm@925
   190
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
wenzelm@4089
   191
by (asm_simp_tac (simpset() addsimps [inj_Suc RS inj_eq]) 3);
wenzelm@4089
   192
by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 2);
clasohm@1266
   193
by (Asm_simp_tac 1);
clasohm@925
   194
by (rtac impI 1);
clasohm@925
   195
by (etac subst 1);
clasohm@925
   196
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
wenzelm@4089
   197
by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 1);
clasohm@925
   198
qed "zmagnitude_congruent";
clasohm@925
   199
clasohm@925
   200
(*Resolve th against the corresponding facts for zmagnitude*)
clasohm@925
   201
val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
clasohm@925
   202
clasohm@925
   203
wenzelm@5069
   204
Goalw [zmagnitude_def]
clasohm@972
   205
    "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
clasohm@972
   206
\    Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
clasohm@925
   207
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
wenzelm@4089
   208
by (asm_simp_tac (simpset() addsimps [zmagnitude_ize UN_equiv_class]) 1);
clasohm@925
   209
qed "zmagnitude";
clasohm@925
   210
wenzelm@5069
   211
Goalw [znat_def] "zmagnitude($# n) = $#n";
wenzelm@4089
   212
by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1);
clasohm@925
   213
qed "zmagnitude_znat";
clasohm@925
   214
wenzelm@5069
   215
Goalw [znat_def] "zmagnitude($~ $# n) = $#n";
wenzelm@4089
   216
by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1);
clasohm@925
   217
qed "zmagnitude_zminus_znat";
clasohm@925
   218
clasohm@925
   219
clasohm@925
   220
(**** zadd: addition on Integ ****)
clasohm@925
   221
clasohm@925
   222
(** Congruence property for addition **)
clasohm@925
   223
wenzelm@5069
   224
Goalw [congruent2_def]
clasohm@925
   225
    "congruent2 intrel (%p1 p2.                  \
clasohm@972
   226
\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
clasohm@925
   227
(*Proof via congruent2_commuteI seems longer*)
paulson@4162
   228
by Safe_tac;
wenzelm@4089
   229
by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
clasohm@925
   230
(*The rest should be trivial, but rearranging terms is hard*)
clasohm@925
   231
by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
wenzelm@4089
   232
by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
clasohm@925
   233
qed "zadd_congruent2";
clasohm@925
   234
clasohm@925
   235
(*Resolve th against the corresponding facts for zadd*)
clasohm@925
   236
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
clasohm@925
   237
wenzelm@5069
   238
Goalw [zadd_def]
clasohm@972
   239
  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
clasohm@972
   240
\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
clasohm@925
   241
by (asm_simp_tac
wenzelm@4089
   242
    (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
clasohm@925
   243
qed "zadd";
clasohm@925
   244
wenzelm@5069
   245
Goalw [znat_def] "$#0 + z = z";
clasohm@925
   246
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
wenzelm@4089
   247
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
clasohm@925
   248
qed "zadd_0";
clasohm@925
   249
wenzelm@5069
   250
Goal "$~ (z + w) = $~ z + $~ w";
clasohm@925
   251
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   252
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   253
by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
clasohm@925
   254
qed "zminus_zadd_distrib";
clasohm@925
   255
wenzelm@5069
   256
Goal "(z::int) + w = w + z";
clasohm@925
   257
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   258
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   259
by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1);
clasohm@925
   260
qed "zadd_commute";
clasohm@925
   261
wenzelm@5069
   262
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
clasohm@925
   263
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   264
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   265
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
wenzelm@4089
   266
by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
clasohm@925
   267
qed "zadd_assoc";
clasohm@925
   268
clasohm@925
   269
(*For AC rewriting*)
wenzelm@5069
   270
Goal "(x::int)+(y+z)=y+(x+z)";
clasohm@925
   271
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   272
by (rtac (zadd_assoc RS trans) 1);
clasohm@925
   273
by (rtac (zadd_commute RS arg_cong) 1);
clasohm@925
   274
qed "zadd_left_commute";
clasohm@925
   275
clasohm@925
   276
(*Integer addition is an AC operator*)
clasohm@925
   277
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
clasohm@925
   278
wenzelm@5069
   279
Goalw [znat_def] "$# (m + n) = ($#m) + ($#n)";
wenzelm@4089
   280
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
clasohm@925
   281
qed "znat_add";
clasohm@925
   282
wenzelm@5069
   283
Goalw [znat_def] "z + ($~ z) = $#0";
clasohm@925
   284
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
wenzelm@4089
   285
by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
clasohm@925
   286
qed "zadd_zminus_inverse";
clasohm@925
   287
wenzelm@5069
   288
Goal "($~ z) + z = $#0";
clasohm@925
   289
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   290
by (rtac zadd_zminus_inverse 1);
clasohm@925
   291
qed "zadd_zminus_inverse2";
clasohm@925
   292
wenzelm@5069
   293
Goal "z + $#0 = z";
clasohm@925
   294
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   295
by (rtac zadd_0 1);
clasohm@925
   296
qed "zadd_0_right";
clasohm@925
   297
clasohm@925
   298
paulson@2224
   299
(** Lemmas **)
paulson@2224
   300
paulson@2224
   301
qed_goal "zadd_assoc_cong" Integ.thy
paulson@2224
   302
    "!!z. (z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
wenzelm@4089
   303
 (fn _ => [(asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1)]);
paulson@2224
   304
paulson@2224
   305
qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
paulson@2224
   306
 (fn _ => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
paulson@2224
   307
paulson@2224
   308
clasohm@925
   309
(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
clasohm@925
   310
clasohm@925
   311
(**** zmult: multiplication on Integ ****)
clasohm@925
   312
clasohm@925
   313
(** Congruence property for multiplication **)
clasohm@925
   314
wenzelm@5069
   315
Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
wenzelm@4089
   316
by (simp_tac (simpset() addsimps add_ac) 1);
clasohm@925
   317
qed "zmult_congruent_lemma";
clasohm@925
   318
paulson@5278
   319
Goal "congruent2 intrel (%p1 p2.                 \
clasohm@1465
   320
\               split (%x1 y1. split (%x2 y2.   \
clasohm@972
   321
\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
clasohm@925
   322
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
oheimb@4817
   323
 by (pair_tac "w" 2);
oheimb@4817
   324
 by (rename_tac "z1 z2" 2);
oheimb@4772
   325
 by Safe_tac;
oheimb@4772
   326
 by (rewtac split_def);
oheimb@4772
   327
 by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
wenzelm@4089
   328
by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
clasohm@1266
   329
                           addsimps add_ac@mult_ac) 1);
clasohm@925
   330
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
clasohm@925
   331
by (rtac (zmult_congruent_lemma RS trans) 1);
clasohm@925
   332
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
clasohm@925
   333
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
clasohm@925
   334
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
wenzelm@4089
   335
by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1);
wenzelm@4089
   336
by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
clasohm@925
   337
qed "zmult_congruent2";
clasohm@925
   338
clasohm@925
   339
(*Resolve th against the corresponding facts for zmult*)
clasohm@925
   340
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
clasohm@925
   341
wenzelm@5069
   342
Goalw [zmult_def]
clasohm@1465
   343
   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
clasohm@972
   344
\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
wenzelm@4089
   345
by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
clasohm@925
   346
qed "zmult";
clasohm@925
   347
wenzelm@5069
   348
Goalw [znat_def] "$#0 * z = $#0";
clasohm@925
   349
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
wenzelm@4089
   350
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
clasohm@925
   351
qed "zmult_0";
clasohm@925
   352
wenzelm@5069
   353
Goalw [znat_def] "$#Suc(0) * z = z";
clasohm@925
   354
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
wenzelm@4089
   355
by (asm_simp_tac (simpset() addsimps [zmult]) 1);
clasohm@925
   356
qed "zmult_1";
clasohm@925
   357
wenzelm@5069
   358
Goal "($~ z) * w = $~ (z * w)";
clasohm@925
   359
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   360
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   361
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
clasohm@925
   362
qed "zmult_zminus";
clasohm@925
   363
clasohm@925
   364
wenzelm@5069
   365
Goal "($~ z) * ($~ w) = (z * w)";
clasohm@925
   366
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   367
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   368
by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
clasohm@925
   369
qed "zmult_zminus_zminus";
clasohm@925
   370
wenzelm@5069
   371
Goal "(z::int) * w = w * z";
clasohm@925
   372
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   373
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   374
by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1);
clasohm@925
   375
qed "zmult_commute";
clasohm@925
   376
wenzelm@5069
   377
Goal "z * $# 0 = $#0";
clasohm@925
   378
by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
clasohm@925
   379
qed "zmult_0_right";
clasohm@925
   380
wenzelm@5069
   381
Goal "z * $#Suc(0) = z";
clasohm@925
   382
by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
clasohm@925
   383
qed "zmult_1_right";
clasohm@925
   384
wenzelm@5069
   385
Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
clasohm@925
   386
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   387
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   388
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
wenzelm@4089
   389
by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ 
paulson@2036
   390
                                     add_ac @ mult_ac)) 1);
clasohm@925
   391
qed "zmult_assoc";
clasohm@925
   392
clasohm@925
   393
(*For AC rewriting*)
clasohm@925
   394
qed_goal "zmult_left_commute" Integ.thy
clasohm@925
   395
    "(z1::int)*(z2*z3) = z2*(z1*z3)"
clasohm@925
   396
 (fn _ => [rtac (zmult_commute RS trans) 1, rtac (zmult_assoc RS trans) 1,
clasohm@925
   397
           rtac (zmult_commute RS arg_cong) 1]);
clasohm@925
   398
clasohm@925
   399
(*Integer multiplication is an AC operator*)
clasohm@925
   400
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
clasohm@925
   401
wenzelm@5069
   402
Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
clasohm@925
   403
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   404
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   405
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   406
by (asm_simp_tac 
wenzelm@4089
   407
    (simpset() addsimps ([add_mult_distrib2, zadd, zmult] @ 
paulson@2036
   408
                        add_ac @ mult_ac)) 1);
clasohm@925
   409
qed "zadd_zmult_distrib";
clasohm@925
   410
clasohm@925
   411
val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
clasohm@925
   412
wenzelm@5069
   413
Goal "w * ($~ z) = $~ (w * z)";
wenzelm@4089
   414
by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
clasohm@925
   415
qed "zmult_zminus_right";
clasohm@925
   416
wenzelm@5069
   417
Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
wenzelm@4089
   418
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
clasohm@925
   419
qed "zadd_zmult_distrib2";
clasohm@925
   420
clasohm@925
   421
val zadd_simps = 
clasohm@925
   422
    [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
clasohm@925
   423
clasohm@925
   424
val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib];
clasohm@925
   425
clasohm@925
   426
val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, 
clasohm@1465
   427
                   zmult_zminus, zmult_zminus_right];
clasohm@925
   428
clasohm@1266
   429
Addsimps (zadd_simps @ zminus_simps @ zmult_simps @ 
clasohm@1266
   430
          [zmagnitude_znat, zmagnitude_zminus_znat]);
clasohm@925
   431
clasohm@925
   432
clasohm@925
   433
(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****)
clasohm@925
   434
clasohm@925
   435
(* Some Theorems about zsuc and zpred *)
wenzelm@5069
   436
Goalw [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
wenzelm@4089
   437
by (simp_tac (simpset() addsimps [znat_add RS sym]) 1);
clasohm@925
   438
qed "znat_Suc";
clasohm@925
   439
wenzelm@5069
   440
Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
clasohm@1266
   441
by (Simp_tac 1);
clasohm@925
   442
qed "zminus_zsuc";
clasohm@925
   443
wenzelm@5069
   444
Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
clasohm@1266
   445
by (Simp_tac 1);
clasohm@925
   446
qed "zminus_zpred";
clasohm@925
   447
wenzelm@5069
   448
Goalw [zsuc_def,zpred_def,zdiff_def]
clasohm@925
   449
   "zpred(zsuc(z)) = z";
wenzelm@4089
   450
by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
clasohm@925
   451
qed "zpred_zsuc";
clasohm@925
   452
wenzelm@5069
   453
Goalw [zsuc_def,zpred_def,zdiff_def]
clasohm@925
   454
   "zsuc(zpred(z)) = z";
wenzelm@4089
   455
by (simp_tac (simpset() addsimps [zadd_assoc]) 1);
clasohm@925
   456
qed "zsuc_zpred";
clasohm@925
   457
wenzelm@5069
   458
Goal "(zpred(z)=w) = (z=zsuc(w))";
paulson@4162
   459
by Safe_tac;
clasohm@925
   460
by (rtac (zsuc_zpred RS sym) 1);
clasohm@925
   461
by (rtac zpred_zsuc 1);
clasohm@925
   462
qed "zpred_to_zsuc";
clasohm@925
   463
wenzelm@5069
   464
Goal "(zsuc(z)=w)=(z=zpred(w))";
paulson@4162
   465
by Safe_tac;
clasohm@925
   466
by (rtac (zpred_zsuc RS sym) 1);
clasohm@925
   467
by (rtac zsuc_zpred 1);
clasohm@925
   468
qed "zsuc_to_zpred";
clasohm@925
   469
wenzelm@5069
   470
Goal "($~ z = w) = (z = $~ w)";
paulson@4162
   471
by Safe_tac;
clasohm@925
   472
by (rtac (zminus_zminus RS sym) 1);
clasohm@925
   473
by (rtac zminus_zminus 1);
clasohm@925
   474
qed "zminus_exchange";
clasohm@925
   475
wenzelm@5069
   476
Goal"(zsuc(z)=zsuc(w)) = (z=w)";
paulson@4162
   477
by Safe_tac;
clasohm@925
   478
by (dres_inst_tac [("f","zpred")] arg_cong 1);
wenzelm@4089
   479
by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1);
clasohm@925
   480
qed "bijective_zsuc";
clasohm@925
   481
wenzelm@5069
   482
Goal"(zpred(z)=zpred(w)) = (z=w)";
paulson@4162
   483
by Safe_tac;
clasohm@925
   484
by (dres_inst_tac [("f","zsuc")] arg_cong 1);
wenzelm@4089
   485
by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1);
clasohm@925
   486
qed "bijective_zpred";
clasohm@925
   487
clasohm@925
   488
(* Additional Theorems about zadd *)
clasohm@925
   489
wenzelm@5069
   490
Goalw [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
wenzelm@4089
   491
by (simp_tac (simpset() addsimps zadd_ac) 1);
clasohm@925
   492
qed "zadd_zsuc";
clasohm@925
   493
wenzelm@5069
   494
Goalw [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
wenzelm@4089
   495
by (simp_tac (simpset() addsimps zadd_ac) 1);
clasohm@925
   496
qed "zadd_zsuc_right";
clasohm@925
   497
wenzelm@5069
   498
Goalw [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
wenzelm@4089
   499
by (simp_tac (simpset() addsimps zadd_ac) 1);
clasohm@925
   500
qed "zadd_zpred";
clasohm@925
   501
wenzelm@5069
   502
Goalw [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
wenzelm@4089
   503
by (simp_tac (simpset() addsimps zadd_ac) 1);
clasohm@925
   504
qed "zadd_zpred_right";
clasohm@925
   505
clasohm@925
   506
clasohm@925
   507
(* Additional Theorems about zmult *)
clasohm@925
   508
wenzelm@5069
   509
Goalw [zsuc_def] "zsuc(w) * z = z + w * z";
wenzelm@4089
   510
by (simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_commute]) 1);
clasohm@925
   511
qed "zmult_zsuc";
clasohm@925
   512
wenzelm@5069
   513
Goalw [zsuc_def] "z * zsuc(w) = z + w * z";
clasohm@925
   514
by (simp_tac 
wenzelm@4089
   515
    (simpset() addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1);
clasohm@925
   516
qed "zmult_zsuc_right";
clasohm@925
   517
wenzelm@5069
   518
Goalw [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
wenzelm@4089
   519
by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
clasohm@925
   520
qed "zmult_zpred";
clasohm@925
   521
wenzelm@5069
   522
Goalw [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
wenzelm@4089
   523
by (simp_tac (simpset() addsimps [zadd_zmult_distrib2, zmult_commute]) 1);
clasohm@925
   524
qed "zmult_zpred_right";
clasohm@925
   525
clasohm@925
   526
(* Further Theorems about zsuc and zpred *)
wenzelm@5069
   527
Goal "$#Suc(m) ~= $#0";
wenzelm@4089
   528
by (simp_tac (simpset() addsimps [inj_znat RS inj_eq]) 1);
clasohm@925
   529
qed "znat_Suc_not_znat_Zero";
clasohm@925
   530
clasohm@925
   531
bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym));
clasohm@925
   532
clasohm@925
   533
wenzelm@5069
   534
Goalw [zsuc_def,znat_def] "w ~= zsuc(w)";
clasohm@925
   535
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
wenzelm@4089
   536
by (asm_full_simp_tac (simpset() addsimps [zadd]) 1);
clasohm@925
   537
qed "n_not_zsuc_n";
clasohm@925
   538
clasohm@925
   539
val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
clasohm@925
   540
wenzelm@5069
   541
Goal "w ~= zpred(w)";
paulson@4162
   542
by Safe_tac;
clasohm@925
   543
by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
wenzelm@4089
   544
by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
clasohm@925
   545
qed "n_not_zpred_n";
clasohm@925
   546
clasohm@925
   547
val zpred_n_not_n = n_not_zpred_n RS not_sym;
clasohm@925
   548
clasohm@925
   549
clasohm@925
   550
(* Theorems about less and less_equal *)
clasohm@925
   551
wenzelm@5069
   552
Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
paulson@5148
   553
    "w<z ==> ? n. z = w + $#(Suc(n))";
clasohm@925
   554
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   555
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
paulson@4162
   556
by Safe_tac;
wenzelm@4089
   557
by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
wenzelm@4089
   558
by (safe_tac (claset() addSDs [less_eq_Suc_add]));
clasohm@925
   559
by (res_inst_tac [("x","k")] exI 1);
paulson@4676
   560
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
clasohm@925
   561
qed "zless_eq_zadd_Suc";
clasohm@925
   562
wenzelm@5069
   563
Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
clasohm@925
   564
    "z < z + $#(Suc(n))";
clasohm@925
   565
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
paulson@4676
   566
by (Clarify_tac 1);
wenzelm@4089
   567
by (simp_tac (simpset() addsimps [zadd, zminus]) 1);
clasohm@925
   568
qed "zless_zadd_Suc";
clasohm@925
   569
paulson@5143
   570
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
wenzelm@4089
   571
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
clasohm@925
   572
by (simp_tac 
wenzelm@4089
   573
    (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
clasohm@925
   574
qed "zless_trans";
clasohm@925
   575
wenzelm@5069
   576
Goalw [zsuc_def] "z<zsuc(z)";
clasohm@925
   577
by (rtac zless_zadd_Suc 1);
clasohm@925
   578
qed "zlessI";
clasohm@925
   579
clasohm@925
   580
val zless_zsucI = zlessI RSN (2,zless_trans);
clasohm@925
   581
wenzelm@5069
   582
Goal "!!z w::int. z<w ==> ~w<z";
wenzelm@4089
   583
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
clasohm@925
   584
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
paulson@4162
   585
by Safe_tac;
wenzelm@4089
   586
by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
clasohm@925
   587
qed "zless_not_sym";
clasohm@925
   588
clasohm@925
   589
(* [| n<m; m<n |] ==> R *)
clasohm@925
   590
bind_thm ("zless_asym", (zless_not_sym RS notE));
clasohm@925
   591
wenzelm@5069
   592
Goal "!!z::int. ~ z<z";
clasohm@925
   593
by (resolve_tac [zless_asym RS notI] 1);
clasohm@925
   594
by (REPEAT (assume_tac 1));
clasohm@925
   595
qed "zless_not_refl";
clasohm@925
   596
clasohm@925
   597
(* z<z ==> R *)
paulson@1619
   598
bind_thm ("zless_irrefl", (zless_not_refl RS notE));
clasohm@925
   599
paulson@5143
   600
Goal "z<w ==> w ~= (z::int)";
wenzelm@4089
   601
by (fast_tac (claset() addEs [zless_irrefl]) 1);
clasohm@925
   602
qed "zless_not_refl2";
clasohm@925
   603
clasohm@925
   604
clasohm@925
   605
(*"Less than" is a linear ordering*)
wenzelm@5069
   606
Goalw [zless_def, znegative_def, zdiff_def] 
clasohm@925
   607
    "z<w | z=w | w<(z::int)";
clasohm@925
   608
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   609
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
paulson@4162
   610
by Safe_tac;
clasohm@925
   611
by (asm_full_simp_tac
wenzelm@4089
   612
    (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
clasohm@925
   613
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
wenzelm@4089
   614
by (REPEAT (fast_tac (claset() addss (simpset() addsimps add_ac)) 1));
clasohm@925
   615
qed "zless_linear";
clasohm@925
   616
clasohm@925
   617
clasohm@925
   618
(*** Properties of <= ***)
clasohm@925
   619
wenzelm@5069
   620
Goalw  [zless_def, znegative_def, zdiff_def, znat_def]
clasohm@925
   621
    "($#m < $#n) = (m<n)";
clasohm@925
   622
by (simp_tac
wenzelm@4089
   623
    (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
wenzelm@4089
   624
by (fast_tac (claset() addIs [add_commute] addSEs [less_add_eq_less]) 1);
clasohm@925
   625
qed "zless_eq_less";
clasohm@925
   626
wenzelm@5069
   627
Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
wenzelm@4089
   628
by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
clasohm@925
   629
qed "zle_eq_le";
clasohm@925
   630
paulson@5143
   631
Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
clasohm@925
   632
by (assume_tac 1);
clasohm@925
   633
qed "zleI";
clasohm@925
   634
paulson@5143
   635
Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
clasohm@925
   636
by (assume_tac 1);
clasohm@925
   637
qed "zleD";
clasohm@925
   638
clasohm@925
   639
val zleE = make_elim zleD;
clasohm@925
   640
paulson@5143
   641
Goalw [zle_def] "~ z <= w ==> w<(z::int)";
berghofe@1894
   642
by (Fast_tac 1);
clasohm@925
   643
qed "not_zleE";
clasohm@925
   644
paulson@5143
   645
Goalw [zle_def] "z < w ==> z <= (w::int)";
wenzelm@4089
   646
by (fast_tac (claset() addEs [zless_asym]) 1);
clasohm@925
   647
qed "zless_imp_zle";
clasohm@925
   648
paulson@5143
   649
Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
clasohm@925
   650
by (cut_facts_tac [zless_linear] 1);
wenzelm@4089
   651
by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
clasohm@925
   652
qed "zle_imp_zless_or_eq";
clasohm@925
   653
paulson@5143
   654
Goalw [zle_def] "z<w | z=w ==> z <=(w::int)";
clasohm@925
   655
by (cut_facts_tac [zless_linear] 1);
wenzelm@4089
   656
by (fast_tac (claset() addEs [zless_irrefl,zless_asym]) 1);
clasohm@925
   657
qed "zless_or_eq_imp_zle";
clasohm@925
   658
wenzelm@5069
   659
Goal "(x <= (y::int)) = (x < y | x=y)";
clasohm@925
   660
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
clasohm@925
   661
qed "zle_eq_zless_or_eq";
clasohm@925
   662
wenzelm@5069
   663
Goal "w <= (w::int)";
wenzelm@4089
   664
by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
clasohm@925
   665
qed "zle_refl";
clasohm@925
   666
clasohm@925
   667
val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
clasohm@925
   668
by (dtac zle_imp_zless_or_eq 1);
wenzelm@4089
   669
by (fast_tac (claset() addIs [zless_trans]) 1);
clasohm@925
   670
qed "zle_zless_trans";
clasohm@925
   671
paulson@5143
   672
Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
clasohm@925
   673
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
wenzelm@4089
   674
            rtac zless_or_eq_imp_zle, fast_tac (claset() addIs [zless_trans])]);
clasohm@925
   675
qed "zle_trans";
clasohm@925
   676
paulson@5143
   677
Goal "[| z <= w; w <= z |] ==> z = (w::int)";
clasohm@925
   678
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
wenzelm@4089
   679
            fast_tac (claset() addEs [zless_irrefl,zless_asym])]);
clasohm@925
   680
qed "zle_anti_sym";
clasohm@925
   681
clasohm@925
   682
wenzelm@5069
   683
Goal "!!w w' z::int. z + w' = z + w ==> w' = w";
clasohm@925
   684
by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
wenzelm@4089
   685
by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
clasohm@925
   686
qed "zadd_left_cancel";
clasohm@925
   687
clasohm@925
   688
clasohm@925
   689
(*** Monotonicity results ***)
clasohm@925
   690
wenzelm@5069
   691
Goal "!!v w z::int. v < w ==> v + z < w + z";
wenzelm@4089
   692
by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
wenzelm@4089
   693
by (simp_tac (simpset() addsimps zadd_ac) 1);
wenzelm@4089
   694
by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
clasohm@925
   695
qed "zadd_zless_mono1";
clasohm@925
   696
wenzelm@5069
   697
Goal "!!v w z::int. (v+z < w+z) = (v < w)";
wenzelm@4089
   698
by (safe_tac (claset() addSEs [zadd_zless_mono1]));
clasohm@925
   699
by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
wenzelm@4089
   700
by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
clasohm@925
   701
qed "zadd_left_cancel_zless";
clasohm@925
   702
wenzelm@5069
   703
Goal "!!v w z::int. (v+z <= w+z) = (v <= w)";
clasohm@925
   704
by (asm_full_simp_tac
wenzelm@4089
   705
    (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
clasohm@925
   706
qed "zadd_left_cancel_zle";
clasohm@925
   707
clasohm@925
   708
(*"v<=w ==> v+z <= w+z"*)
clasohm@925
   709
bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
clasohm@925
   710
clasohm@925
   711
wenzelm@5069
   712
Goal "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
clasohm@925
   713
by (etac (zadd_zle_mono1 RS zle_trans) 1);
wenzelm@4089
   714
by (simp_tac (simpset() addsimps [zadd_commute]) 1);
clasohm@925
   715
(*w moves to the end because it is free while z', z are bound*)
clasohm@925
   716
by (etac zadd_zle_mono1 1);
clasohm@925
   717
qed "zadd_zle_mono";
clasohm@925
   718
wenzelm@5069
   719
Goal "!!w z::int. z<=$#0 ==> w+z <= w";
clasohm@925
   720
by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
wenzelm@4089
   721
by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1);
clasohm@925
   722
qed "zadd_zle_self";
paulson@2224
   723
paulson@2224
   724
wenzelm@4195
   725
(**** Comparisons: lemmas and proofs by Norbert Voelker ****)
paulson@2224
   726
paulson@2224
   727
(** One auxiliary theorem...**)
paulson@2224
   728
paulson@2224
   729
goal HOL.thy "(x = False) = (~ x)";
paulson@2224
   730
  by (fast_tac HOL_cs 1);
paulson@2224
   731
qed "eq_False_conv";
paulson@2224
   732
paulson@2224
   733
(** Additional theorems for Integ.thy **) 
paulson@2224
   734
paulson@2224
   735
Addsimps [zless_eq_less, zle_eq_le,
paulson@2224
   736
	  znegative_zminus_znat, not_znegative_znat]; 
paulson@2224
   737
paulson@5143
   738
Goal "(x::int) = y ==> x <= y"; 
paulson@2224
   739
  by (etac subst 1); by (rtac zle_refl 1); 
paulson@3725
   740
qed "zequalD1"; 
paulson@2224
   741
wenzelm@5069
   742
Goal "($~ x < $~ y) = (y < x)";
paulson@2224
   743
  by (rewrite_goals_tac [zless_def,zdiff_def]); 
wenzelm@4089
   744
  by (simp_tac (simpset() addsimps zadd_ac ) 1); 
paulson@3725
   745
qed "zminus_zless_zminus"; 
paulson@2224
   746
wenzelm@5069
   747
Goal "($~ x <= $~ y) = (y <= x)";
paulson@2224
   748
  by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); 
paulson@3725
   749
qed "zminus_zle_zminus"; 
paulson@2224
   750
wenzelm@5069
   751
Goal "(x < $~ y) = (y < $~ x)";
paulson@2224
   752
  by (rewrite_goals_tac [zless_def,zdiff_def]); 
wenzelm@4089
   753
  by (simp_tac (simpset() addsimps zadd_ac ) 1); 
paulson@3725
   754
qed "zless_zminus"; 
paulson@2224
   755
wenzelm@5069
   756
Goal "($~ x < y) = ($~ y < x)";
paulson@2224
   757
  by (rewrite_goals_tac [zless_def,zdiff_def]); 
wenzelm@4089
   758
  by (simp_tac (simpset() addsimps zadd_ac ) 1); 
paulson@3725
   759
qed "zminus_zless"; 
paulson@2224
   760
wenzelm@5069
   761
Goal "(x <= $~ y) = (y <=  $~ x)";
paulson@2224
   762
  by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); 
paulson@3725
   763
qed "zle_zminus"; 
paulson@2224
   764
wenzelm@5069
   765
Goal "($~ x <= y) = ($~ y <=  x)";
paulson@2224
   766
  by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); 
paulson@3725
   767
qed "zminus_zle"; 
paulson@2224
   768
wenzelm@5069
   769
Goal " $#0 < $# Suc n"; 
paulson@2224
   770
  by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
paulson@3725
   771
qed "zero_zless_Suc_pos"; 
paulson@2224
   772
wenzelm@5069
   773
Goal "($# n= $# m) = (n = m)"; 
paulson@2224
   774
  by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); 
paulson@3725
   775
qed "znat_znat_eq"; 
paulson@2224
   776
AddIffs[znat_znat_eq]; 
paulson@2224
   777
wenzelm@5069
   778
Goal "$~ $# Suc n < $#0";
paulson@2224
   779
  by (stac (zminus_0 RS sym) 1); 
paulson@2224
   780
  by (rtac (zminus_zless_zminus RS iffD2) 1); 
paulson@2224
   781
  by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); 
paulson@3725
   782
qed "negative_zless_0"; 
paulson@2224
   783
Addsimps [zero_zless_Suc_pos, negative_zless_0]; 
paulson@2224
   784
wenzelm@5069
   785
Goal "$~ $#  n <= $#0";
paulson@2224
   786
  by (rtac zless_or_eq_imp_zle 1); 
berghofe@5184
   787
  by (induct_tac "n" 1); 
paulson@2224
   788
  by (ALLGOALS Asm_simp_tac); 
paulson@3725
   789
qed "negative_zle_0"; 
paulson@2224
   790
Addsimps[negative_zle_0]; 
paulson@2224
   791
wenzelm@5069
   792
Goal "~($#0 <= $~ $# Suc n)";
paulson@2224
   793
  by (stac zle_zminus 1);
paulson@2224
   794
  by (Simp_tac 1);
paulson@3725
   795
qed "not_zle_0_negative"; 
paulson@2224
   796
Addsimps[not_zle_0_negative]; 
paulson@2224
   797
wenzelm@5069
   798
Goal "($# n <= $~ $# m) = (n = 0 & m = 0)"; 
paulson@2224
   799
  by (safe_tac HOL_cs); 
paulson@2224
   800
  by (Simp_tac 3); 
paulson@2224
   801
  by (dtac (zle_zminus RS iffD1) 2); 
paulson@2224
   802
  by (ALLGOALS(dtac (negative_zle_0 RSN(2,zle_trans)))); 
paulson@2224
   803
  by (ALLGOALS Asm_full_simp_tac); 
paulson@3725
   804
qed "znat_zle_znegative"; 
paulson@2224
   805
wenzelm@5069
   806
Goal "~($# n < $~ $# Suc m)";
paulson@2224
   807
  by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); 
paulson@2224
   808
  by (dtac (znat_zle_znegative RS iffD1) 1); 
paulson@2224
   809
  by (safe_tac HOL_cs); 
paulson@2224
   810
  by (dtac (zless_zminus RS iffD1) 1); 
paulson@2224
   811
  by (Asm_full_simp_tac 1);
paulson@3725
   812
qed "not_znat_zless_negative"; 
paulson@2224
   813
wenzelm@5069
   814
Goal "($~ $# n = $# m) = (n = 0 & m = 0)"; 
paulson@2224
   815
  by (rtac iffI 1);
paulson@2224
   816
  by (rtac  (znat_zle_znegative RS iffD1) 1); 
paulson@2224
   817
  by (dtac sym 1); 
paulson@2224
   818
  by (ALLGOALS Asm_simp_tac); 
paulson@3725
   819
qed "negative_eq_positive"; 
paulson@2224
   820
paulson@2224
   821
Addsimps [zminus_zless_zminus, zminus_zle_zminus, 
paulson@2224
   822
	  negative_eq_positive, not_znat_zless_negative]; 
paulson@2224
   823
paulson@5143
   824
Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
paulson@4477
   825
  by Auto_tac; 
paulson@3725
   826
qed "znegative_less_0"; 
paulson@2224
   827
paulson@5143
   828
Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)";
paulson@2224
   829
  by (stac znegative_less_0 1); 
paulson@2224
   830
  by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); 
paulson@3725
   831
qed "not_znegative_ge_0"; 
paulson@2224
   832
paulson@5143
   833
Goal "znegative x ==> ? n. x = $~ $# Suc n"; 
paulson@2224
   834
  by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); 
paulson@2224
   835
  by (etac exE 1); 
paulson@2224
   836
  by (rtac exI 1);
paulson@2224
   837
  by (dres_inst_tac [("f","(% z. z + $~ $# Suc n )")] arg_cong 1); 
wenzelm@4089
   838
  by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); 
paulson@3725
   839
qed "znegativeD"; 
paulson@2224
   840
paulson@5143
   841
Goal "~znegative x ==> ? n. x = $# n"; 
paulson@2224
   842
  by (dtac (not_znegative_ge_0 RS iffD1) 1); 
paulson@2224
   843
  by (dtac zle_imp_zless_or_eq 1); 
paulson@2224
   844
  by (etac disjE 1); 
paulson@2224
   845
  by (dtac zless_eq_zadd_Suc 1); 
paulson@4477
   846
  by Auto_tac; 
paulson@3725
   847
qed "not_znegativeD"; 
paulson@2224
   848
paulson@2224
   849
(* a case theorem distinguishing positive and negative int *)  
paulson@2224
   850
paulson@2224
   851
val prems = goal Integ.thy 
paulson@2224
   852
    "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; 
paulson@2224
   853
  by (cut_inst_tac [("P","znegative z")] excluded_middle 1); 
paulson@2224
   854
  by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1); 
paulson@3725
   855
qed "int_cases"; 
paulson@2224
   856
paulson@2224
   857
fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
paulson@2224
   858