src/HOL/IMP/Abs_Int3.thy

 
 begin
 
 definition "m_st S = (SUM x:dom S. m(fun S x))"
 
-lemma h_st: assumes "finite X" and "dom S \<subseteq> X"
-shows "m_st S \<le> h * card X"
-proof(auto simp: m_st_def)
-  have "(\<Sum>x\<in>dom S. m (fun S x)) \<le> (\<Sum>x\<in>dom S. h)" (is "?L \<le> _")
-    by(rule setsum_mono)(simp add: m_height)
-  also have "\<dots> \<le> (\<Sum>x\<in>X. h)"
-    by(rule setsum_mono3[OF assms]) simp
-  also have "\<dots> = h * card X" by simp
-  finally show "?L \<le> \<dots>" .
-qed
-
-
-(* FIXME identical *)
+lemma m_st_h: "x \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_st x \<le> h * card X"
+by(simp add: L_st_def m_st_def)
+  (metis nat_mult_commute of_nat_id setsum_bounded[OF m_height])
+
 lemma m_st_anti_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st S1 \<ge> m_st S2"
 proof(auto simp add: le_st_def m_st_def)
   assume "\<forall>x\<in>dom S2. fun S1 x \<sqsubseteq> fun S2 x"
   hence "\<forall>x\<in>dom S2. m(fun S1 x) \<ge> m(fun S2 x)" by (metis m_anti_mono)
   thus "(\<Sum>x\<in>dom S2. m (fun S2 x)) \<le> (\<Sum>x\<in>dom S2. m (fun S1 x))"

     apply(rule setsum_strict_mono_ex1[OF `finite(dom S1)`]) using 1 2 by blast+
   moreover have "dom (S1 \<triangle> S2) = dom S1" by(simp add: narrow_st_def)
   ultimately show ?thesis by(simp add: n_st_def)
 qed
 
-
-definition "m_o k opt = (case opt of None \<Rightarrow> k+1 | Some x \<Rightarrow> m_st x)"
+definition m_o :: "nat \<Rightarrow> 'av st option \<Rightarrow> nat" where
+"m_o d opt = (case opt of None \<Rightarrow> h*d+1 | Some S \<Rightarrow> m_st S)"
+
+lemma m_o_h: "ost \<in> L X \<Longrightarrow> finite X \<Longrightarrow> m_o (card X) ost \<le> (h*card X + 1)"
+by(auto simp add: m_o_def m_st_h split: option.split dest!:m_st_h)
 
 lemma m_o_anti_mono: "S1 \<in> L X \<Longrightarrow> S2 \<in> L X \<Longrightarrow> finite X \<Longrightarrow>
-  S1 \<sqsubseteq> S2 \<Longrightarrow> m_o (h * card X) S2 \<le> m_o (h * card X) S1"
+  S1 \<sqsubseteq> S2 \<Longrightarrow> m_o (card X) S2 \<le> m_o (card X) S1"
 apply(induction S1 S2 rule: le_option.induct)
-apply(auto simp: m_o_def m_st_anti_mono le_SucI h_st L_st_def
+apply(auto simp: m_o_def m_st_anti_mono le_SucI m_st_h L_st_def
            split: option.splits)
 done
 
 lemma m_o_widen: "\<lbrakk> S1 \<in> L X; S2 \<in> L X; finite X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
-  m_o (h * card X) (S1 \<nabla> S2) < m_o (h * card X) S1"
-by(auto simp: m_o_def L_st_def h_st less_Suc_eq_le m_st_widen
+  m_o (card X) (S1 \<nabla> S2) < m_o (card X) S1"
+by(auto simp: m_o_def L_st_def m_st_h less_Suc_eq_le m_st_widen
         split: option.split)
 
 definition "n_o opt = (case opt of None \<Rightarrow> 0 | Some x \<Rightarrow> n_st x + 1)"
 
 lemma n_o_mono: "S1 \<sqsubseteq> S2 \<Longrightarrow> n_o S1 \<le> n_o S2"

 by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" C1 C2 rule: map2_acom.induct)
   (simp_all add: narrow_acom_def size_annos_same2)
 
 
 definition "m_c C = (let as = annos C in
-  \<Sum>i=0..<size as. m_o (h * card(vars(strip C))) (as!i))"
+  \<Sum>i<size as. m_o (card(vars(strip C))) (as!i))"
+
+lemma m_c_h: assumes "C \<in> L(vars(strip C))"
+shows "m_c C \<le> size(annos C) * (h * card(vars(strip C)) + 1)"
+proof-
+  let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"
+  { fix i assume "i < ?a"
+    hence "annos C ! i \<in> L ?X" using assms by(simp add: L_acom_def)
+    note m_o_h[OF this finite_cvars]
+  } note 1 = this
+  have "m_c C = (\<Sum>i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def Let_def)
+  also have "\<dots> \<le> (\<Sum>i<?a. h * ?n + 1)"
+    apply(rule setsum_mono) using 1 by simp
+  also have "\<dots> = ?a * (h * ?n + 1)" by simp
+  finally show ?thesis .
+qed
 
 lemma m_c_widen:
   "C1 \<in> Lc c \<Longrightarrow> C2 \<in> Lc c \<Longrightarrow> \<not> C2 \<sqsubseteq> C1 \<Longrightarrow> m_c (C1 \<nabla> C2) < m_c C1"
 apply(auto simp: Lc_acom_def m_c_def Let_def widen_acom_def)
 apply(subgoal_tac "length(annos C2) = length(annos C1)")

 apply simp
 apply (clarsimp)
 apply(rule n_o_mono)
 apply(rule narrow2)
 apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
-apply(auto simp: le_iff_le_annos listrel_iff_nth strip_narrow_acom)
+apply(auto simp: le_iff_le_annos listrel_iff_nth)
 apply(rule_tac x=i in bexI)
 prefer 2 apply simp
 apply(rule n_o_narrow[where X = "vars(strip C1)"])
 apply (simp add: finite_cvars)+
 done

 next
   show "P C" by(rule `P C`)
 next
   fix C assume "P C" thus "P (C \<nabla> f C)" by(simp add: P_f P_widen)
 qed
-thm mono_step'(*FIXME does not need wt assms*)
+
 lemma iter_narrow_termination:
 fixes n :: "'a::WN_Lc \<Rightarrow> nat"
 assumes P_f: "\<And>C. P C \<Longrightarrow> P(f C)"
 and P_narrow: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> P(C1 \<triangle> C2)"
 and mono: "\<And>C1 C2. P C1 \<Longrightarrow> P C2 \<Longrightarrow> C1 \<sqsubseteq> C2 \<Longrightarrow> f C1 \<sqsubseteq> f C2"