simplified def
authornipkow
Fri Apr 26 07:49:38 2013 +0200 (2013-04-26)
changeset 51783f4a00cdae743
parent 51782 84e7225f5ab6
child 51784 89fb9f4abf84
simplified def
src/HOL/IMP/Abs_Int0.thy
     1.1 --- a/src/HOL/IMP/Abs_Int0.thy	Thu Apr 25 19:18:20 2013 +0200
     1.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Fri Apr 26 07:49:38 2013 +0200
     1.3 @@ -323,13 +323,14 @@
     1.4  by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)
     1.5  
     1.6  definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
     1.7 -"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
     1.8 +"m_c C = listsum (map (m_o (vars C)) (annos C))"
     1.9  
    1.10  text{* Upper complexity bound: *}
    1.11  lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
    1.12  proof-
    1.13    let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
    1.14 -  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
    1.15 +  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))"
    1.16 +    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
    1.17    also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
    1.18      apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
    1.19    also have "\<dots> = ?a * (h * ?n + 1)" by simp
    1.20 @@ -436,7 +437,7 @@
    1.21  
    1.22  lemma m_c2: "top_on_acom (-vars C1) C1 \<Longrightarrow> top_on_acom (-vars C2) C2 \<Longrightarrow>
    1.23    C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
    1.24 -proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
    1.25 +proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
    1.26    let ?X = "vars(strip C2)"
    1.27    assume top: "top_on_acom (- vars(strip C2)) C1"  "top_on_acom (- vars(strip C2)) C2"
    1.28    and strip_eq: "strip C1 = strip C2"
    1.29 @@ -452,9 +453,11 @@
    1.30    from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
    1.31      by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
    1.32    hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
    1.33 -  show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
    1.34 +  have "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
    1.35           < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
    1.36      apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
    1.37 +  thus ?thesis
    1.38 +    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
    1.39  qed
    1.40  
    1.41  end