Email Gateway (Aug 19 2022 at 12:16): Email Gateway (Aug 19 2022 at 12:16):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi all,
I was a bit surprised to discover that "code_pred" introduces axioms with strange names in some circumstances. I've checked the behavior with a recent repository version of Isabelle but it has been around for several weeks and should be in Isabelle2013-1-RC1 as well (and probably Isabelle2013).
In "Jinja/Common/TypeRel.thy", there is the following command
code_pred
(modes: i ⇒ i × o ⇒ bool, i ⇒ i × i ⇒ bool)
[inductify]
subcls1
.
Right after it,
ML {* Theory.axioms_of @{theory} |> map fst |> rev |> take 2 *}
will produce somehting like
val it = ["TypeRel.unnamed_axiom_2088252", "TypeRel.unnamed_axiom_2088251"]: string list
where the numbers change on each invocation.
(1) Is it desirable that "code_pred" introduces axioms for something that could (from what I can tell) easily be done using a definition?
(2) If the answer yes, shouldn't it provide some decent names to them rather than unpredictable, ever changing ones?
Jasmin
Email Gateway (Aug 19 2022 at 12:17):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Jasmin,
When Lukas told me about the axioms about three years ago, he said that indeed these
axioms only specify new constants which the inductify option of code_pred introduces for
code generation. He wanted to somewhen implement proper definitions for these constants,
but never found the time. So no, it is not desirable to have axioms instead of
definitions, even in code_pred [inductify].
However a simple definition will not work, one would have to build quite some machinery,
because the definitions can be recursive. The following example illustrates the problem:
theory Scratch
imports Main
begin
definition Id :: "('a => 'a) => 'a => 'a" where "Id f x = f x"
lemma [fundef_cong]: "[| x = y; f y = g y |] ==> Id f x = Id g y"
by(simp add: Id_def)
fun bar :: "nat => nat" where
bar0: "bar 0 = 1"
| bar1: "bar (Suc n) = Id bar n" (* higher-order recursion through Id *)
inductive foo :: "nat => bool"
where "foo 0" | "foo (bar k)"
code_pred [inductify] foo .
The invocation of code_pred introduces two new constants IdP and barP and specified the
following three axioms:
IdP barP p res ==> barP (Suc p) res
barP 0 1
h z res ==> IdP h z res
The introduction rules for barP are recursive and go through the higher-order predicate
IdP (just like the definition of bar higher-order-recurses throuch Id). If one wants to do
this definitionally (e.g., with the inductive package), then one also has to prove the
monotonicity rule for IdP. I am not sure whether one should spent that much effort, as
[inductify] itself is very flaky anyway.
With respect to the names of the axioms, I don't care what they are called. I have never
wanted to use them, because they are really internal constructions of the code generator.
Only the generated .equation theorem is of interest. But if you want to implement stable
names, how about <predicate name>.intros?
Andreas
Email Gateway (Aug 19 2022 at 12:17):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
Thank you for the (as usual) very thorough explanation.
The introduction rules for barP are recursive and go through the higher-order predicate IdP (just like the definition of bar higher-order-recurses throuch Id). If one wants to do this definitionally (e.g., with the inductive package), then one also has to prove the monotonicity rule for IdP. I am not sure whether one should spent that much effort, as [inductify] itself is very flaky anyway.
I believe Lars Hupel is trying to attack similar problems, also in the context of the code generator.
With respect to the names of the axioms, I don't care what they are called. I have never wanted to use them, because they are really internal constructions of the code generator. Only the generated .equation theorem is of interest. But if you want to implement stable names, how about <predicate name>.intros?
I did something a bit simpler -- ".intros" doesn't quite work with "Specification.axiom", which does one axiom at a time. It's not that I care so much about the names, but for a tool like MaSh it's a bit worrying when the fact names change each time you reload the theory.
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC