src/HOL/IMP/Live.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45212 e87feee00a4c child 45770 5d35cb2c0f02 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (* Author: Tobias Nipkow *)
3 header "Live Variable Analysis"
5 theory Live imports Vars Big_Step
6 begin
8 subsection "Liveness Analysis"
10 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where
11 "L SKIP X = X" |
12 "L (x ::= a) X = X-{x} \<union> vars a" |
13 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" |
14 "L (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = vars b \<union> L c\<^isub>1 X \<union> L c\<^isub>2 X" |
15 "L (WHILE b DO c) X = vars b \<union> X \<union> L c X"
17 value "show (L (''y'' ::= V ''z''; ''x'' ::= Plus (V ''y'') (V ''z'')) {''x''})"
19 value "show (L (WHILE Less (V ''x'') (V ''x'') DO ''y'' ::= V ''z'') {''x''})"
21 fun "kill" :: "com \<Rightarrow> vname set" where
22 "kill SKIP = {}" |
23 "kill (x ::= a) = {x}" |
24 "kill (c\<^isub>1; c\<^isub>2) = kill c\<^isub>1 \<union> kill c\<^isub>2" |
25 "kill (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = kill c\<^isub>1 \<inter> kill c\<^isub>2" |
26 "kill (WHILE b DO c) = {}"
28 fun gen :: "com \<Rightarrow> vname set" where
29 "gen SKIP = {}" |
30 "gen (x ::= a) = vars a" |
31 "gen (c\<^isub>1; c\<^isub>2) = gen c\<^isub>1 \<union> (gen c\<^isub>2 - kill c\<^isub>1)" |
32 "gen (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> gen c\<^isub>1 \<union> gen c\<^isub>2" |
33 "gen (WHILE b DO c) = vars b \<union> gen c"
35 lemma L_gen_kill: "L c X = (X - kill c) \<union> gen c"
36 by(induct c arbitrary:X) auto
38 lemma L_While_subset: "L c (L (WHILE b DO c) X) \<subseteq> L (WHILE b DO c) X"
39 by(auto simp add:L_gen_kill)
42 subsection "Soundness"
44 theorem L_sound:
45   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
46   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
47 proof (induction arbitrary: X t rule: big_step_induct)
48   case Skip then show ?case by auto
49 next
50   case Assign then show ?case
51     by (auto simp: ball_Un)
52 next
53   case (Semi c1 s1 s2 c2 s3 X t1)
54   from Semi.IH(1) Semi.prems obtain t2 where
55     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
56     by simp blast
57   from Semi.IH(2)[OF s2t2] obtain t3 where
58     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
59     by auto
60   show ?case using t12 t23 s3t3 by auto
61 next
62   case (IfTrue b s c1 s' c2)
63   hence "s = t on vars b" "s = t on L c1 X" by auto
64   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
65   from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
66     "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto
67   thus ?case using `bval b t` by auto
68 next
69   case (IfFalse b s c2 s' c1)
70   hence "s = t on vars b" "s = t on L c2 X" by auto
71   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
72   from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
73     "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto
74   thus ?case using `~bval b t` by auto
75 next
76   case (WhileFalse b s c)
77   hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
78   thus ?case using WhileFalse(2) by auto
79 next
80   case (WhileTrue b s1 c s2 s3 X t1)
81   let ?w = "WHILE b DO c"
82   from `bval b s1` WhileTrue(6) have "bval b t1"
83     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
84   have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
85     by (blast)
86   from WhileTrue.IH(1)[OF this] obtain t2 where
87     "(c, t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
88   from WhileTrue.IH(2)[OF this(2)] obtain t3 where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
89     by auto
90   with `bval b t1` `(c, t1) \<Rightarrow> t2` show ?case by auto
91 qed
94 subsection "Program Optimization"
96 text{* Burying assignments to dead variables: *}
97 fun bury :: "com \<Rightarrow> vname set \<Rightarrow> com" where
98 "bury SKIP X = SKIP" |
99 "bury (x ::= a) X = (if x:X then x::= a else SKIP)" |
100 "bury (c\<^isub>1; c\<^isub>2) X = (bury c\<^isub>1 (L c\<^isub>2 X); bury c\<^isub>2 X)" |
101 "bury (IF b THEN c\<^isub>1 ELSE c\<^isub>2) X = IF b THEN bury c\<^isub>1 X ELSE bury c\<^isub>2 X" |
102 "bury (WHILE b DO c) X = WHILE b DO bury c (vars b \<union> X \<union> L c X)"
104 text{* We could prove the analogous lemma to @{thm[source]L_sound}, and the
105 proof would be very similar. However, we phrase it as a semantics
106 preservation property: *}
108 theorem bury_sound:
109   "(c,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
110   \<exists> t'. (bury c X,t) \<Rightarrow> t' & s' = t' on X"
111 proof (induction arbitrary: X t rule: big_step_induct)
112   case Skip then show ?case by auto
113 next
114   case Assign then show ?case
115     by (auto simp: ball_Un)
116 next
117   case (Semi c1 s1 s2 c2 s3 X t1)
118   from Semi.IH(1) Semi.prems obtain t2 where
119     t12: "(bury c1 (L c2 X), t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X"
120     by simp blast
121   from Semi.IH(2)[OF s2t2] obtain t3 where
122     t23: "(bury c2 X, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
123     by auto
124   show ?case using t12 t23 s3t3 by auto
125 next
126   case (IfTrue b s c1 s' c2)
127   hence "s = t on vars b" "s = t on L c1 X" by auto
128   from  bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
129   from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where
130     "(bury c1 X, t) \<Rightarrow> t'" "s' =t' on X" by auto
131   thus ?case using `bval b t` by auto
132 next
133   case (IfFalse b s c2 s' c1)
134   hence "s = t on vars b" "s = t on L c2 X" by auto
135   from  bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
136   from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where
137     "(bury c2 X, t) \<Rightarrow> t'" "s' = t' on X" by auto
138   thus ?case using `~bval b t` by auto
139 next
140   case (WhileFalse b s c)
141   hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
142   thus ?case using WhileFalse(2) by auto
143 next
144   case (WhileTrue b s1 c s2 s3 X t1)
145   let ?w = "WHILE b DO c"
146   from `bval b s1` WhileTrue(6) have "bval b t1"
147     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
148   have "s1 = t1 on L c (L ?w X)"
149     using L_While_subset WhileTrue.prems by blast
150   from WhileTrue.IH(1)[OF this] obtain t2 where
151     "(bury c (L ?w X), t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
152   from WhileTrue.IH(2)[OF this(2)] obtain t3
153     where "(bury ?w X,t2) \<Rightarrow> t3" "s3 = t3 on X"
154     by auto
155   with `bval b t1` `(bury c (L ?w X), t1) \<Rightarrow> t2` show ?case by auto
156 qed
158 corollary final_bury_sound: "(c,s) \<Rightarrow> s' \<Longrightarrow> (bury c UNIV,s) \<Rightarrow> s'"
159 using bury_sound[of c s s' UNIV]
160 by (auto simp: fun_eq_iff[symmetric])
162 text{* Now the opposite direction. *}
164 lemma SKIP_bury[simp]:
165   "SKIP = bury c X \<longleftrightarrow> c = SKIP | (EX x a. c = x::=a & x \<notin> X)"
166 by (cases c) auto
168 lemma Assign_bury[simp]: "x::=a = bury c X \<longleftrightarrow> c = x::=a & x : X"
169 by (cases c) auto
171 lemma Semi_bury[simp]: "bc\<^isub>1;bc\<^isub>2 = bury c X \<longleftrightarrow>
172   (EX c\<^isub>1 c\<^isub>2. c = c\<^isub>1;c\<^isub>2 & bc\<^isub>2 = bury c\<^isub>2 X & bc\<^isub>1 = bury c\<^isub>1 (L c\<^isub>2 X))"
173 by (cases c) auto
175 lemma If_bury[simp]: "IF b THEN bc1 ELSE bc2 = bury c X \<longleftrightarrow>
176   (EX c1 c2. c = IF b THEN c1 ELSE c2 &
177      bc1 = bury c1 X & bc2 = bury c2 X)"
178 by (cases c) auto
180 lemma While_bury[simp]: "WHILE b DO bc' = bury c X \<longleftrightarrow>
181   (EX c'. c = WHILE b DO c' & bc' = bury c' (vars b \<union> X \<union> L c X))"
182 by (cases c) auto
184 theorem bury_sound2:
185   "(bury c X,s) \<Rightarrow> s'  \<Longrightarrow> s = t on L c X \<Longrightarrow>
186   \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X"
187 proof (induction "bury c X" s s' arbitrary: c X t rule: big_step_induct)
188   case Skip then show ?case by auto
189 next
190   case Assign then show ?case
191     by (auto simp: ball_Un)
192 next
193   case (Semi bc1 s1 s2 bc2 s3 c X t1)
194   then obtain c1 c2 where c: "c = c1;c2"
195     and bc2: "bc2 = bury c2 X" and bc1: "bc1 = bury c1 (L c2 X)" by auto
196   note IH = Semi.hyps(2,4)
197   from IH(1)[OF bc1, of t1] Semi.prems c obtain t2 where
198     t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" by auto
199   from IH(2)[OF bc2 s2t2] obtain t3 where
200     t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X"
201     by auto
202   show ?case using c t12 t23 s3t3 by auto
203 next
204   case (IfTrue b s bc1 s' bc2)
205   then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
206     and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
207   have "s = t on vars b" "s = t on L c1 X" using IfTrue.prems c by auto
208   from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp
209   note IH = IfTrue.hyps(3)
210   from IH[OF bc1 `s = t on L c1 X`] obtain t' where
211     "(c1, t) \<Rightarrow> t'" "s' =t' on X" by auto
212   thus ?case using c `bval b t` by auto
213 next
214   case (IfFalse b s bc2 s' bc1)
215   then obtain c1 c2 where c: "c = IF b THEN c1 ELSE c2"
216     and bc1: "bc1 = bury c1 X" and bc2: "bc2 = bury c2 X" by auto
217   have "s = t on vars b" "s = t on L c2 X" using IfFalse.prems c by auto
218   from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp
219   note IH = IfFalse.hyps(3)
220   from IH[OF bc2 `s = t on L c2 X`] obtain t' where
221     "(c2, t) \<Rightarrow> t'" "s' =t' on X" by auto
222   thus ?case using c `~bval b t` by auto
223 next
224   case (WhileFalse b s c)
225   hence "~ bval b t" by (auto simp: ball_Un dest: bval_eq_if_eq_on_vars)
226   thus ?case using WhileFalse by auto
227 next
228   case (WhileTrue b s1 bc' s2 s3 c X t1)
229   then obtain c' where c: "c = WHILE b DO c'"
230     and bc': "bc' = bury c' (vars b \<union> X \<union> L c' X)" by auto
231   let ?w = "WHILE b DO c'"
232   from `bval b s1` WhileTrue.prems c have "bval b t1"
233     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
234   note IH = WhileTrue.hyps(3,5)
235   have "s1 = t1 on L c' (L ?w X)"
236     using L_While_subset WhileTrue.prems c by blast
237   with IH(1)[OF bc', of t1] obtain t2 where
238     "(c', t1) \<Rightarrow> t2" "s2 = t2 on L ?w X" by auto
239   from IH(2)[OF WhileTrue.hyps(6), of t2] c this(2) obtain t3
240     where "(?w,t2) \<Rightarrow> t3" "s3 = t3 on X"
241     by auto
242   with `bval b t1` `(c', t1) \<Rightarrow> t2` c show ?case by auto
243 qed
245 corollary final_bury_sound2: "(bury c UNIV,s) \<Rightarrow> s' \<Longrightarrow> (c,s) \<Rightarrow> s'"
246 using bury_sound2[of c UNIV]
247 by (auto simp: fun_eq_iff[symmetric])
249 corollary bury_iff: "(bury c UNIV,s) \<Rightarrow> s' \<longleftrightarrow> (c,s) \<Rightarrow> s'"
250 by(metis final_bury_sound final_bury_sound2)
252 end