src/HOL/Hoare/Pointer_ExamplesAbort.thy
author wenzelm
Mon, 21 Jul 2025 16:21:37 +0200
changeset 82892 45107da819fc
parent 72990 db8f94656024
permissions -rw-r--r--
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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