[isabelle] Problem copying logical relation from TAPL



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.