Re: [isabelle] What happens to ?thesis when there's a meta-for all quantifier?



On 12.07.2014 00:07, Holden Lee wrote:
> In the example, p and q are of type int==>bool. Contrast:
>
> lemma "⋀x. (p x)==>(q x)"
> proof -
> term ?thesis (*"q":: "int ⇒ bool"*)
> show ?thesis sorry
> qed
>
> (*
> Type unification failed: Clash of types "_ ⇒ _" and "bool"
>
> Type error in application: incompatible operand type
>
> Operator:  Trueprop :: bool ⇒ prop
> Operand:   ?thesis :: int ⇒ bool
> *)
If you have a look at ?thesis ("term ?thesis"), you'll see that ?thesis
is a lambda abstraction in this case and must be given a parameter.




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