Re: [isabelle] Problem copying logical relation from TAPL



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.