195 |
195 |
196 |
196 |
197 locale Measure1 = |
197 locale Measure1 = |
198 fixes m :: "'av::order \<Rightarrow> nat" |
198 fixes m :: "'av::order \<Rightarrow> nat" |
199 fixes h :: "nat" |
199 fixes h :: "nat" |
200 assumes m1: "x \<le> y \<Longrightarrow> m x \<ge> m y" |
|
201 assumes h: "m x \<le> h" |
200 assumes h: "m x \<le> h" |
202 begin |
201 begin |
203 |
202 |
204 definition m_s :: "'av st \<Rightarrow> nat" ("m\<^isub>s") where |
203 definition m_s :: "'av st \<Rightarrow> nat" ("m\<^isub>s") where |
205 "m_s S = (\<Sum> x \<in> dom S. m(fun S x))" |
204 "m_s S = (\<Sum> x \<in> dom S. m(fun S x))" |
206 |
205 |
207 lemma m_s_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_s x \<le> h * card X" |
206 lemma m_s_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_s x \<le> h * card X" |
208 by(simp add: L_st_def m_s_def) |
207 by(simp add: L_st_def m_s_def) |
209 (metis nat_mult_commute of_nat_id setsum_bounded[OF h]) |
208 (metis nat_mult_commute of_nat_id setsum_bounded[OF h]) |
210 |
209 |
211 lemma m_s1: "S1 \<le> S2 \<Longrightarrow> m_s S1 \<ge> m_s S2" |
|
212 proof(auto simp add: less_eq_st_def m_s_def) |
|
213 assume "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x" |
|
214 hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1) |
|
215 thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))" |
|
216 by (metis setsum_mono) |
|
217 qed |
|
218 |
|
219 definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where |
210 definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" ("m\<^isub>o") where |
220 "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_s S)" |
211 "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_s S)" |
221 |
212 |
222 lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)" |
213 lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)" |
223 by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h) |
214 by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h) |
224 |
|
225 lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow> |
|
226 o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2" |
|
227 proof(induction o1 o2 rule: less_eq_option.induct) |
|
228 case 1 thus ?case by (simp add: m_o_def)(metis m_s1) |
|
229 next |
|
230 case 2 thus ?case |
|
231 by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits) |
|
232 next |
|
233 case 3 thus ?case by simp |
|
234 qed |
|
235 |
215 |
236 definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where |
216 definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where |
237 "m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))" |
217 "m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))" |
238 |
218 |
239 lemma m_c_h: assumes "C \<in> L(vars(strip C))" |
219 lemma m_c_h: assumes "C \<in> L(vars(strip C))" |
255 |
235 |
256 locale Measure = Measure1 + |
236 locale Measure = Measure1 + |
257 assumes m2: "x < y \<Longrightarrow> m x > m y" |
237 assumes m2: "x < y \<Longrightarrow> m x > m y" |
258 begin |
238 begin |
259 |
239 |
|
240 lemma m1: "x \<le> y \<Longrightarrow> m x \<ge> m y" |
|
241 by(auto simp: le_less m2) |
|
242 |
260 lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2" |
243 lemma m_s2: "finite(dom S1) \<Longrightarrow> S1 < S2 \<Longrightarrow> m_s S1 > m_s S2" |
261 proof(auto simp add: less_st_def less_eq_st_def m_s_def) |
244 proof(auto simp add: less_st_def less_eq_st_def m_s_def) |
262 assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x" |
245 assume "finite(dom S2)" and 0: "\<forall>x\<in>dom S2. fun S1 x \<le> fun S2 x" |
263 hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1) |
246 hence 1: "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m1) |
264 fix x assume "x \<in> dom S2" "\<not> fun S2 x \<le> fun S1 x" |
247 fix x assume "x \<in> dom S2" "\<not> fun S2 x \<le> fun S1 x" |
275 case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h) |
258 case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h) |
276 next |
259 next |
277 case 3 thus ?case by (auto simp: less_option_def) |
260 case 3 thus ?case by (auto simp: less_option_def) |
278 qed |
261 qed |
279 |
262 |
280 find_theorems "(_<_) = _" |
263 lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow> |
|
264 o1 \<le> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2" |
|
265 by(auto simp: le_less m_o2) |
|
266 |
281 lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow> |
267 lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow> |
282 C1 < C2 \<Longrightarrow> m_c C1 > m_c C2" |
268 C1 < C2 \<Longrightarrow> m_c C1 > m_c C2" |
283 proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] less_acom_def L_acom_def) |
269 proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] less_acom_def L_acom_def) |
284 let ?X = "vars(strip C2)" |
270 let ?X = "vars(strip C2)" |
285 let ?n = "card ?X" |
271 let ?n = "card ?X" |