[STATEMENT]
lemma gen_cast_fun_set_rel[autoref_rules_raw]:
  assumes INS: "GEN_OP mem (\<in>) (Rk\<rightarrow>\<langle>Rk\<rangle>Rs\<rightarrow>bool_rel)"
  shows "(\<lambda>s x. mem x s,CAST) \<in> (\<langle>Rk\<rangle>Rs) \<rightarrow> (\<langle>Rk\<rangle>fun_set_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
have A: "\<And>s. (\<lambda>x. x\<in>s,CAST s) \<in> br Collect (\<lambda>_. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<lambda>x. x \<in> s, CAST s) \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
by (auto simp: br_def)
[PROOF STATE]
proof (state)
this:
(\<lambda>x. x \<in> ?s, CAST ?s) \<in> br Collect (\<lambda>_. True)

goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel
[PROOF STEP]
unfolding fun_set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> (Rk \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, CAST a') \<in> (Rk \<rightarrow> bool_rel) O br Collect (\<lambda>_. True)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, ?b2 a a') \<in> Rk \<rightarrow> bool_rel
 2. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (?b2 a a', CAST a') \<in> br Collect (\<lambda>_. True)
[PROOF STEP]
defer
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (?b2 a a', CAST a') \<in> br Collect (\<lambda>_. True)
 2. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, ?b2 a a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
apply (rule A)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, \<lambda>x. x \<in> a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
using INS[simplified]
[PROOF STATE]
proof (prove)
using this:
(mem, (\<in>)) \<in> Rk \<rightarrow> \<langle>Rk\<rangle>Rs \<rightarrow> bool_rel

goal (1 subgoal):
 1. \<And>a a'. (a, a') \<in> \<langle>Rk\<rangle>Rs \<Longrightarrow> (\<lambda>x. mem x a, \<lambda>x. x \<in> a') \<in> Rk \<rightarrow> bool_rel
[PROOF STEP]
apply parametricity
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>s x. mem x s, CAST) \<in> \<langle>Rk\<rangle>Rs \<rightarrow> \<langle>Rk\<rangle>fun_set_rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finlsts_rec_LNil_def:
  "f \<equiv> finlsts_rec c d \<Longrightarrow> f LNil = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<equiv> finlsts_rec c d \<Longrightarrow> f LNil = c
[PROOF STEP]
by (auto simp: finlsts_rec_LNil)


[STATEMENT]
lemma lrev_is_LNil_conv [iff]:
  "xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (lrev xs = LNil) = (xs = LNil)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in> UNIV\<^sup>\<star> \<Longrightarrow> (lrev xs = LNil) = (xs = LNil)
[PROOF STEP]
by (induct rule: finlsts.induct) auto


[STATEMENT]
lemma fdia_arden_iff: "\<nabla>x = 0 \<Longrightarrow> (d p = d q + |x\<rangle> p \<longleftrightarrow> d p = |x\<^sup>\<star>\<rangle> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nabla>x = (zero_class.zero::'a) \<Longrightarrow> (d p = d q +  |x\<rangle> p) = (d p =  |x\<^sup>\<star>\<rangle> q)
[PROOF STEP]
by (metis fdia_arden_eq dka.fdia_d_simp dka.fdia_star_unfold_var)


[STATEMENT]
lemma mtx_vec_mult_minus_rdistrib: "(A - B) *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A - B) *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x
[PROOF STEP]
unfolding minus_sq_mtx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun to_vec (map_fun to_vec to_mtx) (-) A B *\<^sub>V x = A *\<^sub>V x - B *\<^sub>V x
[PROOF STEP]
by(transfer, simp add: matrix_vector_mult_diff_rdistrib)


[STATEMENT]
lemma interpret_floatarith_norm[simp]:
  assumes [simp]: "length x = DIM('a)"
  shows "interpret_floatarith (Norm x) vs = norm (einterpret x vs::'a::executable_euclidean_space)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. interpret_floatarith (Norm x) vs = norm (einterpret x vs)
[PROOF STEP]
apply (auto simp: Norm_def norm_eq_sqrt_inner)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. interpret_floatarith i vs * interpret_floatarith i vs) = einterpret x vs \<bullet> einterpret x vs
[PROOF STEP]
apply (subst euclidean_inner[where 'a='a])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. interpret_floatarith i vs * interpret_floatarith i vs) = (\<Sum>b\<in>Basis. einterpret x vs \<bullet> b * (einterpret x vs \<bullet> b))
[PROOF STEP]
apply (auto simp: power2_eq_square[symmetric] )
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. (interpret_floatarith i vs)\<^sup>2) = (\<Sum>b\<in>Basis. (einterpret x vs \<bullet> b)\<^sup>2)
[PROOF STEP]
apply (subst sum_list_Basis_list[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>x. (interpret_floatarith i vs)\<^sup>2) = (\<Sum>b\<leftarrow>Basis_list. (einterpret x vs \<bullet> b)\<^sup>2)
[PROOF STEP]
apply (rule sum_list_nth_eqI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. length (map (\<lambda>i. (interpret_floatarith i vs)\<^sup>2) x) = length (map (\<lambda>b. (einterpret x vs \<bullet> b)\<^sup>2) Basis_list)
 2. \<And>xa y. (xa, y) \<in> set (zip (map (\<lambda>i. (interpret_floatarith i vs)\<^sup>2) x) (map (\<lambda>b. (einterpret x vs \<bullet> b)\<^sup>2) Basis_list)) \<Longrightarrow> xa = y
[PROOF STEP]
by (auto simp: in_set_zip eucl_of_list_inner)


[STATEMENT]
lemma max_Var_floatariths_map_uminus[simp]:
  "max_Var_floatariths (map (\<lambda>i. - fa1 i) xs) = max_Var_floatariths (map fa1 xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_Var_floatariths (map (\<lambda>i. - fa1 i) xs) = max_Var_floatariths (map fa1 xs)
[PROOF STEP]
by (auto simp: max_Var_floatariths_Max image_image Max_Image_distrib)


[STATEMENT]
lemma isFDERIV_imp_isFDERIV_FDERIV_n:
  assumes "length fas = length ds"
  shows "isFDERIV N xs fas vs \<Longrightarrow> isFDERIV N xs ds vs \<Longrightarrow>
    isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isFDERIV N xs fas vs; isFDERIV N xs ds vs\<rbrakk> \<Longrightarrow> isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length fas = length ds

goal (1 subgoal):
 1. \<lbrakk>isFDERIV N xs fas vs; isFDERIV N xs ds vs\<rbrakk> \<Longrightarrow> isFDERIV N xs (FDERIV_n_floatariths fas xs ds n) vs
[PROOF STEP]
by (induction n) (auto intro!: isDERIV_FDERIV_floatariths)


[STATEMENT]
lemma  fixes E :: "('a,'b, 'addr) exp" and Es :: "('a,'b, 'addr) exp list"
  shows inline_call_eq_Throw [dest]: "inline_call e E = Throw a \<Longrightarrow> call E = \<lfloor>aMvs\<rfloor> \<Longrightarrow> e = Throw a \<or> e = addr a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inline_call e E = Throw a; call E = \<lfloor>aMvs\<rfloor>\<rbrakk> \<Longrightarrow> e = Throw a \<or> e = addr a
[PROOF STEP]
by(induct E rule: exp.induct)(fastforce split:if_split_asm)+


[STATEMENT]
lemma mpoly_eqI:
  assumes "\<And>mon. MPoly_Type.coeff p mon = MPoly_Type.coeff q mon"
  shows   "p = q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
MPoly_Type.coeff p ?mon = MPoly_Type.coeff q ?mon

goal (1 subgoal):
 1. p = q
[PROOF STEP]
by (transfer, transfer) (auto simp: fun_eq_iff)


[STATEMENT]
lemma vars_0 [simp]: "vars 0 = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars 0 = {}
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of 0)) = {}
[PROOF STEP]
by transfer' simp


[STATEMENT]
lemma vars_Const [simp]: "vars (Const c) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Const c) = {}
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (Const c))) = {}
[PROOF STEP]
by transfer' (auto simp: keys_Const\<^sub>0)


[STATEMENT]
lemma prod_fun_max:
  fixes f g :: "'a::{linorder, ordered_cancel_comm_monoid_add} \<Rightarrow> 'b::semiring_0"
  assumes zero: "\<And>m. m > a \<Longrightarrow> f m = 0" "\<And>m. m > b \<Longrightarrow> g m = 0"
  assumes fin: "finite {m. f m \<noteq> 0}" "finite {m. g m \<noteq> 0}"
  shows   "prod_fun f g (a + b) = f a * g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
note fin' = finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)]
[PROOF STATE]
proof (state)
this:
?A \<subseteq> {m. f m \<noteq> (0::'b)} \<Longrightarrow> finite ?A
?A \<subseteq> {m. g m \<noteq> (0::'b)} \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))
[PROOF STEP]
by (simp add: prod_fun_def Sum_any_right_distrib)
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)
[PROOF STEP]
by (subst Sum_any_right_distrib) (auto intro!: Sum_any.cong fin'(2) simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<Sum>l. f l * (\<Sum>q. g q when a + b = l + q)) = (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
fix l q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
assume lq: "a + b = l + q" "(a, b) \<noteq> (l, q)" and nz: "f l * g q \<noteq> 0"
[PROOF STATE]
proof (state)
this:
a + b = l + q
(a, b) \<noteq> (l, q)
f l * g q \<noteq> (0::'b)

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
from nz and zero
[PROOF STATE]
proof (chain)
picking this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)
[PROOF STEP]
have "l \<le> a" "q \<le> b"
[PROOF STATE]
proof (prove)
using this:
f l * g q \<noteq> (0::'b)
a < ?m \<Longrightarrow> f ?m = (0::'b)
b < ?m \<Longrightarrow> g ?m = (0::'b)

goal (1 subgoal):
 1. l \<le> a &&& q \<le> b
[PROOF STEP]
by (auto intro: leI)
[PROOF STATE]
proof (state)
this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
l \<le> a
q \<le> b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
from this and lq(2)
[PROOF STATE]
proof (chain)
picking this:
l \<le> a
q \<le> b
(a, b) \<noteq> (l, q)
[PROOF STEP]
have "l < a \<or> q < b"
[PROOF STATE]
proof (prove)
using this:
l \<le> a
q \<le> b
(a, b) \<noteq> (l, q)

goal (1 subgoal):
 1. l < a \<or> q < b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < a \<or> q < b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
l \<le> a
q \<le> b
l < a \<or> q < b
[PROOF STEP]
have "l + q < a + b"
[PROOF STATE]
proof (prove)
using this:
l \<le> a
q \<le> b
l < a \<or> q < b

goal (1 subgoal):
 1. l + q < a + b
[PROOF STEP]
by (auto intro: add_less_le_mono add_le_less_mono)
[PROOF STATE]
proof (state)
this:
l + q < a + b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
with lq(1)
[PROOF STATE]
proof (chain)
picking this:
a + b = l + q
l + q < a + b
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
a + b = l + q
l + q < a + b

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

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>a + b = ?l2 + ?q2; (a, b) \<noteq> (?l2, ?q2); f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
hence "(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>a + b = ?l2 + ?q2; (a, b) \<noteq> (?l2, ?q2); f ?l2 * g ?q2 \<noteq> (0::'b)\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.cong refl) (auto simp: when_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when a + b = l + q) = (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(l,q). f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.cartesian_product[of "{(a, b)}"]) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l. \<Sum>q. f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q). f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = (\<Sum>(l,q)\<in>{(a,b)}. f l * g q when (a, b) = (l, q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))
[PROOF STEP]
by (intro Sum_any.expand_superset) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q). f l * g q when (a, b) = (l, q)) = (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q))

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
have "\<dots> = f a * g b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q)) = f a * g b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>(l, q)\<in>{(a, b)}. f l * g q when (a, b) = (l, q)) = f a * g b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prod_fun f g (a + b) = f a * g b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prod_fun f g (a + b) = f a * g b

goal (1 subgoal):
 1. prod_fun f g (a + b) = f a * g b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prod_fun f g (a + b) = f a * g b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poly_mapping_map_conv_mapp: "Poly_Mapping.map f = Poly_Mapping.mapp (\<lambda>_. f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Poly_Mapping.map f = Poly_Mapping.mapp (\<lambda>_. f)
[PROOF STEP]
by (auto simp: Poly_Mapping.mapp_def Poly_Mapping.map_def map_fun_def
                 o_def fun_eq_iff when_def in_keys_iff cong: if_cong)


[STATEMENT]
theorem FNTT_correct:
  assumes "length numbers = n"
  shows "FNTT numbers = NTT numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FNTT numbers = NTT numbers
[PROOF STEP]
using FNTT_NTT_gen_eq NTT_gen_NTT_full_length assms n_two_pot
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?numbers = 2 ^ ?l; 2 ^ ?l \<le> n\<rbrakk> \<Longrightarrow> FNTT ?numbers = NTT_gen (length ?numbers) ?numbers
length ?numbers = n \<Longrightarrow> NTT_gen n ?numbers = NTT ?numbers
length numbers = n
n = 2 ^ N

goal (1 subgoal):
 1. FNTT numbers = NTT numbers
[PROOF STEP]
by force


[STATEMENT]
lemma DynPDG_ddep_edge_only_first_edge:
  "\<lbrakk>n -{V}a#as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a#as)) s\<rbrakk> \<Longrightarrow>
    state_val (transfers (kinds (a#as)) s) V = state_val (transfer (kind a) s) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -{V}a # as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n -{V}a # as\<rightarrow>\<^sub>d\<^sub>d n'; preds (kinds (a # as)) s\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(erule DynPDG_edge.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>na n'a asa. \<lbrakk>preds (kinds (a # as)) s; n = na; Some V = None; a # as = asa; n' = n'a; na controls n'a via asa\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
 2. \<And>na Va n'a asa. \<lbrakk>preds (kinds (a # as)) s; n = na; Some V = Some Va; a # as = asa; n' = n'a; na influences Va in n'a via asa\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(frule dyn_influence_Cons_source)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as; sourcenode a = n\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
apply(frule dyn_influence_source_notin_tl_edges)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preds (kinds (a # as)) s; n influences V in n' via a # as; sourcenode a = n; n \<notin> set (sourcenodes as)\<rbrakk> \<Longrightarrow> state_val (transfers (kinds (a # as)) s) V = state_val (transfer (kind a) s) V
[PROOF STEP]
by(erule dyn_influence_only_first_edge)


[STATEMENT]
lemma lmirror_llist_of [simp]: "lmirror (llist_of xs) = llist_of (xs @ rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lmirror (llist_of xs) = llist_of (xs @ rev xs)
[PROOF STEP]
by(induct xs)(simp_all add: lappend_llist_of_LCons)


[STATEMENT]
lemma is_strict_orD: "is_strict (\<Otimes>\<^sub>\<or>\<^sub>D) d r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_strict (\<Otimes>\<^sub>\<or>\<^sub>D) d r
[PROOF STEP]
apply (simp add: is_strict_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d o\<^sub>f (\<emptyset> \<circ> r) = \<emptyset>
[PROOF STEP]
apply (simp add: policy_range_comp_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma differenceset_translate_eq_left:
  assumes "A \<subseteq> G" and "B \<subseteq> G" and "x \<in> G"
  shows "(differenceset {x} A = differenceset {x} B) \<longleftrightarrow> A = B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (differenceset {x} A = differenceset {x} B) = (A = B)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> G
B \<subseteq> G
x \<in> G

goal (1 subgoal):
 1. (differenceset {x} A = differenceset {x} B) = (A = B)
[PROOF STEP]
by (metis differenceset_commute differenceset_translate_eq_right)


[STATEMENT]
lemma lookup_insert [simp]:
  "lookup (insert (k :: 'a) v t) = (lookup t)(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (RBT_Mapping2.insert k v t) = lookup t(k \<mapsto> v)
[PROOF STEP]
by transfer (simp add: ID_ccompare_neq_None
  linorder.rbt_lookup_rbt_insert[OF mapping_linorder])


[STATEMENT]
lemma iso_finfun_inf [code_unfold]:
  "inf (($) A) (($) B) = ($) (inf A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf (($) A) (($) B) = ($) (inf A B)
[PROOF STEP]
by(simp)


[STATEMENT]
lemma inv_pair_update1:
  "inv_pair m'"
  if "State_Monad.run_state (update1 (key2 k) v) m = (v', m')" "inv_pair m" "fst (State_Monad.run_state get_k1 m) = key1 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
using that update_inv[of "key2 k" v] inv_pair_P_D[OF \<open>inv_pair m\<close>]
[PROOF STATE]
proof (prove)
using this:
run_state (update1 (key2 k) v) m = (v', m')
inv_pair m
fst (run_state get_k1 m) = key1 k
lift_p P (update1 (key2 k) v)
lift_p P (update2 (key2 k) v)
P m

goal (1 subgoal):
 1. inv_pair m'
[PROOF STEP]
unfolding inv_pair_def
[PROOF STATE]
proof (prove)
using this:
run_state (update1 (key2 k) v) m = (v', m')
let k1 = fst (run_state get_k1 m); k2 = fst (run_state get_k2 m) in (\<forall>k\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m
fst (run_state get_k1 m) = key1 k
lift_p P (update1 (key2 k) v)
lift_p P (update2 (key2 k) v)
P m

goal (1 subgoal):
 1. let k1 = fst (run_state get_k1 m'); k2 = fst (run_state get_k2 m') in (\<forall>k\<in>dom (mem1.map_of m'). \<exists>k'. key1 k' = k1 \<and> key2 k' = k) \<and> (\<forall>k\<in>dom (mem2.map_of m'). \<exists>k'. key1 k' = k2 \<and> key2 k' = k) \<and> k1 \<noteq> k2 \<and> P m'
[PROOF STEP]
apply (auto
        simp: Let_def update_keys
        dest: lift_p_P update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]
     )
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem1.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka
 2. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = ka
[PROOF STEP]
apply (frule update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]; auto 13 2; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ka y. \<lbrakk>run_state (update1 (key2 k) v) m = ((), m'); fst (run_state get_k1 m) = key1 k; lift_p P (update1 (key2 k) v); lift_p P (update2 (key2 k) v); P m; \<forall>ka\<in>dom (mem1.map_of m). \<exists>k'. key1 k' = key1 k \<and> key2 k' = ka; \<forall>k\<in>dom (mem2.map_of m). \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = k; key1 k \<noteq> fst (run_state get_k2 m); mem2.map_of m' ka = Some y\<rbrakk> \<Longrightarrow> \<exists>k'. key1 k' = fst (run_state get_k2 m) \<and> key2 k' = ka
[PROOF STEP]
apply (frule update_correct[of _ "key2 k" v, THEN map_le_implies_dom_le]; auto 13 2; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma vars_clause_hd_partitioned_from_tl:
  assumes "Cs \<noteq>[]"
  shows "vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs)))
    \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
Cs \<noteq> []

goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
[PROOF STEP]
proof (induction Cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
case (Cons C Cs)
[PROOF STATE]
proof (state)
this:
Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}
C # Cs \<noteq> []

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
define \<sigma>' :: "nat \<Rightarrow> nat"
    where "\<sigma>' = (\<lambda>v. (Suc (v + Max ((vars_clause_list (subst_cls_lists Cs
                        (renamings_apart Cs))) \<union> {0}))))"
[PROOF STATE]
proof (state)
this:
\<sigma>' = (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0})))

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
define \<sigma> :: "nat \<Rightarrow> ('a, nat) term"
    where "\<sigma> = (\<lambda>v. Var (\<sigma>' v))"
[PROOF STATE]
proof (state)
this:
\<sigma> = (\<lambda>v. Var (\<sigma>' v))

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
have "vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
using vars_in_instance_in_range_cls[of C "hd (renamings_apart (C # Cs))"] \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (hd (renamings_apart (C # Cs)))) \<subseteq> \<Union> (vars_term ` range (hd (renamings_apart (C # Cs))))
\<sigma> = (\<lambda>v. Var (\<sigma>' v))
\<sigma>' = (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0})))

goal (1 subgoal):
 1. vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
have "\<Union> (vars_term ` range \<sigma>)
    \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
have "range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
unfolding \<sigma>'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
using Suc_Max_notin_set
[PROOF STATE]
proof (prove)
using this:
finite ?X \<Longrightarrow> Suc (?v + Max (insert 0 ?X)) \<notin> ?X

goal (1 subgoal):
 1. range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
range \<sigma>' \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
unfolding \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
range (\<lambda>v. Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. \<Union> (vars_term ` range (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
have "vars_clause (subst_cls C \<sigma>)
     \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}"
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C \<sigma>) \<subseteq> \<Union> (vars_term ` range \<sigma>)
\<Union> (vars_term ` range \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (2 subgoals):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
 2. \<And>a Cs. \<lbrakk>Cs \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists Cs (renamings_apart Cs))) \<inter> vars_clause_list (tl (subst_cls_lists Cs (renamings_apart Cs))) = {}; a # Cs \<noteq> []\<rbrakk> \<Longrightarrow> vars_clause (hd (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (a # Cs) (renamings_apart (a # Cs)))) = {}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C \<sigma>) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) = {}
[PROOF STEP]
unfolding \<sigma>_def \<sigma>'_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (\<lambda>v. Var (Suc (v + Max (vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (subst_cls_lists Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (hd (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) = {}
[PROOF STEP]
unfolding subst_cls_lists_def
[PROOF STATE]
proof (prove)
using this:
vars_clause (subst_cls C (\<lambda>v. Var (Suc (v + Max (vars_clause_list (Map2.map2 subst_cls Cs (renamings_apart Cs)) \<union> {0}))))) \<inter> vars_clause_list (Map2.map2 subst_cls Cs (renamings_apart Cs)) = {}

goal (1 subgoal):
 1. vars_clause (hd (Map2.map2 subst_cls (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (Map2.map2 subst_cls (C # Cs) (renamings_apart (C # Cs)))) = {}
[PROOF STEP]
by (simp add: Let_def subst_cls_lists_def)
[PROOF STATE]
proof (state)
this:
vars_clause (hd (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) \<inter> vars_clause_list (tl (subst_cls_lists (C # Cs) (renamings_apart (C # Cs)))) = {}

goal (1 subgoal):
 1. [] \<noteq> [] \<Longrightarrow> vars_clause (hd (subst_cls_lists [] (renamings_apart []))) \<inter> vars_clause_list (tl (subst_cls_lists [] (renamings_apart []))) = {}
[PROOF STEP]
qed auto


[STATEMENT]
lemma index_mat_multrow[simp]:
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_multrow_gen mul k a A $$ (i,j) = (if k = i then mul a (A $$ (i,j)) else A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> mat_multrow_gen mul i a A $$ (i,j) = mul a (A $$ (i,j))"
  "i < dim_row A \<Longrightarrow> j < dim_col A \<Longrightarrow> k \<noteq> i \<Longrightarrow> mat_multrow_gen mul k a A $$ (i,j) = A $$ (i,j)"
  "dim_row (mat_multrow_gen mul k a A) = dim_row A" "dim_col (mat_multrow_gen mul k a A) = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_multrow_gen mul k a A $$ (i, j) = (if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat_multrow_gen mul i a A $$ (i, j) = mul a (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat_multrow_gen mul k a A $$ (i, j) = A $$ (i, j)) &&& dim_row (mat_multrow_gen mul k a A) = dim_row A &&& dim_col (mat_multrow_gen mul k a A) = dim_col A
[PROOF STEP]
unfolding mat_multrow_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = (if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) &&& (\<lbrakk>i < dim_row A; j < dim_col A\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(ia, j). if i = ia then mul a (A $$ (ia, j)) else A $$ (ia, j)) $$ (i, j) = mul a (A $$ (i, j)))) &&& (\<lbrakk>i < dim_row A; j < dim_col A; k \<noteq> i\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j)) $$ (i, j) = A $$ (i, j)) &&& dim_row (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) = dim_row A &&& dim_col (mat (dim_row A) (dim_col A) (\<lambda>(i, j). if k = i then mul a (A $$ (i, j)) else A $$ (i, j))) = dim_col A
[PROOF STEP]
by auto


[STATEMENT]
lemma mat_t_mult_mm [simp]:
  shows "mat_transpose (A *\<^sub>m\<^sub>m B) = mat_transpose B *\<^sub>m\<^sub>m mat_transpose A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_transpose (A *\<^sub>m\<^sub>m B) = mat_transpose B *\<^sub>m\<^sub>m mat_transpose A
[PROOF STEP]
by (cases A, cases B) auto


[STATEMENT]
lemma consistent_swapSyms[simp]:
"consistent t \<Longrightarrow> consistent (swapSyms t a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. consistent t \<Longrightarrow> consistent (swapSyms t a b)
[PROOF STEP]
by (simp add: swapSyms_def)


[STATEMENT]
lemma \<T>_return_eq:
  shows
    "\<T> p s = do {
  a \<leftarrow> measure_pmf (p [] s);
  s' \<leftarrow> measure_pmf (K (s,a));
  w \<leftarrow> T (\<pi>_Suc p (s,a)) (return_pmf s');
  return S ((s,a)##w)
}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
have "\<T> p s = do {
    a \<leftarrow> measure_pmf (p [] s);
    \<omega> \<leftarrow> T (\<pi>_Suc p (s, a)) (K (s, a));
   return S ((s, a) ## \<omega>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))
[PROOF STEP]
using \<T>_eq_return
[PROOF STATE]
proof (prove)
using this:
\<T> ?p ?s = measure_pmf (?p [] ?s) \<bind> (\<lambda>y. T (\<pi>_Suc ?p (?s, y)) (K (?s, y)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((?s, y) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>)))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
have "\<dots> =  do {
    a \<leftarrow> measure_pmf (p [] s);
    s' \<leftarrow> measure_pmf (K (s, a));
    \<omega> \<leftarrow> T (\<pi>_Suc p (s, a)) (return_pmf s');
   return S ((s, a) ## \<omega>)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
unfolding \<T>_return
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> \<T> (\<pi>_Suc p (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. measure_pmf (return_pmf s') \<bind> \<T> (\<pi>_Suc p (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
by (subst bind_assoc[of _ _ S _ S]) (auto simp add: \<T>_def \<T>_return[symmetric])
[PROOF STATE]
proof (state)
this:
measure_pmf (p [] s) \<bind> (\<lambda>a. T (\<pi>_Suc p (s, a)) (K (s, a)) \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))) = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>\<omega>. return (stream_space (count_space UNIV)) ((s, a) ## \<omega>))))

goal (1 subgoal):
 1. \<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<T> p s = measure_pmf (p [] s) \<bind> (\<lambda>a. measure_pmf (K (s, a)) \<bind> (\<lambda>s'. T (\<pi>_Suc p (s, a)) (return_pmf s') \<bind> (\<lambda>w. return (stream_space (count_space UNIV)) ((s, a) ## w))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma icard_insert_disjoint: "x \<notin> A \<Longrightarrow> icard (insert x A) = eSuc (icard A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<notin> A \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (case_tac "finite A")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<notin> A; finite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
 2. \<lbrakk>x \<notin> A; infinite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (simp add: icard_finite eSuc_enat card_insert_disjoint)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<notin> A; infinite A\<rbrakk> \<Longrightarrow> icard (insert x A) = eSuc (icard A)
[PROOF STEP]
apply (simp add: infinite_insert)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma not_conflicting_objects_empty_object [elim!]:
  "(sep_heap x) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sep_heap x obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id
[PROOF STEP]
by (clarsimp simp: not_conflicting_objects_def)


[STATEMENT]
lemma op_dghm_dghm_const[dg_op_simps]:
  "op_dghm (dghm_const \<CC> \<DD> a f) = dghm_const (op_dg \<CC>) (op_dg \<DD>) a f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (dghm_const \<CC> \<DD> a f) = dghm_const (op_dg \<CC>) (op_dg \<DD>) a f
[PROOF STEP]
unfolding dghm_const_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [vconst_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>) f, \<CC>, \<DD>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [vconst_on ([\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>) a, vconst_on ([\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>) f, [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<DD>\<lparr>[]\<^sub>\<circ>\<rparr>, \<DD>\<lparr>1\<^sub>\<nat>\<rparr>, \<DD>\<lparr>3\<^sub>\<nat>\<rparr>, \<DD>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma distinct_vertices12[simp]: "vertex_1 \<noteq> vertex_2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_2
[PROOF STEP]
using distinct_vertices
[PROOF STATE]
proof (prove)
using this:
distinct [vertex_1, vertex_2, vertex_3]

goal (1 subgoal):
 1. vertex_1 \<noteq> vertex_2
[PROOF STEP]
by(simp)


[STATEMENT]
theorem seqr_post_transfer: "out\<alpha> \<sharp> q \<Longrightarrow> (P ;; (q \<and> R)) = ((P \<and> q\<^sup>-) ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. out\<alpha> \<sharp> q \<Longrightarrow> P ;; (q \<and> R) = (P \<and> q\<^sup>-) ;; R
[PROOF STEP]
by (rel_auto)


[STATEMENT]
lemma frame_contract_RID:
  assumes "vwb_lens x" "P is RID(x)" "x \<bowtie> y"
  shows "(x;y):[P] = y:[P]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
vwb_lens x
x \<bowtie> y
[PROOF STEP]
have "(x;y):[RID(x)(P)] = y:[RID(x)(P)]"
[PROOF STATE]
proof (prove)
using this:
vwb_lens x
x \<bowtie> y

goal (1 subgoal):
 1. {x, y}:[RID x P] = {y}:[RID x P]
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>x\<^esub> (put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)) (get\<^bsub>x\<^esub> a)\<rbrakk> \<Longrightarrow> b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)
 2. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a)
[PROOF STEP]
apply (simp add: lens_indep.lens_put_comm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b v va. \<lbrakk>vwb_lens x; x \<bowtie> y; \<lbrakk>P\<rbrakk>\<^sub>e (put\<^bsub>x\<^esub> a v, put\<^bsub>x\<^esub> b va); get\<^bsub>x\<^esub> b = get\<^bsub>x\<^esub> a; b = put\<^bsub>y\<^esub> a (get\<^bsub>y\<^esub> b)\<rbrakk> \<Longrightarrow> b = put\<^bsub>x\<^esub> b (get\<^bsub>x\<^esub> a)
[PROOF STEP]
apply (metis (no_types) vwb_lens_wb wb_lens.get_put)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
{x, y}:[RID x P] = {y}:[RID x P]

goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{x, y}:[RID x P] = {y}:[RID x P]

goal (1 subgoal):
 1. {x, y}:[P] = {y}:[P]
[PROOF STEP]
by (simp add: Healthy_if assms)
[PROOF STATE]
proof (state)
this:
{x, y}:[P] = {y}:[P]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma swap0in2:  assumes "set l = {x,y}" "x\<noteq>y" "length l = 2" "dist_perm l l"
  shows
    "x < y in (swap 0) l = (~ x < y in l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
proof (cases "x < y in l")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y in l

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y in l
[PROOF STEP]
have a: "index l x < index l y"
[PROOF STATE]
proof (prove)
using this:
x < y in l

goal (1 subgoal):
 1. index l x < index l y
[PROOF STEP]
unfolding before_in_def
[PROOF STATE]
proof (prove)
using this:
index l x < index l y \<and> y \<in> set l

goal (1 subgoal):
 1. index l x < index l y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l x < index l y

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have drin: "x\<in>set l" "y\<in>set l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

goal (1 subgoal):
 1. x \<in> set l &&& y \<in> set l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set l
y \<in> set l

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
length l = 2
[PROOF STEP]
have b: "index l y < 2"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
length l = 2

goal (1 subgoal):
 1. index l y < 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y < 2

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
index l x < index l y
index l y < 2
[PROOF STEP]
have k: "index l x = 0" "index l y = 1"
[PROOF STATE]
proof (prove)
using this:
index l x < index l y
index l y < 2

goal (1 subgoal):
 1. index l x = 0 &&& index l y = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 0
index l y = 1

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have g: "x = l ! 0" "y = l ! 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = l ! 0 &&& y = l ! 1
[PROOF STEP]
using k nth_index assms(1)
[PROOF STATE]
proof (prove)
using this:
index l x = 0
index l y = 1
?x \<in> set ?xs \<Longrightarrow> ?xs ! index ?xs ?x = ?x
set l = {x, y}

goal (1 subgoal):
 1. x = l ! 0 &&& y = l ! 1
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
x = l ! 0
y = l ! 1

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "x < y in swap 0 l
      = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
apply(rule before_in_swap)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist_perm l ?ys
 2. Suc 0 < length l
[PROOF STEP]
apply(fact assms(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
length l = 2

goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = (\<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
x < y in l

goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False
[PROOF STEP]
using g assms(2)
[PROOF STATE]
proof (prove)
using this:
x = l ! 0
y = l ! 1
x \<noteq> y

goal (1 subgoal):
 1. (\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = False

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l = False
[PROOF STEP]
have "~ x < y in (swap 0) l"
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l = False

goal (1 subgoal):
 1. \<not> x < y in swap 0 l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> x < y in swap 0 l

goal (2 subgoals):
 1. x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
 2. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y in swap 0 l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in swap 0 l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in swap 0 l
x < y in l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (\<not> x < y in l)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < y in l

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
x \<noteq> y
[PROOF STEP]
have "index l y \<noteq> index l x"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
x \<noteq> y

goal (1 subgoal):
 1. index l y \<noteq> index l x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l y \<noteq> index l x

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
with False assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y in l
set l = {x, y}
x \<noteq> y
index l y \<noteq> index l x
[PROOF STEP]
have a: "index l y < index l x"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in l
set l = {x, y}
x \<noteq> y
index l y \<noteq> index l x

goal (1 subgoal):
 1. index l y < index l x
[PROOF STEP]
by (metis before_in_def insert_iff linorder_neqE_nat)
[PROOF STATE]
proof (state)
this:
index l y < index l x

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
[PROOF STEP]
have drin: "x\<in>set l" "y\<in>set l"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}

goal (1 subgoal):
 1. x \<in> set l &&& y \<in> set l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set l
y \<in> set l

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
set l = {x, y}
length l = 2
[PROOF STEP]
have b: "index l x < 2"
[PROOF STATE]
proof (prove)
using this:
set l = {x, y}
length l = 2

goal (1 subgoal):
 1. index l x < 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
index l x < 2

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
from a b
[PROOF STATE]
proof (chain)
picking this:
index l y < index l x
index l x < 2
[PROOF STEP]
have k: "index l x = 1" "index l y = 0"
[PROOF STATE]
proof (prove)
using this:
index l y < index l x
index l x < 2

goal (1 subgoal):
 1. index l x = 1 &&& index l y = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index l x = 1
index l y = 0

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
index l x = 1
index l y = 0
[PROOF STEP]
have g: "x = l ! 1" "y = l ! 0"
[PROOF STATE]
proof (prove)
using this:
index l x = 1
index l y = 0

goal (1 subgoal):
 1. x = l ! 1 &&& y = l ! 0
[PROOF STEP]
using k nth_index assms(1)
[PROOF STATE]
proof (prove)
using this:
index l x = 1
index l y = 0
index l x = 1
index l y = 0
?x \<in> set ?xs \<Longrightarrow> ?xs ! index ?xs ?x = ?x
set l = {x, y}

goal (1 subgoal):
 1. x = l ! 1 &&& y = l ! 0
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
x = l ! 1
y = l ! 0

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "x < y in swap 0 l
      = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0)
            \<or>  x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
apply(rule before_in_swap)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. dist_perm l ?ys
 2. Suc 0 < length l
[PROOF STEP]
apply(fact assms(4))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
length l = 2

goal (1 subgoal):
 1. Suc 0 < length l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = (x = l ! Suc 0 \<and> y = l ! 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> x < y in l

goal (1 subgoal):
 1. (x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x < y in l \<and> \<not> (x = l ! 0 \<and> y = l ! Suc 0) \<or> x = l ! Suc 0 \<and> y = l ! 0) = (x = l ! Suc 0 \<and> y = l ! 0)

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
have "\<dots> = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x = l ! Suc 0 \<and> y = l ! 0) = True
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
x = l ! 1
y = l ! 0

goal (1 subgoal):
 1. (x = l ! Suc 0 \<and> y = l ! 0) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x = l ! Suc 0 \<and> y = l ! 0) = True

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l = True
[PROOF STEP]
have "x < y in (swap 0) l"
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l = True

goal (1 subgoal):
 1. x < y in swap 0 l
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l

goal (1 subgoal):
 1. \<not> x < y in l \<Longrightarrow> x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < y in swap 0 l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
x < y in swap 0 l
\<not> x < y in l

goal (1 subgoal):
 1. x < y in swap 0 l = (\<not> x < y in l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < y in swap 0 l = (\<not> x < y in l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma R36_a [simp]: "pmf (sds R36) a = 1/2" and R36_b [simp]: "pmf (sds R36) b = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (sds R36) a = 1 / 2 &&& pmf (sds R36) b = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. pmf (sds R36) a = 1 / 2
 2. pmf (sds R36) b = 0
[PROOF STEP]
from R10_R36.strategyproofness(1) lottery_conditions[OF R36.wf]
[PROOF STATE]
proof (chain)
picking this:
pmf (sds R36) a + pmf (sds R36) b \<le> pmf (sds R10) d + pmf (sds R10) c
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1
[PROOF STEP]
have "pmf (sds R36) a + pmf (sds R36) b \<le> 1/2"
[PROOF STATE]
proof (prove)
using this:
pmf (sds R36) a + pmf (sds R36) b \<le> pmf (sds R10) d + pmf (sds R10) c
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1

goal (1 subgoal):
 1. pmf (sds R36) a + pmf (sds R36) b \<le> 1 / 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R36) a + pmf (sds R36) b \<le> 1 / 2

goal (2 subgoals):
 1. pmf (sds R36) a = 1 / 2
 2. pmf (sds R36) b = 0
[PROOF STEP]
with R36_R10.strategyproofness(1) lottery_conditions[OF R36.wf]
[PROOF STATE]
proof (chain)
picking this:
(pmf (sds R10) d < pmf (sds R36) a \<or> pmf (sds R10) d + pmf (sds R10) c < pmf (sds R36) a + pmf (sds R36) b) \<or> pmf (sds R10) d = pmf (sds R36) a \<and> pmf (sds R10) d + pmf (sds R10) c = pmf (sds R36) a + pmf (sds R36) b
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1
pmf (sds R36) a + pmf (sds R36) b \<le> 1 / 2
[PROOF STEP]
show "pmf (sds R36) a = 1/2" "pmf (sds R36) b = 0"
[PROOF STATE]
proof (prove)
using this:
(pmf (sds R10) d < pmf (sds R36) a \<or> pmf (sds R10) d + pmf (sds R10) c < pmf (sds R36) a + pmf (sds R36) b) \<or> pmf (sds R10) d = pmf (sds R36) a \<and> pmf (sds R10) d + pmf (sds R10) c = pmf (sds R36) a + pmf (sds R36) b
0 \<le> pmf (sds R36) a
0 \<le> pmf (sds R36) b
0 \<le> pmf (sds R36) c
0 \<le> pmf (sds R36) d
pmf (sds R36) a + pmf (sds R36) b + pmf (sds R36) c + pmf (sds R36) d = 1
pmf (sds R36) a + pmf (sds R36) b \<le> 1 / 2

goal (1 subgoal):
 1. pmf (sds R36) a = 1 / 2 &&& pmf (sds R36) b = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pmf (sds R36) a = 1 / 2
pmf (sds R36) b = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "float_of 2 < float_of 3 + float_of 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Double.float_of 2 < Double.float_of 3 + Double.float_of 4
[PROOF STEP]
by eval


[STATEMENT]
lemma is_finite_double_eq:
  "is_finite_Float TYPE((11, 52)float) f \<longleftrightarrow>
    (let e = Float.exponent f; bm = bitlen (abs (mantissa f))
    in (bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_finite_Float TYPE((11, 52) IEEE.float) f = (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e)
[PROOF STEP]
unfolding is_finite_Float_eq
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> int (Suc LENGTH(52)) \<and> bm \<le> 2 ^ (LENGTH(11) - 1) - e \<and> 1 - 2 ^ (LENGTH(11) - 1) - int LENGTH(52) < e) = (let e = Float.exponent f; bm = bitlen \<bar>mantissa f\<bar> in bm \<le> 53 \<and> e + bm < 1025 \<and> - 1075 < e)
[PROOF STEP]
by (auto simp: Let_def)


[STATEMENT]
lemma "i<0 \<longrightarrow> [[]!i] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < 0 \<longrightarrow> [[] ! i] = []
[PROOF STEP]
by auto


[STATEMENT]
theorem elements_matrix_distribution2:
fixes A1 A2 B1 B2 i j
assumes wf1:"mat (row_length A1) (length A1) A1"
   and wf2:"mat (row_length A2) (length A2) A2"
   and wf3:"mat (row_length B1) (length B1) B1"
   and wf4:"mat (row_length B2) (length B2) B2"
   and matchAA:"length A1 = row_length A2"
   and matchBB:"length B1 = row_length B2"
   and non_Nil:"(A1 \<noteq> [])\<and>(A2 \<noteq> [])\<and>(B1 \<noteq> [])\<and>(B2 \<noteq> [])"
         and i:"i<(row_length A1)*(row_length B1)" and j:"j< (length A2)*(length B2)"
shows
"((A1 \<otimes> B1)\<circ>(A2 \<otimes> B2))!j!i
  =  scalar_product
          (vec_vec_Tensor
                    (row A1 (i div row_length B1))
                    (row B1 (i mod row_length B1)))
          (vec_vec_Tensor
                    (col A2 (j div length B2))
                    (col B2 (j mod length B2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 1:"mat
              ((row_length A1)*(row_length B1))
              ((length A1)*(length B1))
                                   (A1 \<otimes> B1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
[PROOF STEP]
using wf1 wf3 well_defined_Tensor
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length B1) (length B1) B1
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<Longrightarrow> mat (row_length ?M1.0 * row_length ?M2.0) (length ?M1.0 * length ?M2.0) (?M1.0 \<otimes> ?M2.0)

goal (1 subgoal):
 1. mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 2:"mat
                   ((row_length A2)*(row_length B2))
                   ((length A2)*(length B2))
                                   (A2 \<otimes> B2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
[PROOF STEP]
using wf2 wf4 well_defined_Tensor
[PROOF STATE]
proof (prove)
using this:
mat (row_length A2) (length A2) A2
mat (row_length B2) (length B2) B2
mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<Longrightarrow> mat (row_length ?M1.0 * row_length ?M2.0) (length ?M1.0 * length ?M2.0) (?M1.0 \<otimes> ?M2.0)

goal (1 subgoal):
 1. mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have 3:"((length A1)*(length B1))
                           = ((row_length A2)*(row_length B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
using matchAA matchBB
[PROOF STATE]
proof (prove)
using this:
length A1 = row_length A2
length B1 = row_length B2

goal (1 subgoal):
 1. length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length A1 * length B1 = row_length A2 * row_length B2

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2
[PROOF STEP]
have 4:"((A1\<otimes>B1)\<circ>(A2\<otimes>B2))!j!i
                        = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)"
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
[PROOF STEP]
using i j matrix_mult_index non_Nil mat_mult_index
                    row_length_mat scalar_product_def
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1 * row_length B1) (length A1 * length B1) (A1 \<otimes> B1)
mat (row_length A2 * row_length B2) (length A2 * length B2) (A2 \<otimes> B2)
length A1 * length B1 = row_length A2 * row_length B2
i < row_length A1 * row_length B1
j < length A2 * length B2
\<lbrakk>?m1.0 \<noteq> []; mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < ?nr; ?j < ?nc\<rbrakk> \<Longrightarrow> (?m1.0 \<circ> ?m2.0) ! ?j ! ?i = scalar_product (row ?m1.0 ?i) (col ?m2.0 ?j)
A1 \<noteq> [] \<and> A2 \<noteq> [] \<and> B1 \<noteq> [] \<and> B2 \<noteq> []
\<lbrakk>mat ?nr ?n ?m1.0; mat ?n ?nc ?m2.0; ?i < ?nr; ?j < ?nc\<rbrakk> \<Longrightarrow> mat_multI ?ze ?pl ?ti ?nr ?m1.0 ?m2.0 ! ?j ! ?i = scalar_prodI ?ze ?pl ?ti (row ?m1.0 ?i) (col ?m2.0 ?j)
row_length (?m1.0 \<otimes> ?m2.0) = row_length ?m1.0 * row_length ?m2.0
scalar_product ?v ?w = scalar_prodI zer (+) (*) ?v ?w

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have "(row (A1 \<otimes> B1) i)
                  =  vec_vec_Tensor
                           (row A1 (i div row_length B1))
                           (row B1 (i mod row_length B1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
[PROOF STEP]
using  wf1 wf3 i effective_row_formula
[PROOF STATE]
proof (prove)
using this:
mat (row_length A1) (length A1) A1
mat (row_length B1) (length B1) B1
i < row_length A1 * row_length B1
\<lbrakk>?i < row_length ?M1.0 * row_length ?M2.0; mat (row_length ?M1.0) (length ?M1.0) ?M1.0; mat (row_length ?M2.0) (length ?M2.0) ?M2.0\<rbrakk> \<Longrightarrow> row (?M1.0 \<otimes> ?M2.0) ?i = vec_vec_Tensor (row ?M1.0 (?i div row_length ?M2.0)) (row ?M2.0 (?i mod row_length ?M2.0))

goal (1 subgoal):
 1. row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
have " col (A2 \<otimes> B2) j =  vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))
[PROOF STEP]
using wf2 wf4 j col_formula
[PROOF STATE]
proof (prove)
using this:
mat (row_length A2) (length A2) A2
mat (row_length B2) (length B2) B2
j < length A2 * length B2
\<forall>j. j < length ?M1.0 * length ?M2.0 \<and> mat (row_length ?M1.0) (length ?M1.0) ?M1.0 \<and> mat (row_length ?M2.0) (length ?M2.0) ?M2.0 \<longrightarrow> col (?M1.0 \<otimes> ?M2.0) j = vec_vec_Tensor (col ?M1.0 (j div length ?M2.0)) (col ?M2.0 (j mod length ?M2.0))

goal (1 subgoal):
 1. col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (row (A1 \<otimes> B1) i) (col (A2 \<otimes> B2) j)
row (A1 \<otimes> B1) i = vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))
col (A2 \<otimes> B2) j = vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2))

goal (1 subgoal):
 1. ((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
((A1 \<otimes> B1) \<circ> (A2 \<otimes> B2)) ! j ! i = scalar_product (vec_vec_Tensor (row A1 (i div row_length B1)) (row B1 (i mod row_length B1))) (vec_vec_Tensor (col A2 (j div length B2)) (col B2 (j mod length B2)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma all_edges_between_disjoint_family_on1:
  assumes "disjoint R"
  shows "disjoint_family_on (\<lambda>X. all_edges_between X Y) R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. disjoint_family_on (\<lambda>X. all_edges_between X Y) R
[PROOF STEP]
by (metis (no_types, lifting) all_edges_between_disjnt1 assms disjnt_def disjoint_family_on_def pairwiseD)


[STATEMENT]
lemma subgraph_trans:
  assumes "graph_system V E"
  assumes "graph_system V' E'"
  assumes "graph_system V'' E''"
  shows "subgraph V'' E'' V' E' \<Longrightarrow> subgraph V' E' V E \<Longrightarrow> subgraph V'' E'' V E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>subgraph V'' E'' V' E'; subgraph V' E' V E\<rbrakk> \<Longrightarrow> subgraph V'' E'' V E
[PROOF STEP]
by (meson assms(1) assms(3) is_subgraphI subgraph.edges_ss subgraph.verts_ss subset_trans)


[STATEMENT]
lemma meet_char: "a \<^bold>\<preceq> b \<longleftrightarrow> a \<^bold>\<and> b \<^bold>\<approx> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a \<^bold>\<and> b) w = a w)
[PROOF STEP]
unfolding conn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<^bold>\<succeq> a) = (\<forall>w. (a w \<and> b w) = a w)
[PROOF STEP]
by blast


[STATEMENT]
lemma box_omega_unfold_n:
  "|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y) = n(y) * |n(y) * x]|x\<^sup>\<omega> \<squnion> x\<^sup>\<star>]n(y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y = n y * | n y * x ] | x\<^sup>\<omega> \<squnion> x\<^sup>\<star> ] n y
[PROOF STEP]
by (smt an_export an_n_L box_diamond diamond_box diamond_omega_unfold_an n_an_def n_export)


[STATEMENT]
lemma norm_transfer[transfer_rule]:
  "(A ===> (=)) norm norm"
  if [transfer_rule]: "(A ===> A ===> (=)) inner inner"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=)) norm norm
[PROOF STEP]
unfolding norm_eq_sqrt_inner
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=)) (\<lambda>x. sqrt (x \<bullet> x)) (\<lambda>x. sqrt (x \<bullet> x))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma uniformity_transfer[transfer_rule]:
  "(rel_filter (rel_prod A A)) uniformity uniformity"
  if [transfer_rule]: "bi_total A"  "bi_unique A" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_filter (rel_prod A A) uniformity uniformity
[PROOF STEP]
unfolding uniformity_dist
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_filter (rel_prod A A) (INF e\<in>{0<..}. principal {(x, y). dist x y < e}) (INF e\<in>{0<..}. principal {(x, y). dist x y < e})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma c_tl_aux3: "c_tl u = (sgn1 ((c_len u) - 1))*((c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1)" (is "_ = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S1: "u=0 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2: "u>0 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
assume A1: "u>0"
[PROOF STATE]
proof (state)
this:
0 < u

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2_1: "c_len u = 1 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by (simp add: c_tl_aux1)
[PROOF STATE]
proof (state)
this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
have S2_2: "c_len u \<noteq> 1 \<Longrightarrow> ?thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
assume A2_2_1: "c_len u \<noteq> 1"
[PROOF STATE]
proof (state)
this:
c_len u \<noteq> 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
0 < u
[PROOF STEP]
have S2_2_1: "c_len u > 0"
[PROOF STATE]
proof (prove)
using this:
0 < u

goal (1 subgoal):
 1. 0 < c_len u
[PROOF STEP]
by (rule c_len_3)
[PROOF STATE]
proof (state)
this:
0 < c_len u

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from A2_2_1 S2_2_1
[PROOF STATE]
proof (chain)
picking this:
c_len u \<noteq> 1
0 < c_len u
[PROOF STEP]
have S2_2_2: "c_len u > 1"
[PROOF STATE]
proof (prove)
using this:
c_len u \<noteq> 1
0 < c_len u

goal (1 subgoal):
 1. 1 < c_len u
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
1 < c_len u

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
1 < c_len u
[PROOF STEP]
have S2_2_3: "c_len u - 1 > 0"
[PROOF STATE]
proof (prove)
using this:
1 < c_len u

goal (1 subgoal):
 1. 0 < c_len u - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < c_len u - 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
0 < c_len u - 1
[PROOF STEP]
have S2_2_4: "sgn1 (c_len u - 1)=1"
[PROOF STATE]
proof (prove)
using this:
0 < c_len u - 1

goal (1 subgoal):
 1. sgn1 (c_len u - 1) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn1 (c_len u - 1) = 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_4
[PROOF STATE]
proof (chain)
picking this:
sgn1 (c_len u - 1) = 1
[PROOF STEP]
have S2_2_5: "?R = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"
[PROOF STATE]
proof (prove)
using this:
sgn1 (c_len u - 1) = 1

goal (1 subgoal):
 1. sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_2
[PROOF STATE]
proof (chain)
picking this:
1 < c_len u
[PROOF STEP]
have S2_2_6: "c_tl u = (c_pair (c_len u - (2::nat)) (c_snd (c_snd (u-(1::nat))))) + 1"
[PROOF STATE]
proof (prove)
using this:
1 < c_len u

goal (1 subgoal):
 1. c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
by (rule c_tl_aux2)
[PROOF STATE]
proof (state)
this:
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_2_5 S2_2_6
[PROOF STATE]
proof (chain)
picking this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1) = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1
c_tl u = c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. 0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S2_1 S2_2
[PROOF STATE]
proof (chain)
picking this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_len u = 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
c_len u \<noteq> 1 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
from S1 S2
[PROOF STATE]
proof (chain)
picking this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u = 0 \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
0 < u \<Longrightarrow> c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal (1 subgoal):
 1. c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
c_tl u = sgn1 (c_len u - 1) * (c_pair (c_len u - 2) (c_snd (c_snd (u - 1))) + 1)

goal:
No subgoals!
[PROOF STEP]
qed