# HG changeset patch
# User clasohm
# Date 794228685 -3600
# Node ID 15539deb68638ef34966e8ee7a8fd92a1a3c81d8
# Parent  806721cfbf460d699bf3aa087a0ddb569e5aa693
new version of HOL/Integ with curried function application

diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Equiv.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Equiv.ML	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,311 @@
+(*  Title: 	Equiv.ML
+    ID:         $Id$
+    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+Equivalence relations in HOL Set Theory 
+*)
+
+open Equiv;
+
+(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
+
+(** first half: equiv A r ==> converse(r) O r = r **)
+
+goalw Equiv.thy [trans_def,sym_def,converse_def]
+    "!!r. [| sym(r); trans(r) |] ==> converse(r) O r <= r";
+by (fast_tac (comp_cs addSEs [converseD]) 1);
+qed "sym_trans_comp_subset";
+
+val [major,minor]=goal Equiv.thy "[|<x,y>:r; z=<x,y>|] ==>  z:r";
+by (simp_tac (prod_ss addsimps [minor]) 1);
+by (rtac major 1);
+qed "BreakPair";
+
+val [major]=goal Equiv.thy "[|? x y. <x,y>:r & z=<x,y>|] ==>  z:r";
+by (resolve_tac [major RS exE] 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (asm_simp_tac (prod_ss addsimps [minor]) 1);
+qed "BreakPair1";
+
+val [major,minor]=goal Equiv.thy "[|z:r; z=<x,y>|] ==> <x,y>:r";
+by (simp_tac (prod_ss addsimps [minor RS sym]) 1);
+by (rtac major 1);
+qed "BuildPair";
+
+val [major]=goal Equiv.thy "[|? z:r. <x,y>=z|] ==> <x,y>:r";
+by (resolve_tac [major RS bexE] 1);
+by (asm_simp_tac (prod_ss addsimps []) 1);
+qed "BuildPair1";
+
+val rel_pair_cs = rel_cs addIs [BuildPair1] 
+                         addEs [BreakPair1];
+
+goalw Equiv.thy [refl_def,converse_def]
+    "!!A r. refl A r ==> r <= converse(r) O r";
+by (step_tac comp_cs 1);
+by (dtac subsetD 1);
+by (assume_tac 1);
+by (etac SigmaE 1);
+by (rtac BreakPair1 1);
+by (fast_tac comp_cs 1);
+qed "refl_comp_subset";
+
+goalw Equiv.thy [equiv_def]
+    "!!A r. equiv A r ==> converse(r) O r = r";
+by (rtac equalityI 1);
+by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
+     ORELSE etac conjE 1));
+qed "equiv_comp_eq";
+
+(*second half*)
+goalw Equiv.thy [equiv_def,refl_def,sym_def,trans_def]
+    "!!A r. [| converse(r) O r = r;  Domain(r) = A |] ==> equiv A r";
+by (etac equalityE 1);
+by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
+by (safe_tac set_cs);
+by (fast_tac (set_cs addSIs [converseI] addIs [compI]) 3);
+by (fast_tac (set_cs addSIs [converseI] addIs [compI] addSEs [DomainE]) 2);
+by (fast_tac (rel_pair_cs addSEs [SigmaE] addSIs [SigmaI]) 1);
+by (dtac subsetD 1);
+by (dtac subsetD 1);
+by (fast_tac rel_cs 1);
+by (fast_tac rel_cs 1);
+by flexflex_tac;
+by (dtac subsetD 1);
+by (fast_tac converse_cs 2);
+by (fast_tac converse_cs 1);
+qed "comp_equivI";
+
+(** Equivalence classes **)
+
+(*Lemma for the next result*)
+goalw Equiv.thy [equiv_def,trans_def,sym_def]
+    "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} <= r^^{b}";
+by (safe_tac rel_cs);
+by (rtac ImageI 1);
+by (fast_tac rel_cs 2);
+by (fast_tac rel_cs 1);
+qed "equiv_class_subset";
+
+goal Equiv.thy "!!A r. [| equiv A r;  <a,b>: r |] ==> r^^{a} = r^^{b}";
+by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
+by (rewrite_goals_tac [equiv_def,sym_def]);
+by (fast_tac rel_cs 1);
+qed "equiv_class_eq";
+
+val prems = goalw Equiv.thy [equiv_def,refl_def]
+    "[| equiv A r;  a: A |] ==> a: r^^{a}";
+by (cut_facts_tac prems 1);
+by (fast_tac rel_cs 1);
+qed "equiv_class_self";
+
+(*Lemma for the next result*)
+goalw Equiv.thy [equiv_def,refl_def]
+    "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> <a,b>: r";
+by (fast_tac rel_cs 1);
+qed "subset_equiv_class";
+
+val prems = goal Equiv.thy
+    "[| r^^{a} = r^^{b};  equiv A r;  b: A |] ==> <a,b>: r";
+by (REPEAT (resolve_tac (prems @ [equalityD2, subset_equiv_class]) 1));
+qed "eq_equiv_class";
+
+(*thus r^^{a} = r^^{b} as well*)
+goalw Equiv.thy [equiv_def,trans_def,sym_def]
+    "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> <a,b>: r";
+by (fast_tac rel_cs 1);
+qed "equiv_class_nondisjoint";
+
+val [major] = goalw Equiv.thy [equiv_def,refl_def]
+    "equiv A r ==> r <= Sigma A (%x.A)";
+by (rtac (major RS conjunct1 RS conjunct1) 1);
+qed "equiv_type";
+
+goal Equiv.thy
+    "!!A r. equiv A r ==> (<x,y>: r) = (r^^{x} = r^^{y} & x:A & y:A)";
+by (safe_tac rel_cs);
+by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
+by ((rtac eq_equiv_class 3) THEN 
+    (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
+by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
+    (assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1));
+by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
+    (assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1));
+qed "equiv_class_eq_iff";
+
+goal Equiv.thy
+    "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = (<x,y>: r)";
+by (safe_tac rel_cs);
+by ((rtac eq_equiv_class 1) THEN 
+    (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
+by ((rtac equiv_class_eq 1) THEN 
+    (assume_tac 1) THEN (assume_tac 1));
+qed "eq_equiv_class_iff";
+
+(*** Quotients ***)
+
+(** Introduction/elimination rules -- needed? **)
+
+val prems = goalw Equiv.thy [quotient_def] "x:A ==> r^^{x}: A/r";
+by (rtac UN_I 1);
+by (resolve_tac prems 1);
+by (rtac singletonI 1);
+qed "quotientI";
+
+val [major,minor] = goalw Equiv.thy [quotient_def]
+    "[| X:(A/r);  !!x. [| X = r^^{x};  x:A |] ==> P |] 	\
+\    ==> P";
+by (resolve_tac [major RS UN_E] 1);
+by (rtac minor 1);
+by (assume_tac 2);
+by (fast_tac rel_cs 1);
+qed "quotientE";
+
+(** Not needed by Theory Integ --> bypassed **)
+(**goalw Equiv.thy [equiv_def,refl_def,quotient_def]
+    "!!A r. equiv A r ==> Union(A/r) = A";
+by (fast_tac eq_cs 1);
+qed "Union_quotient";
+**)
+
+(** Not needed by Theory Integ --> bypassed **)
+(*goalw Equiv.thy [quotient_def]
+    "!!A r. [| equiv A r;  X: A/r;  Y: A/r |] ==> X=Y | (X Int Y <= 0)";
+by (safe_tac (ZF_cs addSIs [equiv_class_eq]));
+by (assume_tac 1);
+by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
+by (fast_tac ZF_cs 1);
+qed "quotient_disj";
+**)
+
+(**** Defining unary operations upon equivalence classes ****)
+
+(* theorem needed to prove UN_equiv_class *)
+goal Set.thy "!!A. [| a:A; ! y:A. b(y)=b(a) |] ==> (UN y:A. b(y))=b(a)";
+by (fast_tac (eq_cs addSEs [equalityE]) 1);
+qed "UN_singleton_lemma";
+val UN_singleton = ballI RSN (2,UN_singleton_lemma);
+
+
+(** These proofs really require as local premises
+     equiv A r;  congruent r b
+**)
+
+(*Conversion rule*)
+val prems as [equivA,bcong,_] = goal Equiv.thy
+    "[| equiv A r;  congruent r b;  a: A |] ==> (UN x:r^^{a}. b(x)) = b(a)";
+by (cut_facts_tac prems 1);
+by (rtac UN_singleton 1);
+by (rtac equiv_class_self 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
+by (fast_tac rel_cs 1);
+qed "UN_equiv_class";
+
+(*Resolve th against the "local" premises*)
+val localize = RSLIST [equivA,bcong];
+
+(*type checking of  UN x:r``{a}. b(x) *)
+val _::_::prems = goalw Equiv.thy [quotient_def]
+    "[| equiv A r;  congruent r b;  X: A/r;	\
+\	!!x.  x : A ==> b(x) : B |] 	\
+\    ==> (UN x:X. b(x)) : B";
+by (cut_facts_tac prems 1);
+by (safe_tac rel_cs);
+by (rtac (localize UN_equiv_class RS ssubst) 1);
+by (REPEAT (ares_tac prems 1));
+qed "UN_equiv_class_type";
+
+(*Sufficient conditions for injectiveness.  Could weaken premises!
+  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
+*)
+val _::_::prems = goalw Equiv.thy [quotient_def]
+    "[| equiv A r;   congruent r b;  \
+\       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
+\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
+\    ==> X=Y";
+by (cut_facts_tac prems 1);
+by (safe_tac rel_cs);
+by (rtac (equivA RS equiv_class_eq) 1);
+by (REPEAT (ares_tac prems 1));
+by (etac box_equals 1);
+by (REPEAT (ares_tac [localize UN_equiv_class] 1));
+qed "UN_equiv_class_inject";
+
+
+(**** Defining binary operations upon equivalence classes ****)
+
+
+goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
+    "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
+by (fast_tac rel_cs 1);
+qed "congruent2_implies_congruent";
+
+val equivA::prems = goalw Equiv.thy [congruent_def]
+    "[| equiv A r;  congruent2 r b;  a: A |] ==> \
+\    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
+by (cut_facts_tac (equivA::prems) 1);
+by (safe_tac rel_cs);
+by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
+by (assume_tac 1);
+by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class,
+				 congruent2_implies_congruent]) 1);
+by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
+by (fast_tac rel_cs 1);
+qed "congruent2_implies_congruent_UN";
+
+val prems as equivA::_ = goal Equiv.thy
+    "[| equiv A r;  congruent2 r b;  a1: A;  a2: A |]  \
+\    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
+by (cut_facts_tac prems 1);
+by (asm_simp_tac (prod_ss addsimps [equivA RS UN_equiv_class,
+				    congruent2_implies_congruent,
+				    congruent2_implies_congruent_UN]) 1);
+qed "UN_equiv_class2";
+
+(*type checking*)
+val prems = goalw Equiv.thy [quotient_def]
+    "[| equiv A r;  congruent2 r b;  \
+\       X1: A/r;  X2: A/r;	\
+\	!!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
+\    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
+by (cut_facts_tac prems 1);
+by (safe_tac rel_cs);
+by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
+			     congruent2_implies_congruent_UN,
+			     congruent2_implies_congruent, quotientI]) 1));
+qed "UN_equiv_class_type2";
+
+
+(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
+  than the direct proof*)
+val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
+    "[| equiv A r;	\
+\       !! y z w. [| w: A;  <y,z> : r |] ==> b y w = b z w;      \
+\       !! y z w. [| w: A;  <y,z> : r |] ==> b w y = b w z       \
+\    |] ==> congruent2 r b";
+by (cut_facts_tac prems 1);
+by (safe_tac rel_cs);
+by (rtac trans 1);
+by (REPEAT (ares_tac prems 1
+     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
+qed "congruent2I";
+
+val [equivA,commute,congt] = goal Equiv.thy
+    "[| equiv A r;	\
+\       !! y z. [| y: A;  z: A |] ==> b y z = b z y;        \
+\       !! y z w. [| w: A;  <y,z>: r |] ==> b w y = b w z	\
+\    |] ==> congruent2 r b";
+by (resolve_tac [equivA RS congruent2I] 1);
+by (rtac (commute RS trans) 1);
+by (rtac (commute RS trans RS sym) 3);
+by (rtac sym 5);
+by (REPEAT (ares_tac [congt] 1
+     ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
+qed "congruent2_commuteI";
+
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Equiv.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Equiv.thy	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,28 @@
+(*  Title: 	Equiv.thy
+    ID:         $Id$
+    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+Equivalence relations in Higher-Order Set Theory 
+*)
+
+Equiv = Relation +
+consts
+    refl,equiv 	::      "['a set,('a*'a) set]=>bool"
+    sym         ::      "('a*'a) set=>bool"
+    "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90) 
+                        (*set of equiv classes*)
+    congruent	::	"[('a*'a) set,'a=>'b]=>bool"
+    congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
+
+defs
+    refl_def      "refl A r == r <= Sigma A (%x.A) & (ALL x: A. <x,x> : r)"
+    sym_def       "sym(r)    == ALL x y. <x,y>: r --> <y,x>: r"
+    equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
+    quotient_def  "A/r == UN x:A. {r^^{x}}"  
+    congruent_def   "congruent r b  == ALL y z. <y,z>:r --> b(y)=b(z)"
+    congruent2_def  "congruent2 r b == ALL y1 z1 y2 z2. \
+\           <y1,z1>:r --> <y2,z2>:r --> b y1 y2 = b z1 z2"
+end
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Integ.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Integ.ML	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,752 @@
+(*  Title: 	Integ.ML
+    ID:         $Id$
+    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+
+Could also prove...
+"znegative(z) ==> $# zmagnitude(z) = $~ z"
+"~ znegative(z) ==> $# zmagnitude(z) = z"
+< is a linear ordering
++ and * are monotonic wrt <
+*)
+
+open Integ;
+
+
+(*** 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 [("k2","x2")] (add_left_cancel RS iffD1) 1);
+by (rtac (add_left_commute RS trans) 1);
+by (rtac (eqb RS ssubst) 1);
+by (rtac (add_left_commute RS trans) 1);
+by (rtac (eqa RS ssubst) 1);
+by (rtac (add_left_commute) 1);
+qed "integ_trans_lemma";
+
+(** Natural deduction for intrel **)
+
+val prems = goalw Integ.thy [intrel_def]
+    "[| x1+y2 = x2+y1|] ==> \
+\    <<x1,y1>,<x2,y2>>: intrel";
+by (fast_tac (rel_cs addIs prems) 1);
+qed "intrelI";
+
+(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
+goalw Integ.thy [intrel_def]
+  "p: intrel --> (EX x1 y1 x2 y2. \
+\                  p = <<x1,y1>,<x2,y2>> & x1+y2 = x2+y1)";
+by (fast_tac rel_cs 1);
+qed "intrelE_lemma";
+
+val [major,minor] = goal Integ.thy
+  "[| 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";
+
+val intrel_cs = rel_cs addSIs [intrelI] addSEs [intrelE];
+
+goal Integ.thy "<<x1,y1>,<x2,y2>>: intrel = (x1+y2 = x2+y1)";
+by (fast_tac intrel_cs 1);
+qed "intrel_iff";
+
+goal Integ.thy "<x,x>: intrel";
+by (rtac (surjective_pairing RS ssubst) 1 THEN rtac (refl RS intrelI) 1);
+qed "intrel_refl";
+
+goalw Integ.thy [equiv_def, refl_def, sym_def, trans_def]
+    "equiv {x::(nat*nat).True} intrel";
+by (fast_tac (intrel_cs 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.thy  [Integ_def,intrel_def,quotient_def] "intrel^^{<x,y>}:Integ";
+by (fast_tac set_cs 1);
+qed "intrel_in_integ";
+
+goal Integ.thy "inj_onto Abs_Integ Integ";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_Integ_inverse 1);
+qed "inj_onto_Abs_Integ";
+
+val intrel_ss = 
+    arith_ss addsimps [equiv_intrel_iff, inj_onto_Abs_Integ RS inj_onto_iff,
+		       intrel_iff, intrel_in_integ, Abs_Integ_inverse];
+
+goal Integ.thy "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 Integ.thy "inj(znat)";
+by (rtac injI 1);
+by (rewtac znat_def);
+by (dtac (inj_onto_Abs_Integ RS inj_ontoD) 1);
+by (REPEAT (rtac intrel_in_integ 1));
+by (dtac eq_equiv_class 1);
+by (rtac equiv_intrel 1);
+by (fast_tac set_cs 1);
+by (safe_tac intrel_cs);
+by (asm_full_simp_tac arith_ss 1);
+qed "inj_znat";
+
+
+(**** zminus: unary negation on Integ ****)
+
+goalw Integ.thy [congruent_def]
+  "congruent intrel (%p. split (%x y. intrel^^{<y,x>}) p)";
+by (safe_tac intrel_cs);
+by (asm_simp_tac (intrel_ss addsimps add_ac) 1);
+qed "zminus_congruent";
+
+
+(*Resolve th against the corresponding facts for zminus*)
+val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
+
+goalw Integ.thy [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 (set_ss addsimps 
+   [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1);
+by (rewtac split_def);
+by (simp_tac prod_ss 1);
+qed "zminus";
+
+(*by lcp*)
+val [prem] = goal Integ.thy
+    "(!!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 (HOL_ss addsimps [Rep_Integ_inverse]) 1);
+qed "eq_Abs_Integ";
+
+goal Integ.thy "$~ ($~ z) = z";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (asm_simp_tac (HOL_ss addsimps [zminus]) 1);
+qed "zminus_zminus";
+
+goal Integ.thy "inj(zminus)";
+by (rtac injI 1);
+by (dres_inst_tac [("f","zminus")] arg_cong 1);
+by (asm_full_simp_tac (HOL_ss addsimps [zminus_zminus]) 1);
+qed "inj_zminus";
+
+goalw Integ.thy [znat_def] "$~ ($#0) = $#0";
+by (simp_tac (arith_ss addsimps [zminus]) 1);
+qed "zminus_0";
+
+
+(**** znegative: the test for negative integers ****)
+
+goal Arith.thy "!!m x n::nat. n+m=x ==> m<=x";
+by (dtac (disjI2 RS less_or_eq_imp_le) 1);
+by (asm_full_simp_tac (arith_ss addsimps add_ac) 1);
+by (dtac add_leD1 1);
+by (assume_tac 1);
+qed "not_znegative_znat_lemma";
+
+
+goalw Integ.thy [znegative_def, znat_def]
+    "~ znegative($# n)";
+by (simp_tac intrel_ss 1);
+by (safe_tac intrel_cs);
+by (rtac ccontr 1);
+by (etac notE 1);
+by (asm_full_simp_tac arith_ss 1);
+by (dtac not_znegative_znat_lemma 1);
+by (fast_tac (HOL_cs addDs [leD]) 1);
+qed "not_znegative_znat";
+
+goalw Integ.thy [znegative_def, znat_def] "znegative($~ $# Suc(n))";
+by (simp_tac (intrel_ss addsimps [zminus]) 1);
+by (REPEAT (ares_tac [exI, conjI] 1));
+by (rtac (intrelI RS ImageI) 2);
+by (rtac singletonI 3);
+by (simp_tac arith_ss 2);
+by (rtac less_add_Suc1 1);
+qed "znegative_zminus_znat";
+
+
+(**** zmagnitude: magnitide of an integer, as a natural number ****)
+
+goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS(asm_simp_tac arith_ss));
+qed "diff_Suc_add_0";
+
+goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS(asm_simp_tac arith_ss));
+qed "diff_Suc_add_inverse";
+
+goalw Integ.thy [congruent_def]
+    "congruent intrel (split (%x y. intrel^^{<(y-x) + (x-(y::nat)),0>}))";
+by (safe_tac intrel_cs);
+by (asm_simp_tac intrel_ss 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1);
+by (asm_simp_tac (arith_ss addsimps [inj_Suc RS inj_eq]) 3);
+by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 2);
+by (asm_simp_tac arith_ss 1);
+by (rtac impI 1);
+by (etac subst 1);
+by (res_inst_tac [("m1","x")] (add_commute RS ssubst) 1);
+by (asm_simp_tac (arith_ss addsimps [diff_add_inverse,diff_add_0]) 1);
+by (rtac impI 1);
+by (asm_simp_tac (arith_ss addsimps
+		  [diff_add_inverse, diff_add_0, diff_Suc_add_0,
+		   diff_Suc_add_inverse]) 1);
+qed "zmagnitude_congruent";
+
+(*Resolve th against the corresponding facts for zmagnitude*)
+val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
+
+
+goalw Integ.thy [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 (intrel_ss addsimps [zmagnitude_ize UN_equiv_class]) 1);
+qed "zmagnitude";
+
+goalw Integ.thy [znat_def] "zmagnitude($# n) = $#n";
+by (asm_simp_tac (intrel_ss addsimps [zmagnitude]) 1);
+qed "zmagnitude_znat";
+
+goalw Integ.thy [znat_def] "zmagnitude($~ $# n) = $#n";
+by (asm_simp_tac (intrel_ss addsimps [zmagnitude, zminus]) 1);
+qed "zmagnitude_zminus_znat";
+
+
+(**** zadd: addition on Integ ****)
+
+(** Congruence property for addition **)
+
+goalw Integ.thy [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 intrel_cs);
+by (asm_simp_tac (intrel_ss 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 (arith_ss addsimps [add_assoc RS sym]) 1);
+by (asm_simp_tac (arith_ss addsimps add_ac) 1);
+qed "zadd_congruent2";
+
+(*Resolve th against the corresponding facts for zadd*)
+val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
+
+goalw Integ.thy [zadd_def]
+  "Abs_Integ(intrel^^{<x1,y1>}) + Abs_Integ(intrel^^{<x2,y2>}) = \
+\  Abs_Integ(intrel^^{<x1+x2, y1+y2>})";
+by (asm_simp_tac
+    (intrel_ss addsimps [zadd_ize UN_equiv_class2]) 1);
+qed "zadd";
+
+goalw Integ.thy [znat_def] "$#0 + z = z";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
+qed "zadd_0";
+
+goal Integ.thy "$~ (z + w) = $~ z + $~ w";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
+by (asm_simp_tac (arith_ss addsimps [zminus,zadd]) 1);
+qed "zminus_zadd_distrib";
+
+goal Integ.thy "(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 (intrel_ss addsimps (add_ac @ [zadd])) 1);
+qed "zadd_commute";
+
+goal Integ.thy "((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 (arith_ss addsimps [zadd, add_assoc]) 1);
+qed "zadd_assoc";
+
+(*For AC rewriting*)
+goal Integ.thy "(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 Integ.thy [znat_def] "$# (m + n) = ($#m) + ($#n)";
+by (asm_simp_tac (arith_ss addsimps [zadd]) 1);
+qed "znat_add";
+
+goalw Integ.thy [znat_def] "z + ($~ z) = $#0";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (asm_simp_tac (intrel_ss addsimps [zminus, zadd, add_commute]) 1);
+qed "zadd_zminus_inverse";
+
+goal Integ.thy "($~ z) + z = $#0";
+by (rtac (zadd_commute RS trans) 1);
+by (rtac zadd_zminus_inverse 1);
+qed "zadd_zminus_inverse2";
+
+goal Integ.thy "z + $#0 = z";
+by (rtac (zadd_commute RS trans) 1);
+by (rtac zadd_0 1);
+qed "zadd_0_right";
+
+
+(*Need properties of subtraction?  Or use $- just as an abbreviation!*)
+
+(**** zmult: multiplication on Integ ****)
+
+(** Congruence property for multiplication **)
+
+goal Integ.thy "((k::nat) + l) + (m + n) = (k + m) + (n + l)";
+by (simp_tac (arith_ss addsimps add_ac) 1);
+qed "zmult_congruent_lemma";
+
+goal Integ.thy 
+    "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 (safe_tac intrel_cs);
+by (rewtac split_def);
+by (simp_tac (arith_ss addsimps add_ac@mult_ac) 1);
+by (asm_simp_tac (arith_ss 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 (HOL_ss addsimps [add_mult_distrib RS sym]) 1);
+by (asm_simp_tac (arith_ss 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 Integ.thy [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 (intrel_ss addsimps [zmult_ize UN_equiv_class2]) 1);
+qed "zmult";
+
+goalw Integ.thy [znat_def] "$#0 * z = $#0";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (asm_simp_tac (arith_ss addsimps [zmult]) 1);
+qed "zmult_0";
+
+goalw Integ.thy [znat_def] "$#Suc(0) * z = z";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (asm_simp_tac (arith_ss addsimps [zmult, add_0_right]) 1);
+qed "zmult_1";
+
+goal Integ.thy "($~ z) * w = $~ (z * w)";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
+by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
+qed "zmult_zminus";
+
+
+goal Integ.thy "($~ z) * ($~ w) = (z * w)";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
+by (asm_simp_tac (intrel_ss addsimps ([zminus, zmult] @ add_ac)) 1);
+qed "zmult_zminus_zminus";
+
+goal Integ.thy "(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 (intrel_ss addsimps ([zmult] @ add_ac @ mult_ac)) 1);
+qed "zmult_commute";
+
+goal Integ.thy "z * $# 0 = $#0";
+by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
+qed "zmult_0_right";
+
+goal Integ.thy "z * $#Suc(0) = z";
+by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
+qed "zmult_1_right";
+
+goal Integ.thy "((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 (intrel_ss addsimps ([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 Integ.thy "((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 
+    (intrel_ss addsimps ([zadd, zmult, add_mult_distrib] @ 
+			 add_ac @ mult_ac)) 1);
+qed "zadd_zmult_distrib";
+
+val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
+
+goal Integ.thy "w * ($~ z) = $~ (w * z)";
+by (simp_tac (HOL_ss addsimps [zmult_commute', zmult_zminus]) 1);
+qed "zmult_zminus_right";
+
+goal Integ.thy "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
+by (simp_tac (HOL_ss addsimps [zmult_commute',zadd_zmult_distrib]) 1);
+qed "zadd_zmult_distrib2";
+
+val zadd_simps = 
+    [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+
+val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib];
+
+val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, 
+		   zmult_zminus, zmult_zminus_right];
+
+val integ_ss =
+    arith_ss addsimps (zadd_simps @ zminus_simps @ zmult_simps @ 
+		       [zmagnitude_znat, zmagnitude_zminus_znat]);
+
+
+(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****)
+
+(* Some Theorems about zsuc and zpred *)
+goalw Integ.thy [zsuc_def] "$#(Suc(n)) = zsuc($# n)";
+by (simp_tac (arith_ss addsimps [znat_add RS sym]) 1);
+qed "znat_Suc";
+
+goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)";
+by (simp_tac integ_ss 1);
+qed "zminus_zsuc";
+
+goalw Integ.thy [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)";
+by (simp_tac integ_ss 1);
+qed "zminus_zpred";
+
+goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
+   "zpred(zsuc(z)) = z";
+by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
+qed "zpred_zsuc";
+
+goalw Integ.thy [zsuc_def,zpred_def,zdiff_def]
+   "zsuc(zpred(z)) = z";
+by (simp_tac (integ_ss addsimps [zadd_assoc]) 1);
+qed "zsuc_zpred";
+
+goal Integ.thy "(zpred(z)=w) = (z=zsuc(w))";
+by (safe_tac HOL_cs);
+by (rtac (zsuc_zpred RS sym) 1);
+by (rtac zpred_zsuc 1);
+qed "zpred_to_zsuc";
+
+goal Integ.thy "(zsuc(z)=w)=(z=zpred(w))";
+by (safe_tac HOL_cs);
+by (rtac (zpred_zsuc RS sym) 1);
+by (rtac zsuc_zpred 1);
+qed "zsuc_to_zpred";
+
+goal Integ.thy "($~ z = w) = (z = $~ w)";
+by (safe_tac HOL_cs);
+by (rtac (zminus_zminus RS sym) 1);
+by (rtac zminus_zminus 1);
+qed "zminus_exchange";
+
+goal Integ.thy"(zsuc(z)=zsuc(w)) = (z=w)";
+by (safe_tac intrel_cs);
+by (dres_inst_tac [("f","zpred")] arg_cong 1);
+by (asm_full_simp_tac (HOL_ss addsimps [zpred_zsuc]) 1);
+qed "bijective_zsuc";
+
+goal Integ.thy"(zpred(z)=zpred(w)) = (z=w)";
+by (safe_tac intrel_cs);
+by (dres_inst_tac [("f","zsuc")] arg_cong 1);
+by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred]) 1);
+qed "bijective_zpred";
+
+(* Additional Theorems about zadd *)
+
+goalw Integ.thy [zsuc_def] "zsuc(z) + w = zsuc(z+w)";
+by (simp_tac (arith_ss addsimps zadd_ac) 1);
+qed "zadd_zsuc";
+
+goalw Integ.thy [zsuc_def] "w + zsuc(z) = zsuc(w+z)";
+by (simp_tac (arith_ss addsimps zadd_ac) 1);
+qed "zadd_zsuc_right";
+
+goalw Integ.thy [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)";
+by (simp_tac (arith_ss addsimps zadd_ac) 1);
+qed "zadd_zpred";
+
+goalw Integ.thy [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)";
+by (simp_tac (arith_ss addsimps zadd_ac) 1);
+qed "zadd_zpred_right";
+
+
+(* Additional Theorems about zmult *)
+
+goalw Integ.thy [zsuc_def] "zsuc(w) * z = z + w * z";
+by (simp_tac (integ_ss addsimps [zadd_zmult_distrib, zadd_commute]) 1);
+qed "zmult_zsuc";
+
+goalw Integ.thy [zsuc_def] "z * zsuc(w) = z + w * z";
+by (simp_tac 
+    (integ_ss addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1);
+qed "zmult_zsuc_right";
+
+goalw Integ.thy [zpred_def, zdiff_def] "zpred(w) * z = w * z - z";
+by (simp_tac (integ_ss addsimps [zadd_zmult_distrib]) 1);
+qed "zmult_zpred";
+
+goalw Integ.thy [zpred_def, zdiff_def] "z * zpred(w) = w * z - z";
+by (simp_tac (integ_ss addsimps [zadd_zmult_distrib2, zmult_commute]) 1);
+qed "zmult_zpred_right";
+
+(* Further Theorems about zsuc and zpred *)
+goal Integ.thy "$#Suc(m) ~= $#0";
+by (simp_tac (integ_ss addsimps [inj_znat RS inj_eq]) 1);
+qed "znat_Suc_not_znat_Zero";
+
+bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym));
+
+
+goalw Integ.thy [zsuc_def,znat_def] "w ~= zsuc(w)";
+by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
+by (asm_full_simp_tac (intrel_ss addsimps [zadd]) 1);
+qed "n_not_zsuc_n";
+
+val zsuc_n_not_n = n_not_zsuc_n RS not_sym;
+
+goal Integ.thy "w ~= zpred(w)";
+by (safe_tac HOL_cs);
+by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1);
+by (asm_full_simp_tac (HOL_ss addsimps [zsuc_zpred,zsuc_n_not_n]) 1);
+qed "n_not_zpred_n";
+
+val zpred_n_not_n = n_not_zpred_n RS not_sym;
+
+
+(* Theorems about less and less_equal *)
+
+goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
+    "!!w. w<z ==> ? 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 (safe_tac intrel_cs);
+by (asm_full_simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
+by (safe_tac (intrel_cs addSDs [less_eq_Suc_add]));
+by (res_inst_tac [("x","k")] exI 1);
+by (asm_full_simp_tac (HOL_ss addsimps ([add_Suc RS sym] @ add_ac)) 1);
+(*To cancel x2, rename it to be first!*)
+by (rename_tac "a b c" 1);
+by (asm_full_simp_tac (HOL_ss addsimps (add_left_cancel::add_ac)) 1);
+qed "zless_eq_zadd_Suc";
+
+goalw Integ.thy [zless_def, znegative_def, zdiff_def, znat_def] 
+    "z < z + $#(Suc(n))";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (safe_tac intrel_cs);
+by (simp_tac (intrel_ss addsimps [zadd, zminus]) 1);
+by (REPEAT_SOME (ares_tac [refl, exI, singletonI, ImageI, conjI, intrelI]));
+by (rtac le_less_trans 1);
+by (rtac lessI 2);
+by (asm_simp_tac (arith_ss addsimps ([le_add1,add_left_cancel_le]@add_ac)) 1);
+qed "zless_zadd_Suc";
+
+goal Integ.thy "!!z1 z2 z3. [| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
+by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (simp_tac 
+    (arith_ss addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1);
+qed "zless_trans";
+
+goalw Integ.thy [zsuc_def] "z<zsuc(z)";
+by (rtac zless_zadd_Suc 1);
+qed "zlessI";
+
+val zless_zsucI = zlessI RSN (2,zless_trans);
+
+goal Integ.thy "!!z w::int. z<w ==> ~w<z";
+by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by (safe_tac intrel_cs);
+by (asm_full_simp_tac (intrel_ss addsimps ([znat_def, zadd])) 1);
+by (asm_full_simp_tac
+ (HOL_ss addsimps [add_left_cancel, add_assoc, add_Suc_right RS sym]) 1);
+by (resolve_tac [less_not_refl2 RS notE] 1);
+by (etac sym 2);
+by (REPEAT (resolve_tac [lessI, trans_less_add2, less_SucI] 1));
+qed "zless_not_sym";
+
+(* [| n<m; m<n |] ==> R *)
+bind_thm ("zless_asym", (zless_not_sym RS notE));
+
+goal Integ.thy "!!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_anti_refl", (zless_not_refl RS notE));
+
+goal Integ.thy "!!w. z<w ==> w ~= (z::int)";
+by(fast_tac (HOL_cs addEs [zless_anti_refl]) 1);
+qed "zless_not_refl2";
+
+
+(*"Less than" is a linear ordering*)
+goalw Integ.thy [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 intrel_cs);
+by (asm_full_simp_tac
+    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
+by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
+by (etac disjE 2);
+by (assume_tac 2);
+by (DEPTH_SOLVE
+    (swap_res_tac [exI] 1 THEN 
+     swap_res_tac [exI] 1 THEN 
+     etac conjI 1 THEN 
+     simp_tac (arith_ss addsimps add_ac)  1));
+qed "zless_linear";
+
+
+(*** Properties of <= ***)
+
+goalw Integ.thy  [zless_def, znegative_def, zdiff_def, znat_def]
+    "($#m < $#n) = (m<n)";
+by (simp_tac
+    (intrel_ss addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
+by (fast_tac (HOL_cs addIs [add_commute] addSEs [less_add_eq_less]) 1);
+qed "zless_eq_less";
+
+goalw Integ.thy [zle_def, le_def] "($#m <= $#n) = (m<=n)";
+by (simp_tac (HOL_ss addsimps [zless_eq_less]) 1);
+qed "zle_eq_le";
+
+goalw Integ.thy [zle_def] "!!w. ~(w<z) ==> z<=(w::int)";
+by (assume_tac 1);
+qed "zleI";
+
+goalw Integ.thy [zle_def] "!!w. z<=w ==> ~(w<(z::int))";
+by (assume_tac 1);
+qed "zleD";
+
+val zleE = make_elim zleD;
+
+goalw Integ.thy [zle_def] "!!z. ~ z <= w ==> w<(z::int)";
+by (fast_tac HOL_cs 1);
+qed "not_zleE";
+
+goalw Integ.thy [zle_def] "!!z. z < w ==> z <= (w::int)";
+by (fast_tac (HOL_cs addEs [zless_asym]) 1);
+qed "zless_imp_zle";
+
+goalw Integ.thy [zle_def] "!!z. z <= w ==> z < w | z=(w::int)";
+by (cut_facts_tac [zless_linear] 1);
+by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
+qed "zle_imp_zless_or_eq";
+
+goalw Integ.thy [zle_def] "!!z. z<w | z=w ==> z <=(w::int)";
+by (cut_facts_tac [zless_linear] 1);
+by (fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym]) 1);
+qed "zless_or_eq_imp_zle";
+
+goal Integ.thy "(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 Integ.thy "w <= (w::int)";
+by (simp_tac (HOL_ss addsimps [zle_eq_zless_or_eq]) 1);
+qed "zle_refl";
+
+val prems = goal Integ.thy "!!i. [| i <= j; j < k |] ==> i < (k::int)";
+by (dtac zle_imp_zless_or_eq 1);
+by (fast_tac (HOL_cs addIs [zless_trans]) 1);
+qed "zle_zless_trans";
+
+goal Integ.thy "!!i. [| 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, fast_tac (HOL_cs addIs [zless_trans])]);
+qed "zle_trans";
+
+goal Integ.thy "!!z. [| z <= w; w <= z |] ==> z = (w::int)";
+by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
+	    fast_tac (HOL_cs addEs [zless_anti_refl,zless_asym])]);
+qed "zle_anti_sym";
+
+
+goal Integ.thy "!!w w' z::int. z + w' = z + w ==> w' = w";
+by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1);
+by (asm_full_simp_tac (integ_ss addsimps zadd_ac) 1);
+qed "zadd_left_cancel";
+
+
+(*** Monotonicity results ***)
+
+goal Integ.thy "!!v w z::int. v < w ==> v + z < w + z";
+by (safe_tac (HOL_cs addSDs [zless_eq_zadd_Suc]));
+by (simp_tac (HOL_ss addsimps zadd_ac) 1);
+by (simp_tac (HOL_ss addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1);
+qed "zadd_zless_mono1";
+
+goal Integ.thy "!!v w z::int. (v+z < w+z) = (v < w)";
+by (safe_tac (HOL_cs addSEs [zadd_zless_mono1]));
+by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1);
+by (asm_full_simp_tac (integ_ss addsimps [zadd_assoc]) 1);
+qed "zadd_left_cancel_zless";
+
+goal Integ.thy "!!v w z::int. (v+z <= w+z) = (v <= w)";
+by (asm_full_simp_tac
+    (integ_ss addsimps [zle_def, zadd_left_cancel_zless]) 1);
+qed "zadd_left_cancel_zle";
+
+(*"v<=w ==> v+z <= w+z"*)
+bind_thm ("zadd_zle_mono1", zadd_left_cancel_zle RS iffD2);
+
+
+goal Integ.thy "!!z' z::int. [| w'<=w; z'<=z |] ==> w' + z' <= w + z";
+by (etac (zadd_zle_mono1 RS zle_trans) 1);
+by (simp_tac (HOL_ss addsimps [zadd_commute]) 1);
+(*w moves to the end because it is free while z', z are bound*)
+by (etac zadd_zle_mono1 1);
+qed "zadd_zle_mono";
+
+goal Integ.thy "!!w z::int. z<=$#0 ==> w+z <= w";
+by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1);
+by (asm_full_simp_tac (integ_ss addsimps [zadd_commute]) 1);
+qed "zadd_zle_self";
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Integ.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Integ.thy	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,80 @@
+(*  Title: 	Integ.thy
+    ID:         $Id$
+    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+*)
+
+Integ = Equiv + Arith +
+consts
+  intrel      :: "((nat * nat) * (nat * nat)) set"
+
+defs
+  intrel_def
+   "intrel == {p. ? x1 y1 x2 y2. p=<<x1::nat,y1>,<x2,y2>> & x1+y2 = x2+y1}"
+
+subtype (Integ)
+  int = "{x::(nat*nat).True}/intrel"		("quotient_def")
+
+arities int :: ord
+        int :: plus
+        int :: times
+        int :: minus
+consts
+  zNat        :: "nat set"
+  znat	      :: "nat => int"	   ("$# _" [80] 80)
+  zminus      :: "int => int"	   ("$~ _" [80] 80)
+  znegative   :: "int => bool"
+  zmagnitude  :: "int => int"
+  zdiv,zmod   :: "[int,int]=>int"  (infixl 70)
+  zpred,zsuc  :: "int=>int"
+
+defs
+  zNat_def    "zNat == {x::nat. True}"
+
+  znat_def    "$# m == Abs_Integ(intrel ^^ {<m,0>})"
+
+  zminus_def
+	"$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{<y,x>}) p)"
+
+  znegative_def
+      "znegative(Z) == EX x y. x<y & <x,y::nat>:Rep_Integ(Z)"
+
+  zmagnitude_def
+      "zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).split (%x y. intrel^^{<(y-x) + (x-y),0>}) p)"
+
+  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 + zminus(Z2)"
+
+  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)"
+
+  zdiv_def
+   "Z1 zdiv Z2 ==   \
+\       Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1.   \
+\           split (%x2 y2. intrel^^{<(x1-y1)div(x2-y2)+(y1-x1)div(y2-x2),   \
+\           (x1-y1)div(y2-x2)+(y1-x1)div(x2-y2)>}) p2) p1)"
+
+  zmod_def
+   "Z1 zmod Z2 ==   \
+\       Abs_Integ(UN p1:Rep_Integ(Z1).UN p2:Rep_Integ(Z2).split (%x1 y1.   \
+\           split (%x2 y2. intrel^^{<(x1-y1)mod((x2-y2)+(y2-x2)),   \
+\           (x1-y1)mod((x2-y2)+(x2-y2))>}) p2) p1)"
+
+  zsuc_def     "zsuc(Z) == Z + $# Suc(0)"
+
+  zpred_def    "zpred(Z) == Z - $# Suc(0)"
+end
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/ROOT.ML	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,12 @@
+(*  Title:  	CHOL/Integ/ROOT
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1995  University of Cambridge
+
+The Integers in CHOL (ported from ZF by Riccardo Mattolini)
+*)
+
+CHOL_build_completed;    (*Cause examples to fail if CHOL did*)
+
+loadpath := ["Integ"];
+time_use_thy "Integ" handle _ => exit 1;
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Relation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Relation.ML	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,98 @@
+(*  Title: 	Relation.ML
+    ID:         $Id$
+    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+Functions represented as relations in HOL Set Theory 
+*)
+
+val RSLIST = curry (op MRS);
+
+open Relation;
+
+goalw Relation.thy [converse_def] "!!a b r. <a,b>:r ==> <b,a>:converse(r)";
+by (simp_tac prod_ss 1);
+by (fast_tac set_cs 1);
+qed "converseI";
+
+goalw Relation.thy [converse_def] "!!a b r. <a,b> : converse(r) ==> <b,a> : r";
+by (fast_tac comp_cs 1);
+qed "converseD";
+
+qed_goalw "converseE" Relation.thy [converse_def]
+    "[| yx : converse(r);  \
+\       !!x y. [| yx=<y,x>;  <x,y>:r |] ==> P \
+\    |] ==> P"
+ (fn [major,minor]=>
+  [ (rtac (major RS CollectE) 1),
+    (REPEAT (eresolve_tac [bexE,exE, conjE, minor] 1)),
+    (hyp_subst_tac 1),
+    (assume_tac 1) ]);
+
+val converse_cs = comp_cs addSIs [converseI] 
+			  addSEs [converseD,converseE];
+
+qed_goalw "Domain_iff" Relation.thy [Domain_def]
+    "a: Domain(r) = (EX y. <a,y>: r)"
+ (fn _=> [ (fast_tac comp_cs 1) ]);
+
+qed_goal "DomainI" Relation.thy "!!a b r. <a,b>: r ==> a: Domain(r)"
+ (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
+
+qed_goal "DomainE" Relation.thy
+    "[| a : Domain(r);  !!y. <a,y>: r ==> P |] ==> P"
+ (fn prems=>
+  [ (rtac (Domain_iff RS iffD1 RS exE) 1),
+    (REPEAT (ares_tac prems 1)) ]);
+
+qed_goalw "RangeI" Relation.thy [Range_def] "!!a b r.<a,b>: r ==> b : Range(r)"
+ (fn _ => [ (etac (converseI RS DomainI) 1) ]);
+
+qed_goalw "RangeE" Relation.thy [Range_def]
+    "[| b : Range(r);  !!x. <x,b>: r ==> P |] ==> P"
+ (fn major::prems=>
+  [ (rtac (major RS DomainE) 1),
+    (resolve_tac prems 1),
+    (etac converseD 1) ]);
+
+(*** Image of a set under a function/relation ***)
+
+qed_goalw "Image_iff" Relation.thy [Image_def]
+    "b : r^^A = (? x:A. <x,b>:r)"
+ (fn _ => [ fast_tac (comp_cs addIs [RangeI]) 1 ]);
+
+qed_goal "Image_singleton_iff" Relation.thy
+    "(b : r^^{a}) = (<a,b>:r)"
+ (fn _ => [ rtac (Image_iff RS trans) 1,
+	    fast_tac comp_cs 1 ]);
+
+qed_goalw "ImageI" Relation.thy [Image_def]
+    "!!a b r. [| <a,b>: r;  a:A |] ==> b : r^^A"
+ (fn _ => [ (REPEAT (ares_tac [CollectI,RangeI,bexI] 1)),
+            (resolve_tac [conjI ] 1),
+            (resolve_tac [RangeI] 1),
+            (REPEAT (fast_tac set_cs 1))]);
+
+qed_goalw "ImageE" Relation.thy [Image_def]
+    "[| b: r^^A;  !!x.[| <x,b>: r;  x:A |] ==> P |] ==> P"
+ (fn major::prems=>
+  [ (rtac (major RS CollectE) 1),
+    (safe_tac set_cs),
+    (etac RangeE 1),
+    (rtac (hd prems) 1),
+    (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
+
+qed_goal "Image_subset" Relation.thy
+    "!!A B r. r <= Sigma A (%x.B) ==> r^^C <= B"
+ (fn _ =>
+  [ (rtac subsetI 1),
+    (REPEAT (eresolve_tac [asm_rl, ImageE, subsetD RS SigmaD2] 1)) ]);
+
+val rel_cs = converse_cs addSIs [converseI] 
+                         addIs  [ImageI, DomainI, RangeI]
+                         addSEs [ImageE, DomainE, RangeE];
+
+val rel_eq_cs = rel_cs addSIs [equalityI];
+
diff -r 806721cfbf46 -r 15539deb6863 src/HOL/Integ/Relation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/Relation.thy	Fri Mar 03 12:04:45 1995 +0100
@@ -0,0 +1,24 @@
+(*  Title: 	Relation.thy
+    ID:         $Id$
+    Author: 	Riccardo Mattolini, Dip. Sistemi e Informatica
+        and	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1994 Universita' di Firenze
+    Copyright   1993  University of Cambridge
+
+Functions represented as relations in Higher-Order Set Theory 
+*)
+
+Relation = Trancl +
+consts
+    converse    ::      "('a*'a) set => ('a*'a) set"
+    "^^"        ::      "[('a*'a) set,'a set] => 'a set" (infixl 90)
+    Domain      ::      "('a*'a) set => 'a set"
+    Range       ::      "('a*'a) set => 'a set"
+
+defs
+    converse_def  "converse(r) == {z. (? w:r. ? x y. w=<x,y> & z=<y,x>)}"
+    Domain_def    "Domain(r) == {z. ! x. (z=x --> (? y. <x,y>:r))}"
+    Range_def     "Range(r) == Domain(converse(r))"
+    Image_def     "r ^^ s == {y. y:Range(r) &  (? x:s. <x,y>:r)}"
+
+end