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