*To*: Jasmin Christian Blanchette <jasmin.blanchette at gmail.com>, "<isabelle-users at cl.cam.ac.uk> Mailinglist" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] "code_pred" introduces axioms?*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Thu, 31 Oct 2013 16:27:57 +0100*In-reply-to*: <C28A4932-867F-4A73-A99C-6B20CAA9A19A@in.tum.de>*References*: <C28A4932-867F-4A73-A99C-6B20CAA9A19A@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.0

Hi Jasmin,

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 .

IdP barP p res ==> barP (Suc p) res barP 0 1 h z res ==> IdP h z res

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

**Follow-Ups**:**Re: [isabelle] "code_pred" introduces axioms?***From:*Jasmin Blanchette

**References**:**[isabelle] "code_pred" introduces axioms?***From:*Jasmin Christian Blanchette

- Previous by Date: [isabelle] "code_pred" introduces axioms?
- Next by Date: Re: [isabelle] "code_pred" introduces axioms?
- Previous by Thread: [isabelle] "code_pred" introduces axioms?
- Next by Thread: Re: [isabelle] "code_pred" introduces axioms?
- Cl-isabelle-users October 2013 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