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.
On Mon, Nov 17, 2014 at 4:40 AM, Christian Urban <christian.urban at kcl.ac.uk>
> 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
> 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,
> 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
> > 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
> > 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 
> > (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
> > 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