[STATEMENT]
lemma COMB_pairwise: "pairwise (COMB [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List_Factoring.pairwise (COMB [])
[PROOF STEP]
proof(rule pairwise_property_lemma, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>init qs x y. \<lbrakk>distinct init; qs \<in> {xs. set xs \<subseteq> set init}; (x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}; x \<noteq> y\<rbrakk> \<Longrightarrow> Pbefore_in x y (COMB []) qs init = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})
 2. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
case (1 init qs x y)
[PROOF STATE]
proof (state)
this:
distinct init
qs \<in> {xs. set xs \<subseteq> set init}
(x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
x \<noteq> y

goal (2 subgoals):
 1. \<And>init qs x y. \<lbrakk>distinct init; qs \<in> {xs. set xs \<subseteq> set init}; (x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}; x \<noteq> y\<rbrakk> \<Longrightarrow> Pbefore_in x y (COMB []) qs init = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})
 2. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct init
qs \<in> {xs. set xs \<subseteq> set init}
(x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
x \<noteq> y
[PROOF STEP]
have qsininit: "set qs \<subseteq> set init"
[PROOF STATE]
proof (prove)
using this:
distinct init
qs \<in> {xs. set xs \<subseteq> set init}
(x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}
x \<noteq> y

goal (1 subgoal):
 1. set qs \<subseteq> set init
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set qs \<subseteq> set init

goal (2 subgoals):
 1. \<And>init qs x y. \<lbrakk>distinct init; qs \<in> {xs. set xs \<subseteq> set init}; (x, y) \<in> {(x, y). x \<in> set init \<and> y \<in> set init \<and> x \<noteq> y}; x \<noteq> y\<rbrakk> \<Longrightarrow> Pbefore_in x y (COMB []) qs init = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})
 2. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
show "Pbefore_in x y (COMB []) qs init
        = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Pbefore_in x y (COMB []) qs init = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})
[PROOF STEP]
unfolding Pbefore_in_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>p. x < y in fst p) (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) qs) = map_pmf (\<lambda>p. x < y in fst p) (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
apply(subst config_rand_COMB)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>p. x < y in fst p) (bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))) = map_pmf (\<lambda>p. x < y in fst p) (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}))
[PROOF STEP]
apply(subst config_rand_COMB)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_pmf (\<lambda>p. x < y in fst p) (bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2)))))) = map_pmf (\<lambda>p. x < y in fst p) (bernoulli_pmf (8 / 10) \<bind> (\<lambda>b. Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(b1, b2). Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if b then (b1, Inl b2) else (t1, Inr t2))))))
[PROOF STEP]
apply(simp only: map_pmf_def  bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bernoulli_pmf (8 / 10) \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))) = bernoulli_pmf (8 / 10) \<bind> (\<lambda>xa. Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))))
[PROOF STEP]
apply(rule bind_pmf_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. bernoulli_pmf (8 / 10) = bernoulli_pmf (8 / 10)
 2. \<And>xa. xa \<in> set_pmf (bernoulli_pmf (8 / 10)) \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> set_pmf (bernoulli_pmf (8 / 10)) \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(simp only: set_pmf_bernoulli)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. xa \<in> UNIV \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(case_tac xa)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>xa \<in> UNIV; xa\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
 2. \<And>xa. \<lbrakk>xa \<in> UNIV; \<not> xa\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xa. xa \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. return_pmf (fst xa, Inl (snd xa)) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (BIT_init (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xa. return_pmf (fst xa, Inl (snd xa)) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
 2. \<And>xa. \<lbrakk>xa \<in> UNIV; \<not> xa\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
using BIT_pairwise'[OF qsininit 1(3,4,1), unfolded Pbefore_in_def map_pmf_def]
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))

goal (2 subgoals):
 1. \<And>xa. xa \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (BIT_init init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. return_pmf (fst xa, Inl (snd xa)) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (BIT_init (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xa. return_pmf (fst xa, Inl (snd xa)) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
 2. \<And>xa. \<lbrakk>xa \<in> UNIV; \<not> xa\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>xa \<in> UNIV; \<not> xa\<rbrakk> \<Longrightarrow> Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))) = Partial_Cost_Model.config'_rand BIT (fst BIT (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xaa. (case xaa of (b1, b2) \<Rightarrow> Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>(t1, t2). return_pmf (if xa then (b1, Inl b2) else (t1, Inr t2)))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)))
[PROOF STEP]
apply(simp add: split_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<not> xa \<Longrightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) (return_pmf (fst (rTS []) init) \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>p. return_pmf (fst p, Inr (snd p))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) = Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) (return_pmf (fst (rTS []) (Lxy init {x, y})) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>p. return_pmf (fst p, Inr (snd p))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))
[PROOF STEP]
using TS_pairwise'[OF 1(2,3,4,1), unfolded Pbefore_in_def map_pmf_def]
[PROOF STATE]
proof (prove)
using this:
Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) init \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) = Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS [])) (fst (Partial_Cost_Model.embed (rTS [])) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))

goal (1 subgoal):
 1. \<And>xa. \<not> xa \<Longrightarrow> Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) (return_pmf (fst (rTS []) init) \<bind> (\<lambda>is. return_pmf (init, is))) qs \<bind> (\<lambda>p. return_pmf (fst p, Inr (snd p))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa)) = Partial_Cost_Model.config'_rand (\<lambda>s. return_pmf (fst (rTS []) s), \<lambda>s r. return_pmf (snd (rTS []) s r)) (return_pmf (fst (rTS []) (Lxy init {x, y})) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<bind> (\<lambda>p. return_pmf (fst p, Inr (snd p))) \<bind> (\<lambda>xa. return_pmf (x < y in fst xa))
[PROOF STEP]
by(simp add: bind_return_pmf bind_assoc_pmf)
[PROOF STATE]
proof (state)
this:
Pbefore_in x y (COMB []) qs init = Pbefore_in x y (COMB []) (Lxy qs {x, y}) (Lxy init {x, y})

goal (1 subgoal):
 1. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
case (2 xa r)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>xa r. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
using COMB_no_paid
[PROOF STATE]
proof (prove)
using this:
\<forall>((free, paid), t)\<in>set_pmf (snd (COMB []) (?s, ?is) ?q). paid = []

goal (1 subgoal):
 1. \<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []
[PROOF STEP]
by (metis (mono_tags) case_prod_unfold surj_pair)
[PROOF STATE]
proof (state)
this:
\<forall>z\<in>set_pmf (snd (COMB []) xa r). snd (fst z) = []

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_config_TS: "finite (set_pmf (config'' (embed (rTS h)) qs init n))" (is "finite ?D")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (take n qs)))
[PROOF STEP]
apply(subst config_embed)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (return_pmf (TSdet init h qs n)))
[PROOF STEP]
by(simp)


[STATEMENT]
lemma COMB_has_finite_config_set: assumes [simp]: "distinct init"
      and "set qs \<subseteq> set init"
      shows "finite (set_pmf (config_rand (COMB h) init qs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs))
[PROOF STEP]
from finite_config_TS[where n="length qs" and qs=qs]
      finite_config_BIT[OF assms(1)]
[PROOF STATE]
proof (chain)
picking this:
finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) (fst (Partial_Cost_Model.embed (rTS ?h)) ?init \<bind> (\<lambda>is. return_pmf (?init, is))) (take (length qs) qs)))
finite (set_pmf (Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) ?qs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS ?h)) (fst (Partial_Cost_Model.embed (rTS ?h)) ?init \<bind> (\<lambda>is. return_pmf (?init, is))) (take (length qs) qs)))
finite (set_pmf (Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) ?qs))

goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs))
[PROOF STEP]
apply(subst obligation1'')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>h init. finite (set_pmf (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) (take (length qs) qs))); \<And>qs. finite (set_pmf (Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs))\<rbrakk> \<Longrightarrow> finite (set_pmf (map_pmf noc (Sum_pmf (8 / 10) (Partial_Cost_Model.config'_rand BIT (fst BIT init \<bind> (\<lambda>is. return_pmf (init, is))) qs) (Partial_Cost_Model.config'_rand (Partial_Cost_Model.embed (rTS h)) (fst (Partial_Cost_Model.embed (rTS h)) init \<bind> (\<lambda>is. return_pmf (init, is))) qs))))
[PROOF STEP]
by(simp add: Sum_pmf_def)
[PROOF STATE]
proof (state)
this:
finite (set_pmf (Partial_Cost_Model.config'_rand (COMB h) (fst (COMB h) init \<bind> (\<lambda>is. return_pmf (init, is))) qs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem COMB_competitive: "\<forall>s0\<in>{x::nat list. distinct x \<and> x\<noteq>[]}.
   \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}.
             T\<^sub>p_on_rand (COMB []) s0 qs \<le> ((8::nat)/(5::nat)) *  T\<^sub>p_opt s0 qs + b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> real 8 / real 5 * real (T\<^sub>p_opt s0 qs) + b
[PROOF STEP]
proof(rule factoringlemma_withconstant, goal_cases)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. List_Factoring.pairwise (COMB [])
 5. \<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
 6. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 7. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
case 5
[PROOF STATE]
proof (state)
this:

goal (7 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. List_Factoring.pairwise (COMB [])
 5. \<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
 6. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 7. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s0. \<lbrakk>distinct s0; s0 \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
[PROOF STEP]
case (1 init)
[PROOF STATE]
proof (state)
this:
distinct init
init \<noteq> []

goal (1 subgoal):
 1. \<And>s0. \<lbrakk>distinct s0; s0 \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
[PROOF STEP]
note out=this
[PROOF STATE]
proof (state)
this:
distinct init
init \<noteq> []

goal (1 subgoal):
 1. \<And>s0. \<lbrakk>distinct s0; s0 \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b
[PROOF STEP]
apply(rule exI[where x=2])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 2 \<and> (\<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + 2)
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qs. set qs \<subseteq> set init \<longrightarrow> (\<forall>a b. a \<in> set init \<and> b \<in> set init \<and> a < b \<longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2)
[PROOF STEP]
proof (safe, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
case (1 qs a b)
[PROOF STATE]
proof (state)
this:
set qs \<subseteq> set init
a \<in> set init
b \<in> set init
a < b

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set qs \<subseteq> set init
a \<in> set init
b \<in> set init
a < b
[PROOF STEP]
have a: "a\<noteq>b"
[PROOF STATE]
proof (prove)
using this:
set qs \<subseteq> set init
a \<in> set init
b \<in> set init
a < b

goal (1 subgoal):
 1. a \<noteq> b
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a \<noteq> b

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have twist: "{a,b}={b, a}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a, b} = {b, a}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{a, b} = {b, a}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have b1: "set (Lxy qs {a, b}) \<subseteq> {a, b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Lxy qs {a, b}) \<subseteq> {a, b}
[PROOF STEP]
unfolding Lxy_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (filter (\<lambda>z. z \<in> {a, b}) qs) \<subseteq> {a, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (Lxy qs {a, b}) \<subseteq> {a, b}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
with this[unfolded twist]
[PROOF STATE]
proof (chain)
picking this:
set (Lxy qs {b, a}) \<subseteq> {b, a}
set (Lxy qs {a, b}) \<subseteq> {a, b}
[PROOF STEP]
have b2: "set (Lxy qs {b, a}) \<subseteq> {b, a}"
[PROOF STATE]
proof (prove)
using this:
set (Lxy qs {b, a}) \<subseteq> {b, a}
set (Lxy qs {a, b}) \<subseteq> {a, b}

goal (1 subgoal):
 1. set (Lxy qs {b, a}) \<subseteq> {b, a}
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
set (Lxy qs {b, a}) \<subseteq> {b, a}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have "set (Lxy init {a, b}) = {a,b} \<inter> (set init)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (Lxy init {a, b}) = {a, b} \<inter> set init
[PROOF STEP]
apply(induct init)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set (Lxy [] {a, b}) = {a, b} \<inter> set []
 2. \<And>aa init. set (Lxy init {a, b}) = {a, b} \<inter> set init \<Longrightarrow> set (Lxy (aa # init) {a, b}) = {a, b} \<inter> set (aa # init)
[PROOF STEP]
unfolding Lxy_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set (filter (\<lambda>z. z \<in> {a, b}) []) = {a, b} \<inter> set []
 2. \<And>aa init. set (filter (\<lambda>z. z \<in> {a, b}) init) = {a, b} \<inter> set init \<Longrightarrow> set (filter (\<lambda>z. z \<in> {a, b}) (aa # init)) = {a, b} \<inter> set (aa # init)
[PROOF STEP]
by(auto)
[PROOF STATE]
proof (state)
this:
set (Lxy init {a, b}) = {a, b} \<inter> set init

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
with 1
[PROOF STATE]
proof (chain)
picking this:
set qs \<subseteq> set init
a \<in> set init
b \<in> set init
a < b
set (Lxy init {a, b}) = {a, b} \<inter> set init
[PROOF STEP]
have A: "set (Lxy init {a, b}) = {a,b}"
[PROOF STATE]
proof (prove)
using this:
set qs \<subseteq> set init
a \<in> set init
b \<in> set init
a < b
set (Lxy init {a, b}) = {a, b} \<inter> set init

goal (1 subgoal):
 1. set (Lxy init {a, b}) = {a, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (Lxy init {a, b}) = {a, b}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have "finite {a,b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a, b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {a, b}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
from out
[PROOF STATE]
proof (chain)
picking this:
distinct init
init \<noteq> []
[PROOF STEP]
have B: "distinct (Lxy init {a, b})"
[PROOF STATE]
proof (prove)
using this:
distinct init
init \<noteq> []

goal (1 subgoal):
 1. distinct (Lxy init {a, b})
[PROOF STEP]
unfolding Lxy_def
[PROOF STATE]
proof (prove)
using this:
distinct init
init \<noteq> []

goal (1 subgoal):
 1. distinct (filter (\<lambda>z. z \<in> {a, b}) init)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (Lxy init {a, b})

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have C: "length (Lxy init {a, b}) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (Lxy init {a, b}) = 2
[PROOF STEP]
using distinct_card[OF B, unfolded A]
[PROOF STATE]
proof (prove)
using this:
card {a, b} = length (Lxy init {a, b})

goal (1 subgoal):
 1. length (Lxy init {a, b}) = 2
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
card {a, b} = length (Lxy init {a, b})
a \<noteq> b

goal (1 subgoal):
 1. length (Lxy init {a, b}) = 2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (Lxy init {a, b}) = 2

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
have "{xs. set xs = {a,b} \<and> distinct xs \<and> length xs =(2::nat)}
                    = { [a,b], [b,a] }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {xs. set xs = {a, b} \<and> distinct xs \<and> length xs = 2} = {[a, b], [b, a]}
[PROOF STEP]
apply(auto simp: a a[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
proof (goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
case (1 xs)
[PROOF STATE]
proof (state)
this:
xs \<noteq> [a, b]
set xs = {a, b}
distinct xs
length xs = 2

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
from 1(4)
[PROOF STATE]
proof (chain)
picking this:
length xs = 2
[PROOF STEP]
obtain x xs' where r:"xs=x#xs'"
[PROOF STATE]
proof (prove)
using this:
length xs = 2

goal (1 subgoal):
 1. (\<And>x xs'. xs = x # xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc_length_conv add_2_eq_Suc' append_Nil length_append)
[PROOF STATE]
proof (state)
this:
xs = x # xs'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
with 1(4)
[PROOF STATE]
proof (chain)
picking this:
length xs = 2
xs = x # xs'
[PROOF STEP]
have "length xs' = 1"
[PROOF STATE]
proof (prove)
using this:
length xs = 2
xs = x # xs'

goal (1 subgoal):
 1. length xs' = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length xs' = 1

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length xs' = 1
[PROOF STEP]
obtain y where s: "[y] = xs'"
[PROOF STATE]
proof (prove)
using this:
length xs' = 1

goal (1 subgoal):
 1. (\<And>y. [y] = xs' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis One_nat_def length_0_conv length_Suc_conv)
[PROOF STATE]
proof (state)
this:
[y] = xs'

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
from r s
[PROOF STATE]
proof (chain)
picking this:
xs = x # xs'
[y] = xs'
[PROOF STEP]
have t: "[x,y] = xs"
[PROOF STATE]
proof (prove)
using this:
xs = x # xs'
[y] = xs'

goal (1 subgoal):
 1. [x, y] = xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[x, y] = xs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[x, y] = xs

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
from t 1(1)
[PROOF STATE]
proof (chain)
picking this:
[x, y] = xs
xs \<noteq> [a, b]
[PROOF STEP]
have "x=b"
[PROOF STATE]
proof (prove)
using this:
[x, y] = xs
xs \<noteq> [a, b]

goal (1 subgoal):
 1. x = b
[PROOF STEP]
using doubleton_eq_iff 1(2)
[PROOF STATE]
proof (prove)
using this:
[x, y] = xs
xs \<noteq> [a, b]
({?a, ?b} = {?c, ?d}) = (?a = ?c \<and> ?b = ?d \<or> ?a = ?d \<and> ?b = ?c)
set xs = {a, b}

goal (1 subgoal):
 1. x = b
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
x = b

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = b

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
from t 1(1)
[PROOF STATE]
proof (chain)
picking this:
[x, y] = xs
xs \<noteq> [a, b]
[PROOF STEP]
have "y=a"
[PROOF STATE]
proof (prove)
using this:
[x, y] = xs
xs \<noteq> [a, b]

goal (1 subgoal):
 1. y = a
[PROOF STEP]
using doubleton_eq_iff 1(2)
[PROOF STATE]
proof (prove)
using this:
[x, y] = xs
xs \<noteq> [a, b]
({?a, ?b} = {?c, ?d}) = (?a = ?c \<and> ?b = ?d \<or> ?a = ?d \<and> ?b = ?c)
set xs = {a, b}

goal (1 subgoal):
 1. y = a
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
y = a

goal (1 subgoal):
 1. \<And>x. \<lbrakk>x \<noteq> [a, b]; set x = {a, b}; distinct x; length x = 2\<rbrakk> \<Longrightarrow> x = [b, a]
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[x, y] = xs
x = b
y = a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[x, y] = xs
x = b
y = a

goal (1 subgoal):
 1. xs = [b, a]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs = [b, a]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{xs. set xs = {a, b} \<and> distinct xs \<and> length xs = 2} = {[a, b], [b, a]}

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
with A B C
[PROOF STATE]
proof (chain)
picking this:
set (Lxy init {a, b}) = {a, b}
distinct (Lxy init {a, b})
length (Lxy init {a, b}) = 2
{xs. set xs = {a, b} \<and> distinct xs \<and> length xs = 2} = {[a, b], [b, a]}
[PROOF STEP]
have pos: "(Lxy init {a, b}) = [a,b]
                  \<or> (Lxy init {a, b}) = [b,a]"
[PROOF STATE]
proof (prove)
using this:
set (Lxy init {a, b}) = {a, b}
distinct (Lxy init {a, b})
length (Lxy init {a, b}) = 2
{xs. set xs = {a, b} \<and> distinct xs \<and> length xs = 2} = {[a, b], [b, a]}

goal (1 subgoal):
 1. Lxy init {a, b} = [a, b] \<or> Lxy init {a, b} = [b, a]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Lxy init {a, b} = [a, b] \<or> Lxy init {a, b} = [b, a]

goal (1 subgoal):
 1. \<And>qs a b. \<lbrakk>set qs \<subseteq> set init; a \<in> set init; b \<in> set init; a < b\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
apply(cases "(Lxy init {a, b}) = [a,b]")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Lxy init {a, b} = [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
 2. Lxy init {a, b} \<noteq> [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Lxy init {a, b} = [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [a, b] \<bind> (\<lambda>is. return_pmf ([a, b], is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt [a, b] (Lxy qs {a, b})) / 5 + 2
 2. Lxy init {a, b} \<noteq> [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
using COMB_OPT2'[OF a b1] a
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [a, b] \<bind> (\<lambda>is. return_pmf ([a, b], is))) (Lxy qs {a, b}) \<le> 16 / 10 * real (T\<^sub>p_opt [a, b] (Lxy qs {a, b})) + 16 / 10
a \<noteq> b

goal (2 subgoals):
 1. Lxy init {a, b} = [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [a, b] \<bind> (\<lambda>is. return_pmf ([a, b], is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt [a, b] (Lxy qs {a, b})) / 5 + 2
 2. Lxy init {a, b} \<noteq> [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lxy init {a, b} \<noteq> [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
using pos
[PROOF STATE]
proof (prove)
using this:
Lxy init {a, b} = [a, b] \<or> Lxy init {a, b} = [b, a]

goal (1 subgoal):
 1. Lxy init {a, b} \<noteq> [a, b] \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<noteq> a; Lxy init {a, b} = [b, a]\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [b, a] \<bind> (\<lambda>is. return_pmf ([b, a], is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt [b, a] (Lxy qs {a, b})) / 5 + 2
[PROOF STEP]
unfolding twist
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<noteq> a; Lxy init {b, a} = [b, a]\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [b, a] \<bind> (\<lambda>is. return_pmf ([b, a], is))) (Lxy qs {b, a}) \<le> 8 * real (T\<^sub>p_opt [b, a] (Lxy qs {b, a})) / 5 + 2
[PROOF STEP]
using COMB_OPT2'[OF a[symmetric] b2]
[PROOF STATE]
proof (prove)
using this:
T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [b, a] \<bind> (\<lambda>is. return_pmf ([b, a], is))) (Lxy qs {b, a}) \<le> 16 / 10 * real (T\<^sub>p_opt [b, a] (Lxy qs {b, a})) + 16 / 10

goal (1 subgoal):
 1. \<lbrakk>b \<noteq> a; Lxy init {b, a} = [b, a]\<rbrakk> \<Longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) [b, a] \<bind> (\<lambda>is. return_pmf ([b, a], is))) (Lxy qs {b, a}) \<le> 8 * real (T\<^sub>p_opt [b, a] (Lxy qs {b, a})) / 5 + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {a, b}) \<bind> (\<lambda>is. return_pmf (Lxy init {a, b}, is))) (Lxy qs {a, b}) \<le> 8 * real (T\<^sub>p_opt (Lxy init {a, b}) (Lxy qs {a, b})) / 5 + 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set init}. \<forall>(x, y)\<in>{(x, y). x \<in> set init \<and> y \<in> set init \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy init {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy init {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy init {x, y}) (Lxy qs {x, y})) + b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. \<forall>(x, y)\<in>{(x, y). x \<in> set s0 \<and> y \<in> set s0 \<and> x < y}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) (Lxy s0 {x, y}) \<bind> (\<lambda>is. return_pmf (Lxy s0 {x, y}, is))) (Lxy qs {x, y}) \<le> real 8 / real 5 * real (T\<^sub>p_opt (Lxy s0 {x, y}) (Lxy qs {x, y})) + b

goal (6 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. List_Factoring.pairwise (COMB [])
 5. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 6. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. List_Factoring.pairwise (COMB [])
 5. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 6. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:

goal (6 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. List_Factoring.pairwise (COMB [])
 5. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 6. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List_Factoring.pairwise (COMB [])
[PROOF STEP]
using COMB_pairwise
[PROOF STATE]
proof (prove)
using this:
List_Factoring.pairwise (COMB [])

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

goal (5 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 5. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 5. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
case 7
[PROOF STATE]
proof (state)
this:
distinct init_
set qs_ \<subseteq> set init_
x_ < length qs_

goal (5 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
 5. \<And>init qs x. \<lbrakk>distinct init; set qs \<subseteq> set init; x < length qs\<rbrakk> \<Longrightarrow> finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init \<bind> (\<lambda>is. return_pmf (init, is))) (take x qs)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct init_
set qs_ \<subseteq> set init_
x_ < length qs_
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct init_
set qs_ \<subseteq> set init_
x_ < length qs_

goal (1 subgoal):
 1. finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init_ \<bind> (\<lambda>is. return_pmf (init_, is))) (take x_ qs_)))
[PROOF STEP]
apply(subst COMB_has_finite_config_set[OF 7(1)])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct init_; set qs_ \<subseteq> set init_; x_ < length qs_\<rbrakk> \<Longrightarrow> set (take x_ qs_) \<subseteq> set init_
 2. \<lbrakk>distinct init_; set qs_ \<subseteq> set init_; x_ < length qs_\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
using set_take_subset
[PROOF STATE]
proof (prove)
using this:
set (take ?n ?xs) \<subseteq> set ?xs

goal (2 subgoals):
 1. \<lbrakk>distinct init_; set qs_ \<subseteq> set init_; x_ < length qs_\<rbrakk> \<Longrightarrow> set (take x_ qs_) \<subseteq> set init_
 2. \<lbrakk>distinct init_; set qs_ \<subseteq> set init_; x_ < length qs_\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
apply fast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct init_; set qs_ \<subseteq> set init_; x_ < length qs_\<rbrakk> \<Longrightarrow> True
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (set_pmf (Partial_Cost_Model.config'_rand (COMB []) (fst (COMB []) init_ \<bind> (\<lambda>is. return_pmf (init_, is))) (take x_ qs_)))

goal (4 subgoals):
 1. 1 \<le> real 8 / real 5
 2. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. distinct e
 3. \<forall>e\<in>{x. distinct x \<and> x \<noteq> []}. 0 < length e
 4. \<And>is s q. \<forall>((free, paid), uu_)\<in>set_pmf (snd (COMB []) (s, is) q). paid = []
[PROOF STEP]
qed (simp_all add: COMB_no_paid)


[STATEMENT]
theorem COMB_competitive_nice: "compet_rand (COMB []) ((8::nat)/(5::nat)) {x::nat list. distinct x \<and> x\<noteq>[]}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Partial_Cost_Model.compet_rand (COMB []) (real 8 / real 5) {x. distinct x \<and> x \<noteq> []}
[PROOF STEP]
unfolding compet_rand_def static_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>rs. set rs \<subseteq> set s \<longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) s \<bind> (\<lambda>is. return_pmf (s, is))) rs \<le> real 8 / real 5 * real (T\<^sub>p_opt s rs) + b
[PROOF STEP]
using COMB_competitive
[PROOF STATE]
proof (prove)
using this:
\<forall>s0\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>qs\<in>{x. set x \<subseteq> set s0}. T\<^sub>p_on_rand' (COMB []) (fst (COMB []) s0 \<bind> (\<lambda>is. return_pmf (s0, is))) qs \<le> real 8 / real 5 * real (T\<^sub>p_opt s0 qs) + b

goal (1 subgoal):
 1. \<forall>s\<in>{x. distinct x \<and> x \<noteq> []}. \<exists>b\<ge>0. \<forall>rs. set rs \<subseteq> set s \<longrightarrow> T\<^sub>p_on_rand' (COMB []) (fst (COMB []) s \<bind> (\<lambda>is. return_pmf (s, is))) rs \<le> real 8 / real 5 * real (T\<^sub>p_opt s rs) + b
[PROOF STEP]
by simp


[STATEMENT]
lemma dim_gen_eigenspace_order_char_poly: assumes jnf: "jordan_nf A n_as"
  shows "dim_gen_eigenspace A lam k \<le> order lam (char_poly A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_gen_eigenspace A lam k \<le> order lam (char_poly A)
[PROOF STEP]
unfolding jordan_nf_order[OF jnf]  dim_gen_eigenspace[OF jnf]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map (min k) (map fst (filter (\<lambda>(n, e). e = lam) n_as))) \<le> sum_list (map fst (filter (\<lambda>na. snd na = lam) n_as))
[PROOF STEP]
by (induct n_as, auto)


[STATEMENT]
lemma eigenvector_mat_kernel_char_matrix: assumes A: "A \<in> carrier_mat n n"
  and ev: "eigenvector A v lam"
shows "v \<in> mat_kernel (char_matrix A lam)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
using ev[unfolded eigenvector_char_matrix[OF A]] A
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A lam *\<^sub>v v = 0\<^sub>v n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
unfolding mat_kernel_def
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> char_matrix A lam *\<^sub>v v = 0\<^sub>v n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> {v \<in> carrier_vec (dim_col (char_matrix A lam)). char_matrix A lam *\<^sub>v v = 0\<^sub>v (dim_row (char_matrix A lam))}
[PROOF STEP]
by (auto simp: char_matrix_def)


[STATEMENT]
lemma unique_eigenvector_jnf: assumes jnf: "jordan_nf (A :: 'a :: field mat) n_as"
  and ord: "order lam (char_poly A) = 1"
  and ev: "eigenvector A v lam" "eigenvector A w lam"
shows "\<exists> a. v = a \<cdot>\<^sub>v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
let ?cA = "char_matrix A lam"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from similar_matD jnf[unfolded jordan_nf_def]
[PROOF STATE]
proof (chain)
picking this:
similar_mat ?A ?B \<Longrightarrow> \<exists>n P Q. {?A, ?B, P, Q} \<subseteq> carrier_mat n n \<and> P * Q = 1\<^sub>m n \<and> Q * P = 1\<^sub>m n \<and> ?A = P * ?B * Q
0 \<notin> fst ` set n_as \<and> similar_mat A (jordan_matrix n_as)
[PROOF STEP]
obtain n where
    A: "A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
similar_mat ?A ?B \<Longrightarrow> \<exists>n P Q. {?A, ?B, P, Q} \<subseteq> carrier_mat n n \<and> P * Q = 1\<^sub>m n \<and> Q * P = 1\<^sub>m n \<and> ?A = P * ?B * Q
0 \<notin> fst ` set n_as \<and> similar_mat A (jordan_matrix n_as)

goal (1 subgoal):
 1. (\<And>n. A \<in> carrier_mat n n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from dim_gen_eigenspace_order_char_poly[OF jnf, of lam 1, unfolded ord]
[PROOF STATE]
proof (chain)
picking this:
dim_gen_eigenspace A lam 1 \<le> 1
[PROOF STEP]
have dim: "kernel_dim ?cA \<le> 1"
[PROOF STATE]
proof (prove)
using this:
dim_gen_eigenspace A lam 1 \<le> 1

goal (1 subgoal):
 1. kernel_dim (char_matrix A lam) \<le> 1
[PROOF STEP]
unfolding dim_gen_eigenspace_def
[PROOF STATE]
proof (prove)
using this:
kernel_dim (char_matrix A lam ^\<^sub>m 1) \<le> 1

goal (1 subgoal):
 1. kernel_dim (char_matrix A lam) \<le> 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
kernel_dim (char_matrix A lam) \<le> 1

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from eigenvector_mat_kernel_char_matrix[OF A ev(1)]
[PROOF STATE]
proof (chain)
picking this:
v \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
have vk: "v \<in> mat_kernel ?cA"
[PROOF STATE]
proof (prove)
using this:
v \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. v \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
v \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from eigenvector_mat_kernel_char_matrix[OF A ev(2)]
[PROOF STATE]
proof (chain)
picking this:
w \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
have wk: "w \<in> mat_kernel ?cA"
[PROOF STATE]
proof (prove)
using this:
w \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. w \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
w \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from ev[unfolded eigenvector_def] A
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = lam \<cdot>\<^sub>v v
w \<in> carrier_vec (dim_row A) \<and> w \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v w = lam \<cdot>\<^sub>v w
A \<in> carrier_mat n n
[PROOF STEP]
have
    v: "v \<in> carrier_vec n" "v \<noteq> 0\<^sub>v n" and
    w: "w \<in> carrier_vec n" "w \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = lam \<cdot>\<^sub>v v
w \<in> carrier_vec (dim_row A) \<and> w \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v w = lam \<cdot>\<^sub>v w
A \<in> carrier_mat n n

goal (1 subgoal):
 1. (v \<in> carrier_vec n &&& v \<noteq> 0\<^sub>v n) &&& w \<in> carrier_vec n &&& w \<noteq> 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
have cA: "?cA \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_matrix A lam \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. char_matrix A lam \<in> carrier_mat n n
[PROOF STEP]
unfolding char_matrix_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. A + - lam \<cdot>\<^sub>m 1\<^sub>m (dim_row A) \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
char_matrix A lam \<in> carrier_mat n n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
interpret kernel n n ?cA
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix_Kernel.kernel n n (char_matrix A lam)
[PROOF STEP]
by (unfold_locales, rule cA)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from kernel_basis_exists[OF A]
[PROOF STATE]
proof (chain)
picking this:
\<exists>B. finite B \<and> basis B
[PROOF STEP]
obtain B where B: "finite B" "basis B"
[PROOF STATE]
proof (prove)
using this:
\<exists>B. finite B \<and> basis B

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>finite B; basis B\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite B
basis B

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from this[unfolded Ker.basis_def]
[PROOF STATE]
proof (chain)
picking this:
finite B
lin_indpt B \<and> local.span B = mat_kernel (char_matrix A lam) \<and> B \<subseteq> mat_kernel (char_matrix A lam)
[PROOF STEP]
have basis: "mat_kernel ?cA = span B"
[PROOF STATE]
proof (prove)
using this:
finite B
lin_indpt B \<and> local.span B = mat_kernel (char_matrix A lam) \<and> B \<subseteq> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. mat_kernel (char_matrix A lam) = local.span B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span B

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span B

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
assume "card B = 0"
[PROOF STATE]
proof (state)
this:
card B = 0

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
with B basis
[PROOF STATE]
proof (chain)
picking this:
finite B
basis B
mat_kernel (char_matrix A lam) = local.span B
card B = 0
[PROOF STEP]
have bas: "mat_kernel ?cA = local.span {}"
[PROOF STATE]
proof (prove)
using this:
finite B
basis B
mat_kernel (char_matrix A lam) = local.span B
card B = 0

goal (1 subgoal):
 1. mat_kernel (char_matrix A lam) = local.span {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span {}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span {}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
have "\<dots> = {0\<^sub>v n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span {} = {0\<^sub>v n}
[PROOF STEP]
unfolding Ker.span_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {lincomb a A |a A. finite A \<and> A \<subseteq> {} \<and> a \<in> A \<rightarrow> UNIV} = {0\<^sub>v n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span {} = {0\<^sub>v n}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mat_kernel (char_matrix A lam) = {0\<^sub>v n}
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
mat_kernel (char_matrix A lam) = {0\<^sub>v n}

goal (1 subgoal):
 1. False
[PROOF STEP]
using v vk
[PROOF STATE]
proof (prove)
using this:
mat_kernel (char_matrix A lam) = {0\<^sub>v n}
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
v \<in> mat_kernel (char_matrix A lam)

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

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
card B = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
with Ker.dim_basis[OF B] dim
[PROOF STATE]
proof (chain)
picking this:
local.dim = card B
kernel_dim (char_matrix A lam) \<le> 1
card B = 0 \<Longrightarrow> False
[PROOF STEP]
have "card B = Suc 0"
[PROOF STATE]
proof (prove)
using this:
local.dim = card B
kernel_dim (char_matrix A lam) \<le> 1
card B = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. card B = Suc 0
[PROOF STEP]
by (cases "card B", auto)
[PROOF STATE]
proof (state)
this:
card B = Suc 0

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
hence "\<exists> b. B = {b}"
[PROOF STATE]
proof (prove)
using this:
card B = Suc 0

goal (1 subgoal):
 1. \<exists>b. B = {b}
[PROOF STEP]
using card_eq_SucD
[PROOF STATE]
proof (prove)
using this:
card B = Suc 0
card ?A = Suc ?k \<Longrightarrow> \<exists>b B. ?A = insert b B \<and> b \<notin> B \<and> card B = ?k \<and> (?k = 0 \<longrightarrow> B = {})

goal (1 subgoal):
 1. \<exists>b. B = {b}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>b. B = {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>b. B = {b}
[PROOF STEP]
obtain b where Bb: "B = {b}"
[PROOF STATE]
proof (prove)
using this:
\<exists>b. B = {b}

goal (1 subgoal):
 1. (\<And>b. B = {b} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B = {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from B(2)[unfolded Bb Ker.basis_def]
[PROOF STATE]
proof (chain)
picking this:
lin_indpt {b} \<and> local.span {b} = mat_kernel (char_matrix A lam) \<and> {b} \<subseteq> mat_kernel (char_matrix A lam)
[PROOF STEP]
have bk: "b \<in> mat_kernel ?cA"
[PROOF STATE]
proof (prove)
using this:
lin_indpt {b} \<and> local.span {b} = mat_kernel (char_matrix A lam) \<and> {b} \<subseteq> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. b \<in> mat_kernel (char_matrix A lam)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
hence b: "b \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
b \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. b \<in> carrier_vec n
[PROOF STEP]
using cA mat_kernelD(1)
[PROOF STATE]
proof (prove)
using this:
b \<in> mat_kernel (char_matrix A lam)
char_matrix A lam \<in> carrier_mat n n
\<lbrakk>?A \<in> carrier_mat ?nr ?nc; ?v \<in> mat_kernel ?A\<rbrakk> \<Longrightarrow> ?v \<in> carrier_vec ?nc

goal (1 subgoal):
 1. b \<in> carrier_vec n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
b \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from Bb basis
[PROOF STATE]
proof (chain)
picking this:
B = {b}
mat_kernel (char_matrix A lam) = local.span B
[PROOF STEP]
have "mat_kernel ?cA = span {b}"
[PROOF STATE]
proof (prove)
using this:
B = {b}
mat_kernel (char_matrix A lam) = local.span B

goal (1 subgoal):
 1. mat_kernel (char_matrix A lam) = local.span {b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mat_kernel (char_matrix A lam) = local.span {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
have "\<dots> = NC.span {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span {b} = NC.span {b}
[PROOF STEP]
by (rule span_same, insert bk, auto)
[PROOF STATE]
proof (state)
this:
local.span {b} = NC.span {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.span {b} = NC.span {b}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
have "\<dots> \<subseteq> { a \<cdot>\<^sub>v b | a. True}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
assume "x \<in> NC.span {b}"
[PROOF STATE]
proof (state)
this:
x \<in> NC.span {b}

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
from this[unfolded NC.span_def]
[PROOF STATE]
proof (chain)
picking this:
x \<in> {NC.lincomb a A |a A. finite A \<and> A \<subseteq> {b}}
[PROOF STEP]
obtain a A
        where x: "x = NC.lincomb a A" and A: "A \<subseteq> {b}"
[PROOF STATE]
proof (prove)
using this:
x \<in> {NC.lincomb a A |a A. finite A \<and> A \<subseteq> {b}}

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>x = NC.lincomb a A; A \<subseteq> {b}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = NC.lincomb a A
A \<subseteq> {b}

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
hence "A = {} \<or> A = {b}"
[PROOF STATE]
proof (prove)
using this:
x = NC.lincomb a A
A \<subseteq> {b}

goal (1 subgoal):
 1. A = {} \<or> A = {b}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = {} \<or> A = {b}

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
hence "\<exists> a. x = a \<cdot>\<^sub>v b"
[PROOF STATE]
proof (prove)
using this:
A = {} \<or> A = {b}

goal (1 subgoal):
 1. \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A = {} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
 2. A = {b} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
assume "A = {}"
[PROOF STATE]
proof (state)
this:
A = {}

goal (2 subgoals):
 1. A = {} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
 2. A = {b} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = {}

goal (1 subgoal):
 1. \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
A = {}

goal (1 subgoal):
 1. \<exists>aa. NC.lincomb a A = aa \<cdot>\<^sub>v b
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
A = {}
b \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>aa. NC.lincomb a A = aa \<cdot>\<^sub>v b
[PROOF STEP]
by (intro exI[of _ 0], auto)
[PROOF STATE]
proof (state)
this:
\<exists>a. x = a \<cdot>\<^sub>v b

goal (1 subgoal):
 1. A = {b} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A = {b} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
assume "A = {b}"
[PROOF STATE]
proof (state)
this:
A = {b}

goal (1 subgoal):
 1. A = {b} \<Longrightarrow> \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A = {b}

goal (1 subgoal):
 1. \<exists>a. x = a \<cdot>\<^sub>v b
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
A = {b}

goal (1 subgoal):
 1. \<exists>aa. NC.lincomb a A = aa \<cdot>\<^sub>v b
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
A = {b}
b \<in> carrier_vec n

goal (1 subgoal):
 1. \<exists>aa. NC.lincomb a A = aa \<cdot>\<^sub>v b
[PROOF STEP]
by (intro exI[of _ "a b"], auto simp: NC.lincomb_def)
[PROOF STATE]
proof (state)
this:
\<exists>a. x = a \<cdot>\<^sub>v b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>a. x = a \<cdot>\<^sub>v b

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x3 \<in> NC.span {b} \<Longrightarrow> \<exists>a. ?x3 = a \<cdot>\<^sub>v b

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?x3 \<in> NC.span {b} \<Longrightarrow> \<exists>a. ?x3 = a \<cdot>\<^sub>v b

goal (1 subgoal):
 1. NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
NC.span {b} \<subseteq> {a \<cdot>\<^sub>v b |a. True}

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mat_kernel (char_matrix A lam) \<subseteq> {a \<cdot>\<^sub>v b |a. True}
[PROOF STEP]
obtain vv ww where vb: "v = vv \<cdot>\<^sub>v b" and wb: "w = ww \<cdot>\<^sub>v b"
[PROOF STATE]
proof (prove)
using this:
mat_kernel (char_matrix A lam) \<subseteq> {a \<cdot>\<^sub>v b |a. True}

goal (1 subgoal):
 1. (\<And>vv ww. \<lbrakk>v = vv \<cdot>\<^sub>v b; w = ww \<cdot>\<^sub>v b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vk wk
[PROOF STATE]
proof (prove)
using this:
mat_kernel (char_matrix A lam) \<subseteq> {a \<cdot>\<^sub>v b |a. True}
v \<in> mat_kernel (char_matrix A lam)
w \<in> mat_kernel (char_matrix A lam)

goal (1 subgoal):
 1. (\<And>vv ww. \<lbrakk>v = vv \<cdot>\<^sub>v b; w = ww \<cdot>\<^sub>v b\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force+
[PROOF STATE]
proof (state)
this:
v = vv \<cdot>\<^sub>v b
w = ww \<cdot>\<^sub>v b

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from wb w b
[PROOF STATE]
proof (chain)
picking this:
w = ww \<cdot>\<^sub>v b
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
b \<in> carrier_vec n
[PROOF STEP]
have ww: "ww \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
w = ww \<cdot>\<^sub>v b
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
b \<in> carrier_vec n

goal (1 subgoal):
 1. ww \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ww \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from arg_cong[OF wb, of "\<lambda> x. inverse ww \<cdot>\<^sub>v x"] w ww b
[PROOF STATE]
proof (chain)
picking this:
inverse ww \<cdot>\<^sub>v w = inverse ww \<cdot>\<^sub>v (ww \<cdot>\<^sub>v b)
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
ww \<noteq> (0::'a)
b \<in> carrier_vec n
[PROOF STEP]
have "b = inverse ww \<cdot>\<^sub>v w"
[PROOF STATE]
proof (prove)
using this:
inverse ww \<cdot>\<^sub>v w = inverse ww \<cdot>\<^sub>v (ww \<cdot>\<^sub>v b)
w \<in> carrier_vec n
w \<noteq> 0\<^sub>v n
ww \<noteq> (0::'a)
b \<in> carrier_vec n

goal (1 subgoal):
 1. b = inverse ww \<cdot>\<^sub>v w
[PROOF STEP]
by (auto simp: smult_smult_assoc)
[PROOF STATE]
proof (state)
this:
b = inverse ww \<cdot>\<^sub>v w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from vb[unfolded this smult_smult_assoc]
[PROOF STATE]
proof (chain)
picking this:
v = vv * inverse ww \<cdot>\<^sub>v w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v = vv * inverse ww \<cdot>\<^sub>v w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. v = a \<cdot>\<^sub>v w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique_eigenvector_complex: assumes A: "A \<in> carrier_mat n n"
  and ord: "order lam (char_poly A :: complex poly) = 1"
  and ev: "eigenvector A v lam" "eigenvector A w lam"
shows "\<exists> a. v = a \<cdot>\<^sub>v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from jordan_nf_exists[OF A] char_poly_factorized[OF A]
[PROOF STATE]
proof (chain)
picking this:
char_poly A = (\<Prod>a\<leftarrow>?as. [:- a, 1:]) \<Longrightarrow> \<exists>n_as. jordan_nf A n_as
\<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n
[PROOF STEP]
obtain n_as
    where "jordan_nf A n_as"
[PROOF STATE]
proof (prove)
using this:
char_poly A = (\<Prod>a\<leftarrow>?as. [:- a, 1:]) \<Longrightarrow> \<exists>n_as. jordan_nf A n_as
\<exists>as. char_poly A = (\<Prod>a\<leftarrow>as. [:- a, 1:]) \<and> length as = n

goal (1 subgoal):
 1. (\<And>n_as. jordan_nf A n_as \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
jordan_nf A n_as

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from unique_eigenvector_jnf[OF this ord ev]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>a. v = a \<cdot>\<^sub>v w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<exists>a. v = a \<cdot>\<^sub>v w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique_eigenvector_real: assumes A: "A \<in> carrier_mat n n"
  and ord: "order lam (char_poly A :: real poly) = 1"
  and ev: "eigenvector A v lam" "eigenvector A w lam"
shows "\<exists> a. v = a \<cdot>\<^sub>v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
let ?c = complex_of_real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
let ?A = "map_mat ?c A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have cA: "?A \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. of_real_hom.mat_hom A \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_real_hom.mat_hom A \<in> carrier_mat n n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
have ord: "order (?c lam) (char_poly ?A) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real lam) (char_poly (of_real_hom.mat_hom A)) = 1
[PROOF STEP]
unfolding of_real_hom.char_poly_hom[OF A]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order (complex_of_real lam) (map_poly complex_of_real (char_poly A)) = 1
[PROOF STEP]
by (subst map_poly_inj_idom_divide_hom.order_hom, unfold_locales, rule ord)
[PROOF STATE]
proof (state)
this:
order (complex_of_real lam) (char_poly (of_real_hom.mat_hom A)) = 1

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
note evc = of_real_hom.eigenvector_hom[OF A]
[PROOF STATE]
proof (state)
this:
eigenvector A ?v ?ev \<Longrightarrow> eigenvector (of_real_hom.mat_hom A) (of_real_hom.vec_hom ?v) (of_real ?ev)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from unique_eigenvector_complex[OF cA ord evc evc, OF ev]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. of_real_hom.vec_hom v = a \<cdot>\<^sub>v of_real_hom.vec_hom w
[PROOF STEP]
obtain a :: complex
    where id: "map_vec ?c v = a \<cdot>\<^sub>v map_vec ?c w"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. of_real_hom.vec_hom v = a \<cdot>\<^sub>v of_real_hom.vec_hom w

goal (1 subgoal):
 1. (\<And>a. of_real_hom.vec_hom v = a \<cdot>\<^sub>v of_real_hom.vec_hom w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_real_hom.vec_hom v = a \<cdot>\<^sub>v of_real_hom.vec_hom w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
(* now prove that a is real *)
[PROOF STATE]
proof (state)
this:
of_real_hom.vec_hom v = a \<cdot>\<^sub>v of_real_hom.vec_hom w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from ev[unfolded eigenvector_def] A
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = lam \<cdot>\<^sub>v v
w \<in> carrier_vec (dim_row A) \<and> w \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v w = lam \<cdot>\<^sub>v w
A \<in> carrier_mat n n
[PROOF STEP]
have carr: "v \<in> carrier_vec n" "w \<in> carrier_vec n"
    "v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec (dim_row A) \<and> v \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v v = lam \<cdot>\<^sub>v v
w \<in> carrier_vec (dim_row A) \<and> w \<noteq> 0\<^sub>v (dim_row A) \<and> A *\<^sub>v w = lam \<cdot>\<^sub>v w
A \<in> carrier_mat n n

goal (1 subgoal):
 1. v \<in> carrier_vec n &&& w \<in> carrier_vec n &&& v \<noteq> 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
w \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
w \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
[PROOF STEP]
obtain i where i: "i < n" "v $ i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v $v i \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Matrix.vec_eq_iff
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n
\<not> (dim_vec v = dim_vec (0\<^sub>v n) \<and> (\<forall>i<dim_vec (0\<^sub>v n). v $v i = 0\<^sub>v n $v i))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v $v i \<noteq> 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n
v $v i \<noteq> 0

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from arg_cong[OF id, of "\<lambda> x. x $ i"] carr i
[PROOF STATE]
proof (chain)
picking this:
of_real_hom.vec_hom v $v i = (a \<cdot>\<^sub>v of_real_hom.vec_hom w) $v i
v \<in> carrier_vec n
w \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
i < n
v $v i \<noteq> 0
[PROOF STEP]
have "?c (v $ i) = a * ?c (w $ i)"
[PROOF STATE]
proof (prove)
using this:
of_real_hom.vec_hom v $v i = (a \<cdot>\<^sub>v of_real_hom.vec_hom w) $v i
v \<in> carrier_vec n
w \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
i < n
v $v i \<noteq> 0

goal (1 subgoal):
 1. complex_of_real (v $v i) = a * complex_of_real (w $v i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
complex_of_real (v $v i) = a * complex_of_real (w $v i)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
with i(2)
[PROOF STATE]
proof (chain)
picking this:
v $v i \<noteq> 0
complex_of_real (v $v i) = a * complex_of_real (w $v i)
[PROOF STEP]
have "a \<in> Reals"
[PROOF STATE]
proof (prove)
using this:
v $v i \<noteq> 0
complex_of_real (v $v i) = a * complex_of_real (w $v i)

goal (1 subgoal):
 1. a \<in> \<real>
[PROOF STEP]
by (metis Reals_cnj_iff complex_cnj_complex_of_real complex_cnj_mult mult_cancel_right
        mult_eq_0_iff of_real_hom.hom_zero of_real_hom.injectivity)
[PROOF STATE]
proof (state)
this:
a \<in> \<real>

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> \<real>
[PROOF STEP]
obtain b where a: "a = ?c b"
[PROOF STATE]
proof (prove)
using this:
a \<in> \<real>

goal (1 subgoal):
 1. (\<And>b. a = complex_of_real b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Reals_cases)
[PROOF STATE]
proof (state)
this:
a = complex_of_real b

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
from id[unfolded a]
[PROOF STATE]
proof (chain)
picking this:
of_real_hom.vec_hom v = complex_of_real b \<cdot>\<^sub>v of_real_hom.vec_hom w
[PROOF STEP]
have "map_vec ?c v = map_vec ?c (b \<cdot>\<^sub>v w)"
[PROOF STATE]
proof (prove)
using this:
of_real_hom.vec_hom v = complex_of_real b \<cdot>\<^sub>v of_real_hom.vec_hom w

goal (1 subgoal):
 1. of_real_hom.vec_hom v = of_real_hom.vec_hom (b \<cdot>\<^sub>v w)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_real_hom.vec_hom v = of_real_hom.vec_hom (b \<cdot>\<^sub>v w)

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
hence "v = b \<cdot>\<^sub>v w"
[PROOF STATE]
proof (prove)
using this:
of_real_hom.vec_hom v = of_real_hom.vec_hom (b \<cdot>\<^sub>v w)

goal (1 subgoal):
 1. v = b \<cdot>\<^sub>v w
[PROOF STEP]
by (rule of_real_hom.vec_hom_inj)
[PROOF STATE]
proof (state)
this:
v = b \<cdot>\<^sub>v w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = b \<cdot>\<^sub>v w

goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a. v = a \<cdot>\<^sub>v w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unique_eigen_vector_real: assumes ord: "order lam (charpoly A :: real poly) = 1"
  and ev: "eigen_vector A v lam" "eigen_vector A w lam"
shows "\<exists> a. v = a *s w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. v = a *s w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
order lam (charpoly A) = 1
eigen_vector A v lam
eigen_vector A w lam

goal (1 subgoal):
 1. \<exists>a. v = a *s w
[PROOF STEP]
proof (transfer, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>lam A v w. \<lbrakk>A \<in> carrier_mat CARD('a) CARD('a); order lam (char_poly A) = 1; v \<in> carrier_vec CARD('a); eigenvector A v lam; w \<in> carrier_vec CARD('a); eigenvector A w lam\<rbrakk> \<Longrightarrow> \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
case (1 lam A v w)
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat CARD('a) CARD('a)
order lam (char_poly A) = 1
v \<in> carrier_vec CARD('a)
eigenvector A v lam
w \<in> carrier_vec CARD('a)
eigenvector A w lam

goal (1 subgoal):
 1. \<And>lam A v w. \<lbrakk>A \<in> carrier_mat CARD('a) CARD('a); order lam (char_poly A) = 1; v \<in> carrier_vec CARD('a); eigenvector A v lam; w \<in> carrier_vec CARD('a); eigenvector A w lam\<rbrakk> \<Longrightarrow> \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. v = a \<cdot>\<^sub>v w
[PROOF STEP]
by (rule unique_eigenvector_real[OF 1(1-2,4,6)])
[PROOF STATE]
proof (state)
this:
\<exists>a. v = a \<cdot>\<^sub>v w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma unary_eval: "eval (UNARY R P) a = R (peval P a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (UNARY R P) a = R (peval P a)
[PROOF STEP]
unfolding UNARY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. R (l ! 0)) [P]) a = R (peval P a)
[PROOF STEP]
by simp


[STATEMENT]
lemma binary_eval: "eval (BINARY R P\<^sub>1 P\<^sub>2) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (BINARY R P\<^sub>1 P\<^sub>2) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a)
[PROOF STEP]
unfolding BINARY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. R (l ! 0) (l ! 1)) [P\<^sub>1, P\<^sub>2]) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a)
[PROOF STEP]
by simp


[STATEMENT]
lemma ternary_eval: "eval (TERNARY R P\<^sub>1 P\<^sub>2 P\<^sub>3) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a) (peval P\<^sub>3 a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (TERNARY R P\<^sub>1 P\<^sub>2 P\<^sub>3) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a) (peval P\<^sub>3 a)
[PROOF STEP]
unfolding TERNARY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. R (l ! 0) (l ! 1) (l ! 2)) [P\<^sub>1, P\<^sub>2, P\<^sub>3]) a = R (peval P\<^sub>1 a) (peval P\<^sub>2 a) (peval P\<^sub>3 a)
[PROOF STEP]
by simp


[STATEMENT]
lemma ALLC_LIST_eval_list_all: "eval ([\<forall> in L] DF) a = list_all (\<lambda>l. eval (DF l) a) L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval [\<forall> in L] DF a = list_all (\<lambda>l. eval (DF l) a) L
[PROOF STEP]
by (induction L, auto simp: TRUE_def UNARY_def)


[STATEMENT]
lemma ALLC_LIST_eval:  "eval ([\<forall> in L] DF) a = (\<forall>k<length L. eval (DF (L!k)) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval [\<forall> in L] DF a = (\<forall>k<length L. eval (DF (L ! k)) a)
[PROOF STEP]
by (simp add: ALLC_LIST_eval_list_all list_all_length)


[STATEMENT]
lemma ALLC_eval: "eval ([\<forall><n] DF) a = (\<forall>k<n. eval (DF k) a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval [\<forall><n] DF a = (\<forall>k<n. eval (DF k) a)
[PROOF STEP]
unfolding ALLC_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval [\<forall> in [0..<n]] DF a = (\<forall>k<n. eval (DF k) a)
[PROOF STEP]
by (simp add: ALLC_LIST_eval)


[STATEMENT]
lemma split_concat:
  "splits (map f (concat pls)) (map length pls) = map (map f) pls"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. splits (map f (Diophantine_Relations.concat pls)) (map length pls) = map (map f) pls
[PROOF STEP]
by (induction pls, auto)


[STATEMENT]
lemma LARY_eval:
  fixes PLL :: "polynomial list list"
  shows "eval (LARY R PLL) a = R (map (map (\<lambda>P. peval P a)) PLL)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (LARY R PLL) a = R (map (map (\<lambda>P. peval P a)) PLL)
[PROOF STEP]
unfolding LARY_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. R (splits l (map length PLL))) (Diophantine_Relations.concat PLL)) a = R (map (map (\<lambda>P. peval P a)) PLL)
[PROOF STEP]
apply (induction PLL, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>aa PLL. eval (NARY (\<lambda>l. R (splits l (map length PLL))) (Diophantine_Relations.concat PLL)) a = R (map (map (\<lambda>P. peval P a)) PLL) \<Longrightarrow> eval (NARY (\<lambda>l. R (splits l (map length (aa # PLL)))) (Diophantine_Relations.concat (aa # PLL))) a = R (map (map (\<lambda>P. peval P a)) (aa # PLL))
[PROOF STEP]
subgoal for pl pls
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (NARY (\<lambda>l. R (splits l (map length pls))) (Diophantine_Relations.concat pls)) a = R (map (map (\<lambda>P. peval P a)) pls) \<Longrightarrow> eval (NARY (\<lambda>l. R (splits l (map length (pl # pls)))) (Diophantine_Relations.concat (pl # pls))) a = R (map (map (\<lambda>P. peval P a)) (pl # pls))
[PROOF STEP]
by (induction pl, auto simp: split_concat)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma or_dioph:
  assumes "is_dioph_rel A" and "is_dioph_rel B"
  shows "is_dioph_rel (A [\<or>] B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_dioph_rel A
is_dioph_rel B
[PROOF STEP]
obtain PA1 PA2 where PA: "\<forall>a. (eval A a) \<longleftrightarrow> (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)"
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel A
is_dioph_rel B

goal (1 subgoal):
 1. (\<And>PA1 PA2. \<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
\<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
is_dioph_rel A
is_dioph_rel B
[PROOF STEP]
obtain PB1 PB2 where PB: "\<forall>a. (eval B a) \<longleftrightarrow> (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)"
[PROOF STATE]
proof (prove)
using this:
is_dioph_rel A
is_dioph_rel B

goal (1 subgoal):
 1. (\<And>PB1 PB2. \<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: is_dioph_rel_def)
[PROOF STATE]
proof (state)
this:
\<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
(* OR means (A1 - A2) * (B1 - B2) = 0
     Rewrite as A1*B1 + A2*B2 = A1*B2 + A2*B1 to eliminate subtraction. *)
[PROOF STATE]
proof (state)
this:
\<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_dioph_rel (A [\<or>] B)
[PROOF STEP]
unfolding is_dioph_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>1 P\<^sub>2. \<forall>a. eval (A [\<or>] B) a = (\<exists>v. ppeval P\<^sub>1 a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "PA1 \<^bold>* PB1 \<^bold>+ PA2 \<^bold>* PB2"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P\<^sub>2. \<forall>a. eval (A [\<or>] B) a = (\<exists>v. ppeval (PA1 \<^bold>* PB1 \<^bold>+ PA2 \<^bold>* PB2) a v = ppeval P\<^sub>2 a v)
[PROOF STEP]
apply (rule exI[of _ "PA1 \<^bold>* PB2 \<^bold>+ PA2 \<^bold>* PB1"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>a. eval (A [\<or>] B) a = (\<exists>v. ppeval (PA1 \<^bold>* PB1 \<^bold>+ PA2 \<^bold>* PB2) a v = ppeval (PA1 \<^bold>* PB2 \<^bold>+ PA2 \<^bold>* PB1) a v)
[PROOF STEP]
using PA PB
[PROOF STATE]
proof (prove)
using this:
\<forall>a. eval A a = (\<exists>v. ppeval PA1 a v = ppeval PA2 a v)
\<forall>a. eval B a = (\<exists>v. ppeval PB1 a v = ppeval PB2 a v)

goal (1 subgoal):
 1. \<forall>a. eval (A [\<or>] B) a = (\<exists>v. ppeval (PA1 \<^bold>* PB1 \<^bold>+ PA2 \<^bold>* PB2) a v = ppeval (PA1 \<^bold>* PB2 \<^bold>+ PA2 \<^bold>* PB1) a v)
[PROOF STEP]
by (auto) (metis crossproduct_eq add.commute)+
[PROOF STATE]
proof (state)
this:
is_dioph_rel (A [\<or>] B)

goal:
No subgoals!
[PROOF STEP]
(* For each subgoal, a different fact is unused. The warning is due to 'metis+' being used. *)
[PROOF STATE]
proof (state)
this:
is_dioph_rel (A [\<or>] B)

goal:
No subgoals!
[PROOF STEP]
qed