author | nipkow |
Sun, 23 Mar 2003 11:57:07 +0100 | |
changeset 13875 | 12997e3ddd8d |
parent 13773 | 58dc4ab362d0 |
child 14062 | 7f0d5cc52615 |
permissions | -rw-r--r-- |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
1 |
(* Title: HOL/Hoare/Pointers.thy |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
4 |
Copyright 2002 TUM |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
5 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
6 |
Examples of verifications of pointer programs |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
7 |
*) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
8 |
|
13875 | 9 |
theory Pointer_Examples = HeapSyntax: |
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
10 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
11 |
section "Verifications" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
12 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
13 |
subsection "List reversal" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
14 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
15 |
text "A short but unreadable proof:" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
16 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
17 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
18 |
{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
|
19 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
20 |
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
|
21 |
rev ps @ qs = rev Ps @ Qs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
22 |
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
|
23 |
{List tl q (rev Ps @ Qs)}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
24 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
25 |
apply fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
26 |
apply(fastsimp intro:notin_List_update[THEN iffD2]) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
27 |
(* explicit: |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
28 |
apply clarify |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
29 |
apply(rename_tac ps b qs) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
30 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
31 |
apply(rename_tac ps') |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
32 |
apply(fastsimp intro:notin_List_update[THEN iffD2]) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
33 |
apply(rule_tac x = ps' in exI) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
34 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
35 |
apply(rule_tac x = "b#qs" in exI) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
36 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
37 |
*) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
38 |
apply fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
39 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
40 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
41 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
42 |
text "A longer readable version:" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
43 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
44 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
45 |
{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
|
46 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
47 |
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
|
48 |
rev ps @ qs = rev Ps @ Qs} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
49 |
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
|
50 |
{List tl q (rev Ps @ Qs)}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
51 |
proof vcg |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
52 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
53 |
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
|
54 |
thus "\<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
|
55 |
rev ps @ qs = rev Ps @ Qs" by fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
56 |
next |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
57 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
58 |
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
|
59 |
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
|
60 |
(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
|
61 |
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
|
62 |
by fast |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
63 |
then obtain ps' where "ps = a # ps'" by fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
rev ps' @ (a#qs) = rev Ps @ Qs" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
68 |
using I by fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
69 |
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
|
70 |
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
|
71 |
set ps' \<inter> set qs' = {} \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
72 |
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
|
73 |
next |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
74 |
fix tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
75 |
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
|
76 |
rev ps @ qs = rev Ps @ Qs) \<and> \<not> p \<noteq> Null" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
77 |
thus "List tl q (rev Ps @ Qs)" by fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
78 |
qed |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
79 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
80 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
81 |
text{* Finaly, the functional version. A bit more verbose, but automatic! *} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
82 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
83 |
lemma "VARS tl p q r |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
84 |
{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
|
85 |
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
|
86 |
WHILE p \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
{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
|
92 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
93 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
94 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
95 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
96 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
97 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
98 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
99 |
subsection "Searching in a list" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
100 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
101 |
text{*What follows is a sequence of successively more intelligent proofs that |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
102 |
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
|
103 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
104 |
We start with a proof based on the @{term List} predicate. This means it only |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
105 |
works for acyclic lists. *} |
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 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
108 |
{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
|
109 |
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
|
110 |
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
|
111 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
112 |
{p = Ref X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
113 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
114 |
apply blast |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
115 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
116 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
117 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
118 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
119 |
text{*Using @{term Path} instead of @{term List} generalizes the correctness |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
120 |
statement to cyclic lists as well: *} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
121 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
122 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
123 |
{Path tl p Ps X} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
124 |
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
|
125 |
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
|
126 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
127 |
{p = X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
128 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
129 |
apply blast |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
130 |
apply fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
131 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
132 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
133 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
134 |
text{*Now it dawns on us that we do not need the list witness at all --- it |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
135 |
suffices to talk about reachability, i.e.\ we can use relations directly. The |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
136 |
first version uses a relation on @{typ"'a ref"}: *} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
137 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
138 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
139 |
{(p,X) \<in> {(Ref x,tl x) |x. True}^*} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
140 |
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
|
141 |
INV {(p,X) \<in> {(Ref x,tl x) |x. True}^*} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
142 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
143 |
{p = X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
144 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
145 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
146 |
apply(erule converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
147 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
148 |
apply(clarsimp elim:converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
149 |
apply(fast elim:converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
150 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
151 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
152 |
text{*Finally, a version based on a relation on type @{typ 'a}:*} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
153 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
154 |
lemma "VARS tl p |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
155 |
{p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
156 |
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
|
157 |
INV {p \<noteq> Null \<and> (addr p,X) \<in> {(x,y). tl x = Ref y}^*} |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
158 |
DO p := p^.tl OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
159 |
{p = Ref X}" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
160 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
161 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
162 |
apply(erule converse_rtranclE) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
163 |
apply simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
164 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
165 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
166 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
167 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
168 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
169 |
subsection "Merging two lists" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
170 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
171 |
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
|
172 |
|
13773 | 173 |
constdefs |
174 |
cor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
175 |
"cor P Q == if P then True else Q" |
|
176 |
cand :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
177 |
"cand P Q == if P then Q else False" |
|
178 |
||
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
179 |
consts merge :: "'a list * 'a list * ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
180 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
181 |
recdef merge "measure(%(xs,ys,f). size xs + size ys)" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
182 |
"merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
183 |
else y # merge(x#xs,ys,f))" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
184 |
"merge(x#xs,[],f) = x # merge(xs,[],f)" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
185 |
"merge([],y#ys,f) = y # merge([],ys,f)" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
186 |
"merge([],[],f) = []" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
187 |
|
13773 | 188 |
text{* Simplifies the proof a little: *} |
189 |
||
190 |
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
|
191 |
by blast |
13773 | 192 |
lemma [simp]: "({} = A \<inter> insert b B) = (b \<notin> A & {} = A \<inter> B)" |
193 |
by blast |
|
194 |
lemma [simp]: "({} = A \<inter> (B \<union> C)) = ({} = A \<inter> B & {} = A \<inter> C)" |
|
195 |
by blast |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
196 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
197 |
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
|
198 |
{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
|
199 |
(p \<noteq> Null \<or> q \<noteq> Null)} |
13773 | 200 |
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
|
201 |
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
|
202 |
s := r; |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
203 |
WHILE p \<noteq> Null \<or> q \<noteq> Null |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
204 |
INV {EX rs ps qs a. Path tl r rs s \<and> List tl p ps \<and> List tl q qs \<and> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
205 |
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
|
206 |
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
|
207 |
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
|
208 |
(tl a = p \<or> tl a = q)} |
13773 | 209 |
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
|
210 |
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
|
211 |
s := s^.tl |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
212 |
OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
213 |
{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
|
214 |
apply vcg_simp |
13773 | 215 |
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
|
216 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
217 |
apply (fastsimp) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
218 |
|
13773 | 219 |
apply clarsimp |
220 |
apply(rule conjI) |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
221 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
222 |
apply(rule conjI) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
223 |
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
224 |
apply clarsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
225 |
apply(rule conjI) |
13773 | 226 |
apply (clarsimp) |
227 |
apply(rule_tac x = "rs @ [a]" in exI) |
|
228 |
apply(clarsimp simp:eq_sym_conv) |
|
229 |
apply(rule_tac x = "bs" in exI) |
|
230 |
apply(clarsimp simp:eq_sym_conv) |
|
231 |
apply(rule_tac x = "ya#bsa" in exI) |
|
232 |
apply(simp) |
|
233 |
apply(clarsimp simp:eq_sym_conv) |
|
234 |
apply(rule_tac x = "rs @ [a]" in exI) |
|
235 |
apply(clarsimp simp:eq_sym_conv) |
|
236 |
apply(rule_tac x = "y#bs" in exI) |
|
237 |
apply(clarsimp simp:eq_sym_conv) |
|
238 |
apply(rule_tac x = "bsa" in exI) |
|
239 |
apply(simp) |
|
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
240 |
apply (fastsimp intro!:Path_snoc intro:Path_upd[THEN iffD2] notin_List_update[THEN iffD2] simp:eq_sym_conv) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
241 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
242 |
apply(clarsimp simp add:List_app) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
243 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
244 |
|
13773 | 245 |
|
246 |
text{* More of the proof can be automated, but the runtime goes up |
|
247 |
drastically. In general it is usually more efficient to give the |
|
248 |
witness directly than to have it found by proof. |
|
249 |
||
250 |
Now we try a functional version of the abstraction relation @{term |
|
251 |
Path}. Since the result is not that convincing, we do not prove any of |
|
252 |
the lemmas.*} |
|
253 |
||
254 |
consts ispath:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> bool" |
|
255 |
path:: "('a \<Rightarrow> 'a ref) \<Rightarrow> 'a ref \<Rightarrow> 'a ref \<Rightarrow> 'a list" |
|
256 |
||
257 |
ML"set quick_and_dirty" |
|
258 |
||
259 |
text"First some basic lemmas:" |
|
260 |
||
261 |
lemma [simp]: "ispath f p p" |
|
262 |
sorry |
|
263 |
lemma [simp]: "path f p p = []" |
|
264 |
sorry |
|
265 |
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> ispath (f(a := r)) p q" |
|
266 |
sorry |
|
267 |
lemma [simp]: "ispath f p q \<Longrightarrow> a \<notin> set(path f p q) \<Longrightarrow> |
|
268 |
path (f(a := r)) p q = path f p q" |
|
269 |
sorry |
|
270 |
||
271 |
text"Some more specific lemmas needed by the example:" |
|
272 |
||
273 |
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> ispath (f(a := q)) p q" |
|
274 |
sorry |
|
275 |
lemma [simp]: "ispath (f(a := q)) p (Ref a) \<Longrightarrow> |
|
276 |
path (f(a := q)) p q = path (f(a := q)) p (Ref a) @ [a]" |
|
277 |
sorry |
|
278 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Ref b \<Longrightarrow> |
|
279 |
b \<notin> set (path f p (Ref a))" |
|
280 |
sorry |
|
281 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> islist f p" |
|
282 |
sorry |
|
283 |
lemma [simp]: "ispath f p (Ref a) \<Longrightarrow> f a = Null \<Longrightarrow> list f p = path f p (Ref a) @ [a]" |
|
284 |
sorry |
|
285 |
||
286 |
lemma [simp]: "islist f p \<Longrightarrow> distinct (list f p)" |
|
287 |
sorry |
|
288 |
ML"reset quick_and_dirty" |
|
289 |
||
290 |
lemma "VARS hd tl p q r s |
|
291 |
{islist tl p & Ps = list tl p \<and> islist tl q & Qs = list tl q \<and> |
|
292 |
set Ps \<inter> set Qs = {} \<and> |
|
293 |
(p \<noteq> Null \<or> q \<noteq> Null)} |
|
294 |
IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
|
295 |
THEN r := p; p := p^.tl ELSE r := q; q := q^.tl FI; |
|
296 |
s := r; |
|
297 |
WHILE p \<noteq> Null \<or> q \<noteq> Null |
|
298 |
INV {EX rs ps qs a. ispath tl r s & rs = path tl r s \<and> |
|
299 |
islist tl p & ps = list tl p \<and> islist tl q & qs = list tl q \<and> |
|
300 |
distinct(a # ps @ qs @ rs) \<and> s = Ref a \<and> |
|
301 |
merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y) = |
|
302 |
rs @ a # merge(ps,qs,\<lambda>x y. hd x \<le> hd y) \<and> |
|
303 |
(tl a = p \<or> tl a = q)} |
|
304 |
DO IF cor (q = Null) (cand (p \<noteq> Null) (p^.hd \<le> q^.hd)) |
|
305 |
THEN s^.tl := p; p := p^.tl ELSE s^.tl := q; q := q^.tl FI; |
|
306 |
s := s^.tl |
|
307 |
OD |
|
308 |
{islist tl r & list tl r = (merge(Ps,Qs,\<lambda>x y. hd x \<le> hd y))}" |
|
309 |
apply vcg_simp |
|
310 |
||
311 |
apply (simp_all add: cand_def cor_def) |
|
312 |
apply (fastsimp) |
|
313 |
apply (fastsimp simp: eq_sym_conv) |
|
314 |
apply(clarsimp) |
|
315 |
done |
|
316 |
||
317 |
text"The proof is automatic, but requires a numbet of special lemmas." |
|
318 |
||
13772
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
319 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
320 |
subsection "Storage allocation" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
321 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
322 |
constdefs new :: "'a set \<Rightarrow> 'a" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
323 |
"new A == SOME a. a \<notin> A" |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
324 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
325 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
326 |
lemma new_notin: |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
327 |
"\<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
|
328 |
apply(unfold new_def) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
329 |
apply(rule someI2_ex) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
330 |
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
|
331 |
apply (fast) |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
332 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
333 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
334 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
335 |
lemma "~finite(UNIV::'a set) \<Longrightarrow> |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
336 |
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
|
337 |
{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
|
338 |
WHILE xs \<noteq> [] |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
339 |
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
|
340 |
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
|
341 |
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
|
342 |
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
|
343 |
OD |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
344 |
{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
|
345 |
apply vcg_simp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
346 |
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
|
347 |
apply fastsimp |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
348 |
done |
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
349 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
350 |
|
73d041cc6a66
Split Pointers.thy and automated one proof, which caused the runtime to explode
nipkow
parents:
diff
changeset
|
351 |
end |