Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to understand the example hoare

Email Gateway (Aug 18 2022 at 09:26):

From: li yongjian <lyj238@ios.ac.cn>
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.

Especially what is "K"?

This example is too difficult for me.

who write the example or understand it, and can you give some helpful
suggestion to read it?

regards

Email Gateway (Aug 18 2022 at 09:29):

From: Norbert Schirmer <norbert.schirmer@web.de>
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

Last updated: May 03 2024 at 08:18 UTC