121 by (induction b) auto |
121 by (induction b) auto |
122 |
122 |
123 lemma cfinite[simp]: "finite(vars(c::com))" |
123 lemma cfinite[simp]: "finite(vars(c::com))" |
124 by (induction c) auto |
124 by (induction c) auto |
125 |
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 (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: *} |
126 text{* For code generation: *} |
176 lemma L_While: fixes b c X |
127 lemma L_While: fixes b c X |
177 assumes "finite X" defines "f == \<lambda>A. vars b \<union> X \<union> L c A" |
128 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") |
129 shows "L (WHILE b DO c) X = the(while_option (\<lambda>A. f A \<noteq> A) f {})" (is "_ = ?r") |
179 proof - |
130 proof - |
180 let ?V = "vars b \<union> vars c \<union> X" |
131 let ?V = "vars b \<union> vars c \<union> X" |
181 have "lfp f = ?r" |
132 have "lfp f = ?r" |
182 proof(rule lfp_eq_while_option[where C = "?V"]) |
133 proof(rule lfp_the_while_option[where C = "?V"]) |
183 show "mono f" by(simp add: f_def mono_union_L) |
134 show "mono f" by(simp add: f_def mono_union_L) |
184 next |
135 next |
185 fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V" |
136 fix Y show "Y \<subseteq> ?V \<Longrightarrow> f Y \<subseteq> ?V" |
186 unfolding f_def using L_subset_vars[of c] by blast |
137 unfolding f_def using L_subset_vars[of c] by blast |
187 next |
138 next |