Re: [isabelle] Problem copying logical relation from TAPL



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
>
> --
>



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