[STATEMENT]
lemma Ctxt_valid_validn: "\<Turnstile> G \<Longrightarrow> \<Turnstile>\<^sub>n G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Turnstile> G  \<Longrightarrow>  \<Turnstile>\<^sub>n G
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  \<Turnstile> G  \<Longrightarrow>  \<Turnstile>\<^sub>n G
[PROOF STEP]
apply (simp add: Ctxt_valid_def Ctxt_validn_def, clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m A. \<lbrakk>\<forall>A. A \<in> G \<longrightarrow>  \<Turnstile> Call : A ; m \<le> n; A \<in> G\<rbrakk> \<Longrightarrow>  \<Turnstile>\<^sub>m Call : A
[PROOF STEP]
apply (rule VDM_valid_validn)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m A. \<lbrakk>\<forall>A. A \<in> G \<longrightarrow>  \<Turnstile> Call : A ; m \<le> n; A \<in> G\<rbrakk> \<Longrightarrow>  \<Turnstile> Call : A
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma xeq4: assumes not_new: "x \<noteq> new s t"
  shows "s \<equiv>[x] s\<langle>t\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<equiv>[x] s\<langle>t\<rangle>
[PROOF STEP]
proof (rule xeqI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. alive x s = alive x (s\<langle>t\<rangle>)
 2. \<And>l. s\<turnstile> l reachable_from x \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
from not_new
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> new s t
[PROOF STEP]
show "alive x s = alive x (s\<langle>t\<rangle>)"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> new s t

goal (1 subgoal):
 1. alive x s = alive x (s\<langle>t\<rangle>)
[PROOF STEP]
by (simp add: alive_alloc_exhaust)
[PROOF STATE]
proof (state)
this:
alive x s = alive x (s\<langle>t\<rangle>)

goal (1 subgoal):
 1. \<And>l. s\<turnstile> l reachable_from x \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. s\<turnstile> l reachable_from x \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
fix l
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>l. s\<turnstile> l reachable_from x \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
assume reach_l: "s\<turnstile> l reachable_from x"
[PROOF STATE]
proof (state)
this:
s\<turnstile> l reachable_from x

goal (1 subgoal):
 1. \<And>l. s\<turnstile> l reachable_from x \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
show "s@@l = s\<langle>t\<rangle>@@l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
proof (cases "isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
 2. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)

goal (2 subgoals):
 1. isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
 2. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
with reach_l
[PROOF STATE]
proof (chain)
picking this:
s\<turnstile> l reachable_from x
isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s\<turnstile> l reachable_from x
isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)

goal (1 subgoal):
 1. s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s@@l = s\<langle>t\<rangle>@@l

goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t))

goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t))
[PROOF STEP]
obtain T n where t: "t = new_array T n" and
                          l: "l = arr_len (new s t)"
[PROOF STATE]
proof (prove)
using this:
\<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t))

goal (1 subgoal):
 1. (\<And>T n. \<lbrakk>t = new_array T n; l = arr_len (new s t)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t) auto
[PROOF STATE]
proof (state)
this:
t = new_array T n
l = arr_len (new s t)

goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
hence "ref l = new s t"
[PROOF STATE]
proof (prove)
using this:
t = new_array T n
l = arr_len (new s t)

goal (1 subgoal):
 1. ref l = new s t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ref l = new s t

goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
from this reach_l
[PROOF STATE]
proof (chain)
picking this:
ref l = new s t
s\<turnstile> l reachable_from x
[PROOF STEP]
have "x = new s t"
[PROOF STATE]
proof (prove)
using this:
ref l = new s t
s\<turnstile> l reachable_from x

goal (1 subgoal):
 1. x = new s t
[PROOF STEP]
by (rule loc_new_reach)
[PROOF STATE]
proof (state)
this:
x = new s t

goal (1 subgoal):
 1. \<not> (isNewArr t \<longrightarrow> l \<noteq> arr_len (new s t)) \<Longrightarrow> s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
with not_new
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> new s t
x = new s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> new s t
x = new s t

goal (1 subgoal):
 1. s@@l = s\<langle>t\<rangle>@@l
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s@@l = s\<langle>t\<rangle>@@l

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s@@l = s\<langle>t\<rangle>@@l

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R': "hd (tl R'_walk) \<leadsto>R'\<leadsto> z" "set R' \<subseteq> set (tl R'_walk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z &&& set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
have "tl R'_walk \<noteq> Nil"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tl R'_walk \<noteq> []
[PROOF STEP]
by (simp add: P_k_pre_not_Nil R'_walk_def)
[PROOF STATE]
proof (state)
this:
tl R'_walk \<noteq> []

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
tl R'_walk \<noteq> []

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
have "last R'_walk = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last R'_walk = z
[PROOF STEP]
unfolding R'_walk_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. last (P_k_pre @ R_pre @ [z]) = z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last R'_walk = z

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
last R'_walk = z

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
have "walk (tl R'_walk)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. walk (tl R'_walk)
[PROOF STEP]
by (metis (no_types, lifting) path_from_toE walk_tl H_def P_k_decomp R'_walk_def R(1)
          R_decomp path_P_k y_eq_new_last hd_append list.sel(1) list.simps(3) path_decomp'
          remove_vertex_path_from_to_add walk_comp walk_decomp(1) walk_last_edge)
[PROOF STATE]
proof (state)
this:
walk (tl R'_walk)

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
tl R'_walk \<noteq> []
last R'_walk = z
walk (tl R'_walk)
[PROOF STEP]
obtain R'' where "hd (tl R'_walk) \<leadsto>R''\<leadsto> z" "set R'' \<subseteq> set (tl R'_walk)"
[PROOF STATE]
proof (prove)
using this:
tl R'_walk \<noteq> []
last R'_walk = z
walk (tl R'_walk)

goal (1 subgoal):
 1. (\<And>R''. \<lbrakk>hd (tl R'_walk) \<leadsto>R''\<leadsto> z; set R'' \<subseteq> set (tl R'_walk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using walk_to_path[of "tl R'_walk" "hd (tl R'_walk)" z] last_tl
[PROOF STATE]
proof (prove)
using this:
tl R'_walk \<noteq> []
last R'_walk = z
walk (tl R'_walk)
\<lbrakk>walk (tl R'_walk); tl R'_walk \<noteq> []; hd (tl R'_walk) = hd (tl R'_walk); last (tl R'_walk) = z\<rbrakk> \<Longrightarrow> \<exists>ys. hd (tl R'_walk) \<leadsto>ys\<leadsto> z \<and> set ys \<subseteq> set (tl R'_walk)
?xs = [] \<or> tl ?xs \<noteq> [] \<Longrightarrow> last (tl ?xs) = last ?xs

goal (1 subgoal):
 1. (\<And>R''. \<lbrakk>hd (tl R'_walk) \<leadsto>R''\<leadsto> z; set R'' \<subseteq> set (tl R'_walk)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
hd (tl R'_walk) \<leadsto>R''\<leadsto> z
set R'' \<subseteq> set (tl R'_walk)

goal (2 subgoals):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z
 2. set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
hd (tl R'_walk) \<leadsto>R''\<leadsto> z
set R'' \<subseteq> set (tl R'_walk)
[PROOF STEP]
show "hd (tl R'_walk) \<leadsto>R'\<leadsto> z" "set R' \<subseteq> set (tl R'_walk)"
[PROOF STATE]
proof (prove)
using this:
hd (tl R'_walk) \<leadsto>R''\<leadsto> z
set R'' \<subseteq> set (tl R'_walk)

goal (1 subgoal):
 1. hd (tl R'_walk) \<leadsto>R'\<leadsto> z &&& set R' \<subseteq> set (tl R'_walk)
[PROOF STEP]
unfolding R'_def
[PROOF STATE]
proof (prove)
using this:
hd (tl R'_walk) \<leadsto>R''\<leadsto> z
set R'' \<subseteq> set (tl R'_walk)

goal (1 subgoal):
 1. hd (tl R'_walk) \<leadsto>(SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk))\<leadsto> z &&& set (SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk)) \<subseteq> set (tl R'_walk)
[PROOF STEP]
using someI[of "\<lambda>R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk)"]
[PROOF STATE]
proof (prove)
using this:
hd (tl R'_walk) \<leadsto>R''\<leadsto> z
set R'' \<subseteq> set (tl R'_walk)
hd (tl R'_walk) \<leadsto>?x\<leadsto> z \<and> set ?x \<subseteq> set (tl R'_walk) \<Longrightarrow> hd (tl R'_walk) \<leadsto>(SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk))\<leadsto> z \<and> set (SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk)) \<subseteq> set (tl R'_walk)

goal (1 subgoal):
 1. hd (tl R'_walk) \<leadsto>(SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk))\<leadsto> z &&& set (SOME R'. hd (tl R'_walk) \<leadsto>R'\<leadsto> z \<and> set R' \<subseteq> set (tl R'_walk)) \<subseteq> set (tl R'_walk)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hd (tl R'_walk) \<leadsto>R'\<leadsto> z
set R' \<subseteq> set (tl R'_walk)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_imp_inext_le: "\<lbrakk> a < b; a \<in> I; b \<in> I \<rbrakk> \<Longrightarrow> inext a I \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; a \<in> I; b \<in> I\<rbrakk> \<Longrightarrow> inext a I \<le> b
[PROOF STEP]
by (metis inext_min_step not_le)


[STATEMENT]
lemma iprev_less_mono_if_neq_iMin: "
  \<lbrakk> a < b; a \<in> I; b \<in> I; iMin I \<noteq> a \<rbrakk> \<Longrightarrow> iprev a I < iprev b I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; a \<in> I; b \<in> I; iMin I \<noteq> a\<rbrakk> \<Longrightarrow> iprev a I < iprev b I
[PROOF STEP]
by (metis iprev_in_iff iprev_less_mono iprev_mono2_if_neq_iMin)


[STATEMENT]
lemma map_Val_throw_eq:
 "map Val vs @ throw ex # es = map Val vs' @ throw ex' # es' \<Longrightarrow> ex = ex'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map Val vs @ throw ex # es = map Val vs' @ throw ex' # es' \<Longrightarrow> ex = ex'
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map Val vs @ throw ex # es = map Val vs' @ throw ex' # es' \<Longrightarrow> ex = ex'
[PROOF STEP]
by(induct vs arbitrary: vs'; case_tac vs') auto


[STATEMENT]
lemma map_vals_of_throw[simp]:
 "map_vals_of (map Val vs @ throw e # es') = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vals_of (map Val vs @ throw e # es') = None
[PROOF STEP]
by(induct vs, auto)


[STATEMENT]
lemma qdsnd_setsum:
  "finite A \<Longrightarrow> qdsnd (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. qdsnd (f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A \<Longrightarrow> qdsnd (sum f A) = (\<Sum>x\<in>A. qdsnd (f x))
[PROOF STEP]
by (induct A rule: finite_induct) (auto simp add: zero_QDelta_def plus_QDelta_def)


[STATEMENT]
lemma has_next_map_generator [simp]:
  "list.has_next (map_generator g) = list.has_next g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list.has_next (local.map_generator g) = list.has_next g
[PROOF STEP]
by transfer clarsimp


[STATEMENT]
lemma subtermeq_vars_subset: "M \<sqsubseteq> N \<Longrightarrow> fv M \<subseteq> fv N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M \<sqsubseteq> N \<Longrightarrow> fv M \<subseteq> fv N
[PROOF STEP]
by (induct N) auto


[STATEMENT]
lemma subterms_union_ground:
  assumes "ground M"
  shows "ground (subterms\<^sub>s\<^sub>e\<^sub>t M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
assume "t \<in> M"
[PROOF STATE]
proof (state)
this:
t \<in> M

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
hence "fv t = {}"
[PROOF STATE]
proof (prove)
using this:
t \<in> M

goal (1 subgoal):
 1. fv t = {}
[PROOF STEP]
using ground_iff_no_vars[of M] assms
[PROOF STATE]
proof (prove)
using this:
t \<in> M
ground M = (\<forall>v. Var v \<notin> subterms\<^sub>s\<^sub>e\<^sub>t M)
ground M

goal (1 subgoal):
 1. fv t = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv t = {}

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
hence "\<forall>t' \<in> subterms t. fv t' = {}"
[PROOF STATE]
proof (prove)
using this:
fv t = {}

goal (1 subgoal):
 1. \<forall>t'\<in>subterms t. fv t' = {}
[PROOF STEP]
using subtermeq_vars_subset[of _ t]
[PROOF STATE]
proof (prove)
using this:
fv t = {}
?M \<sqsubseteq> t \<Longrightarrow> fv ?M \<subseteq> fv t

goal (1 subgoal):
 1. \<forall>t'\<in>subterms t. fv t' = {}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>t'\<in>subterms t. fv t' = {}

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
hence "ground (subterms t)"
[PROOF STATE]
proof (prove)
using this:
\<forall>t'\<in>subterms t. fv t' = {}

goal (1 subgoal):
 1. ground (subterms t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground (subterms t)

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t2 \<in> M \<Longrightarrow> ground (subterms ?t2)

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?t2 \<in> M \<Longrightarrow> ground (subterms ?t2)

goal (1 subgoal):
 1. ground (subterms\<^sub>s\<^sub>e\<^sub>t M)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground (subterms\<^sub>s\<^sub>e\<^sub>t M)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem wpl_opt_bst: "wpl i j (opt_bst i j) = min_wpl i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
proof(induction i j rule: min_wpl.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<And>x. \<lbrakk>\<not> j < i; x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl i (x - 1) (local.opt_bst i (x - 1)) = local.min_wpl i (x - 1); \<And>x. \<lbrakk>\<not> j < i; x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl (x + 1) j (local.opt_bst (x + 1) j) = local.min_wpl (x + 1) j\<rbrakk> \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
case (1 i j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> j < i; ?x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl i (?x - 1) (local.opt_bst i (?x - 1)) = local.min_wpl i (?x - 1)
\<lbrakk>\<not> j < i; ?x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl (?x + 1) j (local.opt_bst (?x + 1) j) = local.min_wpl (?x + 1) j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>\<And>x. \<lbrakk>\<not> j < i; x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl i (x - 1) (local.opt_bst i (x - 1)) = local.min_wpl i (x - 1); \<And>x. \<lbrakk>\<not> j < i; x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl (x + 1) j (local.opt_bst (x + 1) j) = local.min_wpl (x + 1) j\<rbrakk> \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
 2. \<not> ?P \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
assume "i > j"
[PROOF STATE]
proof (state)
this:
j < i

goal (2 subgoals):
 1. ?P \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
 2. \<not> ?P \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
j < i

goal (1 subgoal):
 1. local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
local.wpl i j (local.opt_bst i j) = local.min_wpl i j

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
assume [arith]: "\<not> i > j"
[PROOF STATE]
proof (state)
this:
\<not> j < i

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
let ?ts = "[\<langle>opt_bst i (k-1), k, opt_bst (k+1) j\<rangle>. k \<leftarrow> [i..j]]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
let ?M = "((\<lambda>k. min_wpl i (k-1) + min_wpl (k+1) j + w i j) ` {i..j})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
have 1: "?ts \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j] \<noteq> []
[PROOF STEP]
by (auto simp add: upto.simps)
[PROOF STATE]
proof (state)
this:
map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j] \<noteq> []

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
have "wpl i j (opt_bst i j) = wpl i j (argmin (wpl i j) ?ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wpl i j (local.opt_bst i j) = local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.wpl i j (local.opt_bst i j) = local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.wpl i j (local.opt_bst i j) = local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
have "\<dots> = Min (wpl i j ` (set ?ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))
[PROOF STEP]
by(rule argmin_Min[OF 1])
[PROOF STATE]
proof (state)
this:
local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.wpl i j (argmin (local.wpl i j) (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]))

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
have "\<dots> = Min ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = (MIN k\<in>{i..j}. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j)
[PROOF STEP]
proof (rule arg_cong[where f=Min])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]) = (\<lambda>k. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) ` {i..j}
[PROOF STEP]
show "wpl i j ` (set ?ts) = ?M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]) = (\<lambda>k. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) ` {i..j}
[PROOF STEP]
using "1.IH"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<not> j < i; ?x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl i (?x - 1) (local.opt_bst i (?x - 1)) = local.min_wpl i (?x - 1)
\<lbrakk>\<not> j < i; ?x \<in> {i..j}\<rbrakk> \<Longrightarrow> local.wpl (?x + 1) j (local.opt_bst (?x + 1) j) = local.min_wpl (?x + 1) j

goal (1 subgoal):
 1. local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]) = (\<lambda>k. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) ` {i..j}
[PROOF STEP]
by (force simp: Bex_def image_iff "1.IH")
[PROOF STATE]
proof (state)
this:
local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j]) = (\<lambda>k. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) ` {i..j}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = (MIN k\<in>{i..j}. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j)

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Min (local.wpl i j ` set (map (\<lambda>k. \<langle>local.opt_bst i (k - 1), k, local.opt_bst (k + 1) j\<rangle>) [i..j])) = (MIN k\<in>{i..j}. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j)

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
have "\<dots> = min_wpl i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MIN k\<in>{i..j}. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) = local.min_wpl i j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(MIN k\<in>{i..j}. local.min_wpl i (k - 1) + local.min_wpl (k + 1) j + w i j) = local.min_wpl i j

goal (1 subgoal):
 1. \<not> j < i \<Longrightarrow> local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.wpl i j (local.opt_bst i j) = local.min_wpl i j

goal (1 subgoal):
 1. local.wpl i j (local.opt_bst i j) = local.min_wpl i j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.wpl i j (local.opt_bst i j) = local.min_wpl i j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.wpl i j (local.opt_bst i j) = local.min_wpl i j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reachable_trans[trans]: "q \<in> reachable p \<Longrightarrow> s \<in> reachable q \<Longrightarrow> s \<in> reachable p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>q \<in> reachable p; s \<in> reachable q\<rbrakk> \<Longrightarrow> s \<in> reachable p
[PROOF STEP]
by auto


[STATEMENT]
lemma has_density_emeasure_space':
    "has_density M N f \<Longrightarrow> emeasure (density N f) (space (density N f)) = \<integral>\<^sup>+x. f x \<partial>N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_density M N f \<Longrightarrow> emeasure (density N f) (space (density N f)) = integral\<^sup>N N f
[PROOF STEP]
by (frule has_densityD(2)[symmetric]) (simp add: has_density_emeasure_space)


[STATEMENT]
lemma enf_not_fulfilled_if_in_offending:
  assumes validRs: "valid_reqs M"
    and   wfG:     "wf_graph G"
    and   enf:     "\<forall>m \<in> set M. \<exists>P. \<forall>G. c_sinvar m G = (\<forall>e \<in> edges G. P e)"
    shows "\<forall>x \<in> (\<Union>m\<in>set M. \<Union>(c_offending_flows m (fully_connected G))).
                \<not> all_security_requirements_fulfilled M \<lparr> nodes = V, edges = insert x E\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<Union>m\<in>set M. \<Union> (c_offending_flows m (fully_connected G)). \<not> all_security_requirements_fulfilled M \<lparr>nodes = V, edges = insert x E\<rparr>
[PROOF STEP]
unfolding all_security_requirements_fulfilled_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>\<Union>m\<in>set M. \<Union> (c_offending_flows m (fully_connected G)). \<not> (\<forall>m\<in>set M. c_sinvar m \<lparr>nodes = V, edges = insert x E\<rparr>)
[PROOF STEP]
proof(simp, clarify, rename_tac m F a b)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
let ?G="(fully_connected G)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
fix m F v1 v2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
assume "m \<in> set M" and "F \<in> c_offending_flows m ?G" and "(v1, v2) \<in> F"
[PROOF STATE]
proof (state)
this:
m \<in> set M
F \<in> c_offending_flows m (fully_connected G)
(v1, v2) \<in> F

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from validRs
[PROOF STATE]
proof (chain)
picking this:
valid_reqs M
[PROOF STEP]
have valid_mD:"\<And>m. m \<in> set M \<Longrightarrow> configured_SecurityInvariant m "
[PROOF STATE]
proof (prove)
using this:
valid_reqs M

goal (1 subgoal):
 1. \<And>m. m \<in> set M \<Longrightarrow> configured_SecurityInvariant m
[PROOF STEP]
by(simp add: valid_reqs_def)
[PROOF STATE]
proof (state)
this:
?m \<in> set M \<Longrightarrow> configured_SecurityInvariant ?m

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from \<open>m \<in> set M\<close> valid_mD
[PROOF STATE]
proof (chain)
picking this:
m \<in> set M
?m \<in> set M \<Longrightarrow> configured_SecurityInvariant ?m
[PROOF STEP]
have "configured_SecurityInvariant m"
[PROOF STATE]
proof (prove)
using this:
m \<in> set M
?m \<in> set M \<Longrightarrow> configured_SecurityInvariant ?m

goal (1 subgoal):
 1. configured_SecurityInvariant m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
configured_SecurityInvariant m

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from enf \<open>m \<in> set M\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>m\<in>set M. \<exists>P. \<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)
m \<in> set M
[PROOF STEP]
obtain P where enf_m: "\<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)"
[PROOF STATE]
proof (prove)
using this:
\<forall>m\<in>set M. \<exists>P. \<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)
m \<in> set M

goal (1 subgoal):
 1. (\<And>P. \<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from \<open>(v1, v2) \<in> F\<close>
[PROOF STATE]
proof (chain)
picking this:
(v1, v2) \<in> F
[PROOF STEP]
have "F \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> F

goal (1 subgoal):
 1. F \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F \<noteq> {}

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from enf_offending_flows[OF \<open>configured_SecurityInvariant m\<close> \<open>\<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)\<close>]
[PROOF STATE]
proof (chain)
picking this:
\<forall>G. c_offending_flows m G = (if c_sinvar m G then {} else {{e \<in> edges G. \<not> P e}})
[PROOF STEP]
have
      offending: "\<And>G. c_offending_flows m G = (if c_sinvar m G then {} else {{e \<in> edges G. \<not> P e}})"
[PROOF STATE]
proof (prove)
using this:
\<forall>G. c_offending_flows m G = (if c_sinvar m G then {} else {{e \<in> edges G. \<not> P e}})

goal (1 subgoal):
 1. \<And>G. c_offending_flows m G = (if c_sinvar m G then {} else {{e \<in> edges G. \<not> P e}})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_offending_flows m ?G = (if c_sinvar m ?G then {} else {{e \<in> edges ?G. \<not> P e}})

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from \<open>F \<in> c_offending_flows m ?G\<close> \<open>F \<noteq> {}\<close>
[PROOF STATE]
proof (chain)
picking this:
F \<in> c_offending_flows m (fully_connected G)
F \<noteq> {}
[PROOF STEP]
have "F = {e \<in> edges ?G. \<not> P e}"
[PROOF STATE]
proof (prove)
using this:
F \<in> c_offending_flows m (fully_connected G)
F \<noteq> {}

goal (1 subgoal):
 1. F = {e \<in> edges (fully_connected G). \<not> P e}
[PROOF STEP]
by(simp split: if_split_asm add: offending)
[PROOF STATE]
proof (state)
this:
F = {e \<in> edges (fully_connected G). \<not> P e}

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from this \<open>(v1, v2) \<in> F\<close>
[PROOF STATE]
proof (chain)
picking this:
F = {e \<in> edges (fully_connected G). \<not> P e}
(v1, v2) \<in> F
[PROOF STEP]
have "\<not> P (v1, v2)"
[PROOF STATE]
proof (prove)
using this:
F = {e \<in> edges (fully_connected G). \<not> P e}
(v1, v2) \<in> F

goal (1 subgoal):
 1. \<not> P (v1, v2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> P (v1, v2)

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
from this enf_m
[PROOF STATE]
proof (chain)
picking this:
\<not> P (v1, v2)
\<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)
[PROOF STEP]
have "\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<not> P (v1, v2)
\<forall>G. c_sinvar m G = (\<forall>e\<in>edges G. P e)

goal (1 subgoal):
 1. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>

goal (1 subgoal):
 1. \<And>m F a b. \<lbrakk>m \<in> set M; F \<in> c_offending_flows m (fully_connected G); (a, b) \<in> F\<rbrakk> \<Longrightarrow> \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (a, b) E\<rparr>
[PROOF STEP]
thus "\<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>

goal (1 subgoal):
 1. \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>
[PROOF STEP]
using \<open>m \<in> set M\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>
m \<in> set M

goal (1 subgoal):
 1. \<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>
[PROOF STEP]
apply(rule_tac x="m" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>; m \<in> set M\<rbrakk> \<Longrightarrow> \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>
 2. \<lbrakk>\<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>; m \<in> set M\<rbrakk> \<Longrightarrow> m \<in> set M
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<exists>m\<in>set M. \<not> c_sinvar m \<lparr>nodes = V, edges = insert (v1, v2) E\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed