1.1 --- a/src/HOL/IMP/Abs_Int1.thy	Mon Sep 17 21:33:12 2012 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Tue Sep 18 01:55:13 2012 +0200
     1.3 @@ -235,6 +235,10 @@
     1.4  
     1.5  definition "m_st S = (\<Sum> x \<in> dom S. m(fun S x))"
     1.6  
     1.7 +lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
     1.8 +by(simp add: L_st_def m_st_def)
     1.9 +  (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
    1.10 +
    1.11  lemma m_st1: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
    1.12  proof(auto simp add: le_st_def m_st_def)
    1.13    assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
    1.14 @@ -257,12 +261,8 @@
    1.15  definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
    1.16  "m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
    1.17  
    1.18 -definition m_c :: "'av st option acom \<Rightarrow> nat" where
    1.19 -"m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
    1.20 -
    1.21 -lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
    1.22 -by(simp add: L_st_def m_st_def)
    1.23 -  (metis nat_mult_commute of_nat_id setsum_bounded[OF h])
    1.24 +lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
    1.25 +by(auto simp add: m_o_def m_st_h split: option.split dest!:m_st_h)
    1.26  
    1.27  lemma m_o1: "finite X \<Longrightarrow> o1 \<in> L X \<Longrightarrow> o2 \<in> L X \<Longrightarrow>
    1.28    o1 \<sqsubseteq> o2 \<Longrightarrow> m_o (card X) o1 \<ge> m_o (card X) o2"
    1.29 @@ -286,6 +286,25 @@
    1.30    case 3 thus ?case by simp
    1.31  qed
    1.32  
    1.33 +
    1.34 +definition m_c :: "'av st option acom \<Rightarrow> nat" where
    1.35 +"m_c C = (\<Sum>i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"
    1.36 +
    1.37 +lemma m_c_h: assumes "C \<in> L(vars(strip C))"
    1.38 +shows "m_c C \<le> size(annos C) * (h * card(vars(strip C)) + 1)"
    1.39 +proof-
    1.40 +  let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"
    1.41 +  { fix i assume "i < ?a"
    1.42 +    hence "annos C ! i \<in> L ?X" using assms by(simp add: L_acom_def)
    1.43 +    note m_o_h[OF this finite_cvars]
    1.44 +  } note 1 = this
    1.45 +  have "m_c C = (\<Sum>i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def)
    1.46 +  also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    1.47 +    apply(rule setsum_mono) using 1 by simp
    1.48 +  also have "\<dots> = ?a * (h * ?n + 1)" by simp
    1.49 +  finally show ?thesis .
    1.50 +qed
    1.51 +
    1.52  lemma m_c2: "C1 \<in> L(vars(strip C1)) \<Longrightarrow> C2 \<in> L(vars(strip C2)) \<Longrightarrow>
    1.53    C1 \<sqsubset> C2 \<Longrightarrow> m_c C1 > m_c C2"
    1.54  proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] L_acom_def)