isabelle: src/HOLCF/IMP/HoareEx.thy@284b56463da8 (annotated)

3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	1	(* Title: HOLCF/IMP/HoareEx.thy
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, TUM
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
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	7	header "Correctness of Hoare by Fixpoint Reasoning"
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	8
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 12600 diff changeset	9	theory HoareEx imports Denotational begin
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	10
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	11	text {*
12546 0c90e581379f tuned; wenzelm parents: 12431 diff changeset	12	An example from the HOLCF paper by M�ller, Nipkow, Oheimb, Slotosch
0c90e581379f tuned; wenzelm parents: 12431 diff changeset	13	\cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing
0c90e581379f tuned; wenzelm parents: 12431 diff changeset	14	the correctness of the Hoare rule for while-loops.
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	15	*}
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	16
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	17	types assn = "state => bool"
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	18
19737 3b8920131be2 tuned; wenzelm parents: 16417 diff changeset	19	definition
21404 eb85850d3eb7 more robust syntax for definition/abbreviation/notation; wenzelm parents: 19737 diff changeset	20	hoare_valid :: "[assn, com, assn] => bool" ("\|= {(1_)}/ (_)/ {(1_)}" 50) where
19737 3b8920131be2 tuned; wenzelm parents: 16417 diff changeset	21	"\|= {A} c {B} = (\<forall>s t. A s \<and> D c $(Discr s) = Def t --> B t)"
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	22
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	23	lemma WHILE_rule_sound:
12600 30ec65eaaf5f tuned; wenzelm parents: 12546 diff changeset	24	"\|= {A} c {A} ==> \|= {A} \<WHILE> b \<DO> c {\<lambda>s. A s \<and> \<not> b s}"
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	25	apply (unfold hoare_valid_def)
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	26	apply (simp (no_asm))
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	27	apply (rule fix_ind)
12600 30ec65eaaf5f tuned; wenzelm parents: 12546 diff changeset	28	apply (simp (no_asm)) -- "simplifier with enhanced @{text adm}-tactic"
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	29	apply (simp (no_asm))
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	30	apply (simp (no_asm))
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	31	apply blast
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	32	done
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	33
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	34	end

author	wenzelm
	Fri, 11 May 2007 17:54:36 +0200
changeset 22936	284b56463da8
parent 21404	eb85850d3eb7
child 35174	e15040ae75d7
permissions	-rw-r--r--