Re: [isabelle] "PROOF FAILED for depth4"




         > lemma te_zero: "EX func t. func t = 0"
         >
         > proof (intro exI)
         >
         >  show "F s = 0"
         >
         >

        Thanks for the help. Unfortunately, I get an error from this,
        saying that it can't solve goal by exported rule: F s = 0. Any
        hint on this will be appreciated.


    You may need to add type annotations to make sure that the types in
    your lemma statement are not more general than you want. Switch on
    "Isabelle -> Settings -> Show Types".


I see. However, why can't the types in the lemma be more general even the function is existentially quantified? Can't a' and b' be instantiated to real for F s = 0 in the proof?

The variable func is existentially quantified, but the type variables 'a and 'b are (implicitly) universally quantified. So you cannot instantiate them.

In HOL it is not possible to express existential quantification over types.

Alex






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