isabelle: src/HOLCF/IMP/HoareEx.ML@2e53109d4bc8 (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
	Mon, 27 Apr 1998 16:47:50 +0200
changeset 4833	2e53109d4bc8
parent 4423	a129b817b58a
permissions	-rw-r--r--