Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
authorpaulson
Fri Sep 25 13:18:07 1998 +0200 (1998-09-25)
changeset 5561426c1e330903
parent 5560 c17471a9c99c
child 5562 02261e6880d1
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants
src/ZF/Integ/Bin.ML
src/ZF/Integ/Bin.thy
src/ZF/Integ/Int.ML
src/ZF/Integ/Int.thy
src/ZF/Integ/Integ.ML
src/ZF/Integ/Integ.thy
src/ZF/IsaMakefile
     1.1 --- a/src/ZF/Integ/Bin.ML	Fri Sep 25 12:12:07 1998 +0200
     1.2 +++ b/src/ZF/Integ/Bin.ML	Fri Sep 25 13:18:07 1998 +0200
     1.3 @@ -99,8 +99,8 @@
     1.4  
     1.5  val bin_typechecks0 = bin_rec_type :: bin.intrs;
     1.6  
     1.7 -Goalw [integ_of_def] "w: bin ==> integ_of(w) : integ";
     1.8 -by (typechk_tac (bin_typechecks0@integ_typechecks@
     1.9 +Goalw [integ_of_def] "w: bin ==> integ_of(w) : int";
    1.10 +by (typechk_tac (bin_typechecks0@int_typechecks@
    1.11                   nat_typechecks@[bool_into_nat]));
    1.12  qed "integ_of_type";
    1.13  
    1.14 @@ -143,33 +143,13 @@
    1.15  	   bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @ 
    1.16  	  bin_recs integ_of_def @ bin_typechecks);
    1.17  
    1.18 -val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
    1.19 +val typechecks = bin_typechecks @ int_typechecks @ nat_typechecks @
    1.20                   [bool_subset_nat RS subsetD];
    1.21  
    1.22  (**** The carry/borrow functions, bin_succ and bin_pred ****)
    1.23  
    1.24 -(** Lemmas **)
    1.25 -
    1.26 -goal Integ.thy 
    1.27 -    "!!z v. [| z $+ v = z' $+ v';  \
    1.28 -\       z: integ; z': integ;  v: integ; v': integ;  w: integ |]   \
    1.29 -\    ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
    1.30 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
    1.31 -qed "zadd_assoc_cong";
    1.32 -
    1.33 -goal Integ.thy 
    1.34 -    "!!z v w. [| z: integ;  v: integ;  w: integ |]   \
    1.35 -\    ==> z $+ (v $+ w) = v $+ (z $+ w)";
    1.36 -by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
    1.37 -qed "zadd_assoc_swap";
    1.38 -
    1.39 -(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
    1.40 -bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap));
    1.41 -
    1.42 -
    1.43  Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
    1.44  
    1.45 -
    1.46  (*NCons preserves the integer value of its argument*)
    1.47  Goal "[| w: bin; b: bool |] ==>     \
    1.48  \         integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
    1.49 @@ -346,7 +326,7 @@
    1.50  (*** The computation simpset ***)
    1.51  
    1.52  (*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
    1.53 -val bin_comp_ss = simpset_of Integ.thy 
    1.54 +val bin_comp_ss = simpset_of Int.thy 
    1.55      addsimps [integ_of_add RS sym,   (*invoke bin_add*)
    1.56                integ_of_minus RS sym, (*invoke bin_minus*)
    1.57                integ_of_mult RS sym,  (*invoke bin_mult*)
     2.1 --- a/src/ZF/Integ/Bin.thy	Fri Sep 25 12:12:07 1998 +0200
     2.2 +++ b/src/ZF/Integ/Bin.thy	Fri Sep 25 13:18:07 1998 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4  Division is not defined yet!
     2.5  *)
     2.6  
     2.7 -Bin = Integ + Datatype + 
     2.8 +Bin = Int + Datatype + 
     2.9  
    2.10  consts
    2.11    bin_rec   :: [i, i, i, [i,i,i]=>i] => i
    2.12 @@ -143,15 +143,15 @@
    2.13          | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
    2.14          | bin_of _ = raise Match;
    2.15  
    2.16 -      fun int_of [] = 0
    2.17 -        | int_of (b :: bs) = b + 2 * int_of bs;
    2.18 +      fun integ_of [] = 0
    2.19 +        | integ_of (b :: bs) = b + 2 * integ_of bs;
    2.20  
    2.21        val rev_digs = bin_of tm;
    2.22        val (sign, zs) =
    2.23          (case rev rev_digs of
    2.24            ~1 :: bs => ("-", prefix_len (equal 1) bs)
    2.25          | bs => ("", prefix_len (equal 0) bs));
    2.26 -      val num = string_of_int (abs (int_of rev_digs));
    2.27 +      val num = string_of_int (abs (integ_of rev_digs));
    2.28      in
    2.29        "#" ^ sign ^ implode (replicate zs "0") ^ num
    2.30      end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Integ/Int.ML	Fri Sep 25 13:18:07 1998 +0200
     3.3 @@ -0,0 +1,412 @@
     3.4 +(*  Title:      ZF/Integ/Int.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1993  University of Cambridge
     3.8 +
     3.9 +The integers as equivalence classes over nat*nat.
    3.10 +
    3.11 +Could also prove...
    3.12 +"znegative(z) ==> $# zmagnitude(z) = $~ z"
    3.13 +"~ znegative(z) ==> $# zmagnitude(z) = z"
    3.14 +$< is a linear ordering
    3.15 +$+ and $* are monotonic wrt $<
    3.16 +*)
    3.17 +
    3.18 +AddSEs [quotientE];
    3.19 +
    3.20 +(*** Proving that intrel is an equivalence relation ***)
    3.21 +
    3.22 +(*By luck, requires no typing premises for y1, y2,y3*)
    3.23 +val eqa::eqb::prems = goal Arith.thy 
    3.24 +    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    3.25 +\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    3.26 +by (res_inst_tac [("k","x2")] add_left_cancel 1);
    3.27 +by (resolve_tac prems 2);
    3.28 +by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    3.29 +by (stac eqb 1);
    3.30 +by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    3.31 +by (stac eqa 1);
    3.32 +by (rtac (add_left_commute) 1 THEN typechk_tac prems);
    3.33 +qed "int_trans_lemma";
    3.34 +
    3.35 +(** Natural deduction for intrel **)
    3.36 +
    3.37 +Goalw [intrel_def]
    3.38 +    "<<x1,y1>,<x2,y2>>: intrel <-> \
    3.39 +\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    3.40 +by (Fast_tac 1);
    3.41 +qed "intrel_iff";
    3.42 +
    3.43 +Goalw [intrel_def]
    3.44 +    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
    3.45 +\             <<x1,y1>,<x2,y2>>: intrel";
    3.46 +by (fast_tac (claset() addIs prems) 1);
    3.47 +qed "intrelI";
    3.48 +
    3.49 +(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    3.50 +Goalw [intrel_def]
    3.51 +  "p: intrel --> (EX x1 y1 x2 y2. \
    3.52 +\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    3.53 +\                  x1: nat & y1: nat & x2: nat & y2: nat)";
    3.54 +by (Fast_tac 1);
    3.55 +qed "intrelE_lemma";
    3.56 +
    3.57 +val [major,minor] = goal thy
    3.58 +  "[| p: intrel;  \
    3.59 +\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    3.60 +\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    3.61 +\  ==> Q";
    3.62 +by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    3.63 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    3.64 +qed "intrelE";
    3.65 +
    3.66 +AddSIs [intrelI];
    3.67 +AddSEs [intrelE];
    3.68 +
    3.69 +Goalw [equiv_def, refl_def, sym_def, trans_def]
    3.70 +    "equiv(nat*nat, intrel)";
    3.71 +by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
    3.72 +qed "equiv_intrel";
    3.73 +
    3.74 +
    3.75 +Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    3.76 +	  add_0_right, add_succ_right];
    3.77 +Addcongs [conj_cong];
    3.78 +
    3.79 +val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    3.80 +
    3.81 +(** int_of: the injection from nat to int **)
    3.82 +
    3.83 +Goalw [int_def,quotient_def,int_of_def]
    3.84 +    "m : nat ==> $#m : int";
    3.85 +by (fast_tac (claset() addSIs [nat_0I]) 1);
    3.86 +qed "int_of_type";
    3.87 +
    3.88 +Addsimps [int_of_type];
    3.89 +
    3.90 +Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    3.91 +by (dtac (sym RS eq_intrelD) 1);
    3.92 +by (typechk_tac [nat_0I, SigmaI]);
    3.93 +by (Asm_full_simp_tac 1);
    3.94 +qed "int_of_inject";
    3.95 +
    3.96 +AddSDs [int_of_inject];
    3.97 +
    3.98 +Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
    3.99 +by (Blast_tac 1); 
   3.100 +qed "int_of_eq"; 
   3.101 +Addsimps [int_of_eq]; 
   3.102 +
   3.103 +(**** zminus: unary negation on int ****)
   3.104 +
   3.105 +Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   3.106 +by Safe_tac;
   3.107 +by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   3.108 +qed "zminus_congruent";
   3.109 +
   3.110 +(*Resolve th against the corresponding facts for zminus*)
   3.111 +val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   3.112 +
   3.113 +Goalw [int_def,zminus_def] "z : int ==> $~z : int";
   3.114 +by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
   3.115 +                 quotientI]);
   3.116 +qed "zminus_type";
   3.117 +
   3.118 +Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
   3.119 +by (etac (zminus_ize UN_equiv_class_inject) 1);
   3.120 +by Safe_tac;
   3.121 +(*The setloop is only needed because assumptions are in the wrong order!*)
   3.122 +by (asm_full_simp_tac (simpset() addsimps add_ac
   3.123 +                       setloop dtac eq_intrelD) 1);
   3.124 +qed "zminus_inject";
   3.125 +
   3.126 +Goalw [zminus_def]
   3.127 +    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   3.128 +by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   3.129 +qed "zminus";
   3.130 +
   3.131 +Goalw [int_def] "z : int ==> $~ ($~ z) = z";
   3.132 +by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   3.133 +by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   3.134 +qed "zminus_zminus";
   3.135 +
   3.136 +Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
   3.137 +by (simp_tac (simpset() addsimps [zminus]) 1);
   3.138 +qed "zminus_0";
   3.139 +
   3.140 +Addsimps [zminus_zminus, zminus_0];
   3.141 +
   3.142 +
   3.143 +(**** znegative: the test for negative integers ****)
   3.144 +
   3.145 +(*No natural number is negative!*)
   3.146 +Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
   3.147 +by Safe_tac;
   3.148 +by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   3.149 +by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   3.150 +by (force_tac (claset(),
   3.151 +	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   3.152 +qed "not_znegative_int_of";
   3.153 +
   3.154 +Addsimps [not_znegative_int_of];
   3.155 +AddSEs   [not_znegative_int_of RS notE];
   3.156 +
   3.157 +Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
   3.158 +by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   3.159 +by (blast_tac (claset() addIs [nat_0_le]) 1);
   3.160 +qed "znegative_zminus_int_of";
   3.161 +
   3.162 +Addsimps [znegative_zminus_int_of];
   3.163 +
   3.164 +Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   3.165 +by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   3.166 +be natE 1;
   3.167 +by (dres_inst_tac [("x","0")] spec 2);
   3.168 +by Auto_tac;
   3.169 +qed "not_znegative_imp_zero";
   3.170 +
   3.171 +(**** zmagnitude: magnitide of an integer, as a natural number ****)
   3.172 +
   3.173 +Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
   3.174 +by Auto_tac;
   3.175 +qed "zmagnitude_int_of";
   3.176 +
   3.177 +Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
   3.178 +by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
   3.179 +qed "zmagnitude_zminus_int_of";
   3.180 +
   3.181 +Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
   3.182 +
   3.183 +Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   3.184 +br theI2 1;
   3.185 +by Auto_tac;
   3.186 +qed "zmagnitude_type";
   3.187 +
   3.188 +Goalw [int_def, znegative_def, int_of_def]
   3.189 +     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   3.190 +by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   3.191 +by (rename_tac "i j" 1);
   3.192 +by (dres_inst_tac [("x", "i")] spec 1);
   3.193 +by (dres_inst_tac [("x", "j")] spec 1);
   3.194 +br bexI 1;
   3.195 +br (add_diff_inverse2 RS sym) 1;
   3.196 +by Auto_tac;
   3.197 +by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
   3.198 +qed "not_zneg_int_of";
   3.199 +
   3.200 +Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   3.201 +bd not_zneg_int_of 1;
   3.202 +by Auto_tac;
   3.203 +qed "not_zneg_mag"; 
   3.204 +
   3.205 +Addsimps [not_zneg_mag];
   3.206 +
   3.207 +
   3.208 +Goalw [int_def, znegative_def, int_of_def]
   3.209 +     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   3.210 +by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   3.211 +	     simpset() addsimps [zminus, image_singleton_iff]));
   3.212 +by (rename_tac "m n j k" 1);
   3.213 +by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   3.214 +by (rotate_tac ~2 2);
   3.215 +by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   3.216 +by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   3.217 +qed "zneg_int_of";
   3.218 +
   3.219 +Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   3.220 +bd zneg_int_of 1;
   3.221 +by Auto_tac;
   3.222 +qed "zneg_mag"; 
   3.223 +
   3.224 +Addsimps [zneg_mag];
   3.225 +
   3.226 +
   3.227 +(**** zadd: addition on int ****)
   3.228 +
   3.229 +(** Congruence property for addition **)
   3.230 +
   3.231 +Goalw [congruent2_def]
   3.232 +    "congruent2(intrel, %z1 z2.                      \
   3.233 +\         let <x1,y1>=z1; <x2,y2>=z2                 \
   3.234 +\                           in intrel``{<x1#+x2, y1#+y2>})";
   3.235 +(*Proof via congruent2_commuteI seems longer*)
   3.236 +by Safe_tac;
   3.237 +by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   3.238 +(*The rest should be trivial, but rearranging terms is hard;
   3.239 +  add_ac does not help rewriting with the assumptions.*)
   3.240 +by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   3.241 +by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
   3.242 +by (typechk_tac [add_type]);
   3.243 +by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   3.244 +qed "zadd_congruent2";
   3.245 +
   3.246 +(*Resolve th against the corresponding facts for zadd*)
   3.247 +val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   3.248 +
   3.249 +Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
   3.250 +by (rtac (zadd_ize UN_equiv_class_type2) 1);
   3.251 +by (simp_tac (simpset() addsimps [Let_def]) 3);
   3.252 +by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   3.253 +qed "zadd_type";
   3.254 +
   3.255 +Goalw [zadd_def]
   3.256 +  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   3.257 +\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
   3.258 +\           intrel `` {<x1#+x2, y1#+y2>}";
   3.259 +by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   3.260 +by (simp_tac (simpset() addsimps [Let_def]) 1);
   3.261 +qed "zadd";
   3.262 +
   3.263 +Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
   3.264 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.265 +by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   3.266 +qed "zadd_0";
   3.267 +
   3.268 +Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   3.269 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.270 +by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   3.271 +qed "zminus_zadd_distrib";
   3.272 +
   3.273 +Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
   3.274 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.275 +by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   3.276 +qed "zadd_commute";
   3.277 +
   3.278 +Goalw [int_def]
   3.279 +    "[| z1: int;  z2: int;  z3: int |]   \
   3.280 +\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   3.281 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.282 +(*rewriting is much faster without intrel_iff, etc.*)
   3.283 +by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   3.284 +qed "zadd_assoc";
   3.285 +
   3.286 +(*For AC rewriting*)
   3.287 +Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   3.288 +by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
   3.289 +qed "zadd_left_commute";
   3.290 +
   3.291 +(*Integer addition is an AC operator*)
   3.292 +val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   3.293 +
   3.294 +Goalw [int_of_def]
   3.295 +    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   3.296 +by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   3.297 +qed "int_of_add";
   3.298 +
   3.299 +Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
   3.300 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.301 +by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   3.302 +qed "zadd_zminus_inverse";
   3.303 +
   3.304 +Goal "z : int ==> ($~ z) $+ z = $#0";
   3.305 +by (asm_simp_tac
   3.306 +    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
   3.307 +qed "zadd_zminus_inverse2";
   3.308 +
   3.309 +Goal "z:int ==> z $+ $#0 = z";
   3.310 +by (rtac (zadd_commute RS trans) 1);
   3.311 +by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
   3.312 +qed "zadd_0_right";
   3.313 +
   3.314 +Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   3.315 +
   3.316 +
   3.317 +(*Need properties of $- ???  Or use $- just as an abbreviation?
   3.318 +     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   3.319 +*)
   3.320 +
   3.321 +(**** zmult: multiplication on int ****)
   3.322 +
   3.323 +(** Congruence property for multiplication **)
   3.324 +
   3.325 +Goal "congruent2(intrel, %p1 p2.                 \
   3.326 +\               split(%x1 y1. split(%x2 y2.     \
   3.327 +\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   3.328 +by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   3.329 +by Safe_tac;
   3.330 +by (ALLGOALS Asm_simp_tac);
   3.331 +(*Proof that zmult is congruent in one argument*)
   3.332 +by (asm_simp_tac 
   3.333 +    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   3.334 +by (asm_simp_tac
   3.335 +    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   3.336 +(*Proof that zmult is commutative on representatives*)
   3.337 +by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   3.338 +qed "zmult_congruent2";
   3.339 +
   3.340 +
   3.341 +(*Resolve th against the corresponding facts for zmult*)
   3.342 +val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   3.343 +
   3.344 +Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
   3.345 +by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   3.346 +                      split_type, add_type, mult_type, 
   3.347 +                      quotientI, SigmaI] 1));
   3.348 +qed "zmult_type";
   3.349 +
   3.350 +Goalw [zmult_def]
   3.351 +     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   3.352 +\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   3.353 +\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   3.354 +by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   3.355 +qed "zmult";
   3.356 +
   3.357 +Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
   3.358 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.359 +by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   3.360 +qed "zmult_0";
   3.361 +
   3.362 +Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
   3.363 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.364 +by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
   3.365 +qed "zmult_1";
   3.366 +
   3.367 +Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
   3.368 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.369 +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   3.370 +qed "zmult_zminus";
   3.371 +
   3.372 +Addsimps [zmult_0, zmult_1, zmult_zminus];
   3.373 +
   3.374 +Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
   3.375 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.376 +by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   3.377 +qed "zmult_zminus_zminus";
   3.378 +
   3.379 +Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
   3.380 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.381 +by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   3.382 +qed "zmult_commute";
   3.383 +
   3.384 +Goalw [int_def]
   3.385 +    "[| z1: int;  z2: int;  z3: int |]     \
   3.386 +\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   3.387 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.388 +by (asm_simp_tac 
   3.389 +    (simpset() addsimps [zmult, add_mult_distrib_left, 
   3.390 +                         add_mult_distrib] @ add_ac @ mult_ac) 1);
   3.391 +qed "zmult_assoc";
   3.392 +
   3.393 +(*For AC rewriting*)
   3.394 +Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   3.395 +by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
   3.396 +qed "zmult_left_commute";
   3.397 +
   3.398 +(*Integer multiplication is an AC operator*)
   3.399 +val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   3.400 +
   3.401 +Goalw [int_def]
   3.402 +    "[| z1: int;  z2: int;  w: int |] ==> \
   3.403 +\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   3.404 +by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   3.405 +by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
   3.406 +by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
   3.407 +qed "zadd_zmult_distrib";
   3.408 +
   3.409 +val int_typechecks =
   3.410 +    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   3.411 +
   3.412 +Addsimps int_typechecks;
   3.413 +
   3.414 +
   3.415 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/Integ/Int.thy	Fri Sep 25 13:18:07 1998 +0200
     4.3 @@ -0,0 +1,60 @@
     4.4 +(*  Title:      ZF/Integ/Int.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1993  University of Cambridge
     4.8 +
     4.9 +The integers as equivalence classes over nat*nat.
    4.10 +*)
    4.11 +
    4.12 +Int = EquivClass + Arith +
    4.13 +consts
    4.14 +    intrel,int::      i
    4.15 +    int_of      ::      i=>i            ("$# _" [80] 80)
    4.16 +    zminus      ::      i=>i            ("$~ _" [80] 80)
    4.17 +    znegative   ::      i=>o
    4.18 +    zmagnitude  ::      i=>i
    4.19 +    "$*"        ::      [i,i]=>i      (infixl 70)
    4.20 +    "$'/"       ::      [i,i]=>i      (infixl 70) 
    4.21 +    "$'/'/"     ::      [i,i]=>i      (infixl 70)
    4.22 +    "$+"        ::      [i,i]=>i      (infixl 65)
    4.23 +    "$-"        ::      [i,i]=>i      (infixl 65)
    4.24 +    "$<"        ::      [i,i]=>o        (infixl 50)
    4.25 +
    4.26 +defs
    4.27 +
    4.28 +    intrel_def
    4.29 +     "intrel == {p:(nat*nat)*(nat*nat).                 
    4.30 +        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    4.31 +
    4.32 +    int_def   "int == (nat*nat)/intrel"
    4.33 +    
    4.34 +    int_of_def  "$# m == intrel `` {<m,0>}"
    4.35 +    
    4.36 +    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    4.37 +    
    4.38 +    znegative_def
    4.39 +        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    4.40 +    
    4.41 +    zmagnitude_def
    4.42 +        "zmagnitude(Z) ==
    4.43 +	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
    4.44 +	                   (znegative(Z) & $~ Z = $# m))"
    4.45 +    
    4.46 +    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    4.47 +      Perhaps a "curried" or even polymorphic congruent predicate would be
    4.48 +      better.*)
    4.49 +    zadd_def
    4.50 +     "Z1 $+ Z2 == 
    4.51 +       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
    4.52 +                           in intrel``{<x1#+x2, y1#+y2>}"
    4.53 +    
    4.54 +    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    4.55 +    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    4.56 +    
    4.57 +    (*This illustrates the primitive form of definitions (no patterns)*)
    4.58 +    zmult_def
    4.59 +     "Z1 $* Z2 == 
    4.60 +       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
    4.61 +                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    4.62 +    
    4.63 + end
     5.1 --- a/src/ZF/Integ/Integ.ML	Fri Sep 25 12:12:07 1998 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,412 +0,0 @@
     5.4 -(*  Title:      ZF/ex/integ.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1993  University of Cambridge
     5.8 -
     5.9 -The integers as equivalence classes over nat*nat.
    5.10 -
    5.11 -Could also prove...
    5.12 -"znegative(z) ==> $# zmagnitude(z) = $~ z"
    5.13 -"~ znegative(z) ==> $# zmagnitude(z) = z"
    5.14 -$< is a linear ordering
    5.15 -$+ and $* are monotonic wrt $<
    5.16 -*)
    5.17 -
    5.18 -AddSEs [quotientE];
    5.19 -
    5.20 -(*** Proving that intrel is an equivalence relation ***)
    5.21 -
    5.22 -(*By luck, requires no typing premises for y1, y2,y3*)
    5.23 -val eqa::eqb::prems = goal Arith.thy 
    5.24 -    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
    5.25 -\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
    5.26 -by (res_inst_tac [("k","x2")] add_left_cancel 1);
    5.27 -by (resolve_tac prems 2);
    5.28 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    5.29 -by (stac eqb 1);
    5.30 -by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
    5.31 -by (stac eqa 1);
    5.32 -by (rtac (add_left_commute) 1 THEN typechk_tac prems);
    5.33 -qed "integ_trans_lemma";
    5.34 -
    5.35 -(** Natural deduction for intrel **)
    5.36 -
    5.37 -Goalw [intrel_def]
    5.38 -    "<<x1,y1>,<x2,y2>>: intrel <-> \
    5.39 -\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
    5.40 -by (Fast_tac 1);
    5.41 -qed "intrel_iff";
    5.42 -
    5.43 -Goalw [intrel_def]
    5.44 -    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
    5.45 -\             <<x1,y1>,<x2,y2>>: intrel";
    5.46 -by (fast_tac (claset() addIs prems) 1);
    5.47 -qed "intrelI";
    5.48 -
    5.49 -(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
    5.50 -Goalw [intrel_def]
    5.51 -  "p: intrel --> (EX x1 y1 x2 y2. \
    5.52 -\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
    5.53 -\                  x1: nat & y1: nat & x2: nat & y2: nat)";
    5.54 -by (Fast_tac 1);
    5.55 -qed "intrelE_lemma";
    5.56 -
    5.57 -val [major,minor] = goal Integ.thy
    5.58 -  "[| p: intrel;  \
    5.59 -\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
    5.60 -\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
    5.61 -\  ==> Q";
    5.62 -by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
    5.63 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    5.64 -qed "intrelE";
    5.65 -
    5.66 -AddSIs [intrelI];
    5.67 -AddSEs [intrelE];
    5.68 -
    5.69 -Goalw [equiv_def, refl_def, sym_def, trans_def]
    5.70 -    "equiv(nat*nat, intrel)";
    5.71 -by (fast_tac (claset() addSEs [sym, integ_trans_lemma]) 1);
    5.72 -qed "equiv_intrel";
    5.73 -
    5.74 -
    5.75 -Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
    5.76 -	  add_0_right, add_succ_right];
    5.77 -Addcongs [conj_cong];
    5.78 -
    5.79 -val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
    5.80 -
    5.81 -(** znat: the injection from nat to integ **)
    5.82 -
    5.83 -Goalw [integ_def,quotient_def,znat_def]
    5.84 -    "m : nat ==> $#m : integ";
    5.85 -by (fast_tac (claset() addSIs [nat_0I]) 1);
    5.86 -qed "znat_type";
    5.87 -
    5.88 -Addsimps [znat_type];
    5.89 -
    5.90 -Goalw [znat_def] "[| $#m = $#n;  m: nat |] ==> m=n";
    5.91 -by (dtac (sym RS eq_intrelD) 1);
    5.92 -by (typechk_tac [nat_0I, SigmaI]);
    5.93 -by (Asm_full_simp_tac 1);
    5.94 -qed "znat_inject";
    5.95 -
    5.96 -AddSDs [znat_inject];
    5.97 -
    5.98 -Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
    5.99 -by (Blast_tac 1); 
   5.100 -qed "znat_znat_eq"; 
   5.101 -Addsimps [znat_znat_eq]; 
   5.102 -
   5.103 -(**** zminus: unary negation on integ ****)
   5.104 -
   5.105 -Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
   5.106 -by Safe_tac;
   5.107 -by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
   5.108 -qed "zminus_congruent";
   5.109 -
   5.110 -(*Resolve th against the corresponding facts for zminus*)
   5.111 -val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
   5.112 -
   5.113 -Goalw [integ_def,zminus_def] "z : integ ==> $~z : integ";
   5.114 -by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
   5.115 -                 quotientI]);
   5.116 -qed "zminus_type";
   5.117 -
   5.118 -Goalw [integ_def,zminus_def] "[| $~z = $~w;  z: integ;  w: integ |] ==> z=w";
   5.119 -by (etac (zminus_ize UN_equiv_class_inject) 1);
   5.120 -by Safe_tac;
   5.121 -(*The setloop is only needed because assumptions are in the wrong order!*)
   5.122 -by (asm_full_simp_tac (simpset() addsimps add_ac
   5.123 -                       setloop dtac eq_intrelD) 1);
   5.124 -qed "zminus_inject";
   5.125 -
   5.126 -Goalw [zminus_def]
   5.127 -    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
   5.128 -by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
   5.129 -qed "zminus";
   5.130 -
   5.131 -Goalw [integ_def] "z : integ ==> $~ ($~ z) = z";
   5.132 -by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
   5.133 -by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   5.134 -qed "zminus_zminus";
   5.135 -
   5.136 -Goalw [integ_def, znat_def] "$~ ($#0) = $#0";
   5.137 -by (simp_tac (simpset() addsimps [zminus]) 1);
   5.138 -qed "zminus_0";
   5.139 -
   5.140 -Addsimps [zminus_zminus, zminus_0];
   5.141 -
   5.142 -
   5.143 -(**** znegative: the test for negative integers ****)
   5.144 -
   5.145 -(*No natural number is negative!*)
   5.146 -Goalw [znegative_def, znat_def]  "~ znegative($# n)";
   5.147 -by Safe_tac;
   5.148 -by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
   5.149 -by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
   5.150 -by (force_tac (claset(),
   5.151 -	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
   5.152 -qed "not_znegative_znat";
   5.153 -
   5.154 -Addsimps [not_znegative_znat];
   5.155 -AddSEs   [not_znegative_znat RS notE];
   5.156 -
   5.157 -Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
   5.158 -by (asm_simp_tac (simpset() addsimps [zminus]) 1);
   5.159 -by (blast_tac (claset() addIs [nat_0_le]) 1);
   5.160 -qed "znegative_zminus_znat";
   5.161 -
   5.162 -Addsimps [znegative_zminus_znat];
   5.163 -
   5.164 -Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
   5.165 -by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
   5.166 -be natE 1;
   5.167 -by (dres_inst_tac [("x","0")] spec 2);
   5.168 -by Auto_tac;
   5.169 -qed "not_znegative_imp_zero";
   5.170 -
   5.171 -(**** zmagnitude: magnitide of an integer, as a natural number ****)
   5.172 -
   5.173 -Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
   5.174 -by Auto_tac;
   5.175 -qed "zmagnitude_znat";
   5.176 -
   5.177 -Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
   5.178 -by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
   5.179 -qed "zmagnitude_zminus_znat";
   5.180 -
   5.181 -Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
   5.182 -
   5.183 -Goalw [zmagnitude_def] "zmagnitude(z) : nat";
   5.184 -br theI2 1;
   5.185 -by Auto_tac;
   5.186 -qed "zmagnitude_type";
   5.187 -
   5.188 -Goalw [integ_def, znegative_def, znat_def]
   5.189 -     "[| z: integ; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
   5.190 -by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
   5.191 -by (rename_tac "i j" 1);
   5.192 -by (dres_inst_tac [("x", "i")] spec 1);
   5.193 -by (dres_inst_tac [("x", "j")] spec 1);
   5.194 -br bexI 1;
   5.195 -br (add_diff_inverse2 RS sym) 1;
   5.196 -by Auto_tac;
   5.197 -by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
   5.198 -qed "not_zneg_znat";
   5.199 -
   5.200 -Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
   5.201 -bd not_zneg_znat 1;
   5.202 -by Auto_tac;
   5.203 -qed "not_zneg_mag"; 
   5.204 -
   5.205 -Addsimps [not_zneg_mag];
   5.206 -
   5.207 -
   5.208 -Goalw [integ_def, znegative_def, znat_def]
   5.209 -     "[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
   5.210 -by (auto_tac(claset() addSDs [less_imp_Suc_add], 
   5.211 -	     simpset() addsimps [zminus, image_singleton_iff]));
   5.212 -by (rename_tac "m n j k" 1);
   5.213 -by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
   5.214 -by (rotate_tac ~2 2);
   5.215 -by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
   5.216 -by (blast_tac (claset() addSDs [add_left_cancel]) 1);
   5.217 -qed "zneg_znat";
   5.218 -
   5.219 -Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
   5.220 -bd zneg_znat 1;
   5.221 -by Auto_tac;
   5.222 -qed "zneg_mag"; 
   5.223 -
   5.224 -Addsimps [zneg_mag];
   5.225 -
   5.226 -
   5.227 -(**** zadd: addition on integ ****)
   5.228 -
   5.229 -(** Congruence property for addition **)
   5.230 -
   5.231 -Goalw [congruent2_def]
   5.232 -    "congruent2(intrel, %z1 z2.                      \
   5.233 -\         let <x1,y1>=z1; <x2,y2>=z2                 \
   5.234 -\                           in intrel``{<x1#+x2, y1#+y2>})";
   5.235 -(*Proof via congruent2_commuteI seems longer*)
   5.236 -by Safe_tac;
   5.237 -by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
   5.238 -(*The rest should be trivial, but rearranging terms is hard;
   5.239 -  add_ac does not help rewriting with the assumptions.*)
   5.240 -by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
   5.241 -by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
   5.242 -by (typechk_tac [add_type]);
   5.243 -by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
   5.244 -qed "zadd_congruent2";
   5.245 -
   5.246 -(*Resolve th against the corresponding facts for zadd*)
   5.247 -val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
   5.248 -
   5.249 -Goalw [integ_def,zadd_def] "[| z: integ;  w: integ |] ==> z $+ w : integ";
   5.250 -by (rtac (zadd_ize UN_equiv_class_type2) 1);
   5.251 -by (simp_tac (simpset() addsimps [Let_def]) 3);
   5.252 -by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
   5.253 -qed "zadd_type";
   5.254 -
   5.255 -Goalw [zadd_def]
   5.256 -  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
   5.257 -\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
   5.258 -\           intrel `` {<x1#+x2, y1#+y2>}";
   5.259 -by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
   5.260 -by (simp_tac (simpset() addsimps [Let_def]) 1);
   5.261 -qed "zadd";
   5.262 -
   5.263 -Goalw [integ_def,znat_def] "z : integ ==> $#0 $+ z = z";
   5.264 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.265 -by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   5.266 -qed "zadd_0";
   5.267 -
   5.268 -Goalw [integ_def] "[| z: integ;  w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
   5.269 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.270 -by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
   5.271 -qed "zminus_zadd_distrib";
   5.272 -
   5.273 -Goalw [integ_def] "[| z: integ;  w: integ |] ==> z $+ w = w $+ z";
   5.274 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.275 -by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
   5.276 -qed "zadd_commute";
   5.277 -
   5.278 -Goalw [integ_def]
   5.279 -    "[| z1: integ;  z2: integ;  z3: integ |]   \
   5.280 -\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
   5.281 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.282 -(*rewriting is much faster without intrel_iff, etc.*)
   5.283 -by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
   5.284 -qed "zadd_assoc";
   5.285 -
   5.286 -(*For AC rewriting*)
   5.287 -Goal "[| z1:integ;  z2:integ;  z3: integ |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
   5.288 -by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
   5.289 -qed "zadd_left_commute";
   5.290 -
   5.291 -(*Integer addition is an AC operator*)
   5.292 -val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
   5.293 -
   5.294 -Goalw [znat_def]
   5.295 -    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
   5.296 -by (asm_simp_tac (simpset() addsimps [zadd]) 1);
   5.297 -qed "znat_add";
   5.298 -
   5.299 -Goalw [integ_def,znat_def] "z : integ ==> z $+ ($~ z) = $#0";
   5.300 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.301 -by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
   5.302 -qed "zadd_zminus_inverse";
   5.303 -
   5.304 -Goal "z : integ ==> ($~ z) $+ z = $#0";
   5.305 -by (asm_simp_tac
   5.306 -    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
   5.307 -qed "zadd_zminus_inverse2";
   5.308 -
   5.309 -Goal "z:integ ==> z $+ $#0 = z";
   5.310 -by (rtac (zadd_commute RS trans) 1);
   5.311 -by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1));
   5.312 -qed "zadd_0_right";
   5.313 -
   5.314 -Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
   5.315 -
   5.316 -
   5.317 -(*Need properties of $- ???  Or use $- just as an abbreviation?
   5.318 -     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
   5.319 -*)
   5.320 -
   5.321 -(**** zmult: multiplication on integ ****)
   5.322 -
   5.323 -(** Congruence property for multiplication **)
   5.324 -
   5.325 -Goal "congruent2(intrel, %p1 p2.                 \
   5.326 -\               split(%x1 y1. split(%x2 y2.     \
   5.327 -\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
   5.328 -by (rtac (equiv_intrel RS congruent2_commuteI) 1);
   5.329 -by Safe_tac;
   5.330 -by (ALLGOALS Asm_simp_tac);
   5.331 -(*Proof that zmult is congruent in one argument*)
   5.332 -by (asm_simp_tac 
   5.333 -    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
   5.334 -by (asm_simp_tac
   5.335 -    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
   5.336 -(*Proof that zmult is commutative on representatives*)
   5.337 -by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
   5.338 -qed "zmult_congruent2";
   5.339 -
   5.340 -
   5.341 -(*Resolve th against the corresponding facts for zmult*)
   5.342 -val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
   5.343 -
   5.344 -Goalw [integ_def,zmult_def] "[| z: integ;  w: integ |] ==> z $* w : integ";
   5.345 -by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
   5.346 -                      split_type, add_type, mult_type, 
   5.347 -                      quotientI, SigmaI] 1));
   5.348 -qed "zmult_type";
   5.349 -
   5.350 -Goalw [zmult_def]
   5.351 -     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
   5.352 -\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
   5.353 -\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
   5.354 -by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
   5.355 -qed "zmult";
   5.356 -
   5.357 -Goalw [integ_def,znat_def] "z : integ ==> $#0 $* z = $#0";
   5.358 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.359 -by (asm_simp_tac (simpset() addsimps [zmult]) 1);
   5.360 -qed "zmult_0";
   5.361 -
   5.362 -Goalw [integ_def,znat_def] "z : integ ==> $#1 $* z = z";
   5.363 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.364 -by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
   5.365 -qed "zmult_1";
   5.366 -
   5.367 -Goalw [integ_def] "[| z: integ;  w: integ |] ==> ($~ z) $* w = $~ (z $* w)";
   5.368 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.369 -by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   5.370 -qed "zmult_zminus";
   5.371 -
   5.372 -Addsimps [zmult_0, zmult_1, zmult_zminus];
   5.373 -
   5.374 -Goalw [integ_def] "[| z: integ;  w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
   5.375 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.376 -by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
   5.377 -qed "zmult_zminus_zminus";
   5.378 -
   5.379 -Goalw [integ_def] "[| z: integ;  w: integ |] ==> z $* w = w $* z";
   5.380 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.381 -by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
   5.382 -qed "zmult_commute";
   5.383 -
   5.384 -Goalw [integ_def]
   5.385 -    "[| z1: integ;  z2: integ;  z3: integ |]     \
   5.386 -\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
   5.387 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.388 -by (asm_simp_tac 
   5.389 -    (simpset() addsimps [zmult, add_mult_distrib_left, 
   5.390 -                         add_mult_distrib] @ add_ac @ mult_ac) 1);
   5.391 -qed "zmult_assoc";
   5.392 -
   5.393 -(*For AC rewriting*)
   5.394 -Goal "[| z1:integ;  z2:integ;  z3: integ |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
   5.395 -by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
   5.396 -qed "zmult_left_commute";
   5.397 -
   5.398 -(*Integer multiplication is an AC operator*)
   5.399 -val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
   5.400 -
   5.401 -Goalw [integ_def]
   5.402 -    "[| z1: integ;  z2: integ;  w: integ |] ==> \
   5.403 -\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
   5.404 -by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
   5.405 -by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
   5.406 -by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
   5.407 -qed "zadd_zmult_distrib";
   5.408 -
   5.409 -val integ_typechecks =
   5.410 -    [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
   5.411 -
   5.412 -Addsimps integ_typechecks;
   5.413 -
   5.414 -
   5.415 -
     6.1 --- a/src/ZF/Integ/Integ.thy	Fri Sep 25 12:12:07 1998 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,60 +0,0 @@
     6.4 -(*  Title:      ZF/ex/integ.thy
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1993  University of Cambridge
     6.8 -
     6.9 -The integers as equivalence classes over nat*nat.
    6.10 -*)
    6.11 -
    6.12 -Integ = EquivClass + Arith +
    6.13 -consts
    6.14 -    intrel,integ::      i
    6.15 -    znat        ::      i=>i            ("$# _" [80] 80)
    6.16 -    zminus      ::      i=>i            ("$~ _" [80] 80)
    6.17 -    znegative   ::      i=>o
    6.18 -    zmagnitude  ::      i=>i
    6.19 -    "$*"        ::      [i,i]=>i      (infixl 70)
    6.20 -    "$'/"       ::      [i,i]=>i      (infixl 70) 
    6.21 -    "$'/'/"     ::      [i,i]=>i      (infixl 70)
    6.22 -    "$+"        ::      [i,i]=>i      (infixl 65)
    6.23 -    "$-"        ::      [i,i]=>i      (infixl 65)
    6.24 -    "$<"        ::      [i,i]=>o        (infixl 50)
    6.25 -
    6.26 -defs
    6.27 -
    6.28 -    intrel_def
    6.29 -     "intrel == {p:(nat*nat)*(nat*nat).                 
    6.30 -        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
    6.31 -
    6.32 -    integ_def   "integ == (nat*nat)/intrel"
    6.33 -    
    6.34 -    znat_def    "$# m == intrel `` {<m,0>}"
    6.35 -    
    6.36 -    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
    6.37 -    
    6.38 -    znegative_def
    6.39 -        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
    6.40 -    
    6.41 -    zmagnitude_def
    6.42 -        "zmagnitude(Z) ==
    6.43 -	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
    6.44 -	                   (znegative(Z) & $~ Z = $# m))"
    6.45 -    
    6.46 -    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
    6.47 -      Perhaps a "curried" or even polymorphic congruent predicate would be
    6.48 -      better.*)
    6.49 -    zadd_def
    6.50 -     "Z1 $+ Z2 == 
    6.51 -       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
    6.52 -                           in intrel``{<x1#+x2, y1#+y2>}"
    6.53 -    
    6.54 -    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
    6.55 -    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
    6.56 -    
    6.57 -    (*This illustrates the primitive form of definitions (no patterns)*)
    6.58 -    zmult_def
    6.59 -     "Z1 $* Z2 == 
    6.60 -       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
    6.61 -                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
    6.62 -    
    6.63 - end
     7.1 --- a/src/ZF/IsaMakefile	Fri Sep 25 12:12:07 1998 +0200
     7.2 +++ b/src/ZF/IsaMakefile	Fri Sep 25 13:18:07 1998 +0200
     7.3 @@ -44,7 +44,7 @@
     7.4    ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
     7.5    intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
     7.6    subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
     7.7 -  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Integ.ML Integ/Integ.thy \
     7.8 +  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
     7.9    Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
    7.10  	@$(ISATOOL) usedir -b $(OUT)/FOL ZF
    7.11