isabelle: src/HOLCF/IMP/HoareEx.ML@6acf3ff0f486 (annotated)

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";

author	nipkow
	Thu, 26 Nov 1998 12:18:08 +0100
changeset 5974	6acf3ff0f486
parent 4833	2e53109d4bc8
permissions	-rw-r--r--