--- a/src/ZF/Integ/Int.ML Wed Aug 02 16:06:54 2000 +0200
+++ b/src/ZF/Integ/Int.ML Wed Aug 02 16:07:32 2000 +0200
@@ -25,8 +25,8 @@
qed "intrel_iff";
Goalw [intrel_def]
- "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
-\ <<x1,y1>,<x2,y2>>: intrel";
+ "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] \
+\ ==> <<x1,y1>,<x2,y2>>: intrel";
by (fast_tac (claset() addIs prems) 1);
qed "intrelI";
@@ -66,6 +66,11 @@
qed "equiv_intrel";
+Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
+by (blast_tac (claset() addIs [quotientI]) 1);
+qed "image_intrel_int";
+
+
Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
add_0_right, add_succ_right];
Addcongs [conj_cong];
@@ -74,25 +79,78 @@
(** int_of: the injection from nat to int **)
-Goalw [int_def,quotient_def,int_of_def]
- "m : nat ==> $#m : int";
+Goalw [int_def,quotient_def,int_of_def] "$#m : int";
by Auto_tac;
qed "int_of_type";
-Addsimps [int_of_type];
-AddTCs [int_of_type];
+AddIffs [int_of_type];
+AddTCs [int_of_type];
+
-Goalw [int_of_def] "[| $#m = $#n; m: nat |] ==> m=n";
-by (dtac (sym RS eq_intrelD) 1);
+Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)";
+by Auto_tac;
+qed "int_of_eq";
+AddIffs [int_of_eq];
+
+Goal "[| $#m = $#n; m: nat; n: nat |] ==> m=n";
+by (dtac (int_of_eq RS iffD1) 1);
by Auto_tac;
qed "int_of_inject";
-AddSDs [int_of_inject];
+
+(** intify: coercion from anything to int **)
+
+Goal "intify(x) : int";
+by (simp_tac (simpset() addsimps [intify_def]) 1);
+qed "intify_in_int";
+AddIffs [intify_in_int];
+AddTCs [intify_in_int];
+
+Goal "n : int ==> intify(n) = n";
+by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
+qed "intify_ident";
+Addsimps [intify_ident];
+
+
+(*** Collapsing rules: to remove intify from arithmetic expressions ***)
+
+Goal "intify(intify(x)) = intify(x)";
+by (Simp_tac 1);
+qed "intify_idem";
+Addsimps [intify_idem];
+
+Goal "$# (natify(m)) = $# m";
+by (simp_tac (simpset() addsimps [int_of_def]) 1);
+qed "int_of_natify";
-Goal "m: nat ==> ($# m = $# n) <-> (m = n)";
-by (Blast_tac 1);
-qed "int_of_eq";
-Addsimps [int_of_eq];
+Goal "$~ (intify(m)) = $~ m";
+by (simp_tac (simpset() addsimps [zminus_def]) 1);
+qed "zminus_intify";
+
+Addsimps [int_of_natify, zminus_intify];
+
+(** Addition **)
+
+Goal "intify(x) $+ y = x $+ y";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+qed "zadd_intify1";
+
+Goal "x $+ intify(y) = x $+ y";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+qed "zadd_intify2";
+Addsimps [zadd_intify1, zadd_intify2];
+
+(** Multiplication **)
+
+Goal "intify(x) $* y = x $* y";
+by (simp_tac (simpset() addsimps [zmult_def]) 1);
+qed "zmult_intify1";
+
+Goal "x $* intify(y) = x $* y";
+by (simp_tac (simpset() addsimps [zmult_def]) 1);
+qed "zmult_intify2";
+Addsimps [zmult_intify1, zmult_intify2];
+
(**** zminus: unary negation on int ****)
@@ -106,34 +164,64 @@
(*Resolve th against the corresponding facts for zminus*)
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
-Goalw [int_def,zminus_def] "z : int ==> $~z : int";
+Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
+qed "raw_zminus_type";
+
+Goalw [zminus_def] "$~z : int";
+by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
qed "zminus_type";
+AddIffs [zminus_type];
AddTCs [zminus_type];
-Goalw [int_def,zminus_def] "[| $~z = $~w; z: int; w: int |] ==> z=w";
+
+Goalw [int_def,raw_zminus_def]
+ "[| raw_zminus(z) = raw_zminus(w); z: int; w: int |] ==> z=w";
by (etac (zminus_ize UN_equiv_class_inject) 1);
by Safe_tac;
-(*The setloop is only needed because assumptions are in the wrong order!*)
-by (asm_full_simp_tac (simpset() addsimps add_ac
- setloop dtac eq_intrelD) 1);
+by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));
+qed "raw_zminus_inject";
+
+Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
+by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
+qed "zminus_inject_intify";
+
+AddSDs [zminus_inject_intify];
+
+Goal "[| $~z = $~w; z: int; w: int |] ==> z=w";
+by Auto_tac;
qed "zminus_inject";
+Goalw [raw_zminus_def]
+ "[| x: nat; y: nat |] \
+\ ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+qed "raw_zminus";
+
Goalw [zminus_def]
- "[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+ "[| x: nat; y: nat |] \
+\ ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
qed "zminus";
-Goalw [int_def] "z : int ==> $~ ($~ z) = z";
-by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_zminus";
+Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zminus]));
+qed "raw_zminus_zminus";
-Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
+Goal "$~ ($~ z) = intify(z)";
+by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type,
+ raw_zminus_zminus]) 1);
+qed "zminus_zminus_intify";
+
+Goalw [int_of_def] "$~ ($#0) = $#0";
by (simp_tac (simpset() addsimps [zminus]) 1);
qed "zminus_0";
-Addsimps [zminus_zminus, zminus_0];
+Addsimps [zminus_zminus_intify, zminus_0];
+
+Goal "z : int ==> $~ ($~ z) = z";
+by (Asm_simp_tac 1);
+qed "zminus_zminus";
(**** znegative: the test for negative integers ****)
@@ -150,28 +238,37 @@
Addsimps [not_znegative_int_of];
AddSEs [not_znegative_int_of RS notE];
-Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
+Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
by (asm_simp_tac (simpset() addsimps [zminus]) 1);
by (blast_tac (claset() addIs [nat_0_le]) 1);
qed "znegative_zminus_int_of";
Addsimps [znegative_zminus_int_of];
-Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
+Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
-by (etac natE 1);
-by (dres_inst_tac [("x","0")] spec 2);
-by Auto_tac;
+by (dres_inst_tac [("x","0")] spec 1);
+by (auto_tac(claset(),
+ simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
qed "not_znegative_imp_zero";
(**** zmagnitude: magnitide of an integer, as a natural number ****)
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
-by Auto_tac;
+Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
+by (auto_tac (claset(), simpset() addsimps [int_of_eq]));
qed "zmagnitude_int_of";
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
-by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
+Goal "natify(x)=n ==> $#x = $# n";
+by (dtac sym 1);
+by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
+qed "natify_int_of_eq";
+
+Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
+by (rtac the_equality 1);
+by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq],
+ simpset())
+ delIffs [int_of_eq]));
+by Auto_tac;
qed "zmagnitude_zminus_int_of";
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
@@ -242,46 +339,74 @@
(*Resolve th against the corresponding facts for zadd*)
val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
-Goalw [int_def,zadd_def] "[| z: int; w: int |] ==> z $+ w : int";
+Goalw [int_def,raw_zadd_def] "[| z: int; w: int |] ==> raw_zadd(z,w) : int";
by (rtac (zadd_ize UN_equiv_class_type2) 1);
by (simp_tac (simpset() addsimps [Let_def]) 3);
-by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
-qed "zadd_type";
-AddTCs [zadd_type];
+by (REPEAT (assume_tac 1));
+qed "raw_zadd_type";
-Goalw [zadd_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
-\ (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#+x2, y1#+y2>}";
+Goal "z $+ w : int";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
+qed "zadd_type";
+AddIffs [zadd_type]; AddTCs [zadd_type];
+
+Goalw [raw_zadd_def]
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
+\ ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) = \
+\ intrel `` {<x1#+x2, y1#+y2>}";
by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
by (simp_tac (simpset() addsimps [Let_def]) 1);
+qed "raw_zadd";
+
+Goalw [zadd_def]
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
+\ ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = \
+\ intrel `` {<x1#+x2, y1#+y2>}";
+by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
qed "zadd";
-Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zadd]));
+qed "raw_zadd_0";
+
+Goal "$#0 $+ z = intify(z)";
+by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
+qed "zadd_0_intify";
+Addsimps [zadd_0_intify];
+
+Goal "z: int ==> $#0 $+ z = z";
+by (Asm_simp_tac 1);
qed "zadd_0";
-Goalw [int_def] "[| z: int; w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
+Goalw [int_def]
+ "[| z: int; w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
+by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));
+qed "raw_zminus_zadd_distrib";
+
+Goal "$~ (z $+ w) = $~ z $+ $~ w";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
qed "zminus_zadd_distrib";
-Goalw [int_def] "[| z: int; w: int |] ==> z $+ w = w $+ z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
+Goalw [int_def] "[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
+by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));
+qed "raw_zadd_commute";
+
+Goal "z $+ w = w $+ z";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
qed "zadd_commute";
Goalw [int_def]
"[| z1: int; z2: int; z3: int |] \
-\ ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-(*rewriting is much faster without intrel_iff, etc.*)
-by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
+\ ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
+by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));
+qed "raw_zadd_assoc";
+
+Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
+by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
qed "zadd_assoc";
(*For AC rewriting*)
-Goal "[| z1:int; z2:int; z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
+Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
qed "zadd_left_commute";
@@ -289,31 +414,38 @@
(*Integer addition is an AC operator*)
val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
-Goalw [int_of_def]
- "[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
+Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
qed "int_of_add";
-Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
+by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));
+qed "raw_zadd_zminus_inverse";
+
+Goal "z $+ ($~ z) = $#0";
+by (simp_tac (simpset() addsimps [zadd_def]) 1);
+by (stac (zminus_intify RS sym) 1);
+by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1);
qed "zadd_zminus_inverse";
-Goal "z : int ==> ($~ z) $+ z = $#0";
-by (asm_simp_tac
- (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
+Goal "($~ z) $+ z = $#0";
+by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
qed "zadd_zminus_inverse2";
+Goal "z $+ $#0 = intify(z)";
+by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
+qed "zadd_0_right_intify";
+Addsimps [zadd_0_right_intify];
+
Goal "z:int ==> z $+ $#0 = z";
-by (rtac (zadd_commute RS trans) 1);
-by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
+by (Asm_simp_tac 1);
qed "zadd_0_right";
-Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+Addsimps [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)
+ [| m: nat; n: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
*)
(**** zmult: multiplication on int ****)
@@ -339,58 +471,93 @@
(*Resolve th against the corresponding facts for zmult*)
val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
-Goalw [int_def,zmult_def] "[| z: int; w: int |] ==> z $* w : int";
+Goalw [int_def,raw_zmult_def] "[| z: int; w: int |] ==> raw_zmult(z,w) : int";
by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
split_type, add_type, mult_type,
quotientI, SigmaI] 1));
+qed "raw_zmult_type";
+
+Goal "z $* w : int";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
qed "zmult_type";
-AddTCs [zmult_type];
+AddIffs [zmult_type]; AddTCs [zmult_type];
+
+Goalw [raw_zmult_def]
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
+\ ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) = \
+\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
+by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
+qed "raw_zmult";
Goalw [zmult_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
-\ (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
+\ ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
+\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
+by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
qed "zmult";
-Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
+qed "raw_zmult_0";
+
+Goal "$#0 $* z = $#0";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
qed "zmult_0";
+Addsimps [zmult_0];
-Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
+Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
+qed "raw_zmult_1";
+
+Goal "$#1 $* z = intify(z)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
+qed "zmult_1_intify";
+Addsimps [zmult_1_intify];
+
+Goal "z : int ==> $#1 $* z = z";
+by (Asm_simp_tac 1);
qed "zmult_1";
-Goalw [int_def] "[| z: int; w: int |] ==> ($~ z) $* w = $~ (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus";
-
-Addsimps [zmult_0, zmult_1, zmult_zminus];
+Goalw [int_def] "[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
+by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));
+qed "raw_zmult_commute";
-Goalw [int_def] "[| z: int; w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus_zminus";
-
-Goalw [int_def] "[| z: int; w: int |] ==> z $* w = w $* z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
+Goal "z $* w = w $* z";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
qed "zmult_commute";
Goalw [int_def]
- "[| z1: int; z2: int; z3: int |] \
-\ ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac
- (simpset() addsimps [zmult, add_mult_distrib_left,
- add_mult_distrib] @ add_ac @ mult_ac) 1);
+ "[| z: int; w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
+by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));
+qed "raw_zmult_zminus";
+
+Goal "($~ z) $* w = $~ (z $* w)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
+by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1);
+by Auto_tac;
+qed "zmult_zminus";
+Addsimps [zmult_zminus];
+
+Goal "($~ z) $* ($~ w) = (z $* w)";
+by (stac zmult_zminus 1);
+by (stac zmult_commute 1 THEN stac zmult_zminus 1);
+by (simp_tac (simpset() addsimps [zmult_commute])1);
+qed "zmult_zminus_zminus";
+
+Goalw [int_def]
+ "[| z1: int; z2: int; z3: int |] \
+\ ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
+by (auto_tac (claset(),
+ simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));
+qed "raw_zmult_assoc";
+
+Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type,
+ raw_zmult_assoc]) 1);
qed "zmult_assoc";
(*For AC rewriting*)
-Goal "[| z1:int; z2:int; z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
+Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
qed "zmult_left_commute";
@@ -399,17 +566,25 @@
val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
Goalw [int_def]
- "[| z1: int; z2: int; w: int |] ==> \
-\ (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
+ "[| z1: int; z2: int; w: int |] \
+\ ==> raw_zmult(raw_zadd(z1,z2), w) = \
+\ raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
+by (auto_tac (claset(),
+ simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @
+ add_ac @ mult_ac));
+qed "raw_zadd_zmult_distrib";
+
+Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
+by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type,
+ raw_zmult_type, raw_zadd_zmult_distrib]) 1);
qed "zadd_zmult_distrib";
+Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
+by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
+ zadd_zmult_distrib]) 1);
+qed "zadd_zmult_distrib_left";
+
val int_typechecks =
[int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
-Addsimps int_typechecks;
-
-
--- a/src/ZF/Integ/Int.thy Wed Aug 02 16:06:54 2000 +0200
+++ b/src/ZF/Integ/Int.thy Wed Aug 02 16:07:32 2000 +0200
@@ -7,54 +7,64 @@
*)
Int = EquivClass + Arith +
-consts
- intrel,int:: i
- int_of :: i=>i ("$# _" [80] 80)
- zminus :: i=>i ("$~ _" [80] 80)
- znegative :: i=>o
- zmagnitude :: i=>i
- "$*" :: [i,i]=>i (infixl 70)
- "$'/" :: [i,i]=>i (infixl 70)
- "$'/'/" :: [i,i]=>i (infixl 70)
- "$+" :: [i,i]=>i (infixl 65)
- "$-" :: [i,i]=>i (infixl 65)
- "$<" :: [i,i]=>o (infixl 50)
+
+constdefs
+ intrel :: i
+ "intrel == {p:(nat*nat)*(nat*nat).
+ EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
-defs
+ int :: i
+ "int == (nat*nat)//intrel"
+
+ int_of :: i=>i (*coercion from nat to int*) ("$# _" [80] 80)
+ "$# m == intrel `` {<natify(m), 0>}"
+
+ intify :: i=>i (*coercion from ANYTHING to int*)
+ "intify(m) == if m : int then m else $#0"
- intrel_def
- "intrel == {p:(nat*nat)*(nat*nat).
- EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+ raw_zminus :: i=>i
+ "raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
+
+ zminus :: i=>i ("$~ _" [80] 80)
+ "$~ z == raw_zminus (intify(z))"
- int_def "int == (nat*nat)//intrel"
-
- int_of_def "$# m == intrel `` {<m,0>}"
-
- zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
-
- znegative_def
- "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
-
- zmagnitude_def
- "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.
+ znegative :: i=>o
+ "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
+
+ zmagnitude :: i=>i
+ "zmagnitude(z) ==
+ THE m. m : nat & ((~ znegative(z) & z = $# m) |
+ (znegative(z) & $~ z = $# m))"
+
+ raw_zmult :: [i,i]=>i
+ (*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
Perhaps a "curried" or even polymorphic congruent predicate would be
better.*)
- zadd_def
- "Z1 $+ Z2 ==
- UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2
+ "raw_zmult(z1,z2) ==
+ UN p1:z1. UN p2:z2. split(%x1 y1. split(%x2 y2.
+ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+
+ zmult :: [i,i]=>i (infixl "$*" 70)
+ "z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
+
+ raw_zadd :: [i,i]=>i
+ "raw_zadd (z1, z2) ==
+ UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2
in intrel``{<x1#+x2, y1#+y2>}"
-
- zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)"
- zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
+
+ zadd :: [i,i]=>i (infixl "$+" 65)
+ "z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
+
+ zdiff :: [i,i]=>i (infixl "$-" 65)
+ "z1 $- z2 == z1 $+ zminus(z2)"
+
+ zless :: [i,i]=>o (infixl "$<" 50)
+ "z1 $< z2 == znegative(z1 $- z2)"
+
+(*div and mod await definitions!*)
+consts
+ "$'/" :: [i,i]=>i (infixl 70)
+
+ "$'/'/" :: [i,i]=>i (infixl 70)
- (*This illustrates the primitive form of definitions (no patterns)*)
- zmult_def
- "Z1 $* Z2 ==
- UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2.
- intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
-
- end
+end