equal
deleted
inserted
replaced
315 |
315 |
316 definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>s") where |
316 definition m_s :: "'av st \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>s") where |
317 "m_s S X = (\<Sum> x \<in> X. m(S x))" |
317 "m_s S X = (\<Sum> x \<in> X. m(S x))" |
318 |
318 |
319 lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X" |
319 lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X" |
320 by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h]) |
320 by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h]) |
321 |
321 |
322 fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where |
322 fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where |
323 "m_o (Some S) X = m_s S X" | |
323 "m_o (Some S) X = m_s S X" | |
324 "m_o None X = h * card X + 1" |
324 "m_o None X = h * card X + 1" |
325 |
325 |