[STATEMENT]
lemma n_ivl_narrow:
  "~ x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl(x \<triangle> y) < n_ivl x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> x \<sqsubseteq> x \<triangle> y \<Longrightarrow> n_ivl (x \<triangle> y) < n_ivl x
[PROOF STEP]
by(auto simp: n_ivl_def m_ivl_def narrow_ivl_def le_option_def le_ivl_def
        split: ivl.splits option.splits if_splits)


[STATEMENT]
lemma m_st_height: assumes "finite X" and "set (dom S) \<subseteq> X"
shows "m_st m_ivl S \<le> 2 * card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_st m_ivl S \<le> 2 * card X
[PROOF STEP]
proof(auto simp: m_st_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
have "(\<Sum>x\<in>set(dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set(dom S). 2)" (is "?L \<le> _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S). 2)
[PROOF STEP]
by(rule sum_mono)(simp add:m_ivl_height)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S). 2)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S). 2)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
have "\<dots> \<le> (\<Sum>x\<in>X. 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). 2) \<le> (\<Sum>x\<in>X. 2)
[PROOF STEP]
by(rule sum_mono2[OF assms]) simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S). 2) \<le> (\<Sum>x\<in>X. 2)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S). 2) \<le> (\<Sum>x\<in>X. 2)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
have "\<dots> = 2 * card X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. 2) = 2 * card X
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. 2) = 2 * card X

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
show "?L \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S). m_ivl (fun S x)) \<le> 2 * card X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m_st_anti_mono:
  "S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S1 \<sqsubseteq> S2 \<Longrightarrow> m_st m_ivl S2 \<le> m_st m_ivl S1
[PROOF STEP]
proof(auto simp: m_st_def le_st_def lookup_def split: if_splits)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
let ?X = "set(dom S1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
let ?Y = "set(dom S2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
let ?f = "fun S1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
let ?g = "fun S2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
assume asm: "\<forall>x\<in>?Y. (x \<in> ?X \<longrightarrow> ?f x \<sqsubseteq> ?g x) \<and> (x \<in> ?X \<or> \<top> \<sqsubseteq> ?g x)"
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x)

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
hence 1: "\<forall>y\<in>?Y\<inter>?X. m_ivl(?g y) \<le> m_ivl(?f y)"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x)

goal (1 subgoal):
 1. \<forall>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y) \<le> m_ivl (fun S1 y)
[PROOF STEP]
by(simp add: m_ivl_anti_mono)
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y) \<le> m_ivl (fun S1 y)

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have 0: "\<forall>x\<in>?Y-?X. m_ivl(?g x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. m_ivl (fun S2 x)) = \<lambda>x. 0 on set (Abs_State.dom S2) - set (Abs_State.dom S1)
[PROOF STEP]
using asm
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x)

goal (1 subgoal):
 1. (\<lambda>x. m_ivl (fun S2 x)) = \<lambda>x. 0 on set (Abs_State.dom S2) - set (Abs_State.dom S1)
[PROOF STEP]
by (auto simp: Top_less_ivl)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. m_ivl (fun S2 x)) = \<lambda>x. 0 on set (Abs_State.dom S2) - set (Abs_State.dom S1)

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "(\<Sum>y\<in>?Y. m_ivl(?g y)) = (\<Sum>y\<in>(?Y-?X) \<union> (?Y\<inter>?X). m_ivl(?g y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))
[PROOF STEP]
by (metis Un_Diff_Int)
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> = (\<Sum>y\<in>?Y-?X. m_ivl(?g y)) + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))
[PROOF STEP]
by(subst sum.union_disjoint) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1) \<union> set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "(\<Sum>y\<in>?Y-?X. m_ivl(?g y)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) = 0
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. m_ivl (fun S2 x)) = \<lambda>x. 0 on set (Abs_State.dom S2) - set (Abs_State.dom S1)

goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) = 0

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) - set (Abs_State.dom S1). m_ivl (fun S2 y)) = 0

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "0 + (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y)) = (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?g y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 + (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) = (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> \<le> (\<Sum>y\<in>?Y\<inter>?X. m_ivl(?f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S1 y))
[PROOF STEP]
by(rule sum_mono)(simp add: 1)
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S1 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S2 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S1 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> \<le> (\<Sum>y\<in>?X. m_ivl(?f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S1 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S1). m_ivl (fun S1 y))
[PROOF STEP]
by(simp add: sum_mono2[of "?X" "?Y Int ?X", OF _ Int_lower2])
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2) \<inter> set (Abs_State.dom S1). m_ivl (fun S1 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S1). m_ivl (fun S1 y))

goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S2). (x \<in> set (Abs_State.dom S1) \<longrightarrow> fun S1 x \<sqsubseteq> fun S2 x) \<and> (x \<in> set (Abs_State.dom S1) \<or> \<top> \<sqsubseteq> fun S2 x) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S2). m_ivl (fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S1). m_ivl (fun S1 y))
[PROOF STEP]
show "(\<Sum>y\<in>?Y. m_ivl(?g y)) \<le> (\<Sum>x\<in>?X. m_ivl(?f x))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) \<le> (\<Sum>y\<in>set (Abs_State.dom S1). m_ivl (fun S1 y))

goal (1 subgoal):
 1. (\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>set (Abs_State.dom S2). m_ivl (fun S2 y)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m_st_widen:
assumes "\<not> S2 \<sqsubseteq> S1" shows "m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
let ?X = "set(dom S1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
let ?Y = "set(dom S2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
let ?f = "fun S1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
let ?g = "fun S2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
assume "x \<in> ?X" "\<not> lookup S2 x \<sqsubseteq> ?f x"
[PROOF STATE]
proof (state)
this:
x \<in> set (Abs_State.dom S1)
\<not> lookup S2 x \<sqsubseteq> fun S1 x

goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
have "(\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x)) < (\<Sum>x\<in>?X. m_ivl(?f x))" (is "?L < ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
 2. \<not> ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
assume "x : ?Y"
[PROOF STATE]
proof (state)
this:
x \<in> set (Abs_State.dom S2)

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
 2. \<not> ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "?L < (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))
[PROOF STEP]
proof(rule sum_strict_mono_ex1, simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
 2. \<exists>a\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 a \<nabla> fun S2 a) < m_ivl (fun S1 a)
[PROOF STEP]
show "\<forall>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
[PROOF STEP]
by (metis m_ivl_anti_mono widen1)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)

goal (1 subgoal):
 1. \<exists>a\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 a \<nabla> fun S2 a) < m_ivl (fun S1 a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 a \<nabla> fun S2 a) < m_ivl (fun S1 a)
[PROOF STEP]
show "\<exists>x\<in>?X\<inter>?Y. m_ivl(?f x \<nabla> ?g x) < m_ivl(?f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) < m_ivl (fun S1 x)
[PROOF STEP]
using \<open>x:?X\<close> \<open>x:?Y\<close> \<open>\<not> lookup S2 x \<sqsubseteq> ?f x\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> set (Abs_State.dom S1)
x \<in> set (Abs_State.dom S2)
\<not> lookup S2 x \<sqsubseteq> fun S1 x

goal (1 subgoal):
 1. \<exists>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) < m_ivl (fun S1 x)
[PROOF STEP]
by (metis IntI m_ivl_widen lookup_def)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x) < m_ivl (fun S1 x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
 2. \<not> ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
 2. \<not> ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> \<le> ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
by(simp add: sum_mono2[OF _ Int_lower1])
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (2 subgoals):
 1. ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
 2. \<not> ?P \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
assume "x ~: ?Y"
[PROOF STATE]
proof (state)
this:
x \<notin> set (Abs_State.dom S2)

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "?L \<le> (\<Sum>x\<in>?X\<inter>?Y. m_ivl(?f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))
[PROOF STEP]
proof(rule sum_mono, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (Abs_State.dom S1) \<and> x \<in> set (Abs_State.dom S2) \<Longrightarrow> m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (Abs_State.dom S1) \<and> x \<in> set (Abs_State.dom S2) \<Longrightarrow> m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
[PROOF STEP]
assume "x:?X \<and> x:?Y"
[PROOF STATE]
proof (state)
this:
x \<in> set (Abs_State.dom S1) \<and> x \<in> set (Abs_State.dom S2)

goal (1 subgoal):
 1. \<And>x. x \<in> set (Abs_State.dom S1) \<and> x \<in> set (Abs_State.dom S2) \<Longrightarrow> m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
[PROOF STEP]
show "m_ivl(?f x \<nabla> ?g x) \<le> m_ivl (?f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)
[PROOF STEP]
by (metis m_ivl_anti_mono widen1)
[PROOF STATE]
proof (state)
this:
m_ivl (fun S1 x \<nabla> fun S2 x) \<le> m_ivl (fun S1 x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> < m_ivl(?f x) + \<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) < m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))
[PROOF STEP]
using m_ivl_widen[OF \<open>\<not> lookup S2 x \<sqsubseteq> ?f x\<close>]
[PROOF STATE]
proof (prove)
using this:
m_ivl (fun S1 x \<nabla> lookup S2 x) < m_ivl (fun S1 x)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) < m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))
[PROOF STEP]
by (metis Nat.le_refl add_strict_increasing gr0I not_less0)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) < m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) < m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> = (\<Sum>y\<in>insert x (?X\<inter>?Y). m_ivl(?f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) = (\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y))
[PROOF STEP]
using \<open>x ~: ?Y\<close>
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (Abs_State.dom S2)

goal (1 subgoal):
 1. m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) = (\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) = (\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
m_ivl (fun S1 x) + (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x)) = (\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
have "\<dots> \<le> (\<Sum>x\<in>?X. m_ivl(?f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
by(rule sum_mono2)(insert \<open>x:?X\<close>, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>y\<in>insert x (set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2)). m_ivl (fun S1 y)) \<le> (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. x \<notin> set (Abs_State.dom S2) \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2 \<in> set (Abs_State.dom S1); \<not> lookup S2 ?x2 \<sqsubseteq> fun S1 ?x2\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<not> S2 \<sqsubseteq> S1
\<lbrakk>?x2 \<in> set (Abs_State.dom S1); \<not> lookup S2 ?x2 \<sqsubseteq> fun S1 ?x2\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> S2 \<sqsubseteq> S1
\<lbrakk>?x2 \<in> set (Abs_State.dom S1); \<not> lookup S2 ?x2 \<sqsubseteq> fun S1 ?x2\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (Abs_State.dom S1) \<inter> set (Abs_State.dom S2). m_ivl (fun S1 x \<nabla> fun S2 x)) < (\<Sum>x\<in>set (Abs_State.dom S1). m_ivl (fun S1 x))

goal (1 subgoal):
 1. m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1
[PROOF STEP]
by(auto simp: le_st_def widen_st_def m_st_def Int_def)
[PROOF STATE]
proof (state)
this:
m_st m_ivl (S1 \<nabla> S2) < m_st m_ivl S1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_st_mono: assumes "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X" "S1 \<sqsubseteq> S2"
shows "n_st n_ivl X S1 \<le> n_st n_ivl X S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_st n_ivl X S1 \<le> n_st n_ivl X S2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n_st n_ivl X S1 \<le> n_st n_ivl X S2
[PROOF STEP]
have "(\<Sum>x\<in>X. n_ivl(lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl(lookup S2 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. n_ivl (lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl (lookup S2 x))
[PROOF STEP]
apply(rule sum_mono)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> n_ivl (lookup S1 x) \<le> n_ivl (lookup S2 x)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set (Abs_State.dom S1) \<subseteq> X
set (Abs_State.dom S2) \<subseteq> X
S1 \<sqsubseteq> S2

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> n_ivl (lookup S1 x) \<le> n_ivl (lookup S2 x)
[PROOF STEP]
by(auto simp: le_st_def lookup_def n_ivl_mono split: if_splits)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. n_ivl (lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl (lookup S2 x))

goal (1 subgoal):
 1. n_st n_ivl X S1 \<le> n_st n_ivl X S2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>X. n_ivl (lookup S1 x)) \<le> (\<Sum>x\<in>X. n_ivl (lookup S2 x))

goal (1 subgoal):
 1. n_st n_ivl X S1 \<le> n_st n_ivl X S2
[PROOF STEP]
by(simp add: n_st_def)
[PROOF STATE]
proof (state)
this:
n_st n_ivl X S1 \<le> n_st n_ivl X S2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma n_st_narrow:
assumes "finite X" and "set(dom S1) \<subseteq> X" "set(dom S2) \<subseteq> X"
and "S2 \<sqsubseteq> S1" "\<not> S1 \<sqsubseteq> S1 \<triangle> S2"
shows "n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
have 1: "\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)
[PROOF STEP]
using assms(2-4)
[PROOF STATE]
proof (prove)
using this:
set (Abs_State.dom S1) \<subseteq> X
set (Abs_State.dom S2) \<subseteq> X
S2 \<sqsubseteq> S1

goal (1 subgoal):
 1. \<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)
[PROOF STEP]
by(auto simp: le_st_def narrow_st_def lookup_def n_ivl_mono narrow2
            split: if_splits)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)

goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
have 2: "\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)
[PROOF STEP]
using assms(2-5)
[PROOF STATE]
proof (prove)
using this:
set (Abs_State.dom S1) \<subseteq> X
set (Abs_State.dom S2) \<subseteq> X
S2 \<sqsubseteq> S1
\<not> S1 \<sqsubseteq> S1 \<triangle> S2

goal (1 subgoal):
 1. \<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)
[PROOF STEP]
by(auto simp: le_st_def narrow_st_def lookup_def intro: n_ivl_narrow
            split: if_splits)
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)

goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
have "(\<Sum>x\<in>X. n_ivl(lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl(lookup S1 x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl (lookup S1 x))
[PROOF STEP]
apply(rule sum_strict_mono_ex1[OF \<open>finite X\<close>])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)
 2. \<exists>a\<in>X. n_ivl (lookup (S1 \<triangle> S2) a) < n_ivl (lookup S1 a)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)
\<exists>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) < n_ivl (lookup S1 x)

goal (2 subgoals):
 1. \<forall>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x) \<le> n_ivl (lookup S1 x)
 2. \<exists>a\<in>X. n_ivl (lookup (S1 \<triangle> S2) a) < n_ivl (lookup S1 a)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl (lookup S1 x))

goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<in>X. n_ivl (lookup (S1 \<triangle> S2) x)) < (\<Sum>x\<in>X. n_ivl (lookup S1 x))

goal (1 subgoal):
 1. n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1
[PROOF STEP]
by(simp add: n_st_def)
[PROOF STATE]
proof (state)
this:
n_st n_ivl X (S1 \<triangle> S2) < n_st n_ivl X S1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m_o_anti_mono: "finite X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow>
  m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; domo S2 \<subseteq> X; S1 \<sqsubseteq> S2\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) S2 \<le> m_o (m_st m_ivl) (2 * card X) S1
[PROOF STEP]
apply(induction S1 S2 rule: le_option.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>finite X; domo (Some y) \<subseteq> X; Some x \<sqsubseteq> Some y\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (Some y) \<le> m_o (m_st m_ivl) (2 * card X) (Some x)
 2. \<And>y. \<lbrakk>finite X; domo y \<subseteq> X; None \<sqsubseteq> y\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) y \<le> m_o (m_st m_ivl) (2 * card X) None
 3. \<And>uu_. \<lbrakk>finite X; domo None \<subseteq> X; Some uu_ \<sqsubseteq> None\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) None \<le> m_o (m_st m_ivl) (2 * card X) (Some uu_)
[PROOF STEP]
apply(auto simp: domo_def m_o_def m_st_anti_mono le_SucI m_st_height
           split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma m_o_widen: "\<lbrakk> finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1 \<rbrakk> \<Longrightarrow>
  m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; domo S2 \<subseteq> X; \<not> S2 \<sqsubseteq> S1\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (S1 \<nabla> S2) < m_o (m_st m_ivl) (2 * card X) S1
[PROOF STEP]
by(auto simp: m_o_def domo_def m_st_height less_Suc_eq_le m_st_widen
        split: option.split)


[STATEMENT]
lemma n_o_mono: "domo S1 \<subseteq> X \<Longrightarrow> domo S2 \<subseteq> X \<Longrightarrow> S1 \<sqsubseteq> S2 \<Longrightarrow>
  n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>domo S1 \<subseteq> X; domo S2 \<subseteq> X; S1 \<sqsubseteq> S2\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) S1 \<le> n_o (n_st n_ivl X) S2
[PROOF STEP]
apply(induction S1 S2 rule: le_option.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>domo (Some x) \<subseteq> X; domo (Some y) \<subseteq> X; Some x \<sqsubseteq> Some y\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (Some x) \<le> n_o (n_st n_ivl X) (Some y)
 2. \<And>y. \<lbrakk>domo None \<subseteq> X; domo y \<subseteq> X; None \<sqsubseteq> y\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) None \<le> n_o (n_st n_ivl X) y
 3. \<And>uu_. \<lbrakk>domo (Some uu_) \<subseteq> X; domo None \<subseteq> X; Some uu_ \<sqsubseteq> None\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (Some uu_) \<le> n_o (n_st n_ivl X) None
[PROOF STEP]
apply(auto simp: domo_def n_o_def n_st_mono
           split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma n_o_narrow:
  "\<lbrakk> finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2 \<rbrakk>
  \<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite X; domo S1 \<subseteq> X; domo S2 \<subseteq> X; S2 \<sqsubseteq> S1; \<not> S1 \<sqsubseteq> S1 \<triangle> S2\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (S1 \<triangle> S2) < n_o (n_st n_ivl X) S1
[PROOF STEP]
apply(induction S1 S2 rule: narrow_option.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>finite X; domo None \<subseteq> X; domo x \<subseteq> X; x \<sqsubseteq> None; \<not> None \<sqsubseteq> None \<triangle> x\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (None \<triangle> x) < n_o (n_st n_ivl X) None
 2. \<And>v. \<lbrakk>finite X; domo (Some v) \<subseteq> X; domo None \<subseteq> X; None \<sqsubseteq> Some v; \<not> Some v \<sqsubseteq> Some v \<triangle> None\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (Some v \<triangle> None) < n_o (n_st n_ivl X) (Some v)
 3. \<And>x y. \<lbrakk>finite X; domo (Some x) \<subseteq> X; domo (Some y) \<subseteq> X; Some y \<sqsubseteq> Some x; \<not> Some x \<sqsubseteq> Some x \<triangle> Some y\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (Some x \<triangle> Some y) < n_o (n_st n_ivl X) (Some x)
[PROOF STEP]
apply(auto simp: n_o_def domo_def n_st_narrow)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domo_widen_subset: "domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domo (S1 \<nabla> S2) \<subseteq> domo S1 \<union> domo S2
[PROOF STEP]
apply(induction S1 S2 rule: widen_option.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. domo (None \<nabla> x) \<subseteq> domo None \<union> domo x
 2. \<And>v. domo (Some v \<nabla> None) \<subseteq> domo (Some v) \<union> domo None
 3. \<And>x y. domo (Some x \<nabla> Some y) \<subseteq> domo (Some x) \<union> domo (Some y)
[PROOF STEP]
apply (auto simp: domo_def widen_st_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma domo_narrow_subset: "domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. domo (S1 \<triangle> S2) \<subseteq> domo S1 \<union> domo S2
[PROOF STEP]
apply(induction S1 S2 rule: narrow_option.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. domo (None \<triangle> x) \<subseteq> domo None \<union> domo x
 2. \<And>v. domo (Some v \<triangle> None) \<subseteq> domo (Some v) \<union> domo None
 3. \<And>x y. domo (Some x \<triangle> Some y) \<subseteq> domo (Some x) \<union> domo (Some y)
[PROOF STEP]
apply (auto simp: domo_def narrow_st_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma strip_widen_acom[simp]:
  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<nabla>\<^sub>c c') = strip c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c' = strip c \<Longrightarrow> strip (c \<nabla>\<^sub>c c') = strip c
[PROOF STEP]
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all


[STATEMENT]
lemma strip_narrow_acom[simp]:
  "strip c' = strip (c::'a::WN acom) \<Longrightarrow>  strip (c \<triangle>\<^sub>c c') = strip c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c' = strip c \<Longrightarrow> strip (c \<triangle>\<^sub>c c') = strip c
[PROOF STEP]
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c c' rule: map2_acom.induct) simp_all


[STATEMENT]
lemma annos_widen_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
  annos(c1 \<nabla>\<^sub>c c2) = map (%(x,y).x\<nabla>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c1 = strip c2 \<Longrightarrow> annos (c1 \<nabla>\<^sub>c c2) = map2 (\<nabla>) (annos c1) (annos c2)
[PROOF STEP]
by(induction "widen::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
  (simp_all add: size_annos_same2)


[STATEMENT]
lemma annos_narrow_acom[simp]: "strip c1 = strip (c2::'a::WN acom) \<Longrightarrow>
  annos(c1 \<triangle>\<^sub>c c2) = map (%(x,y).x\<triangle>y) (zip (annos c1) (annos(c2::'a::WN acom)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c1 = strip c2 \<Longrightarrow> annos (c1 \<triangle>\<^sub>c c2) = map2 (\<triangle>) (annos c1) (annos c2)
[PROOF STEP]
by(induction "narrow::'a\<Rightarrow>'a\<Rightarrow>'a" c1 c2 rule: map2_acom.induct)
  (simp_all add: size_annos_same2)


[STATEMENT]
lemma widen_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
  c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<nabla>\<^sub>c c2) : Com X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strip c2 = strip c1; c1 \<in> Com X; c2 \<in> Com X\<rbrakk> \<Longrightarrow> c1 \<nabla>\<^sub>c c2 \<in> Com X
[PROOF STEP]
apply(auto simp add: Com_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; (a, b) \<in> set (zip (annos c1) (annos c2)); x \<in> domo (a \<nabla> b)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(rename_tac S S' x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; (S, S') \<in> set (zip (annos c1) (annos c2)); x \<in> domo (S \<nabla> S')\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(erule in_set_zipE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; x \<in> domo (S \<nabla> S'); S \<in> set (annos c1); S' \<in> set (annos c2)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(auto simp: domo_def split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = Some a\<rbrakk> \<Longrightarrow> x \<in> X
 3. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = Some a\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a aa. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = Some aa\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2 a aa. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<nabla> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = Some aa\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply (fastforce simp: widen_st_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma narrow_acom_Com[simp]: "strip c2 = strip c1 \<Longrightarrow>
  c1 : Com X \<Longrightarrow> c2 : Com X \<Longrightarrow> (c1 \<triangle>\<^sub>c c2) : Com X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>strip c2 = strip c1; c1 \<in> Com X; c2 \<in> Com X\<rbrakk> \<Longrightarrow> c1 \<triangle>\<^sub>c c2 \<in> Com X
[PROOF STEP]
apply(auto simp add: Com_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; (a, b) \<in> set (zip (annos c1) (annos c2)); x \<in> domo (a \<triangle> b)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(rename_tac S S' x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; (S, S') \<in> set (zip (annos c1) (annos c2)); x \<in> domo (S \<triangle> S')\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(erule in_set_zipE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x. \<lbrakk>strip c2 = strip c1; \<forall>S\<in>set (annos c1). domo S \<subseteq> X; \<forall>S\<in>set (annos c2). domo S \<subseteq> X; x \<in> domo (S \<triangle> S'); S \<in> set (annos c1); S' \<in> set (annos c2)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(auto simp: domo_def split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2)\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S')
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>S S' x x2. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = Some a\<rbrakk> \<Longrightarrow> x \<in> X
 3. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = None; S' = Some a\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply(case_tac S')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>S S' x x2 a. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = None\<rbrakk> \<Longrightarrow> x \<in> X
 2. \<And>S S' x x2 a aa. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = Some aa\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>S S' x x2 a aa. \<lbrakk>S \<in> set (annos c1); S' \<in> set (annos c2); strip c2 = strip c1; \<forall>S\<in>set (annos c1). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; \<forall>S\<in>set (annos c2). \<forall>x2. S = Some x2 \<longrightarrow> set (Abs_State.dom x2) \<subseteq> X; S \<triangle> S' = Some x2; x \<in> set (Abs_State.dom x2); S = Some a; S' = Some aa\<rbrakk> \<Longrightarrow> x \<in> X
[PROOF STEP]
apply (fastforce simp: narrow_st_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma measure_m_c: "finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'::ivl st option acom.
     strip c' = strip c \<and> c : Com X \<and> c' : Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse>
    \<subseteq> measure(m_c(m_o (m_st m_ivl) (2*card(X))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X \<Longrightarrow> {(c, c \<nabla>\<^sub>c c') |c c'. strip c' = strip c \<and> c \<in> Com X \<and> c' \<in> Com X \<and> \<not> c' \<sqsubseteq> c}\<inverse> \<subseteq> measure (m_c (m_o (m_st m_ivl) (2 * card X)))
[PROOF STEP]
apply(auto simp: m_c_def Let_def Com_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). m_o (m_st m_ivl) (2 * card X) (annos c ! i \<nabla> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i))
[PROOF STEP]
apply(subgoal_tac "length(annos c') = length(annos c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). m_o (m_st m_ivl) (2 * card X) (annos c ! i \<nabla> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i))
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c\<rbrakk> \<Longrightarrow> length (annos c') = length (annos c)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c\<rbrakk> \<Longrightarrow> length (annos c') = length (annos c)
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). m_o (m_st m_ivl) (2 * card X) (annos c ! i \<nabla> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i))
[PROOF STEP]
apply (simp add: size_annos_same2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). m_o (m_st m_ivl) (2 * card X) (annos c ! i \<nabla> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i \<nabla> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). m_o (m_st m_ivl) (2 * card X) (annos c ! i))
[PROOF STEP]
apply(rule sum_strict_mono_ex1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> finite {0..<length (annos c)}
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<forall>x\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! x \<nabla> annos c' ! x) \<le> m_o (m_st m_ivl) (2 * card X) (annos c ! x)
 3. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<forall>x\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! x \<nabla> annos c' ! x) \<le> m_o (m_st m_ivl) (2 * card X) (annos c ! x)
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (annos c ! x \<nabla> annos c' ! x) \<le> m_o (m_st m_ivl) (2 * card X) (annos c ! x)
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply(erule m_o_anti_mono)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c' x. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x \<nabla> annos c' ! x) \<subseteq> X
 2. \<And>c c' x. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<sqsubseteq> annos c ! x \<nabla> annos c' ! x
 3. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply(rule subset_trans[OF domo_widen_subset])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c' x. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x) \<union> domo (annos c' ! x) \<subseteq> X
 2. \<And>c c' x. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<sqsubseteq> annos c ! x \<nabla> annos c' ! x
 3. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' x. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<sqsubseteq> annos c ! x \<nabla> annos c' ! x
 2. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply(rule widen1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<not> c' \<sqsubseteq> c; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply(auto simp: le_iff_le_annos listrel_iff_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. m_o (m_st m_ivl) (2 * card X) (annos c ! a \<nabla> annos c' ! a) < m_o (m_st m_ivl) (2 * card X) (annos c ! a)
[PROOF STEP]
apply(rule_tac x=n in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (annos c ! n \<nabla> annos c' ! n) < m_o (m_st m_ivl) (2 * card X) (annos c ! n)
 2. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> n \<in> {0..<length (annos c)}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> n \<in> {0..<length (annos c)}
 2. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (annos c ! n \<nabla> annos c' ! n) < m_o (m_st m_ivl) (2 * card X) (annos c ! n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c' n. \<lbrakk>finite X; strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> m_o (m_st m_ivl) (2 * card X) (annos c ! n \<nabla> annos c' ! n) < m_o (m_st m_ivl) (2 * card X) (annos c ! n)
[PROOF STEP]
apply(erule m_o_widen)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' n. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> domo (annos c' ! n) \<subseteq> X
 2. \<And>c c' n. \<lbrakk>strip c' = strip c; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; length (annos c') = length (annos c); n < length (annos c); \<not> annos c' ! n \<sqsubseteq> annos c ! n\<rbrakk> \<Longrightarrow> \<not> annos c' ! n \<sqsubseteq> annos c ! n
[PROOF STEP]
apply (simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma measure_n_c: "finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'.
  strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse>
  \<subseteq> measure(m_c(n_o (n_st n_ivl X)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X \<Longrightarrow> {(c, c \<triangle>\<^sub>c c') |c c'. strip c = strip c' \<and> c \<in> Com X \<and> c' \<in> Com X \<and> c' \<sqsubseteq> c \<and> \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'}\<inverse> \<subseteq> measure (m_c (n_o (n_st n_ivl X)))
[PROOF STEP]
apply(auto simp: m_c_def Let_def Com_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). n_o (n_st n_ivl X) (annos c ! i \<triangle> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i))
[PROOF STEP]
apply(subgoal_tac "length(annos c') = length(annos c)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). n_o (n_st n_ivl X) (annos c ! i \<triangle> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i))
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'\<rbrakk> \<Longrightarrow> length (annos c') = length (annos c)
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'\<rbrakk> \<Longrightarrow> length (annos c') = length (annos c)
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). n_o (n_st n_ivl X) (annos c ! i \<triangle> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i))
[PROOF STEP]
apply (simp add: size_annos_same2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<min (length (annos c)) (length (annos c')). n_o (n_st n_ivl X) (annos c ! i \<triangle> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i))
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i \<triangle> annos c' ! i)) < (\<Sum>i = 0..<length (annos c). n_o (n_st n_ivl X) (annos c ! i))
[PROOF STEP]
apply(rule sum_strict_mono_ex1)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> finite {0..<length (annos c)}
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<forall>x\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! x \<triangle> annos c' ! x) \<le> n_o (n_st n_ivl X) (annos c ! x)
 3. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<forall>x\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! x \<triangle> annos c' ! x) \<le> n_o (n_st n_ivl X) (annos c ! x)
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply (clarsimp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (annos c ! x \<triangle> annos c' ! x) \<le> n_o (n_st n_ivl X) (annos c ! x)
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply(rule n_o_mono)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x \<triangle> annos c' ! x) \<subseteq> X
 2. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x) \<subseteq> X
 3. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<triangle> annos c' ! x \<sqsubseteq> annos c ! x
 4. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
using domo_narrow_subset
[PROOF STATE]
proof (prove)
using this:
domo (?S1.0 \<triangle> ?S2.0) \<subseteq> domo ?S1.0 \<union> domo ?S2.0

goal (4 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x \<triangle> annos c' ! x) \<subseteq> X
 2. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x) \<subseteq> X
 3. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<triangle> annos c' ! x \<sqsubseteq> annos c ! x
 4. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> domo (annos c ! x) \<subseteq> X
 2. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<triangle> annos c' ! x \<sqsubseteq> annos c ! x
 3. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c ! x \<triangle> annos c' ! x \<sqsubseteq> annos c ! x
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply(rule narrow2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' x. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c); x < length (annos c)\<rbrakk> \<Longrightarrow> annos c' ! x \<sqsubseteq> annos c ! x
 2. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply(fastforce simp: le_iff_le_annos listrel_iff_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c'. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; c' \<sqsubseteq> c; \<not> c \<sqsubseteq> c \<triangle>\<^sub>c c'; length (annos c') = length (annos c)\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply(auto simp: le_iff_le_annos listrel_iff_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> \<exists>a\<in>{0..<length (annos c)}. n_o (n_st n_ivl X) (annos c ! a \<triangle> annos c' ! a) < n_o (n_st n_ivl X) (annos c ! a)
[PROOF STEP]
apply(rule_tac x=n in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (annos c ! n \<triangle> annos c' ! n) < n_o (n_st n_ivl X) (annos c ! n)
 2. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> n \<in> {0..<length (annos c)}
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> n \<in> {0..<length (annos c)}
 2. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (annos c ! n \<triangle> annos c' ! n) < n_o (n_st n_ivl X) (annos c ! n)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c c' n. \<lbrakk>finite X; strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> n_o (n_st n_ivl X) (annos c ! n \<triangle> annos c' ! n) < n_o (n_st n_ivl X) (annos c ! n)
[PROOF STEP]
apply(erule n_o_narrow)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>c c' n. \<lbrakk>strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> domo (annos c ! n) \<subseteq> X
 2. \<And>c c' n. \<lbrakk>strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> domo (annos c' ! n) \<subseteq> X
 3. \<And>c c' n. \<lbrakk>strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> annos c' ! n \<sqsubseteq> annos c ! n
 4. \<And>c c' n. \<lbrakk>strip c = strip c'; \<forall>S\<in>set (annos c). domo S \<subseteq> X; \<forall>S\<in>set (annos c'). domo S \<subseteq> X; \<forall>n<length (annos c). annos c' ! n \<sqsubseteq> annos c ! n; length (annos c') = length (annos c); n < length (annos c); \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n\<rbrakk> \<Longrightarrow> \<not> annos c ! n \<sqsubseteq> annos c ! n \<triangle> annos c' ! n
[PROOF STEP]
apply (simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma iter_widen_termination:
fixes c0 :: "'a::WN acom"
assumes P_f: "\<And>c. P c \<Longrightarrow> P(f c)"
assumes P_widen: "\<And>c c'. P c \<Longrightarrow> P c' \<Longrightarrow> P(c \<nabla>\<^sub>c c')"
and "wf({(c::'a acom,c \<nabla>\<^sub>c c')|c c'. P c \<and> P c' \<and> ~ c' \<sqsubseteq> c}^-1)"
and "P c0" and "c0 \<sqsubseteq> f c0" shows "\<exists>c. iter_widen f c0 = Some c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. iter_widen f c0 = Some c
[PROOF STEP]
proof(simp add: iter_widen_def, rule wf_while_option_Some[where P = "P"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. wf {(c, s). (P s \<and> \<not> f s \<sqsubseteq> s) \<and> c = s \<nabla>\<^sub>c f s}
 2. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
 3. P c0
[PROOF STEP]
show "wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}
[PROOF STEP]
apply(rule wf_subset[OF assms(3)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c} \<subseteq> {(c, c \<nabla>\<^sub>c c') |c c'. P c \<and> P c' \<and> \<not> c' \<sqsubseteq> c}\<inverse>
[PROOF STEP]
by(blast intro: P_f)
[PROOF STATE]
proof (state)
this:
wf {(cc', c). (P c \<and> \<not> f c \<sqsubseteq> c) \<and> cc' = c \<nabla>\<^sub>c f c}

goal (2 subgoals):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
 2. P c0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
 2. P c0
[PROOF STEP]
show "P c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P c0
[PROOF STEP]
by(rule \<open>P c0\<close>)
[PROOF STATE]
proof (state)
this:
P c0

goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
[PROOF STEP]
assume "P c"
[PROOF STATE]
proof (state)
this:
P c

goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<not> f s \<sqsubseteq> s\<rbrakk> \<Longrightarrow> P (s \<nabla>\<^sub>c f s)
[PROOF STEP]
thus "P (c \<nabla>\<^sub>c f c)"
[PROOF STATE]
proof (prove)
using this:
P c

goal (1 subgoal):
 1. P (c \<nabla>\<^sub>c f c)
[PROOF STEP]
by(simp add: P_f P_widen)
[PROOF STATE]
proof (state)
this:
P (c \<nabla>\<^sub>c f c)

goal:
No subgoals!
[PROOF STEP]
qed