Re: [isabelle] Rewriting nat numerals to Suc notation



On 18.03.2015 16:05, Manuel Eberl wrote:
> 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.
Either use a fixed setup for the simplifier or build your own
specialized rewriter using Conv.rewr_conv.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.