*To*: christian.urban at kcl.ac.uk*Subject*: Re: [isabelle] Problem copying logical relation from TAPL*From*: Clarissa Littler <clarissa.littler at gmail.com>*Date*: Mon, 17 Nov 2014 07:40:30 -0800*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <m2bno6ov90.fsf@kcl.ac.uk>*References*: <CAH-5XseAqNWFxMW9PSfKxxfZoYMg9dfaCkXH4upHpS1tsyXwAw@mail.gmail.com> <m2bno6ov90.fsf@kcl.ac.uk>

Ah, that makes perfect sense. The "negativeness" in the definition of reducibility candidates just becomes recursive calls at a smaller type, which primrec/fun will accept with no problem. Thanks! On Mon, Nov 17, 2014 at 4:40 AM, Christian Urban <christian.urban at kcl.ac.uk> wrote: > > Hi Clarissa, > > Yes, indeed the negative occurrence is the stumbling block > for the inductive command. What you can do instead is define > the candidates by recursion over the type. Right now I am not > having TAPL available for the details, but I remember I followed > the strong normalisation proof in Girard's Proofs & Types book. > Maybe the file > > isabelle/src/HOL/Nominal/Examples/SN.thy > > where the candidates are defined around line 228 is of help to you. > You possibly need to ignore the nominal stuff there that is not really > important for the candidates definition. If I remember correctly > also somewhere in the sources or AFP is a similar proof by Stefan > Berghofer providing a definition for candidates. > > Hope this helps, > Christian > > On Sunday, November 16, 2014 at 10:01:43 (-0800), Clarissa Littler wrote: > > Hi, > > So just as an exercise I was going to formalize ch 12 of Types and > > Programming Languages and, well, I was defining the inductive relation > for > > reducibility candidates as > > > > inductive R :: "lam ⇒ ty ⇒ bool" where > > Ra : "⟦halts y; typing [] y A⟧ ⟹ R a A" | > > RArr : "⟦halts l; (∀ y. R y ty1 ⟶ R (App l y) ty2); typing [] l (Arr > ty1 > > ty2)⟧ ⟹ R l (Arr ty1 ty2)" > > > > and I got the following error that I really don't know how to fix > > > > Proof failed. > > 1. ⋀x y xa xb l ty1 ty2 ya. > > x (?x25 x y xa xb l ty1 ty2 ya) (?x26 x y xa xb l ty1 ty2 ya) ⟶ > > y (?x25 x y xa xb l ty1 ty2 ya) (?x26 x y xa xb l ty1 ty2 ya) ⟹ > > y ya ty1 ⟶ x ya ty1 > > 2. ⋀x y xa xb l ty1 ty2 ya. x ≤ y ⟹ x (App l ya) ty2 ⟶ y (App l ya) ty2 > > 3. ⋀x y xa xb l ty1 ty2. x ≤ y ⟹ typing [] l (Arr ty1 ty2) ⟶ typing [] > l > > (Arr ty1 ty2) > > The error(s) above occurred for the goal statement⌂: > > mono (λp x1 x2. > > (∃y. x1 = a ∧ x2 = A ∧ halts y ∧ typing [] y A) ∨ > > (∃l ty1 ty2. > > x1 = l ∧ > > x2 = Arr ty1 ty2 ∧ halts l ∧ (∀y. p y ty1 ⟶ p (App l y) > ty2) ∧ > > typing [] l (Arr ty1 ty2))) > > > > I'm guessing it's about negative recursion in the pre-condition of the > RArr > > rule, but that also seems to be exactly the definition that TAPL uses so > > I'm not sure what's what. > > > > Cheers, > > Clarissa > > -- >

**References**:**[isabelle] Problem copying logical relation from TAPL***From:*Clarissa Littler

**Re: [isabelle] Problem copying logical relation from TAPL***From:*Christian Urban

- Previous by Date: Re: [isabelle] Behaviour of Variable.variant_fixes
- Next by Date: Re: [isabelle] Reindexing series
- Previous by Thread: Re: [isabelle] Problem copying logical relation from TAPL
- Next by Thread: [isabelle] Reindexing series
- Cl-isabelle-users November 2014 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