src/HOL/Integ/Integ.ML
author clasohm
Fri Mar 24 12:30:35 1995 +0100 (1995-03-24)
changeset 972 e61b058d58d2
parent 925 15539deb6863
child 1266 3ae9fe3c0f68
permissions -rw-r--r--
changed syntax of tuples from <..., ...> to (..., ...)
clasohm@925
     1
(*  Title: 	Integ.ML
clasohm@925
     2
    ID:         $Id$
clasohm@925
     3
    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
clasohm@925
     4
        	Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@925
     5
    Copyright   1994 Universita' di Firenze
clasohm@925
     6
    Copyright   1993  University of Cambridge
clasohm@925
     7
clasohm@925
     8
The integers as equivalence classes over nat*nat.
clasohm@925
     9
clasohm@925
    10
Could also prove...
clasohm@925
    11
"znegative(z) ==> $# zmagnitude(z) = $~ z"
clasohm@925
    12
"~ znegative(z) ==> $# zmagnitude(z) = z"
clasohm@925
    13
< is a linear ordering
clasohm@925
    14
+ and * are monotonic wrt <
clasohm@925
    15
*)
clasohm@925
    16
clasohm@925
    17
open Integ;
clasohm@925
    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";
clasohm@925
    25
by (res_inst_tac [("k2","x2")] (add_left_cancel RS iffD1) 1);
clasohm@925
    26
by (rtac (add_left_commute RS trans) 1);
clasohm@925
    27
by (rtac (eqb RS ssubst) 1);
clasohm@925
    28
by (rtac (add_left_commute RS trans) 1);
clasohm@925
    29
by (rtac (eqa RS ssubst) 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";
clasohm@925
    38
by (fast_tac (rel_cs 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*)
clasohm@925
    42
goalw Integ.thy [intrel_def]
clasohm@925
    43
  "p: intrel --> (EX x1 y1 x2 y2. \
clasohm@972
    44
\                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
clasohm@925
    45
by (fast_tac rel_cs 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
clasohm@925
    56
val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
clasohm@925
    57
clasohm@972
    58
goal Integ.thy "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
clasohm@925
    59
by (fast_tac intrel_cs 1);
clasohm@925
    60
qed "intrel_iff";
clasohm@925
    61
clasohm@972
    62
goal Integ.thy "(x,x): intrel";
clasohm@925
    63
by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
clasohm@925
    64
qed "intrel_refl";
clasohm@925
    65
clasohm@925
    66
goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
clasohm@925
    67
    "equiv {x::(nat*nat).True} intrel";
clasohm@925
    68
by (fast_tac (intrel_cs addSIs [intrel_refl] 
clasohm@925
    69
                        addSEs [sym, integ_trans_lemma]) 1);
clasohm@925
    70
qed "equiv_intrel";
clasohm@925
    71
clasohm@925
    72
val equiv_intrel_iff =
clasohm@925
    73
    [TrueI, TrueI] MRS 
clasohm@925
    74
    ([CollectI, CollectI] MRS 
clasohm@925
    75
    (equiv_intrel RS eq_equiv_class_iff));
clasohm@925
    76
clasohm@972
    77
goalw Integ.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
clasohm@925
    78
by (fast_tac set_cs 1);
clasohm@925
    79
qed "intrel_in_integ";
clasohm@925
    80
clasohm@925
    81
goal Integ.thy "inj_onto Abs_Integ Integ";
clasohm@925
    82
by (rtac inj_onto_inverseI 1);
clasohm@925
    83
by (etac Abs_Integ_inverse 1);
clasohm@925
    84
qed "inj_onto_Abs_Integ";
clasohm@925
    85
clasohm@925
    86
val intrel_ss = 
clasohm@925
    87
    arith_ss addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff,
clasohm@925
    88
		       intrel_iff, intrel_in_integ, Abs_Integ_inverse];
clasohm@925
    89
clasohm@925
    90
goal Integ.thy "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
clasohm@925
   100
goal Integ.thy "inj(znat)";
clasohm@925
   101
by (rtac injI 1);
clasohm@925
   102
by (rewtac znat_def);
clasohm@925
   103
by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 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);
clasohm@925
   107
by (fast_tac set_cs 1);
clasohm@925
   108
by (safe_tac intrel_cs);
clasohm@925
   109
by (asm_full_simp_tac arith_ss 1);
clasohm@925
   110
qed "inj_znat";
clasohm@925
   111
clasohm@925
   112
clasohm@925
   113
(**** zminus: unary negation on Integ ****)
clasohm@925
   114
clasohm@925
   115
goalw Integ.thy [congruent_def]
clasohm@972
   116
  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
clasohm@925
   117
by (safe_tac intrel_cs);
clasohm@925
   118
by (asm_simp_tac (intrel_ss 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
clasohm@925
   125
goalw Integ.thy [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);
clasohm@925
   128
by (simp_tac (set_ss addsimps 
clasohm@925
   129
   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
clasohm@925
   130
by (rewtac split_def);
clasohm@925
   131
by (simp_tac prod_ss 1);
clasohm@925
   132
qed "zminus";
clasohm@925
   133
clasohm@925
   134
(*by lcp*)
clasohm@925
   135
val [prem] = goal Integ.thy
clasohm@972
   136
    "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
clasohm@925
   137
by (res_inst_tac [("x1","z")] 
clasohm@925
   138
    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
clasohm@925
   139
by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
clasohm@925
   140
by (res_inst_tac [("p","x")] PairE 1);
clasohm@925
   141
by (rtac prem 1);
clasohm@925
   142
by (asm_full_simp_tac (HOL_ss addsimps [Rep_Integ_inverse]) 1);
clasohm@925
   143
qed "eq_Abs_Integ";
clasohm@925
   144
clasohm@925
   145
goal Integ.thy "$~ ($~ z) = z";
clasohm@925
   146
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   147
by (asm_simp_tac (HOL_ss addsimps [zminus]) 1);
clasohm@925
   148
qed "zminus_zminus";
clasohm@925
   149
clasohm@925
   150
goal Integ.thy "inj(zminus)";
clasohm@925
   151
by (rtac injI 1);
clasohm@925
   152
by (dres_inst_tac [("f","zminus")] arg_cong 1);
clasohm@925
   153
by (asm_full_simp_tac (HOL_ss addsimps [zminus_zminus]) 1);
clasohm@925
   154
qed "inj_zminus";
clasohm@925
   155
clasohm@925
   156
goalw Integ.thy [znat_def] "$~ ($#0) = $#0";
clasohm@925
   157
by (simp_tac (arith_ss addsimps [zminus]) 1);
clasohm@925
   158
qed "zminus_0";
clasohm@925
   159
clasohm@925
   160
clasohm@925
   161
(**** znegative: the test for negative integers ****)
clasohm@925
   162
clasohm@925
   163
goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x";
clasohm@925
   164
by (dtac (disjI2 RS less_or_eq_imp_le) 1);
clasohm@925
   165
by (asm_full_simp_tac (arith_ss addsimps add_ac) 1);
clasohm@925
   166
by (dtac add_leD1 1);
clasohm@925
   167
by (assume_tac 1);
clasohm@925
   168
qed "not_znegative_znat_lemma";
clasohm@925
   169
clasohm@925
   170
clasohm@925
   171
goalw Integ.thy [znegative_def, znat_def]
clasohm@925
   172
    "~ znegative($# n)";
clasohm@925
   173
by (simp_tac intrel_ss 1);
clasohm@925
   174
by (safe_tac intrel_cs);
clasohm@925
   175
by (rtac ccontr 1);
clasohm@925
   176
by (etac notE 1);
clasohm@925
   177
by (asm_full_simp_tac arith_ss 1);
clasohm@925
   178
by (dtac not_znegative_znat_lemma 1);
clasohm@925
   179
by (fast_tac (HOL_cs addDs [leD]) 1);
clasohm@925
   180
qed "not_znegative_znat";
clasohm@925
   181
clasohm@925
   182
goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
clasohm@925
   183
by (simp_tac (intrel_ss addsimps [zminus]) 1);
clasohm@925
   184
by (REPEAT (ares_tac [exI, conjI] 1));
clasohm@925
   185
by (rtac (intrelI RS ImageI) 2);
clasohm@925
   186
by (rtac singletonI 3);
clasohm@925
   187
by (simp_tac arith_ss 2);
clasohm@925
   188
by (rtac less_add_Suc1 1);
clasohm@925
   189
qed "znegative_zminus_znat";
clasohm@925
   190
clasohm@925
   191
clasohm@925
   192
(**** zmagnitude: magnitide of an integer, as a natural number ****)
clasohm@925
   193
clasohm@925
   194
goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
clasohm@925
   195
by (nat_ind_tac "n" 1);
clasohm@925
   196
by (ALLGOALS(asm_simp_tac arith_ss));
clasohm@925
   197
qed "diff_Suc_add_0";
clasohm@925
   198
clasohm@925
   199
goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
clasohm@925
   200
by (nat_ind_tac "n" 1);
clasohm@925
   201
by (ALLGOALS(asm_simp_tac arith_ss));
clasohm@925
   202
qed "diff_Suc_add_inverse";
clasohm@925
   203
clasohm@925
   204
goalw Integ.thy [congruent_def]
clasohm@972
   205
    "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
clasohm@925
   206
by (safe_tac intrel_cs);
clasohm@925
   207
by (asm_simp_tac intrel_ss 1);
clasohm@925
   208
by (etac rev_mp 1);
clasohm@925
   209
by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
clasohm@925
   210
by (asm_simp_tac (arith_ss addsimps [inj_Suc RS inj_eq]) 3);
clasohm@925
   211
by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 2);
clasohm@925
   212
by (asm_simp_tac arith_ss 1);
clasohm@925
   213
by (rtac impI 1);
clasohm@925
   214
by (etac subst 1);
clasohm@925
   215
by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
clasohm@925
   216
by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
clasohm@925
   217
by (rtac impI 1);
clasohm@925
   218
by (asm_simp_tac (arith_ss addsimps
clasohm@925
   219
		  [diff_add_inverse, diff_add_0, diff_Suc_add_0,
clasohm@925
   220
		   diff_Suc_add_inverse]) 1);
clasohm@925
   221
qed "zmagnitude_congruent";
clasohm@925
   222
clasohm@925
   223
(*Resolve th against the corresponding facts for zmagnitude*)
clasohm@925
   224
val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
clasohm@925
   225
clasohm@925
   226
clasohm@925
   227
goalw Integ.thy [zmagnitude_def]
clasohm@972
   228
    "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
clasohm@972
   229
\    Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
clasohm@925
   230
by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
clasohm@925
   231
by (asm_simp_tac (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1);
clasohm@925
   232
qed "zmagnitude";
clasohm@925
   233
clasohm@925
   234
goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n";
clasohm@925
   235
by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1);
clasohm@925
   236
qed "zmagnitude_znat";
clasohm@925
   237
clasohm@925
   238
goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n";
clasohm@925
   239
by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus]) 1);
clasohm@925
   240
qed "zmagnitude_zminus_znat";
clasohm@925
   241
clasohm@925
   242
clasohm@925
   243
(**** zadd: addition on Integ ****)
clasohm@925
   244
clasohm@925
   245
(** Congruence property for addition **)
clasohm@925
   246
clasohm@925
   247
goalw Integ.thy [congruent2_def]
clasohm@925
   248
    "congruent2 intrel (%p1 p2.                  \
clasohm@972
   249
\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
clasohm@925
   250
(*Proof via congruent2_commuteI seems longer*)
clasohm@925
   251
by (safe_tac intrel_cs);
clasohm@925
   252
by (asm_simp_tac (intrel_ss addsimps [add_assoc]) 1);
clasohm@925
   253
(*The rest should be trivial, but rearranging terms is hard*)
clasohm@925
   254
by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
clasohm@925
   255
by (asm_simp_tac (arith_ss addsimps [add_assoc RS sym]) 1);
clasohm@925
   256
by (asm_simp_tac (arith_ss addsimps add_ac) 1);
clasohm@925
   257
qed "zadd_congruent2";
clasohm@925
   258
clasohm@925
   259
(*Resolve th against the corresponding facts for zadd*)
clasohm@925
   260
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
clasohm@925
   261
clasohm@925
   262
goalw Integ.thy [zadd_def]
clasohm@972
   263
  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
clasohm@972
   264
\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
clasohm@925
   265
by (asm_simp_tac
clasohm@925
   266
    (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1);
clasohm@925
   267
qed "zadd";
clasohm@925
   268
clasohm@925
   269
goalw Integ.thy [znat_def] "$#0 + z = z";
clasohm@925
   270
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   271
by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
clasohm@925
   272
qed "zadd_0";
clasohm@925
   273
clasohm@925
   274
goal Integ.thy "$~ (z + w) = $~ z + $~ w";
clasohm@925
   275
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   276
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   277
by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
clasohm@925
   278
qed "zminus_zadd_distrib";
clasohm@925
   279
clasohm@925
   280
goal Integ.thy "(z::int) + w = w + z";
clasohm@925
   281
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   282
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   283
by (asm_simp_tac (intrel_ss addsimps (add_ac @ [zadd])) 1);
clasohm@925
   284
qed "zadd_commute";
clasohm@925
   285
clasohm@925
   286
goal Integ.thy "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
clasohm@925
   287
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   288
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   289
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
clasohm@925
   290
by (asm_simp_tac (arith_ss addsimps [zadd, add_assoc]) 1);
clasohm@925
   291
qed "zadd_assoc";
clasohm@925
   292
clasohm@925
   293
(*For AC rewriting*)
clasohm@925
   294
goal Integ.thy "(x::int)+(y+z)=y+(x+z)";
clasohm@925
   295
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   296
by (rtac (zadd_assoc RS trans) 1);
clasohm@925
   297
by (rtac (zadd_commute RS arg_cong) 1);
clasohm@925
   298
qed "zadd_left_commute";
clasohm@925
   299
clasohm@925
   300
(*Integer addition is an AC operator*)
clasohm@925
   301
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
clasohm@925
   302
clasohm@925
   303
goalw Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)";
clasohm@925
   304
by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
clasohm@925
   305
qed "znat_add";
clasohm@925
   306
clasohm@925
   307
goalw Integ.thy [znat_def] "z + ($~ z) = $#0";
clasohm@925
   308
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   309
by (asm_simp_tac (intrel_ss addsimps [zminus, zadd, add_commute]) 1);
clasohm@925
   310
qed "zadd_zminus_inverse";
clasohm@925
   311
clasohm@925
   312
goal Integ.thy "($~ z) + z = $#0";
clasohm@925
   313
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   314
by (rtac zadd_zminus_inverse 1);
clasohm@925
   315
qed "zadd_zminus_inverse2";
clasohm@925
   316
clasohm@925
   317
goal Integ.thy "z + $#0 = z";
clasohm@925
   318
by (rtac (zadd_commute RS trans) 1);
clasohm@925
   319
by (rtac zadd_0 1);
clasohm@925
   320
qed "zadd_0_right";
clasohm@925
   321
clasohm@925
   322
clasohm@925
   323
(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
clasohm@925
   324
clasohm@925
   325
(**** zmult: multiplication on Integ ****)
clasohm@925
   326
clasohm@925
   327
(** Congruence property for multiplication **)
clasohm@925
   328
clasohm@925
   329
goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
clasohm@925
   330
by (simp_tac (arith_ss addsimps add_ac) 1);
clasohm@925
   331
qed "zmult_congruent_lemma";
clasohm@925
   332
clasohm@925
   333
goal Integ.thy 
clasohm@925
   334
    "congruent2 intrel (%p1 p2.  		\
clasohm@925
   335
\               split (%x1 y1. split (%x2 y2. 	\
clasohm@972
   336
\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
clasohm@925
   337
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
clasohm@925
   338
by (safe_tac intrel_cs);
clasohm@925
   339
by (rewtac split_def);
clasohm@925
   340
by (simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
clasohm@925
   341
by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
clasohm@925
   342
by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
clasohm@925
   343
by (rtac (zmult_congruent_lemma RS trans) 1);
clasohm@925
   344
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
clasohm@925
   345
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
clasohm@925
   346
by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
clasohm@925
   347
by (asm_simp_tac (HOL_ss addsimps [add_mult_distrib RS sym]) 1);
clasohm@925
   348
by (asm_simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
clasohm@925
   349
qed "zmult_congruent2";
clasohm@925
   350
clasohm@925
   351
(*Resolve th against the corresponding facts for zmult*)
clasohm@925
   352
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
clasohm@925
   353
clasohm@925
   354
goalw Integ.thy [zmult_def]
clasohm@972
   355
   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) = 	\
clasohm@972
   356
\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
clasohm@925
   357
by (simp_tac (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1);
clasohm@925
   358
qed "zmult";
clasohm@925
   359
clasohm@925
   360
goalw Integ.thy [znat_def] "$#0 * z = $#0";
clasohm@925
   361
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   362
by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
clasohm@925
   363
qed "zmult_0";
clasohm@925
   364
clasohm@925
   365
goalw Integ.thy [znat_def] "$#Suc(0) * z = z";
clasohm@925
   366
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   367
by (asm_simp_tac (arith_ss addsimps [zmult, add_0_right]) 1);
clasohm@925
   368
qed "zmult_1";
clasohm@925
   369
clasohm@925
   370
goal Integ.thy "($~ z) * w = $~ (z * w)";
clasohm@925
   371
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   372
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   373
by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
clasohm@925
   374
qed "zmult_zminus";
clasohm@925
   375
clasohm@925
   376
clasohm@925
   377
goal Integ.thy "($~ z) * ($~ w) = (z * w)";
clasohm@925
   378
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   379
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   380
by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
clasohm@925
   381
qed "zmult_zminus_zminus";
clasohm@925
   382
clasohm@925
   383
goal Integ.thy "(z::int) * w = w * z";
clasohm@925
   384
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   385
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   386
by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
clasohm@925
   387
qed "zmult_commute";
clasohm@925
   388
clasohm@925
   389
goal Integ.thy "z * $# 0 = $#0";
clasohm@925
   390
by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
clasohm@925
   391
qed "zmult_0_right";
clasohm@925
   392
clasohm@925
   393
goal Integ.thy "z * $#Suc(0) = z";
clasohm@925
   394
by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
clasohm@925
   395
qed "zmult_1_right";
clasohm@925
   396
clasohm@925
   397
goal Integ.thy "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
clasohm@925
   398
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   399
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   400
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
clasohm@925
   401
by (asm_simp_tac (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
clasohm@925
   402
qed "zmult_assoc";
clasohm@925
   403
clasohm@925
   404
(*For AC rewriting*)
clasohm@925
   405
qed_goal "zmult_left_commute" Integ.thy
clasohm@925
   406
    "(z1::int)*(z2*z3) = z2*(z1*z3)"
clasohm@925
   407
 (fn _ => [rtac (zmult_commute RS trans) 1, rtac (zmult_assoc RS trans) 1,
clasohm@925
   408
           rtac (zmult_commute RS arg_cong) 1]);
clasohm@925
   409
clasohm@925
   410
(*Integer multiplication is an AC operator*)
clasohm@925
   411
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
clasohm@925
   412
clasohm@925
   413
goal Integ.thy "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
clasohm@925
   414
by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
clasohm@925
   415
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
clasohm@925
   416
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   417
by (asm_simp_tac 
clasohm@925
   418
    (intrel_ss addsimps ([zadd, zmult, add_mult_distrib] @ 
clasohm@925
   419
			 add_ac @ mult_ac)) 1);
clasohm@925
   420
qed "zadd_zmult_distrib";
clasohm@925
   421
clasohm@925
   422
val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
clasohm@925
   423
clasohm@925
   424
goal Integ.thy "w * ($~ z) = $~ (w * z)";
clasohm@925
   425
by (simp_tac (HOL_ss addsimps [zmult_commute', zmult_zminus]) 1);
clasohm@925
   426
qed "zmult_zminus_right";
clasohm@925
   427
clasohm@925
   428
goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
clasohm@925
   429
by (simp_tac (HOL_ss addsimps [zmult_commute',zadd_zmult_distrib]) 1);
clasohm@925
   430
qed "zadd_zmult_distrib2";
clasohm@925
   431
clasohm@925
   432
val zadd_simps = 
clasohm@925
   433
    [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
clasohm@925
   434
clasohm@925
   435
val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib];
clasohm@925
   436
clasohm@925
   437
val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, 
clasohm@925
   438
		   zmult_zminus, zmult_zminus_right];
clasohm@925
   439
clasohm@925
   440
val integ_ss =
clasohm@925
   441
    arith_ss addsimps (zadd_simps @ zminus_simps @ zmult_simps @ 
clasohm@925
   442
		       [zmagnitude_znat, zmagnitude_zminus_znat]);
clasohm@925
   443
clasohm@925
   444
clasohm@925
   445
(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****)
clasohm@925
   446
clasohm@925
   447
(* Some Theorems about zsuc and zpred *)
clasohm@925
   448
goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
clasohm@925
   449
by (simp_tac (arith_ss addsimps [znat_add RS sym]) 1);
clasohm@925
   450
qed "znat_Suc";
clasohm@925
   451
clasohm@925
   452
goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
clasohm@925
   453
by (simp_tac integ_ss 1);
clasohm@925
   454
qed "zminus_zsuc";
clasohm@925
   455
clasohm@925
   456
goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
clasohm@925
   457
by (simp_tac integ_ss 1);
clasohm@925
   458
qed "zminus_zpred";
clasohm@925
   459
clasohm@925
   460
goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
clasohm@925
   461
   "zpred(zsuc(z)) = z";
clasohm@925
   462
by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
clasohm@925
   463
qed "zpred_zsuc";
clasohm@925
   464
clasohm@925
   465
goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
clasohm@925
   466
   "zsuc(zpred(z)) = z";
clasohm@925
   467
by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
clasohm@925
   468
qed "zsuc_zpred";
clasohm@925
   469
clasohm@925
   470
goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
clasohm@925
   471
by (safe_tac HOL_cs);
clasohm@925
   472
by (rtac (zsuc_zpred RS sym) 1);
clasohm@925
   473
by (rtac zpred_zsuc 1);
clasohm@925
   474
qed "zpred_to_zsuc";
clasohm@925
   475
clasohm@925
   476
goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
clasohm@925
   477
by (safe_tac HOL_cs);
clasohm@925
   478
by (rtac (zpred_zsuc RS sym) 1);
clasohm@925
   479
by (rtac zsuc_zpred 1);
clasohm@925
   480
qed "zsuc_to_zpred";
clasohm@925
   481
clasohm@925
   482
goal Integ.thy "($~ z = w) = (z = $~ w)";
clasohm@925
   483
by (safe_tac HOL_cs);
clasohm@925
   484
by (rtac (zminus_zminus RS sym) 1);
clasohm@925
   485
by (rtac zminus_zminus 1);
clasohm@925
   486
qed "zminus_exchange";
clasohm@925
   487
clasohm@925
   488
goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
clasohm@925
   489
by (safe_tac intrel_cs);
clasohm@925
   490
by (dres_inst_tac [("f","zpred")] arg_cong 1);
clasohm@925
   491
by (asm_full_simp_tac (HOL_ss addsimps [zpred_zsuc]) 1);
clasohm@925
   492
qed "bijective_zsuc";
clasohm@925
   493
clasohm@925
   494
goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
clasohm@925
   495
by (safe_tac intrel_cs);
clasohm@925
   496
by (dres_inst_tac [("f","zsuc")] arg_cong 1);
clasohm@925
   497
by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred]) 1);
clasohm@925
   498
qed "bijective_zpred";
clasohm@925
   499
clasohm@925
   500
(* Additional Theorems about zadd *)
clasohm@925
   501
clasohm@925
   502
goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
clasohm@925
   503
by (simp_tac (arith_ss addsimps zadd_ac) 1);
clasohm@925
   504
qed "zadd_zsuc";
clasohm@925
   505
clasohm@925
   506
goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
clasohm@925
   507
by (simp_tac (arith_ss addsimps zadd_ac) 1);
clasohm@925
   508
qed "zadd_zsuc_right";
clasohm@925
   509
clasohm@925
   510
goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
clasohm@925
   511
by (simp_tac (arith_ss addsimps zadd_ac) 1);
clasohm@925
   512
qed "zadd_zpred";
clasohm@925
   513
clasohm@925
   514
goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
clasohm@925
   515
by (simp_tac (arith_ss addsimps zadd_ac) 1);
clasohm@925
   516
qed "zadd_zpred_right";
clasohm@925
   517
clasohm@925
   518
clasohm@925
   519
(* Additional Theorems about zmult *)
clasohm@925
   520
clasohm@925
   521
goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z";
clasohm@925
   522
by (simp_tac (integ_ss addsimps [zadd_zmult_distrib, zadd_commute]) 1);
clasohm@925
   523
qed "zmult_zsuc";
clasohm@925
   524
clasohm@925
   525
goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z";
clasohm@925
   526
by (simp_tac 
clasohm@925
   527
    (integ_ss addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1);
clasohm@925
   528
qed "zmult_zsuc_right";
clasohm@925
   529
clasohm@925
   530
goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
clasohm@925
   531
by (simp_tac (integ_ss addsimps [zadd_zmult_distrib]) 1);
clasohm@925
   532
qed "zmult_zpred";
clasohm@925
   533
clasohm@925
   534
goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
clasohm@925
   535
by (simp_tac (integ_ss addsimps [zadd_zmult_distrib2, zmult_commute]) 1);
clasohm@925
   536
qed "zmult_zpred_right";
clasohm@925
   537
clasohm@925
   538
(* Further Theorems about zsuc and zpred *)
clasohm@925
   539
goal Integ.thy "$#Suc(m) ~= $#0";
clasohm@925
   540
by (simp_tac (integ_ss addsimps [inj_znat RS inj_eq]) 1);
clasohm@925
   541
qed "znat_Suc_not_znat_Zero";
clasohm@925
   542
clasohm@925
   543
bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym));
clasohm@925
   544
clasohm@925
   545
clasohm@925
   546
goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)";
clasohm@925
   547
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   548
by (asm_full_simp_tac (intrel_ss addsimps [zadd]) 1);
clasohm@925
   549
qed "n_not_zsuc_n";
clasohm@925
   550
clasohm@925
   551
val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
clasohm@925
   552
clasohm@925
   553
goal Integ.thy "w ~= zpred(w)";
clasohm@925
   554
by (safe_tac HOL_cs);
clasohm@925
   555
by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
clasohm@925
   556
by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
clasohm@925
   557
qed "n_not_zpred_n";
clasohm@925
   558
clasohm@925
   559
val zpred_n_not_n = n_not_zpred_n RS not_sym;
clasohm@925
   560
clasohm@925
   561
clasohm@925
   562
(* Theorems about less and less_equal *)
clasohm@925
   563
clasohm@925
   564
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
clasohm@925
   565
    "!!w. w<z ==> ? n. z = w + $#(Suc(n))";
clasohm@925
   566
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   567
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   568
by (safe_tac intrel_cs);
clasohm@925
   569
by (asm_full_simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
clasohm@925
   570
by (safe_tac (intrel_cs addSDs [less_eq_Suc_add]));
clasohm@925
   571
by (res_inst_tac [("x","k")] exI 1);
clasohm@925
   572
by (asm_full_simp_tac (HOL_ss addsimps ([add_Suc RS sym] @ add_ac)) 1);
clasohm@925
   573
(*To cancel x2, rename it to be first!*)
clasohm@925
   574
by (rename_tac "a b c" 1);
clasohm@925
   575
by (asm_full_simp_tac (HOL_ss addsimps (add_left_cancel::add_ac)) 1);
clasohm@925
   576
qed "zless_eq_zadd_Suc";
clasohm@925
   577
clasohm@925
   578
goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
clasohm@925
   579
    "z < z + $#(Suc(n))";
clasohm@925
   580
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   581
by (safe_tac intrel_cs);
clasohm@925
   582
by (simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
clasohm@925
   583
by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
clasohm@925
   584
by (rtac le_less_trans 1);
clasohm@925
   585
by (rtac lessI 2);
clasohm@925
   586
by (asm_simp_tac (arith_ss addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1);
clasohm@925
   587
qed "zless_zadd_Suc";
clasohm@925
   588
clasohm@925
   589
goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
clasohm@925
   590
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
clasohm@925
   591
by (simp_tac 
clasohm@925
   592
    (arith_ss addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
clasohm@925
   593
qed "zless_trans";
clasohm@925
   594
clasohm@925
   595
goalw Integ.thy [zsuc_def] "z<zsuc(z)";
clasohm@925
   596
by (rtac zless_zadd_Suc 1);
clasohm@925
   597
qed "zlessI";
clasohm@925
   598
clasohm@925
   599
val zless_zsucI = zlessI RSN (2,zless_trans);
clasohm@925
   600
clasohm@925
   601
goal Integ.thy "!!z w::int. z<w ==> ~w<z";
clasohm@925
   602
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
clasohm@925
   603
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   604
by (safe_tac intrel_cs);
clasohm@925
   605
by (asm_full_simp_tac (intrel_ss addsimps ([znat_def, zadd])) 1);
clasohm@925
   606
by (asm_full_simp_tac
clasohm@925
   607
 (HOL_ss addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
clasohm@925
   608
by (resolve_tac [less_not_refl2 RS notE] 1);
clasohm@925
   609
by (etac sym 2);
clasohm@925
   610
by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1));
clasohm@925
   611
qed "zless_not_sym";
clasohm@925
   612
clasohm@925
   613
(* [| n<m; m<n |] ==> R *)
clasohm@925
   614
bind_thm ("zless_asym", (zless_not_sym RS notE));
clasohm@925
   615
clasohm@925
   616
goal Integ.thy "!!z::int. ~ z<z";
clasohm@925
   617
by (resolve_tac [zless_asym RS notI] 1);
clasohm@925
   618
by (REPEAT (assume_tac 1));
clasohm@925
   619
qed "zless_not_refl";
clasohm@925
   620
clasohm@925
   621
(* z<z ==> R *)
clasohm@925
   622
bind_thm ("zless_anti_refl", (zless_not_refl RS notE));
clasohm@925
   623
clasohm@925
   624
goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
clasohm@925
   625
by(fast_tac (HOL_cs addEs [zless_anti_refl]) 1);
clasohm@925
   626
qed "zless_not_refl2";
clasohm@925
   627
clasohm@925
   628
clasohm@925
   629
(*"Less than" is a linear ordering*)
clasohm@925
   630
goalw Integ.thy [zless_def, znegative_def, zdiff_def] 
clasohm@925
   631
    "z<w | z=w | w<(z::int)";
clasohm@925
   632
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
clasohm@925
   633
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
clasohm@925
   634
by (safe_tac intrel_cs);
clasohm@925
   635
by (asm_full_simp_tac
clasohm@925
   636
    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
clasohm@925
   637
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
clasohm@925
   638
by (etac disjE 2);
clasohm@925
   639
by (assume_tac 2);
clasohm@925
   640
by (DEPTH_SOLVE
clasohm@925
   641
    (swap_res_tac [exI] 1 THEN 
clasohm@925
   642
     swap_res_tac [exI] 1 THEN 
clasohm@925
   643
     etac conjI 1 THEN 
clasohm@925
   644
     simp_tac (arith_ss addsimps add_ac)  1));
clasohm@925
   645
qed "zless_linear";
clasohm@925
   646
clasohm@925
   647
clasohm@925
   648
(*** Properties of <= ***)
clasohm@925
   649
clasohm@925
   650
goalw Integ.thy  [zless_def, znegative_def, zdiff_def, znat_def]
clasohm@925
   651
    "($#m < $#n) = (m<n)";
clasohm@925
   652
by (simp_tac
clasohm@925
   653
    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
clasohm@925
   654
by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
clasohm@925
   655
qed "zless_eq_less";
clasohm@925
   656
clasohm@925
   657
goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
clasohm@925
   658
by (simp_tac (HOL_ss addsimps [zless_eq_less]) 1);
clasohm@925
   659
qed "zle_eq_le";
clasohm@925
   660
clasohm@925
   661
goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
clasohm@925
   662
by (assume_tac 1);
clasohm@925
   663
qed "zleI";
clasohm@925
   664
clasohm@925
   665
goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
clasohm@925
   666
by (assume_tac 1);
clasohm@925
   667
qed "zleD";
clasohm@925
   668
clasohm@925
   669
val zleE = make_elim zleD;
clasohm@925
   670
clasohm@925
   671
goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
clasohm@925
   672
by (fast_tac HOL_cs 1);
clasohm@925
   673
qed "not_zleE";
clasohm@925
   674
clasohm@925
   675
goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
clasohm@925
   676
by (fast_tac (HOL_cs addEs [zless_asym]) 1);
clasohm@925
   677
qed "zless_imp_zle";
clasohm@925
   678
clasohm@925
   679
goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
clasohm@925
   680
by (cut_facts_tac [zless_linear] 1);
clasohm@925
   681
by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
clasohm@925
   682
qed "zle_imp_zless_or_eq";
clasohm@925
   683
clasohm@925
   684
goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
clasohm@925
   685
by (cut_facts_tac [zless_linear] 1);
clasohm@925
   686
by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
clasohm@925
   687
qed "zless_or_eq_imp_zle";
clasohm@925
   688
clasohm@925
   689
goal Integ.thy "(x <= (y::int)) = (x < y | x=y)";
clasohm@925
   690
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
clasohm@925
   691
qed "zle_eq_zless_or_eq";
clasohm@925
   692
clasohm@925
   693
goal Integ.thy "w <= (w::int)";
clasohm@925
   694
by (simp_tac (HOL_ss addsimps [zle_eq_zless_or_eq]) 1);
clasohm@925
   695
qed "zle_refl";
clasohm@925
   696
clasohm@925
   697
val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
clasohm@925
   698
by (dtac zle_imp_zless_or_eq 1);
clasohm@925
   699
by (fast_tac (HOL_cs addIs [zless_trans]) 1);
clasohm@925
   700
qed "zle_zless_trans";
clasohm@925
   701
clasohm@925
   702
goal Integ.thy "!!i. [| i <= j; j <= k |] ==> i <= (k::int)";
clasohm@925
   703
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
clasohm@925
   704
	    rtac zless_or_eq_imp_zle, fast_tac (HOL_cs addIs [zless_trans])]);
clasohm@925
   705
qed "zle_trans";
clasohm@925
   706
clasohm@925
   707
goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
clasohm@925
   708
by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
clasohm@925
   709
	    fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
clasohm@925
   710
qed "zle_anti_sym";
clasohm@925
   711
clasohm@925
   712
clasohm@925
   713
goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w";
clasohm@925
   714
by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
clasohm@925
   715
by (asm_full_simp_tac (integ_ss addsimps zadd_ac) 1);
clasohm@925
   716
qed "zadd_left_cancel";
clasohm@925
   717
clasohm@925
   718
clasohm@925
   719
(*** Monotonicity results ***)
clasohm@925
   720
clasohm@925
   721
goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
clasohm@925
   722
by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
clasohm@925
   723
by (simp_tac (HOL_ss addsimps zadd_ac) 1);
clasohm@925
   724
by (simp_tac (HOL_ss addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
clasohm@925
   725
qed "zadd_zless_mono1";
clasohm@925
   726
clasohm@925
   727
goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
clasohm@925
   728
by (safe_tac (HOL_cs addSEs [zadd_zless_mono1]));
clasohm@925
   729
by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
clasohm@925
   730
by (asm_full_simp_tac (integ_ss addsimps [zadd_assoc]) 1);
clasohm@925
   731
qed "zadd_left_cancel_zless";
clasohm@925
   732
clasohm@925
   733
goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)";
clasohm@925
   734
by (asm_full_simp_tac
clasohm@925
   735
    (integ_ss addsimps [zle_def, zadd_left_cancel_zless]) 1);
clasohm@925
   736
qed "zadd_left_cancel_zle";
clasohm@925
   737
clasohm@925
   738
(*"v<=w ==> v+z <= w+z"*)
clasohm@925
   739
bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
clasohm@925
   740
clasohm@925
   741
clasohm@925
   742
goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
clasohm@925
   743
by (etac (zadd_zle_mono1 RS zle_trans) 1);
clasohm@925
   744
by (simp_tac (HOL_ss addsimps [zadd_commute]) 1);
clasohm@925
   745
(*w moves to the end because it is free while z', z are bound*)
clasohm@925
   746
by (etac zadd_zle_mono1 1);
clasohm@925
   747
qed "zadd_zle_mono";
clasohm@925
   748
clasohm@925
   749
goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w";
clasohm@925
   750
by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
clasohm@925
   751
by (asm_full_simp_tac (integ_ss addsimps [zadd_commute]) 1);
clasohm@925
   752
qed "zadd_zle_self";