author paulson Fri, 18 Sep 1998 15:15:40 +0200 changeset 5507 2fd99b2d41e1 parent 5506 e07254044384 child 5508 691c70898518
simpler definition of zmagnitude, and new thms for it
 src/ZF/ex/Integ.ML file | annotate | diff | comparison | revisions src/ZF/ex/Integ.thy file | annotate | diff | comparison | revisions
```--- 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;

(*** 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);
+
+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";

+
+Goal "m: nat ==> (\$# m = \$# n) <-> (m = n)";
+by (Blast_tac 1);
+qed "znat_znat_eq";

(**** zminus: unary negation on integ ****)

@@ -126,6 +134,8 @@
by (simp_tac (simpset() addsimps [zminus]) 1);
qed "zminus_0";

+

(**** znegative: the test for negative integers ****)

@@ -138,56 +148,77 @@
qed "not_znegative_znat";

+
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";

+
+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*)
-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));
-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";
+qed "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;
+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";
+

-(*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,
-qed "zmagnitude_type";
+Goalw [integ_def, znegative_def, znat_def]
+     "[| z: integ; znegative(z) |] ==> EX n:nat. z = \$~ (\$# succ(n))";
+by (rename_tac "m n j k" 1);
+by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
+by (rotate_tac ~2 2);
+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";

@@ -277,6 +308,8 @@
by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1));

+

(*Need properties of \$- ???  Or use \$- just as an abbreviation?
[| m: nat;  n: nat;  m>=n |] ==> \$# (m #- n) = (\$#m) \$- (\$#n)
@@ -333,6 +366,8 @@
qed "zmult_zminus";

+
Goalw [integ_def] "[| z: integ;  w: integ |] ==> (\$~ z) \$* (\$~ w) = (z \$* w)";
by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
@@ -373,10 +408,5 @@

-

```--- a/src/ZF/ex/Integ.thy	Fri Sep 18 15:11:05 1998 +0200