src/HOLCF/IMP/HoareEx.ML
author wenzelm
Tue, 28 Jul 1998 17:05:34 +0200
changeset 5210 54aaa779b6b4
parent 4833 2e53109d4bc8
permissions -rw-r--r--
removed global_names flag;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3664
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/IMP/HoareEx.ML
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     4
    Copyright   1997 TUM
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     5
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     6
Correctness of while-loop.
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     7
*)
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     8
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
     9
val prems = goalw thy [hoare_valid_def]
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    10
"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
    11
by (cut_facts_tac prems 1);
3664
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    12
by (Simp_tac 1);
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    13
by (rtac fix_ind 1);
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    14
  (* simplifier with enhanced adm-tactic: *)
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    15
  by (Simp_tac 1);
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    16
 by (Simp_tac 1);
4833
2e53109d4bc8 Renamed expand_const -> split_const
nipkow
parents: 4423
diff changeset
    17
by (Simp_tac 1);
4423
a129b817b58a expandshort;
wenzelm
parents: 4098
diff changeset
    18
by (Blast_tac 1);
3664
2dced1ac2d8e Example from HOLCF paper.
nipkow
parents:
diff changeset
    19
qed "WHILE_rule_sound";