|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Live_True |
|
4 imports "~~/src/HOL/Library/While_Combinator" Vars Big_Step |
|
5 begin |
|
6 |
|
7 subsection "True Liveness Analysis" |
|
8 |
|
9 fun L :: "com \<Rightarrow> vname set \<Rightarrow> vname set" where |
|
10 "L SKIP X = X" | |
|
11 "L (x ::= a) X = (if x:X then X-{x} \<union> vars a else X)" | |
|
12 "L (c\<^isub>1; c\<^isub>2) X = (L c\<^isub>1 \<circ> L c\<^isub>2) X" | |
|
13 "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" | |
|
14 "L (WHILE b DO c) X = lfp(%Y. vars b \<union> X \<union> L c Y)" |
|
15 |
|
16 lemma L_mono: "mono (L c)" |
|
17 proof- |
|
18 { fix X Y have "X \<subseteq> Y \<Longrightarrow> L c X \<subseteq> L c Y" |
|
19 proof(induction c arbitrary: X Y) |
|
20 case (While b c) |
|
21 show ?case |
|
22 proof(simp, rule lfp_mono) |
|
23 fix Z show "vars b \<union> X \<union> L c Z \<subseteq> vars b \<union> Y \<union> L c Z" |
|
24 using While by auto |
|
25 qed |
|
26 next |
|
27 case If thus ?case by(auto simp: subset_iff) |
|
28 qed auto |
|
29 } thus ?thesis by(rule monoI) |
|
30 qed |
|
31 |
|
32 lemma mono_union_L: |
|
33 "mono (%Y. X \<union> L c Y)" |
|
34 by (metis (no_types) L_mono mono_def order_eq_iff set_eq_subset sup_mono) |
|
35 |
|
36 lemma L_While_unfold: |
|
37 "L (WHILE b DO c) X = vars b \<union> X \<union> L c (L (WHILE b DO c) X)" |
|
38 by(metis lfp_unfold[OF mono_union_L] L.simps(5)) |
|
39 |
|
40 |
|
41 subsection "Soundness" |
|
42 |
|
43 theorem L_sound: |
|
44 "(c,s) \<Rightarrow> s' \<Longrightarrow> s = t on L c X \<Longrightarrow> |
|
45 \<exists> t'. (c,t) \<Rightarrow> t' & s' = t' on X" |
|
46 proof (induction arbitrary: X t rule: big_step_induct) |
|
47 case Skip then show ?case by auto |
|
48 next |
|
49 case Assign then show ?case |
|
50 by (auto simp: ball_Un) |
|
51 next |
|
52 case (Semi c1 s1 s2 c2 s3 X t1) |
|
53 from Semi.IH(1) Semi.prems obtain t2 where |
|
54 t12: "(c1, t1) \<Rightarrow> t2" and s2t2: "s2 = t2 on L c2 X" |
|
55 by simp blast |
|
56 from Semi.IH(2)[OF s2t2] obtain t3 where |
|
57 t23: "(c2, t2) \<Rightarrow> t3" and s3t3: "s3 = t3 on X" |
|
58 by auto |
|
59 show ?case using t12 t23 s3t3 by auto |
|
60 next |
|
61 case (IfTrue b s c1 s' c2) |
|
62 hence "s = t on vars b" "s = t on L c1 X" by auto |
|
63 from bval_eq_if_eq_on_vars[OF this(1)] IfTrue(1) have "bval b t" by simp |
|
64 from IfTrue(3)[OF `s = t on L c1 X`] obtain t' where |
|
65 "(c1, t) \<Rightarrow> t'" "s' = t' on X" by auto |
|
66 thus ?case using `bval b t` by auto |
|
67 next |
|
68 case (IfFalse b s c2 s' c1) |
|
69 hence "s = t on vars b" "s = t on L c2 X" by auto |
|
70 from bval_eq_if_eq_on_vars[OF this(1)] IfFalse(1) have "~bval b t" by simp |
|
71 from IfFalse(3)[OF `s = t on L c2 X`] obtain t' where |
|
72 "(c2, t) \<Rightarrow> t'" "s' = t' on X" by auto |
|
73 thus ?case using `~bval b t` by auto |
|
74 next |
|
75 case (WhileFalse b s c) |
|
76 hence "~ bval b t" |
|
77 by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars) |
|
78 thus ?case using WhileFalse.prems L_While_unfold[of b c X] 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.prems have "bval b t1" |
|
83 by (metis L_While_unfold UnI1 bval_eq_if_eq_on_vars) |
|
84 have "s1 = t1 on L c (L ?w X)" using L_While_unfold 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 |
|
92 |
|
93 |
|
94 instantiation com :: vars |
|
95 begin |
|
96 |
|
97 fun vars_com :: "com \<Rightarrow> vname set" where |
|
98 "vars SKIP = {}" | |
|
99 "vars (x::=e) = vars e" | |
|
100 "vars (c\<^isub>1; c\<^isub>2) = vars c\<^isub>1 \<union> vars c\<^isub>2" | |
|
101 "vars (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = vars b \<union> vars c\<^isub>1 \<union> vars c\<^isub>2" | |
|
102 "vars (WHILE b DO c) = vars b \<union> vars c" |
|
103 |
|
104 instance .. |
|
105 |
|
106 end |
|
107 |
|
108 lemma L_subset_vars: "L c X \<subseteq> vars c \<union> X" |
|
109 proof(induction c arbitrary: X) |
|
110 case (While b c) |
|
111 have "lfp(%Y. vars b \<union> X \<union> L c Y) \<subseteq> vars b \<union> vars c \<union> X" |
|
112 using While.IH[of "vars b \<union> vars c \<union> X"] |
|
113 by (auto intro!: lfp_lowerbound) |
|
114 thus ?case by simp |
|
115 qed auto |
|
116 |
|
117 lemma afinite[simp]: "finite(vars(a::aexp))" |
|
118 by (induction a) auto |
|
119 |
|
120 lemma bfinite[simp]: "finite(vars(b::bexp))" |
|
121 by (induction b) auto |
|
122 |
|
123 lemma cfinite[simp]: "finite(vars(c::com))" |
|
124 by (induction c) auto |
|
125 |
|
126 (* move to Inductive; call Kleene? *) |
|
127 lemma lfp_finite_iter: assumes "mono f" and "(f^^Suc k) bot = (f^^k) bot" |
|
128 shows "lfp f = (f^^k) bot" |
|
129 proof(rule antisym) |
|
130 show "lfp f \<le> (f^^k) bot" |
|
131 proof(rule lfp_lowerbound) |
|
132 show "f ((f^^k) bot) \<le> (f^^k) bot" using assms(2) by simp |
|
133 qed |
|
134 next |
|
135 show "(f^^k) bot \<le> lfp f" |
|
136 proof(induction k) |
|
137 case 0 show ?case by simp |
|
138 next |
|
139 case Suc |
|
140 from monoD[OF assms(1) Suc] lfp_unfold[OF assms(1)] |
|
141 show ?case by simp |
|
142 qed |
|
143 qed |
|
144 |
|
145 (* move to While_Combinator *) |
|
146 lemma while_option_stop2: |
|
147 "while_option b c s = Some t \<Longrightarrow> EX k. t = (c^^k) s \<and> \<not> b t" |
|
148 apply(simp add: while_option_def split: if_splits) |
|
149 by (metis (lam_lifting) LeastI_ex) |
|
150 (* move to While_Combinator *) |
|
151 lemma while_option_finite_subset_Some: fixes C :: "'a set" |
|
152 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
|
153 shows "\<exists>P. while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
|
154 proof(rule measure_while_option_Some[where |
|
155 f= "%A::'a set. card C - card A" and P= "%A. A \<subseteq> C \<and> A \<subseteq> f A" and s= "{}"]) |
|
156 fix A assume A: "A \<subseteq> C \<and> A \<subseteq> f A" "f A \<noteq> A" |
|
157 show "(f A \<subseteq> C \<and> f A \<subseteq> f (f A)) \<and> card C - card (f A) < card C - card A" |
|
158 (is "?L \<and> ?R") |
|
159 proof |
|
160 show ?L by(metis A(1) assms(2) monoD[OF `mono f`]) |
|
161 show ?R by (metis A assms(2,3) card_seteq diff_less_mono2 equalityI linorder_le_less_linear rev_finite_subset) |
|
162 qed |
|
163 qed simp |
|
164 (* move to While_Combinator *) |
|
165 lemma lfp_eq_while_option: |
|
166 assumes "mono f" and "!!X. X \<subseteq> C \<Longrightarrow> f X \<subseteq> C" and "finite C" |
|
167 shows "lfp f = the(while_option (\<lambda>A. f A \<noteq> A) f {})" |
|
168 proof- |
|
169 obtain P where "while_option (\<lambda>A. f A \<noteq> A) f {} = Some P" |
|
170 using while_option_finite_subset_Some[OF assms] by blast |
|
171 with while_option_stop2[OF this] lfp_finite_iter[OF assms(1)] |
|
172 show ?thesis by auto |
|
173 qed |
|
174 |
|
175 text{* For code generation: *} |
|
176 lemma L_While: fixes b c X |
|
177 assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A" |
|
178 shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r") |
|
179 proof - |
|
180 let ?V = "vars b \<union> vars c \<union> X" |
|
181 have "lfp f = ?r" |
|
182 proof(rule lfp_eq_while_option[where C = "?V"]) |
|
183 show "mono f" by(simp add: f_def mono_union_L) |
|
184 next |
|
185 fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V" |
|
186 unfolding f_def using L_subset_vars[of c] by blast |
|
187 next |
|
188 show "finite ?V" using `finite X` by simp |
|
189 qed |
|
190 thus ?thesis by (simp add: f_def) |
|
191 qed |
|
192 |
|
193 text{* An approximate computation of the WHILE-case: *} |
|
194 |
|
195 fun iter :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
196 where |
|
197 "iter f 0 p d = d" | |
|
198 "iter f (Suc n) p d = (if f p = p then p else iter f n (f p) d)" |
|
199 |
|
200 lemma iter_pfp: |
|
201 "f d \<le> d \<Longrightarrow> mono f \<Longrightarrow> x \<le> f x \<Longrightarrow> f(iter f i x d) \<le> iter f i x d" |
|
202 apply(induction i arbitrary: x) |
|
203 apply simp |
|
204 apply (simp add: mono_def) |
|
205 done |
|
206 |
|
207 lemma iter_While_pfp: |
|
208 fixes b c X W k f |
|
209 defines "f == \<lambda>A. vars b \<union> X \<union> L c A" and "W == vars b \<union> vars c \<union> X" |
|
210 and "P == iter f k {} W" |
|
211 shows "f P \<subseteq> P" |
|
212 proof- |
|
213 have "f W \<subseteq> W" unfolding f_def W_def using L_subset_vars[of c] by blast |
|
214 have "mono f" by(simp add: f_def mono_union_L) |
|
215 from iter_pfp[of f, OF `f W \<subseteq> W` `mono f` empty_subsetI] |
|
216 show ?thesis by(simp add: P_def) |
|
217 qed |
|
218 |
|
219 end |