equal
deleted
inserted
replaced
1990 |
1990 |
1991 ML{*fun get_thm_alt ctxt (t, n) = |
1991 ML{*fun get_thm_alt ctxt (t, n) = |
1992 let |
1992 let |
1993 val num = HOLogic.mk_number @{typ "nat"} n |
1993 val num = HOLogic.mk_number @{typ "nat"} n |
1994 val goal = Logic.mk_equals (t, num) |
1994 val goal = Logic.mk_equals (t, num) |
1995 val num_ss = HOL_ss addsimps [@{thm One_nat_def}, @{thm Let_def}] @ |
1995 val num_ss = HOL_ss addsimps @{thms semiring_norm} |
1996 @{thms eval_nat_numeral} @ @{thms neg_simps} @ @{thms plus_nat.simps} |
|
1997 in |
1996 in |
1998 Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1)) |
1997 Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1)) |
1999 end*} |
1998 end*} |
2000 |
1999 |
2001 text {* |
2000 text {* |
2015 |
2014 |
2016 ML{*fun nat_number_simproc ss t = |
2015 ML{*fun nat_number_simproc ss t = |
2017 let |
2016 let |
2018 val ctxt = Simplifier.the_context ss |
2017 val ctxt = Simplifier.the_context ss |
2019 in |
2018 in |
2020 SOME (get_thm ctxt (t, dest_suc_trm t)) |
2019 SOME (get_thm_alt ctxt (t, dest_suc_trm t)) |
2021 handle TERM _ => NONE |
2020 handle TERM _ => NONE |
2022 end*} |
2021 end*} |
2023 |
2022 |
2024 text {* |
2023 text {* |
2025 This function uses the fact that @{ML dest_suc_trm} might raise an exception |
2024 This function uses the fact that @{ML dest_suc_trm} might raise an exception |