isabelle: src/HOL/Hoare/Pointer_ExamplesAbort.thy@43142ac556e6 (annotated)

13875 12997e3ddd8d * empty log message * nipkow parents: diff changeset	1	(* Title: HOL/Hoare/Pointer_ExamplesAbort.thy
12997e3ddd8d * empty log message * nipkow parents: diff changeset	2	Author: Tobias Nipkow
12997e3ddd8d * empty log message * nipkow parents: diff changeset	3	Copyright 2002 TUM
12997e3ddd8d * empty log message * nipkow parents: diff changeset	4	*)
12997e3ddd8d * empty log message * nipkow parents: diff changeset	5
72990 db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	6	section \<open>Examples of verifications of pointer programs\<close>
13875 12997e3ddd8d * empty log message * nipkow parents: diff changeset	7
72990 db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	8	theory Pointer_ExamplesAbort
db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	9	imports HeapSyntaxAbort
db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	10	begin
13875 12997e3ddd8d * empty log message * nipkow parents: diff changeset	11
72990 db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	12	subsection "Verifications"
db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	13
db8f94656024 tuned document, notably authors and sections; wenzelm parents: 71989 diff changeset	14	subsubsection "List reversal"
13875 12997e3ddd8d * empty log message * nipkow parents: diff changeset	15
12997e3ddd8d * empty log message * nipkow parents: diff changeset	16	text "Interestingly, this proof is the same as for the unguarded program:"
12997e3ddd8d * empty log message * nipkow parents: diff changeset	17
12997e3ddd8d * empty log message * nipkow parents: diff changeset	18	lemma "VARS tl p q r
12997e3ddd8d * empty log message * nipkow parents: diff changeset	19	{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}}
12997e3ddd8d * empty log message * nipkow parents: diff changeset	20	WHILE p \<noteq> Null
12997e3ddd8d * empty log message * nipkow parents: diff changeset	21	INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and>
12997e3ddd8d * empty log message * nipkow parents: diff changeset	22	rev ps @ qs = rev Ps @ Qs}
12997e3ddd8d * empty log message * nipkow parents: diff changeset	23	DO r := p; (p \<noteq> Null \<rightarrow> p := p^.tl); r^.tl := q; q := r OD
12997e3ddd8d * empty log message * nipkow parents: diff changeset	24	{List tl q (rev Ps @ Qs)}"
12997e3ddd8d * empty log message * nipkow parents: diff changeset	25	apply vcg_simp
44890 22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 38353 diff changeset	26	apply fastforce
22f665a2e91c new fastforce replacing fastsimp - less confusing name nipkow parents: 38353 diff changeset	27	apply(fastforce intro:notin_List_update[THEN iffD2])
13875 12997e3ddd8d * empty log message * nipkow parents: diff changeset	28	done
12997e3ddd8d * empty log message * nipkow parents: diff changeset	29
12997e3ddd8d * empty log message * nipkow parents: diff changeset	30	end

author	haftmann
	Thu, 28 Oct 2021 06:39:36 +0000
changeset 74618	43142ac556e6
parent 72990	db8f94656024
permissions	-rw-r--r--