# HG changeset patch
# User paulson
# Date 906127484 -7200
# Node ID c38cc427976c6126c05a3dcc47afe6ba48dde3ab
# Parent  691c708985186ff0fcaa8facaa2147e1a1f666db
Now defines "int" as a linear order; basic derivations moved to IntDef

diff -r 691c70898518 -r c38cc427976c src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Fri Sep 18 16:04:00 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Fri Sep 18 16:04:44 1998 +0200
@@ -1,663 +1,105 @@
-(*  Title:      Integ.ML
+(*  Title:      Integ.thy
     ID:         $Id$
-    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1998  University of Cambridge
 
-The integers as equivalence classes over nat*nat.
-
-Could also prove...
-"znegative(z) ==> $# zmagnitude(z) = - z"
-"~ znegative(z) ==> $# zmagnitude(z) = z"
+Type "int" is a linear order
 *)
 
-
-(*** Proving that intrel is an equivalence relation ***)
-
-val eqa::eqb::prems = goal Arith.thy 
-    "[| (x1::nat) + y2 = x2 + y1; x2 + y3 = x3 + y2 |] ==> \
-\       x1 + y3 = x3 + y1";
-by (res_inst_tac [("k1","x2")] (add_left_cancel RS iffD1) 1);
-by (rtac (add_left_commute RS trans) 1);
-by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1);
-by (stac eqa 1);
-by (rtac (add_left_commute) 1);
-qed "integ_trans_lemma";
-
-(** Natural deduction for intrel **)
-
-Goalw  [intrel_def] "[| x1+y2 = x2+y1|] ==> ((x1,y1),(x2,y2)): intrel";
-by (Fast_tac 1);
-qed "intrelI";
-
-(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
-Goalw [intrel_def]
-  "p: intrel --> (EX x1 y1 x2 y2. \
-\                  p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1)";
-by (Fast_tac 1);
-qed "intrelE_lemma";
-
-val [major,minor] = Goal
-  "[| p: intrel;  \
-\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1+y2 = x2+y1|] ==> Q |] \
-\  ==> Q";
-by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "intrelE";
-
-AddSIs [intrelI];
-AddSEs [intrelE];
-
-Goal "((x1,y1),(x2,y2)): intrel = (x1+y2 = x2+y1)";
-by (Fast_tac 1);
-qed "intrel_iff";
-
-Goal "(x,x): intrel";
-by (stac surjective_pairing 1 THEN rtac (refl RS intrelI) 1);
-qed "intrel_refl";
-
-Goalw [equiv_def, refl_def, sym_def, trans_def]
-    "equiv {x::(nat*nat).True} intrel";
-by (fast_tac (claset() addSIs [intrel_refl] 
-                        addSEs [sym, integ_trans_lemma]) 1);
-qed "equiv_intrel";
-
-val equiv_intrel_iff =
-    [TrueI, TrueI] MRS 
-    ([CollectI, CollectI] MRS 
-    (equiv_intrel RS eq_equiv_class_iff));
-
-Goalw  [Integ_def,intrel_def,quotient_def] "intrel^^{(x,y)}:Integ";
-by (Fast_tac 1);
-qed "intrel_in_integ";
-
-Goal "inj_on Abs_Integ Integ";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_Integ_inverse 1);
-qed "inj_on_Abs_Integ";
-
-Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
-          intrel_iff, intrel_in_integ, Abs_Integ_inverse];
-
-Goal "inj(Rep_Integ)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_Integ_inverse 1);
-qed "inj_Rep_Integ";
-
-
-
-
-(** znat: the injection from nat to Integ **)
-
-Goal "inj(znat)";
-by (rtac injI 1);
-by (rewtac znat_def);
-by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
-by (REPEAT (rtac intrel_in_integ 1));
-by (dtac eq_equiv_class 1);
-by (rtac equiv_intrel 1);
-by (Fast_tac 1);
-by Safe_tac;
-by (Asm_full_simp_tac 1);
-qed "inj_znat";
-
-
-(**** zminus: unary negation on Integ ****)
-
-Goalw [congruent_def]
-  "congruent intrel (%p. split (%x y. intrel^^{(y,x)}) p)";
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps add_ac) 1);
-qed "zminus_congruent";
-
-
-(*Resolve th against the corresponding facts for zminus*)
-val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
-
-Goalw [zminus_def]
-      "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})";
-by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
-by (simp_tac (simpset() addsimps 
-   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
-qed "zminus";
-
-(*by lcp*)
-val [prem] = Goal "(!!x y. z = Abs_Integ(intrel^^{(x,y)}) ==> P) ==> P";
-by (res_inst_tac [("x1","z")] 
-    (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
-by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (rtac prem 1);
-by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
-qed "eq_Abs_Integ";
-
-Goal "- (- z) = (z::int)";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_zminus";
-Addsimps [zminus_zminus];
-
-Goal "inj(uminus::int=>int)";
-by (rtac injI 1);
-by (dres_inst_tac [("f","uminus")] arg_cong 1);
-by (Asm_full_simp_tac 1);
-qed "inj_zminus";
-
-Goalw [znat_def] "- ($# 0) = $# 0";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_nat0";
-
-Addsimps [zminus_nat0];
-
-
-(**** znegative: the test for negative integers ****)
-
+Goal "(w<z) = znegative(w-z)";
+by (simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zless_eq_znegative";
 
-Goalw [znegative_def, znat_def] "~ znegative($# n)";
-by (Simp_tac 1);
-by Safe_tac;
-qed "not_znegative_znat";
-
-Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "znegative_zminus_znat";
-
-Addsimps [znegative_zminus_znat, not_znegative_znat]; 
-
-
-(**** zmagnitude: magnitide of an integer, as a natural number ****)
-
-Goalw [congruent_def]
-    "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))";
-by Safe_tac;
-by (Asm_simp_tac 1);
-by (etac rev_mp 1);
-by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
-by (asm_simp_tac (simpset() addsimps [inj_Suc RS inj_eq]) 3);
-by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 2);
-by (Asm_simp_tac 1);
-by (rtac impI 1);
-by (etac subst 1);
-by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [diff_add_inverse,diff_add_0]) 1);
-qed "zmagnitude_congruent";
-
-(*Resolve th against the corresponding facts for zmagnitude*)
-val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
-
-
-Goalw [zmagnitude_def]
-    "zmagnitude (Abs_Integ(intrel^^{(x,y)})) = \
-\    Abs_Integ(intrel^^{((y - x) + (x - y),0)})";
-by (res_inst_tac [("f","Abs_Integ")] arg_cong 1);
-by (asm_simp_tac (simpset() addsimps [zmagnitude_ize UN_equiv_class]) 1);
-qed "zmagnitude";
-
-Goalw [znat_def] "zmagnitude($# n) = $#n";
-by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1);
-qed "zmagnitude_znat";
-
-Goalw [znat_def] "zmagnitude(- $# n) = $#n";
-by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1);
-qed "zmagnitude_zminus_znat";
-
-Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
-
-
-(**** zadd: addition on Integ ****)
-
-(** Congruence property for addition **)
-
-Goalw [congruent2_def]
-    "congruent2 intrel (%p1 p2.                  \
-\         split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)";
-(*Proof via congruent2_commuteI seems longer*)
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [add_assoc]) 1);
-(*The rest should be trivial, but rearranging terms is hard*)
-by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
-qed "zadd_congruent2";
-
-(*Resolve th against the corresponding facts for zadd*)
-val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
-
-Goalw [zadd_def]
-  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
-\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
-by (asm_simp_tac
-    (simpset() addsimps [zadd_ize UN_equiv_class2]) 1);
-qed "zadd";
-
-Goal "- (z + w) = - z + - (w::int)";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
-qed "zminus_zadd_distrib";
-Addsimps [zminus_zadd_distrib];
-
-Goal "(z::int) + w = w + z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps (add_ac @ [zadd])) 1);
-qed "zadd_commute";
-
-Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
-qed "zadd_assoc";
-
-(*For AC rewriting*)
-Goal "(x::int)+(y+z)=y+(x+z)";
-by (rtac (zadd_commute RS trans) 1);
-by (rtac (zadd_assoc RS trans) 1);
-by (rtac (zadd_commute RS arg_cong) 1);
-qed "zadd_left_commute";
-
-(*Integer addition is an AC operator*)
-val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
-
-Goalw [znat_def] "($#m) + ($#n) = $# (m + n)";
-by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "add_znat";
-
-Goal "$# (Suc m) = $# 1 + ($# m)";
-by (simp_tac (simpset() addsimps [add_znat]) 1);
-qed "znat_Suc";
-
-Goalw [znat_def] "$# 0 + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
-qed "zadd_nat0";
-
-Goal "z + $# 0 = z";
-by (rtac (zadd_commute RS trans) 1);
-by (rtac zadd_nat0 1);
-qed "zadd_nat0_right";
-
-Goalw [znat_def] "z + (- z) = $# 0";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
-qed "zadd_zminus_inverse_nat";
-
-Goal "(- z) + z = $# 0";
-by (rtac (zadd_commute RS trans) 1);
-by (rtac zadd_zminus_inverse_nat 1);
-qed "zadd_zminus_inverse_nat2";
-
-Addsimps [zadd_nat0, zadd_nat0_right,
-	  zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
-
-
-(** Lemmas **)
-
-qed_goal "zadd_assoc_cong" Integ.thy
-    "!!z. (z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
- (fn _ => [(asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1)]);
-
-qed_goal "zadd_assoc_swap" Integ.thy "(z::int) + (v + w) = v + (z + w)"
- (fn _ => [(REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1))]);
+Goal "(w=z) = iszero(w-z)";
+by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1);
+qed "eq_eq_iszero";
 
-
-(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
-
-(**** zmult: multiplication on Integ ****)
-
-(** Congruence property for multiplication **)
-
-Goal "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
-by (simp_tac (simpset() addsimps add_ac) 1);
-qed "zmult_congruent_lemma";
-
-Goal "congruent2 intrel (%p1 p2.                 \
-\               split (%x1 y1. split (%x2 y2.   \
-\                   intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)";
-by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by (pair_tac "w" 2);
-by (rename_tac "z1 z2" 2);
-by Safe_tac;
-by (rewtac split_def);
-by (simp_tac (simpset() addsimps add_ac@mult_ac) 1);
-by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
-                           addsimps add_ac@mult_ac) 1);
-by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1);
-by (rtac (zmult_congruent_lemma RS trans) 1);
-by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
-by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
-by (rtac (zmult_congruent_lemma RS trans RS sym) 1);
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
-qed "zmult_congruent2";
-
-(*Resolve th against the corresponding facts for zmult*)
-val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
-
-Goalw [zmult_def]
-   "Abs_Integ((intrel^^{(x1,y1)})) * Abs_Integ((intrel^^{(x2,y2)})) =   \
-\   Abs_Integ(intrel ^^ {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
-by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1);
-qed "zmult";
-
-Goal "(- z) * w = - (z * (w::int))";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
-qed "zmult_zminus";
-
-
-Goal "(- z) * (- w) = (z * (w::int))";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
-qed "zmult_zminus_zminus";
-
-Goal "(z::int) * w = w * z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1);
-qed "zmult_commute";
-
-Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)";
-by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @ 
-                                     add_ac @ mult_ac)) 1);
-qed "zmult_assoc";
-
-(*For AC rewriting*)
-qed_goal "zmult_left_commute" Integ.thy
-    "(z1::int)*(z2*z3) = z2*(z1*z3)"
- (fn _ => [rtac (zmult_commute RS trans) 1, rtac (zmult_assoc RS trans) 1,
-           rtac (zmult_commute RS arg_cong) 1]);
-
-(*Integer multiplication is an AC operator*)
-val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
-
-Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
-by (res_inst_tac [("z","z1")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac 
-    (simpset() addsimps ([add_mult_distrib2, zadd, zmult] @ 
-                        add_ac @ mult_ac)) 1);
-qed "zadd_zmult_distrib";
-
-val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
-
-Goal "w * (- z) = - (w * (z::int))";
-by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
-qed "zmult_zminus_right";
-
-Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
-qed "zadd_zmult_distrib2";
-
-Goalw [znat_def] "$# 0 * z = $# 0";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_nat0";
-
-Goalw [znat_def] "$# 1 * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_nat1";
-
-Goal "z * $# 0 = $# 0";
-by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1);
-qed "zmult_nat0_right";
-
-Goal "z * $# 1 = z";
-by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1);
-qed "zmult_nat1_right";
-
-Addsimps [zmult_nat0, zmult_nat0_right, zmult_nat1, zmult_nat1_right];
-
-
-Goal "(- z = w) = (z = - (w::int))";
-by Safe_tac;
-by (rtac (zminus_zminus RS sym) 1);
-by (rtac zminus_zminus 1);
-qed "zminus_exchange";
-
-
-(* Theorems about less and less_equal *)
-
-(*This lemma allows direct proofs of other <-properties*)
-Goalw [zless_def, znegative_def, zdiff_def, znat_def] 
-    "(w < z) = (EX n. z = w + $#(Suc n))";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
-by (safe_tac (claset() addSDs [less_eq_Suc_add]));
-by (res_inst_tac [("x","k")] exI 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
-qed "zless_iff_Suc_zadd";
-
-Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
-by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_znat]));
-qed "zless_trans";
+Goal "(w<=z) = (~ znegative(z-w))";
+by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
+qed "zle_eq_not_znegative";
 
-Goal "!!w::int. z<w ==> ~w<z";
-by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
-qed "zless_not_sym";
-
-(* [| n<m;  ~P ==> m<n |] ==> P *)
-bind_thm ("zless_asym", (zless_not_sym RS swap));
-
-Goal "!!z::int. ~ z<z";
-by (resolve_tac [zless_asym RS notI] 1);
-by (REPEAT (assume_tac 1));
-qed "zless_not_refl";
-
-(* z<z ==> R *)
-bind_thm ("zless_irrefl", (zless_not_refl RS notE));
-AddSEs [zless_irrefl];
-
-Goal "z<w ==> w ~= (z::int)";
-by (Blast_tac 1);
-qed "zless_not_refl2";
-
-
-(*"Less than" is a linear ordering*)
-Goalw [zless_def, znegative_def, zdiff_def] 
-    "z<w | z=w | w<(z::int)";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by Safe_tac;
-by (asm_full_simp_tac
-    (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
-by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (auto_tac (claset(), simpset() addsimps add_ac));
-qed "zless_linear";
-
-Goal "($# m = $# n) = (m = n)"; 
-by (fast_tac (claset() addSEs [inj_znat RS injD]) 1); 
-qed "znat_znat_eq"; 
-AddIffs [znat_znat_eq]; 
-
-Goal "($#m < $#n) = (m<n)";
-by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
-				  add_znat]) 1);
-qed "zless_eq_less";
-Addsimps [zless_eq_less];
-
-
-(*** Properties of <= ***)
-
-Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
-by (Simp_tac 1);
-qed "zle_eq_le";
-Addsimps [zle_eq_le];
-
-Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
-by (assume_tac 1);
-qed "zleI";
-
-Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
-by (assume_tac 1);
-qed "zleD";
-
-val zleE = make_elim zleD;
-
-Goalw [zle_def] "~ z <= w ==> w<(z::int)";
-by (Fast_tac 1);
-qed "not_zleE";
-
-Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
-by (cut_facts_tac [zless_linear] 1);
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zle_imp_zless_or_eq";
+(*This list of rewrites simplifies (in)equalities by subtracting the RHS
+  from the LHS, then using the cancellation simproc.  Use with zadd_ac.*)
+val zcompare_0_rls = 
+    [zdiff_def, zless_eq_znegative, eq_eq_iszero, zle_eq_not_znegative];
 
-Goalw [zle_def] "z<w | z=w ==> z <= (w::int)";
-by (cut_facts_tac [zless_linear] 1);
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zless_or_eq_imp_zle";
-
-Goal "(x <= (y::int)) = (x < y | x=y)";
-by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
-qed "zle_eq_zless_or_eq";
-
-Goal "w <= (w::int)";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
-qed "zle_refl";
-
-Goalw [zle_def] "z < w ==> z <= (w::int)";
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zless_imp_zle";
-
-Addsimps [zle_refl, zless_imp_zle];
-
-Goal "[| i <= j; j < k |] ==> i < (k::int)";
-by (dtac zle_imp_zless_or_eq 1);
-by (blast_tac (claset() addIs [zless_trans]) 1);
-qed "zle_zless_trans";
-
-Goal "[| i < j; j <= k |] ==> i < (k::int)";
-by (dtac zle_imp_zless_or_eq 1);
-by (blast_tac (claset() addIs [zless_trans]) 1);
-qed "zless_zle_trans";
-
-Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
-by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
-            rtac zless_or_eq_imp_zle, 
-	    blast_tac (claset() addIs [zless_trans])]);
-qed "zle_trans";
-
-Goal "[| z <= w; w <= z |] ==> z = (w::int)";
-by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
-            blast_tac (claset() addEs [zless_asym])]);
-qed "zle_anti_sym";
-
-
-Goal "!!w::int. (z + w' = z + w) = (w' = w)";
-by Safe_tac;
-by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zadd_left_cancel";
-
-Addsimps [zadd_left_cancel];
-
-Goal "!!z::int. (w' + z = w + z) = (w' = w)";
-by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zadd_right_cancel";
-
-Addsimps [zadd_right_cancel];
-
-
-Goal "(w < z + $# 1) = (w<z | w=z)";
-by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_znat]));
-by (cut_inst_tac [("m","n")] znat_Suc 1);
-by (exhaust_tac "n" 1);
-auto();
-by (full_simp_tac (simpset() addsimps zadd_ac) 1);
-by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-qed "zless_add_nat1_eq";
-
-
-Goal "(w + $# 1 <= z) = (w<z)";
-by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1);
-by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
-	      simpset() addsimps [symmetric zle_def]));
-qed "add_nat1_zle_eq";
 
 
 (*** Monotonicity results ***)
 
-Goal "!!z::int. v < w ==> v + z < w + z";
-by (full_simp_tac (simpset() addsimps (zless_iff_Suc_zadd::zadd_ac)) 1);
-qed "zadd_zless_mono1";
+Goal "(v+z < w+z) = (v < (w::int))";
+by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+qed "zadd_right_cancel_zless";
 
-Goal "!!z::int. (v+z < w+z) = (v < w)";
-by (safe_tac (claset() addSEs [zadd_zless_mono1]));
-by (dres_inst_tac [("z", "-z")] zadd_zless_mono1 1);
-by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1);
+Goal "(z+v < z+w) = (v < (w::int))";
+by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zadd_left_cancel_zless";
 
-Goal "!!z::int. (v+z <= w+z) = (v <= w)";
-by (asm_full_simp_tac
-    (simpset() addsimps [zle_def, zadd_left_cancel_zless]) 1);
+Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
+
+Goal "(v+z <= w+z) = (v <= (w::int))";
+by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+qed "zadd_right_cancel_zle";
+
+Goal "(z+v <= z+w) = (v <= (w::int))";
+by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zadd_left_cancel_zle";
 
+Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
+
 (*"v<=w ==> v+z <= w+z"*)
-bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
+bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
 
+(*"v<=w ==> v+z <= w+z"*)
+bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
 
 Goal "!!z z'::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
 by (etac (zadd_zle_mono1 RS zle_trans) 1);
-by (simp_tac (simpset() addsimps [zadd_commute]) 1);
-(*w moves to the end because it is free while z', z are bound*)
-by (etac zadd_zle_mono1 1);
+by (Simp_tac 1);
 qed "zadd_zle_mono";
 
+Goal "!!z z'::int. [| w'<w; z'<=z |] ==> w' + z' < w + z";
+by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
+by (Simp_tac 1);
+qed "zadd_zless_mono";
+
 
-(**** Comparisons: lemmas and proofs by Norbert Voelker ****)
+(*** Comparison laws ***)
 
 Goal "(- x < - y) = (y < (x::int))";
-by (rewrite_goals_tac [zless_def,zdiff_def]); 
-by (simp_tac (simpset() addsimps zadd_ac) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zminus_zless_zminus"; 
 Addsimps [zminus_zless_zminus];
 
 Goal "(- x <= - y) = (y <= (x::int))";
-by (simp_tac (simpset() addsimps [zle_def, zminus_zless_zminus]) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zminus_zle_zminus"; 
 Addsimps [zminus_zle_zminus];
 
 (** The next several equations can make the simplifier loop! **)
 
 Goal "(x < - y) = (y < - (x::int))";
-by (rewrite_goals_tac [zless_def,zdiff_def]); 
-by (simp_tac (simpset() addsimps zadd_ac ) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zless_zminus"; 
 
 Goal "(- x < y) = (- y < (x::int))";
-by (rewrite_goals_tac [zless_def,zdiff_def]); 
-by (simp_tac (simpset() addsimps zadd_ac) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zminus_zless"; 
 
 Goal "(x <= - y) = (y <= - (x::int))";
-by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zle_zminus"; 
 
 Goal "(- x <= y) = (- y <= (x::int))";
-by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "zminus_zle"; 
 
+Goal "$#0 < $# Suc n"; 
+by (Simp_tac 1);
+qed "zero_zless_Suc"; 
+
 Goal "- $# Suc n < $# 0";
-by (stac (zminus_nat0 RS sym) 1); 
-by (stac zminus_zless_zminus 1); 
-by (Simp_tac 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "negative_zless_0"; 
 
 Goal "- $# Suc n < $# m";
@@ -667,12 +109,11 @@
 AddIffs [negative_zless]; 
 
 Goal "- $# n <= $#0";
-by (simp_tac (simpset() addsimps [zminus_zle]) 1); 
+by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
 qed "negative_zle_0"; 
 
 Goal "- $# n <= $# m";
-by (rtac (negative_zle_0 RS zle_trans) 1);
-by (Simp_tac 1); 
+by (simp_tac (simpset() addsimps (add_znat::(zcompare_0_rls @ zadd_ac))) 1);
 qed "negative_zle"; 
 AddIffs [negative_zle]; 
 
@@ -703,93 +144,53 @@
 
 Addsimps [negative_eq_positive, not_znat_zless_negative]; 
 
+
+
 Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
 by Auto_tac; 
-qed "znegative_eq_less_0"; 
+qed "znegative_eq_less_nat0"; 
+
+Goalw [zle_def] "(~znegative x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1); 
+qed "not_znegative_eq_ge_nat0"; 
+
+(**** zmagnitude: magnitide of an integer, as a natural number ****)
+
+Goalw [zmagnitude_def] "zmagnitude($# n) = n";
+by Auto_tac;
+qed "zmagnitude_znat";
 
-Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)";
-by (stac znegative_eq_less_0 1); 
-by (safe_tac (claset() addSDs [zleD,not_zleE,zleI]) ); 
-qed "not_znegative_eq_ge_0"; 
+Goalw [zmagnitude_def] "zmagnitude(- $# n) = n";
+by Auto_tac;
+qed "zmagnitude_zminus_znat";
+
+Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
+
+Goal "~ znegative z ==> $# (zmagnitude z) = z"; 
+by (dtac (not_znegative_eq_ge_nat0 RS iffD1) 1); 
+by (dtac zle_imp_zless_or_eq 1); 
+by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd])); 
+qed "not_zneg_mag"; 
 
 Goal "znegative x ==> ? n. x = - $# Suc n"; 
-by (full_simp_tac (simpset() addsimps [znegative_eq_less_0, 
-				       zless_iff_Suc_zadd]) 1); 
-by (etac exE 1); 
-by (rtac exI 1);
-by (dres_inst_tac [("f","(% z. z + - $# Suc n )")] arg_cong 1); 
-by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); 
+by (auto_tac (claset(), 
+	      simpset() addsimps [znegative_eq_less_nat0, zless_iff_Suc_zadd,
+				  zdiff_eq_eq RS sym, zdiff_def])); 
 qed "znegativeD"; 
 
-Goal "~znegative x ==> ? n. x = $# n"; 
-by (dtac (not_znegative_eq_ge_0 RS iffD1) 1); 
-by (dtac zle_imp_zless_or_eq 1); 
-by (etac disjE 1); 
-by (dtac (zless_iff_Suc_zadd RS iffD1) 1); 
+Goal "znegative z ==> $# (zmagnitude z) = -z"; 
+bd znegativeD 1;
 by Auto_tac; 
-qed "not_znegativeD"; 
+qed "zneg_mag"; 
 
 (* a case theorem distinguishing positive and negative int *)  
 
 val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; 
-by (cut_inst_tac [("P","znegative z")] excluded_middle 1); 
-by (fast_tac (claset() addSDs [znegativeD,not_znegativeD] addSIs prems) 1); 
+by (case_tac "znegative z" 1); 
+by (blast_tac (claset() addSDs [znegativeD] addSIs prems) 1); 
+be (not_zneg_mag RS subst) 1;
+brs prems 1;
 qed "int_cases"; 
 
 fun int_case_tac x = res_inst_tac [("z",x)] int_cases; 
 
-
-(*** Subtraction laws ***)
-
-Goal "x + (y - z) = (x + y) - (z::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
-qed "zadd_zdiff_eq";
-
-Goal "(x - y) + z = (x + z) - (y::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
-qed "zdiff_zadd_eq";
-
-Goal "(x - y) - z = x - (y + (z::int))";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
-qed "zdiff_zdiff_eq";
-
-Goal "x - (y - z) = (x + z) - (y::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
-qed "zdiff_zdiff_eq2";
-
-Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
-by (simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zdiff_zless_eq";
-
-Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)";
-by (simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zless_zdiff_eq";
-
-Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))";
-by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1);
-qed "zdiff_zle_eq";
-
-Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)";
-by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1);
-qed "zle_zdiff_eq";
-
-Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))";
-by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
-qed "zdiff_eq_eq";
-
-Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
-by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
-qed "eq_zdiff_eq";
-
-(*Use with zadd_ac*)
-val zcompare_rls = 
-    [symmetric zdiff_def,
-     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
-     zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, 
-     zdiff_eq_eq, eq_zdiff_eq];
-
-
-(*These rewrite to $# 0, while from Bin onwards we should rewrite to #0  *)
-Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
-
-
diff -r 691c70898518 -r c38cc427976c src/HOL/Integ/Integ.thy
--- a/src/HOL/Integ/Integ.thy	Fri Sep 18 16:04:00 1998 +0200
+++ b/src/HOL/Integ/Integ.thy	Fri Sep 18 16:04:44 1998 +0200
@@ -1,53 +1,18 @@
 (*  Title:      Integ.thy
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1996  University of Cambridge
+    Copyright   1998  University of Cambridge
 
-The integers as equivalence classes over nat*nat.
+Type "int" is a linear order
 *)
 
-Integ = Equiv + Arith +
-constdefs
-  intrel      :: "((nat * nat) * (nat * nat)) set"
-  "intrel == {p. ? x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
+Integ = IntDef +
 
-typedef (Integ)
-  int = "{x::(nat*nat).True}/intrel"            (Equiv.quotient_def)
-
-instance
-  int :: {ord, plus, times, minus}
-
-defs
-  zminus_def
-    "- Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)"
+instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le)
+instance int :: linorder (zle_linear)
 
 constdefs
-
-  znat        :: nat => int                                  ("$# _" [80] 80)
-  "$# m == Abs_Integ(intrel ^^ {(m,0)})"
-
-  znegative   :: int => bool
-  "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
-
-  zmagnitude  :: int => int
-  "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).
-                              split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
-
-defs
-  zadd_def
-   "Z1 + Z2 == 
-       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2).   
-           split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)"
-
-  zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)"
-
-  zless_def "Z1<Z2 == znegative(Z1 - Z2)"
-
-  zle_def   "Z1 <= (Z2::int) == ~(Z2 < Z1)"
-
-  zmult_def
-   "Z1 * Z2 == 
-       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   
-           split (%x2 y2. intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
+  zmagnitude  :: int => nat
+  "zmagnitude(Z) == @m. Z = $# m | -Z = $# m"
 
 end