--- 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];