[isabelle] Non-atomic premise



Hi,

when I use

        inductive fun_rel' for P where
          fun_relI'[intro]: "(⋀ x. P (id m x) (id m' x)) ⟹ fun_rel' P m
        m'"
        
inductive works without problem. But when I do

        inductive fun_rel' for P where
          fun_relI'[intro]: "(⋀ x. P (m x) (m' x)) ⟹ fun_rel' P m m'"

I get:

        Proofs for inductive predicate(s) "fun_rel" 
        Ill-formed premise
        ⋀x. P (m x) (m' x)
        in introduction rule "fun_relI"
        ⋀m m'. (⋀x. P (m x) (m' x)) ⟹ fun_rel P m m'
        Non-atomic premise

I don’t understand the error message, nor why it should not work. Can
anyone enlighten me?

Thanks,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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