Re: [isabelle] How to understand the example hoare



Hello li yongjian
On Monday 10 July 2006 11:37, li yongjian wrote:
> cl-isabelle-users:
>     my problem is about a command in the \src\Hoare\Hoare.thy  .
>
> method_setup vcg = {*
>   Method.no_args
>     (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *}
>   "verification condition generator"
>
> where do I find the semantical explanation about this command.

This command links the ML tactic "hoare_tac" to the Isar-method vcg. So you 
can use it by "apply vcg" later on. To use the Hoare-logic you do not have to 
understand this. Only if you want to implement a similar module like "Hoare" 
you have to know about the ML-internals of Isabelle.

>
> Especially what is "K"?
This is the famous combinator: K x y = x

> This example is too difficult for me.

Have a look at /Hoare/Examples.thy to see how to use the Hoare-logic and the 
verification condition generator.

   Norbert





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