Linear arithmetic now copes with mixed nat/int formulae.
--- a/src/HOL/Integ/IntArith.thy Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Integ/IntArith.thy Fri Dec 01 19:53:29 2000 +0100
@@ -1,4 +1,3 @@
-
theory IntArith = Bin
files ("int_arith1.ML") ("int_arith2.ML"):
--- a/src/HOL/Integ/NatBin.ML Fri Dec 01 19:44:48 2000 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,538 +0,0 @@
-(* Title: HOL/NatBin.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1999 University of Cambridge
-
-Binary arithmetic for the natural numbers
-*)
-
-(** 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];
-
-(*These rewrites should one day be re-oriented...*)
-
-Goal "#0 = (0::nat)";
-by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
-qed "numeral_0_eq_0";
-
-Goal "#1 = (1::nat)";
-by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
-qed "numeral_1_eq_1";
-
-Goal "#2 = (2::nat)";
-by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
-qed "numeral_2_eq_2";
-
-bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
-
-(** 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
- (simpset_of Int.thy 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]) 1);
-qed "Suc_nat_eq_nat_zadd1";
-
-Goal "Suc (number_of v) = \
-\ (if neg (number_of v) then #1 else number_of (bin_succ v))";
-by (simp_tac
- (simpset_of Int.thy 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";
-Addsimps [Suc_nat_number_of];
-
-Goal "Suc (number_of v + n) = \
-\ (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
-by (Simp_tac 1);
-qed "Suc_nat_number_of_add";
-
-Goal "Suc #0 = #1";
-by (Simp_tac 1);
-qed "Suc_numeral_0_eq_1";
-
-Goal "Suc #1 = #2";
-by (Simp_tac 1);
-qed "Suc_numeral_1_eq_2";
-
-(** Addition **)
-
-Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
-qed "nat_add_distrib";
-
-(*"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
- (simpset_of Int.thy 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 "[| (#0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
-qed "nat_diff_distrib";
-
-
-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
- (simpset_of Int.thy 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 "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
-by (case_tac "#0 <= z'" 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
- int_0_le_mult_iff]) 1);
-qed "nat_mult_distrib";
-
-Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')";
-by (rtac trans 1);
-by (rtac nat_mult_distrib 2);
-by Auto_tac;
-qed "nat_mult_distrib_neg";
-
-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
- (simpset_of Int.thy 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 "(#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 (zdiv_undefined_case_tac "z' = #0" 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);
-by (rtac (mod_div_equality RS sym RS trans) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
-qed "nat_div_distrib";
-
-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
- (simpset_of Int.thy 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 **)
-
-(*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 (zdiv_undefined_case_tac "z' = #0" 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);
-by (rtac (mod_div_equality RS sym RS trans) 1);
-by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
-qed "nat_mod_distrib";
-
-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
- (simpset_of Int.thy 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];
-
-
-(*** 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
- (simpset_of Int.thy 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 (simpset_of Int.thy 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
- (simpset_of Int.thy 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 (simpset_of Int.thy addsimps [neg_eq_less_int0, 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];
-
-(*** New versions of existing theorems involving 0, 1, 2 ***)
-
-(*Maps n to #n for n = 0, 1, 2*)
-val numeral_sym_ss =
- HOL_ss addsimps [numeral_0_eq_0 RS sym,
- numeral_1_eq_1 RS sym,
- numeral_2_eq_2 RS sym,
- Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
-
-fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
-
-(*Maps #n to n for n = 0, 1, 2*)
-val numeral_ss =
- simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
-
-(** 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');
-
-(** NatDef & Nat **)
-
-Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
-
-AddIffs (map rename_numerals
- [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one,
- le0, le_0_eq,
- neq0_conv, zero_neq_conv, not_gr0]);
-
-(** Arith **)
-
-(*Identity laws for + - * *)
-val basic_renamed_arith_simps =
- map rename_numerals
- [diff_0, diff_0_eq_0, add_0, add_0_right,
- mult_0, mult_0_right, mult_1, mult_1_right];
-
-(*Non-trivial simplifications*)
-val other_renamed_arith_simps =
- map rename_numerals
- [diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
- mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
-
-Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
-
-AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
-
-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'];
-
-(*various theorems that aren't in the default simpset*)
-bind_thm ("add_is_one'", rename_numerals add_is_1);
-bind_thm ("one_is_add'", rename_numerals one_is_add);
-bind_thm ("zero_induct'", rename_numerals zero_induct);
-bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
-bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
-bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
-bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
-
-(** Divides **)
-
-Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
-AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
-
-(*useful?*)
-bind_thm ("mod_self'", rename_numerals mod_self);
-bind_thm ("div_self'", rename_numerals div_self);
-bind_thm ("div_less'", rename_numerals div_less);
-bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
-
-(** Power **)
-
-Goal "(p::nat) ^ #0 = #1";
-by (simp_tac numeral_ss 1);
-qed "power_zero";
-
-Goal "(p::nat) ^ #1 = p";
-by (simp_tac numeral_ss 1);
-qed "power_one";
-Addsimps [power_zero, power_one];
-
-Goal "(p::nat) ^ #2 = p*p";
-by (simp_tac numeral_ss 1);
-qed "power_two";
-
-Goal "#0 < (i::nat) ==> #0 < i^n";
-by (asm_simp_tac numeral_ss 1);
-qed "zero_less_power'";
-Addsimps [zero_less_power'];
-
-bind_thm ("binomial_zero", rename_numerals binomial_0);
-bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
-bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
-
-(*binomial_0_Suc doesn't work well on numerals*)
-Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
-
-Addsimps [rename_numerals card_Pow];
-
-(*** 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]) 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]) 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
- (simpset_of Int.thy 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
- (simpset_of Int.thy 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
- (simpset_of Int.thy 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 [int_Suc,zadd_int RS sym];
-
-Goal "(m+m = n+n) = (m = (n::int))";
-by Auto_tac;
-val lemma1 = result();
-
-Goal "m+m ~= int 1 + 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 (simpset_of Int.thy addsimps
- [number_of_BIT, lemma1, lemma2, eq_commute]) 1);
-qed "eq_number_of_BIT_BIT";
-
-Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
-\ (x=False & (((number_of v) ::int) = number_of Pls))";
-by (simp_tac (simpset_of Int.thy 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 Min) = \
-\ (x=True & (((number_of v) ::int) = number_of Min))";
-by (simp_tac (simpset_of Int.thy 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 Pls ::int) ~= number_of Min";
-by Auto_tac;
-qed "eq_number_of_Pls_Min";
-
-
-(*** Further lemmas about "nat" ***)
-
-Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
-by (case_tac "z=#0 | w=#0" 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym,
- nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
-by (arith_tac 1);
-qed "nat_abs_mult_distrib";
--- a/src/HOL/Integ/NatBin.thy Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Integ/NatBin.thy Fri Dec 01 19:53:29 2000 +0100
@@ -8,14 +8,16 @@
This case is simply reduced to that for the non-negative integers
*)
-NatBin = IntPower +
+theory NatBin = IntPower
+files ("nat_bin.ML"):
-instance
- nat :: number
+instance nat :: number ..
defs
- nat_number_of_def
+ nat_number_of_def:
"number_of v == nat (number_of v)"
(*::bin=>nat ::bin=>int*)
+use "nat_bin.ML" setup nat_bin_arith_setup
+
end
--- a/src/HOL/Integ/int_arith1.ML Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Integ/int_arith1.ML Fri Dec 01 19:53:29 2000 +0100
@@ -392,12 +392,13 @@
(* reduce contradictory <= to False *)
val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
- [int_0, zadd_0, zadd_0_right, zdiff_def,
+ [zadd_0, zadd_0_right, zdiff_def,
zadd_zminus_inverse, zadd_zminus_inverse2,
zmult_0, zmult_0_right,
zmult_1, zmult_1_right,
zmult_minus1, zmult_minus1_right,
- zminus_zadd_distrib, zminus_zminus];
+ zminus_zadd_distrib, zminus_zminus,
+ int_0, zadd_int RS sym, int_Suc];
val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
Int_Numeral_Simprocs.cancel_numerals;
@@ -415,12 +416,14 @@
in
val int_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
{add_mono_thms = add_mono_thms @ add_mono_thms_int,
+ inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
lessD = lessD @ [add1_zle_eq RS iffD2],
simpset = simpset addsimps add_rules
addsimprocs simprocs
addcongs [if_weak_cong]}),
+ arith_inj_const ("IntDef.int", HOLogic.natT --> Type("IntDef.int",[])),
arith_discrete ("IntDef.int", true)];
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/nat_bin.ML Fri Dec 01 19:53:29 2000 +0100
@@ -0,0 +1,548 @@
+(* 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";
+
+(** 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];
+
+(*These rewrites should one day be re-oriented...*)
+
+Goal "#0 = (0::nat)";
+by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
+qed "numeral_0_eq_0";
+
+Goal "#1 = (1::nat)";
+by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
+qed "numeral_1_eq_1";
+
+Goal "#2 = (2::nat)";
+by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
+qed "numeral_2_eq_2";
+
+bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
+
+(** 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
+ (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def,
+ not_neg_nat, int_0]) 1);
+qed "int_nat_number_of";
+Addsimps [int_nat_number_of];
+
+
+val nat_bin_arith_setup =
+ [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
+ {add_mono_thms = add_mono_thms,
+ inj_thms = inj_thms,
+ lessD = lessD,
+ simpset = simpset addsimps [int_nat_number_of,
+ not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})];
+
+(** Successor **)
+
+Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
+by (rtac sym 1);
+by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
+qed "Suc_nat_eq_nat_zadd1";
+
+Goal "Suc (number_of v) = \
+\ (if neg (number_of v) then #1 else number_of (bin_succ v))";
+by (simp_tac
+ (simpset_of Int.thy 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";
+Addsimps [Suc_nat_number_of];
+
+Goal "Suc (number_of v + n) = \
+\ (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
+by (Simp_tac 1);
+qed "Suc_nat_number_of_add";
+
+Goal "Suc #0 = #1";
+by (Simp_tac 1);
+qed "Suc_numeral_0_eq_1";
+
+Goal "Suc #1 = #2";
+by (Simp_tac 1);
+qed "Suc_numeral_1_eq_2";
+
+(** Addition **)
+
+Goal "[| (#0::int) <= z; #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
+qed "nat_add_distrib";
+
+(*"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
+ (simpset_of Int.thy 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 "[| (#0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
+qed "nat_diff_distrib";
+
+
+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
+ (simpset_of Int.thy 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 "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
+by (case_tac "#0 <= z'" 1);
+by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
+by (rtac (inj_int RS injD) 1);
+by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
+ int_0_le_mult_iff]) 1);
+qed "nat_mult_distrib";
+
+Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')";
+by (rtac trans 1);
+by (rtac nat_mult_distrib 2);
+by Auto_tac;
+qed "nat_mult_distrib_neg";
+
+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
+ (simpset_of Int.thy 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 "(#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 (zdiv_undefined_case_tac "z' = #0" 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);
+by (rtac (mod_div_equality RS sym RS trans) 1);
+by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
+qed "nat_div_distrib";
+
+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
+ (simpset_of Int.thy 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 **)
+
+(*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 (zdiv_undefined_case_tac "z' = #0" 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);
+by (rtac (mod_div_equality RS sym RS trans) 1);
+by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
+qed "nat_mod_distrib";
+
+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
+ (simpset_of Int.thy 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];
+
+
+(*** 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
+ (simpset_of Int.thy 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 (simpset_of Int.thy 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
+ (simpset_of Int.thy 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 (simpset_of Int.thy addsimps [neg_eq_less_int0, 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];
+
+(*** New versions of existing theorems involving 0, 1, 2 ***)
+
+(*Maps n to #n for n = 0, 1, 2*)
+val numeral_sym_ss =
+ HOL_ss addsimps [numeral_0_eq_0 RS sym,
+ numeral_1_eq_1 RS sym,
+ numeral_2_eq_2 RS sym,
+ Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
+
+fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
+
+(*Maps #n to n for n = 0, 1, 2*)
+val numeral_ss =
+ simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
+
+(** 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');
+
+(** NatDef & Nat **)
+
+Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
+
+AddIffs (map rename_numerals
+ [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one,
+ le0, le_0_eq,
+ neq0_conv, zero_neq_conv, not_gr0]);
+
+(** Arith **)
+
+(*Identity laws for + - * *)
+val basic_renamed_arith_simps =
+ map rename_numerals
+ [diff_0, diff_0_eq_0, add_0, add_0_right,
+ mult_0, mult_0_right, mult_1, mult_1_right];
+
+(*Non-trivial simplifications*)
+val other_renamed_arith_simps =
+ map rename_numerals
+ [diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
+ mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
+
+Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
+
+AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
+
+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'];
+
+(*various theorems that aren't in the default simpset*)
+bind_thm ("add_is_one'", rename_numerals add_is_1);
+bind_thm ("one_is_add'", rename_numerals one_is_add);
+bind_thm ("zero_induct'", rename_numerals zero_induct);
+bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
+bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
+bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
+bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
+
+(** Divides **)
+
+Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
+AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
+
+(*useful?*)
+bind_thm ("mod_self'", rename_numerals mod_self);
+bind_thm ("div_self'", rename_numerals div_self);
+bind_thm ("div_less'", rename_numerals div_less);
+bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
+
+(** Power **)
+
+Goal "(p::nat) ^ #0 = #1";
+by (simp_tac numeral_ss 1);
+qed "power_zero";
+
+Goal "(p::nat) ^ #1 = p";
+by (simp_tac numeral_ss 1);
+qed "power_one";
+Addsimps [power_zero, power_one];
+
+Goal "(p::nat) ^ #2 = p*p";
+by (simp_tac numeral_ss 1);
+qed "power_two";
+
+Goal "#0 < (i::nat) ==> #0 < i^n";
+by (asm_simp_tac numeral_ss 1);
+qed "zero_less_power'";
+Addsimps [zero_less_power'];
+
+bind_thm ("binomial_zero", rename_numerals binomial_0);
+bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
+bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
+
+(*binomial_0_Suc doesn't work well on numerals*)
+Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
+
+Addsimps [rename_numerals card_Pow];
+
+(*** 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]) 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]) 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
+ (simpset_of Int.thy 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
+ (simpset_of Int.thy 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
+ (simpset_of Int.thy 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 [int_Suc,zadd_int RS sym];
+
+Goal "(m+m = n+n) = (m = (n::int))";
+by Auto_tac;
+val lemma1 = result();
+
+Goal "m+m ~= int 1 + 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 (simpset_of Int.thy addsimps
+ [number_of_BIT, lemma1, lemma2, eq_commute]) 1);
+qed "eq_number_of_BIT_BIT";
+
+Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
+\ (x=False & (((number_of v) ::int) = number_of Pls))";
+by (simp_tac (simpset_of Int.thy 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 Min) = \
+\ (x=True & (((number_of v) ::int) = number_of Min))";
+by (simp_tac (simpset_of Int.thy 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 Pls ::int) ~= number_of Min";
+by Auto_tac;
+qed "eq_number_of_Pls_Min";
+
+
+(*** Further lemmas about "nat" ***)
+
+Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
+by (case_tac "z=#0 | w=#0" 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym,
+ nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
+by (arith_tac 1);
+qed "nat_abs_mult_distrib";
--- a/src/HOL/Integ/nat_simprocs.ML Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Fri Dec 01 19:53:29 2000 +0100
@@ -466,8 +466,8 @@
in
val nat_simprocs_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
- {add_mono_thms = add_mono_thms, lessD = lessD,
+ [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
+ {add_mono_thms = add_mono_thms, inj_thms = inj_thms, lessD = lessD,
simpset = simpset addsimps add_rules
addsimps basic_renamed_arith_simps
addsimprocs simprocs})];
--- a/src/HOL/IsaMakefile Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/IsaMakefile Fri Dec 01 19:53:29 2000 +0100
@@ -78,7 +78,7 @@
Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
Integ/IntDiv.ML Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \
- Integ/NatBin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
+ Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Inverse_Image.ML Inverse_Image.thy Lfp.ML \
--- a/src/HOL/Real/RealArith.ML Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Real/RealArith.ML Fri Dec 01 19:53:29 2000 +0100
@@ -1,4 +1,3 @@
-
(*useful??*)
Goal "(z = z + w) = (w = (#0::real))";
by Auto_tac;
--- a/src/HOL/Real/RealArith.thy Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Real/RealArith.thy Fri Dec 01 19:53:29 2000 +0100
@@ -1,4 +1,3 @@
-
theory RealArith = RealBin
files "real_arith.ML":
--- a/src/HOL/Real/real_arith.ML Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/Real/real_arith.ML Fri Dec 01 19:53:29 2000 +0100
@@ -53,8 +53,9 @@
"fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
val real_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
{add_mono_thms = add_mono_thms @ add_mono_thms_real,
+ inj_thms = inj_thms, (*FIXME: add real*)
lessD = lessD, (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
simpset = simpset addsimps simps@add_rules
addsimprocs simprocs
--- a/src/HOL/arith_data.ML Fri Dec 01 19:44:48 2000 +0100
+++ b/src/HOL/arith_data.ML Fri Dec 01 19:53:29 2000 +0100
@@ -265,24 +265,29 @@
structure ArithTheoryDataArgs =
struct
val name = "HOL/arith";
- type T = {splits: thm list, discrete: (string * bool) list};
+ type T = {splits: thm list, inj_consts: (string * typ)list, discrete: (string * bool) list};
- val empty = {splits = [], discrete = []};
+ val empty = {splits = [], inj_consts = [], discrete = []};
val copy = I;
val prep_ext = I;
- fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) =
+ fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
+ {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
{splits = Drule.merge_rules (splits1, splits2),
+ inj_consts = merge_lists inj_consts1 inj_consts2,
discrete = merge_alists discrete1 discrete2};
fun print _ _ = ();
end;
structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
-fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits, discrete} =>
- {splits = thm :: splits, discrete = discrete}) thy, thm);
+fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
+ {splits= thm::splits, inj_consts= inj_consts, discrete= discrete}) thy, thm);
-fun arith_discrete d = ArithTheoryData.map (fn {splits, discrete} =>
- {splits = splits, discrete = d :: discrete});
+fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
+ {splits = splits, inj_consts = inj_consts, discrete = d :: discrete});
+
+fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
+ {splits = splits, inj_consts = c :: inj_consts, discrete = discrete});
structure LA_Data_Ref: LIN_ARITH_DATA =
@@ -296,6 +301,9 @@
fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
| Some n => (overwrite(p,(t,n+m:int)), i));
+fun decomp2 inj_consts (rel,lhs,rhs) =
+
+let
(* Turn term into list of summand * multiplicity plus a constant *)
fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
| poly(all as Const("op -",T) $ s $ t, m, pi) =
@@ -313,10 +321,11 @@
| poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
((p,i + m*HOLogic.dest_binum t)
handle TERM _ => add_atom(all,m,(p,i)))
+ | poly(all as Const f $ x, m, pi) =
+ if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
| poly x = add_atom x;
-fun decomp2(rel,lhs,rhs) =
- let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
+ val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
in case rel of
"op <" => Some(p,i,"<",q,j)
| "op <=" => Some(p,i,"<=",q,j)
@@ -327,22 +336,24 @@
fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
| negate None = None;
-fun decomp1 discrete (T,xxx) =
+fun decomp1 (discrete,inj_consts) (T,xxx) =
(case T of
Type("fun",[Type(D,[]),_]) =>
(case assoc(discrete,D) of
None => None
- | Some d => (case decomp2 xxx of
+ | Some d => (case decomp2 inj_consts xxx of
None => None
| Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
| _ => None);
-fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
- | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
- negate(decomp1 discrete (T,(rel,lhs,rhs)))
- | decomp2 discrete _ = None
+fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
+ | decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
+ negate(decomp1 data (T,(rel,lhs,rhs)))
+ | decomp2 data _ = None
-val decomp = decomp2 o #discrete o ArithTheoryData.get_sg;
+fun decomp sg =
+ let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
+ in decomp2 (discrete,inj_consts) end
end;
@@ -373,8 +384,9 @@
val init_lin_arith_data =
Fast_Arith.setup @
- [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset = _} =>
{add_mono_thms = add_mono_thms @ add_mono_thms_nat,
+ inj_thms = inj_thms,
lessD = lessD @ [Suc_leI],
simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
ArithTheoryData.init, arith_discrete ("nat", true)];
@@ -416,7 +428,7 @@
in
-val arith_tac = atomize_tac THEN' raw_arith_tac;
+val arith_tac = fast_arith_tac ORELSE' (atomize_tac THEN' raw_arith_tac);
fun arith_method prems =
Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));