--- 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];