# HG changeset patch # User paulson # Date 956066030 -7200 # Node ID f9733879ff25928923591bc514099d0468ad840f # Parent 0bfd6678a5fa6a880ef16bec0e8522cb1bf1281a instantiates new simprocs for numerals of type "nat" diff -r 0bfd6678a5fa -r f9733879ff25 src/HOL/Integ/NatBin.ML --- a/src/HOL/Integ/NatBin.ML Tue Apr 18 15:51:59 2000 +0200 +++ b/src/HOL/Integ/NatBin.ML Tue Apr 18 15:53:50 2000 +0200 @@ -55,13 +55,19 @@ 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 (simpset() addsimps [Suc_nat_number_of]) 1); +by (Simp_tac 1); qed "Suc_numeral_0_eq_1"; Goal "Suc #1 = #2"; -by (simp_tac (simpset() addsimps [Suc_nat_number_of]) 1); +by (Simp_tac 1); qed "Suc_numeral_1_eq_2"; (** Addition **) @@ -256,7 +262,6 @@ Addsimps [le_nat_number_of_eq_not_less]; - (*** New versions of existing theorems involving 0, 1, 2 ***) fun change_theory thy th = @@ -282,7 +287,6 @@ 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'); @@ -300,7 +304,7 @@ (** Arith **) Addsimps (map (rename_numerals thy) - [diff_0_eq_0, add_0, add_0_right, add_pred, + [diff_0, diff_0_eq_0, add_0, add_0_right, add_pred, diff_is_0_eq, zero_is_diff_eq, zero_less_diff, mult_0, mult_0_right, mult_1, mult_1_right, mult_is_0, zero_is_mult, zero_less_mult_iff, @@ -462,6 +466,242 @@ (* Push int(.) inwards: *) Addsimps [int_Suc,zadd_int RS sym]; + +(*** Simprocs for nat numerals ***) + +(*Lemma used for cancel_numerals to prove #n <= i + ... + #m + ... j *) +Goal "!!k::nat. k<=i | k <= j ==> k <= i+j"; +by Auto_tac; +qed "disj_imp_le_add"; + + +structure Nat_Numeral_Simprocs = +struct + +(*Utilities for simproc inverse_fold*) + +fun mk_numeral n = HOLogic.number_of_const $ NumeralSyntax.mk_bin n; + +(*Decodes a numeral to a NATURAL NUMBER*) +fun dest_numeral (Const("Numeral.number_of", _) $ w) = + BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w) + | dest_numeral t = raise TERM("dest_numeral", [t]); + +fun find_first_numeral past (t::terms) = + (dest_numeral t, t, rev past @ terms) + handle _ => find_first_numeral (t::past) terms; + +val zero = mk_numeral 0; +val one = mk_numeral 1; +val mk_plus = HOLogic.mk_binop "op +"; + +fun mk_sum [] = HOLogic.zero + | mk_sum [t] = t + | mk_sum (t :: ts) = if t = zero then mk_sum ts + else mk_plus (t, mk_sum ts); + +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT; + +(*extract the outer Sucs from a term and convert them to a binary numeral*) +fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t) + | dest_Sucs (0, t) = t + | dest_Sucs (k, t) = mk_plus (mk_numeral k, t); + +fun dest_sum (Const ("0", _)) = [] + | dest_sum t = + let val (t,u) = dest_plus t + in dest_sum t @ dest_sum u end + handle _ => [t]; + +fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t)); + +val mk_diff = HOLogic.mk_binop "op -"; +val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT; + +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq; + +fun prove_conv tacs sg (t, u) = + if t aconv u then None + else + Some + (mk_meta_eq (prove_goalw_cterm [] (cterm_of sg (mk_eqv (t, u))) + (K tacs)) + handle ERROR => error + ("The error(s) above occurred while trying to prove " ^ + (string_of_cterm (cterm_of sg (mk_eqv (t, u)))))); + +fun all_simp_tac ss rules = ALLGOALS (simp_tac (ss addsimps rules)); + +val add_norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_ac)); + + +structure InverseFoldData = + struct + val mk_numeral = mk_numeral + val dest_numeral = dest_numeral + val find_first_numeral = find_first_numeral [] + val mk_sum = mk_sum + val dest_sum = dest_Sucs_sum + val mk_diff = HOLogic.mk_binop "op -" + val dest_diff = HOLogic.dest_bin "op -" HOLogic.natT + val double_diff_eq = diff_add_assoc_diff + val move_diff_eq = diff_add_assoc2 + val prove_conv = prove_conv + val numeral_simp_tac = all_simp_tac (simpset()) + val add_norm_tac = ALLGOALS (simp_tac (simpset() addsimps Suc_eq_add_numeral_1::add_ac)) + end; + +structure InverseFold = InverseFoldFun (InverseFoldData); + +structure FoldSuc = FoldSucFun + (open InverseFoldData + val dest_Suc = HOLogic.dest_Suc + val numeral_simp_tac = all_simp_tac (simpset() + addsimps [Suc_nat_number_of_add])); + +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc; +fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT); +val prep_pats = map prep_pat; + +val inverse = + prep_simproc ("inverse_fold", + (map prep_pat ["((i::nat) + j) - number_of v", + "Suc i - number_of v"]), + InverseFold.proc); + +val fold_Suc = + prep_simproc ("fold_Suc", + [prep_pat "Suc (i + j)"], + FoldSuc.proc); + +(*To instantiate "k" in theorems such as eq_diff_iff*) +fun subst_inst_tac th t = + instantiate' [None] [Some (cterm_of (sign_of thy) t)] th; + +fun mk_subst_tac th k = rtac (subst_inst_tac (th RS sym RS trans) k) 1; + +structure CommonData = + struct + val mk_numeral = mk_numeral + val find_first_numeral = find_first_numeral [] + val mk_sum = mk_sum + val dest_sum = dest_Sucs_sum + val prove_conv = prove_conv + val all_simp_tac = all_simp_tac + (simpset() addsimprocs [inverse]) [disj_imp_le_add] + end; + + +(* nat eq *) +structure EqCancelNumerals = CancelNumeralsFun + (open CommonData + val mk_bal = HOLogic.mk_eq + val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT + val subst_tac = mk_subst_tac eq_diff_iff); + +(* nat less *) +structure LessCancelNumerals = CancelNumeralsFun + (open CommonData + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT + val subst_tac = mk_subst_tac less_diff_iff); + +(* nat le *) +structure LeCancelNumerals = CancelNumeralsFun + (open CommonData + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT + val subst_tac = mk_subst_tac le_diff_iff); + +(* nat diff *) +structure DiffCancelNumerals = CancelNumeralsFun + (open CommonData + val mk_bal = HOLogic.mk_binop "op -" + val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT + val subst_tac = mk_subst_tac diff_diff_eq); + +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n"]; +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n"]; +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n"]; + +val diff_pat = prep_pat "(l::nat) - (m + n)"; + (*but ((l::nat) + m) - n" is covered by inverse_fold*) + +val cancel = + map prep_simproc + [("nateq_cancel_numerals", eq_pats, EqCancelNumerals.proc), + ("natless_cancel_numerals", less_pats, LessCancelNumerals.proc), + ("natle_cancel_numerals", le_pats, LeCancelNumerals.proc), + ("natdiff_cancel_numerals", [diff_pat], DiffCancelNumerals.proc)]; + +end; + + +Addsimprocs [Nat_Numeral_Simprocs.inverse, Nat_Numeral_Simprocs.fold_Suc]; +Addsimprocs Nat_Numeral_Simprocs.cancel; + +(*examples: +print_depth 22; +set proof_timing; +fun try s = (Goal s; by (simp_tac (simpset() + addsimprocs Nat_Numeral_Simprocs.cancel @ + [Nat_Numeral_Simprocs.inverse, Nat_Numeral_Simprocs.fold_Suc]) 1)); + +(*inverse*) +try "((i + j) + #12 + (k::nat)) - #15 = y"; +try "((i + j) + #-12 + (k::nat)) - #15 = y"; +try "((i + j) + #12 + (k::nat)) - #-15 = y"; +try "(i + j + #22 + (k::nat)) - #15 = y"; +try "((i + j) + #-12 + (k::nat)) - #-15 = y"; +try "#7 + u - #5 = (yy::nat)"; +try "#2 + u - #5 = (yy::nat)"; + +(*cancel*) +try "((i + j) + #12 + (k::nat)) = u + #15 + y"; +try "((i + j) + #12 + (k::nat)) <= u + #15 + y"; +try "((i + j) + #32 + (k::nat)) - (u + #15 + y) = zz"; +try "((i + j) + #12 + (k::nat)) = u + #5 + y"; +(*negative numerals*) +try "((i + j) + #-23 + (k::nat)) < u + #15 + y"; +try "((i + j) + #3 + (k::nat)) < u + #-15 + y"; + +(*fold_Suc*) +try "Suc (i + j + #3 + k) = u"; +try "Suc (i + j + #-3 + k) = u"; + + +try "Suc u - #2 = y"; +try "Suc (Suc (Suc u)) - #2 = y"; + + +try "((i + j) + #12 + k) = Suc (u + y)"; +try "(i + #2) = Suc u"; +try "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)"; + +try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (u + y)))))"; +(*SLOW because of Addsimps [less_SucI, le_SucI];*) +try "((i + j) + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"; +try "((i + j) + #5 + k) <= Suc (Suc (Suc (Suc (Suc (u + y)))))"; +try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (u + y)))))"; + + +(*so why is this fast?*) +try "((i + j) + #41 + k) < (#5::nat) + (u + y)"; + + +try "((i + j) + #1 + k) = Suc (Suc (u + y))"; + + +try "((i + j) + #1 + k) - #1 = (yy::nat)"; +try "Suc (Suc (u + y)) - #1 = (yy::nat)"; + +try "((i + j) + #41 + k) - #5 = 0"; +try "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = 0"; + +try "((i + j) + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"; +*) + + (*** Prepare linear arithmetic for nat numerals ***) let @@ -482,3 +722,43 @@ LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules addsimprocs simprocs end; + + + +(** For simplifying Suc m - #n **) + +Goal "#0 < n ==> Suc m - n = m - (n - #1)"; +by (asm_full_simp_tac (numeral_ss addsplits [nat_diff_split']) 1); +qed "Suc_diff_eq_diff_pred"; + +(*Now just instantiating n to (number_of v) does the right simplification, + but with some redundant inequality tests.*) + +Goal "neg (number_of (bin_pred v)) = (number_of v = 0)"; +by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1); +by (Asm_simp_tac 1); +by (stac less_number_of_Suc 1); +by (Simp_tac 1); +qed "neg_number_of_bin_pred_iff_0"; + +Goal "neg (number_of (bin_minus v)) ==> \ +\ Suc m - (number_of v) = m - (number_of (bin_pred v))"; +by (stac Suc_diff_eq_diff_pred 1); +by (Simp_tac 1); +by (Simp_tac 1); +by (asm_full_simp_tac + (simpset_of Int.thy addsimps [less_0_number_of RS sym, + neg_number_of_bin_pred_iff_0]) 1); +qed "Suc_diff_number_of"; + +(* now redundant because of the inverse_fold simproc + Addsimps [Suc_diff_number_of]; *) + + +(** For simplifying #m - Suc n **) + +Goal "m - Suc n = (m - #1) - n"; +by (simp_tac (numeral_ss addsplits [nat_diff_split']) 1); +qed "diff_Suc_eq_diff_pred"; + +Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];