# HG changeset patch # User paulson # Date 956309373 -7200 # Node ID 5a5189330337265f95ee73663d4edf59e6a9048b # Parent 04d01ae28508d42dfb7126d7a5e27271dccaa883 moved the simproc code to NatSimprocs.ML diff -r 04d01ae28508 -r 5a5189330337 src/HOL/Integ/NatBin.ML --- a/src/HOL/Integ/NatBin.ML Fri Apr 21 11:28:34 2000 +0200 +++ b/src/HOL/Integ/NatBin.ML Fri Apr 21 11:29:33 2000 +0200 @@ -466,299 +466,3 @@ (* 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 - -(* reduce contradictory <= to False *) -val add_rules = - [add_nat_number_of, diff_nat_number_of, mult_nat_number_of, - eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less, - le_Suc_number_of,le_number_of_Suc, - less_Suc_number_of,less_number_of_Suc, - Suc_eq_number_of,eq_number_of_Suc, - eq_number_of_0, eq_0_number_of, less_0_number_of, - nat_number_of, Let_number_of, if_True, if_False]; - -val simprocs = [Nat_Plus_Assoc.conv,Nat_Times_Assoc.conv]; - -in -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];