simplified def

--- a/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:41:45 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Apr 26 09:53:11 2013 +0200
@@ -121,13 +121,14 @@
 by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)
 
 definition m_c :: "'av st option acom \<Rightarrow> nat" ("m\<^isub>c") where
-"m_c C = (\<Sum>i<size(annos C). m_o (vars C) (annos C ! i))"
+"m_c C = listsum (map (m_o (vars C)) (annos C))"
 
 text{* Upper complexity bound: *}
 lemma m_c_h: "m_c C \<le> size(annos C) * (h * card(vars C) + 1)"
 proof-
   let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
-  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))" by(simp add: m_c_def)
+  have "m_c C = (\<Sum>i<?a. m_o ?X (annos C ! i))"
+    by(simp add: m_c_def listsum_setsum_nth atLeast0LessThan)
   also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
     apply(rule setsum_mono) using m_o_h[OF finite_Cvars] by simp
   also have "\<dots> = ?a * (h * ?n + 1)" by simp
@@ -220,7 +221,7 @@
 
 lemma m_c2: "top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2) \<Longrightarrow>
   C1 < C2 \<Longrightarrow> m_c C1 > m_c C2"
-proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] vars_acom_def less_acom_def)
+proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
   let ?X = "vars(strip C2)"
   assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
   and strip_eq: "strip C1 = strip C2"
@@ -236,9 +237,11 @@
   from i have "m_o ?X (annos C1 ! i) > m_o ?X (annos C2 ! i)" (is "?P i")
     by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
   hence 2: "\<exists>i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
-  show "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
+  have "(\<Sum>i<size(annos C2). m_o ?X (annos C2 ! i))
          < (\<Sum>i<size(annos C2). m_o ?X (annos C1 ! i))"
     apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
+  thus ?thesis
+    by(simp add: m_c_def vars_acom_def strip_eq listsum_setsum_nth atLeast0LessThan size_annos_same[OF strip_eq])
 qed
 
 end

--- a/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 09:41:45 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy	Fri Apr 26 09:53:11 2013 +0200
@@ -398,7 +398,7 @@
 lemma m_c_widen:
   "strip C1 = strip C2  \<Longrightarrow> top_on_acom C1 (-vars C1) \<Longrightarrow> top_on_acom C2 (-vars C2)
    \<Longrightarrow> \<not> C2 \<le> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
-apply(auto simp: m_c_def widen_acom_def)
+apply(auto simp: m_c_def widen_acom_def listsum_setsum_nth atLeast0LessThan)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")
  prefer 2 apply (simp add: size_annos_same2)
 apply (auto)