--- a/src/HOL/Integ/nat_bin.ML Wed Dec 03 10:49:34 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,500 +0,0 @@
-(* Title: HOL/nat_bin.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Binary arithmetic for the natural numbers
-*)
-
-val nat_number_of_def = thm "nat_number_of_def";
-
-val ss_Int = simpset_of Int_thy;
-
-(** nat (coercion from int to nat) **)
-
-Goal "nat (number_of w) = number_of w";
-by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
-qed "nat_number_of";
-Addsimps [nat_number_of, nat_0, nat_1];
-
-Goal "Numeral0 = (0::nat)";
-by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
-qed "numeral_0_eq_0";
-
-Goal "Numeral1 = (1::nat)";
-by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1);
-qed "numeral_1_eq_1";
-
-Goal "Numeral1 = Suc 0";
-by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1);
-qed "numeral_1_eq_Suc_0";
-
-Goalw [nat_number_of_def] "2 = Suc (Suc 0)";
-by (rtac nat_2 1);
-qed "numeral_2_eq_2";
-
-
-(** Distributive laws for "nat". The others are in IntArith.ML, but these
- require div and mod to be defined for type "int". They also need
- some of the lemmas proved just above.**)
-
-Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
-by (case_tac "0 <= z'" 1);
-by (auto_tac (claset(),
- simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
-by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
- by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
-by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
-by (rename_tac "m m'" 1);
-by (subgoal_tac "0 <= int m div int m'" 1);
- by (asm_full_simp_tac
- (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
-by (rtac (inj_int RS injD) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
- by (Force_tac 2);
-by (asm_full_simp_tac
- (simpset() addsimps [nat_less_iff RS sym, quorem_def,
- numeral_0_eq_0, zadd_int, zmult_int]) 1);
-qed "nat_div_distrib";
-
-(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
-Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
-by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
- by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
-by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
-by (rename_tac "m m'" 1);
-by (subgoal_tac "0 <= int m mod int m'" 1);
- by (asm_full_simp_tac
- (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
-by (rtac (inj_int RS injD) 1);
-by (Asm_simp_tac 1);
-by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
- by (Force_tac 2);
-by (asm_full_simp_tac
- (simpset() addsimps [nat_less_iff RS sym, quorem_def,
- numeral_0_eq_0, zadd_int, zmult_int]) 1);
-qed "nat_mod_distrib";
-
-
-(** int (coercion from nat to int) **)
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "int (number_of v :: nat) = \
-\ (if neg (number_of v) then 0 \
-\ else (number_of v :: int))";
-by (simp_tac
- (ss_Int addsimps [neg_nat, nat_number_of_def, not_neg_nat, int_0]) 1);
-qed "int_nat_number_of";
-Addsimps [int_nat_number_of];
-
-
-(** Successor **)
-
-Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
-by (rtac sym 1);
-by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
-qed "Suc_nat_eq_nat_zadd1";
-
-Goal "Suc (number_of v + n) = \
-\ (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
-by (simp_tac (ss_Int addsimps [neg_nat, nat_1, not_neg_eq_ge_0,
- nat_number_of_def, int_Suc,
- Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
-qed "Suc_nat_number_of_add";
-
-Goal "Suc (number_of v) = \
-\ (if neg (number_of v) then 1 else number_of (bin_succ v))";
-by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);
-by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1);
-qed "Suc_nat_number_of";
-Addsimps [Suc_nat_number_of];
-
-val nat_bin_arith_setup =
- [Fast_Arith.map_data
- (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
- {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
- inj_thms = inj_thms,
- lessD = lessD,
- simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
- not_neg_number_of_Pls,
- neg_number_of_Min,neg_number_of_BIT]})];
-
-(** Addition **)
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "(number_of v :: nat) + number_of v' = \
-\ (if neg (number_of v) then number_of v' \
-\ else if neg (number_of v') then number_of v \
-\ else number_of (bin_add v v'))";
-by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
- nat_add_distrib RS sym, number_of_add]) 1);
-qed "add_nat_number_of";
-
-Addsimps [add_nat_number_of];
-
-
-(** Subtraction **)
-
-Goal "nat z - nat z' = \
-\ (if neg z' then nat z \
-\ else let d = z-z' in \
-\ if neg d then 0 else nat d)";
-by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
- neg_eq_less_0, not_neg_eq_ge_0]) 1);
-by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
-qed "diff_nat_eq_if";
-
-Goalw [nat_number_of_def]
- "(number_of v :: nat) - number_of v' = \
-\ (if neg (number_of v') then number_of v \
-\ else let d = number_of (bin_add v (bin_minus v')) in \
-\ if neg d then 0 else nat d)";
-by (simp_tac (ss_Int delcongs [if_weak_cong]
- addsimps [not_neg_eq_ge_0, nat_0,
- diff_nat_eq_if, diff_number_of_eq]) 1);
-qed "diff_nat_number_of";
-
-Addsimps [diff_nat_number_of];
-
-
-(** Multiplication **)
-
-Goal "(number_of v :: nat) * number_of v' = \
-\ (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
-by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
- nat_mult_distrib RS sym, number_of_mult,
- nat_0]) 1);
-qed "mult_nat_number_of";
-
-Addsimps [mult_nat_number_of];
-
-
-(** Quotient **)
-
-Goal "(number_of v :: nat) div number_of v' = \
-\ (if neg (number_of v) then 0 \
-\ else nat (number_of v div number_of v'))";
-by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat,
- nat_div_distrib RS sym, nat_0]) 1);
-qed "div_nat_number_of";
-
-Addsimps [div_nat_number_of];
-
-
-(** Remainder **)
-
-Goal "(number_of v :: nat) mod number_of v' = \
-\ (if neg (number_of v) then 0 \
-\ else if neg (number_of v') then number_of v \
-\ else nat (number_of v mod number_of v'))";
-by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def,
- neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
- nat_mod_distrib RS sym]) 1);
-qed "mod_nat_number_of";
-
-Addsimps [mod_nat_number_of];
-
-structure NatAbstractNumeralsData =
- struct
- val dest_eq = HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
- val is_numeral = Bin_Simprocs.is_numeral
- val numeral_0_eq_0 = numeral_0_eq_0
- val numeral_1_eq_1 = numeral_1_eq_Suc_0
- val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars
- fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps))
- val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq
- end
-
-structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData)
-
-val nat_eval_numerals =
- map Bin_Simprocs.prep_simproc
- [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
- ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];
-
-Addsimprocs nat_eval_numerals;
-
-
-(*** Comparisons ***)
-
-(** Equals (=) **)
-
-Goal "[| (0::int) <= z; 0 <= z' |] ==> (nat z = nat z') = (z=z')";
-by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
-qed "eq_nat_nat_iff";
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "((number_of v :: nat) = number_of v') = \
-\ (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
-\ else if neg (number_of v') then iszero (number_of v) \
-\ else iszero (number_of (bin_add v (bin_minus v'))))";
-by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
- eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
-by (simp_tac (ss_Int addsimps [nat_eq_iff, nat_eq_iff2, iszero_def]) 1);
-by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
-qed "eq_nat_number_of";
-
-Addsimps [eq_nat_number_of];
-
-(** Less-than (<) **)
-
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "((number_of v :: nat) < number_of v') = \
-\ (if neg (number_of v) then neg (number_of (bin_minus v')) \
-\ else neg (number_of (bin_add v (bin_minus v'))))";
-by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
- nat_less_eq_zless, less_number_of_eq_neg, nat_0]) 1);
-by (simp_tac (ss_Int addsimps [neg_eq_less_0, zminus_zless,
- number_of_minus, zless_nat_eq_int_zless]) 1);
-qed "less_nat_number_of";
-
-Addsimps [less_nat_number_of];
-
-
-(** Less-than-or-equals (<=) **)
-
-Goal "(number_of x <= (number_of y::nat)) = \
-\ (~ number_of y < (number_of x::nat))";
-by (rtac (linorder_not_less RS sym) 1);
-qed "le_nat_number_of_eq_not_less";
-
-Addsimps [le_nat_number_of_eq_not_less];
-
-
-(*Maps #n to n for n = 0, 1, 2*)
-bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
-val numeral_ss = simpset() addsimps numerals;
-
-(** Nat **)
-
-Goal "0 < n ==> n = Suc(n - 1)";
-by (asm_full_simp_tac numeral_ss 1);
-qed "Suc_pred'";
-
-(*Expresses a natural number constant as the Suc of another one.
- NOT suitable for rewriting because n recurs in the condition.*)
-bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
-
-(** Arith **)
-
-Goal "Suc n = n + 1";
-by (asm_simp_tac numeral_ss 1);
-qed "Suc_eq_add_numeral_1";
-
-(* These two can be useful when m = number_of... *)
-
-Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))";
-by (case_tac "m" 1);
-by (ALLGOALS (asm_simp_tac numeral_ss));
-qed "add_eq_if";
-
-Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))";
-by (case_tac "m" 1);
-by (ALLGOALS (asm_simp_tac numeral_ss));
-qed "mult_eq_if";
-
-Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))";
-by (case_tac "m" 1);
-by (ALLGOALS (asm_simp_tac numeral_ss));
-qed "power_eq_if";
-
-Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)";
-by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
-qed "diff_less'";
-
-Addsimps [inst "n" "number_of ?v" diff_less'];
-
-(** Power **)
-
-Goal "(p::nat) ^ 2 = p*p";
-by (simp_tac numeral_ss 1);
-qed "power_two";
-
-
-(*** Comparisons involving (0::nat) ***)
-
-Goal "(number_of v = (0::nat)) = \
-\ (if neg (number_of v) then True else iszero (number_of v))";
-by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
-qed "eq_number_of_0";
-
-Goal "((0::nat) = number_of v) = \
-\ (if neg (number_of v) then True else iszero (number_of v))";
-by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
-qed "eq_0_number_of";
-
-Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
-by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
-qed "less_0_number_of";
-
-(*Simplification already handles n<0, n<=0 and 0<=n.*)
-Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
-
-Goal "neg (number_of v) ==> number_of v = (0::nat)";
-by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
-qed "neg_imp_number_of_eq_0";
-
-
-
-(*** Comparisons involving Suc ***)
-
-Goal "(number_of v = Suc n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then False else nat pv = n)";
-by (simp_tac (ss_Int addsimps
- [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
- nat_number_of_def, zadd_0] @ zadd_ac) 1);
-by (res_inst_tac [("x", "number_of v")] spec 1);
-by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
-qed "eq_number_of_Suc";
-
-Goal "(Suc n = number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then False else nat pv = n)";
-by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
-qed "Suc_eq_number_of";
-
-Goal "(number_of v < Suc n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then True else nat pv < n)";
-by (simp_tac (ss_Int addsimps
- [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
- nat_number_of_def, zadd_0] @ zadd_ac) 1);
-by (res_inst_tac [("x", "number_of v")] spec 1);
-by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
-qed "less_number_of_Suc";
-
-Goal "(Suc n < number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then False else n < nat pv)";
-by (simp_tac (ss_Int addsimps
- [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
- nat_number_of_def, zadd_0] @ zadd_ac) 1);
-by (res_inst_tac [("x", "number_of v")] spec 1);
-by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
-qed "less_Suc_number_of";
-
-Goal "(number_of v <= Suc n) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then True else nat pv <= n)";
-by (simp_tac
- (simpset () addsimps
- [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
-qed "le_number_of_Suc";
-
-Goal "(Suc n <= number_of v) = \
-\ (let pv = number_of (bin_pred v) in \
-\ if neg pv then False else n <= nat pv)";
-by (simp_tac
- (simpset () addsimps
- [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
-qed "le_Suc_number_of";
-
-Addsimps [eq_number_of_Suc, Suc_eq_number_of,
- less_number_of_Suc, less_Suc_number_of,
- le_number_of_Suc, le_Suc_number_of];
-
-(* Push int(.) inwards: *)
-Addsimps [zadd_int RS sym];
-
-Goal "(m+m = n+n) = (m = (n::int))";
-by Auto_tac;
-val lemma1 = result();
-
-Goal "m+m ~= (1::int) + n + n";
-by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
-val lemma2 = result();
-
-Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
-\ (x=y & (((number_of v) ::int) = number_of w))";
-by (simp_tac (ss_Int addsimps [number_of_BIT, lemma1, lemma2, eq_commute]) 1);
-qed "eq_number_of_BIT_BIT";
-
-Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
-\ (x=False & (((number_of v) ::int) = number_of bin.Pls))";
-by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Pls, eq_commute]) 1);
-by (res_inst_tac [("x", "number_of v")] spec 1);
-by Safe_tac;
-by (ALLGOALS Full_simp_tac);
-by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1);
-qed "eq_number_of_BIT_Pls";
-
-Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
-\ (x=True & (((number_of v) ::int) = number_of bin.Min))";
-by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Min, eq_commute]) 1);
-by (res_inst_tac [("x", "number_of v")] spec 1);
-by Auto_tac;
-by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
-by Auto_tac;
-qed "eq_number_of_BIT_Min";
-
-Goal "(number_of bin.Pls ::int) ~= number_of bin.Min";
-by Auto_tac;
-qed "eq_number_of_Pls_Min";
-
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "k" "number_of ?v")
- [add_mult_distrib, add_mult_distrib2,
- diff_mult_distrib, diff_mult_distrib2]);
-
-
-(*** Literal arithmetic involving powers, type nat ***)
-
-Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
-by (induct_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
-qed "nat_power_eq";
-
-Goal "(number_of v :: nat) ^ n = \
-\ (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
-by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def,
- nat_power_eq]) 1);
-qed "power_nat_number_of";
-
-Addsimps [inst "n" "number_of ?w" power_nat_number_of];
-
-
-
-(*** Literal arithmetic involving powers, type int ***)
-
-Goal "(z::int) ^ (2*a) = (z^a)^2";
-by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1);
-qed "zpower_even";
-
-Goal "(p::int) ^ 2 = p*p";
-by (simp_tac numeral_ss 1);
-qed "zpower_two";
-
-Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
-by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1);
-qed "zpower_odd";
-
-Goal "(z::int) ^ number_of (w BIT False) = \
-\ (let w = z ^ (number_of w) in w*w)";
-by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
-by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
-by (case_tac "(0::int) <= x" 1);
-by (auto_tac (claset(),
- simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two]));
-qed "zpower_number_of_even";
-
-Goal "(z::int) ^ number_of (w BIT True) = \
-\ (if (0::int) <= number_of w \
-\ then (let w = z ^ (number_of w) in z*w*w) \
-\ else 1)";
-by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
-by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1);
-by (case_tac "(0::int) <= x" 1);
-by (auto_tac (claset(),
- simpset() addsimps [nat_add_distrib, nat_mult_distrib,
- zpower_even, zpower_two]));
-qed "zpower_number_of_odd";
-
-Addsimps (map (inst "z" "number_of ?v")
- [zpower_number_of_even, zpower_number_of_odd]);
-