[isabelle] "code_pred" introduces axioms?



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.