[isabelle] Predicate Compiler fails with "No specification for ..."
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Predicate Compiler fails with "No specification for ..."
- From: Florian Märkl <isabelle-users at florianmaerkl.de>
- Date: Fri, 19 Feb 2021 15:03:49 +0100
- Arc-authentication-results: i=1; strato.com; dkim=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; t=1613743430; s=strato-dkim-0002; d=strato.com; h=Date:Message-ID:Subject:From:To:Cc:Date:From:Subject:Sender; bh=UwyZ8/1GWGuYoi2IO5R5D2S/c4fBL0YoZJbufIajOok=; b=H6imfxyykHcuC5T63bzNVCFkzhhRLn98Uyv5H//0R57v+oYPoYtNEEG/WqTb/fr8Vi gBvm90jWxyiVDGIdyknV3a/LC4GsxTEYe06mYQTxT+M/aBvKwE92j/+xN5Z6mKiD5CFb Uxm0LDQIufAdx5U1KGhpf6QWlu6tmGK0jof+Lc8jZC7JBUKUzLF9uRxRf0AzgabTKWaC SmWPzJwErdD34CMlIgL4GZgmQ+vZjSXR5c9fOISHuEAITtee9sL9pFB3kMWKz/uDAylq FLpoiGzmuX0VP8uEdCHHJi9T38+PaMh5BT9A93w5Jz+fF7XPvS8wUldWUwGAWb0arQQe yHxw==
- Arc-seal: i=1; a=rsa-sha256; t=1613743430; cv=none; d=strato.com; s=strato-dkim-0002; b=pISQdzfIWkHesnzswUwLmcklaHkdmCh3CLesYO2p9jJWTtkt4r0u1zQNDbmLshxtz4 5jzf0tbjVYJtZFz8mSmKUVo5qrxpujPuZJ7cywUeTFRZxWOPt+CXHeFolGWCD8RSX8N8 byWiWuiuMN9Ln6929OC8+Om5mpORHj+EqvhxXpgrLthbZX8xWFYbVzWv9s2+V/L+VyiN dO1GjneqKP7gxY1fhlm2tMlEGv5T9io1Un/Ou6/oDpQmUQV/w2c0ywOfoPkKEYHztzxz yANyg8WB3eiMsGGcoSNz4YfmQKW0KFZc2XNm1W5OL5yYFkwmGCUUw65Q+s/D0JZRNqEO 1P6w==
- Authentication-results: strato.com; dkim=none
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.6.1
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
--
Florian Märkl
https://metallic.software
This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.