*To*: Andreas Lochbihler <mail at andreas-lochbihler.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Predicate Compiler fails with "No specification for ..."*From*: Florian Märkl <isabelle-users at florianmaerkl.de>*Date*: Sun, 21 Feb 2021 17:34:06 +0100*Arc-authentication-results*: i=1; strato.com; dkim=none*Arc-message-signature*: i=1; a=rsa-sha256; c=relaxed/relaxed; t=1613925247; s=strato-dkim-0002; d=strato.com; h=In-Reply-To:Date:Message-ID:Subject:From:References:To:Cc:Date:From: Subject:Sender; bh=E2m5x3MGaMfTtnvQ8+dqqxrFFf+gjzwaGfWHtbZW1P4=; b=B7yN48Sjs8P2PXAEsKOCI43jSL9ZeNdQCeQMs4PDciXjyzgmK7vll35iRibvs4UCQP ShgK8pMpZoA0GFoP/MZgJO2Fy9r9EUct9a+QkHwAZJjIAlV2edYIy4lF+W/QSj4P+5cz Zh0S82YIE7yA8RLumbFJgn09Rx16neFj/1OkKQuH9q5ChsSACbYhbh7xBOmLx4gV1pnV LvuxXtri4FfG6dX7A8+WyqOhLNonsY5yVaQdD06yFh1ppLNndSjbRdfdK/+RR17BXcjM SuvGJgMV8jOoiwG02zQvlpGzkmUvfraE+18+Vnj9r2nkzZ5Yb/kmbg//Hl47M3Funa1a fw5w==*Arc-seal*: i=1; a=rsa-sha256; t=1613925247; cv=none; d=strato.com; s=strato-dkim-0002; b=PV1/Qz/62uF3KLIXPRF6eMCcgMF4gwqT43FDUx6tMsZ01CHijKqSghnWwok1QFMr3M lWEo3OeQlk8jbdGQhhe+Ysma716GyFCGpZFoRBNM3lDlAWql9Z+oMGQO7zzk0YfXWBhS FFe08TO/bSPr+M2Ize+GBAhQob6owh7IWvqUe8LA/c5JVdVCztTaTfadt17brVZc7jfI MzP0Gsv0uJAIaq7AS53gdI95Ui75VFUJHSLB8YJqJSB/dmFc5HIIXhcgXcC2g8lLwhih 2hhdRwSCybGbQksRXd/9cOA2LFEhHmt3C/oDejxvh+lGybzmp7ClCY+3vmcObG2rXl7z 7kyQ==*Authentication-results*: strato.com; dkim=none*In-reply-to*: <87e5446d-18c0-f4d8-fd6b-c10e6056730c@andreas-lochbihler.de>*References*: <1cfb3f7c-7225-cbe0-3f4d-528903c598ba@florianmaerkl.de> <34ae21a8-c22d-caa9-e9db-f7259c944912@in.tum.de> <0321eb1e-9652-fe13-1004-5b6639d513b7@florianmaerkl.de> <87e5446d-18c0-f4d8-fd6b-c10e6056730c@andreas-lochbihler.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.6.1

Hello Andreas, thank you very much, this does bring me one step forward. Now considering the set example again, this is what I have now: 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)^**" lemma P_intro [code_pred_intro]: "P a b" if "a ∈ set [b]" unfolding P_def using that . code_pred (modes: i ⇒ i ⇒ bool) P using P_def by auto (* Output: Inferred modes: Scratch.t: *) code_pred (* errors: (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool)*) [inductify, show_modes] t . export_code t in SML module_name Scratch (* exception Fail raised (line 26 of "generated code"): Transitive_Closure.rtranclp which is no wonder becuause the code is essentially this: fun rtranclp _ _ _ = raise Fail "Transitive_Closure.rtranclp"; fun t x = rtranclp p x; *) value "t 0 1" end So in the end, with HOL-Library.Transitive_Closure_Table, the rtranclp function ist just a one-liner raising an exception here. What seems fishy to me is that the code_pred for t in this case does not infer any modes at all, but I am not really sure what to make of this. Florian On 2/21/21 9:10 AM, Andreas Lochbihler wrote: > Hi Florian, > > code_pred's [inductify] option has its quirks and doesn't always work; > in particular set comprehensions and set membership are tricky > (code_pred was developed when "'a set" was a type abbreviation for "'a > => bool"). What you can do is to do the inductification manually. In > your example with the typedef, the following makes code_pred generate > the right equations (of course, you should manually fill in the sorrys) > > lemma P_intro [code_pred_intro]: "P n m" > if "Rep_mynat n ≠ 0" "m = Abs_mynat (Rep_mynat n - 1)" sorry > > code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) P sorry > > code_pred (modes: i ⇒ i ⇒ bool, i ⇒ o ⇒ bool) [inductify] t . > > Now, however, export_code gives you a well-sortedness error that mynat > isn't an instance of equal. But that's something you probably want to > provide anyway; I'm actually surprised that the setup_lifting doesn't > generate such an instance. > > Hope this helps, > Andreas > > > On 20.02.21 19:32, Florian Märkl wrote: >> 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 >>>> >>> >> >>

**Follow-Ups**:**Re: [isabelle] Predicate Compiler fails with "No specification for ..."***From:*Andreas Lochbihler

**References**:**[isabelle] Predicate Compiler fails with "No specification for ..."***From:*Florian Märkl

**Re: [isabelle] Predicate Compiler fails with "No specification for ..."***From:*Tobias Nipkow

**Re: [isabelle] Predicate Compiler fails with "No specification for ..."***From:*Florian Märkl

**Re: [isabelle] Predicate Compiler fails with "No specification for ..."***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] First day with HOL/Isabelle
- Next by Date: Re: [isabelle] First day with HOL/Isabelle
- Previous by Thread: Re: [isabelle] Predicate Compiler fails with "No specification for ..."
- Next by Thread: Re: [isabelle] Predicate Compiler fails with "No specification for ..."
- Cl-isabelle-users February 2021 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list