# 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