author paulson Fri, 18 Sep 1998 16:04:00 +0200 changeset 5508 691c70898518 parent 5507 2fd99b2d41e1 child 5509 c38cc427976c
new files in Integ
 src/HOL/Integ/IntDef.ML file | annotate | diff | comparison | revisions src/HOL/Integ/IntDef.thy file | annotate | diff | comparison | revisions
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntDef.ML	Fri Sep 18 16:04:00 1998 +0200
@@ -0,0 +1,652 @@
+(*  Title:      IntDef.ML
+    ID:         \$Id\$
+    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+*)
+
+
+(*** 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);
+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";
+
+
+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";
+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";
+
+          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;
+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);
+   [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";
+
+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";
+
+
+
+(**** znegative: the test for negative integers ****)
+
+
+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";
+
+
+
+
+(** 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;
+(*The rest should be trivial, but rearranging terms is hard*)
+by (res_inst_tac [("x1","x1a")] (add_left_commute RS ssubst) 1);
+
+(*Resolve th against the corresponding facts for zadd*)
+
+  "Abs_Integ(intrel^^{(x1,y1)}) + Abs_Integ(intrel^^{(x2,y2)}) = \
+\  Abs_Integ(intrel^^{(x1+x2, y1+y2)})";
+by (asm_simp_tac
+
+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);
+
+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);
+
+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);
+
+(*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);
+
+(*Integer addition is an AC operator*)
+
+Goalw [znat_def] "(\$#m) + (\$#n) = \$# (m + n)";
+
+Goal "\$# (Suc m) = \$# 1 + (\$# m)";
+qed "znat_Suc";
+
+Goalw [znat_def] "\$# 0 + z = z";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+
+Goal "z + \$# 0 = z";
+by (rtac (zadd_commute RS trans) 1);
+
+Goalw [znat_def] "z + (- z) = \$# 0";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+
+Goal "(- z) + z = \$# 0";
+by (rtac (zadd_commute RS trans) 1);
+
+
+Goal "z + (- z + w) = (w::int)";
+
+Goal "(-z) + (z + w) = (w::int)";
+
+
+
+(** Lemmas **)
+
+Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
+
+Goal "(z::int) + (v + w) = v + (z + w)";
+
+
+(*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)";
+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 (asm_simp_tac (simpset() delsimps [equiv_intrel_iff]
+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);
+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);
+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);
+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);
+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);
+qed "zmult_assoc";
+
+(*For AC rewriting*)
+Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
+by (rtac (zmult_commute RS trans) 1);
+by (rtac (zmult_assoc RS trans) 1);
+by (rtac (zmult_commute RS arg_cong) 1);
+qed "zmult_left_commute";
+
+(*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
+
+
+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)";
+
+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";
+
+
+
+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 (res_inst_tac [("x","k")] exI 1);
+
+Goal "z < z + \$# (Suc n)";
+by (auto_tac (claset(),
+
+Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
+by (auto_tac (claset(),
+qed "zless_trans";
+
+Goal "!!w::int. z<w ==> ~w<z";
+by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
+by Safe_tac;
+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));
+
+Goal "z<w ==> w ~= (z::int)";
+by (Blast_tac 1);
+qed "zless_not_refl2";
+
+(* s < t ==> s ~= t *)
+bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym);
+
+
+(*"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
+by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
+qed "zless_linear";
+
+Goal "!!w::int. (w ~= z) = (w<z | z<w)";
+by (cut_facts_tac [zless_linear] 1);
+by (Blast_tac 1);
+qed "int_neq_iff";
+
+(*** eliminates ~= in premises ***)
+bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
+
+Goal "(\$# m = \$# n) = (m = n)";
+by (fast_tac (claset() addSEs [inj_znat RS injD]) 1);
+qed "znat_znat_eq";
+
+Goal "(\$#m < \$#n) = (m<n)";
+qed "zless_eq_less";
+
+
+(*** Properties of <= ***)
+
+Goalw [zle_def, le_def] "(\$#m <= \$#n) = (m<=n)";
+by (Simp_tac 1);
+qed "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";
+
+(*  [| z <= w;  ~ P ==> w < z |] ==> P  *)
+bind_thm ("zleE", zleD RS swap);
+
+Goalw [zle_def] "(~w<=z) = (z<(w::int))";
+by (Simp_tac 1);
+qed "not_zle_iff_zless";
+
+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";
+
+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";
+
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+Goal "(z::int) <= w | w <= z";
+by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
+by (cut_facts_tac [zless_linear] 1);
+by (Blast_tac 1);
+qed "zle_linear";
+
+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,
+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,
+qed "zle_anti_sym";
+
+(* Axiom 'order_less_le' of class 'order': *)
+Goal "(w::int) < z = (w <= z & w ~= z)";
+by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
+by (blast_tac (claset() addSEs [zless_asym]) 1);
+qed "int_less_le";
+
+(* [| w <= z; w ~= z |] ==> w < z *)
+bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2);
+
+
+
+(*** Subtraction laws ***)
+
+Goal "x + (y - z) = (x + y) - (z::int)";
+
+Goal "(x - y) + z = (x + z) - (y::int)";
+
+Goal "(x - y) - z = x - (y + (z::int))";
+qed "zdiff_zdiff_eq";
+
+Goal "x - (y - z) = (x + z) - (y::int)";
+qed "zdiff_zdiff_eq2";
+
+Goalw [zless_def, zdiff_def] "(x-y < z) = (x < z + (y::int))";
+qed "zdiff_zless_eq";
+
+Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)";
+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))";
+qed "zdiff_eq_eq";
+
+Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
+qed "eq_zdiff_eq";
+
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+  to the top and then moving negative terms to the other side.
+val zcompare_rls =
+    [symmetric zdiff_def,
+     zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq,
+     zdiff_eq_eq, eq_zdiff_eq];
+
+
+(** Cancellation laws **)
+
+Goal "!!w::int. (z + w' = z + w) = (w' = w)";
+by Safe_tac;
+by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1);
+
+
+Goal "!!z::int. (w' + z = w + z) = (w' = w)";
+
+
+
+Goal "(w < z + \$# 1) = (w<z | w=z)";
+by (auto_tac (claset(),
+by (cut_inst_tac [("m","n")] znat_Suc 1);
+by (exhaust_tac "n" 1);
+auto();
+
+
+Goal "(w + \$# 1 <= z) = (w<z)";
```--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntDef.thy	Fri Sep 18 16:04:00 1998 +0200
@@ -0,0 +1,53 @@
+(*  Title:      IntDef.thy
+    ID:         \$Id\$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1996  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+*)
+
+IntDef = 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}"
+
+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)"
+
+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)"
+
+  (*For simplifying equalities*)
+  iszero :: int => bool
+  "iszero z == z = \$# 0"
+
+defs
+   "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)"
+
+end```