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



Hello Tobias,

in my larger project I could probably get rid of the typdefd types in
this specific predicate by just duplicating the code of what is called P
here, operating directly on the underying type of the typedef.

However after doing this, I end up with another issue that can be seen
in this example:


theory "Scratch"
  imports "HOL-Library.Transitive_Closure_Table" Main
begin

definition P :: "nat ⇒ nat ⇒ bool" where "P a b ≡ a ∈ set [b]"
definition t where "t ≡ (P)^**"

(* Fails with:
exception TERM raised (line 80 of
"~~/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML"):
  defining_const_of_introrule failed: Not a constant
  {x. x ∈ ?z} ≡ ?z
*)
code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify, show_steps,
show_intermediate_results] t .

(* The final goal *)
export_code t in SML

end


So it seems there is an issue with the ∈ operator now, which might be
possible to eliminate too (here by operating on the list [b], probably
similar in the real project) but this also brings me back to the
original problem: Is it somehow possible to use code_pred on a
definition like "t ≡ (P)^**" that does not use the "inductive" command
at the top level, without code_pred having to recurse through every
little definition that it contains?

Florian

On 2/20/21 6:07 PM, Tobias Nipkow wrote:
> "No specification for Rep_mynat": I suspect the code generator just
> cannot handle types specified by "typedef".
> 
> Tobias
> 
> On 19/02/2021 15:03, Florian Märkl wrote:
>> Hello,
>>
>>
>>
>> I am trying to replicate something like discussed in
>> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2020-November/msg00013.html
>>
>> (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
>>
>> begin
>>
>>
>>
>> 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
>>
>>
>>
>> end
>>
>>
>>
>>
>>
>> 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?
>>
>>
>>
>> Florian
>>
> 




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