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
In HOL it is not possible to express existential quantification over types.
This archive was generated by a fusion of
Pipermail (Mailman edition) and