# HG changeset patch
# User paulson
# Date 906124540 -7200
# Node ID 2fd99b2d41e1764f888c1184a7d67474ac5aa57e
# Parent  e07254044384fac67733bb276920a6260626ce93
simpler definition of zmagnitude, and new thms for it

diff -r e07254044384 -r 2fd99b2d41e1 src/ZF/ex/Integ.ML
--- a/src/ZF/ex/Integ.ML	Fri Sep 18 15:11:05 1998 +0200
+++ b/src/ZF/ex/Integ.ML	Fri Sep 18 15:15:40 1998 +0200
@@ -12,7 +12,7 @@
 $+ and $* are monotonic wrt $<
 *)
 
-open Integ;
+AddSEs [quotientE];
 
 (*** Proving that intrel is an equivalence relation ***)
 
@@ -82,12 +82,20 @@
 by (fast_tac (claset() addSIs [nat_0I]) 1);
 qed "znat_type";
 
-Goalw [znat_def] "[| $#m = $#n;  n: nat |] ==> m=n";
-by (dtac eq_intrelD 1);
+Addsimps [znat_type];
+
+Goalw [znat_def] "[| $#m = $#n;  m: nat |] ==> m=n";
+by (dtac (sym RS eq_intrelD) 1);
 by (typechk_tac [nat_0I, SigmaI]);
 by (Asm_full_simp_tac 1);
 qed "znat_inject";
 
+AddSDs [znat_inject];
+
+Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
+by (Blast_tac 1); 
+qed "znat_znat_eq"; 
+Addsimps [znat_znat_eq]; 
 
 (**** zminus: unary negation on integ ****)
 
@@ -126,6 +134,8 @@
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_0";
 
+Addsimps [zminus_zminus, zminus_0];
+
 
 (**** znegative: the test for negative integers ****)
 
@@ -138,56 +148,77 @@
               (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1);
 qed "not_znegative_znat";
 
+Addsimps [not_znegative_znat];
+AddSEs   [not_znegative_znat RS notE];
+
 Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
 by (asm_simp_tac (simpset() addsimps [zminus]) 1);
 by (blast_tac (claset() addIs [nat_0_le]) 1);
 qed "znegative_zminus_znat";
 
+Addsimps [znegative_zminus_znat];
+
+Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
+by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
+be natE 1;
+by (dres_inst_tac [("x","0")] spec 2);
+by Auto_tac;
+qed "not_znegative_imp_zero";
 
 (**** zmagnitude: magnitide of an integer, as a natural number ****)
 
-Goalw [congruent_def] "congruent(intrel, %<x,y>. (y#-x) #+ (x#-y))";
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-by (etac rev_mp 1);
-by (res_inst_tac [("m","x1"),("n","y1")] diff_induct 1 THEN 
-    REPEAT (assume_tac 1));
-by (Asm_simp_tac 3);
-by (asm_simp_tac  (*this one's very sensitive to order of rewrites*)
-    (simpset() delsimps [add_succ_right] 
-              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 THEN
-    REPEAT (assume_tac 1));
-by (asm_simp_tac (simpset() addsimps [diff_add_inverse, diff_add_0]) 1);
-qed "zmagnitude_congruent";
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
+by Auto_tac;
+qed "zmagnitude_znat";
+
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
+by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
+qed "zmagnitude_zminus_znat";
+
+Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
+
+Goalw [zmagnitude_def] "zmagnitude(z) : nat";
+br theI2 1;
+by Auto_tac;
+qed "zmagnitude_type";
+
+Goalw [integ_def, znegative_def, znat_def]
+     "[| z: integ; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
+by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
+by (rename_tac "i j" 1);
+by (dres_inst_tac [("x", "i")] spec 1);
+by (dres_inst_tac [("x", "j")] spec 1);
+br bexI 1;
+br (add_diff_inverse2 RS sym) 1;
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
+qed "not_zneg_znat";
+
+Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
+bd not_zneg_znat 1;
+by Auto_tac;
+qed "not_zneg_mag"; 
+
+Addsimps [not_zneg_mag];
 
 
-(*Resolve th against the corresponding facts for zmagnitude*)
-val zmagnitude_ize = RSLIST [equiv_intrel, zmagnitude_congruent];
-
-Goalw [integ_def,zmagnitude_def]
-    "z : integ ==> zmagnitude(z) : nat";
-by (typechk_tac [split_type, zmagnitude_ize UN_equiv_class_type,
-                 add_type, diff_type]);
-qed "zmagnitude_type";
+Goalw [integ_def, znegative_def, znat_def]
+     "[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
+by (auto_tac(claset() addSDs [less_imp_Suc_add], 
+	     simpset() addsimps [zminus, image_singleton_iff]));
+by (rename_tac "m n j k" 1);
+by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
+by (rotate_tac ~2 2);
+by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
+by (blast_tac (claset() addSDs [add_left_cancel]) 1);
+qed "zneg_znat";
 
-Goalw [zmagnitude_def]
-    "[| x: nat;  y: nat |]  \
-\    ==> zmagnitude (intrel``{<x,y>}) = (y #- x) #+ (x #- y)";
-by (asm_simp_tac
-    (simpset() addsimps [zmagnitude_ize UN_equiv_class, SigmaI]) 1);
-qed "zmagnitude";
+Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
+bd zneg_znat 1;
+by Auto_tac;
+qed "zneg_mag"; 
 
-Goalw [znat_def] "n: nat ==> zmagnitude($# n) = n";
-by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1);
-qed "zmagnitude_znat";
-
-Goalw [znat_def] "n: nat ==> zmagnitude($~ $# n) = n";
-by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1);
-qed "zmagnitude_zminus_znat";
+Addsimps [zneg_mag];
 
 
 (**** zadd: addition on integ ****)
@@ -277,6 +308,8 @@
 by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1));
 qed "zadd_0_right";
 
+Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+
 
 (*Need properties of $- ???  Or use $- just as an abbreviation?
      [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
@@ -333,6 +366,8 @@
 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
 qed "zmult_zminus";
 
+Addsimps [zmult_0, zmult_1, zmult_zminus];
+
 Goalw [integ_def] "[| z: integ;  w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
 by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
 by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1);
@@ -373,10 +408,5 @@
 
 Addsimps integ_typechecks;
 
-Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
-
-Addsimps [zminus_zminus, zminus_0];
 
-Addsimps [zmult_0, zmult_1, zmult_zminus];
 
-Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
diff -r e07254044384 -r 2fd99b2d41e1 src/ZF/ex/Integ.thy
--- a/src/ZF/ex/Integ.thy	Fri Sep 18 15:11:05 1998 +0200
+++ b/src/ZF/ex/Integ.thy	Fri Sep 18 15:15:40 1998 +0200
@@ -36,7 +36,9 @@
         "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
     
     zmagnitude_def
-        "zmagnitude(Z) == UN <x,y>:Z. (y#-x) #+ (x#-y)"
+        "zmagnitude(Z) ==
+	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
+	                   (znegative(Z) & $~ Z = $# m))"
     
     (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
       Perhaps a "curried" or even polymorphic congruent predicate would be