Re: [isabelle] "code_pred" introduces axioms?



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


On 31/10/13 14:51, Jasmin Christian Blanchette wrote:
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






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