--- a/src/ZF/Integ/Bin.ML Thu Sep 05 14:03:03 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,612 +0,0 @@
-(* Title: ZF/ex/Bin.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Arithmetic on binary integers.
-*)
-
-
-Addsimps bin.intrs;
-AddTCs bin.intrs;
-
-Goal "NCons(Pls,0) = Pls";
-by (Asm_simp_tac 1);
-qed "NCons_Pls_0";
-
-Goal "NCons(Pls,1) = Pls BIT 1";
-by (Asm_simp_tac 1);
-qed "NCons_Pls_1";
-
-Goal "NCons(Min,0) = Min BIT 0";
-by (Asm_simp_tac 1);
-qed "NCons_Min_0";
-
-Goal "NCons(Min,1) = Min";
-by (Asm_simp_tac 1);
-qed "NCons_Min_1";
-
-Goal "NCons(w BIT x,b) = w BIT x BIT b";
-by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
-qed "NCons_BIT";
-
-bind_thms ("NCons_simps",
- [NCons_Pls_0, NCons_Pls_1,
- NCons_Min_0, NCons_Min_1,
- NCons_BIT]);
-Addsimps NCons_simps;
-
-
-(** Type checking **)
-
-Goal "w: bin ==> integ_of(w) : int";
-by (induct_tac "w" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [bool_into_nat])));
-qed "integ_of_type";
-AddTCs [integ_of_type];
-
-Goal "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
-by (induct_tac "w" 1);
-by Auto_tac;
-qed "NCons_type";
-AddTCs [NCons_type];
-
-Goal "w: bin ==> bin_succ(w) : bin";
-by (induct_tac "w" 1);
-by Auto_tac;
-qed "bin_succ_type";
-AddTCs [bin_succ_type];
-
-Goal "w: bin ==> bin_pred(w) : bin";
-by (induct_tac "w" 1);
-by Auto_tac;
-qed "bin_pred_type";
-AddTCs [bin_pred_type];
-
-Goal "w: bin ==> bin_minus(w) : bin";
-by (induct_tac "w" 1);
-by Auto_tac;
-qed "bin_minus_type";
-AddTCs [bin_minus_type];
-
-(*This proof is complicated by the mutual recursion*)
-Goalw [bin_add_def] "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
-by (induct_tac "v" 1);
-by (rtac ballI 3);
-by (rename_tac "w'" 3);
-by (induct_tac "w'" 3);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [NCons_type])));
-qed_spec_mp "bin_add_type";
-AddTCs [bin_add_type];
-
-Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
-by (induct_tac "v" 1);
-by Auto_tac;
-qed "bin_mult_type";
-AddTCs [bin_mult_type];
-
-
-(**** 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)";
-by (etac bin.elim 1);
-by (Asm_simp_tac 3);
-by (ALLGOALS (etac boolE));
-by (ALLGOALS Asm_simp_tac);
-qed "integ_of_NCons";
-
-Addsimps [integ_of_NCons];
-
-Goal "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)";
-by (etac bin.induct 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (etac boolE 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
-qed "integ_of_succ";
-
-Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)";
-by (etac bin.induct 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (etac boolE 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
-qed "integ_of_pred";
-
-Addsimps [integ_of_succ, integ_of_pred];
-
-
-(*** bin_minus: (unary!) negation of binary integers ***)
-
-Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)";
-by (etac bin.induct 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (etac boolE 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps zadd_ac@[zminus_zadd_distrib])));
-qed "integ_of_minus";
-
-
-(*** bin_add: binary addition ***)
-
-Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w";
-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";
-
-Goalw [bin_add_def] "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
-by (Simp_tac 1);
-qed "bin_add_BIT_Min";
-
-Goalw [bin_add_def] "[| w: bin; y: bool |] \
-\ ==> bin_add(v BIT x, w BIT y) = \
-\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
-by (Asm_simp_tac 1);
-qed "bin_add_BIT_BIT";
-
-Addsimps [bin_add_Pls, bin_add_Min, bin_add_BIT_Pls,
- bin_add_BIT_Min, bin_add_BIT_BIT,
- integ_of_succ, integ_of_pred];
-
-Goal "v: bin ==> \
-\ ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)";
-by (etac bin.induct 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-by (rtac ballI 1);
-by (induct_tac "wa" 1);
-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 ***)
-
-Goal "[| v: bin; w: bin |] \
-\ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
-by (induct_tac "v" 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [integ_of_minus]) 1);
-by (etac boolE 1);
-by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
-by (asm_simp_tac (simpset() addsimps [integ_of_add,
- zadd_zmult_distrib] @ zadd_ac) 1);
-qed "integ_of_mult";
-
-(**** Computations ****)
-
-(** extra rules for bin_succ, bin_pred **)
-
-Goal "bin_succ(w BIT 1) = bin_succ(w) BIT 0";
-by (Simp_tac 1);
-qed "bin_succ_1";
-
-Goal "bin_succ(w BIT 0) = NCons(w,1)";
-by (Simp_tac 1);
-qed "bin_succ_0";
-
-Goal "bin_pred(w BIT 1) = NCons(w,0)";
-by (Simp_tac 1);
-qed "bin_pred_1";
-
-Goal "bin_pred(w BIT 0) = bin_pred(w) BIT 1";
-by (Simp_tac 1);
-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_1";
-
-Goal "bin_minus(w BIT 0) = bin_minus(w) BIT 0";
-by (Simp_tac 1);
-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_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_10";
-
-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_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_1";
-
-Goal "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)";
-by (Simp_tac 1);
-qed "bin_mult_0";
-
-
-(** Simplification rules with integer constants **)
-
-Goal "$#0 = #0";
-by (Simp_tac 1);
-qed "int_of_0";
-
-Goal "$# succ(n) = #1 $+ $#n";
-by (simp_tac (simpset() addsimps [int_of_add RS sym, natify_succ]) 1);
-qed "int_of_succ";
-
-Goal "$- #0 = #0";
-by (Simp_tac 1);
-qed "zminus_0";
-
-Addsimps [zminus_0];
-
-Goal "#0 $+ z = intify(z)";
-by (Simp_tac 1);
-qed "zadd_0_intify";
-
-Goal "z $+ #0 = intify(z)";
-by (Simp_tac 1);
-qed "zadd_0_right_intify";
-
-Addsimps [zadd_0_intify, zadd_0_right_intify];
-
-Goal "#1 $* z = intify(z)";
-by (Simp_tac 1);
-qed "zmult_1_intify";
-
-Goal "z $* #1 = intify(z)";
-by (stac zmult_commute 1);
-by (Simp_tac 1);
-qed "zmult_1_right_intify";
-
-Addsimps [zmult_1_intify, zmult_1_right_intify];
-
-Goal "#0 $* z = #0";
-by (Simp_tac 1);
-qed "zmult_0";
-
-Goal "z $* #0 = #0";
-by (stac zmult_commute 1);
-by (Simp_tac 1);
-qed "zmult_0_right";
-
-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(n)) <-> znegative ($# succ(n))" 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(n #+ n)) = $- $# succ(n #+ n)" 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";
-
-(** 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,
- NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];
-
-(*Hide the binary representation of integer constants*)
-Delsimps [integ_of_Pls, integ_of_Min, integ_of_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];
-
-
-(** More for integer constants **)
-
-Addsimps [int_of_0, int_of_succ];
-
-Goal "#0 $- x = $-x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0";
-
-Goal "x $- #0 = intify(x)";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0_right";
-
-Goal "x $- x = #0";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_self";
-
-Addsimps [zdiff0, zdiff0_right, zdiff_self];
-
-Goal "k: int ==> znegative(k) <-> k $< #0";
-by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
-qed "znegative_iff_zless_0";
-
-Goal "[| #0 $< k; k: int |] ==> znegative($-k)";
-by (asm_full_simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zero_zless_imp_znegative_zminus";
-
-Goal "#0 $<= $# n";
-by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym,
- znegative_iff_zless_0 RS iff_sym]) 1);
-qed "zero_zle_int_of";
-Addsimps [zero_zle_int_of];
-
-Goal "nat_of(#0) = 0";
-by (simp_tac (ZF_ss addsimps [natify_0, int_of_0 RS sym, nat_of_int_of]) 1);
-qed "nat_of_0";
-Addsimps [nat_of_0];
-
-Goal "[| z $<= $#0; z: int |] ==> nat_of(z) = 0";
-by (auto_tac (claset(),
- simpset() addsimps [znegative_iff_zless_0 RS iff_sym,
- zle_def, zneg_nat_of]));
-val lemma = result();
-
-Goal "z $<= $#0 ==> nat_of(z) = 0";
-by (subgoal_tac "nat_of(intify(z)) = 0" 1);
-by (rtac lemma 2);
-by Auto_tac;
-qed "nat_le_int0";
-
-Goal "$# n = #0 ==> natify(n) = 0";
-by (rtac not_znegative_imp_zero 1);
-by Auto_tac;
-qed "int_of_eq_0_imp_natify_eq_0";
-
-Goalw [nat_of_def, raw_nat_of_def] "nat_of($- $# n) = 0";
-by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq],
- simpset()) delIffs [int_of_eq]));
-by (rtac the_equality 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [int_of_eq_0_imp_natify_eq_0, sym]) 1);
-qed "nat_of_zminus_int_of";
-
-Goal "#0 $<= z ==> $# nat_of(z) = intify(z)";
-by (rtac not_zneg_nat_of_intify 1);
-by (asm_simp_tac (simpset() addsimps [znegative_iff_zless_0,
- not_zless_iff_zle]) 1);
-qed "int_of_nat_of";
-
-Addsimps [int_of_nat_of, nat_of_zminus_int_of];
-
-Goal "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)";
-by (simp_tac (simpset() addsimps [int_of_nat_of,
- znegative_iff_zless_0, not_zle_iff_zless]) 1);
-qed "int_of_nat_of_if";
-
-Goal "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)";
-by (case_tac "znegative(z)" 1);
-by (etac (not_zneg_nat_of RS subst) 2);
-by (auto_tac (claset() addDs [zless_trans]
- addSDs [zero_zle_int_of RS zle_zless_trans],
- simpset() addsimps [znegative_iff_zless_0]));
-qed "zless_nat_iff_int_zless";
-
-
-(** nat_of and zless **)
-
-(*An alternative condition is $#0 <= w *)
-Goal "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)";
-by (rtac iff_trans 1);
-by (rtac (zless_int_of RS iff_sym) 1);
-by (auto_tac (claset(),
- simpset() addsimps [int_of_nat_of_if] delsimps [zless_int_of]));
-by (auto_tac (claset() addEs [zless_asym],
- simpset() addsimps [not_zle_iff_zless]));
-by (blast_tac (claset() addIs [zless_zle_trans]) 1);
-val lemma = result();
-
-Goal "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)";
-by (case_tac "$#0 $< z" 1);
-by (auto_tac (claset(),
- simpset() addsimps [lemma, nat_le_int0, not_zless_iff_zle]));
-qed "zless_nat_conj";
-
-(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
- unconditional!
-
- (*The condition "True" is a hack to prevent looping.
- Conditional rewrite rules are tried after unconditional ones, so a rule
- like eq_nat_number_of will be tried first to eliminate #mm=#nn. *)
- Goal "True ==> (integ_of(w) = x) <-> (x = integ_of(w))";
- by Auto_tac;
- qed "integ_of_reorient";
- Addsimps [integ_of_reorient];
-*)
-
-Goal "(integ_of(w) = $- x) <-> ($- x = integ_of(w))";
-by Auto_tac;
-qed "integ_of_minus_reorient";
-Addsimps [integ_of_minus_reorient];
-
-Goal "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))";
-by Auto_tac;
-qed "integ_of_add_reorient";
-Addsimps [integ_of_add_reorient];
-
-Goal "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))";
-by Auto_tac;
-qed "integ_of_diff_reorient";
-Addsimps [integ_of_diff_reorient];
-
-Goal "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))";
-by Auto_tac;
-qed "integ_of_mult_reorient";
-Addsimps [integ_of_mult_reorient];
--- a/src/ZF/Integ/Bin.thy Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/Integ/Bin.thy Sat Sep 07 22:04:28 2002 +0200
@@ -3,8 +3,6 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Arithmetic on binary integers.
-
The sign Pls stands for an infinite string of leading 0's.
The sign Min stands for an infinite string of leading 1's.
@@ -16,7 +14,9 @@
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
*)
-Bin = Int + Datatype +
+header{*Arithmetic on Binary Integers*}
+
+theory Bin = Int + Datatype:
consts bin :: i
datatype
@@ -25,55 +25,54 @@
| Bit ("w: bin", "b: bool") (infixl "BIT" 90)
syntax
- "_Int" :: xnum => i ("_")
+ "_Int" :: "xnum => i" ("_")
consts
- integ_of :: i=>i
- NCons :: [i,i]=>i
- bin_succ :: i=>i
- bin_pred :: i=>i
- bin_minus :: i=>i
- bin_add :: [i,i]=>i
- bin_adder :: i=>i
- bin_mult :: [i,i]=>i
+ integ_of :: "i=>i"
+ NCons :: "[i,i]=>i"
+ bin_succ :: "i=>i"
+ bin_pred :: "i=>i"
+ bin_minus :: "i=>i"
+ bin_adder :: "i=>i"
+ bin_mult :: "[i,i]=>i"
primrec
- integ_of_Pls "integ_of (Pls) = $# 0"
- integ_of_Min "integ_of (Min) = $-($#1)"
- integ_of_BIT "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
+ integ_of_Pls: "integ_of (Pls) = $# 0"
+ integ_of_Min: "integ_of (Min) = $-($#1)"
+ integ_of_BIT: "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
primrec (*NCons adds a bit, suppressing leading 0s and 1s*)
- NCons_Pls "NCons (Pls,b) = cond(b,Pls BIT b,Pls)"
- NCons_Min "NCons (Min,b) = cond(b,Min,Min BIT b)"
- NCons_BIT "NCons (w BIT c,b) = w BIT c BIT b"
+ NCons_Pls: "NCons (Pls,b) = cond(b,Pls BIT b,Pls)"
+ NCons_Min: "NCons (Min,b) = cond(b,Min,Min BIT b)"
+ NCons_BIT: "NCons (w BIT c,b) = w BIT c BIT b"
primrec (*successor. If a BIT, can change a 0 to a 1 without recursion.*)
- bin_succ_Pls "bin_succ (Pls) = Pls BIT 1"
- bin_succ_Min "bin_succ (Min) = Pls"
- bin_succ_BIT "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
+ bin_succ_Pls: "bin_succ (Pls) = Pls BIT 1"
+ bin_succ_Min: "bin_succ (Min) = Pls"
+ bin_succ_BIT: "bin_succ (w BIT b) = cond(b, bin_succ(w) BIT 0, NCons(w,1))"
primrec (*predecessor*)
- bin_pred_Pls "bin_pred (Pls) = Min"
- bin_pred_Min "bin_pred (Min) = Min BIT 0"
- bin_pred_BIT "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
+ bin_pred_Pls: "bin_pred (Pls) = Min"
+ bin_pred_Min: "bin_pred (Min) = Min BIT 0"
+ bin_pred_BIT: "bin_pred (w BIT b) = cond(b, NCons(w,0), bin_pred(w) BIT 1)"
primrec (*unary negation*)
- bin_minus_Pls
+ bin_minus_Pls:
"bin_minus (Pls) = Pls"
- bin_minus_Min
+ bin_minus_Min:
"bin_minus (Min) = Pls BIT 1"
- bin_minus_BIT
+ bin_minus_BIT:
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
bin_minus(w) BIT 0)"
primrec (*sum*)
- bin_adder_Pls
+ bin_adder_Pls:
"bin_adder (Pls) = (lam w:bin. w)"
- bin_adder_Min
+ bin_adder_Min:
"bin_adder (Min) = (lam w:bin. bin_pred(w))"
- bin_adder_BIT
+ bin_adder_BIT:
"bin_adder (v BIT x) =
(lam w:bin.
bin_case (v BIT x, bin_pred(v BIT x),
@@ -89,19 +88,610 @@
x xor y)"
*)
-defs
- bin_add_def "bin_add(v,w) == bin_adder(v)`w"
+constdefs
+ bin_add :: "[i,i]=>i"
+ "bin_add(v,w) == bin_adder(v)`w"
primrec
- bin_mult_Pls
+ bin_mult_Pls:
"bin_mult (Pls,w) = Pls"
- bin_mult_Min
+ bin_mult_Min:
"bin_mult (Min,w) = bin_minus(w)"
- bin_mult_BIT
+ bin_mult_BIT:
"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
+
+declare bin.intros [simp,TC]
+
+lemma NCons_Pls_0: "NCons(Pls,0) = Pls"
+by simp
+
+lemma NCons_Pls_1: "NCons(Pls,1) = Pls BIT 1"
+by simp
+
+lemma NCons_Min_0: "NCons(Min,0) = Min BIT 0"
+by simp
+
+lemma NCons_Min_1: "NCons(Min,1) = Min"
+by simp
+
+lemma NCons_BIT: "NCons(w BIT x,b) = w BIT x BIT b"
+by (simp add: bin.case_eqns)
+
+lemmas NCons_simps [simp] =
+ NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
+
+
+
+(** Type checking **)
+
+lemma integ_of_type [TC]: "w: bin ==> integ_of(w) : int"
+apply (induct_tac "w")
+apply (simp_all add: bool_into_nat)
+done
+
+lemma NCons_type [TC]: "[| w: bin; b: bool |] ==> NCons(w,b) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_succ_type [TC]: "w: bin ==> bin_succ(w) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_pred_type [TC]: "w: bin ==> bin_pred(w) : bin"
+by (induct_tac "w", auto)
+
+lemma bin_minus_type [TC]: "w: bin ==> bin_minus(w) : bin"
+by (induct_tac "w", auto)
+
+(*This proof is complicated by the mutual recursion*)
+lemma bin_add_type [rule_format,TC]:
+ "v: bin ==> ALL w: bin. bin_add(v,w) : bin"
+apply (unfold bin_add_def)
+apply (induct_tac "v")
+apply (rule_tac [3] ballI)
+apply (rename_tac [3] "w'")
+apply (induct_tac [3] "w'")
+apply (simp_all add: NCons_type)
+done
+
+lemma bin_mult_type [TC]: "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin"
+by (induct_tac "v", auto)
+
+
+subsubsection{*The Carry and Borrow Functions,
+ @{term bin_succ} and @{term bin_pred}*}
+
+(*NCons preserves the integer value of its argument*)
+lemma integ_of_NCons [simp]:
+ "[| w: bin; b: bool |] ==> integ_of(NCons(w,b)) = integ_of(w BIT b)"
+apply (erule bin.cases)
+apply (auto elim!: boolE)
+done
+
+lemma integ_of_succ [simp]:
+ "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)"
+apply (erule bin.induct)
+apply (auto simp add: zadd_ac elim!: boolE)
+done
+
+lemma integ_of_pred [simp]:
+ "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)"
+apply (erule bin.induct)
+apply (auto simp add: zadd_ac elim!: boolE)
+done
+
+
+subsubsection{*@{term bin_minus}: Unary Negation of Binary Integers*}
+
+lemma integ_of_minus: "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)"
+apply (erule bin.induct)
+apply (auto simp add: zadd_ac zminus_zadd_distrib elim!: boolE)
+done
+
+
+subsubsection{*@{term bin_add}: Binary Addition*}
+
+lemma bin_add_Pls [simp]: "w: bin ==> bin_add(Pls,w) = w"
+by (unfold bin_add_def, simp)
+
+lemma bin_add_Pls_right: "w: bin ==> bin_add(w,Pls) = w"
+apply (unfold bin_add_def)
+apply (erule bin.induct, auto)
+done
+
+lemma bin_add_Min [simp]: "w: bin ==> bin_add(Min,w) = bin_pred(w)"
+by (unfold bin_add_def, simp)
+
+lemma bin_add_Min_right: "w: bin ==> bin_add(w,Min) = bin_pred(w)"
+apply (unfold bin_add_def)
+apply (erule bin.induct, auto)
+done
+
+lemma bin_add_BIT_Pls [simp]: "bin_add(v BIT x,Pls) = v BIT x"
+by (unfold bin_add_def, simp)
+
+lemma bin_add_BIT_Min [simp]: "bin_add(v BIT x,Min) = bin_pred(v BIT x)"
+by (unfold bin_add_def, simp)
+
+lemma bin_add_BIT_BIT [simp]:
+ "[| w: bin; y: bool |]
+ ==> bin_add(v BIT x, w BIT y) =
+ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)"
+by (unfold bin_add_def, simp)
+
+lemma integ_of_add [rule_format]:
+ "v: bin ==>
+ ALL w: bin. integ_of(bin_add(v,w)) = integ_of(v) $+ integ_of(w)"
+apply (erule bin.induct, simp, simp)
+apply (rule ballI)
+apply (induct_tac "wa")
+apply (auto simp add: zadd_ac elim!: boolE)
+done
+
+(*Subtraction*)
+lemma diff_integ_of_eq:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $- integ_of(w) = integ_of(bin_add (v, bin_minus(w)))"
+apply (unfold zdiff_def)
+apply (simp add: integ_of_add integ_of_minus)
+done
+
+
+subsubsection{*@{term bin_mult}: Binary Multiplication*}
+
+lemma integ_of_mult:
+ "[| v: bin; w: bin |]
+ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)"
+apply (induct_tac "v", simp)
+apply (simp add: integ_of_minus)
+apply (auto simp add: zadd_ac integ_of_add zadd_zmult_distrib elim!: boolE)
+done
+
+
+subsection{*Computations*}
+
+(** extra rules for bin_succ, bin_pred **)
+
+lemma bin_succ_1: "bin_succ(w BIT 1) = bin_succ(w) BIT 0"
+by simp
+
+lemma bin_succ_0: "bin_succ(w BIT 0) = NCons(w,1)"
+by simp
+
+lemma bin_pred_1: "bin_pred(w BIT 1) = NCons(w,0)"
+by simp
+
+lemma bin_pred_0: "bin_pred(w BIT 0) = bin_pred(w) BIT 1"
+by simp
+
+(** extra rules for bin_minus **)
+
+lemma bin_minus_1: "bin_minus(w BIT 1) = bin_pred(NCons(bin_minus(w), 0))"
+by simp
+
+lemma bin_minus_0: "bin_minus(w BIT 0) = bin_minus(w) BIT 0"
+by simp
+
+(** extra rules for bin_add **)
+
+lemma bin_add_BIT_11: "w: bin ==> bin_add(v BIT 1, w BIT 1) =
+ NCons(bin_add(v, bin_succ(w)), 0)"
+by simp
+
+lemma bin_add_BIT_10: "w: bin ==> bin_add(v BIT 1, w BIT 0) =
+ NCons(bin_add(v,w), 1)"
+by simp
+
+lemma bin_add_BIT_0: "[| w: bin; y: bool |]
+ ==> bin_add(v BIT 0, w BIT y) = NCons(bin_add(v,w), y)"
+by simp
+
+(** extra rules for bin_mult **)
+
+lemma bin_mult_1: "bin_mult(v BIT 1, w) = bin_add(NCons(bin_mult(v,w),0), w)"
+by simp
+
+lemma bin_mult_0: "bin_mult(v BIT 0, w) = NCons(bin_mult(v,w),0)"
+by simp
+
+
+(** Simplification rules with integer constants **)
+
+lemma int_of_0: "$#0 = #0"
+by simp
+
+lemma int_of_succ: "$# succ(n) = #1 $+ $#n"
+by (simp add: int_of_add [symmetric] natify_succ)
+
+lemma zminus_0 [simp]: "$- #0 = #0"
+by simp
+
+lemma zadd_0_intify [simp]: "#0 $+ z = intify(z)"
+by simp
+
+lemma zadd_0_right_intify [simp]: "z $+ #0 = intify(z)"
+by simp
+
+lemma zmult_1_intify [simp]: "#1 $* z = intify(z)"
+by simp
+
+lemma zmult_1_right_intify [simp]: "z $* #1 = intify(z)"
+by (subst zmult_commute, simp)
+
+lemma zmult_0 [simp]: "#0 $* z = #0"
+by simp
+
+lemma zmult_0_right [simp]: "z $* #0 = #0"
+by (subst zmult_commute, simp)
+
+lemma zmult_minus1 [simp]: "#-1 $* z = $-z"
+by (simp add: zcompare_rls)
+
+lemma zmult_minus1_right [simp]: "z $* #-1 = $-z"
+apply (subst zmult_commute)
+apply (rule zmult_minus1)
+done
+
+
+subsection{*Simplification Rules for Comparison of Binary Numbers*}
+text{*Thanks to Norbert Voelker*}
+
+(** Equals (=) **)
+
+lemma eq_integ_of_eq:
+ "[| v: bin; w: bin |]
+ ==> ((integ_of(v)) = integ_of(w)) <->
+ iszero (integ_of (bin_add (v, bin_minus(w))))"
+apply (unfold iszero_def)
+apply (simp add: zcompare_rls integ_of_add integ_of_minus)
+done
+
+lemma iszero_integ_of_Pls: "iszero (integ_of(Pls))"
+by (unfold iszero_def, simp)
+
+
+lemma nonzero_integ_of_Min: "~ iszero (integ_of(Min))"
+apply (unfold iszero_def)
+apply (simp add: zminus_equation)
+done
+
+lemma iszero_integ_of_BIT:
+ "[| w: bin; x: bool |]
+ ==> iszero (integ_of (w BIT x)) <-> (x=0 & iszero (integ_of(w)))"
+apply (unfold iszero_def, simp)
+apply (subgoal_tac "integ_of (w) : int")
+apply typecheck
+apply (drule int_cases)
+apply (auto elim!: boolE simp add: int_of_add [symmetric])
+apply (simp_all add: zcompare_rls zminus_zadd_distrib [symmetric]
+ int_of_add [symmetric])
+apply (subgoal_tac "znegative ($- $# succ (n)) <-> znegative ($# succ (n))")
+ apply (simp (no_asm_use))
+apply simp
+done
+
+lemma iszero_integ_of_0:
+ "w: bin ==> iszero (integ_of (w BIT 0)) <-> iszero (integ_of(w))"
+by (simp only: iszero_integ_of_BIT, blast)
+
+lemma iszero_integ_of_1: "w: bin ==> ~ iszero (integ_of (w BIT 1))"
+by (simp only: iszero_integ_of_BIT, blast)
+
+
+
+(** Less-than (<) **)
+
+lemma less_integ_of_eq_neg:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $< integ_of(w)
+ <-> znegative (integ_of (bin_add (v, bin_minus(w))))"
+apply (unfold zless_def zdiff_def)
+apply (simp add: integ_of_minus integ_of_add)
+done
+
+lemma not_neg_integ_of_Pls: "~ znegative (integ_of(Pls))"
+by simp
+
+lemma neg_integ_of_Min: "znegative (integ_of(Min))"
+by simp
+
+lemma neg_integ_of_BIT:
+ "[| w: bin; x: bool |]
+ ==> znegative (integ_of (w BIT x)) <-> znegative (integ_of(w))"
+apply simp
+apply (subgoal_tac "integ_of (w) : int")
+apply typecheck
+apply (drule int_cases)
+apply (auto elim!: boolE simp add: int_of_add [symmetric] zcompare_rls)
+apply (simp_all add: zminus_zadd_distrib [symmetric] zdiff_def
+ int_of_add [symmetric])
+apply (subgoal_tac "$#1 $- $# succ (succ (n #+ n)) = $- $# succ (n #+ n) ")
+ apply (simp add: zdiff_def)
+apply (simp add: equation_zminus int_of_diff [symmetric])
+done
+
+(** Less-than-or-equals (<=) **)
+
+lemma le_integ_of_eq_not_less:
+ "(integ_of(x) $<= (integ_of(w))) <-> ~ (integ_of(w) $< (integ_of(x)))"
+by (simp add: not_zless_iff_zle [THEN iff_sym])
+
+
+(*Delete the original rewrites, with their clumsy conditional expressions*)
+declare bin_succ_BIT [simp del]
+ bin_pred_BIT [simp del]
+ bin_minus_BIT [simp del]
+ NCons_Pls [simp del]
+ NCons_Min [simp del]
+ bin_adder_BIT [simp del]
+ bin_mult_BIT [simp del]
+
+(*Hide the binary representation of integer constants*)
+declare integ_of_Pls [simp del] integ_of_Min [simp del] integ_of_BIT [simp del]
+
+
+lemmas bin_arith_extra_simps =
+ integ_of_add [symmetric]
+ integ_of_minus [symmetric]
+ integ_of_mult [symmetric]
+ 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*)
+lemmas 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*)
+lemmas 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
+
+declare bin_arith_simps [simp]
+declare bin_rel_simps [simp]
+
+
+(** Simplification of arithmetic when nested to the right **)
+
+lemma add_integ_of_left [simp]:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $+ (integ_of(w) $+ z) = (integ_of(bin_add(v,w)) $+ z)"
+by (simp add: zadd_assoc [symmetric])
+
+lemma mult_integ_of_left [simp]:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $* (integ_of(w) $* z) = (integ_of(bin_mult(v,w)) $* z)"
+by (simp add: zmult_assoc [symmetric])
+
+lemma add_integ_of_diff1 [simp]:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $+ (integ_of(w) $- c) = integ_of(bin_add(v,w)) $- (c)"
+apply (unfold zdiff_def)
+apply (rule add_integ_of_left, auto)
+done
+
+lemma add_integ_of_diff2 [simp]:
+ "[| v: bin; w: bin |]
+ ==> integ_of(v) $+ (c $- integ_of(w)) =
+ integ_of (bin_add (v, bin_minus(w))) $+ (c)"
+apply (subst diff_integ_of_eq [symmetric])
+apply (simp_all add: zdiff_def zadd_ac)
+done
+
+
+(** More for integer constants **)
+
+declare int_of_0 [simp] int_of_succ [simp]
+
+lemma zdiff0 [simp]: "#0 $- x = $-x"
+by (simp add: zdiff_def)
+
+lemma zdiff0_right [simp]: "x $- #0 = intify(x)"
+by (simp add: zdiff_def)
+
+lemma zdiff_self [simp]: "x $- x = #0"
+by (simp add: zdiff_def)
+
+lemma znegative_iff_zless_0: "k: int ==> znegative(k) <-> k $< #0"
+by (simp add: zless_def)
+
+lemma zero_zless_imp_znegative_zminus: "[|#0 $< k; k: int|] ==> znegative($-k)"
+by (simp add: zless_def)
+
+lemma zero_zle_int_of [simp]: "#0 $<= $# n"
+by (simp add: not_zless_iff_zle [THEN iff_sym] znegative_iff_zless_0 [THEN iff_sym])
+
+lemma nat_of_0 [simp]: "nat_of(#0) = 0"
+by (simp only: natify_0 int_of_0 [symmetric] nat_of_int_of)
+
+lemma nat_le_int0_lemma: "[| z $<= $#0; z: int |] ==> nat_of(z) = 0"
+by (auto simp add: znegative_iff_zless_0 [THEN iff_sym] zle_def zneg_nat_of)
+
+lemma nat_le_int0: "z $<= $#0 ==> nat_of(z) = 0"
+apply (subgoal_tac "nat_of (intify (z)) = 0")
+apply (rule_tac [2] nat_le_int0_lemma, auto)
+done
+
+lemma int_of_eq_0_imp_natify_eq_0: "$# n = #0 ==> natify(n) = 0"
+by (rule not_znegative_imp_zero, auto)
+
+lemma nat_of_zminus_int_of: "nat_of($- $# n) = 0"
+apply (unfold nat_of_def raw_nat_of_def)
+apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
+ iff del: int_of_eq)
+apply (rule the_equality, auto)
+apply (blast intro: int_of_eq_0_imp_natify_eq_0 sym)
+done
+
+lemma int_of_nat_of: "#0 $<= z ==> $# nat_of(z) = intify(z)"
+apply (rule not_zneg_nat_of_intify)
+apply (simp add: znegative_iff_zless_0 not_zless_iff_zle)
+done
+
+declare int_of_nat_of [simp] nat_of_zminus_int_of [simp]
+
+lemma int_of_nat_of_if: "$# nat_of(z) = (if #0 $<= z then intify(z) else #0)"
+by (simp add: int_of_nat_of znegative_iff_zless_0 not_zle_iff_zless)
+
+lemma zless_nat_iff_int_zless: "[| m: nat; z: int |] ==> (m < nat_of(z)) <-> ($#m $< z)"
+apply (case_tac "znegative (z) ")
+apply (erule_tac [2] not_zneg_nat_of [THEN subst])
+apply (auto dest: zless_trans dest!: zero_zle_int_of [THEN zle_zless_trans]
+ simp add: znegative_iff_zless_0)
+done
+
+
+(** nat_of and zless **)
+
+(*An alternative condition is $#0 <= w *)
+lemma zless_nat_conj_lemma: "$#0 $< z ==> (nat_of(w) < nat_of(z)) <-> (w $< z)"
+apply (rule iff_trans)
+apply (rule zless_int_of [THEN iff_sym])
+apply (auto simp add: int_of_nat_of_if simp del: zless_int_of)
+apply (auto elim: zless_asym simp add: not_zle_iff_zless)
+apply (blast intro: zless_zle_trans)
+done
+
+lemma zless_nat_conj: "(nat_of(w) < nat_of(z)) <-> ($#0 $< z & w $< z)"
+apply (case_tac "$#0 $< z")
+apply (auto simp add: zless_nat_conj_lemma nat_le_int0 not_zless_iff_zle)
+done
+
+(*This simprule cannot be added unless we can find a way to make eq_integ_of_eq
+ unconditional!
+ [The condition "True" is a hack to prevent looping.
+ Conditional rewrite rules are tried after unconditional ones, so a rule
+ like eq_nat_number_of will be tried first to eliminate #mm=#nn.]
+ lemma integ_of_reorient [simp]:
+ "True ==> (integ_of(w) = x) <-> (x = integ_of(w))"
+ by auto
+*)
+
+lemma integ_of_minus_reorient [simp]:
+ "(integ_of(w) = $- x) <-> ($- x = integ_of(w))"
+by auto
+
+lemma integ_of_add_reorient [simp]:
+ "(integ_of(w) = x $+ y) <-> (x $+ y = integ_of(w))"
+by auto
+
+lemma integ_of_diff_reorient [simp]:
+ "(integ_of(w) = x $- y) <-> (x $- y = integ_of(w))"
+by auto
+
+lemma integ_of_mult_reorient [simp]:
+ "(integ_of(w) = x $* y) <-> (x $* y = integ_of(w))"
+by auto
+
+ML
+{*
+val bin_pred_Pls = thm "bin_pred_Pls";
+val bin_pred_Min = thm "bin_pred_Min";
+val bin_minus_Pls = thm "bin_minus_Pls";
+val bin_minus_Min = thm "bin_minus_Min";
+
+val NCons_Pls_0 = thm "NCons_Pls_0";
+val NCons_Pls_1 = thm "NCons_Pls_1";
+val NCons_Min_0 = thm "NCons_Min_0";
+val NCons_Min_1 = thm "NCons_Min_1";
+val NCons_BIT = thm "NCons_BIT";
+val NCons_simps = thms "NCons_simps";
+val integ_of_type = thm "integ_of_type";
+val NCons_type = thm "NCons_type";
+val bin_succ_type = thm "bin_succ_type";
+val bin_pred_type = thm "bin_pred_type";
+val bin_minus_type = thm "bin_minus_type";
+val bin_add_type = thm "bin_add_type";
+val bin_mult_type = thm "bin_mult_type";
+val integ_of_NCons = thm "integ_of_NCons";
+val integ_of_succ = thm "integ_of_succ";
+val integ_of_pred = thm "integ_of_pred";
+val integ_of_minus = thm "integ_of_minus";
+val bin_add_Pls = thm "bin_add_Pls";
+val bin_add_Pls_right = thm "bin_add_Pls_right";
+val bin_add_Min = thm "bin_add_Min";
+val bin_add_Min_right = thm "bin_add_Min_right";
+val bin_add_BIT_Pls = thm "bin_add_BIT_Pls";
+val bin_add_BIT_Min = thm "bin_add_BIT_Min";
+val bin_add_BIT_BIT = thm "bin_add_BIT_BIT";
+val integ_of_add = thm "integ_of_add";
+val diff_integ_of_eq = thm "diff_integ_of_eq";
+val integ_of_mult = thm "integ_of_mult";
+val bin_succ_1 = thm "bin_succ_1";
+val bin_succ_0 = thm "bin_succ_0";
+val bin_pred_1 = thm "bin_pred_1";
+val bin_pred_0 = thm "bin_pred_0";
+val bin_minus_1 = thm "bin_minus_1";
+val bin_minus_0 = thm "bin_minus_0";
+val bin_add_BIT_11 = thm "bin_add_BIT_11";
+val bin_add_BIT_10 = thm "bin_add_BIT_10";
+val bin_add_BIT_0 = thm "bin_add_BIT_0";
+val bin_mult_1 = thm "bin_mult_1";
+val bin_mult_0 = thm "bin_mult_0";
+val int_of_0 = thm "int_of_0";
+val int_of_succ = thm "int_of_succ";
+val zminus_0 = thm "zminus_0";
+val zadd_0_intify = thm "zadd_0_intify";
+val zadd_0_right_intify = thm "zadd_0_right_intify";
+val zmult_1_intify = thm "zmult_1_intify";
+val zmult_1_right_intify = thm "zmult_1_right_intify";
+val zmult_0 = thm "zmult_0";
+val zmult_0_right = thm "zmult_0_right";
+val zmult_minus1 = thm "zmult_minus1";
+val zmult_minus1_right = thm "zmult_minus1_right";
+val eq_integ_of_eq = thm "eq_integ_of_eq";
+val iszero_integ_of_Pls = thm "iszero_integ_of_Pls";
+val nonzero_integ_of_Min = thm "nonzero_integ_of_Min";
+val iszero_integ_of_BIT = thm "iszero_integ_of_BIT";
+val iszero_integ_of_0 = thm "iszero_integ_of_0";
+val iszero_integ_of_1 = thm "iszero_integ_of_1";
+val less_integ_of_eq_neg = thm "less_integ_of_eq_neg";
+val not_neg_integ_of_Pls = thm "not_neg_integ_of_Pls";
+val neg_integ_of_Min = thm "neg_integ_of_Min";
+val neg_integ_of_BIT = thm "neg_integ_of_BIT";
+val le_integ_of_eq_not_less = thm "le_integ_of_eq_not_less";
+val bin_arith_extra_simps = thms "bin_arith_extra_simps";
+val bin_arith_simps = thms "bin_arith_simps";
+val bin_rel_simps = thms "bin_rel_simps";
+val add_integ_of_left = thm "add_integ_of_left";
+val mult_integ_of_left = thm "mult_integ_of_left";
+val add_integ_of_diff1 = thm "add_integ_of_diff1";
+val add_integ_of_diff2 = thm "add_integ_of_diff2";
+val zdiff0 = thm "zdiff0";
+val zdiff0_right = thm "zdiff0_right";
+val zdiff_self = thm "zdiff_self";
+val znegative_iff_zless_0 = thm "znegative_iff_zless_0";
+val zero_zless_imp_znegative_zminus = thm "zero_zless_imp_znegative_zminus";
+val zero_zle_int_of = thm "zero_zle_int_of";
+val nat_of_0 = thm "nat_of_0";
+val nat_le_int0 = thm "nat_le_int0";
+val int_of_eq_0_imp_natify_eq_0 = thm "int_of_eq_0_imp_natify_eq_0";
+val nat_of_zminus_int_of = thm "nat_of_zminus_int_of";
+val int_of_nat_of = thm "int_of_nat_of";
+val int_of_nat_of_if = thm "int_of_nat_of_if";
+val zless_nat_iff_int_zless = thm "zless_nat_iff_int_zless";
+val zless_nat_conj = thm "zless_nat_conj";
+val integ_of_minus_reorient = thm "integ_of_minus_reorient";
+val integ_of_add_reorient = thm "integ_of_add_reorient";
+val integ_of_diff_reorient = thm "integ_of_diff_reorient";
+val integ_of_mult_reorient = thm "integ_of_mult_reorient";
+*}
+
end
--- a/src/ZF/Integ/Int.ML Thu Sep 05 14:03:03 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1064 +0,0 @@
-(* Title: ZF/Integ/Int.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-The integers as equivalence classes over nat*nat.
-
-Could also prove...
-"znegative(z) ==> $# zmagnitude(z) = $- z"
-"~ znegative(z) ==> $# zmagnitude(z) = z"
-*)
-
-AddSEs [quotientE];
-
-(*** Proving that intrel is an equivalence relation ***)
-
-(** Natural deduction for intrel **)
-
-Goalw [intrel_def]
- "<<x1,y1>,<x2,y2>>: intrel <-> \
-\ x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
-by (Fast_tac 1);
-qed "intrel_iff";
-
-Goalw [intrel_def]
- "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] \
-\ ==> <<x1,y1>,<x2,y2>>: intrel";
-by (fast_tac (claset() addIs prems) 1);
-qed "intrelI";
-
-(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
-Goalw [intrel_def]
- "p: intrel --> (EX x1 y1 x2 y2. \
-\ p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
-\ x1: nat & y1: nat & x2: nat & y2: nat)";
-by (Fast_tac 1);
-qed "intrelE_lemma";
-
-val [major,minor] = goal (the_context ())
- "[| p: intrel; \
-\ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1; \
-\ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
-\ ==> Q";
-by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "intrelE";
-
-AddSIs [intrelI];
-AddSEs [intrelE];
-
-Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
-by (rtac sym 1);
-by (REPEAT (etac add_left_cancel 1));
-by (ALLGOALS Asm_simp_tac);
-qed "int_trans_lemma";
-
-Goalw [equiv_def, refl_def, sym_def, trans_def]
- "equiv(nat*nat, intrel)";
-by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
-qed "equiv_intrel";
-
-
-Goalw [int_def] "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int";
-by (blast_tac (claset() addIs [quotientI]) 1);
-qed "image_intrel_int";
-
-
-Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
- add_0_right, add_succ_right];
-Addcongs [conj_cong];
-
-bind_thm ("eq_intrelD", equiv_intrel RSN (2,eq_equiv_class));
-
-(** int_of: the injection from nat to int **)
-
-Goalw [int_def,quotient_def,int_of_def] "$#m : int";
-by Auto_tac;
-qed "int_of_type";
-
-Addsimps [int_of_type];
-AddTCs [int_of_type];
-
-
-Goalw [int_of_def] "($# m = $# n) <-> natify(m)=natify(n)";
-by Auto_tac;
-qed "int_of_eq";
-AddIffs [int_of_eq];
-
-Goal "[| $#m = $#n; m: nat; n: nat |] ==> m=n";
-by (dtac (int_of_eq RS iffD1) 1);
-by Auto_tac;
-qed "int_of_inject";
-
-
-(** intify: coercion from anything to int **)
-
-Goal "intify(x) : int";
-by (simp_tac (simpset() addsimps [intify_def]) 1);
-qed "intify_in_int";
-AddIffs [intify_in_int];
-AddTCs [intify_in_int];
-
-Goal "n : int ==> intify(n) = n";
-by (asm_simp_tac (simpset() addsimps [intify_def]) 1);
-qed "intify_ident";
-Addsimps [intify_ident];
-
-
-(*** Collapsing rules: to remove intify from arithmetic expressions ***)
-
-Goal "intify(intify(x)) = intify(x)";
-by (Simp_tac 1);
-qed "intify_idem";
-Addsimps [intify_idem];
-
-Goal "$# (natify(m)) = $# m";
-by (simp_tac (simpset() addsimps [int_of_def]) 1);
-qed "int_of_natify";
-
-Goal "$- (intify(m)) = $- m";
-by (simp_tac (simpset() addsimps [zminus_def]) 1);
-qed "zminus_intify";
-
-Addsimps [int_of_natify, zminus_intify];
-
-(** Addition **)
-
-Goal "intify(x) $+ y = x $+ y";
-by (simp_tac (simpset() addsimps [zadd_def]) 1);
-qed "zadd_intify1";
-
-Goal "x $+ intify(y) = x $+ y";
-by (simp_tac (simpset() addsimps [zadd_def]) 1);
-qed "zadd_intify2";
-Addsimps [zadd_intify1, zadd_intify2];
-
-(** Subtraction **)
-
-Goal "intify(x) $- y = x $- y";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_intify1";
-
-Goal "x $- intify(y) = x $- y";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_intify2";
-Addsimps [zdiff_intify1, zdiff_intify2];
-
-(** Multiplication **)
-
-Goal "intify(x) $* y = x $* y";
-by (simp_tac (simpset() addsimps [zmult_def]) 1);
-qed "zmult_intify1";
-
-Goal "x $* intify(y) = x $* y";
-by (simp_tac (simpset() addsimps [zmult_def]) 1);
-qed "zmult_intify2";
-Addsimps [zmult_intify1, zmult_intify2];
-
-(** Orderings **)
-
-Goal "intify(x) $< y <-> x $< y";
-by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_intify1";
-
-Goal "x $< intify(y) <-> x $< y";
-by (simp_tac (simpset() addsimps [zless_def]) 1);
-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 ****)
-
-Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
-qed "zminus_congruent";
-
-val RSLIST = curry (op MRS);
-
-(*Resolve th against the corresponding facts for zminus*)
-val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
-
-Goalw [int_def,raw_zminus_def] "z : int ==> raw_zminus(z) : int";
-by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
-qed "raw_zminus_type";
-
-Goalw [zminus_def] "$-z : int";
-by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
-qed "zminus_type";
-AddIffs [zminus_type];
-AddTCs [zminus_type];
-
-
-Goalw [int_def,raw_zminus_def]
- "[| raw_zminus(z) = raw_zminus(w); z: int; w: int |] ==> z=w";
-by (etac (zminus_ize UN_equiv_class_inject) 1);
-by Safe_tac;
-by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));
-qed "raw_zminus_inject";
-
-Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
-by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
-qed "zminus_inject_intify";
-
-AddSDs [zminus_inject_intify];
-
-Goal "[| $-z = $-w; z: int; w: int |] ==> z=w";
-by Auto_tac;
-qed "zminus_inject";
-
-Goalw [raw_zminus_def]
- "[| x: nat; y: nat |] \
-\ ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
-qed "raw_zminus";
-
-Goalw [zminus_def]
- "[| x: nat; y: nat |] \
-\ ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
-qed "zminus";
-
-Goalw [int_def] "z : int ==> raw_zminus (raw_zminus(z)) = z";
-by (auto_tac (claset(), simpset() addsimps [raw_zminus]));
-qed "raw_zminus_zminus";
-
-Goal "$- ($- z) = intify(z)";
-by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type,
- raw_zminus_zminus]) 1);
-qed "zminus_zminus_intify";
-
-Goalw [int_of_def] "$- ($#0) = $#0";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_int0";
-
-Addsimps [zminus_zminus_intify, zminus_int0];
-
-Goal "z : int ==> $- ($- z) = z";
-by (Asm_simp_tac 1);
-qed "zminus_zminus";
-
-
-(**** znegative: the test for negative integers ****)
-
-(*No natural number is negative!*)
-Goalw [znegative_def, int_of_def] "~ znegative($# n)";
-by Safe_tac;
-by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
-by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
-by (force_tac (claset(),
- simpset() addsimps [add_le_self2 RS le_imp_not_lt,
- natify_succ]) 1);
-qed "not_znegative_int_of";
-
-Addsimps [not_znegative_int_of];
-AddSEs [not_znegative_int_of RS notE];
-
-Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
-by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
-by (blast_tac (claset() addIs [nat_0_le]) 1);
-qed "znegative_zminus_int_of";
-
-Addsimps [znegative_zminus_int_of];
-
-Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
-by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
-by (dres_inst_tac [("x","0")] spec 1);
-by (auto_tac(claset(),
- simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff RS iff_sym]));
-qed "not_znegative_imp_zero";
-
-(**** nat_of: coercion of an integer to a natural number ****)
-
-Goalw [nat_of_def] "nat_of(intify(z)) = nat_of(z)";
-by Auto_tac;
-qed "nat_of_intify";
-Addsimps [nat_of_intify];
-
-Goalw [nat_of_def, raw_nat_of_def] "nat_of($# n) = natify(n)";
-by (auto_tac (claset(), simpset() addsimps [int_of_eq]));
-qed "nat_of_int_of";
-Addsimps [nat_of_int_of];
-
-Goalw [raw_nat_of_def] "raw_nat_of(z) : nat";
-by Auto_tac;
-by (case_tac "EX! m. m: nat & z = int_of(m)" 1);
-by (asm_simp_tac (simpset() addsimps [the_0]) 2);
-by (rtac theI2 1);
-by Auto_tac;
-qed "raw_nat_of_type";
-
-Goalw [nat_of_def] "nat_of(z) : nat";
-by (simp_tac (simpset() addsimps [raw_nat_of_type]) 1);
-qed "nat_of_type";
-AddIffs [nat_of_type];
-AddTCs [nat_of_type];
-
-(**** zmagnitude: magnitide of an integer, as a natural number ****)
-
-Goalw [zmagnitude_def] "zmagnitude($# n) = natify(n)";
-by (auto_tac (claset(), simpset() addsimps [int_of_eq]));
-qed "zmagnitude_int_of";
-
-Goal "natify(x)=n ==> $#x = $# n";
-by (dtac sym 1);
-by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
-qed "natify_int_of_eq";
-
-Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
-by (rtac the_equality 1);
-by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq],
- simpset())
- delIffs [int_of_eq]));
-by Auto_tac;
-qed "zmagnitude_zminus_int_of";
-
-Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
-
-Goalw [zmagnitude_def] "zmagnitude(z) : nat";
-by (rtac theI2 1);
-by Auto_tac;
-qed "zmagnitude_type";
-AddIffs [zmagnitude_type];
-AddTCs [zmagnitude_type];
-
-Goalw [int_def, znegative_def, int_of_def]
- "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n";
-by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
-by (rename_tac "i j" 1);
-by (dres_inst_tac [("x", "i")] spec 1);
-by (dres_inst_tac [("x", "j")] spec 1);
-by (rtac bexI 1);
-by (rtac (add_diff_inverse2 RS sym) 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1);
-qed "not_zneg_int_of";
-
-Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z";
-by (dtac not_zneg_int_of 1);
-by Auto_tac;
-qed "not_zneg_mag";
-
-Addsimps [not_zneg_mag];
-
-Goalw [int_def, znegative_def, int_of_def]
- "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))";
-by (auto_tac(claset() addSDs [less_imp_succ_add],
- simpset() addsimps [zminus, image_singleton_iff]));
-qed "zneg_int_of";
-
-Goal "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z";
-by (dtac zneg_int_of 1);
-by Auto_tac;
-qed "zneg_mag";
-
-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";
-
-Goal "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z";
-by (dtac not_zneg_int_of 1);
-by (auto_tac (claset(), simpset() addsimps [raw_nat_of_type]));
-by (auto_tac (claset(), simpset() addsimps [raw_nat_of_def]));
-qed "not_zneg_raw_nat_of";
-
-Goal "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)";
-by (asm_simp_tac (simpset() addsimps [nat_of_def, not_zneg_raw_nat_of]) 1);
-qed "not_zneg_nat_of_intify";
-
-Goal "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z";
-by (asm_simp_tac (simpset() addsimps [not_zneg_nat_of_intify]) 1);
-qed "not_zneg_nat_of";
-
-Goalw [nat_of_def, raw_nat_of_def] "znegative(intify(z)) ==> nat_of(z) = 0";
-by Auto_tac;
-qed "zneg_nat_of";
-Addsimps [zneg_nat_of];
-
-
-(**** zadd: addition on int ****)
-
-(** Congruence property for addition **)
-
-Goalw [congruent2_def]
- "congruent2(intrel, %z1 z2. \
-\ let <x1,y1>=z1; <x2,y2>=z2 \
-\ in intrel``{<x1#+x2, y1#+y2>})";
-(*Proof via congruent2_commuteI seems longer*)
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
-(*The rest should be trivial, but rearranging terms is hard;
- add_ac does not help rewriting with the assumptions.*)
-by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
-by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 1);
-by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
-qed "zadd_congruent2";
-
-(*Resolve th against the corresponding facts for zadd*)
-val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
-
-Goalw [int_def,raw_zadd_def] "[| z: int; w: int |] ==> raw_zadd(z,w) : int";
-by (rtac (zadd_ize UN_equiv_class_type2) 1);
-by (simp_tac (simpset() addsimps [Let_def]) 3);
-by (REPEAT (assume_tac 1));
-qed "raw_zadd_type";
-
-Goal "z $+ w : int";
-by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type]) 1);
-qed "zadd_type";
-AddIffs [zadd_type]; AddTCs [zadd_type];
-
-Goalw [raw_zadd_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
-\ ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#+x2, y1#+y2>}";
-by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
-by (simp_tac (simpset() addsimps [Let_def]) 1);
-qed "raw_zadd";
-
-Goalw [zadd_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
-\ ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#+x2, y1#+y2>}";
-by (asm_simp_tac (simpset() addsimps [raw_zadd, image_intrel_int]) 1);
-qed "zadd";
-
-Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
-by (auto_tac (claset(), simpset() addsimps [raw_zadd]));
-qed "raw_zadd_int0";
-
-Goal "$#0 $+ z = intify(z)";
-by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
-qed "zadd_int0_intify";
-Addsimps [zadd_int0_intify];
-
-Goal "z: int ==> $#0 $+ z = z";
-by (Asm_simp_tac 1);
-qed "zadd_int0";
-
-Goalw [int_def]
- "[| z: int; w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
-by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));
-qed "raw_zminus_zadd_distrib";
-
-Goal "$- (z $+ w) = $- z $+ $- w";
-by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
-qed "zminus_zadd_distrib";
-
-Addsimps [zminus_zadd_distrib];
-
-Goalw [int_def] "[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
-by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));
-qed "raw_zadd_commute";
-
-Goal "z $+ w = w $+ z";
-by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_commute]) 1);
-qed "zadd_commute";
-
-Goalw [int_def]
- "[| z1: int; z2: int; z3: int |] \
-\ ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))";
-by (auto_tac (claset(), simpset() addsimps [raw_zadd, add_assoc]));
-qed "raw_zadd_assoc";
-
-Goal "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
-by (simp_tac (simpset() addsimps [zadd_def, raw_zadd_type, raw_zadd_assoc]) 1);
-qed "zadd_assoc";
-
-(*For AC rewriting*)
-Goal "z1$+(z2$+z3) = z2$+(z1$+z3)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [zadd_commute]) 1);
-qed "zadd_left_commute";
-
-(*Integer addition is an AC operator*)
-bind_thms ("zadd_ac", [zadd_assoc, zadd_commute, zadd_left_commute]);
-
-Goalw [int_of_def] "$# (m #+ n) = ($#m) $+ ($#n)";
-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";
-
-Goal "z $+ ($- z) = $#0";
-by (simp_tac (simpset() addsimps [zadd_def]) 1);
-by (stac (zminus_intify RS sym) 1);
-by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1);
-qed "zadd_zminus_inverse";
-
-Goal "($- z) $+ z = $#0";
-by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
-qed "zadd_zminus_inverse2";
-
-Goal "z $+ $#0 = intify(z)";
-by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
-qed "zadd_int0_right_intify";
-Addsimps [zadd_int0_right_intify];
-
-Goal "z:int ==> z $+ $#0 = z";
-by (Asm_simp_tac 1);
-qed "zadd_int0_right";
-
-Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
-
-
-
-(**** zmult: multiplication on int ****)
-
-(** Congruence property for multiplication **)
-
-Goal "congruent2(intrel, %p1 p2. \
-\ split(%x1 y1. split(%x2 y2. \
-\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
-by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by Auto_tac;
-(*Proof that zmult is congruent in one argument*)
-by (rename_tac "x y" 1);
-by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
-by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
-by (REPEAT (etac add_left_cancel 1));
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
-by Auto_tac;
-qed "zmult_congruent2";
-
-
-(*Resolve th against the corresponding facts for zmult*)
-val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
-
-Goalw [int_def,raw_zmult_def] "[| z: int; w: int |] ==> raw_zmult(z,w) : int";
-by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
- split_type, add_type, mult_type,
- quotientI, SigmaI] 1));
-qed "raw_zmult_type";
-
-Goal "z $* w : int";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type]) 1);
-qed "zmult_type";
-AddIffs [zmult_type]; AddTCs [zmult_type];
-
-Goalw [raw_zmult_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
-\ ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
-qed "raw_zmult";
-
-Goalw [zmult_def]
- "[| x1: nat; y1: nat; x2: nat; y2: nat |] \
-\ ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) = \
-\ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (asm_simp_tac (simpset() addsimps [raw_zmult, image_intrel_int]) 1);
-qed "zmult";
-
-Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
-by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
-qed "raw_zmult_int0";
-
-Goal "$#0 $* z = $#0";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
-qed "zmult_int0";
-Addsimps [zmult_int0];
-
-Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
-by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
-qed "raw_zmult_int1";
-
-Goal "$#1 $* z = intify(z)";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
-qed "zmult_int1_intify";
-Addsimps [zmult_int1_intify];
-
-Goal "z : int ==> $#1 $* z = z";
-by (Asm_simp_tac 1);
-qed "zmult_int1";
-
-Goalw [int_def] "[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
-by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));
-qed "raw_zmult_commute";
-
-Goal "z $* w = w $* z";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_commute]) 1);
-qed "zmult_commute";
-
-Goalw [int_def]
- "[| z: int; w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
-by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));
-qed "raw_zmult_zminus";
-
-Goal "($- z) $* w = $- (z $* w)";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
-by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1);
-by Auto_tac;
-qed "zmult_zminus";
-Addsimps [zmult_zminus];
-
-Goal "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 |] \
-\ ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))";
-by (auto_tac (claset(),
- simpset() addsimps [raw_zmult, add_mult_distrib_left] @ add_ac @ mult_ac));
-qed "raw_zmult_assoc";
-
-Goal "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_type,
- raw_zmult_assoc]) 1);
-qed "zmult_assoc";
-
-(*For AC rewriting*)
-Goal "z1$*(z2$*z3) = z2$*(z1$*z3)";
-by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_commute]) 1);
-qed "zmult_left_commute";
-
-(*Integer multiplication is an AC operator*)
-bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
-
-Goalw [int_def]
- "[| z1: int; z2: int; w: int |] \
-\ ==> raw_zmult(raw_zadd(z1,z2), w) = \
-\ raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))";
-by (auto_tac (claset(),
- simpset() addsimps [raw_zadd, raw_zmult, add_mult_distrib_left] @
- add_ac @ mult_ac));
-qed "raw_zadd_zmult_distrib";
-
-Goal "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
-by (simp_tac (simpset() addsimps [zmult_def, zadd_def, raw_zadd_type,
- raw_zmult_type, raw_zadd_zmult_distrib]) 1);
-qed "zadd_zmult_distrib";
-
-Goal "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)";
-by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute,
- zadd_zmult_distrib]) 1);
-qed "zadd_zmult_distrib2";
-
-bind_thms ("int_typechecks",
- [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type]);
-
-
-(*** Subtraction laws ***)
-
-Goal "z $- w : int";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff_type";
-AddIffs [zdiff_type]; AddTCs [zdiff_type];
-
-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);
-by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
-qed "zdiff_zmult_distrib";
-
-Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
-by (simp_tac (simpset() addsimps [inst "z" "w" zmult_commute, zdiff_zmult_distrib]) 1);
-qed "zdiff_zmult_distrib2";
-
-Goal "x $+ (y $- z) = (x $+ y) $- z";
-by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
-qed "zadd_zdiff_eq";
-
-Goal "(x $- y) $+ z = (x $+ z) $- y";
-by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
-qed "zdiff_zadd_eq";
-
-
-(*** "Less Than" ***)
-
-(*"Less than" is a linear ordering*)
-Goalw [int_def, zless_def, znegative_def, zdiff_def]
- "[| z: int; w: int |] ==> z$<w | z=w | w$<z";
-by Auto_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
-by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
-by (ALLGOALS (force_tac (claset() addSDs [spec],
- simpset() addsimps add_ac)));
-qed "zless_linear_lemma";
-
-Goal "z$<w | intify(z)=intify(w) | w$<z";
-by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
-by Auto_tac;
-qed "zless_linear";
-
-Goal "~ (z$<z)";
-by (auto_tac (claset(),
- simpset() addsimps [zless_def, znegative_def, int_of_def,
- zdiff_def]));
-by (rotate_tac 2 1);
-by Auto_tac;
-qed "zless_not_refl";
-AddIffs [zless_not_refl];
-
-Goal "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)";
-by (cut_inst_tac [("z","x"),("w","y")] zless_linear 1);
-by Auto_tac;
-qed "neq_iff_zless";
-
-Goal "w $< z ==> intify(w) ~= intify(z)";
-by Auto_tac;
-by (subgoal_tac "~ (intify(w) $< intify(z))" 1);
-by (etac ssubst 2);
-by (Full_simp_tac 1);
-by Auto_tac;
-qed "zless_imp_intify_neq";
-
-(*This lemma allows direct proofs of other <-properties*)
-Goalw [zless_def, znegative_def, zdiff_def, int_def]
- "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))";
-by (auto_tac (claset() addSDs [less_imp_succ_add],
- simpset() addsimps [zadd, zminus, int_of_def]));
-by (res_inst_tac [("x","k")] bexI 1);
-by (etac add_left_cancel 1);
-by Auto_tac;
-val lemma = result();
-
-Goal "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
-by (subgoal_tac "intify(w) $< intify(z)" 1);
-by (dres_inst_tac [("w","intify(w)")] lemma 1);
-by Auto_tac;
-qed "zless_imp_succ_zadd";
-
-Goalw [zless_def, znegative_def, zdiff_def, int_def]
- "w : int ==> w $< w $+ $# succ(n)";
-by (auto_tac (claset(),
- simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
-by (res_inst_tac [("x","0")] exI 1);
-by Auto_tac;
-val lemma = result();
-
-Goal "w $< w $+ $# succ(n)";
-by (cut_facts_tac [intify_in_int RS lemma] 1);
-by Auto_tac;
-qed "zless_succ_zadd";
-
-Goal "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))";
-by (rtac iffI 1);
-by (etac zless_imp_succ_zadd 1);
-by Auto_tac;
-by (rename_tac "n" 1);
-by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
-by Auto_tac;
-qed "zless_iff_succ_zadd";
-
-Goal "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)";
-by (asm_simp_tac (simpset() addsimps [less_iff_succ_add, zless_iff_succ_zadd,
- int_of_add RS sym]) 1);
-by (blast_tac (claset() addIs [sym]) 1);
-qed "zless_int_of";
-Addsimps [zless_int_of];
-
-Goalw [zless_def, znegative_def, zdiff_def, int_def]
- "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z";
-by (auto_tac (claset(), simpset() addsimps [zadd, zminus, image_iff]));
-by (rename_tac "x1 x2 y1 y2" 1);
-by (res_inst_tac [("x","x1#+x2")] exI 1);
-by (res_inst_tac [("x","y1#+y2")] exI 1);
-by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));
-by (rtac sym 1);
-by (REPEAT (etac add_left_cancel 1));
-by Auto_tac;
-qed "zless_trans_lemma";
-
-Goal "[| x $< y; y $< z |] ==> x $< z";
-by (subgoal_tac "intify(x) $< intify(z)" 1);
-by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
-by Auto_tac;
-qed "zless_trans";
-
-Goal "z $< w ==> ~ (w $< z)";
-by (blast_tac (claset() addDs [zless_trans]) 1);
-qed "zless_not_sym";
-
-(* [| z $< w; ~ P ==> w $< z |] ==> P *)
-bind_thm ("zless_asym", zless_not_sym RS swap);
-
-Goalw [zle_def] "z $< w ==> z $<= w";
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zless_imp_zle";
-
-Goal "z $<= w | w $<= z";
-by (simp_tac (simpset() addsimps [zle_def]) 1);
-by (cut_facts_tac [zless_linear] 1);
-by (Blast_tac 1);
-qed "zle_linear";
-
-
-(*** "Less Than or Equals", $<= ***)
-
-Goalw [zle_def] "z $<= z";
-by Auto_tac;
-qed "zle_refl";
-
-Goal "x=y ==> x $<= y";
-by (asm_simp_tac (simpset() addsimps [zle_refl]) 1);
-qed "zle_eq_refl";
-
-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_intify";
-
-Goal "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y";
-by (dtac zle_anti_sym_intify 1);
-by Auto_tac;
-qed "zle_anti_sym";
-
-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";
-
-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() addSDs [zless_imp_intify_neq], simpset()));
-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);
-qed "zdiff_zdiff_eq";
-
-Goal "x $- (y $- z) = (x $+ z) $- y";
-by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
-qed "zdiff_zdiff_eq2";
-
-Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
-by (simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zdiff_zless_iff";
-
-Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
-by (simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zless_zdiff_iff";
-
-Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
-by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
-qed "zdiff_eq_iff";
-
-Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
-by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
-qed "eq_zdiff_iff";
-
-Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
-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: 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
- of the CancelNumerals simprocs ***)
-
-Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
-by Safe_tac;
-by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
-by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zadd_left_cancel";
-
-Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
-by (rtac iff_trans 1);
-by (rtac zadd_left_cancel 2);
-by Auto_tac;
-qed "zadd_left_cancel_intify";
-
-Addsimps [zadd_left_cancel_intify];
-
-Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
-by Safe_tac;
-by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
-by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
-qed "zadd_right_cancel";
-
-Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
-by (rtac iff_trans 1);
-by (rtac zadd_right_cancel 2);
-by Auto_tac;
-qed "zadd_right_cancel_intify";
-
-Addsimps [zadd_right_cancel_intify];
-
-
-Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
-by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
-by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
-qed "zadd_right_cancel_zless";
-
-Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
-by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
- zadd_right_cancel_zless]) 1);
-qed "zadd_left_cancel_zless";
-
-Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
-
-
-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) <-> 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];
-
-
-(*"v $<= w ==> v$+z $<= w$+z"*)
-bind_thm ("zadd_zless_mono1", zadd_right_cancel_zless RS iffD2);
-
-(*"v $<= w ==> z$+v $<= z$+w"*)
-bind_thm ("zadd_zless_mono2", zadd_left_cancel_zless RS iffD2);
-
-(*"v $<= w ==> v$+z $<= w$+z"*)
-bind_thm ("zadd_zle_mono1", zadd_right_cancel_zle RS iffD2);
-
-(*"v $<= w ==> z$+v $<= z$+w"*)
-bind_thm ("zadd_zle_mono2", zadd_left_cancel_zle RS iffD2);
-
-Goal "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z";
-by (etac (zadd_zle_mono1 RS zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zle_mono";
-
-Goal "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z";
-by (etac (zadd_zless_mono1 RS zless_zle_trans) 1);
-by (Simp_tac 1);
-qed "zadd_zless_mono";
-
-
-(*** Comparison laws ***)
-
-Goal "($- x $< $- y) <-> (y $< x)";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zminus_zless_zminus";
-Addsimps [zminus_zless_zminus];
-
-Goal "($- x $<= $- y) <-> (y $<= x)";
-by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym]) 1);
-qed "zminus_zle_zminus";
-Addsimps [zminus_zle_zminus];
-
-
-(*** 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";
-
-Goal "(intify(x) = $- y) <-> (intify(y) = $- x)";
-by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] equation_zminus 1);
-by Auto_tac;
-qed "equation_zminus_intify";
-
-Goal "($- x = intify(y)) <-> ($- y = intify(x))";
-by (cut_inst_tac [("x","intify(x)"), ("y","intify(y)")] zminus_equation 1);
-by Auto_tac;
-qed "zminus_equation_intify";
-
-
-(** The next several equations are permutative: watch out! **)
-
-Goal "(x $< $- y) <-> (y $< $- x)";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zless_zminus";
-
-Goal "($- x $< y) <-> ($- y $< x)";
-by (simp_tac (simpset() addsimps [zless_def, zdiff_def] @ zadd_ac) 1);
-qed "zminus_zless";
-
-Goal "(x $<= $- y) <-> (y $<= $- x)";
-by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym,
- zminus_zless]) 1);
-qed "zle_zminus";
-
-Goal "($- x $<= y) <-> ($- y $<= x)";
-by (simp_tac (simpset() addsimps [not_zless_iff_zle RS iff_sym,
- zless_zminus]) 1);
-qed "zminus_zle";
--- a/src/ZF/Integ/Int.thy Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/Integ/Int.thy Sat Sep 07 22:04:28 2002 +0200
@@ -3,51 +3,52 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
-The integers as equivalence classes over nat*nat.
*)
-Int = EquivClass + ArithSimp +
+header{*The Integers as Equivalence Classes Over Pairs of Natural Numbers*}
+
+theory Int = EquivClass + ArithSimp:
constdefs
intrel :: i
- "intrel == {p:(nat*nat)*(nat*nat).
+ "intrel == {p : (nat*nat)*(nat*nat).
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
int :: i
"int == (nat*nat)//intrel"
- int_of :: i=>i (*coercion from nat to int*) ("$# _" [80] 80)
+ int_of :: "i=>i" --{*coercion from nat to int*} ("$# _" [80] 80)
"$# m == intrel `` {<natify(m), 0>}"
- intify :: i=>i (*coercion from ANYTHING to int*)
+ intify :: "i=>i" --{*coercion from ANYTHING to int*}
"intify(m) == if m : int then m else $#0"
- raw_zminus :: i=>i
+ raw_zminus :: "i=>i"
"raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
- zminus :: i=>i ("$- _" [80] 80)
+ zminus :: "i=>i" ("$- _" [80] 80)
"$- z == raw_zminus (intify(z))"
- znegative :: i=>o
+ znegative :: "i=>o"
"znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
- iszero :: i=>o
+ iszero :: "i=>o"
"iszero(z) == z = $# 0"
- raw_nat_of :: i => i
+ raw_nat_of :: "i=>i"
"raw_nat_of(z) == if znegative(z) then 0
else (THE m. m: nat & z = int_of(m))"
- nat_of :: i => i
+ nat_of :: "i=>i"
"nat_of(z) == raw_nat_of (intify(z))"
- (*could be replaced by an absolute value function from int to int?*)
- zmagnitude :: i=>i
+ zmagnitude :: "i=>i"
+ --{*could be replaced by an absolute value function from int to int?*}
"zmagnitude(z) ==
THE m. m : nat & ((~ znegative(z) & z = $# m) |
(znegative(z) & $- z = $# m))"
- raw_zmult :: [i,i]=>i
+ raw_zmult :: "[i,i]=>i"
(*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
Perhaps a "curried" or even polymorphic congruent predicate would be
better.*)
@@ -55,31 +56,1069 @@
UN p1:z1. UN p2:z2. split(%x1 y1. split(%x2 y2.
intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
- zmult :: [i,i]=>i (infixl "$*" 70)
+ zmult :: "[i,i]=>i" (infixl "$*" 70)
"z1 $* z2 == raw_zmult (intify(z1),intify(z2))"
- raw_zadd :: [i,i]=>i
+ raw_zadd :: "[i,i]=>i"
"raw_zadd (z1, z2) ==
UN z1:z1. UN z2:z2. let <x1,y1>=z1; <x2,y2>=z2
in intrel``{<x1#+x2, y1#+y2>}"
- zadd :: [i,i]=>i (infixl "$+" 65)
+ zadd :: "[i,i]=>i" (infixl "$+" 65)
"z1 $+ z2 == raw_zadd (intify(z1),intify(z2))"
- zdiff :: [i,i]=>i (infixl "$-" 65)
+ zdiff :: "[i,i]=>i" (infixl "$-" 65)
"z1 $- z2 == z1 $+ zminus(z2)"
- zless :: [i,i]=>o (infixl "$<" 50)
+ zless :: "[i,i]=>o" (infixl "$<" 50)
"z1 $< z2 == znegative(z1 $- z2)"
- zle :: [i,i]=>o (infixl "$<=" 50)
+ zle :: "[i,i]=>o" (infixl "$<=" 50)
"z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)"
syntax (xsymbols)
- "zmult" :: [i,i] => i (infixl "$\\<times>" 70)
- "zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than / equals*)
+ zmult :: "[i,i]=>i" (infixl "$\<times>" 70)
+ zle :: "[i,i]=>o" (infixl "$\<le>" 50) --{*less than or equals*}
syntax (HTML output)
- "zmult" :: [i,i] => i (infixl "$\\<times>" 70)
+ zmult :: "[i,i]=>i" (infixl "$\<times>" 70)
+
+
+declare quotientE [elim!]
+
+subsection{*Proving that @{term intrel} is an equivalence relation*}
+
+(** Natural deduction for intrel **)
+
+lemma intrel_iff [simp]:
+ "<<x1,y1>,<x2,y2>>: intrel <->
+ x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1"
+by (unfold intrel_def, fast)
+
+lemma intrelI [intro!]:
+ "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |]
+ ==> <<x1,y1>,<x2,y2>>: intrel"
+by (unfold intrel_def, fast)
+
+lemma intrelE [elim!]:
+ "[| p: intrel;
+ !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>; x1#+y2 = x2#+y1;
+ x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |]
+ ==> Q"
+by (unfold intrel_def, blast)
+
+lemma int_trans_lemma:
+ "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1"
+apply (rule sym)
+apply (erule add_left_cancel)+
+apply (simp_all (no_asm_simp))
+done
+
+lemma equiv_intrel: "equiv(nat*nat, intrel)"
+apply (unfold equiv_def refl_def sym_def trans_def)
+apply (fast elim!: sym int_trans_lemma)
+done
+
+lemma image_intrel_int: "[| m: nat; n: nat |] ==> intrel `` {<m,n>} : int"
+apply (unfold int_def)
+apply (blast intro: quotientI)
+done
+
+declare equiv_intrel [THEN eq_equiv_class_iff, simp]
+declare conj_cong [cong]
+
+lemmas eq_intrelD = eq_equiv_class [OF _ equiv_intrel]
+
+(** int_of: the injection from nat to int **)
+
+lemma int_of_type [simp,TC]: "$#m : int"
+by (unfold int_def quotient_def int_of_def, auto)
+
+lemma int_of_eq [iff]: "($# m = $# n) <-> natify(m)=natify(n)"
+by (unfold int_of_def, auto)
+
+lemma int_of_inject: "[| $#m = $#n; m: nat; n: nat |] ==> m=n"
+by (drule int_of_eq [THEN iffD1], auto)
+
+
+(** intify: coercion from anything to int **)
+
+lemma intify_in_int [iff,TC]: "intify(x) : int"
+by (simp add: intify_def)
+
+lemma intify_ident [simp]: "n : int ==> intify(n) = n"
+by (simp add: intify_def)
+
+
+subsection{*Collapsing rules: to remove @{term intify}
+ from arithmetic expressions*}
+
+lemma intify_idem [simp]: "intify(intify(x)) = intify(x)"
+by simp
+
+lemma int_of_natify [simp]: "$# (natify(m)) = $# m"
+by (simp add: int_of_def)
+
+lemma zminus_intify [simp]: "$- (intify(m)) = $- m"
+by (simp add: zminus_def)
+
+(** Addition **)
+
+lemma zadd_intify1 [simp]: "intify(x) $+ y = x $+ y"
+by (simp add: zadd_def)
+
+lemma zadd_intify2 [simp]: "x $+ intify(y) = x $+ y"
+by (simp add: zadd_def)
+
+(** Subtraction **)
+
+lemma zdiff_intify1 [simp]:"intify(x) $- y = x $- y"
+by (simp add: zdiff_def)
+
+lemma zdiff_intify2 [simp]:"x $- intify(y) = x $- y"
+by (simp add: zdiff_def)
+
+(** Multiplication **)
+
+lemma zmult_intify1 [simp]:"intify(x) $* y = x $* y"
+by (simp add: zmult_def)
+
+lemma zmult_intify2 [simp]:"x $* intify(y) = x $* y"
+by (simp add: zmult_def)
+
+(** Orderings **)
+
+lemma zless_intify1 [simp]:"intify(x) $< y <-> x $< y"
+by (simp add: zless_def)
+
+lemma zless_intify2 [simp]:"x $< intify(y) <-> x $< y"
+by (simp add: zless_def)
+
+lemma zle_intify1 [simp]:"intify(x) $<= y <-> x $<= y"
+by (simp add: zle_def)
+
+lemma zle_intify2 [simp]:"x $<= intify(y) <-> x $<= y"
+by (simp add: zle_def)
+
+
+subsection{*@{term zminus}: unary negation on @{term int}*}
+
+lemma zminus_congruent: "congruent(intrel, %<x,y>. intrel``{<y,x>})"
+apply (unfold congruent_def, safe)
+apply (simp add: add_ac)
+done
+
+lemma raw_zminus_type: "z : int ==> raw_zminus(z) : int"
+apply (unfold int_def raw_zminus_def)
+apply (typecheck add: UN_equiv_class_type [OF equiv_intrel zminus_congruent])
+done
+
+lemma zminus_type [TC,iff]: "$-z : int"
+apply (unfold zminus_def)
+apply (simp add: zminus_def raw_zminus_type)
+done
+
+lemma raw_zminus_inject:
+ "[| raw_zminus(z) = raw_zminus(w); z: int; w: int |] ==> z=w"
+apply (unfold int_def raw_zminus_def)
+apply (erule UN_equiv_class_inject [OF equiv_intrel zminus_congruent], safe)
+apply (auto dest: eq_intrelD simp add: add_ac)
+done
+
+lemma zminus_inject_intify [dest!]: "$-z = $-w ==> intify(z) = intify(w)"
+apply (unfold zminus_def)
+apply (blast dest!: raw_zminus_inject)
+done
+
+lemma zminus_inject: "[| $-z = $-w; z: int; w: int |] ==> z=w"
+by auto
+
+lemma raw_zminus:
+ "[| x: nat; y: nat |] ==> raw_zminus(intrel``{<x,y>}) = intrel `` {<y,x>}"
+apply (unfold raw_zminus_def)
+apply (simp add: UN_equiv_class [OF equiv_intrel zminus_congruent])
+done
+
+lemma zminus:
+ "[| x: nat; y: nat |]
+ ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}"
+apply (unfold zminus_def)
+apply (simp (no_asm_simp) add: raw_zminus image_intrel_int)
+done
+
+lemma raw_zminus_zminus: "z : int ==> raw_zminus (raw_zminus(z)) = z"
+apply (unfold int_def)
+apply (auto simp add: raw_zminus)
+done
+
+lemma zminus_zminus_intify [simp]: "$- ($- z) = intify(z)"
+by (simp add: zminus_def raw_zminus_type raw_zminus_zminus)
+
+lemma zminus_int0 [simp]: "$- ($#0) = $#0"
+apply (unfold int_of_def)
+apply (simp add: zminus)
+done
+
+lemma zminus_zminus: "z : int ==> $- ($- z) = z"
+by simp
+
+
+subsection{*@{term znegative}: the test for negative integers*}
+
+(*No natural number is negative!*)
+lemma not_znegative_int_of [iff]: "~ znegative($# n)"
+apply (unfold znegative_def int_of_def, safe)
+apply (drule_tac psi = "?lhs=?rhs" in asm_rl)
+apply (drule_tac psi = "?lhs<?rhs" in asm_rl)
+apply (force simp add: add_le_self2 [THEN le_imp_not_lt] natify_succ)
+done
+
+lemma znegative_zminus_int_of [simp]: "znegative($- $# succ(n))"
+apply (unfold znegative_def int_of_def)
+apply (simp (no_asm_simp) add: zminus natify_succ)
+apply (blast intro: nat_0_le)
+done
+
+lemma not_znegative_imp_zero: "~ znegative($- $# n) ==> natify(n)=0"
+apply (unfold znegative_def int_of_def)
+apply (simp add: zminus image_singleton_iff)
+apply (drule_tac x = 0 in spec)
+apply (auto simp add: nat_into_Ord [THEN Ord_0_lt_iff, THEN iff_sym])
+done
+
+
+subsection{*@{term nat_of}: Coercion of an Integer to a Natural Number*}
+
+lemma nat_of_intify [simp]: "nat_of(intify(z)) = nat_of(z)"
+by (unfold nat_of_def, auto)
+
+lemma nat_of_int_of [simp]: "nat_of($# n) = natify(n)"
+apply (unfold nat_of_def raw_nat_of_def)
+apply (auto simp add: int_of_eq)
+done
+
+lemma raw_nat_of_type: "raw_nat_of(z) : nat"
+apply (unfold raw_nat_of_def, auto)
+apply (case_tac "EX! m. m: nat & z = int_of (m) ")
+apply (rule theI2)
+apply (simp_all add: the_0)
+done
+
+lemma nat_of_type [iff,TC]: "nat_of(z) : nat"
+apply (unfold nat_of_def)
+apply (simp add: raw_nat_of_type)
+done
+
+subsection{*zmagnitude: magnitide of an integer, as a natural number*}
+
+lemma zmagnitude_int_of [simp]: "zmagnitude($# n) = natify(n)"
+apply (unfold zmagnitude_def)
+apply (auto simp add: int_of_eq)
+done
+
+lemma natify_int_of_eq: "natify(x)=n ==> $#x = $# n"
+apply (drule sym)
+apply (simp (no_asm_simp) add: int_of_eq)
+done
+
+lemma zmagnitude_zminus_int_of [simp]: "zmagnitude($- $# n) = natify(n)"
+apply (unfold zmagnitude_def)
+apply (rule the_equality)
+apply (auto dest!: not_znegative_imp_zero natify_int_of_eq
+ iff del: int_of_eq, auto)
+done
+
+lemma zmagnitude_type [iff,TC]: "zmagnitude(z) : nat"
+apply (unfold zmagnitude_def)
+apply (rule theI2, auto)
+done
+
+lemma not_zneg_int_of:
+ "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"
+apply (unfold int_def znegative_def int_of_def)
+apply (auto simp add: image_singleton_iff)
+apply (rename_tac i j)
+apply (drule_tac x = i in spec)
+apply (drule_tac x = j in spec)
+apply (rule bexI)
+apply (rule add_diff_inverse2 [symmetric], auto)
+apply (simp add: not_lt_iff_le)
+done
+
+lemma not_zneg_mag [simp]:
+ "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"
+by (drule not_zneg_int_of, auto)
+
+lemma zneg_int_of:
+ "[| znegative(z); z: int |] ==> EX n:nat. z = $- ($# succ(n))"
+apply (unfold int_def znegative_def int_of_def)
+apply (auto dest!: less_imp_succ_add simp add: zminus image_singleton_iff)
+done
+
+lemma zneg_mag [simp]:
+ "[| znegative(z); z: int |] ==> $# (zmagnitude(z)) = $- z"
+apply (drule zneg_int_of, auto)
+done
+
+lemma int_cases: "z : int ==> EX n: nat. z = $# n | z = $- ($# succ(n))"
+apply (case_tac "znegative (z) ")
+prefer 2 apply (blast dest: not_zneg_mag sym)
+apply (blast dest: zneg_int_of)
+done
+
+lemma not_zneg_raw_nat_of:
+ "[| ~ znegative(z); z: int |] ==> $# (raw_nat_of(z)) = z"
+apply (drule not_zneg_int_of)
+apply (auto simp add: raw_nat_of_type)
+apply (auto simp add: raw_nat_of_def)
+done
+
+lemma not_zneg_nat_of_intify:
+ "~ znegative(intify(z)) ==> $# (nat_of(z)) = intify(z)"
+by (simp (no_asm_simp) add: nat_of_def not_zneg_raw_nat_of)
+
+lemma not_zneg_nat_of: "[| ~ znegative(z); z: int |] ==> $# (nat_of(z)) = z"
+apply (simp (no_asm_simp) add: not_zneg_nat_of_intify)
+done
+
+lemma zneg_nat_of [simp]: "znegative(intify(z)) ==> nat_of(z) = 0"
+by (unfold nat_of_def raw_nat_of_def, auto)
+
+
+subsection{*@{term zadd}: addition on int*}
+
+text{*Congruence Property for Addition*}
+lemma zadd_congruent2:
+ "congruent2(intrel, %z1 z2.
+ let <x1,y1>=z1; <x2,y2>=z2
+ in intrel``{<x1#+x2, y1#+y2>})"
+apply (unfold congruent2_def)
+(*Proof via congruent2_commuteI seems longer*)
+apply safe
+apply (simp (no_asm_simp) add: add_assoc Let_def)
+(*The rest should be trivial, but rearranging terms is hard
+ add_ac does not help rewriting with the assumptions.*)
+apply (rule_tac m1 = x1a in add_left_commute [THEN ssubst])
+apply (rule_tac m1 = x2a in add_left_commute [THEN ssubst])
+apply (simp (no_asm_simp) add: add_assoc [symmetric])
+done
+
+lemma raw_zadd_type: "[| z: int; w: int |] ==> raw_zadd(z,w) : int"
+apply (unfold int_def raw_zadd_def)
+apply (rule UN_equiv_class_type2 [OF equiv_intrel zadd_congruent2], assumption+)
+apply (simp add: Let_def)
+done
+
+lemma zadd_type [iff,TC]: "z $+ w : int"
+by (simp add: zadd_def raw_zadd_type)
+
+lemma raw_zadd:
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |]
+ ==> raw_zadd (intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
+ intrel `` {<x1#+x2, y1#+y2>}"
+apply (unfold raw_zadd_def)
+apply (simp add: UN_equiv_class2 [OF equiv_intrel zadd_congruent2])
+apply (simp add: Let_def)
+done
+
+lemma zadd:
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |]
+ ==> (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =
+ intrel `` {<x1#+x2, y1#+y2>}"
+apply (unfold zadd_def)
+apply (simp (no_asm_simp) add: raw_zadd image_intrel_int)
+done
+
+lemma raw_zadd_int0: "z : int ==> raw_zadd ($#0,z) = z"
+apply (unfold int_def int_of_def)
+apply (auto simp add: raw_zadd)
+done
+
+lemma zadd_int0_intify [simp]: "$#0 $+ z = intify(z)"
+by (simp add: zadd_def raw_zadd_int0)
+
+lemma zadd_int0: "z: int ==> $#0 $+ z = z"
+by simp
+
+lemma raw_zminus_zadd_distrib:
+ "[| z: int; w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)"
+apply (unfold int_def)
+apply (auto simp add: zminus raw_zadd)
+done
+
+lemma zminus_zadd_distrib [simp]: "$- (z $+ w) = $- z $+ $- w"
+by (simp add: zadd_def raw_zminus_zadd_distrib)
+
+lemma raw_zadd_commute:
+ "[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)"
+apply (unfold int_def)
+apply (auto simp add: raw_zadd add_ac)
+done
+
+lemma zadd_commute: "z $+ w = w $+ z"
+by (simp add: zadd_def raw_zadd_commute)
+
+lemma raw_zadd_assoc:
+ "[| z1: int; z2: int; z3: int |]
+ ==> raw_zadd (raw_zadd(z1,z2),z3) = raw_zadd(z1,raw_zadd(z2,z3))"
+apply (unfold int_def)
+apply (auto simp add: raw_zadd add_assoc)
+done
+
+lemma zadd_assoc: "(z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)"
+by (simp add: zadd_def raw_zadd_type raw_zadd_assoc)
+
+(*For AC rewriting*)
+lemma zadd_left_commute: "z1$+(z2$+z3) = z2$+(z1$+z3)"
+apply (simp add: zadd_assoc [symmetric])
+apply (simp add: zadd_commute)
+done
+
+(*Integer addition is an AC operator*)
+lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
+
+lemma int_of_add: "$# (m #+ n) = ($#m) $+ ($#n)"
+apply (unfold int_of_def)
+apply (simp add: zadd)
+done
+
+lemma int_succ_int_1: "$# succ(m) = $# 1 $+ ($# m)"
+by (simp add: int_of_add [symmetric] natify_succ)
+
+lemma int_of_diff:
+ "[| m: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)"
+apply (unfold int_of_def zdiff_def)
+apply (frule lt_nat_in_nat)
+apply (simp_all add: zadd zminus add_diff_inverse2)
+done
+
+lemma raw_zadd_zminus_inverse: "z : int ==> raw_zadd (z, $- z) = $#0"
+apply (unfold int_def int_of_def)
+apply (auto simp add: zminus raw_zadd add_commute)
+done
+
+lemma zadd_zminus_inverse [simp]: "z $+ ($- z) = $#0"
+apply (simp add: zadd_def)
+apply (subst zminus_intify [symmetric])
+apply (rule intify_in_int [THEN raw_zadd_zminus_inverse])
+done
+
+lemma zadd_zminus_inverse2 [simp]: "($- z) $+ z = $#0"
+by (simp add: zadd_commute zadd_zminus_inverse)
+
+lemma zadd_int0_right_intify [simp]: "z $+ $#0 = intify(z)"
+by (rule trans [OF zadd_commute zadd_int0_intify])
+
+lemma zadd_int0_right: "z:int ==> z $+ $#0 = z"
+by simp
+
+
+subsection{*@{term zmult}: Integer Multiplication*}
+
+text{*Congruence property for multiplication*}
+lemma zmult_congruent2:
+ "congruent2(intrel, %p1 p2.
+ split(%x1 y1. split(%x2 y2.
+ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))"
+apply (rule equiv_intrel [THEN congruent2_commuteI], auto)
+(*Proof that zmult is congruent in one argument*)
+apply (rename_tac x y)
+apply (frule_tac t = "%u. x#*u" in sym [THEN subst_context])
+apply (drule_tac t = "%u. y#*u" in subst_context)
+apply (erule add_left_cancel)+
+apply (simp_all add: add_mult_distrib_left)
+done
+
+
+lemma raw_zmult_type: "[| z: int; w: int |] ==> raw_zmult(z,w) : int"
+apply (unfold int_def raw_zmult_def)
+apply (rule UN_equiv_class_type2 [OF equiv_intrel zmult_congruent2], assumption+)
+apply (simp add: Let_def)
+done
+
+lemma zmult_type [iff,TC]: "z $* w : int"
+by (simp add: zmult_def raw_zmult_type)
+
+lemma raw_zmult:
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |]
+ ==> raw_zmult(intrel``{<x1,y1>}, intrel``{<x2,y2>}) =
+ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
+apply (unfold raw_zmult_def)
+apply (simp add: UN_equiv_class2 [OF equiv_intrel zmult_congruent2])
+done
+
+lemma zmult:
+ "[| x1: nat; y1: nat; x2: nat; y2: nat |]
+ ==> (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =
+ intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}"
+apply (unfold zmult_def)
+apply (simp add: raw_zmult image_intrel_int)
+done
+
+lemma raw_zmult_int0: "z : int ==> raw_zmult ($#0,z) = $#0"
+apply (unfold int_def int_of_def)
+apply (auto simp add: raw_zmult)
+done
+
+lemma zmult_int0 [simp]: "$#0 $* z = $#0"
+by (simp add: zmult_def raw_zmult_int0)
+
+lemma raw_zmult_int1: "z : int ==> raw_zmult ($#1,z) = z"
+apply (unfold int_def int_of_def)
+apply (auto simp add: raw_zmult)
+done
+
+lemma zmult_int1_intify [simp]: "$#1 $* z = intify(z)"
+by (simp add: zmult_def raw_zmult_int1)
+
+lemma zmult_int1: "z : int ==> $#1 $* z = z"
+by simp
+
+lemma raw_zmult_commute:
+ "[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)"
+apply (unfold int_def)
+apply (auto simp add: raw_zmult add_ac mult_ac)
+done
+
+lemma zmult_commute: "z $* w = w $* z"
+by (simp add: zmult_def raw_zmult_commute)
+
+lemma raw_zmult_zminus:
+ "[| z: int; w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)"
+apply (unfold int_def)
+apply (auto simp add: zminus raw_zmult add_ac)
+done
+
+lemma zmult_zminus [simp]: "($- z) $* w = $- (z $* w)"
+apply (simp add: zmult_def raw_zmult_zminus)
+apply (subst zminus_intify [symmetric], rule raw_zmult_zminus, auto)
+done
+
+lemma zmult_zminus_right [simp]: "w $* ($- z) = $- (w $* z)"
+by (simp add: zmult_commute [of w])
+
+lemma raw_zmult_assoc:
+ "[| z1: int; z2: int; z3: int |]
+ ==> raw_zmult (raw_zmult(z1,z2),z3) = raw_zmult(z1,raw_zmult(z2,z3))"
+apply (unfold int_def)
+apply (auto simp add: raw_zmult add_mult_distrib_left add_ac mult_ac)
+done
+
+lemma zmult_assoc: "(z1 $* z2) $* z3 = z1 $* (z2 $* z3)"
+by (simp add: zmult_def raw_zmult_type raw_zmult_assoc)
+
+(*For AC rewriting*)
+lemma zmult_left_commute: "z1$*(z2$*z3) = z2$*(z1$*z3)"
+apply (simp add: zmult_assoc [symmetric])
+apply (simp add: zmult_commute)
+done
+
+(*Integer multiplication is an AC operator*)
+lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
+
+lemma raw_zadd_zmult_distrib:
+ "[| z1: int; z2: int; w: int |]
+ ==> raw_zmult(raw_zadd(z1,z2), w) =
+ raw_zadd (raw_zmult(z1,w), raw_zmult(z2,w))"
+apply (unfold int_def)
+apply (auto simp add: raw_zadd raw_zmult add_mult_distrib_left add_ac mult_ac)
+done
+
+lemma zadd_zmult_distrib: "(z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)"
+by (simp add: zmult_def zadd_def raw_zadd_type raw_zmult_type
+ raw_zadd_zmult_distrib)
+
+lemma zadd_zmult_distrib2: "w $* (z1 $+ z2) = (w $* z1) $+ (w $* z2)"
+by (simp add: zmult_commute [of w] zadd_zmult_distrib)
+
+lemmas int_typechecks =
+ int_of_type zminus_type zmagnitude_type zadd_type zmult_type
+
+
+(*** Subtraction laws ***)
+
+lemma zdiff_type [iff,TC]: "z $- w : int"
+by (simp add: zdiff_def)
+
+lemma zminus_zdiff_eq [simp]: "$- (z $- y) = y $- z"
+by (simp add: zdiff_def zadd_commute)
+
+lemma zdiff_zmult_distrib: "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)"
+apply (unfold zdiff_def)
+apply (subst zadd_zmult_distrib)
+apply (simp add: zmult_zminus)
+done
+
+lemma zdiff_zmult_distrib2: "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)"
+by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
+
+lemma zadd_zdiff_eq: "x $+ (y $- z) = (x $+ y) $- z"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zadd_eq: "(x $- y) $+ z = (x $+ z) $- y"
+by (simp add: zdiff_def zadd_ac)
+
+
+subsection{*The "Less Than" Relation*}
+
+(*"Less than" is a linear ordering*)
+lemma zless_linear_lemma:
+ "[| z: int; w: int |] ==> z$<w | z=w | w$<z"
+apply (unfold int_def zless_def znegative_def zdiff_def, auto)
+apply (simp add: zadd zminus image_iff Bex_def)
+apply (rule_tac i = "xb#+ya" and j = "xc #+ y" in Ord_linear_lt)
+apply (force dest!: spec simp add: add_ac)+
+done
+
+lemma zless_linear: "z$<w | intify(z)=intify(w) | w$<z"
+apply (cut_tac z = " intify (z) " and w = " intify (w) " in zless_linear_lemma)
+apply auto
+done
+
+lemma zless_not_refl [iff]: "~ (z$<z)"
+apply (auto simp add: zless_def znegative_def int_of_def zdiff_def)
+apply (rotate_tac 2, auto)
+done
+
+lemma neq_iff_zless: "[| x: int; y: int |] ==> (x ~= y) <-> (x $< y | y $< x)"
+by (cut_tac z = x and w = y in zless_linear, auto)
+
+lemma zless_imp_intify_neq: "w $< z ==> intify(w) ~= intify(z)"
+apply auto
+apply (subgoal_tac "~ (intify (w) $< intify (z))")
+apply (erule_tac [2] ssubst)
+apply (simp (no_asm_use))
+apply auto
+done
+
+(*This lemma allows direct proofs of other <-properties*)
+lemma zless_imp_succ_zadd_lemma:
+ "[| w $< z; w: int; z: int |] ==> (EX n: nat. z = w $+ $#(succ(n)))"
+apply (unfold zless_def znegative_def zdiff_def int_def)
+apply (auto dest!: less_imp_succ_add simp add: zadd zminus int_of_def)
+apply (rule_tac x = k in bexI)
+apply (erule add_left_cancel, auto)
+done
+
+lemma zless_imp_succ_zadd:
+ "w $< z ==> (EX n: nat. w $+ $#(succ(n)) = intify(z))"
+apply (subgoal_tac "intify (w) $< intify (z) ")
+apply (drule_tac w = "intify (w) " in zless_imp_succ_zadd_lemma)
+apply auto
+done
+
+lemma zless_succ_zadd_lemma:
+ "w : int ==> w $< w $+ $# succ(n)"
+apply (unfold zless_def znegative_def zdiff_def int_def)
+apply (auto simp add: zadd zminus int_of_def image_iff)
+apply (rule_tac x = 0 in exI, auto)
+done
+
+lemma zless_succ_zadd: "w $< w $+ $# succ(n)"
+by (cut_tac intify_in_int [THEN zless_succ_zadd_lemma], auto)
+
+lemma zless_iff_succ_zadd:
+ "w $< z <-> (EX n: nat. w $+ $#(succ(n)) = intify(z))"
+apply (rule iffI)
+apply (erule zless_imp_succ_zadd, auto)
+apply (rename_tac "n")
+apply (cut_tac w = w and n = n in zless_succ_zadd, auto)
+done
+
+lemma zless_int_of [simp]: "[| m: nat; n: nat |] ==> ($#m $< $#n) <-> (m<n)"
+apply (simp add: less_iff_succ_add zless_iff_succ_zadd int_of_add [symmetric])
+apply (blast intro: sym)
+done
+
+lemma zless_trans_lemma:
+ "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z"
+apply (unfold zless_def znegative_def zdiff_def int_def)
+apply (auto simp add: zadd zminus image_iff)
+apply (rename_tac x1 x2 y1 y2)
+apply (rule_tac x = "x1#+x2" in exI)
+apply (rule_tac x = "y1#+y2" in exI)
+apply (auto simp add: add_lt_mono)
+apply (rule sym)
+apply (erule add_left_cancel)+
+apply auto
+done
+
+lemma zless_trans: "[| x $< y; y $< z |] ==> x $< z"
+apply (subgoal_tac "intify (x) $< intify (z) ")
+apply (rule_tac [2] y = "intify (y) " in zless_trans_lemma)
+apply auto
+done
+
+lemma zless_not_sym: "z $< w ==> ~ (w $< z)"
+by (blast dest: zless_trans)
+
+(* [| z $< w; ~ P ==> w $< z |] ==> P *)
+lemmas zless_asym = zless_not_sym [THEN swap, standard]
+
+lemma zless_imp_zle: "z $< w ==> z $<= w"
+apply (unfold zle_def)
+apply (blast elim: zless_asym)
+done
+
+lemma zle_linear: "z $<= w | w $<= z"
+apply (simp add: zle_def)
+apply (cut_tac zless_linear, blast)
+done
+
+
+subsection{*Less Than or Equals*}
+
+lemma zle_refl: "z $<= z"
+by (unfold zle_def, auto)
+
+lemma zle_eq_refl: "x=y ==> x $<= y"
+by (simp add: zle_refl)
+
+lemma zle_anti_sym_intify: "[| x $<= y; y $<= x |] ==> intify(x) = intify(y)"
+apply (unfold zle_def, auto)
+apply (blast dest: zless_trans)
+done
+
+lemma zle_anti_sym: "[| x $<= y; y $<= x; x: int; y: int |] ==> x=y"
+by (drule zle_anti_sym_intify, auto)
+
+lemma zle_trans_lemma:
+ "[| x: int; y: int; z: int; x $<= y; y $<= z |] ==> x $<= z"
+apply (unfold zle_def, auto)
+apply (blast intro: zless_trans)
+done
+
+lemma zle_trans: "[| x $<= y; y $<= z |] ==> x $<= z"
+apply (subgoal_tac "intify (x) $<= intify (z) ")
+apply (rule_tac [2] y = "intify (y) " in zle_trans_lemma)
+apply auto
+done
+
+lemma zle_zless_trans: "[| i $<= j; j $< k |] ==> i $< k"
+apply (auto simp add: zle_def)
+apply (blast intro: zless_trans)
+apply (simp add: zless_def zdiff_def zadd_def)
+done
+
+lemma zless_zle_trans: "[| i $< j; j $<= k |] ==> i $< k"
+apply (auto simp add: zle_def)
+apply (blast intro: zless_trans)
+apply (simp add: zless_def zdiff_def zminus_def)
+done
+
+lemma not_zless_iff_zle: "~ (z $< w) <-> (w $<= z)"
+apply (cut_tac z = z and w = w in zless_linear)
+apply (auto dest: zless_trans simp add: zle_def)
+apply (auto dest!: zless_imp_intify_neq)
+done
+
+lemma not_zle_iff_zless: "~ (z $<= w) <-> (w $< z)"
+by (simp add: not_zless_iff_zle [THEN iff_sym])
+
+
+subsection{*More subtraction laws (for @{text zcompare_rls})*}
+
+lemma zdiff_zdiff_eq: "(x $- y) $- z = x $- (y $+ z)"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zdiff_eq2: "x $- (y $- z) = (x $+ z) $- y"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zless_iff: "(x$-y $< z) <-> (x $< z $+ y)"
+apply (unfold zless_def zdiff_def)
+apply (simp add: zadd_ac)
+done
+
+lemma zless_zdiff_iff: "(x $< z$-y) <-> (x $+ y $< z)"
+apply (unfold zless_def zdiff_def)
+apply (simp add: zadd_ac)
+done
+
+lemma zdiff_eq_iff: "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)"
+apply (unfold zdiff_def)
+apply (auto simp add: zadd_assoc)
+done
+
+lemma eq_zdiff_iff: "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)"
+apply (unfold zdiff_def)
+apply (auto simp add: zadd_assoc)
+done
+
+lemma zdiff_zle_iff_lemma:
+ "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)"
+apply (unfold zle_def)
+apply (auto simp add: zdiff_eq_iff zdiff_zless_iff)
+done
+
+lemma zdiff_zle_iff: "(x$-y $<= z) <-> (x $<= z $+ y)"
+by (cut_tac zdiff_zle_iff_lemma [OF intify_in_int intify_in_int], simp)
+
+lemma zle_zdiff_iff_lemma:
+ "[| x: int; z: int |] ==>(x $<= z$-y) <-> (x $+ y $<= z)"
+apply (unfold zle_def)
+apply (auto simp add: zdiff_eq_iff zless_zdiff_iff)
+apply (auto simp add: zdiff_def zadd_assoc)
+done
+
+lemma zle_zdiff_iff: "(x $<= z$-y) <-> (x $+ y $<= z)"
+by (cut_tac zle_zdiff_iff_lemma [ OF intify_in_int intify_in_int], simp)
+
+text{*This list of rewrites simplifies (in)equalities by bringing subtractions
+ to the top and then moving negative terms to the other side.
+ Use with @{text zadd_ac}*}
+lemmas zcompare_rls =
+ zdiff_def [symmetric]
+ 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
+
+
+subsection{*Monotonicity and Cancellation Results for Instantiation
+ of the CancelNumerals Simprocs*}
+
+lemma zadd_left_cancel:
+ "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)"
+apply safe
+apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
+apply (simp add: zadd_ac)
+done
+
+lemma zadd_left_cancel_intify [simp]:
+ "(z $+ w' = z $+ w) <-> intify(w') = intify(w)"
+apply (rule iff_trans)
+apply (rule_tac [2] zadd_left_cancel, auto)
+done
+
+lemma zadd_right_cancel:
+ "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)"
+apply safe
+apply (drule_tac t = "%x. x $+ ($-z) " in subst_context)
+apply (simp add: zadd_ac)
+done
+
+lemma zadd_right_cancel_intify [simp]:
+ "(w' $+ z = w $+ z) <-> intify(w') = intify(w)"
+apply (rule iff_trans)
+apply (rule_tac [2] zadd_right_cancel, auto)
+done
+
+lemma zadd_right_cancel_zless [simp]: "(w' $+ z $< w $+ z) <-> (w' $< w)"
+apply (simp add: zdiff_zless_iff [THEN iff_sym])
+apply (simp add: zdiff_def zadd_assoc)
+done
+
+lemma zadd_left_cancel_zless [simp]: "(z $+ w' $< z $+ w) <-> (w' $< w)"
+by (simp add: zadd_commute [of z] zadd_right_cancel_zless)
+
+lemma zadd_right_cancel_zle [simp]: "(w' $+ z $<= w $+ z) <-> w' $<= w"
+by (simp add: zle_def)
+
+lemma zadd_left_cancel_zle [simp]: "(z $+ w' $<= z $+ w) <-> w' $<= w"
+by (simp add: zadd_commute [of z] zadd_right_cancel_zle)
+
+
+(*"v $<= w ==> v$+z $<= w$+z"*)
+lemmas zadd_zless_mono1 = zadd_right_cancel_zless [THEN iffD2, standard]
+
+(*"v $<= w ==> z$+v $<= z$+w"*)
+lemmas zadd_zless_mono2 = zadd_left_cancel_zless [THEN iffD2, standard]
+
+(*"v $<= w ==> v$+z $<= w$+z"*)
+lemmas zadd_zle_mono1 = zadd_right_cancel_zle [THEN iffD2, standard]
+
+(*"v $<= w ==> z$+v $<= z$+w"*)
+lemmas zadd_zle_mono2 = zadd_left_cancel_zle [THEN iffD2, standard]
+
+lemma zadd_zle_mono: "[| w' $<= w; z' $<= z |] ==> w' $+ z' $<= w $+ z"
+by (erule zadd_zle_mono1 [THEN zle_trans], simp)
+
+lemma zadd_zless_mono: "[| w' $< w; z' $<= z |] ==> w' $+ z' $< w $+ z"
+by (erule zadd_zless_mono1 [THEN zless_zle_trans], simp)
+
+
+subsection{*Comparison laws*}
+
+lemma zminus_zless_zminus [simp]: "($- x $< $- y) <-> (y $< x)"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zminus_zle_zminus [simp]: "($- x $<= $- y) <-> (y $<= x)"
+by (simp add: not_zless_iff_zle [THEN iff_sym])
+
+subsubsection{*More inequality lemmas*}
+
+lemma equation_zminus: "[| x: int; y: int |] ==> (x = $- y) <-> (y = $- x)"
+by auto
+
+lemma zminus_equation: "[| x: int; y: int |] ==> ($- x = y) <-> ($- y = x)"
+by auto
+
+lemma equation_zminus_intify: "(intify(x) = $- y) <-> (intify(y) = $- x)"
+apply (cut_tac x = "intify (x) " and y = "intify (y) " in equation_zminus)
+apply auto
+done
+
+lemma zminus_equation_intify: "($- x = intify(y)) <-> ($- y = intify(x))"
+apply (cut_tac x = "intify (x) " and y = "intify (y) " in zminus_equation)
+apply auto
+done
+
+
+subsubsection{*The next several equations are permutative: watch out!*}
+
+lemma zless_zminus: "(x $< $- y) <-> (y $< $- x)"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zminus_zless: "($- x $< y) <-> ($- y $< x)"
+by (simp add: zless_def zdiff_def zadd_ac)
+
+lemma zle_zminus: "(x $<= $- y) <-> (y $<= $- x)"
+by (simp add: not_zless_iff_zle [THEN iff_sym] zminus_zless)
+
+lemma zminus_zle: "($- x $<= y) <-> ($- y $<= x)"
+by (simp add: not_zless_iff_zle [THEN iff_sym] zless_zminus)
+
+ML
+{*
+val zdiff_def = thm "zdiff_def";
+val int_of_type = thm "int_of_type";
+val int_of_eq = thm "int_of_eq";
+val int_of_inject = thm "int_of_inject";
+val intify_in_int = thm "intify_in_int";
+val intify_ident = thm "intify_ident";
+val intify_idem = thm "intify_idem";
+val int_of_natify = thm "int_of_natify";
+val zminus_intify = thm "zminus_intify";
+val zadd_intify1 = thm "zadd_intify1";
+val zadd_intify2 = thm "zadd_intify2";
+val zdiff_intify1 = thm "zdiff_intify1";
+val zdiff_intify2 = thm "zdiff_intify2";
+val zmult_intify1 = thm "zmult_intify1";
+val zmult_intify2 = thm "zmult_intify2";
+val zless_intify1 = thm "zless_intify1";
+val zless_intify2 = thm "zless_intify2";
+val zle_intify1 = thm "zle_intify1";
+val zle_intify2 = thm "zle_intify2";
+val zminus_congruent = thm "zminus_congruent";
+val zminus_type = thm "zminus_type";
+val zminus_inject_intify = thm "zminus_inject_intify";
+val zminus_inject = thm "zminus_inject";
+val zminus = thm "zminus";
+val zminus_zminus_intify = thm "zminus_zminus_intify";
+val zminus_int0 = thm "zminus_int0";
+val zminus_zminus = thm "zminus_zminus";
+val not_znegative_int_of = thm "not_znegative_int_of";
+val znegative_zminus_int_of = thm "znegative_zminus_int_of";
+val not_znegative_imp_zero = thm "not_znegative_imp_zero";
+val nat_of_intify = thm "nat_of_intify";
+val nat_of_int_of = thm "nat_of_int_of";
+val nat_of_type = thm "nat_of_type";
+val zmagnitude_int_of = thm "zmagnitude_int_of";
+val natify_int_of_eq = thm "natify_int_of_eq";
+val zmagnitude_zminus_int_of = thm "zmagnitude_zminus_int_of";
+val zmagnitude_type = thm "zmagnitude_type";
+val not_zneg_int_of = thm "not_zneg_int_of";
+val not_zneg_mag = thm "not_zneg_mag";
+val zneg_int_of = thm "zneg_int_of";
+val zneg_mag = thm "zneg_mag";
+val int_cases = thm "int_cases";
+val not_zneg_nat_of_intify = thm "not_zneg_nat_of_intify";
+val not_zneg_nat_of = thm "not_zneg_nat_of";
+val zneg_nat_of = thm "zneg_nat_of";
+val zadd_congruent2 = thm "zadd_congruent2";
+val zadd_type = thm "zadd_type";
+val zadd = thm "zadd";
+val zadd_int0_intify = thm "zadd_int0_intify";
+val zadd_int0 = thm "zadd_int0";
+val zminus_zadd_distrib = thm "zminus_zadd_distrib";
+val zadd_commute = thm "zadd_commute";
+val zadd_assoc = thm "zadd_assoc";
+val zadd_left_commute = thm "zadd_left_commute";
+val zadd_ac = thms "zadd_ac";
+val int_of_add = thm "int_of_add";
+val int_succ_int_1 = thm "int_succ_int_1";
+val int_of_diff = thm "int_of_diff";
+val zadd_zminus_inverse = thm "zadd_zminus_inverse";
+val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2";
+val zadd_int0_right_intify = thm "zadd_int0_right_intify";
+val zadd_int0_right = thm "zadd_int0_right";
+val zmult_congruent2 = thm "zmult_congruent2";
+val zmult_type = thm "zmult_type";
+val zmult = thm "zmult";
+val zmult_int0 = thm "zmult_int0";
+val zmult_int1_intify = thm "zmult_int1_intify";
+val zmult_int1 = thm "zmult_int1";
+val zmult_commute = thm "zmult_commute";
+val zmult_zminus = thm "zmult_zminus";
+val zmult_zminus_right = thm "zmult_zminus_right";
+val zmult_assoc = thm "zmult_assoc";
+val zmult_left_commute = thm "zmult_left_commute";
+val zmult_ac = thms "zmult_ac";
+val zadd_zmult_distrib = thm "zadd_zmult_distrib";
+val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
+val int_typechecks = thms "int_typechecks";
+val zdiff_type = thm "zdiff_type";
+val zminus_zdiff_eq = thm "zminus_zdiff_eq";
+val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
+val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
+val zadd_zdiff_eq = thm "zadd_zdiff_eq";
+val zdiff_zadd_eq = thm "zdiff_zadd_eq";
+val zless_linear = thm "zless_linear";
+val zless_not_refl = thm "zless_not_refl";
+val neq_iff_zless = thm "neq_iff_zless";
+val zless_imp_intify_neq = thm "zless_imp_intify_neq";
+val zless_imp_succ_zadd = thm "zless_imp_succ_zadd";
+val zless_succ_zadd = thm "zless_succ_zadd";
+val zless_iff_succ_zadd = thm "zless_iff_succ_zadd";
+val zless_int_of = thm "zless_int_of";
+val zless_trans = thm "zless_trans";
+val zless_not_sym = thm "zless_not_sym";
+val zless_asym = thm "zless_asym";
+val zless_imp_zle = thm "zless_imp_zle";
+val zle_linear = thm "zle_linear";
+val zle_refl = thm "zle_refl";
+val zle_eq_refl = thm "zle_eq_refl";
+val zle_anti_sym_intify = thm "zle_anti_sym_intify";
+val zle_anti_sym = thm "zle_anti_sym";
+val zle_trans = thm "zle_trans";
+val zle_zless_trans = thm "zle_zless_trans";
+val zless_zle_trans = thm "zless_zle_trans";
+val not_zless_iff_zle = thm "not_zless_iff_zle";
+val not_zle_iff_zless = thm "not_zle_iff_zless";
+val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
+val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
+val zdiff_zless_iff = thm "zdiff_zless_iff";
+val zless_zdiff_iff = thm "zless_zdiff_iff";
+val zdiff_eq_iff = thm "zdiff_eq_iff";
+val eq_zdiff_iff = thm "eq_zdiff_iff";
+val zdiff_zle_iff = thm "zdiff_zle_iff";
+val zle_zdiff_iff = thm "zle_zdiff_iff";
+val zcompare_rls = thms "zcompare_rls";
+val zadd_left_cancel = thm "zadd_left_cancel";
+val zadd_left_cancel_intify = thm "zadd_left_cancel_intify";
+val zadd_right_cancel = thm "zadd_right_cancel";
+val zadd_right_cancel_intify = thm "zadd_right_cancel_intify";
+val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
+val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
+val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
+val zadd_left_cancel_zle = thm "zadd_left_cancel_zle";
+val zadd_zless_mono1 = thm "zadd_zless_mono1";
+val zadd_zless_mono2 = thm "zadd_zless_mono2";
+val zadd_zle_mono1 = thm "zadd_zle_mono1";
+val zadd_zle_mono2 = thm "zadd_zle_mono2";
+val zadd_zle_mono = thm "zadd_zle_mono";
+val zadd_zless_mono = thm "zadd_zless_mono";
+val zminus_zless_zminus = thm "zminus_zless_zminus";
+val zminus_zle_zminus = thm "zminus_zle_zminus";
+val equation_zminus = thm "equation_zminus";
+val zminus_equation = thm "zminus_equation";
+val equation_zminus_intify = thm "equation_zminus_intify";
+val zminus_equation_intify = thm "zminus_equation_intify";
+val zless_zminus = thm "zless_zminus";
+val zminus_zless = thm "zminus_zless";
+val zle_zminus = thm "zle_zminus";
+val zminus_zle = thm "zminus_zle";
+*}
+
+
end
--- a/src/ZF/Integ/IntDiv.thy Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/Integ/IntDiv.thy Sat Sep 07 22:04:28 2002 +0200
@@ -3,8 +3,6 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1999 University of Cambridge
-The division operators div and mod (borrowed from the HOL equivalent)
-
Here is the division algorithm in ML:
fun posDivAlg (a,b) =
@@ -31,6 +29,8 @@
*)
+header{*The Division Operators Div and Mod*}
+
theory IntDiv = IntArith + OrderArith:
constdefs
--- a/src/ZF/Integ/int_arith.ML Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/Integ/int_arith.ML Sat Sep 07 22:04:28 2002 +0200
@@ -184,7 +184,8 @@
zmult_minus1, zmult_minus1_right];
val tc_rules = [integ_of_type, intify_in_int,
- int_of_type, zadd_type, zdiff_type, zmult_type] @ bin.intrs;
+ int_of_type, zadd_type, zdiff_type, zmult_type] @
+ thms "bin.intros";
val intifys = [intify_ident, zadd_intify1, zadd_intify2,
zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
zless_intify1, zless_intify2, zle_intify1, zle_intify2];
--- a/src/ZF/IsaMakefile Thu Sep 05 14:03:03 2002 +0200
+++ b/src/ZF/IsaMakefile Sat Sep 07 22:04:28 2002 +0200
@@ -33,8 +33,8 @@
CardinalArith.thy Cardinal_AC.thy \
Datatype.ML Datatype.thy Epsilon.thy Finite.thy \
Fixedpt.thy Inductive.ML Inductive.thy \
- InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \
- Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \
+ InfDatatype.thy Integ/Bin.thy Integ/EquivClass.ML \
+ Integ/EquivClass.thy Integ/Int.thy Integ/IntArith.thy \
Integ/IntDiv.thy Integ/int_arith.ML \
Let.ML Let.thy List.thy Main.ML Main.thy \
Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \