isabelle: src/HOL/HOLCF/IMP/HoareEx.thy@b76f64d7d493 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 41476 diff changeset	1	(* Title: HOL/HOLCF/IMP/HoareEx.thy
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	2	Author: Tobias Nipkow, TUM
2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	3	Copyright 1997 TUM
2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	4	*)
2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	5
58880 0baae4311a9f modernized header; wenzelm parents: 58622 diff changeset	6	section "Correctness of Hoare by Fixpoint Reasoning"
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	7
16417 9bc16273c2d4 migrated theory headers to new format haftmann parents: 12600 diff changeset	8	theory HoareEx imports Denotational begin
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	9
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	10	text \<open>
72835 66ca5016b008 more Unicode; wenzelm parents: 67443 diff changeset	11	An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch
76987 4c275405faae isabelle update -u cite; wenzelm parents: 72835 diff changeset	12	\<^cite>\<open>MuellerNvOS99\<close>. It demonstrates fixpoint reasoning by showing
12546 0c90e581379f tuned; wenzelm parents: 12431 diff changeset	13	the correctness of the Hoare rule for while-loops.
62175 8ffc4d0e652d isabelle update_cartouches -c -t; wenzelm parents: 58880 diff changeset	14	\<close>
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	15
63549 b0d31c7def86 more symbols; wenzelm parents: 62175 diff changeset	16	type_synonym assn = "state \<Rightarrow> bool"
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	17
19737 3b8920131be2 tuned; wenzelm parents: 16417 diff changeset	18	definition
80914 d97fdabd9e2b standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing; wenzelm parents: 76987 diff changeset	19	hoare_valid :: "[assn, com, assn] \<Rightarrow> bool" (\<open>\|= {(1_)}/ (_)/ {(1_)}\<close> 50) where
63549 b0d31c7def86 more symbols; wenzelm parents: 62175 diff changeset	20	"\|= {P} c {Q} = (\<forall>s t. P s \<and> D c\<cdot>(Discr s) = Def t \<longrightarrow> Q t)"
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	21
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	22	lemma WHILE_rule_sound:
63549 b0d31c7def86 more symbols; wenzelm parents: 62175 diff changeset	23	"\|= {A} c {A} \<Longrightarrow> \|= {A} WHILE b DO c {\<lambda>s. A s \<and> \<not> bval b s}"
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	24	apply (unfold hoare_valid_def)
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	25	apply (simp (no_asm))
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	26	apply (rule fix_ind)
67443 3abf6a722518 standardized towards new-style formal comments: isabelle update_comments; wenzelm parents: 63549 diff changeset	27	apply (simp (no_asm)) \<comment> \<open>simplifier with enhanced \<open>adm\<close>-tactic\<close>
12431 07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	28	apply (simp (no_asm))
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 blast
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	31	done
07ec657249e5 converted to Isar kleing parents: 10835 diff changeset	32
3664 2dced1ac2d8e Example from HOLCF paper. nipkow parents: diff changeset	33	end

author	wenzelm
	Tue, 24 Sep 2024 21:31:20 +0200
changeset 80946	b76f64d7d493
parent 80914	d97fdabd9e2b
permissions	-rw-r--r--