--- a/src/ZF/EquivClass.ML Tue Sep 22 13:48:32 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-(* Title: ZF/EquivClass.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Equivalence relations in Zermelo-Fraenkel Set Theory
-*)
-
-val RSLIST = curry (op MRS);
-
-open EquivClass;
-
-(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
-
-(** first half: equiv(A,r) ==> converse(r) O r = r **)
-
-Goalw [trans_def,sym_def]
- "[| sym(r); trans(r) |] ==> converse(r) O r <= r";
-by (Blast_tac 1);
-qed "sym_trans_comp_subset";
-
-Goalw [refl_def]
- "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
-by (Blast_tac 1);
-qed "refl_comp_subset";
-
-Goalw [equiv_def]
- "equiv(A,r) ==> converse(r) O r = r";
-by (blast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
-qed "equiv_comp_eq";
-
-(*second half*)
-Goalw [equiv_def,refl_def,sym_def,trans_def]
- "[| converse(r) O r = r; domain(r) = A |] ==> equiv(A,r)";
-by (etac equalityE 1);
-by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
-by (ALLGOALS Fast_tac);
-qed "comp_equivI";
-
-(** Equivalence classes **)
-
-(*Lemma for the next result*)
-Goalw [trans_def,sym_def]
- "[| sym(r); trans(r); <a,b>: r |] ==> r``{a} <= r``{b}";
-by (Blast_tac 1);
-qed "equiv_class_subset";
-
-Goalw [equiv_def]
- "[| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}";
-by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
-by (rewtac sym_def);
-by (Blast_tac 1);
-qed "equiv_class_eq";
-
-Goalw [equiv_def,refl_def]
- "[| equiv(A,r); a: A |] ==> a: r``{a}";
-by (Blast_tac 1);
-qed "equiv_class_self";
-
-(*Lemma for the next result*)
-Goalw [equiv_def,refl_def]
- "[| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> <a,b>: r";
-by (Blast_tac 1);
-qed "subset_equiv_class";
-
-Goal "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> <a,b>: r";
-by (REPEAT (ares_tac[equalityD2, subset_equiv_class] 1));
-qed "eq_equiv_class";
-
-(*thus r``{a} = r``{b} as well*)
-Goalw [equiv_def,trans_def,sym_def]
- "[| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
-by (Blast_tac 1);
-qed "equiv_class_nondisjoint";
-
-Goalw [equiv_def] "equiv(A,r) ==> r <= A*A";
-by (safe_tac subset_cs);
-qed "equiv_type";
-
-Goal "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
-by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
- addDs [equiv_type]) 1);
-qed "equiv_class_eq_iff";
-
-Goal "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
-by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
- addDs [equiv_type]) 1);
-qed "eq_equiv_class_iff";
-
-(*** Quotients ***)
-
-(** Introduction/elimination rules -- needed? **)
-
-Goalw [quotient_def] "x:A ==> r``{x}: A/r";
-by (etac RepFunI 1);
-qed "quotientI";
-
-val major::prems = Goalw [quotient_def]
- "[| X: A/r; !!x. [| X = r``{x}; x:A |] ==> P |] \
-\ ==> P";
-by (rtac (major RS RepFunE) 1);
-by (eresolve_tac prems 1);
-by (assume_tac 1);
-qed "quotientE";
-
-Goalw [equiv_def,refl_def,quotient_def]
- "equiv(A,r) ==> Union(A/r) = A";
-by (Blast_tac 1);
-qed "Union_quotient";
-
-Goalw [quotient_def]
- "[| equiv(A,r); X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)";
-by (safe_tac (claset() addSIs [equiv_class_eq]));
-by (assume_tac 1);
-by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
-by (Blast_tac 1);
-qed "quotient_disj";
-
-(**** Defining unary operations upon equivalence classes ****)
-
-(** These proofs really require as local premises
- equiv(A,r); congruent(r,b)
-**)
-
-(*Conversion rule*)
-val prems as [equivA,bcong,_] = goal EquivClass.thy
- "[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
-by (cut_facts_tac prems 1);
-by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
-by (etac equiv_class_self 2);
-by (assume_tac 2);
-by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
-by (Blast_tac 1);
-qed "UN_equiv_class";
-
-(*type checking of UN x:r``{a}. b(x) *)
-val prems = Goalw [quotient_def]
- "[| equiv(A,r); congruent(r,b); X: A/r; \
-\ !!x. x : A ==> b(x) : B |] \
-\ ==> (UN x:X. b(x)) : B";
-by (cut_facts_tac prems 1);
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps (UN_equiv_class::prems)) 1);
-qed "UN_equiv_class_type";
-
-(*Sufficient conditions for injectiveness. Could weaken premises!
- major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
-*)
-val prems = Goalw [quotient_def]
- "[| equiv(A,r); congruent(r,b); \
-\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
-\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
-\ ==> X=Y";
-by (cut_facts_tac prems 1);
-by Safe_tac;
-by (rtac equiv_class_eq 1);
-by (REPEAT (ares_tac prems 1));
-by (etac box_equals 1);
-by (REPEAT (ares_tac [UN_equiv_class] 1));
-qed "UN_equiv_class_inject";
-
-
-(**** Defining binary operations upon equivalence classes ****)
-
-
-Goalw [congruent_def,congruent2_def,equiv_def,refl_def]
- "[| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))";
-by (Blast_tac 1);
-qed "congruent2_implies_congruent";
-
-val equivA::prems = goalw EquivClass.thy [congruent_def]
- "[| equiv(A,r); congruent2(r,b); a: A |] ==> \
-\ congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
-by (cut_facts_tac (equivA::prems) 1);
-by Safe_tac;
-by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
- congruent2_implies_congruent]) 1);
-by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
-by (Blast_tac 1);
-qed "congruent2_implies_congruent_UN";
-
-val prems as equivA::_ = goal EquivClass.thy
- "[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
-\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
-by (cut_facts_tac prems 1);
-by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
- congruent2_implies_congruent,
- congruent2_implies_congruent_UN]) 1);
-qed "UN_equiv_class2";
-
-(*type checking*)
-val prems = Goalw [quotient_def]
- "[| equiv(A,r); congruent2(r,b); \
-\ X1: A/r; X2: A/r; \
-\ !!x1 x2. [| x1: A; x2: A |] ==> b(x1,x2) : B \
-\ |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
-by (cut_facts_tac prems 1);
-by Safe_tac;
-by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
- congruent2_implies_congruent_UN,
- congruent2_implies_congruent, quotientI]) 1));
-qed "UN_equiv_class_type2";
-
-
-(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
- than the direct proof*)
-val prems = Goalw [congruent2_def,equiv_def,refl_def]
- "[| equiv(A,r); \
-\ !! y z w. [| w: A; <y,z> : r |] ==> b(y,w) = b(z,w); \
-\ !! y z w. [| w: A; <y,z> : r |] ==> b(w,y) = b(w,z) \
-\ |] ==> congruent2(r,b)";
-by (cut_facts_tac prems 1);
-by Safe_tac;
-by (rtac trans 1);
-by (REPEAT (ares_tac prems 1
- ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
-qed "congruent2I";
-
-val [equivA,commute,congt] = Goal
- "[| equiv(A,r); \
-\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
-\ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
-\ |] ==> congruent2(r,b)";
-by (resolve_tac [equivA RS congruent2I] 1);
-by (rtac (commute RS trans) 1);
-by (rtac (commute RS trans RS sym) 3);
-by (rtac sym 5);
-by (REPEAT (ares_tac [congt] 1
- ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
-qed "congruent2_commuteI";
-
-(*Obsolete?*)
-val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
- "[| equiv(A,r); Z: A/r; \
-\ !!w. [| w: A |] ==> congruent(r, %z. b(w,z)); \
-\ !!x y. [| x: A; y: A |] ==> b(y,x) = b(x,y) \
-\ |] ==> congruent(r, %w. UN z: Z. b(w,z))";
-val congt' = rewrite_rule [congruent_def] congt;
-by (cut_facts_tac [ZinA] 1);
-by (rewtac congruent_def);
-by Safe_tac;
-by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [commute,
- [equivA, congt] MRS UN_equiv_class]) 1);
-by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
-qed "congruent_commuteI";
--- a/src/ZF/EquivClass.thy Tue Sep 22 13:48:32 1998 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Title: ZF/EquivClass.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-Equivalence relations in Zermelo-Fraenkel Set Theory
-*)
-
-EquivClass = Rel + Perm +
-consts
- "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
- congruent :: [i,i=>i]=>o
- congruent2 :: [i,[i,i]=>i]=>o
-
-defs
- quotient_def "A/r == {r``{x} . x:A}"
- congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
-
- congruent2_def
- "congruent2(r,b) == ALL y1 z1 y2 z2.
- <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Bin.ML Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,365 @@
+(* 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.case_eqns;
+
+(*Perform induction on l, then prove the major premise using prems. *)
+fun bin_ind_tac a prems i =
+ EVERY [res_inst_tac [("x",a)] bin.induct i,
+ rename_last_tac a ["1"] (i+3),
+ ares_tac prems i];
+
+
+(** bin_rec -- by Vset recursion **)
+
+Goal "bin_rec(Pls,a,b,h) = a";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+qed "bin_rec_Pls";
+
+Goal "bin_rec(Min,a,b,h) = b";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+qed "bin_rec_Min";
+
+Goal "bin_rec(Cons(w,x),a,b,h) = h(w, x, bin_rec(w,a,b,h))";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+qed "bin_rec_Cons";
+
+(*Type checking*)
+val prems = goal Bin.thy
+ "[| w: bin; \
+\ a: C(Pls); b: C(Min); \
+\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(Cons(w,x)) \
+\ |] ==> bin_rec(w,a,b,h) : C(w)";
+by (bin_ind_tac "w" prems 1);
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps prems @ [bin_rec_Pls, bin_rec_Min,
+ bin_rec_Cons])));
+qed "bin_rec_type";
+
+(** Versions for use with definitions **)
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Pls) = a";
+by (rewtac rew);
+by (rtac bin_rec_Pls 1);
+qed "def_bin_rec_Pls";
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Min) = b";
+by (rewtac rew);
+by (rtac bin_rec_Min 1);
+qed "def_bin_rec_Min";
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Cons(w,x)) = h(w,x,j(w))";
+by (rewtac rew);
+by (rtac bin_rec_Cons 1);
+qed "def_bin_rec_Cons";
+
+fun bin_recs def = map standard
+ ([def] RL [def_bin_rec_Pls, def_bin_rec_Min, def_bin_rec_Cons]);
+
+Goalw [NCons_def] "NCons(Pls,0) = Pls";
+by (Asm_simp_tac 1);
+qed "NCons_Pls_0";
+
+Goalw [NCons_def] "NCons(Pls,1) = Cons(Pls,1)";
+by (Asm_simp_tac 1);
+qed "NCons_Pls_1";
+
+Goalw [NCons_def] "NCons(Min,0) = Cons(Min,0)";
+by (Asm_simp_tac 1);
+qed "NCons_Min_0";
+
+Goalw [NCons_def] "NCons(Min,1) = Min";
+by (Asm_simp_tac 1);
+qed "NCons_Min_1";
+
+Goalw [NCons_def]
+ "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
+by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
+qed "NCons_Cons";
+
+val NCons_simps = [NCons_Pls_0, NCons_Pls_1,
+ NCons_Min_0, NCons_Min_1,
+ NCons_Cons];
+
+(** Type checking **)
+
+val bin_typechecks0 = bin_rec_type :: bin.intrs;
+
+Goalw [integ_of_def] "w: bin ==> integ_of(w) : integ";
+by (typechk_tac (bin_typechecks0@integ_typechecks@
+ nat_typechecks@[bool_into_nat]));
+qed "integ_of_type";
+
+Goalw [NCons_def] "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
+by (etac bin.elim 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps bin.case_eqns)));
+by (typechk_tac (bin_typechecks0@bool_typechecks));
+qed "NCons_type";
+
+Goalw [bin_succ_def] "w: bin ==> bin_succ(w) : bin";
+by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
+qed "bin_succ_type";
+
+Goalw [bin_pred_def] "w: bin ==> bin_pred(w) : bin";
+by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
+qed "bin_pred_type";
+
+Goalw [bin_minus_def] "w: bin ==> bin_minus(w) : bin";
+by (typechk_tac ([NCons_type,bin_pred_type]@
+ bin_typechecks0@bool_typechecks));
+qed "bin_minus_type";
+
+Goalw [bin_add_def]
+ "[| v: bin; w: bin |] ==> bin_add(v,w) : bin";
+by (typechk_tac ([NCons_type, bin_succ_type, bin_pred_type]@
+ bin_typechecks0@ bool_typechecks@ZF_typechecks));
+qed "bin_add_type";
+
+Goalw [bin_mult_def]
+ "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
+by (typechk_tac ([NCons_type, bin_minus_type, bin_add_type]@
+ bin_typechecks0@ bool_typechecks));
+qed "bin_mult_type";
+
+val bin_typechecks = bin_typechecks0 @
+ [integ_of_type, NCons_type, bin_succ_type, bin_pred_type,
+ bin_minus_type, bin_add_type, bin_mult_type];
+
+Addsimps ([bool_1I, bool_0I,
+ bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @
+ bin_recs integ_of_def @ bin_typechecks);
+
+val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
+ [bool_subset_nat RS subsetD];
+
+(**** The carry/borrow functions, bin_succ and bin_pred ****)
+
+(** Lemmas **)
+
+goal Integ.thy
+ "!!z v. [| z $+ v = z' $+ v'; \
+\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
+\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+qed "zadd_assoc_cong";
+
+goal Integ.thy
+ "!!z v w. [| z: integ; v: integ; w: integ |] \
+\ ==> z $+ (v $+ w) = v $+ (z $+ w)";
+by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
+qed "zadd_assoc_swap";
+
+(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
+bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap));
+
+
+Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
+
+
+(*NCons preserves the integer value of its argument*)
+Goal "[| w: bin; b: bool |] ==> \
+\ integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
+by (etac bin.elim 1);
+by (asm_simp_tac (simpset() addsimps NCons_simps) 3);
+by (ALLGOALS (etac boolE));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps NCons_simps)));
+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";
+
+(*These two results replace the definitions of bin_succ and bin_pred*)
+
+
+(*** bin_minus: (unary!) negation of binary integers ***)
+
+Addsimps (bin_recs bin_minus_def @ [integ_of_succ, integ_of_pred]);
+
+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(Min,w) = bin_pred(w)";
+by (Asm_simp_tac 1);
+qed "bin_add_Min";
+
+Goalw [bin_add_def] "bin_add(Cons(v,x),Pls) = Cons(v,x)";
+by (Simp_tac 1);
+qed "bin_add_Cons_Pls";
+
+Goalw [bin_add_def] "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
+by (Simp_tac 1);
+qed "bin_add_Cons_Min";
+
+Goalw [bin_add_def]
+ "[| w: bin; y: bool |] ==> \
+\ bin_add(Cons(v,x), Cons(w,y)) = \
+\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
+by (Asm_simp_tac 1);
+qed "bin_add_Cons_Cons";
+
+Addsimps [bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
+ bin_add_Cons_Min, bin_add_Cons_Cons,
+ integ_of_succ, integ_of_pred];
+
+Addsimps [bool_subset_nat RS subsetD];
+
+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 (bin_ind_tac "wa" [] 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
+val integ_of_add_lemma = result();
+
+bind_thm("integ_of_add", integ_of_add_lemma RS bspec);
+
+
+(*** bin_add: binary multiplication ***)
+
+Addsimps (bin_recs bin_mult_def @
+ [integ_of_minus, integ_of_add]);
+
+val major::prems = goal Bin.thy
+ "[| v: bin; w: bin |] ==> \
+\ integ_of(bin_mult(v,w)) = \
+\ integ_of(v) $* integ_of(w)";
+by (cut_facts_tac prems 1);
+by (bin_ind_tac "v" [major] 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+by (etac boolE 1);
+by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
+by (asm_simp_tac
+ (simpset() addsimps [zadd_zmult_distrib, zmult_1] @ zadd_ac) 1);
+qed "integ_of_mult";
+
+(**** Computations ****)
+
+(** extra rules for bin_succ, bin_pred **)
+
+val [bin_succ_Pls, bin_succ_Min, _] = bin_recs bin_succ_def;
+val [bin_pred_Pls, bin_pred_Min, _] = bin_recs bin_pred_def;
+
+Goal "bin_succ(Cons(w,1)) = Cons(bin_succ(w), 0)";
+by (Simp_tac 1);
+qed "bin_succ_Cons1";
+
+Goal "bin_succ(Cons(w,0)) = NCons(w,1)";
+by (Simp_tac 1);
+qed "bin_succ_Cons0";
+
+Goal "bin_pred(Cons(w,1)) = NCons(w,0)";
+by (Simp_tac 1);
+qed "bin_pred_Cons1";
+
+Goal "bin_pred(Cons(w,0)) = Cons(bin_pred(w), 1)";
+by (Simp_tac 1);
+qed "bin_pred_Cons0";
+
+(** extra rules for bin_minus **)
+
+val [bin_minus_Pls, bin_minus_Min, _] = bin_recs bin_minus_def;
+
+Goal "bin_minus(Cons(w,1)) = bin_pred(NCons(bin_minus(w), 0))";
+by (Simp_tac 1);
+qed "bin_minus_Cons1";
+
+Goal "bin_minus(Cons(w,0)) = Cons(bin_minus(w), 0)";
+by (Simp_tac 1);
+qed "bin_minus_Cons0";
+
+(** extra rules for bin_add **)
+
+Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,1)) = \
+\ NCons(bin_add(v, bin_succ(w)), 0)";
+by (Asm_simp_tac 1);
+qed "bin_add_Cons_Cons11";
+
+Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,0)) = \
+\ NCons(bin_add(v,w), 1)";
+by (Asm_simp_tac 1);
+qed "bin_add_Cons_Cons10";
+
+Goal "[| w: bin; y: bool |] ==> \
+\ bin_add(Cons(v,0), Cons(w,y)) = NCons(bin_add(v,w), y)";
+by (Asm_simp_tac 1);
+qed "bin_add_Cons_Cons0";
+
+(** extra rules for bin_mult **)
+
+val [bin_mult_Pls, bin_mult_Min, _] = bin_recs bin_mult_def;
+
+Goal "bin_mult(Cons(v,1), w) = bin_add(NCons(bin_mult(v,w),0), w)";
+by (Simp_tac 1);
+qed "bin_mult_Cons1";
+
+Goal "bin_mult(Cons(v,0), w) = NCons(bin_mult(v,w),0)";
+by (Simp_tac 1);
+qed "bin_mult_Cons0";
+
+
+(*** The computation simpset ***)
+
+(*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
+val bin_comp_ss = simpset_of Integ.thy
+ addsimps [integ_of_add RS sym, (*invoke bin_add*)
+ integ_of_minus RS sym, (*invoke bin_minus*)
+ integ_of_mult RS sym, (*invoke bin_mult*)
+ bin_succ_Pls, bin_succ_Min,
+ bin_succ_Cons1, bin_succ_Cons0,
+ bin_pred_Pls, bin_pred_Min,
+ bin_pred_Cons1, bin_pred_Cons0,
+ bin_minus_Pls, bin_minus_Min,
+ bin_minus_Cons1, bin_minus_Cons0,
+ bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
+ bin_add_Cons_Min, bin_add_Cons_Cons0,
+ bin_add_Cons_Cons10, bin_add_Cons_Cons11,
+ bin_mult_Pls, bin_mult_Min,
+ bin_mult_Cons1, bin_mult_Cons0]
+ @ NCons_simps
+ setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Bin.thy Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,172 @@
+(* Title: ZF/ex/Bin.thy
+ ID: $Id$
+ 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.
+
+A number can have multiple representations, namely leading 0's with sign
+Pls and leading 1's with sign Min. See twos-compl.ML/int_of_binary for
+the numerical interpretation.
+
+The representation expects that (m mod 2) is 0 or 1, even if m is negative;
+For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
+
+Division is not defined yet!
+*)
+
+Bin = Integ + Datatype +
+
+consts
+ bin_rec :: [i, i, i, [i,i,i]=>i] => i
+ 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_mult :: [i,i]=>i
+
+ bin :: i
+
+syntax
+ "_Int" :: xnum => i ("_")
+
+datatype
+ "bin" = Pls
+ | Min
+ | Cons ("w: bin", "b: bool")
+ type_intrs "[bool_into_univ]"
+
+
+defs
+
+ bin_rec_def
+ "bin_rec(z,a,b,h) ==
+ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
+
+ integ_of_def
+ "integ_of(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
+
+ (** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
+
+ (*NCons adds a bit, suppressing leading 0s and 1s*)
+ NCons_def
+ "NCons(w,b) ==
+ bin_case(cond(b,Cons(w,b),w), cond(b,w,Cons(w,b)),
+ %w' x'. Cons(w,b), w)"
+
+ bin_succ_def
+ "bin_succ(w0) ==
+ bin_rec(w0, Cons(Pls,1), Pls,
+ %w x r. cond(x, Cons(r,0), NCons(w,1)))"
+
+ bin_pred_def
+ "bin_pred(w0) ==
+ bin_rec(w0, Min, Cons(Min,0),
+ %w x r. cond(x, NCons(w,0), Cons(r,1)))"
+
+ bin_minus_def
+ "bin_minus(w0) ==
+ bin_rec(w0, Pls, Cons(Pls,1),
+ %w x r. cond(x, bin_pred(NCons(r,0)), Cons(r,0)))"
+
+ bin_add_def
+ "bin_add(v0,w0) ==
+ bin_rec(v0,
+ lam w:bin. w,
+ lam w:bin. bin_pred(w),
+ %v x r. lam w1:bin.
+ bin_rec(w1, Cons(v,x), bin_pred(Cons(v,x)),
+ %w y s. NCons(r`cond(x and y, bin_succ(w), w),
+ x xor y))) ` w0"
+
+ bin_mult_def
+ "bin_mult(v0,w) ==
+ bin_rec(v0, Pls, bin_minus(w),
+ %v x r. cond(x, bin_add(NCons(r,0),w), NCons(r,0)))"
+end
+
+
+ML
+
+(** Concrete syntax for integers **)
+
+local
+ open Syntax;
+
+ (* Bits *)
+
+ fun mk_bit 0 = const "0"
+ | mk_bit 1 = const "succ" $ const "0"
+ | mk_bit _ = sys_error "mk_bit";
+
+ fun dest_bit (Const ("0", _)) = 0
+ | dest_bit (Const ("succ", _) $ Const ("0", _)) = 1
+ | dest_bit _ = raise Match;
+
+
+ (* Bit strings *) (*we try to handle superfluous leading digits nicely*)
+
+ fun prefix_len _ [] = 0
+ | prefix_len pred (x :: xs) =
+ if pred x then 1 + prefix_len pred xs else 0;
+
+ fun mk_bin str =
+ let
+ val (sign, digs) =
+ (case Symbol.explode str of
+ "#" :: "-" :: cs => (~1, cs)
+ | "#" :: cs => (1, cs)
+ | _ => raise ERROR);
+
+ val zs = prefix_len (equal "0") digs;
+
+ fun bin_of 0 = []
+ | bin_of ~1 = [~1]
+ | bin_of n = (n mod 2) :: bin_of (n div 2);
+
+ fun term_of [] = const "Pls"
+ | term_of [~1] = const "Min"
+ | term_of (b :: bs) = const "Cons" $ term_of bs $ mk_bit b;
+ in
+ term_of (bin_of (sign * (#1 (read_int digs))))
+ end;
+
+ fun dest_bin tm =
+ let
+ fun bin_of (Const ("Pls", _)) = []
+ | bin_of (Const ("Min", _)) = [~1]
+ | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of _ = raise Match;
+
+ fun int_of [] = 0
+ | int_of (b :: bs) = b + 2 * int_of bs;
+
+ val rev_digs = bin_of tm;
+ val (sign, zs) =
+ (case rev rev_digs of
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
+ | bs => ("", prefix_len (equal 0) bs));
+ val num = string_of_int (abs (int_of rev_digs));
+ in
+ "#" ^ sign ^ implode (replicate zs "0") ^ num
+ end;
+
+
+ (* translation of integer constant tokens to and from binary *)
+
+ fun int_tr (*"_Int"*) [t as Free (str, _)] =
+ (const "integ_of" $
+ (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
+ | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
+
+ fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
+ | int_tr' (*"integ_of"*) _ = raise Match;
+in
+ val parse_translation = [("_Int", int_tr)];
+ val print_translation = [("integ_of", int_tr')];
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/EquivClass.ML Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,249 @@
+(* Title: ZF/EquivClass.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Equivalence relations in Zermelo-Fraenkel Set Theory
+*)
+
+val RSLIST = curry (op MRS);
+
+open EquivClass;
+
+(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
+
+(** first half: equiv(A,r) ==> converse(r) O r = r **)
+
+Goalw [trans_def,sym_def]
+ "[| sym(r); trans(r) |] ==> converse(r) O r <= r";
+by (Blast_tac 1);
+qed "sym_trans_comp_subset";
+
+Goalw [refl_def]
+ "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r";
+by (Blast_tac 1);
+qed "refl_comp_subset";
+
+Goalw [equiv_def]
+ "equiv(A,r) ==> converse(r) O r = r";
+by (blast_tac (subset_cs addSIs [sym_trans_comp_subset, refl_comp_subset]) 1);
+qed "equiv_comp_eq";
+
+(*second half*)
+Goalw [equiv_def,refl_def,sym_def,trans_def]
+ "[| converse(r) O r = r; domain(r) = A |] ==> equiv(A,r)";
+by (etac equalityE 1);
+by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
+by (ALLGOALS Fast_tac);
+qed "comp_equivI";
+
+(** Equivalence classes **)
+
+(*Lemma for the next result*)
+Goalw [trans_def,sym_def]
+ "[| sym(r); trans(r); <a,b>: r |] ==> r``{a} <= r``{b}";
+by (Blast_tac 1);
+qed "equiv_class_subset";
+
+Goalw [equiv_def]
+ "[| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}";
+by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
+by (rewtac sym_def);
+by (Blast_tac 1);
+qed "equiv_class_eq";
+
+Goalw [equiv_def,refl_def]
+ "[| equiv(A,r); a: A |] ==> a: r``{a}";
+by (Blast_tac 1);
+qed "equiv_class_self";
+
+(*Lemma for the next result*)
+Goalw [equiv_def,refl_def]
+ "[| equiv(A,r); r``{b} <= r``{a}; b: A |] ==> <a,b>: r";
+by (Blast_tac 1);
+qed "subset_equiv_class";
+
+Goal "[| r``{a} = r``{b}; equiv(A,r); b: A |] ==> <a,b>: r";
+by (REPEAT (ares_tac[equalityD2, subset_equiv_class] 1));
+qed "eq_equiv_class";
+
+(*thus r``{a} = r``{b} as well*)
+Goalw [equiv_def,trans_def,sym_def]
+ "[| equiv(A,r); x: (r``{a} Int r``{b}) |] ==> <a,b>: r";
+by (Blast_tac 1);
+qed "equiv_class_nondisjoint";
+
+Goalw [equiv_def] "equiv(A,r) ==> r <= A*A";
+by (safe_tac subset_cs);
+qed "equiv_type";
+
+Goal "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
+by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
+ addDs [equiv_type]) 1);
+qed "equiv_class_eq_iff";
+
+Goal "[| equiv(A,r); x: A; y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
+by (blast_tac (claset() addIs [eq_equiv_class, equiv_class_eq]
+ addDs [equiv_type]) 1);
+qed "eq_equiv_class_iff";
+
+(*** Quotients ***)
+
+(** Introduction/elimination rules -- needed? **)
+
+Goalw [quotient_def] "x:A ==> r``{x}: A/r";
+by (etac RepFunI 1);
+qed "quotientI";
+
+val major::prems = Goalw [quotient_def]
+ "[| X: A/r; !!x. [| X = r``{x}; x:A |] ==> P |] \
+\ ==> P";
+by (rtac (major RS RepFunE) 1);
+by (eresolve_tac prems 1);
+by (assume_tac 1);
+qed "quotientE";
+
+Goalw [equiv_def,refl_def,quotient_def]
+ "equiv(A,r) ==> Union(A/r) = A";
+by (Blast_tac 1);
+qed "Union_quotient";
+
+Goalw [quotient_def]
+ "[| equiv(A,r); X: A/r; Y: A/r |] ==> X=Y | (X Int Y <= 0)";
+by (safe_tac (claset() addSIs [equiv_class_eq]));
+by (assume_tac 1);
+by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
+by (Blast_tac 1);
+qed "quotient_disj";
+
+(**** Defining unary operations upon equivalence classes ****)
+
+(** These proofs really require as local premises
+ equiv(A,r); congruent(r,b)
+**)
+
+(*Conversion rule*)
+val prems as [equivA,bcong,_] = goal EquivClass.thy
+ "[| equiv(A,r); congruent(r,b); a: A |] ==> (UN x:r``{a}. b(x)) = b(a)";
+by (cut_facts_tac prems 1);
+by (rtac ([refl RS UN_cong, UN_constant] MRS trans) 1);
+by (etac equiv_class_self 2);
+by (assume_tac 2);
+by (rewrite_goals_tac [equiv_def,sym_def,congruent_def]);
+by (Blast_tac 1);
+qed "UN_equiv_class";
+
+(*type checking of UN x:r``{a}. b(x) *)
+val prems = Goalw [quotient_def]
+ "[| equiv(A,r); congruent(r,b); X: A/r; \
+\ !!x. x : A ==> b(x) : B |] \
+\ ==> (UN x:X. b(x)) : B";
+by (cut_facts_tac prems 1);
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps UN_equiv_class::prems) 1);
+qed "UN_equiv_class_type";
+
+(*Sufficient conditions for injectiveness. Could weaken premises!
+ major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
+*)
+val prems = Goalw [quotient_def]
+ "[| equiv(A,r); congruent(r,b); \
+\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
+\ !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] \
+\ ==> X=Y";
+by (cut_facts_tac prems 1);
+by Safe_tac;
+by (rtac equiv_class_eq 1);
+by (REPEAT (ares_tac prems 1));
+by (etac box_equals 1);
+by (REPEAT (ares_tac [UN_equiv_class] 1));
+qed "UN_equiv_class_inject";
+
+
+(**** Defining binary operations upon equivalence classes ****)
+
+
+Goalw [congruent_def,congruent2_def,equiv_def,refl_def]
+ "[| equiv(A,r); congruent2(r,b); a: A |] ==> congruent(r,b(a))";
+by (Blast_tac 1);
+qed "congruent2_implies_congruent";
+
+val equivA::prems = goalw EquivClass.thy [congruent_def]
+ "[| equiv(A,r); congruent2(r,b); a: A |] ==> \
+\ congruent(r, %x1. UN x2:r``{a}. b(x1,x2))";
+by (cut_facts_tac (equivA::prems) 1);
+by Safe_tac;
+by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
+ congruent2_implies_congruent]) 1);
+by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
+by (Blast_tac 1);
+qed "congruent2_implies_congruent_UN";
+
+val prems as equivA::_ = goal EquivClass.thy
+ "[| equiv(A,r); congruent2(r,b); a1: A; a2: A |] \
+\ ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
+by (cut_facts_tac prems 1);
+by (asm_simp_tac (simpset() addsimps [equivA RS UN_equiv_class,
+ congruent2_implies_congruent,
+ congruent2_implies_congruent_UN]) 1);
+qed "UN_equiv_class2";
+
+(*type checking*)
+val prems = Goalw [quotient_def]
+ "[| equiv(A,r); congruent2(r,b); \
+\ X1: A/r; X2: A/r; \
+\ !!x1 x2. [| x1: A; x2: A |] ==> b(x1,x2) : B \
+\ |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
+by (cut_facts_tac prems 1);
+by Safe_tac;
+by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
+ congruent2_implies_congruent_UN,
+ congruent2_implies_congruent, quotientI]) 1));
+qed "UN_equiv_class_type2";
+
+
+(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
+ than the direct proof*)
+val prems = Goalw [congruent2_def,equiv_def,refl_def]
+ "[| equiv(A,r); \
+\ !! y z w. [| w: A; <y,z> : r |] ==> b(y,w) = b(z,w); \
+\ !! y z w. [| w: A; <y,z> : r |] ==> b(w,y) = b(w,z) \
+\ |] ==> congruent2(r,b)";
+by (cut_facts_tac prems 1);
+by Safe_tac;
+by (rtac trans 1);
+by (REPEAT (ares_tac prems 1
+ ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
+qed "congruent2I";
+
+val [equivA,commute,congt] = Goal
+ "[| equiv(A,r); \
+\ !! y z. [| y: A; z: A |] ==> b(y,z) = b(z,y); \
+\ !! y z w. [| w: A; <y,z>: r |] ==> b(w,y) = b(w,z) \
+\ |] ==> congruent2(r,b)";
+by (resolve_tac [equivA RS congruent2I] 1);
+by (rtac (commute RS trans) 1);
+by (rtac (commute RS trans RS sym) 3);
+by (rtac sym 5);
+by (REPEAT (ares_tac [congt] 1
+ ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
+qed "congruent2_commuteI";
+
+(*Obsolete?*)
+val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
+ "[| equiv(A,r); Z: A/r; \
+\ !!w. [| w: A |] ==> congruent(r, %z. b(w,z)); \
+\ !!x y. [| x: A; y: A |] ==> b(y,x) = b(x,y) \
+\ |] ==> congruent(r, %w. UN z: Z. b(w,z))";
+val congt' = rewrite_rule [congruent_def] congt;
+by (cut_facts_tac [ZinA] 1);
+by (rewtac congruent_def);
+by Safe_tac;
+by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
+by (assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [commute,
+ [equivA, congt] MRS UN_equiv_class]) 1);
+by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
+qed "congruent_commuteI";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/EquivClass.thy Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/EquivClass.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Equivalence relations in Zermelo-Fraenkel Set Theory
+*)
+
+EquivClass = Rel + Perm +
+consts
+ "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
+ congruent :: [i,i=>i]=>o
+ congruent2 :: [i,[i,i]=>i]=>o
+
+defs
+ quotient_def "A/r == {r``{x} . x:A}"
+ congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
+
+ congruent2_def
+ "congruent2(r,b) == ALL y1 z1 y2 z2.
+ <y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Integ.ML Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,412 @@
+(* Title: ZF/ex/integ.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"
+$< is a linear ordering
+$+ and $* are monotonic wrt $<
+*)
+
+AddSEs [quotientE];
+
+(*** Proving that intrel is an equivalence relation ***)
+
+(*By luck, requires no typing premises for y1, y2,y3*)
+val eqa::eqb::prems = goal Arith.thy
+ "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2; \
+\ x1: nat; x2: nat; x3: nat |] ==> x1 #+ y3 = x3 #+ y1";
+by (res_inst_tac [("k","x2")] add_left_cancel 1);
+by (resolve_tac prems 2);
+by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
+by (stac eqb 1);
+by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
+by (stac eqa 1);
+by (rtac (add_left_commute) 1 THEN typechk_tac prems);
+qed "integ_trans_lemma";
+
+(** 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 Integ.thy
+ "[| 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];
+
+Goalw [equiv_def, refl_def, sym_def, trans_def]
+ "equiv(nat*nat, intrel)";
+by (fast_tac (claset() addSEs [sym, integ_trans_lemma]) 1);
+qed "equiv_intrel";
+
+
+Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
+ add_0_right, add_succ_right];
+Addcongs [conj_cong];
+
+val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
+
+(** znat: the injection from nat to integ **)
+
+Goalw [integ_def,quotient_def,znat_def]
+ "m : nat ==> $#m : integ";
+by (fast_tac (claset() addSIs [nat_0I]) 1);
+qed "znat_type";
+
+Addsimps [znat_type];
+
+Goalw [znat_def] "[| $#m = $#n; m: nat |] ==> m=n";
+by (dtac (sym RS eq_intrelD) 1);
+by (typechk_tac [nat_0I, SigmaI]);
+by (Asm_full_simp_tac 1);
+qed "znat_inject";
+
+AddSDs [znat_inject];
+
+Goal "m: nat ==> ($# m = $# n) <-> (m = n)";
+by (Blast_tac 1);
+qed "znat_znat_eq";
+Addsimps [znat_znat_eq];
+
+(**** zminus: unary negation on integ ****)
+
+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";
+
+(*Resolve th against the corresponding facts for zminus*)
+val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
+
+Goalw [integ_def,zminus_def] "z : integ ==> $~z : integ";
+by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
+ quotientI]);
+qed "zminus_type";
+
+Goalw [integ_def,zminus_def] "[| $~z = $~w; z: integ; w: integ |] ==> z=w";
+by (etac (zminus_ize UN_equiv_class_inject) 1);
+by Safe_tac;
+(*The setloop is only needed because assumptions are in the wrong order!*)
+by (asm_full_simp_tac (simpset() addsimps add_ac
+ setloop dtac eq_intrelD) 1);
+qed "zminus_inject";
+
+Goalw [zminus_def]
+ "[| x: nat; y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+qed "zminus";
+
+Goalw [integ_def] "z : integ ==> $~ ($~ z) = z";
+by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus]) 1);
+qed "zminus_zminus";
+
+Goalw [integ_def, znat_def] "$~ ($#0) = $#0";
+by (simp_tac (simpset() addsimps [zminus]) 1);
+qed "zminus_0";
+
+Addsimps [zminus_zminus, zminus_0];
+
+
+(**** znegative: the test for negative integers ****)
+
+(*No natural number is negative!*)
+Goalw [znegative_def, znat_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 (fast_tac (claset() addss
+ (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1);
+qed "not_znegative_znat";
+
+Addsimps [not_znegative_znat];
+AddSEs [not_znegative_znat RS notE];
+
+Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
+by (asm_simp_tac (simpset() addsimps [zminus]) 1);
+by (blast_tac (claset() addIs [nat_0_le]) 1);
+qed "znegative_zminus_znat";
+
+Addsimps [znegative_zminus_znat];
+
+Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
+by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
+be natE 1;
+by (dres_inst_tac [("x","0")] spec 2);
+by Auto_tac;
+qed "not_znegative_imp_zero";
+
+(**** zmagnitude: magnitide of an integer, as a natural number ****)
+
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
+by Auto_tac;
+qed "zmagnitude_znat";
+
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
+by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
+qed "zmagnitude_zminus_znat";
+
+Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
+
+Goalw [zmagnitude_def] "zmagnitude(z) : nat";
+br theI2 1;
+by Auto_tac;
+qed "zmagnitude_type";
+
+Goalw [integ_def, znegative_def, znat_def]
+ "[| z: integ; ~ 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);
+br bexI 1;
+br (add_diff_inverse2 RS sym) 1;
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
+qed "not_zneg_znat";
+
+Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z";
+bd not_zneg_znat 1;
+by Auto_tac;
+qed "not_zneg_mag";
+
+Addsimps [not_zneg_mag];
+
+
+Goalw [integ_def, znegative_def, znat_def]
+ "[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))";
+by (auto_tac(claset() addSDs [less_imp_Suc_add],
+ simpset() addsimps [zminus, image_singleton_iff]));
+by (rename_tac "m n j k" 1);
+by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
+by (rotate_tac ~2 2);
+by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
+by (blast_tac (claset() addSDs [add_left_cancel]) 1);
+qed "zneg_znat";
+
+Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z";
+bd zneg_znat 1;
+by Auto_tac;
+qed "zneg_mag";
+
+Addsimps [zneg_mag];
+
+
+(**** zadd: addition on integ ****)
+
+(** 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) 3);
+by (typechk_tac [add_type]);
+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 [integ_def,zadd_def] "[| z: integ; w: integ |] ==> z $+ w : integ";
+by (rtac (zadd_ize UN_equiv_class_type2) 1);
+by (simp_tac (simpset() addsimps [Let_def]) 3);
+by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
+qed "zadd_type";
+
+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 [zadd_ize UN_equiv_class2, SigmaI]) 1);
+by (simp_tac (simpset() addsimps [Let_def]) 1);
+qed "zadd";
+
+Goalw [integ_def,znat_def] "z : integ ==> $#0 $+ z = z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+qed "zadd_0";
+
+Goalw [integ_def] "[| z: integ; w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
+qed "zminus_zadd_distrib";
+
+Goalw [integ_def] "[| z: integ; w: integ |] ==> z $+ w = w $+ z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
+qed "zadd_commute";
+
+Goalw [integ_def]
+ "[| z1: integ; z2: integ; z3: integ |] \
+\ ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+(*rewriting is much faster without intrel_iff, etc.*)
+by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
+qed "zadd_assoc";
+
+(*For AC rewriting*)
+Goal "[| z1:integ; z2:integ; z3: integ |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
+qed "zadd_left_commute";
+
+(*Integer addition is an AC operator*)
+val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
+
+Goalw [znat_def]
+ "[| m: nat; n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
+by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+qed "znat_add";
+
+Goalw [integ_def,znat_def] "z : integ ==> z $+ ($~ z) = $#0";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
+qed "zadd_zminus_inverse";
+
+Goal "z : integ ==> ($~ z) $+ z = $#0";
+by (asm_simp_tac
+ (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
+qed "zadd_zminus_inverse2";
+
+Goal "z:integ ==> z $+ $#0 = z";
+by (rtac (zadd_commute RS trans) 1);
+by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1));
+qed "zadd_0_right";
+
+Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+
+
+(*Need properties of $- ??? Or use $- just as an abbreviation?
+ [| m: nat; n: nat; m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
+*)
+
+(**** zmult: multiplication on integ ****)
+
+(** 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 Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+(*Proof that zmult is congruent in one argument*)
+by (asm_simp_tac
+ (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
+by (asm_simp_tac
+ (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
+(*Proof that zmult is commutative on representatives*)
+by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
+qed "zmult_congruent2";
+
+
+(*Resolve th against the corresponding facts for zmult*)
+val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
+
+Goalw [integ_def,zmult_def] "[| z: integ; w: integ |] ==> z $* w : integ";
+by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
+ split_type, add_type, mult_type,
+ quotientI, SigmaI] 1));
+qed "zmult_type";
+
+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 [zmult_ize UN_equiv_class2, SigmaI]) 1);
+qed "zmult";
+
+Goalw [integ_def,znat_def] "z : integ ==> $#0 $* z = $#0";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult]) 1);
+qed "zmult_0";
+
+Goalw [integ_def,znat_def] "z : integ ==> $#1 $* z = z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
+qed "zmult_1";
+
+Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* w = $~ (z $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
+qed "zmult_zminus";
+
+Addsimps [zmult_0, zmult_1, zmult_zminus];
+
+Goalw [integ_def] "[| z: integ; w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
+qed "zmult_zminus_zminus";
+
+Goalw [integ_def] "[| z: integ; w: integ |] ==> z $* w = w $* z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
+qed "zmult_commute";
+
+Goalw [integ_def]
+ "[| z1: integ; z2: integ; z3: integ |] \
+\ ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac
+ (simpset() addsimps [zmult, add_mult_distrib_left,
+ add_mult_distrib] @ add_ac @ mult_ac) 1);
+qed "zmult_assoc";
+
+(*For AC rewriting*)
+Goal "[| z1:integ; z2:integ; z3: integ |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
+by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
+qed "zmult_left_commute";
+
+(*Integer multiplication is an AC operator*)
+val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
+
+Goalw [integ_def]
+ "[| z1: integ; z2: integ; w: integ |] ==> \
+\ (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
+qed "zadd_zmult_distrib";
+
+val integ_typechecks =
+ [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
+
+Addsimps integ_typechecks;
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Integ.thy Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,60 @@
+(* Title: ZF/ex/integ.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+*)
+
+Integ = EquivClass + Arith +
+consts
+ intrel,integ:: i
+ znat :: i=>i ("$# _" [80] 80)
+ zminus :: i=>i ("$~ _" [80] 80)
+ znegative :: i=>o
+ zmagnitude :: i=>i
+ "$*" :: [i,i]=>i (infixl 70)
+ "$'/" :: [i,i]=>i (infixl 70)
+ "$'/'/" :: [i,i]=>i (infixl 70)
+ "$+" :: [i,i]=>i (infixl 65)
+ "$-" :: [i,i]=>i (infixl 65)
+ "$<" :: [i,i]=>o (infixl 50)
+
+defs
+
+ intrel_def
+ "intrel == {p:(nat*nat)*(nat*nat).
+ EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+
+ integ_def "integ == (nat*nat)/intrel"
+
+ znat_def "$# m == intrel `` {<m,0>}"
+
+ zminus_def "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
+
+ znegative_def
+ "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
+
+ zmagnitude_def
+ "zmagnitude(Z) ==
+ THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
+ (znegative(Z) & $~ Z = $# m))"
+
+ (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
+ Perhaps a "curried" or even polymorphic congruent predicate would be
+ better.*)
+ zadd_def
+ "Z1 $+ Z2 ==
+ UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2
+ in intrel``{<x1#+x2, y1#+y2>}"
+
+ zdiff_def "Z1 $- Z2 == Z1 $+ zminus(Z2)"
+ zless_def "Z1 $< Z2 == znegative(Z1 $- Z2)"
+
+ (*This illustrates the primitive form of definitions (no patterns)*)
+ zmult_def
+ "Z1 $* Z2 ==
+ UN p1:Z1. UN p2:Z2. split(%x1 y1. split(%x2 y2.
+ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+
+ end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/twos_compl.ML Tue Sep 22 13:49:22 1998 +0200
@@ -0,0 +1,128 @@
+(* Title: ZF/ex/twos-compl.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+ML code for Arithmetic on binary integers; the model for theory Bin
+
+ The sign Pls stands for an infinite string of leading 0s.
+ The sign Min stands for an infinite string of leading 1s.
+
+See int_of_binary for the numerical interpretation. A number can have
+multiple representations, namely leading 0s with sign Pls and leading 1s with
+sign Min. A number is in NORMAL FORM if it has no such extra bits.
+
+The representation expects that (m mod 2) is 0 or 1, even if m is negative;
+For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
+
+Still needs division!
+
+print_depth 40;
+System.Control.Print.printDepth := 350;
+*)
+
+infix 5 $$ $$$
+
+(*Recursive datatype of binary integers*)
+datatype bin = Pls | Min | $$ of bin * int;
+
+(** Conversions between bin and int **)
+
+fun int_of_binary Pls = 0
+ | int_of_binary Min = ~1
+ | int_of_binary (w$$b) = 2 * int_of_binary w + b;
+
+fun binary_of_int 0 = Pls
+ | binary_of_int ~1 = Min
+ | binary_of_int n = binary_of_int (n div 2) $$ (n mod 2);
+
+(*** Addition ***)
+
+(*Attach a bit while preserving the normal form. Cases left as default
+ are Pls$$$1 and Min$$$0. *)
+fun Pls $$$ 0 = Pls
+ | Min $$$ 1 = Min
+ | v $$$ x = v$$x;
+
+(*Successor of an integer, assumed to be in normal form.
+ If w$$1 is normal then w is not Min, so bin_succ(w) $$ 0 is normal.
+ But Min$$0 is normal while Min$$1 is not.*)
+fun bin_succ Pls = Pls$$1
+ | bin_succ Min = Pls
+ | bin_succ (w$$1) = bin_succ(w) $$ 0
+ | bin_succ (w$$0) = w $$$ 1;
+
+(*Predecessor of an integer, assumed to be in normal form.
+ If w$$0 is normal then w is not Pls, so bin_pred(w) $$ 1 is normal.
+ But Pls$$1 is normal while Pls$$0 is not.*)
+fun bin_pred Pls = Min
+ | bin_pred Min = Min$$0
+ | bin_pred (w$$1) = w $$$ 0
+ | bin_pred (w$$0) = bin_pred(w) $$ 1;
+
+(*Sum of two binary integers in normal form.
+ Ensure last $$ preserves normal form! *)
+fun bin_add (Pls, w) = w
+ | bin_add (Min, w) = bin_pred w
+ | bin_add (v$$x, Pls) = v$$x
+ | bin_add (v$$x, Min) = bin_pred (v$$x)
+ | bin_add (v$$x, w$$y) =
+ bin_add(v, if x+y=2 then bin_succ w else w) $$$ ((x+y) mod 2);
+
+(*** Subtraction ***)
+
+(*Unary minus*)
+fun bin_minus Pls = Pls
+ | bin_minus Min = Pls$$1
+ | bin_minus (w$$1) = bin_pred (bin_minus(w) $$$ 0)
+ | bin_minus (w$$0) = bin_minus(w) $$ 0;
+
+(*** Multiplication ***)
+
+(*product of two bins; a factor of 0 might cause leading 0s in result*)
+fun bin_mult (Pls, _) = Pls
+ | bin_mult (Min, v) = bin_minus v
+ | bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$$ 0, v)
+ | bin_mult (w$$0, v) = bin_mult(w,v) $$$ 0;
+
+(*** Testing ***)
+
+(*tests addition*)
+fun checksum m n =
+ let val wm = binary_of_int m
+ and wn = binary_of_int n
+ val wsum = bin_add(wm,wn)
+ in if m+n = int_of_binary wsum then (wm, wn, wsum, m+n)
+ else raise Match
+ end;
+
+fun bfact n = if n=0 then Pls$$1
+ else bin_mult(binary_of_int n, bfact(n-1));
+
+(*Examples...
+bfact 5;
+int_of_binary it;
+bfact 69;
+int_of_binary it;
+
+(*For {HOL,ZF}/ex/BinEx.ML*)
+bin_add(binary_of_int 13, binary_of_int 19);
+bin_add(binary_of_int 1234, binary_of_int 5678);
+bin_add(binary_of_int 1359, binary_of_int ~2468);
+bin_add(binary_of_int 93746, binary_of_int ~46375);
+bin_minus(binary_of_int 65745);
+bin_minus(binary_of_int ~54321);
+bin_mult(binary_of_int 13, binary_of_int 19);
+bin_mult(binary_of_int ~84, binary_of_int 51);
+bin_mult(binary_of_int 255, binary_of_int 255);
+bin_mult(binary_of_int 1359, binary_of_int ~2468);
+
+
+(*leading zeros??*)
+bin_add(binary_of_int 1234, binary_of_int ~1234);
+bin_mult(binary_of_int 1234, Pls);
+
+(*leading ones??*)
+bin_add(binary_of_int 1, binary_of_int ~2);
+bin_add(binary_of_int 1234, binary_of_int ~1235);
+*)