Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Rewriting nat numerals to Suc notation


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Email Gateway (Aug 19 2022 at 17:27):

From: Manuel Eberl <eberlm@in.tum.de>
Thanks for the feedback.

view this post on Zulip 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

view this post on Zulip 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: Mar 29 2024 at 08:18 UTC