author | nipkow |
Tue, 07 Sep 2010 10:05:19 +0200 | |
changeset 39198 | f967a16dfcdd |
parent 35802 | 362431732b5e |
child 39302 | d7728f65b353 |
permissions | -rw-r--r-- |
28583 | 1 |
theory Live imports Natural |
2 |
begin |
|
3 |
||
4 |
text{* Which variables/locations does an expression depend on? |
|
5 |
Any set of variables that completely determine the value of the expression, |
|
6 |
in the worst case all locations: *} |
|
7 |
||
8 |
consts Dep :: "((loc \<Rightarrow> 'a) \<Rightarrow> 'b) \<Rightarrow> loc set" |
|
9 |
specification (Dep) |
|
10 |
dep_on: "(\<forall>x\<in>Dep e. s x = t x) \<Longrightarrow> e s = e t" |
|
39198 | 11 |
by(rule_tac x="%x. UNIV" in exI)(simp add: ext_iff[symmetric]) |
28583 | 12 |
|
13 |
text{* The following definition of @{const Dep} looks very tempting |
|
14 |
@{prop"Dep e = {a. EX s t. (ALL x. x\<noteq>a \<longrightarrow> s x = t x) \<and> e s \<noteq> e t}"} |
|
15 |
but does not work in case @{text e} depends on an infinite set of variables. |
|
16 |
For example, if @{term"e s"} tests if @{text s} is 0 at infinitely many locations. Then @{term"Dep e"} incorrectly yields the empty set! |
|
17 |
||
18 |
If we had a concrete representation of expressions, we would simply write |
|
19 |
a recursive free-variables function. |
|
20 |
*} |
|
21 |
||
22 |
primrec L :: "com \<Rightarrow> loc set \<Rightarrow> loc set" where |
|
23 |
"L SKIP A = A" | |
|
24 |
"L (x :== e) A = A-{x} \<union> Dep e" | |
|
25 |
"L (c1; c2) A = (L c1 \<circ> L c2) A" | |
|
26 |
"L (IF b THEN c1 ELSE c2) A = Dep b \<union> L c1 A \<union> L c2 A" | |
|
27 |
"L (WHILE b DO c) A = Dep b \<union> A \<union> L c A" |
|
28 |
||
29 |
primrec "kill" :: "com \<Rightarrow> loc set" where |
|
30 |
"kill SKIP = {}" | |
|
31 |
"kill (x :== e) = {x}" | |
|
32 |
"kill (c1; c2) = kill c1 \<union> kill c2" | |
|
33 |
"kill (IF b THEN c1 ELSE c2) = Dep b \<union> kill c1 \<inter> kill c2" | |
|
34 |
"kill (WHILE b DO c) = {}" |
|
35 |
||
36 |
primrec gen :: "com \<Rightarrow> loc set" where |
|
37 |
"gen SKIP = {}" | |
|
38 |
"gen (x :== e) = Dep e" | |
|
39 |
"gen (c1; c2) = gen c1 \<union> (gen c2-kill c1)" | |
|
40 |
"gen (IF b THEN c1 ELSE c2) = Dep b \<union> gen c1 \<union> gen c2" | |
|
41 |
"gen (WHILE b DO c) = Dep b \<union> gen c" |
|
42 |
||
43 |
lemma L_gen_kill: "L c A = gen c \<union> (A - kill c)" |
|
44 |
by(induct c arbitrary:A) auto |
|
45 |
||
46 |
lemma L_idemp: "L c (L c A) \<subseteq> L c A" |
|
47 |
by(fastsimp simp add:L_gen_kill) |
|
48 |
||
49 |
theorem L_sound: "\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
50 |
\<forall>x\<in>A. s' x = t' x" |
|
51 |
proof (induct c arbitrary: A s t s' t') |
|
52 |
case SKIP then show ?case by auto |
|
53 |
next |
|
54 |
case (Assign x e) then show ?case |
|
55 |
by (auto simp:update_def ball_Un dest!: dep_on) |
|
56 |
next |
|
57 |
case (Semi c1 c2) |
|
58 |
from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" |
|
59 |
by auto |
|
60 |
from Semi(5) obtain t'' where t1: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>c2,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
61 |
by auto |
|
62 |
show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp |
|
63 |
next |
|
64 |
case (Cond b c1 c2) |
|
65 |
show ?case |
|
66 |
proof cases |
|
67 |
assume "b s" |
|
68 |
hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp |
|
69 |
have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
70 |
hence t: "\<langle>c1,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
71 |
show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp |
|
72 |
next |
|
73 |
assume "\<not> b s" |
|
74 |
hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto |
|
75 |
have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
76 |
hence t: "\<langle>c2,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
77 |
show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp |
|
78 |
qed |
|
79 |
next |
|
80 |
case (While b c) note IH = this |
|
81 |
{ fix cw |
|
82 |
have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>cw,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
83 |
\<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x" |
|
84 |
proof (induct arbitrary: t A pred:evalc) |
|
85 |
case WhileFalse |
|
86 |
have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) |
|
87 |
then have "t' = t" using WhileFalse by auto |
|
88 |
then show ?case using WhileFalse by auto |
|
89 |
next |
|
90 |
case (WhileTrue _ s _ s'' s') |
|
91 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp |
|
92 |
have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) |
|
93 |
then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
94 |
using WhileTrue(6,7) by auto |
|
28867 | 95 |
have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
96 |
using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
97 |
by (auto simp:L_gen_kill) |
35802 | 98 |
then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
99 |
then show ?case using WhileTrue(5,6) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
28583 | 100 |
qed auto } |
35802 | 101 |
-- "a terser version" |
102 |
{ let ?w = "While b c" |
|
103 |
have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>?w,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
104 |
\<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x" |
|
105 |
proof (induct ?w s s' arbitrary: t A pred:evalc) |
|
106 |
case WhileFalse |
|
107 |
have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) |
|
108 |
then have "t' = t" using WhileFalse by auto |
|
109 |
then show ?case using WhileFalse by simp |
|
110 |
next |
|
111 |
case (WhileTrue s s'' s') |
|
112 |
have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) |
|
113 |
then obtain t'' where "\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''" and "\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
114 |
using WhileTrue(6,7) by auto |
|
115 |
have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
116 |
using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(7) |
|
117 |
by (auto simp:L_gen_kill) |
|
118 |
then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
|
119 |
then show ?case using WhileTrue(5) `\<langle>While b c,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
120 |
qed } |
|
121 |
from this[OF IH(3) IH(4,2)] show ?case by metis |
|
28583 | 122 |
qed |
123 |
||
28867 | 124 |
|
125 |
primrec bury :: "com \<Rightarrow> loc set \<Rightarrow> com" where |
|
126 |
"bury SKIP _ = SKIP" | |
|
127 |
"bury (x :== e) A = (if x:A then x:== e else SKIP)" | |
|
128 |
"bury (c1; c2) A = (bury c1 (L c2 A); bury c2 A)" | |
|
129 |
"bury (IF b THEN c1 ELSE c2) A = (IF b THEN bury c1 A ELSE bury c2 A)" | |
|
130 |
"bury (WHILE b DO c) A = (WHILE b DO bury c (Dep b \<union> A \<union> L c A))" |
|
131 |
||
132 |
theorem bury_sound: |
|
133 |
"\<forall> x \<in> L c A. s x = t x \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury c A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
134 |
\<forall>x\<in>A. s' x = t' x" |
|
135 |
proof (induct c arbitrary: A s t s' t') |
|
136 |
case SKIP then show ?case by auto |
|
137 |
next |
|
138 |
case (Assign x e) then show ?case |
|
139 |
by (auto simp:update_def ball_Un split:split_if_asm dest!: dep_on) |
|
140 |
next |
|
141 |
case (Semi c1 c2) |
|
142 |
from Semi(4) obtain s'' where s1: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" and s2: "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" |
|
143 |
by auto |
|
144 |
from Semi(5) obtain t'' where t1: "\<langle>bury c1 (L c2 A),t\<rangle> \<longrightarrow>\<^sub>c t''" and t2: "\<langle>bury c2 A,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
145 |
by auto |
|
146 |
show ?case using Semi(1)[OF _ s1 t1] Semi(2)[OF _ s2 t2] Semi(3) by fastsimp |
|
147 |
next |
|
148 |
case (Cond b c1 c2) |
|
149 |
show ?case |
|
150 |
proof cases |
|
151 |
assume "b s" |
|
152 |
hence s: "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by simp |
|
153 |
have "b t" using `b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
154 |
hence t: "\<langle>bury c1 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
155 |
show ?thesis using Cond(1)[OF _ s t] Cond(3) by fastsimp |
|
156 |
next |
|
157 |
assume "\<not> b s" |
|
158 |
hence s: "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" using Cond(4) by auto |
|
159 |
have "\<not> b t" using `\<not> b s` Cond(3) by (simp add: ball_Un)(blast dest: dep_on) |
|
160 |
hence t: "\<langle>bury c2 A,t\<rangle> \<longrightarrow>\<^sub>c t'" using Cond(5) by auto |
|
161 |
show ?thesis using Cond(2)[OF _ s t] Cond(3) by fastsimp |
|
162 |
qed |
|
163 |
next |
|
164 |
case (While b c) note IH = this |
|
165 |
{ fix cw |
|
166 |
have "\<langle>cw,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> cw = (While b c) \<Longrightarrow> \<langle>bury cw A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
167 |
\<forall> x \<in> L cw A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x" |
|
168 |
proof (induct arbitrary: t A pred:evalc) |
|
169 |
case WhileFalse |
|
170 |
have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) |
|
171 |
then have "t' = t" using WhileFalse by auto |
|
172 |
then show ?case using WhileFalse by auto |
|
173 |
next |
|
174 |
case (WhileTrue _ s _ s'' s') |
|
175 |
have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''" using WhileTrue(2,6) by simp |
|
176 |
have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) |
|
177 |
then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
178 |
and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
28867 | 179 |
using WhileTrue(6,7) by auto |
180 |
have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
181 |
using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
182 |
by (auto simp:L_gen_kill) |
28867 | 183 |
moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
184 |
ultimately show ?case |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
28867
diff
changeset
|
185 |
using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
28867 | 186 |
qed auto } |
35802 | 187 |
{ let ?w = "While b c" |
188 |
have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>bury ?w A,t\<rangle> \<longrightarrow>\<^sub>c t' \<Longrightarrow> |
|
189 |
\<forall> x \<in> L ?w A. s x = t x \<Longrightarrow> \<forall>x\<in>A. s' x = t' x" |
|
190 |
proof (induct ?w s s' arbitrary: t A pred:evalc) |
|
191 |
case WhileFalse |
|
192 |
have "\<not> b t" using WhileFalse by (simp add: ball_Un)(blast dest:dep_on) |
|
193 |
then have "t' = t" using WhileFalse by auto |
|
194 |
then show ?case using WhileFalse by simp |
|
195 |
next |
|
196 |
case (WhileTrue s s'' s') |
|
197 |
have "b t" using WhileTrue by (simp add: ball_Un)(blast dest:dep_on) |
|
198 |
then obtain t'' where tt'': "\<langle>bury c (Dep b \<union> A \<union> L c A),t\<rangle> \<longrightarrow>\<^sub>c t''" |
|
199 |
and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
200 |
using WhileTrue(6,7) by auto |
|
201 |
have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
202 |
using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(7) |
|
203 |
by (auto simp:L_gen_kill) |
|
204 |
then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
|
205 |
then show ?case |
|
206 |
using WhileTrue(5) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
207 |
qed } |
|
208 |
from this[OF IH(3) IH(4,2)] show ?case by metis |
|
28867 | 209 |
qed |
210 |
||
211 |
||
28583 | 212 |
end |