installation of cancellation simprocs for the integers
authorpaulson
Thu Aug 10 11:27:34 2000 +0200 (2000-08-10)
changeset 9570e16e168984e1
parent 9569 68400ff46b09
child 9571 c869d1886a32
installation of cancellation simprocs for the integers
src/ZF/Bool.thy
src/ZF/Integ/Bin.ML
src/ZF/Integ/Bin.thy
src/ZF/Integ/Int.ML
src/ZF/Integ/Int.thy
src/ZF/Integ/IntArith.thy
src/ZF/Integ/int_arith.ML
src/ZF/IsaMakefile
src/ZF/Main.thy
src/ZF/Perm.thy
src/ZF/ROOT.ML
src/ZF/Tools/numeral_syntax.ML
src/ZF/arith_data.ML
src/ZF/ex/BinEx.ML
src/ZF/pair.thy
src/ZF/simpdata.ML
src/ZF/subset.thy
src/ZF/upair.ML
src/ZF/upair.thy
     1.1 --- a/src/ZF/Bool.thy	Thu Aug 10 00:45:23 2000 +0200
     1.2 +++ b/src/ZF/Bool.thy	Thu Aug 10 11:27:34 2000 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  2 is equal to bool, but serves a different purpose
     1.5  *)
     1.6  
     1.7 -Bool = upair + 
     1.8 +Bool = pair + 
     1.9  consts
    1.10      bool        :: i
    1.11      cond        :: [i,i,i]=>i
     2.1 --- a/src/ZF/Integ/Bin.ML	Thu Aug 10 00:45:23 2000 +0200
     2.2 +++ b/src/ZF/Integ/Bin.ML	Thu Aug 10 11:27:34 2000 +0200
     2.3 @@ -87,8 +87,7 @@
     2.4  (**** The carry/borrow functions, bin_succ and bin_pred ****)
     2.5  
     2.6  (*NCons preserves the integer value of its argument*)
     2.7 -Goal "[| w: bin; b: bool |] ==>     \
     2.8 -\         integ_of(NCons(w,b)) = integ_of(w BIT b)";
     2.9 +Goal "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)";
    2.10  by (etac bin.elim 1);
    2.11  by (Asm_simp_tac 3);
    2.12  by (ALLGOALS (etac boolE));
    2.13 @@ -134,10 +133,20 @@
    2.14  by (Asm_simp_tac 1);
    2.15  qed "bin_add_Pls";
    2.16  
    2.17 +Goalw [bin_add_def] "w: bin ==> bin_add(w,Pls) = w";
    2.18 +by (etac bin.induct 1);
    2.19 +by Auto_tac;
    2.20 +qed "bin_add_Pls_right";
    2.21 +
    2.22  Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
    2.23  by (Asm_simp_tac 1);
    2.24  qed "bin_add_Min";
    2.25  
    2.26 +Goalw [bin_add_def] "w: bin ==> bin_add(w,Min) = bin_pred(w)";
    2.27 +by (etac bin.induct 1);
    2.28 +by Auto_tac;
    2.29 +qed "bin_add_Min_right";
    2.30 +
    2.31  Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x";
    2.32  by (Simp_tac 1);
    2.33  qed "bin_add_BIT_Pls";
    2.34 @@ -166,6 +175,13 @@
    2.35  by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
    2.36  qed_spec_mp "integ_of_add";
    2.37  
    2.38 +(*Subtraction*)
    2.39 +Goalw [zdiff_def]
    2.40 +     "[| v: bin;  w: bin |]   \
    2.41 +\     ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))";
    2.42 +by (asm_simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
    2.43 +qed "diff_integ_of_eq";
    2.44 +
    2.45  
    2.46  (*** bin_mult: binary multiplication ***)
    2.47  
    2.48 @@ -186,60 +202,64 @@
    2.49  
    2.50  Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
    2.51  by (Simp_tac 1);
    2.52 -qed "bin_succ_BIT1";
    2.53 +qed "bin_succ_1";
    2.54  
    2.55  Goal "bin_succ(w BIT 0) = NCons(w,1)";
    2.56  by (Simp_tac 1);
    2.57 -qed "bin_succ_BIT0";
    2.58 +qed "bin_succ_0";
    2.59  
    2.60  Goal "bin_pred(w BIT 1) = NCons(w,0)";
    2.61  by (Simp_tac 1);
    2.62 -qed "bin_pred_BIT1";
    2.63 +qed "bin_pred_1";
    2.64  
    2.65  Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
    2.66  by (Simp_tac 1);
    2.67 -qed "bin_pred_BIT0";
    2.68 +qed "bin_pred_0";
    2.69  
    2.70  (** extra rules for bin_minus **)
    2.71  
    2.72  Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
    2.73  by (Simp_tac 1);
    2.74 -qed "bin_minus_BIT1";
    2.75 +qed "bin_minus_1";
    2.76  
    2.77  Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
    2.78  by (Simp_tac 1);
    2.79 -qed "bin_minus_BIT0";
    2.80 +qed "bin_minus_0";
    2.81  
    2.82  (** extra rules for bin_add **)
    2.83  
    2.84  Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
    2.85  \                    NCons(bin_add(v, bin_succ(w)), 0)";
    2.86  by (Asm_simp_tac 1);
    2.87 -qed "bin_add_BIT_BIT11";
    2.88 +qed "bin_add_BIT_11";
    2.89  
    2.90  Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) =  \
    2.91  \                    NCons(bin_add(v,w), 1)";
    2.92  by (Asm_simp_tac 1);
    2.93 -qed "bin_add_BIT_BIT10";
    2.94 +qed "bin_add_BIT_10";
    2.95  
    2.96 -Goal "[| w: bin;  y: bool |] ==> \
    2.97 -\           bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
    2.98 +Goal "[| w: bin;  y: bool |] \
    2.99 +\     ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
   2.100  by (Asm_simp_tac 1);
   2.101 -qed "bin_add_BIT_BIT0";
   2.102 +qed "bin_add_BIT_0";
   2.103  
   2.104  (** extra rules for bin_mult **)
   2.105  
   2.106  Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
   2.107  by (Simp_tac 1);
   2.108 -qed "bin_mult_BIT1";
   2.109 +qed "bin_mult_1";
   2.110  
   2.111  Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
   2.112  by (Simp_tac 1);
   2.113 -qed "bin_mult_BIT0";
   2.114 +qed "bin_mult_0";
   2.115  
   2.116  
   2.117  (** Simplification rules with integer constants **)
   2.118  
   2.119 +Goal "$#0 = #0";
   2.120 +by (Simp_tac 1);
   2.121 +qed "int_of_0";
   2.122 +
   2.123  Goal "#0 $+ z = intify(z)";
   2.124  by (Simp_tac 1);
   2.125  qed "zadd_0_intify";
   2.126 @@ -272,6 +292,109 @@
   2.127  
   2.128  Addsimps [zmult_0, zmult_0_right];
   2.129  
   2.130 +Goal "#-1 $* z = $-z";
   2.131 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
   2.132 +qed "zmult_minus1";
   2.133 +
   2.134 +Goal "z $* #-1 = $-z";
   2.135 +by (stac zmult_commute 1);
   2.136 +by (rtac zmult_minus1 1);
   2.137 +qed "zmult_minus1_right";
   2.138 +
   2.139 +Addsimps [zmult_minus1, zmult_minus1_right];
   2.140 +
   2.141 +
   2.142 +(*** Simplification rules for comparison of binary numbers (N Voelker) ***)
   2.143 +
   2.144 +(** Equals (=) **)
   2.145 +
   2.146 +Goalw [iszero_def]
   2.147 +     "[| v: bin;  w: bin |]   \
   2.148 +\     ==> ((integ_of(v)) = integ_of(w)) <-> \
   2.149 +\         iszero (integ_of (bin_add (v, bin_minus(w))))"; 
   2.150 +by (asm_simp_tac (simpset() addsimps
   2.151 +              (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
   2.152 +qed "eq_integ_of_eq"; 
   2.153 +
   2.154 +Goalw [iszero_def] "iszero (integ_of(Pls))"; 
   2.155 +by (Simp_tac 1); 
   2.156 +qed "iszero_integ_of_Pls";
   2.157 +
   2.158 +
   2.159 +Goalw [iszero_def] "~ iszero (integ_of(Min))"; 
   2.160 +by (simp_tac (simpset() addsimps [zminus_equation]) 1);
   2.161 +qed "nonzero_integ_of_Min"; 
   2.162 +
   2.163 +Goalw [iszero_def]
   2.164 +     "[| w: bin; x: bool |] \
   2.165 +\     ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"; 
   2.166 +by (Simp_tac 1);
   2.167 +by (subgoal_tac "integ_of(w) : int" 1);
   2.168 +by (Asm_simp_tac 2);
   2.169 +by (dtac int_cases 1);
   2.170 +by (auto_tac (claset() addSEs [boolE], 
   2.171 +              simpset() addsimps [int_of_add RS sym]));  
   2.172 +by (ALLGOALS (asm_full_simp_tac 
   2.173 +	      (simpset() addsimps zcompare_rls @ 
   2.174 +			  [zminus_zadd_distrib RS sym, int_of_add RS sym])));
   2.175 +by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1);
   2.176 +by (Asm_simp_tac 2);
   2.177 +by (Full_simp_tac 1);
   2.178 +qed "iszero_integ_of_BIT"; 
   2.179 +
   2.180 +Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
   2.181 +by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
   2.182 +qed "iszero_integ_of_0"; 
   2.183 +
   2.184 +Goal "w: bin ==> ~ iszero (integ_of (w BIT 1))"; 
   2.185 +by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
   2.186 +qed "iszero_integ_of_1"; 
   2.187 +
   2.188 +
   2.189 +
   2.190 +(** Less-than (<) **)
   2.191 +
   2.192 +Goalw [zless_def,zdiff_def] 
   2.193 +     "[| v: bin;  w: bin |]   \
   2.194 +\     ==> integ_of(v) $< integ_of(w) \
   2.195 +\         <-> znegative (integ_of (bin_add (v, bin_minus(w))))";
   2.196 +by (asm_simp_tac (simpset() addsimps [integ_of_minus, integ_of_add]) 1);
   2.197 +qed "less_integ_of_eq_neg"; 
   2.198 +
   2.199 +Goal "~ znegative (integ_of(Pls))"; 
   2.200 +by (Simp_tac 1); 
   2.201 +qed "not_neg_integ_of_Pls"; 
   2.202 +
   2.203 +Goal "znegative (integ_of(Min))"; 
   2.204 +by (Simp_tac 1);
   2.205 +qed "neg_integ_of_Min"; 
   2.206 +
   2.207 +Goal "[| w: bin; x: bool |] \
   2.208 +\     ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"; 
   2.209 +by (Asm_simp_tac 1); 
   2.210 +by (subgoal_tac "integ_of(w) : int" 1);
   2.211 +by (Asm_simp_tac 2);
   2.212 +by (dtac int_cases 1);
   2.213 +by (auto_tac (claset() addSEs [boolE], 
   2.214 +              simpset() addsimps [int_of_add RS sym] @ zcompare_rls));  
   2.215 +by (ALLGOALS (asm_full_simp_tac 
   2.216 +	      (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
   2.217 +				   int_of_add RS sym])));
   2.218 +by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1);
   2.219 +by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
   2.220 +by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
   2.221 +qed "neg_integ_of_BIT"; 
   2.222 +
   2.223 +Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"; 
   2.224 +by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1); 
   2.225 +qed "iszero_integ_of_0"; 
   2.226 +
   2.227 +(** Less-than-or-equals (<=) **)
   2.228 +
   2.229 +Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))";
   2.230 +by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   2.231 +qed "le_integ_of_eq_not_less"; 
   2.232 +
   2.233  
   2.234  (*Delete the original rewrites, with their clumsy conditional expressions*)
   2.235  Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   2.236 @@ -281,17 +404,69 @@
   2.237  Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
   2.238  
   2.239  
   2.240 -Addsimps [integ_of_add RS sym,   (*invoke bin_add*)
   2.241 -	  integ_of_minus RS sym, (*invoke bin_minus*)
   2.242 -	  integ_of_mult RS sym,  (*invoke bin_mult*)
   2.243 -	  bin_succ_Pls, bin_succ_Min,
   2.244 -	  bin_succ_BIT1, bin_succ_BIT0,
   2.245 -	  bin_pred_Pls, bin_pred_Min,
   2.246 -	  bin_pred_BIT1, bin_pred_BIT0,
   2.247 -	  bin_minus_Pls, bin_minus_Min,
   2.248 -	  bin_minus_BIT1, bin_minus_BIT0,
   2.249 -	  bin_add_Pls, bin_add_Min, bin_add_BIT_Pls, 
   2.250 -	  bin_add_BIT_Min, bin_add_BIT_BIT0, 
   2.251 -	  bin_add_BIT_BIT10, bin_add_BIT_BIT11,
   2.252 -	  bin_mult_Pls, bin_mult_Min,
   2.253 -	  bin_mult_BIT1, bin_mult_BIT0];
   2.254 +bind_thms ("NCons_simps", 
   2.255 +	   [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
   2.256 +
   2.257 +
   2.258 +bind_thms ("bin_arith_extra_simps",
   2.259 +    [integ_of_add RS sym,   (*invoke bin_add*)
   2.260 +     integ_of_minus RS sym, (*invoke bin_minus*)
   2.261 +     integ_of_mult RS sym,  (*invoke bin_mult*)
   2.262 +     bin_succ_1, bin_succ_0, 
   2.263 +     bin_pred_1, bin_pred_0, 
   2.264 +     bin_minus_1, bin_minus_0,  
   2.265 +     bin_add_Pls_right, bin_add_Min_right,
   2.266 +     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   2.267 +     diff_integ_of_eq,
   2.268 +     bin_mult_1, bin_mult_0] @ NCons_simps);
   2.269 +
   2.270 +
   2.271 +(*For making a minimal simpset, one must include these default simprules
   2.272 +  of thy.  Also include simp_thms, or at least (~False)=True*)
   2.273 +bind_thms ("bin_arith_simps",
   2.274 +    [bin_pred_Pls, bin_pred_Min,
   2.275 +     bin_succ_Pls, bin_succ_Min,
   2.276 +     bin_add_Pls, bin_add_Min,
   2.277 +     bin_minus_Pls, bin_minus_Min,
   2.278 +     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
   2.279 +
   2.280 +(*Simplification of relational operations*)
   2.281 +bind_thms ("bin_rel_simps",
   2.282 +    [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
   2.283 +     iszero_integ_of_0, iszero_integ_of_1,
   2.284 +     less_integ_of_eq_neg,
   2.285 +     not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
   2.286 +     le_integ_of_eq_not_less]);
   2.287 +
   2.288 +Addsimps bin_arith_simps;
   2.289 +Addsimps bin_rel_simps;
   2.290 +
   2.291 +
   2.292 +(** Simplification of arithmetic when nested to the right **)
   2.293 +
   2.294 +Goal "[| v: bin;  w: bin |]   \
   2.295 +\     ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)";
   2.296 +by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   2.297 +qed "add_integ_of_left";
   2.298 +
   2.299 +Goal "[| v: bin;  w: bin |]   \
   2.300 +\     ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)";
   2.301 +by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   2.302 +qed "mult_integ_of_left";
   2.303 +
   2.304 +Goalw [zdiff_def]
   2.305 +    "[| v: bin;  w: bin |]   \
   2.306 +\     ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)";
   2.307 +by (rtac add_integ_of_left 1);
   2.308 +by Auto_tac;  
   2.309 +qed "add_integ_of_diff1";
   2.310 +
   2.311 +Goal "[| v: bin;  w: bin |]   \
   2.312 +\     ==> integ_of(v) $+ (c $- integ_of(w)) = \
   2.313 +\         integ_of (bin_add (v, bin_minus(w))) $+ (c)";
   2.314 +by (stac (diff_integ_of_eq RS sym) 1);
   2.315 +by (ALLGOALS (asm_simp_tac (simpset() addsimps zdiff_def::zadd_ac)));
   2.316 +qed "add_integ_of_diff2";
   2.317 +
   2.318 +Addsimps [add_integ_of_left, mult_integ_of_left,
   2.319 +	  add_integ_of_diff1, add_integ_of_diff2]; 
     3.1 --- a/src/ZF/Integ/Bin.thy	Thu Aug 10 00:45:23 2000 +0200
     3.2 +++ b/src/ZF/Integ/Bin.thy	Thu Aug 10 11:27:34 2000 +0200
     3.3 @@ -18,13 +18,13 @@
     3.4  Division is not defined yet!
     3.5  *)
     3.6  
     3.7 -Bin = Int + Datatype + 
     3.8 +Bin = Int + Datatype +
     3.9  
    3.10  consts  bin :: i
    3.11  datatype
    3.12    "bin" = Pls
    3.13          | Min
    3.14 -        | BIT ("w: bin", "b: bool")	(infixl 90)
    3.15 +        | Bit ("w: bin", "b: bool")	(infixl "BIT" 90)
    3.16  
    3.17  syntax
    3.18    "_Int"           :: xnum => i        ("_")
    3.19 @@ -104,85 +104,9 @@
    3.20      "bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
    3.21  				 NCons(bin_mult(v,w),0))"
    3.22  
    3.23 +setup NumeralSyntax.setup
    3.24 +
    3.25  end
    3.26  
    3.27  
    3.28  ML
    3.29 -
    3.30 -(** Concrete syntax for integers **)
    3.31 -
    3.32 -local
    3.33 -  open Syntax;
    3.34 -
    3.35 -  (* Bits *)
    3.36 -
    3.37 -  fun mk_bit 0 = const "0"
    3.38 -    | mk_bit 1 = const "succ" $ const "0"
    3.39 -    | mk_bit _ = sys_error "mk_bit";
    3.40 -
    3.41 -  fun dest_bit (Const ("0", _)) = 0
    3.42 -    | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
    3.43 -    | dest_bit _ = raise Match;
    3.44 -
    3.45 -
    3.46 -  (* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
    3.47 -
    3.48 -  fun prefix_len _ [] = 0
    3.49 -    | prefix_len pred (x :: xs) =
    3.50 -        if pred x then 1 + prefix_len pred xs else 0;
    3.51 -
    3.52 -  fun mk_bin str =
    3.53 -    let
    3.54 -      val (sign, digs) =
    3.55 -        (case Symbol.explode str of
    3.56 -          "#" :: "-" :: cs => (~1, cs)
    3.57 -        | "#" :: cs => (1, cs)
    3.58 -        | _ => raise ERROR);
    3.59 -
    3.60 -      val zs = prefix_len (equal "0") digs;
    3.61 -
    3.62 -      fun bin_of 0  = []
    3.63 -        | bin_of ~1 = [~1]
    3.64 -        | bin_of n  = (n mod 2) :: bin_of (n div 2);
    3.65 -
    3.66 -      fun term_of [] = const "Pls"
    3.67 -        | term_of [~1] = const "Min"
    3.68 -        | term_of (b :: bs) = const "op BIT" $ term_of bs $ mk_bit b;
    3.69 -    in
    3.70 -      term_of (bin_of (sign * (#1 (read_int digs))))
    3.71 -    end;
    3.72 -
    3.73 -  fun dest_bin tm =
    3.74 -    let
    3.75 -      fun bin_of (Const ("Pls", _)) = []
    3.76 -        | bin_of (Const ("Min", _)) = [~1]
    3.77 -        | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
    3.78 -        | bin_of _ = raise Match;
    3.79 -
    3.80 -      fun integ_of [] = 0
    3.81 -        | integ_of (b :: bs) = b + 2 * integ_of bs;
    3.82 -
    3.83 -      val rev_digs = bin_of tm;
    3.84 -      val (sign, zs) =
    3.85 -        (case rev rev_digs of
    3.86 -          ~1 :: bs => ("-", prefix_len (equal 1) bs)
    3.87 -        | bs => ("", prefix_len (equal 0) bs));
    3.88 -      val num = string_of_int (abs (integ_of rev_digs));
    3.89 -    in
    3.90 -      "#" ^ sign ^ implode (replicate zs "0") ^ num
    3.91 -    end;
    3.92 -
    3.93 -
    3.94 -  (* translation of integer constant tokens to and from binary *)
    3.95 -
    3.96 -  fun int_tr (*"_Int"*) [t as Free (str, _)] =
    3.97 -        (const "integ_of" $
    3.98 -          (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
    3.99 -    | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
   3.100 -
   3.101 -  fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
   3.102 -    | int_tr' (*"integ_of"*) _ = raise Match;
   3.103 -in
   3.104 -  val parse_translation = [("_Int", int_tr)];
   3.105 -  val print_translation = [("integ_of", int_tr')];
   3.106 -end;
     4.1 --- a/src/ZF/Integ/Int.ML	Thu Aug 10 00:45:23 2000 +0200
     4.2 +++ b/src/ZF/Integ/Int.ML	Thu Aug 10 11:27:34 2000 +0200
     4.3 @@ -9,7 +9,6 @@
     4.4  "znegative(z) ==> $# zmagnitude(z) = $- z"
     4.5  "~ znegative(z) ==> $# zmagnitude(z) = z"
     4.6  $+ and $* are monotonic wrt $<
     4.7 -[| m: nat;  n: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
     4.8  *)
     4.9  
    4.10  AddSEs [quotientE];
    4.11 @@ -169,6 +168,15 @@
    4.12  qed "zless_intify2";
    4.13  Addsimps [zless_intify1, zless_intify2];
    4.14  
    4.15 +Goal "intify(x) $<= y <-> x $<= y";
    4.16 +by (simp_tac (simpset() addsimps [zle_def]) 1);
    4.17 +qed "zle_intify1";
    4.18 +
    4.19 +Goal "x $<= intify(y) <-> x $<= y";
    4.20 +by (simp_tac (simpset() addsimps [zle_def]) 1);
    4.21 +qed "zle_intify2";
    4.22 +Addsimps [zle_intify1, zle_intify2];
    4.23 +
    4.24  
    4.25  (**** zminus: unary negation on int ****)
    4.26  
    4.27 @@ -296,6 +304,7 @@
    4.28  by (rtac theI2 1);
    4.29  by Auto_tac;
    4.30  qed "zmagnitude_type";
    4.31 +AddIffs [zmagnitude_type];
    4.32  AddTCs [zmagnitude_type];
    4.33  
    4.34  Goalw [int_def, znegative_def, int_of_def]
    4.35 @@ -317,7 +326,6 @@
    4.36  
    4.37  Addsimps [not_zneg_mag];
    4.38  
    4.39 -
    4.40  Goalw [int_def, znegative_def, int_of_def]
    4.41       "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))"; 
    4.42  by (auto_tac(claset() addSDs [less_imp_succ_add], 
    4.43 @@ -331,6 +339,12 @@
    4.44  
    4.45  Addsimps [zneg_mag];
    4.46  
    4.47 +Goal "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"; 
    4.48 +by (case_tac "znegative(z)" 1);
    4.49 +by (blast_tac (claset() addDs [not_zneg_mag, sym]) 2);
    4.50 +by (blast_tac (claset() addDs [zneg_int_of]) 1);
    4.51 +qed "int_cases"; 
    4.52 +
    4.53  
    4.54  (**** zadd: addition on int ****)
    4.55  
    4.56 @@ -434,6 +448,17 @@
    4.57  by (asm_simp_tac (simpset() addsimps [zadd]) 1);
    4.58  qed "int_of_add";
    4.59  
    4.60 +Goal "$# succ(m) = $# 1 $+ ($# m)";
    4.61 +by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
    4.62 +qed "int_succ_int_1";
    4.63 +
    4.64 +Goalw [int_of_def,zdiff_def]
    4.65 +     "[| m: nat;  n le m |] ==> $# (m #- n) = ($#m) $- ($#n)";
    4.66 +by (ftac lt_nat_in_nat 1);
    4.67 +by (asm_simp_tac (simpset() addsimps [zadd,zminus,add_diff_inverse2]) 2);
    4.68 +by Auto_tac;  
    4.69 +qed "int_of_diff";
    4.70 +
    4.71  Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
    4.72  by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));  
    4.73  qed "raw_zadd_zminus_inverse";
    4.74 @@ -550,11 +575,10 @@
    4.75  qed "zmult_zminus";
    4.76  Addsimps [zmult_zminus];
    4.77  
    4.78 -Goal "($- z) $* ($- w) = (z $* w)";
    4.79 -by (stac zmult_zminus 1);
    4.80 -by (stac zmult_commute 1 THEN stac zmult_zminus 1);
    4.81 -by (simp_tac (simpset() addsimps [zmult_commute])1);
    4.82 -qed "zmult_zminus_zminus";
    4.83 +Goal "w $* ($- z) = $- (w $* z)";
    4.84 +by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute]) 1);
    4.85 +qed "zmult_zminus_right";
    4.86 +Addsimps [zmult_zminus_right];
    4.87  
    4.88  Goalw [int_def]
    4.89      "[| z1: int;  z2: int;  z3: int |]   \
    4.90 @@ -602,6 +626,11 @@
    4.91  
    4.92  (*** Subtraction laws ***)
    4.93  
    4.94 +Goal "z $- w : int";
    4.95 +by (simp_tac (simpset() addsimps [zdiff_def]) 1);
    4.96 +qed "zdiff_type";
    4.97 +AddIffs [zdiff_type];  AddTCs [zdiff_type];
    4.98 +
    4.99  Goal "$#0 $- x = $-x";
   4.100  by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   4.101  qed "zdiff_int0";
   4.102 @@ -616,6 +645,15 @@
   4.103  
   4.104  Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
   4.105  
   4.106 +Goal "$- (z $- y) = y $- z";
   4.107 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
   4.108 +qed "zminus_zdiff_eq";
   4.109 +Addsimps [zminus_zdiff_eq];
   4.110 +
   4.111 +Goal "$- (z $- y) = y $- z";
   4.112 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
   4.113 +qed "zminus_zdiff_eq";
   4.114 +Addsimps [zminus_zdiff_eq];
   4.115  
   4.116  Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
   4.117  by (stac zadd_zmult_distrib 1);
   4.118 @@ -719,21 +757,57 @@
   4.119  by Auto_tac;  
   4.120  qed "zless_trans";
   4.121  
   4.122 +(*** "Less Than or Equals", $<= ***)
   4.123  
   4.124  Goalw [zle_def] "z $<= z";
   4.125  by Auto_tac;  
   4.126  qed "zle_refl";
   4.127  
   4.128 -Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
   4.129 +Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
   4.130 +by Auto_tac;  
   4.131  by (blast_tac (claset() addDs [zless_trans]) 1);
   4.132  qed "zle_anti_sym";
   4.133  
   4.134 -Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
   4.135 +Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
   4.136 +by Auto_tac;  
   4.137  by (blast_tac (claset() addIs [zless_trans]) 1);
   4.138 +val lemma = result();
   4.139 +
   4.140 +Goal "[| x $<= y; y $<= z |] ==> x $<= z";
   4.141 +by (subgoal_tac "intify(x) $<= intify(z)" 1);
   4.142 +by (res_inst_tac [("y", "intify(y)")] lemma 2);
   4.143 +by Auto_tac;  
   4.144  qed "zle_trans";
   4.145  
   4.146 +Goal "[| i $<= j; j $< k |] ==> i $< k";
   4.147 +by (auto_tac (claset(), simpset() addsimps [zle_def]));  
   4.148 +by (blast_tac (claset() addIs [zless_trans]) 1);
   4.149 +by (asm_full_simp_tac (simpset() addsimps [zless_def, zdiff_def, zadd_def]) 1);
   4.150 +qed "zle_zless_trans";
   4.151  
   4.152 -(*** More subtraction laws (for zcompare_rls): useful? ***)
   4.153 +Goal "[| i $< j; j $<= k |] ==> i $< k";
   4.154 +by (auto_tac (claset(), simpset() addsimps [zle_def]));  
   4.155 +by (blast_tac (claset() addIs [zless_trans]) 1);
   4.156 +by (asm_full_simp_tac
   4.157 +    (simpset() addsimps [zless_def, zdiff_def, zminus_def]) 1);
   4.158 +qed "zless_zle_trans";
   4.159 +
   4.160 +Goal "~ (z $< w) <-> (w $<= z)";
   4.161 +by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
   4.162 +by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));  
   4.163 +by (auto_tac (claset(), 
   4.164 +            simpset() addsimps [zless_def, zdiff_def, zadd_def, zminus_def]));
   4.165 +by (fold_tac [zless_def, zdiff_def, zadd_def, zminus_def]);
   4.166 +by Auto_tac;  
   4.167 +qed "not_zless_iff_zle";
   4.168 +
   4.169 +Goal "~ (z $<= w) <-> (w $< z)";
   4.170 +by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
   4.171 +qed "not_zle_iff_zless";
   4.172 +
   4.173 +
   4.174 +
   4.175 +(*** More subtraction laws (for zcompare_rls) ***)
   4.176  
   4.177  Goal "(x $- y) $- z = x $- (y $+ z)";
   4.178  by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
   4.179 @@ -759,16 +833,33 @@
   4.180  by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
   4.181  qed "eq_zdiff_iff";
   4.182  
   4.183 -(**Could not prove these!
   4.184  Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
   4.185 -by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
   4.186 -by Auto_tac;  
   4.187 +by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zdiff_zless_iff]));  
   4.188 +val lemma = result();
   4.189 +
   4.190 +Goal "(x$-y $<= z) <-> (x $<= z $+ y)";
   4.191 +by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
   4.192 +by (Asm_full_simp_tac 1);
   4.193  qed "zdiff_zle_iff";
   4.194  
   4.195 -Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
   4.196 -by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
   4.197 +Goalw [zle_def] "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)";
   4.198 +by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]));  
   4.199 +by (auto_tac (claset(), simpset() addsimps [zdiff_def, zadd_assoc]));  
   4.200 +val lemma = result();
   4.201 +
   4.202 +Goal "(x $<= z$-y) <-> (x $+ y $<= z)";
   4.203 +by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
   4.204 +by (Asm_full_simp_tac 1);
   4.205  qed "zle_zdiff_iff";
   4.206 -**)
   4.207 +
   4.208 +(*This list of rewrites simplifies (in)equalities by bringing subtractions
   4.209 +  to the top and then moving negative terms to the other side.  
   4.210 +  Use with zadd_ac*)
   4.211 +bind_thms ("zcompare_rls",
   4.212 +    [symmetric zdiff_def,
   4.213 +     zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, 
   4.214 +     zdiff_zless_iff, zless_zdiff_iff, zdiff_zle_iff, zle_zdiff_iff, 
   4.215 +     zdiff_eq_iff, eq_zdiff_iff]);
   4.216  
   4.217  
   4.218  (*** Monotonicity/cancellation results that could allow instantiation
   4.219 @@ -816,14 +907,24 @@
   4.220  Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
   4.221  
   4.222  
   4.223 -Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
   4.224 +Goal "(w' $+ z $<= w $+ z) <-> w' $<= w";
   4.225  by (simp_tac (simpset() addsimps [zle_def]) 1);
   4.226  qed "zadd_right_cancel_zle";
   4.227  
   4.228 -Goal "(z $+ w' $<= z $+ w) <->  (intify(w') $<= intify(w))";
   4.229 +Goal "(z $+ w' $<= z $+ w) <->  w' $<= w";
   4.230  by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
   4.231                                    zadd_right_cancel_zle]) 1);
   4.232  qed "zadd_left_cancel_zle";
   4.233  
   4.234  Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
   4.235  
   4.236 +
   4.237 +(*** More inequality lemmas ***)
   4.238 +
   4.239 +Goal "[| x: int;  y: int |] ==> (x = $- y) <-> (y = $- x)";
   4.240 +by Auto_tac;
   4.241 +qed "equation_zminus";
   4.242 +
   4.243 +Goal "[| x: int;  y: int |] ==> ($- x = y) <-> ($- y = x)";
   4.244 +by Auto_tac;
   4.245 +qed "zminus_equation";
     5.1 --- a/src/ZF/Integ/Int.thy	Thu Aug 10 00:45:23 2000 +0200
     5.2 +++ b/src/ZF/Integ/Int.thy	Thu Aug 10 11:27:34 2000 +0200
     5.3 @@ -30,7 +30,10 @@
     5.4  
     5.5    znegative   ::      i=>o
     5.6      "znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
     5.7 -  
     5.8 +
     5.9 +  iszero      ::      i=>o
    5.10 +    "iszero(z) == z = $# 0"
    5.11 +    
    5.12    zmagnitude  ::      i=>i
    5.13      "zmagnitude(z) ==
    5.14       THE m. m : nat & ((~ znegative(z) & z = $# m) |
    5.15 @@ -62,7 +65,7 @@
    5.16       "z1 $< z2 == znegative(z1 $- z2)"
    5.17    
    5.18    zle          ::      [i,i]=>o      (infixl "$<=" 50)
    5.19 -     "z1 $<= z2 == z1 $< z2 | z1=z2"
    5.20 +     "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
    5.21    
    5.22  (*div and mod await definitions!*)
    5.23  consts
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/ZF/Integ/IntArith.thy	Thu Aug 10 11:27:34 2000 +0200
     6.3 @@ -0,0 +1,5 @@
     6.4 +
     6.5 +theory IntArith = Bin
     6.6 +files "int_arith.ML":
     6.7 +
     6.8 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/ZF/Integ/int_arith.ML	Thu Aug 10 11:27:34 2000 +0200
     7.3 @@ -0,0 +1,391 @@
     7.4 +(*  Title:      ZF/Integ/int_arith.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:    Larry Paulson
     7.7 +    Copyright   2000  University of Cambridge
     7.8 +
     7.9 +Simprocs for linear arithmetic.
    7.10 +*)
    7.11 +
    7.12 +(*** Simprocs for numeric literals ***)
    7.13 +
    7.14 +(** Combining of literal coefficients in sums of products **)
    7.15 +
    7.16 +Goal "(x $< y) <-> (x$-y $< #0)";
    7.17 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.18 +qed "zless_iff_zdiff_zless_0";
    7.19 +
    7.20 +Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
    7.21 +by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
    7.22 +qed "eq_iff_zdiff_eq_0";
    7.23 +
    7.24 +Goal "(x $<= y) <-> (x$-y $<= #0)";
    7.25 +by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
    7.26 +qed "zle_iff_zdiff_zle_0";
    7.27 +
    7.28 +
    7.29 +(** For combine_numerals **)
    7.30 +
    7.31 +Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
    7.32 +by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
    7.33 +qed "left_zadd_zmult_distrib";
    7.34 +
    7.35 +
    7.36 +(** For cancel_numerals **)
    7.37 +
    7.38 +val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
    7.39 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    7.40 +			   zle_iff_zdiff_zle_0] @
    7.41 +		        map (inst "y" "n")
    7.42 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    7.43 +			   zle_iff_zdiff_zle_0];
    7.44 +
    7.45 +Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
    7.46 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    7.47 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.48 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    7.49 +qed "eq_add_iff1";
    7.50 +
    7.51 +Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
    7.52 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    7.53 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.54 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    7.55 +qed "eq_add_iff2";
    7.56 +
    7.57 +Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
    7.58 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    7.59 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    7.60 +qed "less_add_iff1";
    7.61 +
    7.62 +Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
    7.63 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    7.64 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    7.65 +qed "less_add_iff2";
    7.66 +
    7.67 +Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= intify(n))";
    7.68 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    7.69 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.70 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    7.71 +qed "le_add_iff1";
    7.72 +
    7.73 +Goal "(i$*u $+ m $<= j$*u $+ n) <-> (intify(m) $<= (j$-i)$*u $+ n)";
    7.74 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    7.75 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    7.76 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    7.77 +qed "le_add_iff2";
    7.78 +
    7.79 +
    7.80 +structure Int_Numeral_Simprocs =
    7.81 +struct
    7.82 +
    7.83 +(*Utilities*)
    7.84 +
    7.85 +val integ_of_const = Const ("Bin.integ_of", iT --> iT);
    7.86 +
    7.87 +fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
    7.88 +
    7.89 +(*Decodes a binary INTEGER*)
    7.90 +fun dest_numeral (Const("Bin.integ_of", _) $ w) = 
    7.91 +     (NumeralSyntax.dest_bin w
    7.92 +      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    7.93 +  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    7.94 +
    7.95 +fun find_first_numeral past (t::terms) =
    7.96 +	((dest_numeral t, rev past @ terms)
    7.97 +	 handle TERM _ => find_first_numeral (t::past) terms)
    7.98 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    7.99 +
   7.100 +val zero = mk_numeral 0;
   7.101 +val mk_plus = FOLogic.mk_binop "Int.zadd";
   7.102 +
   7.103 +val iT = Ind_Syntax.iT;
   7.104 +
   7.105 +val zminus_const = Const ("Int.zminus", iT --> iT);
   7.106 +
   7.107 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   7.108 +fun mk_sum []        = zero
   7.109 +  | mk_sum [t,u]     = mk_plus (t, u)
   7.110 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   7.111 +
   7.112 +(*this version ALWAYS includes a trailing zero*)
   7.113 +fun long_mk_sum []        = zero
   7.114 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   7.115 +
   7.116 +val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
   7.117 +
   7.118 +(*decompose additions AND subtractions as a sum*)
   7.119 +fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
   7.120 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   7.121 +  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
   7.122 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   7.123 +  | dest_summing (pos, t, ts) =
   7.124 +	if pos then t::ts else zminus_const$t :: ts;
   7.125 +
   7.126 +fun dest_sum t = dest_summing (true, t, []);
   7.127 +
   7.128 +val mk_diff = FOLogic.mk_binop "Int.zdiff";
   7.129 +val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
   7.130 +
   7.131 +val one = mk_numeral 1;
   7.132 +val mk_times = FOLogic.mk_binop "Int.zmult";
   7.133 +
   7.134 +fun mk_prod [] = one
   7.135 +  | mk_prod [t] = t
   7.136 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   7.137 +                        else mk_times (t, mk_prod ts);
   7.138 +
   7.139 +val dest_times = FOLogic.dest_bin "Int.zmult" iT;
   7.140 +
   7.141 +fun dest_prod t =
   7.142 +      let val (t,u) = dest_times t 
   7.143 +      in  dest_prod t @ dest_prod u  end
   7.144 +      handle TERM _ => [t];
   7.145 +
   7.146 +(*DON'T do the obvious simplifications; that would create special cases*) 
   7.147 +fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
   7.148 +
   7.149 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   7.150 +fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
   7.151 +  | dest_coeff sign t =
   7.152 +    let val ts = sort Term.term_ord (dest_prod t)
   7.153 +	val (n, ts') = find_first_numeral [] ts
   7.154 +                          handle TERM _ => (1, ts)
   7.155 +    in (sign*n, mk_prod ts') end;
   7.156 +
   7.157 +(*Find first coefficient-term THAT MATCHES u*)
   7.158 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   7.159 +  | find_first_coeff past u (t::terms) =
   7.160 +	let val (n,u') = dest_coeff 1 t
   7.161 +	in  if u aconv u' then (n, rev past @ terms)
   7.162 +			  else find_first_coeff (t::past) u terms
   7.163 +	end
   7.164 +	handle TERM _ => find_first_coeff (t::past) u terms;
   7.165 +
   7.166 +
   7.167 +(*Simplify #1*n and n*#1 to n*)
   7.168 +val add_0s = [zadd_0_intify, zadd_0_right_intify];
   7.169 +
   7.170 +val mult_1s = [zmult_1_intify, zmult_1_right_intify, 
   7.171 +               zmult_minus1, zmult_minus1_right];
   7.172 +
   7.173 +val tc_rules = [integ_of_type, intify_in_int, 
   7.174 +                zadd_type, zdiff_type, zmult_type] @ bin.intrs;
   7.175 +val intifys = [intify_ident, zadd_intify1, zadd_intify2,
   7.176 +               zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
   7.177 +               zless_intify1, zless_intify2, zle_intify1, zle_intify2];
   7.178 +
   7.179 +(*To perform binary arithmetic*)
   7.180 +val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
   7.181 +
   7.182 +(*To evaluate binary negations of coefficients*)
   7.183 +val zminus_simps = NCons_simps @
   7.184 +                   [integ_of_minus RS sym, 
   7.185 +		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   7.186 +		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   7.187 +
   7.188 +(*To let us treat subtraction as addition*)
   7.189 +val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   7.190 +
   7.191 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   7.192 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
   7.193 +                      (s, TypeInfer.anyT ["logic"]);
   7.194 +val prep_pats = map prep_pat;
   7.195 +
   7.196 +structure CancelNumeralsCommon =
   7.197 +  struct
   7.198 +  val mk_sum    	= mk_sum
   7.199 +  val dest_sum		= dest_sum
   7.200 +  val mk_coeff		= mk_coeff
   7.201 +  val dest_coeff	= dest_coeff 1
   7.202 +  val find_first_coeff	= find_first_coeff []
   7.203 +  val trans_tac		= ArithData.gen_trans_tac iff_trans
   7.204 +  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
   7.205 +                                    zminus_simps@zadd_ac
   7.206 +  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
   7.207 +                                    bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
   7.208 +  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
   7.209 +			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   7.210 +  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
   7.211 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   7.212 +  end;
   7.213 +
   7.214 +
   7.215 +structure EqCancelNumerals = CancelNumeralsFun
   7.216 + (open CancelNumeralsCommon
   7.217 +  val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   7.218 +  val mk_bal   = FOLogic.mk_eq
   7.219 +  val dest_bal = FOLogic.dest_bin "op =" iT
   7.220 +  val bal_add1 = eq_add_iff1 RS iff_trans
   7.221 +  val bal_add2 = eq_add_iff2 RS iff_trans
   7.222 +);
   7.223 +
   7.224 +structure LessCancelNumerals = CancelNumeralsFun
   7.225 + (open CancelNumeralsCommon
   7.226 +  val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   7.227 +  val mk_bal   = FOLogic.mk_binrel "Int.zless"
   7.228 +  val dest_bal = FOLogic.dest_bin "Int.zless" iT
   7.229 +  val bal_add1 = less_add_iff1 RS iff_trans
   7.230 +  val bal_add2 = less_add_iff2 RS iff_trans
   7.231 +);
   7.232 +
   7.233 +structure LeCancelNumerals = CancelNumeralsFun
   7.234 + (open CancelNumeralsCommon
   7.235 +  val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   7.236 +  val mk_bal   = FOLogic.mk_binrel "Int.zle"
   7.237 +  val dest_bal = FOLogic.dest_bin "Int.zle" iT
   7.238 +  val bal_add1 = le_add_iff1 RS iff_trans
   7.239 +  val bal_add2 = le_add_iff2 RS iff_trans
   7.240 +);
   7.241 +
   7.242 +val cancel_numerals = 
   7.243 +  map prep_simproc
   7.244 +   [("inteq_cancel_numerals",
   7.245 +     prep_pats ["l $+ m = n", "l = m $+ n", 
   7.246 +		"l $- m = n", "l = m $- n", 
   7.247 +		"l $* m = n", "l = m $* n"], 
   7.248 +     EqCancelNumerals.proc),
   7.249 +    ("intless_cancel_numerals", 
   7.250 +     prep_pats ["l $+ m $< n", "l $< m $+ n", 
   7.251 +		"l $- m $< n", "l $< m $- n", 
   7.252 +		"l $* m $< n", "l $< m $* n"], 
   7.253 +     LessCancelNumerals.proc),
   7.254 +    ("intle_cancel_numerals", 
   7.255 +     prep_pats ["l $+ m $<= n", "l $<= m $+ n", 
   7.256 +		"l $- m $<= n", "l $<= m $- n", 
   7.257 +		"l $* m $<= n", "l $<= m $* n"], 
   7.258 +     LeCancelNumerals.proc)];
   7.259 +
   7.260 +
   7.261 +(*version without the hyps argument*)
   7.262 +fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
   7.263 +
   7.264 +structure CombineNumeralsData =
   7.265 +  struct
   7.266 +  val add		= op + : int*int -> int 
   7.267 +  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x $+ #3*x *)
   7.268 +  val dest_sum		= dest_sum
   7.269 +  val mk_coeff		= mk_coeff
   7.270 +  val dest_coeff	= dest_coeff 1
   7.271 +  val left_distrib	= left_zadd_zmult_distrib RS trans
   7.272 +  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   7.273 +  val trans_tac         = ArithData.gen_trans_tac trans
   7.274 +  val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
   7.275 +                                    zminus_simps@zadd_ac
   7.276 +  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
   7.277 +                                    bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
   7.278 +  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
   7.279 +			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   7.280 +  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps))
   7.281 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s@mult_1s)
   7.282 +  end;
   7.283 +
   7.284 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   7.285 +  
   7.286 +val combine_numerals = 
   7.287 +    prep_simproc ("int_combine_numerals",
   7.288 +		  prep_pats ["i $+ j", "i $- j"],
   7.289 +		  CombineNumerals.proc);
   7.290 +
   7.291 +
   7.292 +
   7.293 +(** Constant folding for integer multiplication **)
   7.294 +
   7.295 +(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   7.296 +  the "sum" of #3, x, #4; the literals are then multiplied*)
   7.297 +structure CombineNumeralsProdData =
   7.298 +  struct
   7.299 +  val add		= op * : int*int -> int
   7.300 +  val mk_sum    	= mk_prod
   7.301 +  val dest_sum		= dest_prod
   7.302 +  fun mk_coeff (k, t) = mk_numeral k
   7.303 +  val dest_coeff	= dest_coeff 1
   7.304 +  val left_distrib	= zmult_assoc RS sym RS trans
   7.305 +  val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   7.306 +  val trans_tac         = ArithData.gen_trans_tac trans
   7.307 +  val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
   7.308 +  val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
   7.309 +                                    bin_simps@zmult_ac@tc_rules@intifys
   7.310 +  val norm_tac		= ALLGOALS (asm_simp_tac norm_tac_ss1)
   7.311 +			  THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
   7.312 +  val numeral_simp_tac	= ALLGOALS (simp_tac (ZF_ss addsimps bin_simps))
   7.313 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s)
   7.314 +  end;
   7.315 +
   7.316 +
   7.317 +structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   7.318 +  
   7.319 +val combine_numerals_prod = 
   7.320 +    prep_simproc ("int_combine_numerals_prod",
   7.321 +		  prep_pats ["i $* j", "i $* j"],
   7.322 +		  CombineNumeralsProd.proc);
   7.323 +
   7.324 +end;
   7.325 +
   7.326 +
   7.327 +Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   7.328 +Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
   7.329 +	     Int_Numeral_Simprocs.combine_numerals_prod];
   7.330 +
   7.331 +
   7.332 +(*examples:*)
   7.333 +(*
   7.334 +print_depth 22;
   7.335 +set timing;
   7.336 +set trace_simp;
   7.337 +fun test s = (Goal s; by (Asm_simp_tac 1)); 
   7.338 +val sg = #sign (rep_thm (topthm()));
   7.339 +val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
   7.340 +val (t,_) = FOLogic.dest_eq t;
   7.341 +
   7.342 +(*combine_numerals_prod (products of separate literals) *)
   7.343 +test "#5 $* x $* #3 = y";
   7.344 +
   7.345 +test "y2 $+ ?x42 = y $+ y2";
   7.346 +
   7.347 +test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
   7.348 +
   7.349 +test "#9$*x $+ y = x$*#23 $+ z";
   7.350 +test "y $+ x = x $+ z";
   7.351 +
   7.352 +test "x : int ==> x $+ y $+ z = x $+ z";
   7.353 +test "x : int ==> y $+ (z $+ x) = z $+ x";
   7.354 +test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
   7.355 +test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
   7.356 +
   7.357 +test "#-3 $* x $+ y $<= x $* #2 $+ z";
   7.358 +test "y $+ x $<= x $+ z";
   7.359 +test "x $+ y $+ z $<= x $+ z";
   7.360 +
   7.361 +test "y $+ (z $+ x) $< z $+ x";
   7.362 +test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
   7.363 +test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
   7.364 +
   7.365 +test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
   7.366 +test "u : int ==> #2 $* u = u";
   7.367 +test "(i $+ j $+ #12 $+ k) $- #15 = y";
   7.368 +test "(i $+ j $+ #12 $+ k) $- #5 = y";
   7.369 +
   7.370 +test "y $- b $< b";
   7.371 +test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
   7.372 +
   7.373 +test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
   7.374 +test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
   7.375 +test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
   7.376 +test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
   7.377 +
   7.378 +test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
   7.379 +test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
   7.380 +
   7.381 +test "#2 $* y $+ #3 $* z $+ #6 $* w $+ #2 $* y $+ #3 $* z $+ #2 $* u = #2 $* y' $+ #3 $* z' $+ #6 $* w' $+ #2 $* y' $+ #3 $* z' $+ u $+ vv";
   7.382 +
   7.383 +test "a $+ $-(b$+c) $+ b = d";
   7.384 +test "a $+ $-(b$+c) $- b = d";
   7.385 +
   7.386 +(*negative numerals*)
   7.387 +test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
   7.388 +test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
   7.389 +test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
   7.390 +test "(i $+ j $+ #-12 $+ k) $- #15 = y";
   7.391 +test "(i $+ j $+ #12 $+ k) $- #-15 = y";
   7.392 +test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
   7.393 +*)
   7.394 +
     8.1 --- a/src/ZF/IsaMakefile	Thu Aug 10 00:45:23 2000 +0200
     8.2 +++ b/src/ZF/IsaMakefile	Thu Aug 10 11:27:34 2000 +0200
     8.3 @@ -33,11 +33,14 @@
     8.4    Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML	\
     8.5    Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML		\
     8.6    Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML	\
     8.7 -  Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy	\
     8.8 +  Integ/Int.thy Integ/twos_compl.ML \
     8.9 +  Integ/int_arith.ML Integ/IntArith.thy \
    8.10 +  Let.ML Let.thy List.ML List.thy	\
    8.11    Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML		\
    8.12    OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy	\
    8.13    Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML	\
    8.14 -  Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML			\
    8.15 +  Rel.ML Rel.thy Sum.ML Sum.thy \
    8.16 +  Tools/numeral_syntax.ML Tools/cartprod.ML			\
    8.17    Tools/datatype_package.ML Tools/induct_tacs.ML			\
    8.18    Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML	\
    8.19    Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML	\
     9.1 --- a/src/ZF/Main.thy	Thu Aug 10 00:45:23 2000 +0200
     9.2 +++ b/src/ZF/Main.thy	Thu Aug 10 11:27:34 2000 +0200
     9.3 @@ -2,5 +2,5 @@
     9.4  (*$Id$
     9.5    theory Main includes everything*)
     9.6  
     9.7 -Main = Update + InfDatatype + List + EquivClass + Bin
     9.8 +Main = Update + InfDatatype + List + EquivClass + IntArith
     9.9  
    10.1 --- a/src/ZF/Perm.thy	Thu Aug 10 00:45:23 2000 +0200
    10.2 +++ b/src/ZF/Perm.thy	Thu Aug 10 11:27:34 2000 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4    -- Lemmas for the Schroeder-Bernstein Theorem
    10.5  *)
    10.6  
    10.7 -Perm = upair + mono + func +
    10.8 +Perm = mono + func +
    10.9  consts
   10.10    O     :: [i,i]=>i      (infixr 60)
   10.11  
    11.1 --- a/src/ZF/ROOT.ML	Thu Aug 10 00:45:23 2000 +0200
    11.2 +++ b/src/ZF/ROOT.ML	Thu Aug 10 11:27:34 2000 +0200
    11.3 @@ -19,9 +19,8 @@
    11.4  use     "thy_syntax";
    11.5  
    11.6  use "~~/src/Provers/Arith/cancel_numerals.ML";
    11.7 +use "~~/src/Provers/Arith/combine_numerals.ML";
    11.8  
    11.9 -use_thy "ZF";
   11.10 -use     "Tools/typechk";
   11.11  use_thy "mono";
   11.12  use     "ind_syntax";
   11.13  use     "Tools/cartprod";
   11.14 @@ -32,6 +31,7 @@
   11.15  use_thy "QUniv";
   11.16  use     "Tools/datatype_package";
   11.17  
   11.18 +use     "Tools/numeral_syntax";
   11.19  (*the all-in-one theory*)
   11.20  with_path "Integ" use_thy "Main";
   11.21  
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/ZF/Tools/numeral_syntax.ML	Thu Aug 10 11:27:34 2000 +0200
    12.3 @@ -0,0 +1,117 @@
    12.4 +(*  Title:      ZF/Tools/numeral_syntax.ML
    12.5 +    ID:         $Id$
    12.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +
    12.8 +Concrete syntax for generic numerals.  Assumes consts and syntax of
    12.9 +theory ZF/Integ/Bin.
   12.10 +*)
   12.11 +
   12.12 +signature NUMERAL_SYNTAX =
   12.13 +sig
   12.14 +  val dest_bin : term -> int
   12.15 +  val mk_bin   : int -> term
   12.16 +  val int_tr   : term list -> term
   12.17 +  val int_tr'  : bool -> typ -> term list -> term
   12.18 +  val setup    : (theory -> theory) list
   12.19 +end;
   12.20 +
   12.21 +structure NumeralSyntax: NUMERAL_SYNTAX =
   12.22 +struct
   12.23 +
   12.24 +open Syntax;
   12.25 +
   12.26 +(* Bits *)
   12.27 +
   12.28 +val zero = Const("0", iT);
   12.29 +val succ = Const("succ", iT --> iT);
   12.30 +
   12.31 +fun mk_bit 0 = zero
   12.32 +  | mk_bit 1 = succ$zero
   12.33 +  | mk_bit _ = sys_error "mk_bit";
   12.34 +
   12.35 +fun dest_bit (Const ("0", _)) = 0
   12.36 +  | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
   12.37 +  | dest_bit _ = raise Match;
   12.38 +
   12.39 +
   12.40 +(* Bit strings *)   (*we try to handle superfluous leading digits nicely*)
   12.41 +
   12.42 +fun prefix_len _ [] = 0
   12.43 +  | prefix_len pred (x :: xs) =
   12.44 +      if pred x then 1 + prefix_len pred xs else 0;
   12.45 +
   12.46 +fun scan_int str =
   12.47 +  let val (sign, digs) =
   12.48 +       (case Symbol.explode str of
   12.49 +	 "#" :: "-" :: cs => (~1, cs)
   12.50 +       | "#" :: cs => (1, cs)
   12.51 +       | _ => raise ERROR);
   12.52 +
   12.53 +  in  sign * (#1 (read_int digs))  end;
   12.54 +
   12.55 +
   12.56 +val pls_const = Const ("Bin.bin.Pls", iT)
   12.57 +and min_const = Const ("Bin.bin.Min", iT)
   12.58 +and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
   12.59 +
   12.60 +fun mk_bin i =
   12.61 +  let fun bin_of 0  = []
   12.62 +	| bin_of ~1 = [~1]
   12.63 +	| bin_of n  = (n mod 2) :: bin_of (n div 2);
   12.64 +
   12.65 +      fun term_of []   = pls_const
   12.66 +	| term_of [~1] = min_const
   12.67 +	| term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
   12.68 +  in
   12.69 +    term_of (bin_of i)
   12.70 +  end;
   12.71 +
   12.72 +(*we consider all "spellings", since they could vary depending on the caller*)
   12.73 +fun bin_of (Const ("Pls", _)) = []
   12.74 +  | bin_of (Const ("bin.Pls", _)) = []
   12.75 +  | bin_of (Const ("Bin.bin.Pls", _)) = []
   12.76 +  | bin_of (Const ("Min", _)) = [~1]
   12.77 +  | bin_of (Const ("bin.Min", _)) = [~1]
   12.78 +  | bin_of (Const ("Bin.bin.Min", _)) = [~1]
   12.79 +  | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   12.80 +  | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   12.81 +  | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
   12.82 +  | bin_of _ = raise Match;
   12.83 +
   12.84 +fun integ_of [] = 0
   12.85 +  | integ_of (b :: bs) = b + 2 * integ_of bs;
   12.86 +
   12.87 +val dest_bin = integ_of o bin_of;
   12.88 +
   12.89 +(*leading 0s and (for negative numbers) -1s cause complications,
   12.90 +  though they should never arise in normal use.*)
   12.91 +fun show_int t =
   12.92 +  let
   12.93 +    val rev_digs = bin_of t;
   12.94 +    val (sign, zs) =
   12.95 +	(case rev rev_digs of
   12.96 +	     ~1 :: bs => ("-", prefix_len (equal 1) bs)
   12.97 +	   | bs =>       ("",  prefix_len (equal 0) bs));
   12.98 +    val num = string_of_int (abs (integ_of rev_digs));
   12.99 +  in
  12.100 +    "#" ^ sign ^ implode (replicate zs "0") ^ num
  12.101 +  end;
  12.102 +
  12.103 +
  12.104 +
  12.105 +(* translation of integer constant tokens to and from binary *)
  12.106 +
  12.107 +fun int_tr (*"_Int"*) [t as Free (str, _)] =
  12.108 +      (const "integ_of" $
  12.109 +	(mk_bin (scan_int str) handle ERROR => raise TERM ("int_tr", [t])))
  12.110 +  | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
  12.111 +
  12.112 +fun int_tr' _ _ (*"integ_of"*) [t] = const "_Int" $ free (show_int t)
  12.113 +  | int_tr' (_:bool) (_:typ)     _ = raise Match;
  12.114 +
  12.115 +
  12.116 +val setup =
  12.117 + [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
  12.118 +  Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
  12.119 +
  12.120 +end;
    13.1 --- a/src/ZF/arith_data.ML	Thu Aug 10 00:45:23 2000 +0200
    13.2 +++ b/src/ZF/arith_data.ML	Thu Aug 10 11:27:34 2000 +0200
    13.3 @@ -8,9 +8,16 @@
    13.4  
    13.5  signature ARITH_DATA =
    13.6  sig
    13.7 +  (*the main outcome*)
    13.8    val nat_cancel: simproc list
    13.9 +  (*tools for use in similar applications*)
   13.10 +  val gen_trans_tac: thm -> thm option -> tactic
   13.11 +  val prove_conv: string -> tactic list -> Sign.sg -> 
   13.12 +                  thm list -> term * term -> thm option
   13.13 +  val simplify_meta_eq: thm list -> thm -> thm
   13.14  end;
   13.15  
   13.16 +
   13.17  structure ArithData: ARITH_DATA =
   13.18  struct
   13.19  
   13.20 @@ -21,11 +28,7 @@
   13.21  fun mk_succ t = succ $ t;
   13.22  val one = mk_succ zero;
   13.23  
   13.24 -(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
   13.25 -fun mk_binop_i  c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
   13.26 -fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
   13.27 -
   13.28 -val mk_plus = mk_binop_i "Arith.add";
   13.29 +val mk_plus = FOLogic.mk_binop "Arith.add";
   13.30  
   13.31  (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   13.32  fun mk_sum []        = zero
   13.33 @@ -81,7 +84,7 @@
   13.34  (*** Use CancelNumerals simproc without binary numerals, 
   13.35       just for cancellation ***)
   13.36  
   13.37 -val mk_times = mk_binop_i "Arith.mult";
   13.38 +val mk_times = FOLogic.mk_binop "Arith.mult";
   13.39  
   13.40  fun mk_prod [] = one
   13.41    | mk_prod [t] = t
   13.42 @@ -120,14 +123,14 @@
   13.43  val mult_1s = [mult_1_natify, mult_1_right_natify];
   13.44  val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
   13.45  val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
   13.46 -               add_natify1, add_natify2, diff_natify1, diff_natify2];
   13.47 +               diff_natify1, diff_natify2];
   13.48  
   13.49  (*Final simplification: cancel + and **)
   13.50  fun simplify_meta_eq rules =
   13.51      mk_meta_eq o
   13.52      simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2] 
   13.53                       delsimps iff_simps (*these could erase the whole rule!*)
   13.54 -		     addsimps rules)
   13.55 +		     addsimps rules);
   13.56  
   13.57  val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
   13.58  
   13.59 @@ -161,7 +164,7 @@
   13.60  structure LessCancelNumerals = CancelNumeralsFun
   13.61   (open CancelNumeralsCommon
   13.62    val prove_conv = prove_conv "natless_cancel_numerals"
   13.63 -  val mk_bal   = mk_binrel_i "Ordinal.op <"
   13.64 +  val mk_bal   = FOLogic.mk_binrel "Ordinal.op <"
   13.65    val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
   13.66    val bal_add1 = less_add_iff RS iff_trans
   13.67    val bal_add2 = less_add_iff RS iff_trans
   13.68 @@ -171,7 +174,7 @@
   13.69  structure DiffCancelNumerals = CancelNumeralsFun
   13.70   (open CancelNumeralsCommon
   13.71    val prove_conv = prove_conv "natdiff_cancel_numerals"
   13.72 -  val mk_bal   = mk_binop_i "Arith.diff"
   13.73 +  val mk_bal   = FOLogic.mk_binop "Arith.diff"
   13.74    val dest_bal = FOLogic.dest_bin "Arith.diff" iT
   13.75    val bal_add1 = diff_add_eq RS trans
   13.76    val bal_add2 = diff_add_eq RS trans
    14.1 --- a/src/ZF/ex/BinEx.ML	Thu Aug 10 00:45:23 2000 +0200
    14.2 +++ b/src/ZF/ex/BinEx.ML	Thu Aug 10 11:27:34 2000 +0200
    14.3 @@ -51,3 +51,30 @@
    14.4  Goal "#1359  $*  #-2468 = #-3354012";
    14.5  by (Simp_tac 1);    (*1.04 secs*)
    14.6  result();
    14.7 +
    14.8 +
    14.9 +(** Comparisons **)
   14.10 +
   14.11 +Goal "(#89) $* #10 ~= #889";  
   14.12 +by (Simp_tac 1); 
   14.13 +result();
   14.14 +
   14.15 +Goal "(#13) $< #18 $- #4";  
   14.16 +by (Simp_tac 1); 
   14.17 +result();
   14.18 +
   14.19 +Goal "(#-345) $< #-242 $+ #-100";  
   14.20 +by (Simp_tac 1); 
   14.21 +result();
   14.22 +
   14.23 +Goal "(#13557456) $< #18678654";  
   14.24 +by (Simp_tac 1); 
   14.25 +result();
   14.26 +
   14.27 +Goal "(#999999) $<= (#1000001 $+ #1) $- #2";  
   14.28 +by (Simp_tac 1); 
   14.29 +result();
   14.30 +
   14.31 +Goal "(#1234567) $<= #1234567";  
   14.32 +by (Simp_tac 1); 
   14.33 +result();
    15.1 --- a/src/ZF/pair.thy	Thu Aug 10 00:45:23 2000 +0200
    15.2 +++ b/src/ZF/pair.thy	Thu Aug 10 11:27:34 2000 +0200
    15.3 @@ -1,4 +1,5 @@
    15.4 -(*Dummy theory to document dependencies *)
    15.5 +theory pair = upair
    15.6 +files "simpdata":
    15.7 +end
    15.8  
    15.9 -pair = upair
   15.10  
    16.1 --- a/src/ZF/simpdata.ML	Thu Aug 10 00:45:23 2000 +0200
    16.2 +++ b/src/ZF/simpdata.ML	Thu Aug 10 11:27:34 2000 +0200
    16.3 @@ -10,7 +10,7 @@
    16.4  
    16.5  local
    16.6    (*For proving rewrite rules*)
    16.7 -  fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
    16.8 +  fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1]));
    16.9  
   16.10  in
   16.11  
   16.12 @@ -106,7 +106,8 @@
   16.13  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
   16.14  
   16.15  simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
   16.16 -                           addsplits [split_if]
   16.17 +                           addcongs [if_weak_cong]
   16.18 +		           addsplits [split_if]
   16.19                             setSolver (mk_solver "types" Type_solver_tac);
   16.20  
   16.21  val ZF_ss = simpset();
    17.1 --- a/src/ZF/subset.thy	Thu Aug 10 00:45:23 2000 +0200
    17.2 +++ b/src/ZF/subset.thy	Thu Aug 10 11:27:34 2000 +0200
    17.3 @@ -1,3 +1,3 @@
    17.4  (*Dummy theory to document dependencies *)
    17.5  
    17.6 -subset = upair
    17.7 +subset = pair
    18.1 --- a/src/ZF/upair.ML	Thu Aug 10 00:45:23 2000 +0200
    18.2 +++ b/src/ZF/upair.ML	Thu Aug 10 11:27:34 2000 +0200
    18.3 @@ -269,6 +269,12 @@
    18.4  by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
    18.5  qed "if_cong";
    18.6  
    18.7 +(*Prevents simplification of x and y: faster and allows the execution
    18.8 +  of functional programs. NOW THE DEFAULT.*)
    18.9 +Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)";
   18.10 +by (Asm_simp_tac 1);
   18.11 +qed "if_weak_cong";
   18.12 +
   18.13  (*Not needed for rewriting, since P would rewrite to True anyway*)
   18.14  Goalw [if_def] "P ==> (if P then a else b) = a";
   18.15  by (Blast_tac 1);
   18.16 @@ -398,4 +404,3 @@
   18.17  (*Not needed now that cons is available.  Deletion reduces the search space.*)
   18.18  Delrules [UpairI1,UpairI2,UpairE];
   18.19  
   18.20 -use"simpdata.ML";
    19.1 --- a/src/ZF/upair.thy	Thu Aug 10 00:45:23 2000 +0200
    19.2 +++ b/src/ZF/upair.thy	Thu Aug 10 11:27:34 2000 +0200
    19.3 @@ -6,7 +6,8 @@
    19.4  Dummy theory, but holds the standard ZF simpset.
    19.5  *)
    19.6  
    19.7 -upair = ZF +
    19.8 +theory upair = ZF
    19.9 +files "Tools/typechk":
   19.10  
   19.11  setup
   19.12    TypeCheck.setup