Email Gateway (Aug 19 2022 at 17:24): Email Gateway (Aug 19 2022 at 17:24):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I am currently working on a tactic that, at one point, needs to convert
nat numerals (like "3") to the corresponding Suc notation (like "Suc
(Suc (Suc 0))").
My current approach is a conversion using Goal.prove and the simplifier:
fun eval_nat_numeral_conv t =
let val ctxt = @{context}
val i = case HOLogic.dest_number t of
(Type ("Nat.nat", []), i) => i
| _ => raise TERM ("eval_nat_numeral_conv", [t])
val t' = HOLogic.mk_nat i
val prop = (t,t') |> HOLogic.mk_eq |> HOLogic.mk_Trueprop
val conv = CONVERSION (Simplifier.full_rewrite ctxt)
in Goal.prove ctxt [] [] prop
(K (ALLGOALS (conv THEN' rtac @{thm TrueI})))
end;
Seeing as the goals have a very fixed form, (i.e. "3 = Suc (Suc (Suc
0))"), I think this could work. Still, I wonder whether there is a
better way to do this.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 17:24):From: Lars Hupel <hupel@in.tum.de>
Try unfolding with these the theorems 'eval_nat_numeral' and
'BitM.simps'. Example:
schematic_lemma "(5 :: nat) = ?x"
unfolding eval_nat_numeral BitM.simps
For simple unfolding, you can use 'Local_Defs.unfold_tac'.
Cheers
Lars
Email Gateway (Aug 19 2022 at 17:24):From: Lars Noschinski <noschinl@in.tum.de>
Either use a fixed setup for the simplifier or build your own
specialized rewriter using Conv.rewr_conv.
Email Gateway (Aug 19 2022 at 17:25):From: Makarius <makarius@sketis.net>
On Wed, 18 Mar 2015, Manuel Eberl wrote:
My current approach is a conversion using Goal.prove and the simplifier:
Just a few notes on proper use of Isabelle/ML:
fun eval_nat_numeral_conv t =
let val ctxt = @{context}
Use of the the compile-time @{context} is strange. You need to pass a
proper run-time context to whatever tool you write, using what the system
hands you over as a context elsewhere.
val i = case HOLogic.dest_number t of
(Type ("Nat.nat", []), i) => i
Formal names should never be hardwired as ML string constants. Use
@{type_name nat} above, or better @{typ nat} for the whole type
expression.
Makarius
Email Gateway (Aug 19 2022 at 17:27):From: Manuel Eberl <eberlm@in.tum.de>
Thanks for the feedback.
Email Gateway (Aug 19 2022 at 17:27):From: Larry Paulson <lp15@cam.ac.uk>
You may be able to write a simplification procedure for this purpose, taking as a starting point one of the ones in directory ~~/src/Provers/Arith/, which aim to cancel common terms or factors in formulas. But they are very tricky to code, test and debug.
Larry Paulson
Email Gateway (Aug 19 2022 at 17:27):From: Makarius <makarius@sketis.net>
It is a strict rule -- otherwise things won't work. Tools need to be run
in the run-time context.
Just as a matter of survival, it is important to develop a habit to do
things the canonical way, by looking closely how existing (good) tools do
it.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC