# [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.*