--- a/src/ZF/Bool.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Bool.thy Thu Aug 10 11:27:34 2000 +0200
@@ -8,7 +8,7 @@
2 is equal to bool, but serves a different purpose
*)
-Bool = upair +
+Bool = pair +
consts
bool :: i
cond :: [i,i,i]=>i
--- a/src/ZF/Integ/Bin.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Bin.ML Thu Aug 10 11:27:34 2000 +0200
@@ -87,8 +87,7 @@
(**** The carry/borrow functions, bin_succ and bin_pred ****)
(*NCons preserves the integer value of its argument*)
-Goal "[| w: bin; b: bool |] ==> \
-\ integ_of(NCons(w,b)) = integ_of(w BIT b)";
+Goal "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)";
by (etac bin.elim 1);
by (Asm_simp_tac 3);
by (ALLGOALS (etac boolE));
@@ -134,10 +133,20 @@
by (Asm_simp_tac 1);
qed "bin_add_Pls";
+Goalw [bin_add_def] "w: bin ==> bin_add(w,Pls) = w";
+by (etac bin.induct 1);
+by Auto_tac;
+qed "bin_add_Pls_right";
+
Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
by (Asm_simp_tac 1);
qed "bin_add_Min";
+Goalw [bin_add_def] "w: bin ==> bin_add(w,Min) = bin_pred(w)";
+by (etac bin.induct 1);
+by Auto_tac;
+qed "bin_add_Min_right";
+
Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x";
by (Simp_tac 1);
qed "bin_add_BIT_Pls";
@@ -166,6 +175,13 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
qed_spec_mp "integ_of_add";
+(*Subtraction*)
+Goalw [zdiff_def]
+ "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))";
+by (asm_simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
+qed "diff_integ_of_eq";
+
(*** bin_mult: binary multiplication ***)
@@ -186,60 +202,64 @@
Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
by (Simp_tac 1);
-qed "bin_succ_BIT1";
+qed "bin_succ_1";
Goal "bin_succ(w BIT 0) = NCons(w,1)";
by (Simp_tac 1);
-qed "bin_succ_BIT0";
+qed "bin_succ_0";
Goal "bin_pred(w BIT 1) = NCons(w,0)";
by (Simp_tac 1);
-qed "bin_pred_BIT1";
+qed "bin_pred_1";
Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
by (Simp_tac 1);
-qed "bin_pred_BIT0";
+qed "bin_pred_0";
(** extra rules for bin_minus **)
Goal "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))";
by (Simp_tac 1);
-qed "bin_minus_BIT1";
+qed "bin_minus_1";
Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
by (Simp_tac 1);
-qed "bin_minus_BIT0";
+qed "bin_minus_0";
(** extra rules for bin_add **)
Goal "w: bin ==> bin_add(v BIT 1, w BIT 1) = \
\ NCons(bin_add(v, bin_succ(w)), 0)";
by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT11";
+qed "bin_add_BIT_11";
Goal "w: bin ==> bin_add(v BIT 1, w BIT 0) = \
\ NCons(bin_add(v,w), 1)";
by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT10";
+qed "bin_add_BIT_10";
-Goal "[| w: bin; y: bool |] ==> \
-\ bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
+Goal "[| w: bin; y: bool |] \
+\ ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)";
by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT0";
+qed "bin_add_BIT_0";
(** extra rules for bin_mult **)
Goal "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)";
by (Simp_tac 1);
-qed "bin_mult_BIT1";
+qed "bin_mult_1";
Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
by (Simp_tac 1);
-qed "bin_mult_BIT0";
+qed "bin_mult_0";
(** Simplification rules with integer constants **)
+Goal "$#0 = #0";
+by (Simp_tac 1);
+qed "int_of_0";
+
Goal "#0 $+ z = intify(z)";
by (Simp_tac 1);
qed "zadd_0_intify";
@@ -272,6 +292,109 @@
Addsimps [zmult_0, zmult_0_right];
+Goal "#-1 $* z = $-z";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zmult_minus1";
+
+Goal "z $* #-1 = $-z";
+by (stac zmult_commute 1);
+by (rtac zmult_minus1 1);
+qed "zmult_minus1_right";
+
+Addsimps [zmult_minus1, zmult_minus1_right];
+
+
+(*** Simplification rules for comparison of binary numbers (N Voelker) ***)
+
+(** Equals (=) **)
+
+Goalw [iszero_def]
+ "[| v: bin; w: bin |] \
+\ ==> ((integ_of(v)) = integ_of(w)) <-> \
+\ iszero (integ_of (bin_add (v, bin_minus(w))))";
+by (asm_simp_tac (simpset() addsimps
+ (zcompare_rls @ [integ_of_add, integ_of_minus])) 1);
+qed "eq_integ_of_eq";
+
+Goalw [iszero_def] "iszero (integ_of(Pls))";
+by (Simp_tac 1);
+qed "iszero_integ_of_Pls";
+
+
+Goalw [iszero_def] "~ iszero (integ_of(Min))";
+by (simp_tac (simpset() addsimps [zminus_equation]) 1);
+qed "nonzero_integ_of_Min";
+
+Goalw [iszero_def]
+ "[| w: bin; x: bool |] \
+\ ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))";
+by (Simp_tac 1);
+by (subgoal_tac "integ_of(w) : int" 1);
+by (Asm_simp_tac 2);
+by (dtac int_cases 1);
+by (auto_tac (claset() addSEs [boolE],
+ simpset() addsimps [int_of_add RS sym]));
+by (ALLGOALS (asm_full_simp_tac
+ (simpset() addsimps zcompare_rls @
+ [zminus_zadd_distrib RS sym, int_of_add RS sym])));
+by (subgoal_tac "znegative ($- $# succ(x)) <-> znegative ($# succ(x))" 1);
+by (Asm_simp_tac 2);
+by (Full_simp_tac 1);
+qed "iszero_integ_of_BIT";
+
+Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))";
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1);
+qed "iszero_integ_of_0";
+
+Goal "w: bin ==> ~ iszero (integ_of (w BIT 1))";
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1);
+qed "iszero_integ_of_1";
+
+
+
+(** Less-than (<) **)
+
+Goalw [zless_def,zdiff_def]
+ "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $< integ_of(w) \
+\ <-> znegative (integ_of (bin_add (v, bin_minus(w))))";
+by (asm_simp_tac (simpset() addsimps [integ_of_minus, integ_of_add]) 1);
+qed "less_integ_of_eq_neg";
+
+Goal "~ znegative (integ_of(Pls))";
+by (Simp_tac 1);
+qed "not_neg_integ_of_Pls";
+
+Goal "znegative (integ_of(Min))";
+by (Simp_tac 1);
+qed "neg_integ_of_Min";
+
+Goal "[| w: bin; x: bool |] \
+\ ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))";
+by (Asm_simp_tac 1);
+by (subgoal_tac "integ_of(w) : int" 1);
+by (Asm_simp_tac 2);
+by (dtac int_cases 1);
+by (auto_tac (claset() addSEs [boolE],
+ simpset() addsimps [int_of_add RS sym] @ zcompare_rls));
+by (ALLGOALS (asm_full_simp_tac
+ (simpset() addsimps [zminus_zadd_distrib RS sym, zdiff_def,
+ int_of_add RS sym])));
+by (subgoal_tac "$#1 $- $# succ(succ(x #+ x)) = $- $# succ(x #+ x)" 1);
+by (asm_full_simp_tac (simpset() addsimps [zdiff_def])1);
+by (asm_simp_tac (simpset() addsimps [equation_zminus, int_of_diff RS sym])1);
+qed "neg_integ_of_BIT";
+
+Goal "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))";
+by (asm_simp_tac (ZF_ss addsimps [iszero_integ_of_BIT]) 1);
+qed "iszero_integ_of_0";
+
+(** Less-than-or-equals (<=) **)
+
+Goal "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+qed "le_integ_of_eq_not_less";
+
(*Delete the original rewrites, with their clumsy conditional expressions*)
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,
@@ -281,17 +404,69 @@
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
-Addsimps [integ_of_add RS sym, (*invoke bin_add*)
- integ_of_minus RS sym, (*invoke bin_minus*)
- integ_of_mult RS sym, (*invoke bin_mult*)
- bin_succ_Pls, bin_succ_Min,
- bin_succ_BIT1, bin_succ_BIT0,
- bin_pred_Pls, bin_pred_Min,
- bin_pred_BIT1, bin_pred_BIT0,
- bin_minus_Pls, bin_minus_Min,
- bin_minus_BIT1, bin_minus_BIT0,
- bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
- bin_add_BIT_Min, bin_add_BIT_BIT0,
- bin_add_BIT_BIT10, bin_add_BIT_BIT11,
- bin_mult_Pls, bin_mult_Min,
- bin_mult_BIT1, bin_mult_BIT0];
+bind_thms ("NCons_simps",
+ [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
+
+
+bind_thms ("bin_arith_extra_simps",
+ [integ_of_add RS sym, (*invoke bin_add*)
+ integ_of_minus RS sym, (*invoke bin_minus*)
+ integ_of_mult RS sym, (*invoke bin_mult*)
+ bin_succ_1, bin_succ_0,
+ bin_pred_1, bin_pred_0,
+ bin_minus_1, bin_minus_0,
+ bin_add_Pls_right, bin_add_Min_right,
+ bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
+ diff_integ_of_eq,
+ bin_mult_1, bin_mult_0] @ NCons_simps);
+
+
+(*For making a minimal simpset, one must include these default simprules
+ of thy. Also include simp_thms, or at least (~False)=True*)
+bind_thms ("bin_arith_simps",
+ [bin_pred_Pls, bin_pred_Min,
+ bin_succ_Pls, bin_succ_Min,
+ bin_add_Pls, bin_add_Min,
+ bin_minus_Pls, bin_minus_Min,
+ bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
+
+(*Simplification of relational operations*)
+bind_thms ("bin_rel_simps",
+ [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
+ iszero_integ_of_0, iszero_integ_of_1,
+ less_integ_of_eq_neg,
+ not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
+ le_integ_of_eq_not_less]);
+
+Addsimps bin_arith_simps;
+Addsimps bin_rel_simps;
+
+
+(** Simplification of arithmetic when nested to the right **)
+
+Goal "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)";
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+qed "add_integ_of_left";
+
+Goal "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)";
+by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
+qed "mult_integ_of_left";
+
+Goalw [zdiff_def]
+ "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)";
+by (rtac add_integ_of_left 1);
+by Auto_tac;
+qed "add_integ_of_diff1";
+
+Goal "[| v: bin; w: bin |] \
+\ ==> integ_of(v) $+ (c $- integ_of(w)) = \
+\ integ_of (bin_add (v, bin_minus(w))) $+ (c)";
+by (stac (diff_integ_of_eq RS sym) 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zdiff_def::zadd_ac)));
+qed "add_integ_of_diff2";
+
+Addsimps [add_integ_of_left, mult_integ_of_left,
+ add_integ_of_diff1, add_integ_of_diff2];
--- a/src/ZF/Integ/Bin.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Bin.thy Thu Aug 10 11:27:34 2000 +0200
@@ -18,13 +18,13 @@
Division is not defined yet!
*)
-Bin = Int + Datatype +
+Bin = Int + Datatype +
consts bin :: i
datatype
"bin" = Pls
| Min
- | BIT ("w: bin", "b: bool") (infixl 90)
+ | Bit ("w: bin", "b: bool") (infixl "BIT" 90)
syntax
"_Int" :: xnum => i ("_")
@@ -104,85 +104,9 @@
"bin_mult (v BIT b,w) = cond(b, bin_add(NCons(bin_mult(v,w),0),w),
NCons(bin_mult(v,w),0))"
+setup NumeralSyntax.setup
+
end
ML
-
-(** Concrete syntax for integers **)
-
-local
- open Syntax;
-
- (* Bits *)
-
- fun mk_bit 0 = const "0"
- | mk_bit 1 = const "succ" $ const "0"
- | mk_bit _ = sys_error "mk_bit";
-
- fun dest_bit (Const ("0", _)) = 0
- | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
- | dest_bit _ = raise Match;
-
-
- (* Bit strings *) (*we try to handle superfluous leading digits nicely*)
-
- fun prefix_len _ [] = 0
- | prefix_len pred (x :: xs) =
- if pred x then 1 + prefix_len pred xs else 0;
-
- fun mk_bin str =
- let
- val (sign, digs) =
- (case Symbol.explode str of
- "#" :: "-" :: cs => (~1, cs)
- | "#" :: cs => (1, cs)
- | _ => raise ERROR);
-
- val zs = prefix_len (equal "0") digs;
-
- fun bin_of 0 = []
- | bin_of ~1 = [~1]
- | bin_of n = (n mod 2) :: bin_of (n div 2);
-
- fun term_of [] = const "Pls"
- | term_of [~1] = const "Min"
- | term_of (b :: bs) = const "op BIT" $ term_of bs $ mk_bit b;
- in
- term_of (bin_of (sign * (#1 (read_int digs))))
- end;
-
- fun dest_bin tm =
- let
- fun bin_of (Const ("Pls", _)) = []
- | bin_of (Const ("Min", _)) = [~1]
- | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
- | bin_of _ = raise Match;
-
- fun integ_of [] = 0
- | integ_of (b :: bs) = b + 2 * integ_of bs;
-
- val rev_digs = bin_of tm;
- val (sign, zs) =
- (case rev rev_digs of
- ~1 :: bs => ("-", prefix_len (equal 1) bs)
- | bs => ("", prefix_len (equal 0) bs));
- val num = string_of_int (abs (integ_of rev_digs));
- in
- "#" ^ sign ^ implode (replicate zs "0") ^ num
- end;
-
-
- (* translation of integer constant tokens to and from binary *)
-
- fun int_tr (*"_Int"*) [t as Free (str, _)] =
- (const "integ_of" $
- (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
- | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
-
- fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
- | int_tr' (*"integ_of"*) _ = raise Match;
-in
- val parse_translation = [("_Int", int_tr)];
- val print_translation = [("integ_of", int_tr')];
-end;
--- a/src/ZF/Integ/Int.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Int.ML Thu Aug 10 11:27:34 2000 +0200
@@ -9,7 +9,6 @@
"znegative(z) ==> $# zmagnitude(z) = $- z"
"~ znegative(z) ==> $# zmagnitude(z) = z"
$+ and $* are monotonic wrt $<
-[| m: nat; n: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
*)
AddSEs [quotientE];
@@ -169,6 +168,15 @@
qed "zless_intify2";
Addsimps [zless_intify1, zless_intify2];
+Goal "intify(x) $<= y <-> x $<= y";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zle_intify1";
+
+Goal "x $<= intify(y) <-> x $<= y";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zle_intify2";
+Addsimps [zle_intify1, zle_intify2];
+
(**** zminus: unary negation on int ****)
@@ -296,6 +304,7 @@
by (rtac theI2 1);
by Auto_tac;
qed "zmagnitude_type";
+AddIffs [zmagnitude_type];
AddTCs [zmagnitude_type];
Goalw [int_def, znegative_def, int_of_def]
@@ -317,7 +326,6 @@
Addsimps [not_zneg_mag];
-
Goalw [int_def, znegative_def, int_of_def]
"[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))";
by (auto_tac(claset() addSDs [less_imp_succ_add],
@@ -331,6 +339,12 @@
Addsimps [zneg_mag];
+Goal "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))";
+by (case_tac "znegative(z)" 1);
+by (blast_tac (claset() addDs [not_zneg_mag, sym]) 2);
+by (blast_tac (claset() addDs [zneg_int_of]) 1);
+qed "int_cases";
+
(**** zadd: addition on int ****)
@@ -434,6 +448,17 @@
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
qed "int_of_add";
+Goal "$# succ(m) = $# 1 $+ ($# m)";
+by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
+qed "int_succ_int_1";
+
+Goalw [int_of_def,zdiff_def]
+ "[| m: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)";
+by (ftac lt_nat_in_nat 1);
+by (asm_simp_tac (simpset() addsimps [zadd,zminus,add_diff_inverse2]) 2);
+by Auto_tac;
+qed "int_of_diff";
+
Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));
qed "raw_zadd_zminus_inverse";
@@ -550,11 +575,10 @@
qed "zmult_zminus";
Addsimps [zmult_zminus];
-Goal "($- z) $* ($- w) = (z $* w)";
-by (stac zmult_zminus 1);
-by (stac zmult_commute 1 THEN stac zmult_zminus 1);
-by (simp_tac (simpset() addsimps [zmult_commute])1);
-qed "zmult_zminus_zminus";
+Goal "w $* ($- z) = $- (w $* z)";
+by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute]) 1);
+qed "zmult_zminus_right";
+Addsimps [zmult_zminus_right];
Goalw [int_def]
"[| z1: int; z2: int; z3: int |] \
@@ -602,6 +626,11 @@
(*** Subtraction laws ***)
+Goal "z $- w : int";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_type";
+AddIffs [zdiff_type]; AddTCs [zdiff_type];
+
Goal "$#0 $- x = $-x";
by (simp_tac (simpset() addsimps [zdiff_def]) 1);
qed "zdiff_int0";
@@ -616,6 +645,15 @@
Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
+Goal "$- (z $- y) = y $- z";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
+qed "zminus_zdiff_eq";
+Addsimps [zminus_zdiff_eq];
+
+Goal "$- (z $- y) = y $- z";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_commute])1);
+qed "zminus_zdiff_eq";
+Addsimps [zminus_zdiff_eq];
Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
by (stac zadd_zmult_distrib 1);
@@ -719,21 +757,57 @@
by Auto_tac;
qed "zless_trans";
+(*** "Less Than or Equals", $<= ***)
Goalw [zle_def] "z $<= z";
by Auto_tac;
qed "zle_refl";
-Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
+Goalw [zle_def] "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)";
+by Auto_tac;
by (blast_tac (claset() addDs [zless_trans]) 1);
qed "zle_anti_sym";
-Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
+Goalw [zle_def] "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z";
+by Auto_tac;
by (blast_tac (claset() addIs [zless_trans]) 1);
+val lemma = result();
+
+Goal "[| x $<= y; y $<= z |] ==> x $<= z";
+by (subgoal_tac "intify(x) $<= intify(z)" 1);
+by (res_inst_tac [("y", "intify(y)")] lemma 2);
+by Auto_tac;
qed "zle_trans";
+Goal "[| i $<= j; j $< k |] ==> i $< k";
+by (auto_tac (claset(), simpset() addsimps [zle_def]));
+by (blast_tac (claset() addIs [zless_trans]) 1);
+by (asm_full_simp_tac (simpset() addsimps [zless_def, zdiff_def, zadd_def]) 1);
+qed "zle_zless_trans";
-(*** More subtraction laws (for zcompare_rls): useful? ***)
+Goal "[| i $< j; j $<= k |] ==> i $< k";
+by (auto_tac (claset(), simpset() addsimps [zle_def]));
+by (blast_tac (claset() addIs [zless_trans]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [zless_def, zdiff_def, zminus_def]) 1);
+qed "zless_zle_trans";
+
+Goal "~ (z $< w) <-> (w $<= z)";
+by (cut_inst_tac [("z","z"),("w","w")] zless_linear 1);
+by (auto_tac (claset() addDs [zless_trans], simpset() addsimps [zle_def]));
+by (auto_tac (claset(),
+ simpset() addsimps [zless_def, zdiff_def, zadd_def, zminus_def]));
+by (fold_tac [zless_def, zdiff_def, zadd_def, zminus_def]);
+by Auto_tac;
+qed "not_zless_iff_zle";
+
+Goal "~ (z $<= w) <-> (w $< z)";
+by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
+qed "not_zle_iff_zless";
+
+
+
+(*** More subtraction laws (for zcompare_rls) ***)
Goal "(x $- y) $- z = x $- (y $+ z)";
by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
@@ -759,16 +833,33 @@
by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
qed "eq_zdiff_iff";
-(**Could not prove these!
Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
-by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zdiff_zless_iff]));
+val lemma = result();
+
+Goal "(x$-y $<= z) <-> (x $<= z $+ y)";
+by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
+by (Asm_full_simp_tac 1);
qed "zdiff_zle_iff";
-Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
-by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
+Goalw [zle_def] "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)";
+by (auto_tac (claset(), simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]));
+by (auto_tac (claset(), simpset() addsimps [zdiff_def, zadd_assoc]));
+val lemma = result();
+
+Goal "(x $<= z$-y) <-> (x $+ y $<= z)";
+by (cut_facts_tac [[intify_in_int, intify_in_int] MRS lemma] 1);
+by (Asm_full_simp_tac 1);
qed "zle_zdiff_iff";
-**)
+
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+ to the top and then moving negative terms to the other side.
+ Use with zadd_ac*)
+bind_thms ("zcompare_rls",
+ [symmetric zdiff_def,
+ zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2,
+ zdiff_zless_iff, zless_zdiff_iff, zdiff_zle_iff, zle_zdiff_iff,
+ zdiff_eq_iff, eq_zdiff_iff]);
(*** Monotonicity/cancellation results that could allow instantiation
@@ -816,14 +907,24 @@
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
-Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
+Goal "(w' $+ z $<= w $+ z) <-> w' $<= w";
by (simp_tac (simpset() addsimps [zle_def]) 1);
qed "zadd_right_cancel_zle";
-Goal "(z $+ w' $<= z $+ w) <-> (intify(w') $<= intify(w))";
+Goal "(z $+ w' $<= z $+ w) <-> w' $<= w";
by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
zadd_right_cancel_zle]) 1);
qed "zadd_left_cancel_zle";
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
+
+(*** More inequality lemmas ***)
+
+Goal "[| x: int; y: int |] ==> (x = $- y) <-> (y = $- x)";
+by Auto_tac;
+qed "equation_zminus";
+
+Goal "[| x: int; y: int |] ==> ($- x = y) <-> ($- y = x)";
+by Auto_tac;
+qed "zminus_equation";
--- a/src/ZF/Integ/Int.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Integ/Int.thy Thu Aug 10 11:27:34 2000 +0200
@@ -30,7 +30,10 @@
znegative :: i=>o
"znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
-
+
+ iszero :: i=>o
+ "iszero(z) == z = $# 0"
+
zmagnitude :: i=>i
"zmagnitude(z) ==
THE m. m : nat & ((~ znegative(z) & z = $# m) |
@@ -62,7 +65,7 @@
"z1 $< z2 == znegative(z1 $- z2)"
zle :: [i,i]=>o (infixl "$<=" 50)
- "z1 $<= z2 == z1 $< z2 | z1=z2"
+ "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
(*div and mod await definitions!*)
consts
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/IntArith.thy Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,5 @@
+
+theory IntArith = Bin
+files "int_arith.ML":
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/int_arith.ML Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,391 @@
+(* Title: ZF/Integ/int_arith.ML
+ ID: $Id$
+ Author: Larry Paulson
+ Copyright 2000 University of Cambridge
+
+Simprocs for linear arithmetic.
+*)
+
+(*** Simprocs for numeric literals ***)
+
+(** Combining of literal coefficients in sums of products **)
+
+Goal "(x $< y) <-> (x$-y $< #0)";
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zless_iff_zdiff_zless_0";
+
+Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
+by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "eq_iff_zdiff_eq_0";
+
+Goal "(x $<= y) <-> (x$-y $<= #0)";
+by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
+qed "zle_iff_zdiff_zle_0";
+
+
+(** For combine_numerals **)
+
+Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
+by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
+qed "left_zadd_zmult_distrib";
+
+
+(** For cancel_numerals **)
+
+val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0] @
+ map (inst "y" "n")
+ [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
+ zle_iff_zdiff_zle_0];
+
+Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "eq_add_iff1";
+
+Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "eq_add_iff2";
+
+Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+ zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff1";
+
+Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
+by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
+ zadd_ac@rel_iff_rel_0_rls) 1);
+qed "less_add_iff2";
+
+Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= intify(n))";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "le_add_iff1";
+
+Goal "(i$*u $+ m $<= j$*u $+ n) <-> (intify(m) $<= (j$-i)$*u $+ n)";
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
+by (simp_tac (simpset() addsimps zcompare_rls) 1);
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "le_add_iff2";
+
+
+structure Int_Numeral_Simprocs =
+struct
+
+(*Utilities*)
+
+val integ_of_const = Const ("Bin.integ_of", iT --> iT);
+
+fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
+
+(*Decodes a binary INTEGER*)
+fun dest_numeral (Const("Bin.integ_of", _) $ w) =
+ (NumeralSyntax.dest_bin w
+ handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
+ | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
+
+fun find_first_numeral past (t::terms) =
+ ((dest_numeral t, rev past @ terms)
+ handle TERM _ => find_first_numeral (t::past) terms)
+ | find_first_numeral past [] = raise TERM("find_first_numeral", []);
+
+val zero = mk_numeral 0;
+val mk_plus = FOLogic.mk_binop "Int.zadd";
+
+val iT = Ind_Syntax.iT;
+
+val zminus_const = Const ("Int.zminus", iT --> iT);
+
+(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
+fun mk_sum [] = zero
+ | mk_sum [t,u] = mk_plus (t, u)
+ | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum [] = zero
+ | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
+
+(*decompose additions AND subtractions as a sum*)
+fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
+ dest_summing (pos, t, dest_summing (pos, u, ts))
+ | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
+ dest_summing (pos, t, dest_summing (not pos, u, ts))
+ | dest_summing (pos, t, ts) =
+ if pos then t::ts else zminus_const$t :: ts;
+
+fun dest_sum t = dest_summing (true, t, []);
+
+val mk_diff = FOLogic.mk_binop "Int.zdiff";
+val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
+
+val one = mk_numeral 1;
+val mk_times = FOLogic.mk_binop "Int.zmult";
+
+fun mk_prod [] = one
+ | mk_prod [t] = t
+ | mk_prod (t :: ts) = if t = one then mk_prod ts
+ else mk_times (t, mk_prod ts);
+
+val dest_times = FOLogic.dest_bin "Int.zmult" iT;
+
+fun dest_prod t =
+ let val (t,u) = dest_times t
+ in dest_prod t @ dest_prod u end
+ handle TERM _ => [t];
+
+(*DON'T do the obvious simplifications; that would create special cases*)
+fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
+
+(*Express t as a product of (possibly) a numeral with other sorted terms*)
+fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
+ | dest_coeff sign t =
+ let val ts = sort Term.term_ord (dest_prod t)
+ val (n, ts') = find_first_numeral [] ts
+ handle TERM _ => (1, ts)
+ in (sign*n, mk_prod ts') end;
+
+(*Find first coefficient-term THAT MATCHES u*)
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+ | find_first_coeff past u (t::terms) =
+ let val (n,u') = dest_coeff 1 t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
+
+
+(*Simplify #1*n and n*#1 to n*)
+val add_0s = [zadd_0_intify, zadd_0_right_intify];
+
+val mult_1s = [zmult_1_intify, zmult_1_right_intify,
+ zmult_minus1, zmult_minus1_right];
+
+val tc_rules = [integ_of_type, intify_in_int,
+ zadd_type, zdiff_type, zmult_type] @ bin.intrs;
+val intifys = [intify_ident, zadd_intify1, zadd_intify2,
+ zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
+ zless_intify1, zless_intify2, zle_intify1, zle_intify2];
+
+(*To perform binary arithmetic*)
+val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
+
+(*To evaluate binary negations of coefficients*)
+val zminus_simps = NCons_simps @
+ [integ_of_minus RS sym,
+ bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
+ bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
+
+(*To let us treat subtraction as addition*)
+val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
+ (s, TypeInfer.anyT ["logic"]);
+val prep_pats = map prep_pat;
+
+structure CancelNumeralsCommon =
+ struct
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val find_first_coeff = find_first_coeff []
+ val trans_tac = ArithData.gen_trans_tac iff_trans
+ val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
+ zminus_simps@zadd_ac
+ val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+ bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps@tc_rules@intifys))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
+ end;
+
+
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
+ val mk_bal = FOLogic.mk_eq
+ val dest_bal = FOLogic.dest_bin "op =" iT
+ val bal_add1 = eq_add_iff1 RS iff_trans
+ val bal_add2 = eq_add_iff2 RS iff_trans
+);
+
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
+ val mk_bal = FOLogic.mk_binrel "Int.zless"
+ val dest_bal = FOLogic.dest_bin "Int.zless" iT
+ val bal_add1 = less_add_iff1 RS iff_trans
+ val bal_add2 = less_add_iff2 RS iff_trans
+);
+
+structure LeCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
+ val mk_bal = FOLogic.mk_binrel "Int.zle"
+ val dest_bal = FOLogic.dest_bin "Int.zle" iT
+ val bal_add1 = le_add_iff1 RS iff_trans
+ val bal_add2 = le_add_iff2 RS iff_trans
+);
+
+val cancel_numerals =
+ map prep_simproc
+ [("inteq_cancel_numerals",
+ prep_pats ["l $+ m = n", "l = m $+ n",
+ "l $- m = n", "l = m $- n",
+ "l $* m = n", "l = m $* n"],
+ EqCancelNumerals.proc),
+ ("intless_cancel_numerals",
+ prep_pats ["l $+ m $< n", "l $< m $+ n",
+ "l $- m $< n", "l $< m $- n",
+ "l $* m $< n", "l $< m $* n"],
+ LessCancelNumerals.proc),
+ ("intle_cancel_numerals",
+ prep_pats ["l $+ m $<= n", "l $<= m $+ n",
+ "l $- m $<= n", "l $<= m $- n",
+ "l $* m $<= n", "l $<= m $* n"],
+ LeCancelNumerals.proc)];
+
+
+(*version without the hyps argument*)
+fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
+
+structure CombineNumeralsData =
+ struct
+ val add = op + : int*int -> int
+ val mk_sum = long_mk_sum (*to work for e.g. #2*x $+ #3*x *)
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff 1
+ val left_distrib = left_zadd_zmult_distrib RS trans
+ val prove_conv = prove_conv_nohyps "int_combine_numerals"
+ val trans_tac = ArithData.gen_trans_tac trans
+ val norm_tac_ss1 = ZF_ss addsimps add_0s@mult_1s@diff_simps@
+ zminus_simps@zadd_ac
+ val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+ bin_simps@zadd_ac@zmult_ac@tc_rules@intifys
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps add_0s@bin_simps))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s@mult_1s)
+ end;
+
+structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
+
+val combine_numerals =
+ prep_simproc ("int_combine_numerals",
+ prep_pats ["i $+ j", "i $- j"],
+ CombineNumerals.proc);
+
+
+
+(** Constant folding for integer multiplication **)
+
+(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
+ the "sum" of #3, x, #4; the literals are then multiplied*)
+structure CombineNumeralsProdData =
+ struct
+ val add = op * : int*int -> int
+ val mk_sum = mk_prod
+ val dest_sum = dest_prod
+ fun mk_coeff (k, t) = mk_numeral k
+ val dest_coeff = dest_coeff 1
+ val left_distrib = zmult_assoc RS sym RS trans
+ val prove_conv = prove_conv_nohyps "int_combine_numerals_prod"
+ val trans_tac = ArithData.gen_trans_tac trans
+ val norm_tac_ss1 = ZF_ss addsimps mult_1s@diff_simps@zminus_simps
+ val norm_tac_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym]@
+ bin_simps@zmult_ac@tc_rules@intifys
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ val numeral_simp_tac = ALLGOALS (simp_tac (ZF_ss addsimps bin_simps))
+ val simplify_meta_eq = ArithData.simplify_meta_eq (mult_1s)
+ end;
+
+
+structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
+
+val combine_numerals_prod =
+ prep_simproc ("int_combine_numerals_prod",
+ prep_pats ["i $* j", "i $* j"],
+ CombineNumeralsProd.proc);
+
+end;
+
+
+Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
+Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
+ Int_Numeral_Simprocs.combine_numerals_prod];
+
+
+(*examples:*)
+(*
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+val sg = #sign (rep_thm (topthm()));
+val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
+val (t,_) = FOLogic.dest_eq t;
+
+(*combine_numerals_prod (products of separate literals) *)
+test "#5 $* x $* #3 = y";
+
+test "y2 $+ ?x42 = y $+ y2";
+
+test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
+
+test "#9$*x $+ y = x$*#23 $+ z";
+test "y $+ x = x $+ z";
+
+test "x : int ==> x $+ y $+ z = x $+ z";
+test "x : int ==> y $+ (z $+ x) = z $+ x";
+test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
+test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
+
+test "#-3 $* x $+ y $<= x $* #2 $+ z";
+test "y $+ x $<= x $+ z";
+test "x $+ y $+ z $<= x $+ z";
+
+test "y $+ (z $+ x) $< z $+ x";
+test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
+test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
+
+test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
+test "u : int ==> #2 $* u = u";
+test "(i $+ j $+ #12 $+ k) $- #15 = y";
+test "(i $+ j $+ #12 $+ k) $- #5 = y";
+
+test "y $- b $< b";
+test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
+
+test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
+test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
+test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
+test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
+
+test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
+test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
+
+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";
+
+test "a $+ $-(b$+c) $+ b = d";
+test "a $+ $-(b$+c) $- b = d";
+
+(*negative numerals*)
+test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
+test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
+test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
+test "(i $+ j $+ #-12 $+ k) $- #15 = y";
+test "(i $+ j $+ #12 $+ k) $- #-15 = y";
+test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
+*)
+
--- a/src/ZF/IsaMakefile Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/IsaMakefile Thu Aug 10 11:27:34 2000 +0200
@@ -33,11 +33,14 @@
Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML \
Inductive.thy InfDatatype.ML InfDatatype.thy Integ/Bin.ML \
Integ/Bin.thy Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML \
- Integ/Int.thy Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy \
+ Integ/Int.thy Integ/twos_compl.ML \
+ Integ/int_arith.ML Integ/IntArith.thy \
+ Let.ML Let.thy List.ML List.thy \
Main.thy Nat.ML Nat.thy Order.ML Order.thy OrderArith.ML \
OrderArith.thy OrderType.ML OrderType.thy Ordinal.ML Ordinal.thy \
Perm.ML Perm.thy QPair.ML QPair.thy QUniv.ML QUniv.thy ROOT.ML \
- Rel.ML Rel.thy Sum.ML Sum.thy Tools/cartprod.ML \
+ Rel.ML Rel.thy Sum.ML Sum.thy \
+ Tools/numeral_syntax.ML Tools/cartprod.ML \
Tools/datatype_package.ML Tools/induct_tacs.ML \
Tools/inductive_package.ML Tools/primrec_package.ML Tools/typechk.ML \
Trancl.ML Trancl.thy Univ.ML Univ.thy Update.ML Update.thy WF.ML \
--- a/src/ZF/Main.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Main.thy Thu Aug 10 11:27:34 2000 +0200
@@ -2,5 +2,5 @@
(*$Id$
theory Main includes everything*)
-Main = Update + InfDatatype + List + EquivClass + Bin
+Main = Update + InfDatatype + List + EquivClass + IntArith
--- a/src/ZF/Perm.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/Perm.thy Thu Aug 10 11:27:34 2000 +0200
@@ -9,7 +9,7 @@
-- Lemmas for the Schroeder-Bernstein Theorem
*)
-Perm = upair + mono + func +
+Perm = mono + func +
consts
O :: [i,i]=>i (infixr 60)
--- a/src/ZF/ROOT.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/ROOT.ML Thu Aug 10 11:27:34 2000 +0200
@@ -19,9 +19,8 @@
use "thy_syntax";
use "~~/src/Provers/Arith/cancel_numerals.ML";
+use "~~/src/Provers/Arith/combine_numerals.ML";
-use_thy "ZF";
-use "Tools/typechk";
use_thy "mono";
use "ind_syntax";
use "Tools/cartprod";
@@ -32,6 +31,7 @@
use_thy "QUniv";
use "Tools/datatype_package";
+use "Tools/numeral_syntax";
(*the all-in-one theory*)
with_path "Integ" use_thy "Main";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Tools/numeral_syntax.ML Thu Aug 10 11:27:34 2000 +0200
@@ -0,0 +1,117 @@
+(* Title: ZF/Tools/numeral_syntax.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Concrete syntax for generic numerals. Assumes consts and syntax of
+theory ZF/Integ/Bin.
+*)
+
+signature NUMERAL_SYNTAX =
+sig
+ val dest_bin : term -> int
+ val mk_bin : int -> term
+ val int_tr : term list -> term
+ val int_tr' : bool -> typ -> term list -> term
+ val setup : (theory -> theory) list
+end;
+
+structure NumeralSyntax: NUMERAL_SYNTAX =
+struct
+
+open Syntax;
+
+(* Bits *)
+
+val zero = Const("0", iT);
+val succ = Const("succ", iT --> iT);
+
+fun mk_bit 0 = zero
+ | mk_bit 1 = succ$zero
+ | mk_bit _ = sys_error "mk_bit";
+
+fun dest_bit (Const ("0", _)) = 0
+ | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
+ | dest_bit _ = raise Match;
+
+
+(* Bit strings *) (*we try to handle superfluous leading digits nicely*)
+
+fun prefix_len _ [] = 0
+ | prefix_len pred (x :: xs) =
+ if pred x then 1 + prefix_len pred xs else 0;
+
+fun scan_int str =
+ let val (sign, digs) =
+ (case Symbol.explode str of
+ "#" :: "-" :: cs => (~1, cs)
+ | "#" :: cs => (1, cs)
+ | _ => raise ERROR);
+
+ in sign * (#1 (read_int digs)) end;
+
+
+val pls_const = Const ("Bin.bin.Pls", iT)
+and min_const = Const ("Bin.bin.Min", iT)
+and bit_const = Const ("Bin.bin.Bit", [iT, iT] ---> iT);
+
+fun mk_bin i =
+ let fun bin_of 0 = []
+ | bin_of ~1 = [~1]
+ | bin_of n = (n mod 2) :: bin_of (n div 2);
+
+ fun term_of [] = pls_const
+ | term_of [~1] = min_const
+ | term_of (b :: bs) = bit_const $ term_of bs $ mk_bit b;
+ in
+ term_of (bin_of i)
+ end;
+
+(*we consider all "spellings", since they could vary depending on the caller*)
+fun bin_of (Const ("Pls", _)) = []
+ | bin_of (Const ("bin.Pls", _)) = []
+ | bin_of (Const ("Bin.bin.Pls", _)) = []
+ | bin_of (Const ("Min", _)) = [~1]
+ | bin_of (Const ("bin.Min", _)) = [~1]
+ | bin_of (Const ("Bin.bin.Min", _)) = [~1]
+ | bin_of (Const ("Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of (Const ("bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of (Const ("Bin.bin.Bit", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of _ = raise Match;
+
+fun integ_of [] = 0
+ | integ_of (b :: bs) = b + 2 * integ_of bs;
+
+val dest_bin = integ_of o bin_of;
+
+(*leading 0s and (for negative numbers) -1s cause complications,
+ though they should never arise in normal use.*)
+fun show_int t =
+ let
+ val rev_digs = bin_of t;
+ val (sign, zs) =
+ (case rev rev_digs of
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
+ | bs => ("", prefix_len (equal 0) bs));
+ val num = string_of_int (abs (integ_of rev_digs));
+ in
+ "#" ^ sign ^ implode (replicate zs "0") ^ num
+ end;
+
+
+
+(* translation of integer constant tokens to and from binary *)
+
+fun int_tr (*"_Int"*) [t as Free (str, _)] =
+ (const "integ_of" $
+ (mk_bin (scan_int str) handle ERROR => raise TERM ("int_tr", [t])))
+ | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
+
+fun int_tr' _ _ (*"integ_of"*) [t] = const "_Int" $ free (show_int t)
+ | int_tr' (_:bool) (_:typ) _ = raise Match;
+
+
+val setup =
+ [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
+ Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
+
+end;
--- a/src/ZF/arith_data.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/arith_data.ML Thu Aug 10 11:27:34 2000 +0200
@@ -8,9 +8,16 @@
signature ARITH_DATA =
sig
+ (*the main outcome*)
val nat_cancel: simproc list
+ (*tools for use in similar applications*)
+ val gen_trans_tac: thm -> thm option -> tactic
+ val prove_conv: string -> tactic list -> Sign.sg ->
+ thm list -> term * term -> thm option
+ val simplify_meta_eq: thm list -> thm -> thm
end;
+
structure ArithData: ARITH_DATA =
struct
@@ -21,11 +28,7 @@
fun mk_succ t = succ $ t;
val one = mk_succ zero;
-(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
-fun mk_binop_i c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
-fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
-
-val mk_plus = mk_binop_i "Arith.add";
+val mk_plus = FOLogic.mk_binop "Arith.add";
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
fun mk_sum [] = zero
@@ -81,7 +84,7 @@
(*** Use CancelNumerals simproc without binary numerals,
just for cancellation ***)
-val mk_times = mk_binop_i "Arith.mult";
+val mk_times = FOLogic.mk_binop "Arith.mult";
fun mk_prod [] = one
| mk_prod [t] = t
@@ -120,14 +123,14 @@
val mult_1s = [mult_1_natify, mult_1_right_natify];
val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
- add_natify1, add_natify2, diff_natify1, diff_natify2];
+ diff_natify1, diff_natify2];
(*Final simplification: cancel + and **)
fun simplify_meta_eq rules =
mk_meta_eq o
simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
delsimps iff_simps (*these could erase the whole rule!*)
- addsimps rules)
+ addsimps rules);
val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
@@ -161,7 +164,7 @@
structure LessCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = prove_conv "natless_cancel_numerals"
- val mk_bal = mk_binrel_i "Ordinal.op <"
+ val mk_bal = FOLogic.mk_binrel "Ordinal.op <"
val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
val bal_add1 = less_add_iff RS iff_trans
val bal_add2 = less_add_iff RS iff_trans
@@ -171,7 +174,7 @@
structure DiffCancelNumerals = CancelNumeralsFun
(open CancelNumeralsCommon
val prove_conv = prove_conv "natdiff_cancel_numerals"
- val mk_bal = mk_binop_i "Arith.diff"
+ val mk_bal = FOLogic.mk_binop "Arith.diff"
val dest_bal = FOLogic.dest_bin "Arith.diff" iT
val bal_add1 = diff_add_eq RS trans
val bal_add2 = diff_add_eq RS trans
--- a/src/ZF/ex/BinEx.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/ex/BinEx.ML Thu Aug 10 11:27:34 2000 +0200
@@ -51,3 +51,30 @@
Goal "#1359 $* #-2468 = #-3354012";
by (Simp_tac 1); (*1.04 secs*)
result();
+
+
+(** Comparisons **)
+
+Goal "(#89) $* #10 ~= #889";
+by (Simp_tac 1);
+result();
+
+Goal "(#13) $< #18 $- #4";
+by (Simp_tac 1);
+result();
+
+Goal "(#-345) $< #-242 $+ #-100";
+by (Simp_tac 1);
+result();
+
+Goal "(#13557456) $< #18678654";
+by (Simp_tac 1);
+result();
+
+Goal "(#999999) $<= (#1000001 $+ #1) $- #2";
+by (Simp_tac 1);
+result();
+
+Goal "(#1234567) $<= #1234567";
+by (Simp_tac 1);
+result();
--- a/src/ZF/pair.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/pair.thy Thu Aug 10 11:27:34 2000 +0200
@@ -1,4 +1,5 @@
-(*Dummy theory to document dependencies *)
+theory pair = upair
+files "simpdata":
+end
-pair = upair
--- a/src/ZF/simpdata.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/simpdata.ML Thu Aug 10 11:27:34 2000 +0200
@@ -10,7 +10,7 @@
local
(*For proving rewrite rules*)
- fun prover s = (prove_goal thy s (fn _ => [Blast_tac 1]));
+ fun prover s = (prove_goal (the_context ()) s (fn _ => [Blast_tac 1]));
in
@@ -106,7 +106,8 @@
val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all)
- addsplits [split_if]
+ addcongs [if_weak_cong]
+ addsplits [split_if]
setSolver (mk_solver "types" Type_solver_tac);
val ZF_ss = simpset();
--- a/src/ZF/subset.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/subset.thy Thu Aug 10 11:27:34 2000 +0200
@@ -1,3 +1,3 @@
(*Dummy theory to document dependencies *)
-subset = upair
+subset = pair
--- a/src/ZF/upair.ML Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/upair.ML Thu Aug 10 11:27:34 2000 +0200
@@ -269,6 +269,12 @@
by (simp_tac (simpset() addsimps prems addcongs [conj_cong]) 1);
qed "if_cong";
+(*Prevents simplification of x and y: faster and allows the execution
+ of functional programs. NOW THE DEFAULT.*)
+Goal "P<->Q ==> (if P then x else y) = (if Q then x else y)";
+by (Asm_simp_tac 1);
+qed "if_weak_cong";
+
(*Not needed for rewriting, since P would rewrite to True anyway*)
Goalw [if_def] "P ==> (if P then a else b) = a";
by (Blast_tac 1);
@@ -398,4 +404,3 @@
(*Not needed now that cons is available. Deletion reduces the search space.*)
Delrules [UpairI1,UpairI2,UpairE];
-use"simpdata.ML";
--- a/src/ZF/upair.thy Thu Aug 10 00:45:23 2000 +0200
+++ b/src/ZF/upair.thy Thu Aug 10 11:27:34 2000 +0200
@@ -6,7 +6,8 @@
Dummy theory, but holds the standard ZF simpset.
*)
-upair = ZF +
+theory upair = ZF
+files "Tools/typechk":
setup
TypeCheck.setup