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" |
|
11 by(rule_tac x="%x. UNIV" in exI)(simp add: fun_eq_iff[symmetric]) |
|
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 |
|
95 have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
96 using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` `\<langle>c,t\<rangle> \<longrightarrow>\<^sub>c t''`] WhileTrue(6,8) |
|
97 by (auto simp:L_gen_kill) |
|
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 |
|
100 qed auto } |
|
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 |
|
122 qed |
|
123 |
|
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''" |
|
178 and "\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'" |
|
179 using WhileTrue(6,7) by auto |
|
180 have "\<forall>x\<in>Dep b \<union> A \<union> L c A. s'' x = t'' x" |
|
181 using IH(1)[OF _ `\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s''` tt''] WhileTrue(6,8) |
|
182 by (auto simp:L_gen_kill) |
|
183 moreover then have "\<forall>x\<in>L (While b c) A. s'' x = t'' x" by auto |
|
184 ultimately show ?case |
|
185 using WhileTrue(5,6) `\<langle>bury (While b c) A,t''\<rangle> \<longrightarrow>\<^sub>c t'` by metis |
|
186 qed auto } |
|
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 |
|
209 qed |
|
210 |
|
211 |
|
212 end |
|