# HG changeset patch
# User nipkow
# Date 873799746 -7200
# Node ID 2dced1ac2d8e8fb90389a007daedbe905fbfdaf3
# Parent  e2d1e1151314b81d336bfdee83a98259bd57f0ec
Example from HOLCF paper.

diff -r e2d1e1151314 -r 2dced1ac2d8e src/HOLCF/IMP/HoareEx.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IMP/HoareEx.ML	Tue Sep 09 12:09:06 1997 +0200
@@ -0,0 +1,19 @@
+(*  Title:      HOLCF/IMP/HoareEx.ML
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1997 TUM
+
+Correctness of while-loop.
+*)
+
+val prems = goalw thy [hoare_valid_def]
+"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
+by(cut_facts_tac prems 1);
+by (Simp_tac 1);
+by (rtac fix_ind 1);
+  (* simplifier with enhanced adm-tactic: *)
+  by (Simp_tac 1);
+ by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by(Blast_tac 1);
+qed "WHILE_rule_sound";
diff -r e2d1e1151314 -r 2dced1ac2d8e src/HOLCF/IMP/HoareEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOLCF/IMP/HoareEx.thy	Tue Sep 09 12:09:06 1997 +0200
@@ -0,0 +1,18 @@
+(*  Title:      HOLCF/IMP/HoareEx.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow, TUM
+    Copyright   1997 TUM
+
+An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
+It demonstrates fixpoint reasoning by showing the correctness of the Hoare
+rule for while-loops.
+*)
+
+HoareEx = Denotational +
+
+types assn = state => bool
+
+constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
+ "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
+
+end