Re: [isabelle] Goal.prove with auto_tac



Hello Steve,

Try using the prop antiquotation, i.e.,

  val t = @{prop "EX x. x = 0"}

The background is that HOL is a logic embedded in Isabelle's
metalogic, and every HOL property needs to be coerced into a meta
justification, for example by using the prop antiquotation.  A more
explicit way to express this would be as follows:

  val t = HOLogic.mk_Trueprop @{term "EX x. x = 0"}

Regards,
Sascha

Steve W wrote:
> Hello,
> 
> I'm trying to experiment with Goal.prove on a very simple lemma:
> 
> ML {*
>   let
>     val trm = @{term "EX x. x = 0"}
>     val ctxt = @{context}
>   in
>     Goal.prove ctxt [] [] trm (K (auto_tac (clasimpset_of ctxt)))
>   end;
> 
> *}
> 
> Unfortunately, I get an exception saying "instantiate: type conflict". Does
> anyone know what I'm doing wrong? I know I could write it as a tactic and
> apply it in Isar, but I'm just trying to experiment with Goal.prove.
> 
> Regards,
> Steve





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