# HG changeset patch # User nipkow # Date 975696809 -3600 # Node ID 8f98f0301d6781cfbe642e9eb0686811575578ad # Parent 1751ab88128938f2011b2aeded44ac2d5051fd09 Linear arithmetic now copes with mixed nat/int formulae. diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/IntArith.thy --- 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"): diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/NatBin.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 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"; diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/NatBin.thy --- 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 diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/int_arith1.ML --- 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; diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/nat_bin.ML --- /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 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"; diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Integ/nat_simprocs.ML --- 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})]; diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/IsaMakefile --- 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 \ diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Real/RealArith.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; diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Real/RealArith.thy --- 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": diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/Real/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 diff -r 1751ab881289 -r 8f98f0301d67 src/HOL/arith_data.ML --- 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));