author | paulson |
Mon, 30 Nov 2020 19:33:07 +0000 | |
changeset 72796 | d39a32cff5d7 |
parent 71989 | bad75618fb82 |
child 72990 | db8f94656024 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Hoare/Pointer_Examples.thy |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
3 |
Copyright 2002 TUM |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
4 |
|
41959 | 5 |
Examples of verifications of pointer programs. |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
6 |
*) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
7 |
|
16417 | 8 |
theory Pointer_Examples imports HeapSyntax begin |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
9 |
|
24499 | 10 |
axiomatization where unproven: "PROP A" |
11 |
||
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
12 |
section "Verifications" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
13 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
14 |
subsection "List reversal" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
15 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
16 |
text "A short but unreadable proof:" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
17 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
18 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
19 |
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
20 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
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> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
22 |
rev ps @ qs = rev Ps @ Qs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
23 |
DO r := p; p := p^.tl; r^.tl := q; q := r OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
24 |
{List tl q (rev Ps @ Qs)}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
25 |
apply vcg_simp |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
26 |
apply fastforce |
67444 | 27 |
apply(fastforce intro:notin_List_update[THEN iffD2]) |
28 |
\<comment> \<open>explicit:\<close> |
|
29 |
\<^cancel>\<open>apply clarify\<close> |
|
30 |
\<^cancel>\<open>apply(rename_tac ps b qs)\<close> |
|
31 |
\<^cancel>\<open>apply clarsimp\<close> |
|
32 |
\<^cancel>\<open>apply(rename_tac ps')\<close> |
|
33 |
\<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close> |
|
34 |
done |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
35 |
|
69597 | 36 |
text\<open>And now with ghost variables \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>. Even |
62042 | 37 |
``more automatic''.\<close> |
14062 | 38 |
|
39 |
lemma "VARS next p ps q qs r |
|
40 |
{List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and> |
|
41 |
ps = Ps \<and> qs = Qs} |
|
42 |
WHILE p \<noteq> Null |
|
43 |
INV {List next p ps \<and> List next q qs \<and> set ps \<inter> set qs = {} \<and> |
|
44 |
rev ps @ qs = rev Ps @ Qs} |
|
45 |
DO r := p; p := p^.next; r^.next := q; q := r; |
|
46 |
qs := (hd ps) # qs; ps := tl ps OD |
|
47 |
{List next q (rev Ps @ Qs)}" |
|
48 |
apply vcg_simp |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
49 |
apply fastforce |
14062 | 50 |
done |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
51 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
52 |
text "A longer readable version:" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
53 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
54 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
55 |
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
56 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
57 |
INV {\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
58 |
rev ps @ qs = rev Ps @ Qs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
59 |
DO r := p; p := p^.tl; r^.tl := q; q := r OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
60 |
{List tl q (rev Ps @ Qs)}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
61 |
proof vcg |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
62 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
63 |
assume "List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
64 |
thus "\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and> |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
65 |
rev ps @ qs = rev Ps @ Qs" by fastforce |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
66 |
next |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
67 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
68 |
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
69 |
rev ps @ qs = rev Ps @ Qs) \<and> p \<noteq> Null" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
70 |
(is "(\<exists>ps qs. ?I ps qs) \<and> _") |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
71 |
then obtain ps qs a where I: "?I ps qs \<and> p = Ref a" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
72 |
by fast |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
73 |
then obtain ps' where "ps = a # ps'" by fastforce |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
74 |
hence "List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
75 |
List (tl(p \<rightarrow> q)) p (a#qs) \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
76 |
set ps' \<inter> set (a#qs) = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
77 |
rev ps' @ (a#qs) = rev Ps @ Qs" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
78 |
using I by fastforce |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
79 |
thus "\<exists>ps' qs'. List (tl(p \<rightarrow> q)) (p^.tl) ps' \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
80 |
List (tl(p \<rightarrow> q)) p qs' \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
81 |
set ps' \<inter> set qs' = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
82 |
rev ps' @ qs' = rev Ps @ Qs" by fast |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
83 |
next |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
84 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
85 |
assume "(\<exists>ps qs. List tl p ps \<and> List tl q qs \<and> set ps \<inter> set qs = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
86 |
rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
87 |
thus "List tl q (rev Ps @ Qs)" by fastforce |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
88 |
qed |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
89 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
90 |
|
62042 | 91 |
text\<open>Finaly, the functional version. A bit more verbose, but automatic!\<close> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
92 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
93 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
94 |
{islist tl p \<and> islist tl q \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
95 |
Ps = list tl p \<and> Qs = list tl q \<and> set Ps \<inter> set Qs = {}} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
96 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
97 |
INV {islist tl p \<and> islist tl q \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
98 |
set(list tl p) \<inter> set(list tl q) = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
99 |
rev(list tl p) @ (list tl q) = rev Ps @ Qs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
100 |
DO r := p; p := p^.tl; r^.tl := q; q := r OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
101 |
{islist tl q \<and> list tl q = rev Ps @ Qs}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
102 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
103 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
104 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
105 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
106 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
107 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
108 |
subsection "Searching in a list" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
109 |
|
62042 | 110 |
text\<open>What follows is a sequence of successively more intelligent proofs that |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
111 |
a simple loop finds an element in a linked list. |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
112 |
|
69597 | 113 |
We start with a proof based on the \<^term>\<open>List\<close> predicate. This means it only |
62042 | 114 |
works for acyclic lists.\<close> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
115 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
116 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
117 |
{List tl p Ps \<and> X \<in> set Ps} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
118 |
WHILE p \<noteq> Null \<and> p \<noteq> Ref X |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
119 |
INV {\<exists>ps. List tl p ps \<and> X \<in> set ps} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
120 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
121 |
{p = Ref X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
122 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
123 |
apply blast |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
124 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
125 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
126 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
127 |
|
69597 | 128 |
text\<open>Using \<^term>\<open>Path\<close> instead of \<^term>\<open>List\<close> generalizes the correctness |
62042 | 129 |
statement to cyclic lists as well:\<close> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
130 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
131 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
132 |
{Path tl p Ps X} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
133 |
WHILE p \<noteq> Null \<and> p \<noteq> X |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
134 |
INV {\<exists>ps. Path tl p ps X} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
135 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
136 |
{p = X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
137 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
138 |
apply blast |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
139 |
apply fastforce |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
140 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
141 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
142 |
|
62042 | 143 |
text\<open>Now it dawns on us that we do not need the list witness at all --- it |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
144 |
suffices to talk about reachability, i.e.\ we can use relations directly. The |
69597 | 145 |
first version uses a relation on \<^typ>\<open>'a ref\<close>:\<close> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
146 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
147 |
lemma "VARS tl p |
67613 | 148 |
{(p,X) \<in> {(Ref x,tl x) |x. True}\<^sup>*} |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
149 |
WHILE p \<noteq> Null \<and> p \<noteq> X |
67613 | 150 |
INV {(p,X) \<in> {(Ref x,tl x) |x. True}\<^sup>*} |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
151 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
152 |
{p = X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
153 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
154 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
155 |
apply(erule converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
156 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
157 |
apply(clarsimp elim:converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
158 |
apply(fast elim:converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
159 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
160 |
|
69597 | 161 |
text\<open>Finally, a version based on a relation on type \<^typ>\<open>'a\<close>:\<close> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
162 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
163 |
lemma "VARS tl p |
67613 | 164 |
{p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}\<^sup>*} |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
165 |
WHILE p \<noteq> Null \<and> p \<noteq> Ref X |
67613 | 166 |
INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}\<^sup>*} |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
167 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
168 |
{p = Ref X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
169 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
170 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
171 |
apply(erule converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
172 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
173 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
174 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
175 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
176 |
|
19397 | 177 |
subsection "Splicing two lists" |
178 |
||
179 |
lemma "VARS tl p q pp qq |
|
180 |
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> size Qs \<le> size Ps} |
|
181 |
pp := p; |
|
182 |
WHILE q \<noteq> Null |
|
183 |
INV {\<exists>as bs qs. |
|
184 |
distinct as \<and> Path tl p as pp \<and> List tl pp bs \<and> List tl q qs \<and> |
|
185 |
set bs \<inter> set qs = {} \<and> set as \<inter> (set bs \<union> set qs) = {} \<and> |
|
186 |
size qs \<le> size bs \<and> splice Ps Qs = as @ splice bs qs} |
|
187 |
DO qq := q^.tl; q^.tl := pp^.tl; pp^.tl := q; pp := q^.tl; q := qq OD |
|
188 |
{List tl p (splice Ps Qs)}" |
|
189 |
apply vcg_simp |
|
190 |
apply(rule_tac x = "[]" in exI) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
191 |
apply fastforce |
19397 | 192 |
apply clarsimp |
193 |
apply(rename_tac y bs qqs) |
|
194 |
apply(case_tac bs) apply simp |
|
195 |
apply clarsimp |
|
196 |
apply(rename_tac x bbs) |
|
197 |
apply(rule_tac x = "as @ [x,y]" in exI) |
|
198 |
apply simp |
|
199 |
apply(rule_tac x = "bbs" in exI) |
|
200 |
apply simp |
|
201 |
apply(rule_tac x = "qqs" in exI) |
|
202 |
apply simp |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
203 |
apply (fastforce simp:List_app) |
19397 | 204 |
done |
205 |
||
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
206 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
207 |
subsection "Merging two lists" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
208 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
209 |
text"This is still a bit rough, especially the proof." |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
210 |
|
38353 | 211 |
definition cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
212 |
where "cor P Q \<longleftrightarrow> (if P then True else Q)" |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35316
diff
changeset
|
213 |
|
38353 | 214 |
definition cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
215 |
where "cand P Q \<longleftrightarrow> (if P then Q else False)" |
|
13773 | 216 |
|
38353 | 217 |
fun merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" |
218 |
where |
|
219 |
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) |
|
220 |
else y # merge(x#xs,ys,f))" |
|
221 |
| "merge(x#xs,[],f) = x # merge(xs,[],f)" |
|
222 |
| "merge([],y#ys,f) = y # merge([],ys,f)" |
|
223 |
| "merge([],[],f) = []" |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
224 |
|
62042 | 225 |
text\<open>Simplifies the proof a little:\<close> |
13773 | 226 |
|
227 |
lemma [simp]: "({} = insert a A \<inter> B) = (a \<notin> B & {} = A \<inter> B)" |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
228 |
by blast |
13773 | 229 |
lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)" |
230 |
by blast |
|
231 |
lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)" |
|
232 |
by blast |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
233 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
234 |
lemma "VARS hd tl p q r s |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
235 |
{List tl p Ps \<and> List tl q Qs \<and> set Ps \<inter> set Qs = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
236 |
(p \<noteq> Null \<or> q \<noteq> Null)} |
13773 | 237 |
IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
238 |
THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI; |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
239 |
s := r; |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
240 |
WHILE p \<noteq> Null \<or> q \<noteq> Null |
67613 | 241 |
INV {\<exists>rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and> |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
242 |
distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
243 |
merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) = |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
244 |
rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
245 |
(tl a = p \<or> tl a = q)} |
13773 | 246 |
DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
247 |
THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI; |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
248 |
s := s^.tl |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
249 |
OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
250 |
{List tl r (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
251 |
apply vcg_simp |
13773 | 252 |
apply (simp_all add: cand_def cor_def) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
253 |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
254 |
apply (fastforce) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
255 |
|
13773 | 256 |
apply clarsimp |
257 |
apply(rule conjI) |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
258 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
259 |
apply(rule conjI) |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
260 |
apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
261 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
262 |
apply(rule conjI) |
13773 | 263 |
apply (clarsimp) |
264 |
apply(rule_tac x = "rs @ [a]" in exI) |
|
265 |
apply(clarsimp simp:eq_sym_conv) |
|
266 |
apply(rule_tac x = "bs" in exI) |
|
267 |
apply(clarsimp simp:eq_sym_conv) |
|
268 |
apply(rule_tac x = "ya#bsa" in exI) |
|
269 |
apply(simp) |
|
270 |
apply(clarsimp simp:eq_sym_conv) |
|
271 |
apply(rule_tac x = "rs @ [a]" in exI) |
|
272 |
apply(clarsimp simp:eq_sym_conv) |
|
273 |
apply(rule_tac x = "y#bs" in exI) |
|
274 |
apply(clarsimp simp:eq_sym_conv) |
|
275 |
apply(rule_tac x = "bsa" in exI) |
|
276 |
apply(simp) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
277 |
apply (fastforce intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv) |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
278 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
279 |
apply(clarsimp simp add:List_app) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
280 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
281 |
|
62042 | 282 |
text\<open>And now with ghost variables:\<close> |
13773 | 283 |
|
14074 | 284 |
lemma "VARS elem next p q r s ps qs rs a |
285 |
{List next p Ps \<and> List next q Qs \<and> set Ps \<inter> set Qs = {} \<and> |
|
286 |
(p \<noteq> Null \<or> q \<noteq> Null) \<and> ps = Ps \<and> qs = Qs} |
|
287 |
IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem)) |
|
288 |
THEN r := p; p := p^.next; ps := tl ps |
|
289 |
ELSE r := q; q := q^.next; qs := tl qs FI; |
|
290 |
s := r; rs := []; a := addr s; |
|
291 |
WHILE p \<noteq> Null \<or> q \<noteq> Null |
|
292 |
INV {Path next r rs s \<and> List next p ps \<and> List next q qs \<and> |
|
293 |
distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and> |
|
294 |
merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y) = |
|
295 |
rs @ a # merge(ps,qs,\<lambda>x y. elem x \<le> elem y) \<and> |
|
296 |
(next a = p \<or> next a = q)} |
|
297 |
DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.elem \<le> q^.elem)) |
|
298 |
THEN s^.next := p; p := p^.next; ps := tl ps |
|
299 |
ELSE s^.next := q; q := q^.next; qs := tl qs FI; |
|
300 |
rs := rs @ [a]; s := s^.next; a := addr s |
|
301 |
OD |
|
302 |
{List next r (merge(Ps,Qs,\<lambda>x y. elem x \<le> elem y))}" |
|
303 |
apply vcg_simp |
|
304 |
apply (simp_all add: cand_def cor_def) |
|
305 |
||
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
306 |
apply (fastforce) |
14074 | 307 |
|
308 |
apply clarsimp |
|
309 |
apply(rule conjI) |
|
310 |
apply(clarsimp) |
|
311 |
apply(rule conjI) |
|
312 |
apply(clarsimp simp:neq_commute) |
|
313 |
apply(clarsimp simp:neq_commute) |
|
314 |
apply(clarsimp simp:neq_commute) |
|
315 |
||
316 |
apply(clarsimp simp add:List_app) |
|
317 |
done |
|
318 |
||
62042 | 319 |
text\<open>The proof is a LOT simpler because it does not need |
14074 | 320 |
instantiations anymore, but it is still not quite automatic, probably |
62042 | 321 |
because of this wrong orientation business.\<close> |
14074 | 322 |
|
62042 | 323 |
text\<open>More of the previous proof without ghost variables can be |
14074 | 324 |
automated, but the runtime goes up drastically. In general it is |
325 |
usually more efficient to give the witness directly than to have it |
|
326 |
found by proof. |
|
13773 | 327 |
|
69597 | 328 |
Now we try a functional version of the abstraction relation \<^term>\<open>Path\<close>. Since the result is not that convincing, we do not prove any of |
62042 | 329 |
the lemmas.\<close> |
13773 | 330 |
|
38353 | 331 |
axiomatization |
332 |
ispath :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" and |
|
333 |
path :: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list" |
|
13773 | 334 |
|
335 |
text"First some basic lemmas:" |
|
336 |
||
337 |
lemma [simp]: "ispath f p p" |
|
24499 | 338 |
by (rule unproven) |
13773 | 339 |
lemma [simp]: "path f p p = []" |
24499 | 340 |
by (rule unproven) |
13773 | 341 |
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q" |
24499 | 342 |
by (rule unproven) |
13773 | 343 |
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> |
344 |
path (f(a := r)) p q = path f p q" |
|
24499 | 345 |
by (rule unproven) |
13773 | 346 |
|
347 |
text"Some more specific lemmas needed by the example:" |
|
348 |
||
349 |
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q" |
|
24499 | 350 |
by (rule unproven) |
13773 | 351 |
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> |
352 |
path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]" |
|
24499 | 353 |
by (rule unproven) |
13773 | 354 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow> |
355 |
b \<notin> set (path f p (Ref a))" |
|
24499 | 356 |
by (rule unproven) |
13773 | 357 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p" |
24499 | 358 |
by (rule unproven) |
13773 | 359 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]" |
24499 | 360 |
by (rule unproven) |
13773 | 361 |
|
362 |
lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)" |
|
24499 | 363 |
by (rule unproven) |
13773 | 364 |
|
365 |
lemma "VARS hd tl p q r s |
|
67613 | 366 |
{islist tl p \<and> Ps = list tl p \<and> islist tl q \<and> Qs = list tl q \<and> |
13773 | 367 |
set Ps \<inter> set Qs = {} \<and> |
368 |
(p \<noteq> Null \<or> q \<noteq> Null)} |
|
369 |
IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
|
370 |
THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI; |
|
371 |
s := r; |
|
372 |
WHILE p \<noteq> Null \<or> q \<noteq> Null |
|
67613 | 373 |
INV {\<exists>rs ps qs a. ispath tl r s \<and> rs = path tl r s \<and> |
374 |
islist tl p \<and> ps = list tl p \<and> islist tl q \<and> qs = list tl q \<and> |
|
13773 | 375 |
distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and> |
376 |
merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) = |
|
377 |
rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and> |
|
378 |
(tl a = p \<or> tl a = q)} |
|
379 |
DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
|
380 |
THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI; |
|
381 |
s := s^.tl |
|
382 |
OD |
|
383 |
{islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}" |
|
384 |
apply vcg_simp |
|
385 |
||
386 |
apply (simp_all add: cand_def cor_def) |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
387 |
apply (fastforce) |
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
388 |
apply (fastforce simp: eq_sym_conv) |
13773 | 389 |
apply(clarsimp) |
390 |
done |
|
391 |
||
392 |
text"The proof is automatic, but requires a numbet of special lemmas." |
|
393 |
||
19399 | 394 |
|
395 |
subsection "Cyclic list reversal" |
|
396 |
||
397 |
||
62042 | 398 |
text\<open>We consider two algorithms for the reversal of circular lists. |
399 |
\<close> |
|
19399 | 400 |
|
401 |
lemma circular_list_rev_I: |
|
402 |
"VARS next root p q tmp |
|
403 |
{root = Ref r \<and> distPath next root (r#Ps) root} |
|
404 |
p := root; q := root^.next; |
|
405 |
WHILE q \<noteq> root |
|
406 |
INV {\<exists> ps qs. distPath next p ps root \<and> distPath next q qs root \<and> |
|
407 |
root = Ref r \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> |
|
408 |
Ps = (rev ps) @ qs } |
|
409 |
DO tmp := q; q := q^.next; tmp^.next := p; p:=tmp OD; |
|
410 |
root^.next := p |
|
411 |
{ root = Ref r \<and> distPath next root (r#rev Ps) root}" |
|
412 |
apply (simp only:distPath_def) |
|
413 |
apply vcg_simp |
|
414 |
apply (rule_tac x="[]" in exI) |
|
415 |
apply auto |
|
416 |
apply (drule (2) neq_dP) |
|
417 |
apply clarsimp |
|
418 |
apply(rule_tac x="a # ps" in exI) |
|
419 |
apply clarsimp |
|
420 |
done |
|
421 |
||
69597 | 422 |
text\<open>In the beginning, we are able to assert \<^term>\<open>distPath next |
423 |
root as root\<close>, with \<^term>\<open>as\<close> set to \<^term>\<open>[]\<close> or |
|
424 |
\<^term>\<open>[r,a,b,c]\<close>. Note that \<^term>\<open>Path next root as root\<close> would |
|
19399 | 425 |
additionally give us an infinite number of lists with the recurring |
69597 | 426 |
sequence \<^term>\<open>[r,a,b,c]\<close>. |
19399 | 427 |
|
428 |
The precondition states that there exists a non-empty non-repeating |
|
69597 | 429 |
path \mbox{\<^term>\<open>r # Ps\<close>} from pointer \<^term>\<open>root\<close> to itself, given that |
430 |
\<^term>\<open>root\<close> points to location \<^term>\<open>r\<close>. Pointers \<^term>\<open>p\<close> and |
|
431 |
\<^term>\<open>q\<close> are then set to \<^term>\<open>root\<close> and the successor of \<^term>\<open>root\<close> respectively. If \<^term>\<open>q = root\<close>, we have circled the loop, |
|
432 |
otherwise we set the \<^term>\<open>next\<close> pointer field of \<^term>\<open>q\<close> to point |
|
433 |
to \<^term>\<open>p\<close>, and shift \<^term>\<open>p\<close> and \<^term>\<open>q\<close> one step forward. The |
|
434 |
invariant thus states that \<^term>\<open>p\<close> and \<^term>\<open>q\<close> point to two |
|
435 |
disjoint lists \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>, such that \<^term>\<open>Ps = rev ps |
|
436 |
@ qs\<close>. After the loop terminates, one |
|
19399 | 437 |
extra step is needed to close the loop. As expected, the postcondition |
69597 | 438 |
states that the \<^term>\<open>distPath\<close> from \<^term>\<open>root\<close> to itself is now |
439 |
\<^term>\<open>r # (rev Ps)\<close>. |
|
19399 | 440 |
|
441 |
It may come as a surprise to the reader that the simple algorithm for |
|
442 |
acyclic list reversal, with modified annotations, works for cyclic |
|
62042 | 443 |
lists as well:\<close> |
19399 | 444 |
|
445 |
||
446 |
lemma circular_list_rev_II: |
|
447 |
"VARS next p q tmp |
|
448 |
{p = Ref r \<and> distPath next p (r#Ps) p} |
|
449 |
q:=Null; |
|
450 |
WHILE p \<noteq> Null |
|
451 |
INV |
|
452 |
{ ((q = Null) \<longrightarrow> (\<exists>ps. distPath next p (ps) (Ref r) \<and> ps = r#Ps)) \<and> |
|
453 |
((q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath next q (qs) (Ref r) \<and> List next p ps \<and> |
|
454 |
set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and> |
|
455 |
\<not> (p = Null \<and> q = Null) } |
|
456 |
DO tmp := p; p := p^.next; tmp^.next := q; q:=tmp OD |
|
457 |
{q = Ref r \<and> distPath next q (r # rev Ps) q}" |
|
458 |
apply (simp only:distPath_def) |
|
459 |
apply vcg_simp |
|
460 |
apply clarsimp |
|
461 |
apply (case_tac "(q = Null)") |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
41959
diff
changeset
|
462 |
apply (fastforce intro: Path_is_List) |
19399 | 463 |
apply clarsimp |
464 |
apply (rule_tac x= "bs" in exI) |
|
465 |
apply (rule_tac x= "y # qs" in exI) |
|
466 |
apply clarsimp |
|
467 |
apply (auto simp:fun_upd_apply) |
|
468 |
done |
|
469 |
||
470 |
||
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
471 |
subsection "Storage allocation" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
472 |
|
38353 | 473 |
definition new :: "'a set \<Rightarrow> 'a" |
474 |
where "new A = (SOME a. a \<notin> A)" |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
475 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
476 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
477 |
lemma new_notin: |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
478 |
"\<lbrakk> ~finite(UNIV::'a set); finite(A::'a set); B \<subseteq> A \<rbrakk> \<Longrightarrow> new (A) \<notin> B" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
479 |
apply(unfold new_def) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
480 |
apply(rule someI2_ex) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
481 |
apply (fast intro:ex_new_if_finite) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
482 |
apply (fast) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
483 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
484 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
485 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
486 |
lemma "~finite(UNIV::'a set) \<Longrightarrow> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
487 |
VARS xs elem next alloc p q |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
488 |
{Xs = xs \<and> p = (Null::'a ref)} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
489 |
WHILE xs \<noteq> [] |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
490 |
INV {islist next p \<and> set(list next p) \<subseteq> set alloc \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
491 |
map elem (rev(list next p)) @ xs = Xs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
492 |
DO q := Ref(new(set alloc)); alloc := (addr q)#alloc; |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
493 |
q^.next := p; q^.elem := hd xs; xs := tl xs; p := q |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
494 |
OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
495 |
{islist next p \<and> map elem (rev(list next p)) = Xs}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
496 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
497 |
apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
498 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
499 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
500 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
501 |
end |