|
3664
|
1 |
(* Title: HOLCF/IMP/HoareEx.ML
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1997 TUM
|
|
|
5 |
|
|
|
6 |
Correctness of while-loop.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
val prems = goalw thy [hoare_valid_def]
|
|
|
10 |
"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
|
|
|
11 |
by(cut_facts_tac prems 1);
|
|
|
12 |
by (Simp_tac 1);
|
|
|
13 |
by (rtac fix_ind 1);
|
|
|
14 |
(* simplifier with enhanced adm-tactic: *)
|
|
|
15 |
by (Simp_tac 1);
|
|
|
16 |
by (Simp_tac 1);
|
|
|
17 |
by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
|
|
|
18 |
by(Blast_tac 1);
|
|
|
19 |
qed "WHILE_rule_sound";
|