Re: [isabelle] Predicate Compiler fails with "No specification for ..."

"No specification for Rep_mynat": I suspect the code generator just cannot handle types specified by "typedef".


On 19/02/2021 15:03, Florian Märkl wrote:

I am trying to replicate something like discussed in
(the part of the JinjaThreads theory), i.e. generating code for a
reflexive transitive closure predicate, however the [inductify] option
that I have to use on code_pred currently seems to give me some headaches.

In essence, what I have in my project is something like this:

theory "Scratch"

   imports "HOL-Library.Transitive_Closure_Table" Main


typedef mynat = "{n :: nat. True}" by auto

setup_lifting type_definition_mynat

definition P :: "mynat ⇒ mynat ⇒ bool" where

   "P a b ≡ Rep_mynat a = Suc (Rep_mynat b)"

definition t where "t = (P)^**"

(* Fails with: "No specification for Rep_mynat" *)

code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify] t .

(* The final goal *)

export_code t in SML


I have some executable predicate P over which I want to execute the
reflexive transitive closure t.

Now from what I understand (please correct me if I am wrong), the
[inductify] option here is necessary so code_pred understands that this
is actually an inductive predicate by digging into the definitions.

But that also means it will go even deeper and try to inspect Rep_mynat
for example, which fails.

What I intuitively would want it to do is to only unfold the t, but then
consider P an opaque constant.

I have seen that code_pred has quite a few more undocumented options,
but didn't find anything yet that did what I need. Is something like
this possible somehow or am I misunderstanding the inner workings of the
predicate compiler here?


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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