[STATEMENT]
lemma multp_imp_multp\<^sub>H\<^sub>O:
  assumes "asymp r" and "transp r"
  shows "multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. multp r M N \<Longrightarrow> multp\<^sub>H\<^sub>O r M N
[PROOF STEP]
unfolding multp_def mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M, N) \<in> (mult1 {(x, y). r x y})\<^sup>+ \<Longrightarrow> multp\<^sub>H\<^sub>O r M N
[PROOF STEP]
proof (induction rule: trancl_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. (M, y) \<in> mult1 {(x, y). r x y} \<Longrightarrow> multp\<^sub>H\<^sub>O r M y
 2. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
case (base P)
[PROOF STATE]
proof (state)
this:
(M, P) \<in> mult1 {(x, y). r x y}

goal (2 subgoals):
 1. \<And>y. (M, y) \<in> mult1 {(x, y). r x y} \<Longrightarrow> multp\<^sub>H\<^sub>O r M y
 2. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(M, P) \<in> mult1 {(x, y). r x y}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(M, P) \<in> mult1 {(x, y). r x y}

goal (1 subgoal):
 1. multp\<^sub>H\<^sub>O r M P
[PROOF STEP]
using \<open>asymp r\<close>
[PROOF STATE]
proof (prove)
using this:
(M, P) \<in> mult1 {(x, y). r x y}
asymp r

goal (1 subgoal):
 1. multp\<^sub>H\<^sub>O r M P
[PROOF STEP]
by (auto elim!: mult1_lessE simp: count_eq_zero_iff multp\<^sub>H\<^sub>O_def split: if_splits
        dest!: Suc_lessD)
[PROOF STATE]
proof (state)
this:
multp\<^sub>H\<^sub>O r M P

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
case (step N P)
[PROOF STATE]
proof (state)
this:
(M, N) \<in> (mult1 {(x, y). r x y})\<^sup>+
(N, P) \<in> mult1 {(x, y). r x y}
multp\<^sub>H\<^sub>O r M N

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
from step(3)
[PROOF STATE]
proof (chain)
picking this:
multp\<^sub>H\<^sub>O r M N
[PROOF STEP]
have "M \<noteq> N" and
    **: "\<And>y. count N y < count M y \<Longrightarrow> (\<exists>x. r y x \<and> count M x < count N x)"
[PROOF STATE]
proof (prove)
using this:
multp\<^sub>H\<^sub>O r M N

goal (1 subgoal):
 1. M \<noteq> N &&& (\<And>y. count N y < count M y \<Longrightarrow> \<exists>x. r y x \<and> count M x < count N x)
[PROOF STEP]
by (simp_all add: multp\<^sub>H\<^sub>O_def)
[PROOF STATE]
proof (state)
this:
M \<noteq> N
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
from step(2)
[PROOF STATE]
proof (chain)
picking this:
(N, P) \<in> mult1 {(x, y). r x y}
[PROOF STEP]
obtain M0 a K where
    *: "P = add_mset a M0" "N = M0 + K" "a \<notin># K" "\<And>b. b \<in># K \<Longrightarrow> r b a"
[PROOF STATE]
proof (prove)
using this:
(N, P) \<in> mult1 {(x, y). r x y}

goal (1 subgoal):
 1. (\<And>a M0 K. \<lbrakk>P = add_mset a M0; N = M0 + K; a \<notin># K; \<And>b. b \<in># K \<Longrightarrow> r b a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>asymp r\<close>
[PROOF STATE]
proof (prove)
using this:
(N, P) \<in> mult1 {(x, y). r x y}
asymp r

goal (1 subgoal):
 1. (\<And>a M0 K. \<lbrakk>P = add_mset a M0; N = M0 + K; a \<notin># K; \<And>b. b \<in># K \<Longrightarrow> r b a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: mult1_lessE)
[PROOF STATE]
proof (state)
this:
P = add_mset a M0
N = M0 + K
a \<notin># K
?b \<in># K \<Longrightarrow> r ?b a

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
from \<open>M \<noteq> N\<close> ** *(1,2,3)
[PROOF STATE]
proof (chain)
picking this:
M \<noteq> N
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
P = add_mset a M0
N = M0 + K
a \<notin># K
[PROOF STEP]
have "M \<noteq> P"
[PROOF STATE]
proof (prove)
using this:
M \<noteq> N
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
P = add_mset a M0
N = M0 + K
a \<notin># K

goal (1 subgoal):
 1. M \<noteq> P
[PROOF STEP]
using *(4) \<open>asymp r\<close>
[PROOF STATE]
proof (prove)
using this:
M \<noteq> N
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
P = add_mset a M0
N = M0 + K
a \<notin># K
?b \<in># K \<Longrightarrow> r ?b a
asymp r

goal (1 subgoal):
 1. M \<noteq> P
[PROOF STEP]
by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
        count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
[PROOF STATE]
proof (state)
this:
M \<noteq> P

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
M \<noteq> P

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
M \<noteq> P

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
assume "count P a \<le> count M a"
[PROOF STATE]
proof (state)
this:
count P a \<le> count M a

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
with \<open>a \<notin># K\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<notin># K
count P a \<le> count M a
[PROOF STEP]
have "count N a < count M a"
[PROOF STATE]
proof (prove)
using this:
a \<notin># K
count P a \<le> count M a

goal (1 subgoal):
 1. count N a < count M a
[PROOF STEP]
unfolding *(1,2)
[PROOF STATE]
proof (prove)
using this:
a \<notin># K
count (add_mset a M0) a \<le> count M a

goal (1 subgoal):
 1. count (M0 + K) a < count M a
[PROOF STEP]
by (auto simp add: not_in_iff)
[PROOF STATE]
proof (state)
this:
count N a < count M a

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
count N a < count M a
[PROOF STEP]
obtain z where z: "r a z" "count M z < count N z"
[PROOF STATE]
proof (prove)
using this:
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
count N a < count M a

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>r a z; count M z < count N z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
r a z
count M z < count N z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
P = add_mset a M0
N = M0 + K
a \<notin># K
?b \<in># K \<Longrightarrow> r ?b a
r a z
count M z < count N z
[PROOF STEP]
have "count N z \<le> count P z"
[PROOF STATE]
proof (prove)
using this:
P = add_mset a M0
N = M0 + K
a \<notin># K
?b \<in># K \<Longrightarrow> r ?b a
r a z
count M z < count N z

goal (1 subgoal):
 1. count N z \<le> count P z
[PROOF STEP]
using \<open>asymp r\<close>
[PROOF STATE]
proof (prove)
using this:
P = add_mset a M0
N = M0 + K
a \<notin># K
?b \<in># K \<Longrightarrow> r ?b a
r a z
count M z < count N z
asymp r

goal (1 subgoal):
 1. count N z \<le> count P z
[PROOF STEP]
by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
            diff_single_trivial in_diff_count not_le_imp_less)
[PROOF STATE]
proof (state)
this:
count N z \<le> count P z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
r a z
count M z < count N z
count N z \<le> count P z
[PROOF STEP]
have "\<exists>z. r a z \<and> count M z < count P z"
[PROOF STATE]
proof (prove)
using this:
r a z
count M z < count N z
count N z \<le> count P z

goal (1 subgoal):
 1. \<exists>z. r a z \<and> count M z < count P z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>z. r a z \<and> count M z < count P z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
count P a \<le> count M a \<Longrightarrow> \<exists>z. r a z \<and> count M z < count P z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
note count_a = this
[PROOF STATE]
proof (state)
this:
count P a \<le> count M a \<Longrightarrow> \<exists>z. r a z \<and> count M z < count P z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
count P a \<le> count M a \<Longrightarrow> \<exists>z. r a z \<and> count M z < count P z

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
assume count_y: "count P y < count M y"
[PROOF STATE]
proof (state)
this:
count P y < count M y

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
have "\<exists>x. r y x \<and> count M x < count P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
proof (cases "y = a")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. y \<noteq> a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y = a

goal (2 subgoals):
 1. y = a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. y \<noteq> a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with count_y count_a
[PROOF STATE]
proof (chain)
picking this:
count P y < count M y
count P a \<le> count M a \<Longrightarrow> \<exists>z. r a z \<and> count M z < count P z
y = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count P y < count M y
count P a \<le> count M a \<Longrightarrow> \<exists>z. r a z \<and> count M z < count P z
y = a

goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<noteq> a

goal (1 subgoal):
 1. y \<noteq> a \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
proof (cases "y \<in># K")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y \<in># K

goal (2 subgoals):
 1. y \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with *(4)
[PROOF STATE]
proof (chain)
picking this:
?b \<in># K \<Longrightarrow> r ?b a
y \<in># K
[PROOF STEP]
have "r y a"
[PROOF STATE]
proof (prove)
using this:
?b \<in># K \<Longrightarrow> r ?b a
y \<in># K

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

goal (2 subgoals):
 1. y \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r y a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r y a

goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
by (cases "count P a \<le> count M a") (auto dest: count_a intro: \<open>transp r\<close>[THEN transpD])
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal (1 subgoal):
 1. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
y \<notin># K

goal (1 subgoal):
 1. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with \<open>y \<noteq> a\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> a
y \<notin># K
[PROOF STEP]
have "count P y = count N y"
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
y \<notin># K

goal (1 subgoal):
 1. count P y = count N y
[PROOF STEP]
unfolding *(1,2)
[PROOF STATE]
proof (prove)
using this:
y \<noteq> a
y \<notin># K

goal (1 subgoal):
 1. count (add_mset a M0) y = count (M0 + K) y
[PROOF STEP]
by (simp add: not_in_iff)
[PROOF STATE]
proof (state)
this:
count P y = count N y

goal (1 subgoal):
 1. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with count_y **
[PROOF STATE]
proof (chain)
picking this:
count P y < count M y
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
count P y = count N y
[PROOF STEP]
obtain z where z: "r y z" "count M z < count N z"
[PROOF STATE]
proof (prove)
using this:
count P y < count M y
count N ?y < count M ?y \<Longrightarrow> \<exists>x. r ?y x \<and> count M x < count N x
count P y = count N y

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>r y z; count M z < count N z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r y z
count M z < count N z

goal (1 subgoal):
 1. y \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
proof (cases "z \<in># K")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. z \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
z \<in># K

goal (2 subgoals):
 1. z \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with *(4)
[PROOF STATE]
proof (chain)
picking this:
?b \<in># K \<Longrightarrow> r ?b a
z \<in># K
[PROOF STEP]
have "r z a"
[PROOF STATE]
proof (prove)
using this:
?b \<in># K \<Longrightarrow> r ?b a
z \<in># K

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

goal (2 subgoals):
 1. z \<in># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
 2. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with z(1)
[PROOF STATE]
proof (chain)
picking this:
r y z
r z a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r y z
r z a

goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
by (cases "count P a \<le> count M a") (auto dest!: count_a intro: \<open>transp r\<close>[THEN transpD])
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal (1 subgoal):
 1. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
z \<notin># K

goal (1 subgoal):
 1. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with \<open>a \<notin># K\<close>
[PROOF STATE]
proof (chain)
picking this:
a \<notin># K
z \<notin># K
[PROOF STEP]
have "count N z \<le> count P z"
[PROOF STATE]
proof (prove)
using this:
a \<notin># K
z \<notin># K

goal (1 subgoal):
 1. count N z \<le> count P z
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
using this:
a \<notin># K
z \<notin># K

goal (1 subgoal):
 1. count (M0 + K) z \<le> count (add_mset a M0) z
[PROOF STEP]
by (auto simp add: not_in_iff)
[PROOF STATE]
proof (state)
this:
count N z \<le> count P z

goal (1 subgoal):
 1. z \<notin># K \<Longrightarrow> \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
r y z
count M z < count N z
count N z \<le> count P z
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r y z
count M z < count N z
count N z \<le> count P z

goal (1 subgoal):
 1. \<exists>x. r y x \<and> count M x < count P x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>x. r y x \<and> count M x < count P x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
count P ?y2 < count M ?y2 \<Longrightarrow> \<exists>x. r ?y2 x \<and> count M x < count P x

goal (1 subgoal):
 1. \<And>y z. \<lbrakk>(M, y) \<in> (mult1 {(x, y). r x y})\<^sup>+; (y, z) \<in> mult1 {(x, y). r x y}; multp\<^sub>H\<^sub>O r M y\<rbrakk> \<Longrightarrow> multp\<^sub>H\<^sub>O r M z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
M \<noteq> P
count P ?y2 < count M ?y2 \<Longrightarrow> \<exists>x. r ?y2 x \<and> count M x < count P x
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
M \<noteq> P
count P ?y2 < count M ?y2 \<Longrightarrow> \<exists>x. r ?y2 x \<and> count M x < count P x

goal (1 subgoal):
 1. multp\<^sub>H\<^sub>O r M P
[PROOF STEP]
unfolding multp\<^sub>H\<^sub>O_def
[PROOF STATE]
proof (prove)
using this:
M \<noteq> P
count P ?y2 < count M ?y2 \<Longrightarrow> \<exists>x. r ?y2 x \<and> count M x < count P x

goal (1 subgoal):
 1. M \<noteq> P \<and> (\<forall>y. count P y < count M y \<longrightarrow> (\<exists>x. r y x \<and> count M x < count P x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
multp\<^sub>H\<^sub>O r M P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma union_le_diff_plus: "P \<subseteq># M \<Longrightarrow> N < P \<Longrightarrow> M - P + N < M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<subseteq># M; N < P\<rbrakk> \<Longrightarrow> M - P + N < M
[PROOF STEP]
by (drule subset_mset.diff_add[symmetric]) (metis union_le_mono2)


[STATEMENT]
lemma suffix_snoc [simp]: "suffix xs (ys @ [y]) \<longleftrightarrow> xs = [] \<or> (\<exists>zs. xs = zs @ [y] \<and> suffix zs ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. suffix xs (ys @ [y]) = (xs = [] \<or> (\<exists>zs. xs = zs @ [y] \<and> suffix zs ys))
[PROOF STEP]
by (cases xs rule: rev_cases) (auto simp: suffix_def)


[STATEMENT]
lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (exp (\<i> * complex_of_real y)) = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma Taylor_sin:
  "norm(sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k))
   \<le> exp\<bar>Im z\<bar> * (norm z) ^ (Suc n) / (fact n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
have mono: "\<And>u w z::real. w \<le> u \<Longrightarrow> z \<le> u \<Longrightarrow> w + z \<le> u*2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>u w z. \<lbrakk>w \<le> u; z \<le> u\<rbrakk> \<Longrightarrow> w + z \<le> u * 2
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<lbrakk>?w \<le> ?u; ?z \<le> ?u\<rbrakk> \<Longrightarrow> ?w + ?z \<le> ?u * 2

goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
have *: "cmod (sin z -
                 (\<Sum>i\<le>n. (-1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / (fact i)))
           \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / (fact n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (sin z - (\<Sum>i\<le>n. (- 1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / fact i)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
proof (rule complex_Taylor [of "closed_segment 0 z" n
                                 "\<lambda>k x. (-1)^(k div 2) * (if even k then sin x else cos x)"
                                 "exp\<bar>Im z\<bar>" 0 z,  simplified])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i x. \<lbrakk>x \<in> closed_segment 0 z; i \<le> n\<rbrakk> \<Longrightarrow> ((\<lambda>x. (- 1) ^ (i div 2) * (if even i then sin x else cos x)) has_field_derivative (- 1) ^ (Suc i div 2) * (if odd i then sin x else cos x)) (at x within closed_segment 0 z)
 2. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
fix k x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i x. \<lbrakk>x \<in> closed_segment 0 z; i \<le> n\<rbrakk> \<Longrightarrow> ((\<lambda>x. (- 1) ^ (i div 2) * (if even i then sin x else cos x)) has_field_derivative (- 1) ^ (Suc i div 2) * (if odd i then sin x else cos x)) (at x within closed_segment 0 z)
 2. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
show "((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative
            (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x))
            (at x within closed_segment 0 z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x)) (at x within closed_segment 0 z)
[PROOF STEP]
apply (auto simp: power_Suc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. odd k \<Longrightarrow> ((\<lambda>x. (- 1) ^ (k div 2) * cos x) has_field_derivative - ((- 1) ^ (k div 2) * sin x)) (at x within closed_segment 0 z)
 2. even k \<Longrightarrow> ((\<lambda>x. (- 1) ^ (k div 2) * sin x) has_field_derivative (- 1) ^ (k div 2) * cos x) (at x within closed_segment 0 z)
[PROOF STEP]
apply (intro derivative_eq_intros | simp)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
((\<lambda>x. (- 1) ^ (k div 2) * (if even k then sin x else cos x)) has_field_derivative (- 1) ^ (Suc k div 2) * (if odd k then sin x else cos x)) (at x within closed_segment 0 z)

goal (1 subgoal):
 1. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
assume "x \<in> closed_segment 0 z"
[PROOF STATE]
proof (state)
this:
x \<in> closed_segment 0 z

goal (1 subgoal):
 1. \<And>x. x \<in> closed_segment 0 z \<Longrightarrow> cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> closed_segment 0 z
[PROOF STEP]
show "cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>"
[PROOF STATE]
proof (prove)
using this:
x \<in> closed_segment 0 z

goal (1 subgoal):
 1. cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>
[PROOF STEP]
by (auto simp: closed_segment_def norm_mult norm_power cmod_sin_le_exp cmod_cos_le_exp)
[PROOF STATE]
proof (state)
this:
cmod ((- 1) ^ (Suc n div 2) * (if odd n then sin x else cos x)) \<le> exp \<bar>Im z\<bar>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cmod (sin z - (\<Sum>i\<le>n. (- 1) ^ (i div 2) * (if even i then sin 0 else cos 0) * z ^ i / fact i)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n

goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
have **: "\<And>k. complex_of_real (sin_coeff k) * z ^ k
            = (-1)^(k div 2) * (if even k then sin 0 else cos 0) * z^k / of_nat (fact k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. complex_of_real (sin_coeff k) * z ^ k = (- 1) ^ (k div 2) * (if even k then sin 0 else cos 0) * z ^ k / of_nat (fact k)
[PROOF STEP]
by (auto simp: sin_coeff_def elim!: oddE)
[PROOF STATE]
proof (state)
this:
complex_of_real (sin_coeff ?k) * z ^ ?k = (- 1) ^ (?k div 2) * (if even ?k then sin 0 else cos 0) * z ^ ?k / of_nat (fact ?k)

goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n
[PROOF STEP]
by (simp add: ** order_trans [OF _ *])
[PROOF STATE]
proof (state)
this:
cmod (sin z - (\<Sum>k\<le>n. complex_of_real (sin_coeff k) * z ^ k)) \<le> exp \<bar>Im z\<bar> * cmod z ^ Suc n / fact n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tendsto_powr_complex:
  fixes f g :: "_ \<Rightarrow> complex"
  assumes a: "a \<notin> \<real>\<^sub>\<le>\<^sub>0"
  assumes f: "(f \<longlongrightarrow> a) F" and g: "(g \<longlongrightarrow> b) F"
  shows   "((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
a \<notin> \<real>\<^sub>\<le>\<^sub>0
[PROOF STEP]
have [simp]: "a \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a \<notin> \<real>\<^sub>\<le>\<^sub>0

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

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
from f g a
[PROOF STATE]
proof (chain)
picking this:
(f \<longlongrightarrow> a) F
(g \<longlongrightarrow> b) F
a \<notin> \<real>\<^sub>\<le>\<^sub>0
[PROOF STEP]
have "((\<lambda>z. exp (g z * ln (f z))) \<longlongrightarrow> a powr b) F" (is ?P)
[PROOF STATE]
proof (prove)
using this:
(f \<longlongrightarrow> a) F
(g \<longlongrightarrow> b) F
a \<notin> \<real>\<^sub>\<le>\<^sub>0

goal (1 subgoal):
 1. ((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F
[PROOF STEP]
by (auto intro!: tendsto_intros simp: powr_def)
[PROOF STATE]
proof (state)
this:
((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
have "eventually (\<lambda>z. z \<noteq> 0) (nhds a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F z in nhds a. z \<noteq> 0
[PROOF STEP]
by (intro t1_space_nhds) simp_all
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in nhds a. z \<noteq> 0

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
with f
[PROOF STATE]
proof (chain)
picking this:
(f \<longlongrightarrow> a) F
\<forall>\<^sub>F z in nhds a. z \<noteq> 0
[PROOF STEP]
have "eventually (\<lambda>z. f z \<noteq> 0) F"
[PROOF STATE]
proof (prove)
using this:
(f \<longlongrightarrow> a) F
\<forall>\<^sub>F z in nhds a. z \<noteq> 0

goal (1 subgoal):
 1. \<forall>\<^sub>F z in F. f z \<noteq> 0
[PROOF STEP]
using filterlim_iff
[PROOF STATE]
proof (prove)
using this:
(f \<longlongrightarrow> a) F
\<forall>\<^sub>F z in nhds a. z \<noteq> 0
filterlim ?f ?F2.0 ?F1.0 = (\<forall>P. eventually P ?F2.0 \<longrightarrow> (\<forall>\<^sub>F x in ?F1.0. P (?f x)))

goal (1 subgoal):
 1. \<forall>\<^sub>F z in F. f z \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in F. f z \<noteq> 0

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F z in F. f z \<noteq> 0

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
hence "?P \<longleftrightarrow> ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F z in F. f z \<noteq> 0

goal (1 subgoal):
 1. ((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F = ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
by (intro tendsto_cong refl) (simp_all add: powr_def mult_ac)
[PROOF STATE]
proof (state)
this:
((\<lambda>z. exp (g z * Ln (f z))) \<longlongrightarrow> a powr b) F = ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F

goal (1 subgoal):
 1. ((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
((\<lambda>z. f z powr g z) \<longlongrightarrow> a powr b) F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ceiling_mono: "x \<ge> y \<Longrightarrow> \<lceil>x\<rceil> \<ge> \<lceil>y\<rceil>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> \<lceil>y\<rceil> \<le> \<lceil>x\<rceil>
[PROOF STEP]
unfolding ceiling_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> - \<lfloor>- y\<rfloor> \<le> - \<lfloor>- x\<rfloor>
[PROOF STEP]
by (simp add: floor_mono)


[STATEMENT]
lemma RDirProd_hom2:
  assumes "f \<in> ring_hom S T"
  shows "(\<lambda>(x, y). (x, f y)) \<in> ring_hom (RDirProd R S) (RDirProd R T)"
    and "(\<lambda>(x, y). (f x, y)) \<in> ring_hom (RDirProd S R) (RDirProd T R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(x, y). (x, f y)) \<in> ring_hom (RDirProd R S) (RDirProd R T) &&& (\<lambda>(x, y). (f x, y)) \<in> ring_hom (RDirProd S R) (RDirProd T R)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> ring_hom S T

goal (1 subgoal):
 1. (\<lambda>(x, y). (x, f y)) \<in> ring_hom (RDirProd R S) (RDirProd R T) &&& (\<lambda>(x, y). (f x, y)) \<in> ring_hom (RDirProd S R) (RDirProd T R)
[PROOF STEP]
by (auto simp add: ring_hom_def RDirProd_def DirProd_def monoid.defs)


[STATEMENT]
lemma square_fact_le_2_fact: "fact n * fact n \<le> (fact (2 * n) :: real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact n * fact n \<le> fact (2 * n)
[PROOF STEP]
proof (induct n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fact 0 * fact 0 \<le> fact (2 * 0)
 2. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. fact 0 * fact 0 \<le> fact (2 * 0)
 2. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact 0 * fact 0 \<le> fact (2 * 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fact 0 * fact 0 \<le> fact (2 * 0)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
fact n * fact n \<le> fact (2 * n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
have "(fact (Suc n)) * (fact (Suc n)) = of_nat (Suc n) * of_nat (Suc n) * (fact n * fact n :: real)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fact (Suc n) * fact (Suc n) = real (Suc n) * real (Suc n) * (fact n * fact n)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
fact (Suc n) * fact (Suc n) = real (Suc n) * real (Suc n) * (fact n * fact n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fact (Suc n) * fact (Suc n) = real (Suc n) * real (Suc n) * (fact n * fact n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
have "\<dots> \<le> of_nat (Suc n) * of_nat (Suc n) * fact (2 * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Suc n) * real (Suc n) * (fact n * fact n) \<le> real (Suc n) * real (Suc n) * fact (2 * n)
[PROOF STEP]
by (rule mult_left_mono [OF Suc]) simp
[PROOF STATE]
proof (state)
this:
real (Suc n) * real (Suc n) * (fact n * fact n) \<le> real (Suc n) * real (Suc n) * fact (2 * n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) * real (Suc n) * (fact n * fact n) \<le> real (Suc n) * real (Suc n) * fact (2 * n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
have "\<dots> \<le> of_nat (Suc (Suc (2 * n))) * of_nat (Suc (2 * n)) * fact (2 * n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Suc n) * real (Suc n) * fact (2 * n) \<le> real (Suc (Suc (2 * n))) * real (Suc (2 * n)) * fact (2 * n)
[PROOF STEP]
by (rule mult_right_mono)+ (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
real (Suc n) * real (Suc n) * fact (2 * n) \<le> real (Suc (Suc (2 * n))) * real (Suc (2 * n)) * fact (2 * n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (Suc n) * real (Suc n) * fact (2 * n) \<le> real (Suc (Suc (2 * n))) * real (Suc (2 * n)) * fact (2 * n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
have "\<dots> = fact (2 * Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Suc (Suc (2 * n))) * real (Suc (2 * n)) * fact (2 * n) = fact (2 * Suc n)
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
real (Suc (Suc (2 * n))) * real (Suc (2 * n)) * fact (2 * n) = fact (2 * Suc n)

goal (1 subgoal):
 1. \<And>n. fact n * fact n \<le> fact (2 * n) \<Longrightarrow> fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)

goal (1 subgoal):
 1. fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fact (Suc n) * fact (Suc n) \<le> fact (2 * Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
  for x :: real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x powr a \<le> y powr a
[PROOF STEP]
using less_eq_real_def powr_less_mono2 that
[PROOF STATE]
proof (prove)
using this:
(?x \<le> ?y) = (?x < ?y \<or> ?x = ?y)
\<lbrakk>0 < ?a; 0 \<le> ?x; ?x < ?y\<rbrakk> \<Longrightarrow> ?x powr ?a < ?y powr ?a
0 \<le> a
0 \<le> x
x \<le> y

goal (1 subgoal):
 1. x powr a \<le> y powr a
[PROOF STEP]
by auto


[STATEMENT]
lemma cot_periodic [simp]: "cot (x + 2 * pi) = cot x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cot (x + 2 * pi) = cot x
[PROOF STEP]
by (simp add: cot_def)


[STATEMENT]
lemma sincos_total_2pi:
  assumes "x\<^sup>2 + y\<^sup>2 = 1"
  obtains t where "0 \<le> t" "t < 2*pi" "x = cos t" "y = sin t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; t < 2 * pi; x = cos t; y = sin t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; t < 2 * pi; x = cos t; y = sin t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from sincos_total_2pi_le [OF assms]
[PROOF STATE]
proof (chain)
picking this:
\<exists>t\<ge>0. t \<le> 2 * pi \<and> x = cos t \<and> y = sin t
[PROOF STEP]
obtain t where t: "0 \<le> t" "t \<le> 2*pi" "x = cos t" "y = sin t"
[PROOF STATE]
proof (prove)
using this:
\<exists>t\<ge>0. t \<le> 2 * pi \<and> x = cos t \<and> y = sin t

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; t \<le> 2 * pi; x = cos t; y = sin t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 \<le> t
t \<le> 2 * pi
x = cos t
y = sin t

goal (1 subgoal):
 1. (\<And>t. \<lbrakk>0 \<le> t; t < 2 * pi; x = cos t; y = sin t\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (cases "t = 2 * pi") (use t that in \<open>force+\<close>)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_prod_ordIso: "\<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> map_prod f f ` r =o r
[PROOF STEP]
unfolding dir_image_alt[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Well_order r; inj_on f (Field r)\<rbrakk> \<Longrightarrow> dir_image r f =o r
[PROOF STEP]
by (rule ordIso_symmetric[OF dir_image_ordIso])


[STATEMENT]
lemma oexp_Preorder: "Preorder oexp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Preorder oexp
[PROOF STEP]
unfolding preorder_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Refl oexp \<and> trans oexp
[PROOF STEP]
using oexp_Refl oexp_trans
[PROOF STATE]
proof (prove)
using this:
Refl oexp
trans oexp

goal (1 subgoal):
 1. Refl oexp \<and> trans oexp
[PROOF STEP]
by blast


[STATEMENT]
lemma summableI_nonneg_bounded:
  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology,conditionally_complete_linorder}"
  assumes pos[simp]: "\<And>n. 0 \<le> f n"
    and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
  shows "summable f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable f
[PROOF STEP]
unfolding summable_def sums_def [abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s. (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> s
[PROOF STEP]
proof (rule exI LIMSEQ_incseq_SUP)+
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bdd_above (range (\<lambda>n. sum f {..<n}))
 2. incseq (\<lambda>n. sum f {..<n})
[PROOF STEP]
show "bdd_above (range (\<lambda>n. sum f {..<n}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (range (\<lambda>n. sum f {..<n}))
[PROOF STEP]
using le
[PROOF STATE]
proof (prove)
using this:
sum f {..<?n} \<le> x

goal (1 subgoal):
 1. bdd_above (range (\<lambda>n. sum f {..<n}))
[PROOF STEP]
by (auto simp: bdd_above_def)
[PROOF STATE]
proof (state)
this:
bdd_above (range (\<lambda>n. sum f {..<n}))

goal (1 subgoal):
 1. incseq (\<lambda>n. sum f {..<n})
[PROOF STEP]
show "incseq (\<lambda>n. sum f {..<n})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. incseq (\<lambda>n. sum f {..<n})
[PROOF STEP]
by (auto simp: mono_def intro!: sum_mono2)
[PROOF STATE]
proof (state)
this:
incseq (\<lambda>n. sum f {..<n})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complete_algebra_summable_geometric:
  fixes x :: "'a::{real_normed_algebra_1,banach}"
  assumes "norm x < 1"
  shows "summable (\<lambda>n. x ^ n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. summable ((^) x)
[PROOF STEP]
proof (rule summable_comparison_test)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> ?g n
 2. summable ?g
[PROOF STEP]
show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n
[PROOF STEP]
by (simp add: norm_power_ineq)
[PROOF STATE]
proof (state)
this:
\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n

goal (1 subgoal):
 1. summable ((^) (norm x))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
norm x < 1
[PROOF STEP]
show "summable (\<lambda>n. norm x ^ n)"
[PROOF STATE]
proof (prove)
using this:
norm x < 1

goal (1 subgoal):
 1. summable ((^) (norm x))
[PROOF STEP]
by (simp add: summable_geometric)
[PROOF STATE]
proof (state)
this:
summable ((^) (norm x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem meet_connection: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubseteq> y) = (x \<sqinter> y = x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x
 2. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
assume "x \<sqsubseteq> y"
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq> y

goal (2 subgoals):
 1. x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x
 2. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<sqsubseteq> y
[PROOF STEP]
have "is_inf x y x"
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y

goal (1 subgoal):
 1. is_inf x y x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
is_inf x y x

goal (2 subgoals):
 1. x \<sqsubseteq> y \<Longrightarrow> x \<sqinter> y = x
 2. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_inf x y x
[PROOF STEP]
show "x \<sqinter> y = x"
[PROOF STATE]
proof (prove)
using this:
is_inf x y x

goal (1 subgoal):
 1. x \<sqinter> y = x
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<sqinter> y = x

goal (1 subgoal):
 1. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
have "x \<sqinter> y \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> y \<sqsubseteq> y
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
x \<sqinter> y \<sqsubseteq> y

goal (1 subgoal):
 1. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<sqinter> y \<sqsubseteq> y

goal (1 subgoal):
 1. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
assume "x \<sqinter> y = x"
[PROOF STATE]
proof (state)
this:
x \<sqinter> y = x

goal (1 subgoal):
 1. x \<sqinter> y = x \<Longrightarrow> x \<sqsubseteq> y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x \<sqsubseteq> y
[PROOF STEP]
show "x \<sqsubseteq> y"
[PROOF STATE]
proof (prove)
using this:
x \<sqsubseteq> y

goal (1 subgoal):
 1. x \<sqsubseteq> y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trivial_relative_homology_group_gen:
  assumes "continuous_map X (subtopology X S) f"
    "homotopic_with (\<lambda>h. True) (subtopology X S) (subtopology X S) f id"
    "homotopic_with (\<lambda>k. True) X X f id"
  shows "trivial_group(relative_homology_group p X S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trivial_group (relative_homology_group p X S)
[PROOF STEP]
proof (rule exact_seq_imp_triviality)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. exact_seq ([?E, ?D, relative_homology_group p X S, ?B, ?A], [?k, ?h, ?g, ?f])
 2. ?f \<in> Group.iso ?A ?B
 3. ?k \<in> Group.iso ?D ?E
[PROOF STEP]
show "exact_seq ([homology_group (p-1) X,
                    homology_group (p-1) (subtopology X S),
                    relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)],
                   [hom_induced (p-1) (subtopology X S) {} X {} id,
                    hom_boundary p X S,
                    hom_induced p X {} X S id,
                    hom_induced p (subtopology X S) {} X {} id])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exact_seq ([homology_group (p - 1) X, homology_group (p - 1) (subtopology X S), relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)], [hom_induced (p - 1) (subtopology X S) {} X {} id, hom_boundary p X S, hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])
[PROOF STEP]
using homology_exactness_axiom_1 homology_exactness_axiom_2 homology_exactness_axiom_3
[PROOF STATE]
proof (prove)
using this:
exact_seq ([homology_group (?p - 1) (subtopology ?X ?S), relative_homology_group ?p ?X ?S, homology_group ?p ?X], [hom_boundary ?p ?X ?S, hom_induced ?p ?X {} ?X ?S id])
exact_seq ([homology_group (?p - 1) ?X, homology_group (?p - 1) (subtopology ?X ?S), relative_homology_group ?p ?X ?S], [hom_induced (?p - 1) (subtopology ?X ?S) {} ?X {} id, hom_boundary ?p ?X ?S])
exact_seq ([relative_homology_group ?p ?X ?S, homology_group ?p ?X, homology_group ?p (subtopology ?X ?S)], [hom_induced ?p ?X {} ?X ?S id, hom_induced ?p (subtopology ?X ?S) {} ?X {} id])

goal (1 subgoal):
 1. exact_seq ([homology_group (p - 1) X, homology_group (p - 1) (subtopology X S), relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)], [hom_induced (p - 1) (subtopology X S) {} X {} id, hom_boundary p X S, hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])
[PROOF STEP]
by (metis exact_seq_cons_iff)
[PROOF STATE]
proof (state)
this:
exact_seq ([homology_group (p - 1) X, homology_group (p - 1) (subtopology X S), relative_homology_group p X S, homology_group p X, homology_group p (subtopology X S)], [hom_induced (p - 1) (subtopology X S) {} X {} id, hom_boundary p X S, hom_induced p X {} X S id, hom_induced p (subtopology X S) {} X {} id])

goal (2 subgoals):
 1. hom_induced p (subtopology X S) {} X {} id \<in> Group.iso (homology_group p (subtopology X S)) (homology_group p X)
 2. hom_induced (p - 1) (subtopology X S) {} X {} id \<in> Group.iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. hom_induced p (subtopology X S) {} X {} id \<in> Group.iso (homology_group p (subtopology X S)) (homology_group p X)
 2. hom_induced (p - 1) (subtopology X S) {} X {} id \<in> Group.iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)
[PROOF STEP]
show "hom_induced p (subtopology X S) {} X {} id
        \<in> iso (homology_group p (subtopology X S)) (homology_group p X)"
       "hom_induced (p - 1) (subtopology X S) {} X {} id
        \<in> iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hom_induced p (subtopology X S) {} X {} id \<in> Group.iso (homology_group p (subtopology X S)) (homology_group p X) &&& hom_induced (p - 1) (subtopology X S) {} X {} id \<in> Group.iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
continuous_map X (subtopology X S) f
homotopic_with (\<lambda>h. True) (subtopology X S) (subtopology X S) f id
homotopic_with (\<lambda>k. True) X X f id

goal (1 subgoal):
 1. hom_induced p (subtopology X S) {} X {} id \<in> Group.iso (homology_group p (subtopology X S)) (homology_group p X) &&& hom_induced (p - 1) (subtopology X S) {} X {} id \<in> Group.iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)
[PROOF STEP]
by (auto intro: homotopy_equivalence_relative_homology_group_isomorphism)
[PROOF STATE]
proof (state)
this:
hom_induced p (subtopology X S) {} X {} id \<in> Group.iso (homology_group p (subtopology X S)) (homology_group p X)
hom_induced (p - 1) (subtopology X S) {} X {} id \<in> Group.iso (homology_group (p - 1) (subtopology X S)) (homology_group (p - 1) X)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma split0_blt:
  assumes nb: "tmboundslt n t"
  shows "tmboundslt n (snd (split0 t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tmboundslt n (snd (split0 t))
[PROOF STEP]
using nb
[PROOF STATE]
proof (prove)
using this:
tmboundslt n t

goal (1 subgoal):
 1. tmboundslt n (snd (split0 t))
[PROOF STEP]
by (induct t rule: split0.induct) (auto simp add: Let_def split_def)


[STATEMENT]
lemma atLeastAtMost_eq_cball:
  fixes a b::real
  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {a..b} = cball ((a + b) / 2) ((b - a) / 2)
[PROOF STEP]
by (auto simp: dist_real_def field_simps)


[STATEMENT]
lemma gbinomial_code [code]:
  "a gchoose k =
    (if k = 0 then 1
     else fold_atLeastAtMost_nat (\<lambda>k acc. (a - of_nat k) * acc) 0 (k - 1) 1 / fact k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a gchoose k = (if k = 0 then 1::'a else fold_atLeastAtMost_nat (\<lambda>k. (*) (a - of_nat k)) 0 (k - 1) (1::'a) / fact k)
[PROOF STEP]
by (cases k)
    (simp_all add: gbinomial_prod_rev prod_atLeastAtMost_code [symmetric]
      atLeastLessThanSuc_atLeastAtMost)


[STATEMENT]
lemma validE_append:
  assumes a: "\<turnstile> (\<Delta>@\<Gamma>) ok"
  shows "\<turnstile> \<Gamma> ok"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<turnstile> \<Gamma> ok
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
\<turnstile> (\<Delta> @ \<Gamma>) ok

goal (1 subgoal):
 1. \<turnstile> \<Gamma> ok
[PROOF STEP]
proof (induct \<Delta>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<turnstile> ([] @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
 2. \<And>a \<Delta>. \<lbrakk>\<turnstile> (\<Delta> @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok; \<turnstile> ((a # \<Delta>) @ \<Gamma>) ok\<rbrakk> \<Longrightarrow> \<turnstile> \<Gamma> ok
[PROOF STEP]
case (Cons a \<Gamma>')
[PROOF STATE]
proof (state)
this:
\<turnstile> (\<Gamma>' @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
\<turnstile> ((a # \<Gamma>') @ \<Gamma>) ok

goal (2 subgoals):
 1. \<turnstile> ([] @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
 2. \<And>a \<Delta>. \<lbrakk>\<turnstile> (\<Delta> @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok; \<turnstile> ((a # \<Delta>) @ \<Gamma>) ok\<rbrakk> \<Longrightarrow> \<turnstile> \<Gamma> ok
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<turnstile> (\<Gamma>' @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
\<turnstile> ((a # \<Gamma>') @ \<Gamma>) ok
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<turnstile> (\<Gamma>' @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
\<turnstile> ((a # \<Gamma>') @ \<Gamma>) ok

goal (1 subgoal):
 1. \<turnstile> \<Gamma> ok
[PROOF STEP]
by (nominal_induct a rule:binding.strong_induct)
       (auto elim: validE)
[PROOF STATE]
proof (state)
this:
\<turnstile> \<Gamma> ok

goal (1 subgoal):
 1. \<turnstile> ([] @ \<Gamma>) ok \<Longrightarrow> \<turnstile> \<Gamma> ok
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma [code_post]:
  "real_of_rat 0 = 0"
  "real_of_rat 1 = 1"
  "real_of_rat (- 1) = - 1"
  "real_of_rat (1 / numeral k) = 1 / numeral k"
  "real_of_rat (numeral k / numeral l) = numeral k / numeral l"
  "real_of_rat (- (1 / numeral k)) = - (1 / numeral k)"
  "real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (real_of_rat 0 = 0 &&& real_of_rat 1 = 1 &&& real_of_rat (- 1) = - 1) &&& (real_of_rat (1 / numeral k) = 1 / numeral k &&& real_of_rat (numeral k / numeral l) = numeral k / numeral l) &&& real_of_rat (- (1 / numeral k)) = - (1 / numeral k) &&& real_of_rat (- (numeral k / numeral l)) = - (numeral k / numeral l)
[PROOF STEP]
by (simp_all add: of_rat_divide of_rat_minus)


[STATEMENT]
lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Ratreal x - Ratreal y = Ratreal (x - y)
[PROOF STEP]
by (simp add: of_rat_diff)


[STATEMENT]
lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0
[PROOF STEP]
by (cases h) (auto simp: split_minNoneN0  split: option.splits)


[STATEMENT]
lemma del_list_sorted3:
  "sorted1 (xs @ (a,a') # ys @ (b,b') # zs) \<Longrightarrow> x < b \<Longrightarrow>
  del_list x (xs @ (a,a') # ys @ (b,b') # zs) = del_list x (xs @ (a,a') # ys) @ (b,b') # zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted1 (xs @ (a, a') # ys @ (b, b') # zs); x < b\<rbrakk> \<Longrightarrow> del_list x (xs @ (a, a') # ys @ (b, b') # zs) = del_list x (xs @ (a, a') # ys) @ (b, b') # zs
[PROOF STEP]
by (auto simp: del_list_sorted sorted_lems)


[STATEMENT]
lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mul (S (S (S (S (S Z))))) (S (S (S Z))) = S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z))))))))))))))
[PROOF STEP]
by normalization


text:
"""
    ImplicitForm{T<:Number}

Type defining an implicit Bernstein form.

### Fields

- `array` -- the vector of vectors holding the Bernstein coefficients
- `dim`   -- an integer representing the ambient dimension
"""
struct ImplicitForm{N<:Number}
    array::Vector{Vector{N}}
    dim::Int64
    ncoeffs::Int64
end

include("monomials.jl")

ext: jl


text:
function myclamp(x)
	return x < 0 ? 0 : x > 1 ? 1 : x
end

myclamp(0.33)

max_stars_repo_name: martin-fabbri/colab-notebooks

max_issues_repo_name: martin-fabbri/colab-notebooks

max_forks_repo_name: martin-fabbri/colab-notebooks


text:
struct LazyHelp
    o::Any
    keys::Tuple{Vararg{String}}
end

LazyHelp(o) = LazyHelp(o, ())
LazyHelp(o, k::AbstractString) = LazyHelp(o, (k,))
LazyHelp(o, k1::AbstractString, k2::AbstractString) = LazyHelp(o, (k1, k2))
LazyHelp(o, s::Symbol) = LazyHelp(o, (string(s),))

function show(io::IO, st, h::LazyHelp)
    py"""
    import inspect
    def get_signature(f):
        try:
            return str(inspect.signature(f))
        except ValueError:
            return ""
    """

    o = h.o
    for k in h.keys
        o = o[k]
    end

    fname = hasproperty(o, "__name__") ? o.__name__ : ""
    sig = hasproperty(o, "__call__") ? py"get_signature"(o) : ""
    fdoc = hasproperty(o, "__doc__") ? o.__doc__ : ""

    docstr = """
        $(fname)$(sig)
    $(fdoc)
    """

    print(io, docstr)
end

Base.show(io::IO, h::LazyHelp) = show(io, "text/plain", h)

function Base.Docs.catdoc(hs::LazyHelp...)
    Base.Docs.Text() do io
        for h in hs
            show(io, MIME"text/plain"(), h)
        end
    end
end

macro pyfunc(_pymod, _func)
	pymod = _pymod |> esc
	func = _func |> esc
	quote
		@doc LazyHelp($(pymod), nameof($(func)))
			function $(func)(args...; kwargs...)
				getproperty($(pymod), nameof($(func)))(args...; kwargs...)
			end
	end
end

macro pyclass(_pymod, _class)
	pymod = _pymod |> esc
	class = _class |> esc
	quote
		@doc LazyHelp($(pymod), nameof($(class)))
			struct $(class)
			    pyobj::$(PyObject)
			    $(class)(args...; kwargs...) = new(getproperty($(pymod), nameof($class))(args...; kwargs...))
			end

		PyCall.PyObject(t::$(class)) = t.pyobj

		function Base.propertynames(t::$(class))
		    propertynames(getfield(t, :pyobj))
		end

		function Base.getproperty(t::$(class), s::Symbol)
		    if s ∈ fieldnames($(class))
		        return getfield(t, s)
		    else
		        return getproperty(getfield(t, :pyobj), s)
		    end
		end
	end
end


text:
function force(x::Float64, potential::Potential)
    f(y) = -derivative(potential.f,y)
    f(x)
end

function friction(z::Float64, thermo::Thermostat)
    g = y -> derivative(thermo.distribution,y)
    g(z)/thermo.distribution(z)
end

function forcederivative(potential::Potential)
    force(x) = -derivative(potential.f,x)
    fprime(x) = derivative(force,x)
end

"""
Equations of motion fot a general potential coupled to any thermostat
"""
function DDfield(r::Vector{Float64}, potential::Potential, beta::Float64, thermo::Thermostat)

    (q, p, z) = r

    f = x-> force(x, potential)

    dq_dt = p
    dp_dt = f(q) + friction(z,thermo)*p/beta
    dz_dt = p^2. - 1.0/beta

    [dq_dt, dp_dt, dz_dt]

end

"""
    jacobian(r, potential, beta, thermo)
Returns the jacobian of the DDfield evaluated at the point `r`
"""
function jacobian(r::Vector{Float64}, potential::Potential, beta::Float64, thermo::Thermostat)

    (q,p,z) = r

    fprime = forcederivative(potential)

    distprime(x) = derivative(thermo.distribution,x)
    distprime2(x) = derivative(distprime,x)

    J = [0. 1. 0.; fprime(q)  friction(z, thermo)/beta p/beta*(distprime2(z)/thermo.distribution(z) - friction(z, thermo)^2.); 0. 2.0*p 0.]

end

"""
Evaluates the variational field associated to the DDfield at the extended vector `r` (q,p,z  and 9 more entries representing the coordinates of three tangent vectors)
"""
function variationalDDfield(r_and_phi::Vector{Float64}, potential::Potential, beta::Float64, thermo::Thermostat)

    v = DDfield(r_and_phi[1:3], potential, beta, thermo)
    J = jacobian(r_and_phi[1:3], potential, beta, thermo)
    rmatrix = reshape(r_and_phi[4:end],3,3)
    DPhi = J*rmatrix'

    return append!(v, DPhi'[:])
end

"""
Given a 3x3 matrix  orthogonalize its columns with the Gram-Schmidt procedure
"""
function gramschmidt(u::Matrix{Float64})
    w = eye(3)
    w[:,1] = u[:,1];
    v1 = w[:,1]/norm(w[:,1])
    w[:,2] = u[:,2] - dot(u[:,2],v1)*v1;
    v2 = w[:,2]/norm(w[:,2]);
    w[:,3] = (u[:,3] - dot(u[:,3],v2)*v2 - dot(u[:,3],v1)*v1)

    return w
end

max_stars_repo_name: dapias/STODs

max_issues_repo_name: dapias/STODs

max_forks_repo_name: dapias/STODs


text:
Pkg.update()
using PkgDev
PkgDev.register("UnitRoot")
PkgDev.tag("UnitRoot")
PkgDev.publish()


text:
using MetroMapRuby
using Test
using JuMP
using GLPKMathProgInterface
using MathProgBase

coord1 = EuclideanCoordinate(1, 2)
coord2 = EuclideanCoordinate(1, 3)
station1 = EuclideanStation(1, coord1, "test", false)
station2 = EuclideanStation(2, coord2, "test", false)
station3 = EuclideanStation(3, coord2, "test", false)
station4 = EuclideanStation(4, coord2, "test", false)
station5 = EuclideanStation(5, coord2, "test", false)
station6 = EuclideanStation(6, coord2, "test", false)
station7 = EuclideanStation(7, coord2, "test", false)
station8 = EuclideanStation(8, coord2, "test", false)
station9 = EuclideanStation(9, coord2, "test", false)
line1 = Line("S1")
line2 = Line("S2")
line3 = Line("S3")
line4 = Line("S4")
edge = ProcessedEdge(station1, station2, line1, 0, 1, false)
edge2 = ProcessedEdge(station2, station3, line1, 0, 1, false)
edge3 = ProcessedEdge(station2, station4, line2, 2, 1, false)
edge4 = ProcessedEdge(station5, station2, line2, 2, 1, false)
edge5 = ProcessedEdge(station6, station2, line3, 1, 1, false)
edge6 = ProcessedEdge(station2, station7, line3, 1, 1, false)
edge7 = ProcessedEdge(station8, station2, line4, 3, 1, false)
edge8 = ProcessedEdge(station2, station9, line4, 3, 1, false)
transit_map = InputGraph([station1, station2, station3, station4, station5,
    station6, station7, station8, station9],
    [edge, edge2, edge3, edge4, edge5, edge6, edge7, edge8],
    [line1, line2, line3, line4])

# 9     4    7
#   x   ^   x
#     x | x
# 1 ->  2 -> 3
#     x ^ x
#   x   |   x
# 6     5    8

result = MetroMapRuby.optimize(GLPKSolverMIP(msg_lev = 3), transit_map, false)

@test result.stations[1].coordinate.y ≈ result.stations[2].coordinate.y
@test result.stations[2].coordinate.y ≈ result.stations[3].coordinate.y
@test result.stations[2].coordinate.x ≈ result.stations[4].coordinate.x
@test result.stations[2].coordinate.x ≈ result.stations[5].coordinate.x
@test result.stations[4].coordinate.y > result.stations[5].coordinate.y

@test result.stations[6].coordinate.x ≈ result.stations[9].coordinate.x
@test result.stations[6].coordinate.x ≈ result.stations[1].coordinate.x
@test result.stations[7].coordinate.x ≈ result.stations[8].coordinate.x
@test result.stations[7].coordinate.x ≈ result.stations[3].coordinate.x
@test result.stations[4].coordinate.y ≈ result.stations[9].coordinate.y
@test result.stations[9].coordinate.y ≈ result.stations[7].coordinate.y
@test result.stations[6].coordinate.y ≈ result.stations[8].coordinate.y
@test result.stations[5].coordinate.y ≈ result.stations[6].coordinate.y

max_stars_repo_name: brainfo/MetroMap

max_issues_repo_name: brainfo/MetroMap

max_forks_repo_name: brainfo/MetroMap


text:
module AutoDiff

using CUDA
using CUDA.CUSPARSE
using ForwardDiff
using KernelAbstractions
using SparseArrays
using TimerOutputs
using SparseDiffTools
using ..ExaPF: Spmat, xzeros

import Base: show

"""
    AbstractJacobian

Automatic differentiation for the compressed Jacobians of the
constraints `g(x,u)` with respect to the state `x` and the control `u`
(here called design).

TODO: Use dispatch to unify the code of the state and control Jacobian.
This is currently not done because the abstraction of the indexing is not yet resolved.

"""
abstract type AbstractJacobian end

function _init_seed!(t1sseeds, coloring, ncolor, nmap)
    t1sseedvec = zeros(Float64, ncolor)
    @inbounds for i in 1:nmap
        for j in 1:ncolor
            if coloring[i] == j
                t1sseedvec[j] = 1.0
            end
        end
        t1sseeds[i] = ForwardDiff.Partials{ncolor, Float64}(NTuple{ncolor, Float64}(t1sseedvec))
        t1sseedvec .= 0
    end
end

"""
    StateJacobian

Creates an object for the state Jacobian

* `J::SMT`: Sparse uncompressed Jacobian to be used by linear solver. This is either of type `SparseMatrixCSC` or `CuSparseMatrixCSR`.
* `compressedJ::MT`: Dense compressed Jacobian used for updating values through AD either of type `Matrix` or `CuMatrix`.
* `coloring::VI`: Row coloring of the Jacobian.
* `t1sseeds::VP`: The seeding vector for AD built based on the coloring.
* `t1sF::VD`: Output array of active (AD) type.
* `x::VT`: Input array of passive type. This includes both state and control.
* `t1sx::VD`: Input array of active type.
* `map::VI`: State and control mapping to array `x`
* `varx::SubT`: View of `map` on `x`
* `t1svarx::SubD`: Active (AD) view of `map` on `x`
"""
struct StateJacobian{VI, VT, MT, SMT, VP, VD, SubT, SubD} <: AbstractJacobian
    J::SMT
    compressedJ::MT
    coloring::VI
    t1sseeds::VP
    t1sF::VD
    x::VT
    t1sx::VD
    map::VI
    # Cache views on x and its dual vector to avoid reallocating on the GPU
    varx::SubT
    t1svarx::SubD
    function StateJacobian(F, v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus)
        nv_m = size(v_m, 1)
        nv_a = size(v_a, 1)
        if F isa Array
            VI = Vector{Int}
            VT = Vector{Float64}
            MT = Matrix{Float64}
            SMT = SparseMatrixCSC
            A = Vector
        elseif F isa CuArray
            VI = CuVector{Int}
            VT = CuVector{Float64}
            MT = CuMatrix{Float64}
            SMT = CuSparseMatrixCSR
            A = CuVector
        else
            error("Wrong array type ", typeof(F))
        end

        mappv = [i + nv_m for i in pv]
        mappq = [i + nv_m for i in pq]
        # Ordering for x is (θ_pv, θ_pq, v_pq)
        map = VI(vcat(mappv, mappq, pq))
        nmap = size(map,1)

        # Used for sparsity detection with randomized inputs
        function residual_jacobian(V, Ybus, pv, pq)
            n = size(V, 1)
            Ibus = Ybus*V
            diagV       = sparse(1:n, 1:n, V, n, n)
            diagIbus    = sparse(1:n, 1:n, Ibus, n, n)
            diagVnorm   = sparse(1:n, 1:n, V./abs.(V), n, n)

            dSbus_dVm = diagV * conj(Ybus * diagVnorm) + conj(diagIbus) * diagVnorm
            dSbus_dVa = 1im * diagV * conj(diagIbus - Ybus * diagV)

            j11 = real(dSbus_dVa[[pv; pq], [pv; pq]])
            j12 = real(dSbus_dVm[[pv; pq], pq])
            j21 = imag(dSbus_dVa[pq, [pv; pq]])
            j22 = imag(dSbus_dVm[pq, pq])

            J = [j11 j12; j21 j22]
        end

        # Need a host arrays for the sparsity detection below
        spmap = Vector(map)
        hybus_re = Spmat{Vector{Int}, Vector{Float64}}(ybus_re)
        hybus_im = Spmat{Vector{Int}, Vector{Float64}}(ybus_im)
        n = nv_a
        Yre = SparseMatrixCSC{Float64,Int64}(n, n, hybus_re.colptr, hybus_re.rowval, hybus_re.nzval)
        Yim = SparseMatrixCSC{Float64,Int64}(n, n, hybus_im.colptr, hybus_im.rowval, hybus_im.nzval)
        Y = Yre .+ 1im .* Yim
        # Randomized inputs
        Vre = Float64.([i for i in 1:n])
        Vim = Float64.([i for i in n+1:2*n])
        V = Vre .+ 1im .* Vim
        J = residual_jacobian(V, Y, pv, pq)
        coloring = VI(matrix_colors(J))
        ncolor = size(unique(coloring),1)
        if F isa CuArray
            J = CuSparseMatrixCSR(J)
        end
        t1s{N} = ForwardDiff.Dual{Nothing,Float64, N} where N
        x = VT(zeros(Float64, nv_m + nv_a))
        t1sx = A{t1s{ncolor}}(x)
        t1sF = A{t1s{ncolor}}(zeros(Float64, nmap))

        t1sseeds = A{ForwardDiff.Partials{ncolor,Float64}}(undef, nmap)
        _init_seed!(t1sseeds, coloring, ncolor, nmap)

        compressedJ = MT(zeros(Float64, ncolor, nmap))
        # Views
        varx = view(x, map)
        t1svarx = view(t1sx, map)
        VP = typeof(t1sseeds)
        VD = typeof(t1sx)
        return new{VI, VT, MT, SMT, VP, VD, typeof(varx), typeof(t1svarx)}(
            J, compressedJ, coloring, t1sseeds, t1sF, x, t1sx, map, varx, t1svarx
        )
    end
end

"""
    ControlJacobian

Creates an object for the control Jacobian.

* `J::SMT`: Sparse uncompressed Jacobian to be used by linear solver. This is either of type `SparseMatrixCSC` or `CuSparseMatrixCSR`.
* `compressedJ::MT`: Dense compressed Jacobian used for updating values through AD either of type `Matrix` or `CuMatrix`.
* `coloring::VI`: Row coloring of the Jacobian.
* `t1sseeds::VP`: The seeding vector for AD built based on the coloring.
* `t1sF::VD`: Output array of active (AD) type.
* `x::VT`: Input array of passive type. This includes both state and control.
* `t1sx::VD`: Input array of active type.
* `map::VI`: State and control mapping to array `x`
* `varx::SubT`: View of `map` on `x`
* `t1svarx::SubD`: Active (AD) view of `map` on `x`
"""
struct ControlJacobian{VI, VT, MT, SMT, VP, VD, SubT, SubD} <: AbstractJacobian
    J::SMT
    compressedJ::MT
    coloring::VI
    t1sseeds::VP
    t1sF::VD
    x::VT
    t1sx::VD
    map::VI
    # Cache views on x and its dual vector to avoid reallocating on the GPU
    varx::SubT
    t1svarx::SubD
    function ControlJacobian(F, v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus)
        nv_m = size(v_m, 1)
        nv_a = size(v_a, 1)
        npbus = size(pinj, 1)
        nref = size(ref, 1)
        if F isa Array
            VI = Vector{Int}
            VT = Vector{Float64}
            MT = Matrix{Float64}
            SMT = SparseMatrixCSC
            A = Vector
        elseif F isa CuArray
            VI = CuVector{Int}
            VT = CuVector{Float64}
            MT = CuMatrix{Float64}
            SMT = CuSparseMatrixCSR
            A = CuVector
        else
            error("Wrong array type ", typeof(F))
        end

        mappv =  [i + nv_a for i in pv]
        map = VI(vcat(ref, mappv, pv))
        nmap = size(map,1)

        # Used for sparsity detection with randomized inputs
        function residual_jacobian(V, Ybus, pinj, qinj, ref, pv, pq)
            n = size(V, 1)
            Ibus = Ybus*V
            diagV       = sparse(1:n, 1:n, V, n, n)
            diagIbus    = sparse(1:n, 1:n, Ibus, n, n)
            diagVnorm   = sparse(1:n, 1:n, V./abs.(V), n, n)

            dSbus_dVm = diagV * conj(Ybus * diagVnorm) + conj(diagIbus) * diagVnorm
            dSbus_dpbus = diagV * conj(Ybus * diagVnorm) + conj(diagIbus) * diagVnorm

            j11 = real(dSbus_dVm[[pv; pq], [ref; pv; pv]])
            j21 = imag(dSbus_dVm[pq, [ref; pv; pv]])
            J = [j11; j21]
        end

        # Need a host arrays for the sparsity detection below
        spmap = Vector(map)
        hybus_re = Spmat{Vector{Int}, Vector{Float64}}(ybus_re)
        hybus_im = Spmat{Vector{Int}, Vector{Float64}}(ybus_im)
        n = nv_a
        Yre = SparseMatrixCSC{Float64,Int64}(n, n, hybus_re.colptr, hybus_re.rowval, hybus_re.nzval)
        Yim = SparseMatrixCSC{Float64,Int64}(n, n, hybus_im.colptr, hybus_im.rowval, hybus_im.nzval)
        Y = Yre .+ 1im .* Yim
        # Randomized inputs
        Vre = Float64.([i for i in 1:n])
        Vim = Float64.([i for i in n+1:2*n])
        V = Vre .+ 1im .* Vim
        J = residual_jacobian(V, Y, pinj, qinj, ref, pv, pq)
        coloring = VI(matrix_colors(J))
        ncolor = size(unique(coloring),1)
        if F isa CuArray
            J = CuSparseMatrixCSR(J)
        end
        t1s{N} = ForwardDiff.Dual{Nothing,Float64, N} where N
        x = xzeros(VT, npbus + nv_a)
        t1sx = A{t1s{ncolor}}(x)
        t1sF = A{t1s{ncolor}}(zeros(Float64, length(F)))
        t1sseeds = A{ForwardDiff.Partials{ncolor,Float64}}(undef, nmap)
        _init_seed!(t1sseeds, coloring, ncolor, nmap)

        compressedJ = MT(zeros(Float64, ncolor, length(F)))
        # Views
        varx = view(x, map)
        t1svarx = view(t1sx, map)
        VP = typeof(t1sseeds)
        VD = typeof(t1sx)
        return new{VI, VT, MT, SMT, VP, VD, typeof(varx), typeof(t1svarx)}(
            J, compressedJ, coloring, t1sseeds, t1sF, x, t1sx, map, varx, t1svarx
        )
    end
end

"""
    seed_kernel_cpu!

Seeding on the CPU, not parallelized.

"""
function seed_kernel_cpu!(
    duals::AbstractArray{ForwardDiff.Dual{T,V,N}}, x,
    seeds::AbstractArray{ForwardDiff.Partials{N,V}}
) where {T,V,N}
    for i in 1:size(duals,1)
        duals[i] = ForwardDiff.Dual{T,V,N}(x[i], seeds[i])
    end
end

"""
    seed_kernel_gpu!

Seeding on GPU parallelized over the `ncolor` number of duals

"""
function seed_kernel_gpu!(
    duals::AbstractArray{ForwardDiff.Dual{T,V,N}}, x,
    seeds::AbstractArray{ForwardDiff.Partials{N,V}}
) where {T,V,N}
    index = (blockIdx().x - 1) * blockDim().x + threadIdx().x
    stride = blockDim().x * gridDim().x
    for i in index:stride:size(duals,1)
        duals[i] = ForwardDiff.Dual{T,V,N}(x[i], seeds[i])
    end
end

"""
    seed_kernel!

Calling the GPU seeding kernel

"""
function seed_kernel!(t1sseeds::CuVector{ForwardDiff.Partials{N,V}}, varx, t1svarx, nbus) where {N, V}
    nthreads = 256
    nblocks = div(nbus, nthreads, RoundUp)
    CUDA.@sync begin
        @cuda threads=nthreads blocks=nblocks seed_kernel_gpu!(
            t1svarx,
            varx,
            t1sseeds,
        )
    end
end

"""
    seed_kernel!(t1sseeds::Vector{ForwardDiff.Partials{N,V}}, varx, t1svarx, nbus) where {N, V}

Calling the CPU seeding kernel

"""
function seed_kernel!(t1sseeds::Vector{ForwardDiff.Partials{N,V}}, varx, t1svarx, nbus) where {N, V}
    seed_kernel_cpu!(t1svarx, varx, t1sseeds)
end

"""
    getpartials_kernel_cpu!(compressedJ, t1sF)

Extract the partials from the AutoDiff dual type on the CPU and put it in the
compressed Jacobian

"""
function getpartials_kernel_cpu!(compressedJ, t1sF)
    for i in 1:size(t1sF,1) # Go over outputs
        compressedJ[:, i] .= ForwardDiff.partials.(t1sF[i]).values
    end
end

"""
    getpartials_kernel_gpu!(compressedJ, t1sF)

Extract the partials from the AutoDiff dual type on the GPU and put it in the
compressed Jacobian

"""
function getpartials_kernel_gpu!(compressedJ, t1sF)
    index = (blockIdx().x - 1) * blockDim().x + threadIdx().x
    stride = blockDim().x * gridDim().x
    for i in index:stride:size(t1sF, 1) # Go over outputs
        for j in eachindex(ForwardDiff.partials.(t1sF[i]).values)
            @inbounds compressedJ[j, i] = ForwardDiff.partials.(t1sF[i]).values[j]
        end
    end
end

"""
    getpartials_kernel!(compressedJ::CuArray{T, 2}, t1sF, nbus) where T

Calling the GPU partial extraction kernel

"""
function getpartials_kernel!(compressedJ::CuArray{T, 2}, t1sF, nbus) where T
    nthreads = 256
    nblocks = div(nbus, nthreads, RoundUp)
    CUDA.@sync begin
        @cuda threads=nthreads blocks=nblocks getpartials_kernel_gpu!(
            compressedJ,
            t1sF
        )
    end
end

"""
    getpartials_kernel!(compressedJ::Array{T, 2}, t1sF, nbus) where T

Calling the CPU partial extraction kernel

"""
function getpartials_kernel!(compressedJ::Array{T, 2}, t1sF, nbus) where T
    getpartials_kernel_cpu!(compressedJ, t1sF)
end

"""
    uncompress_kernel_gpu!(J_nzVal, J_rowPtr, J_colVal, compressedJ, coloring, nmap)

Uncompress the compressed Jacobian matrix from `compressedJ` to sparse CSR on
the GPU. Only bitarguments are allowed for the kernel.
(for GPU only) TODO: should convert to @kernel
"""
function uncompress_kernel_gpu!(J_nzVal, J_rowPtr, J_colVal, compressedJ, coloring, nmap)
    index = (blockIdx().x - 1) * blockDim().x + threadIdx().x
    stride = blockDim().x * gridDim().x
    for i in index:stride:nmap
        for j in J_rowPtr[i]:J_rowPtr[i+1]-1
            @inbounds J_nzVal[j] = compressedJ[coloring[J_colVal[j]], i]
        end
    end
end

"""
    uncompress_kernel!(J::SparseArrays.SparseMatrixCSC, compressedJ, coloring)

Uncompress the compressed Jacobian matrix from `compressedJ` to sparse CSC on
the CPU.
"""
function uncompress_kernel!(J::SparseArrays.SparseMatrixCSC, compressedJ, coloring)
    # CSC is column oriented: nmap is equal to number of columns
    nmap = size(J, 2)
    @assert(maximum(coloring) == size(compressedJ,1))
    for i in 1:nmap
        for j in J.colptr[i]:J.colptr[i+1]-1
            @inbounds J.nzval[j] = compressedJ[coloring[i], J.rowval[j]]
        end
    end
end

"""
    uncompress_kernel!(J::CUDA.CUSPARSE.CuSparseMatrixCSR, compressedJ, coloring)

Uncompress the compressed Jacobian matrix from `compressedJ` to sparse CSC on
the GPU by calling the kernel [`uncompress_kernel_gpu!`](@ref).
"""
function uncompress_kernel!(J::CUDA.CUSPARSE.CuSparseMatrixCSR, compressedJ, coloring)
    # CSR is row oriented: nmap is equal to number of rows
    nmap = size(J, 1)
    nthreads = 256
    nblocks = div(nmap, nthreads, RoundUp)
    CUDA.@sync begin
        @cuda threads=nthreads blocks=nblocks uncompress_kernel_gpu!(
                J.nzVal,
                J.rowPtr,
                J.colVal,
                compressedJ,
                coloring, nmap
        )
    end
end

"""
    residual_jacobian!(arrays::StateJacobian,
                        residual_polar!,
                        v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus,
                        timer = nothing)

Update the sparse Jacobian entries using AutoDiff. No allocations are taking place in this function.

* `arrays::StateJacobian`: Factory created Jacobian object to update
* `residual_polar`: Primal function
* `v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus`: Inputs both
  active and passive parameters. Active inputs are mapped to `x` via the preallocated views.

"""
function residual_jacobian!(arrays::StateJacobian,
                             residual_polar!,
                             v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus,
                             timer = nothing)
    @timeit timer "Before" begin
        @timeit timer "Setup" begin
            nv_m = size(v_m, 1)
            nv_a = size(v_a, 1)
            nmap = size(arrays.map, 1)
            n = nv_m + nv_a
        end
        @timeit timer "Arrays" begin
            arrays.x[1:nv_m] .= v_m
            arrays.x[nv_m+1:nv_m+nv_a] .= v_a
            arrays.t1sx .= arrays.x
            arrays.t1sF .= 0.0
        end
    end
    @timeit timer "Seeding" begin
        seed_kernel!(arrays.t1sseeds, arrays.varx, arrays.t1svarx, nbus)
    end

    @timeit timer "Function" begin
        residual_polar!(
            arrays.t1sF,
            view(arrays.t1sx, 1:nv_m),
            view(arrays.t1sx, nv_m+1:nv_m+nv_a),
            ybus_re, ybus_im,
            pinj, qinj,
            pv, pq, nbus
        )
    end

    @timeit timer "Get partials" begin
        getpartials_kernel!(arrays.compressedJ, arrays.t1sF, nbus)
    end
    @timeit timer "Uncompress" begin
        uncompress_kernel!(arrays.J, arrays.compressedJ, arrays.coloring)
    end
    return nothing
end

"""
    residual_jacobian!(arrays::ControlJacobian,
                        residual_polar!,
                        v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus,
                        timer = nothing)

Update the sparse Jacobian entries using AutoDiff. No allocations are taking place in this function.

* `arrays::ControlJacobian`: Factory created Jacobian object to update
* `residual_polar`: Primal function
* `v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus`: Inputs both active and passive parameters. Active inputs are mapped to `x` via the preallocated views.

"""
function residual_jacobian!(arrays::ControlJacobian,
                             residual_polar!,
                             v_m, v_a, ybus_re, ybus_im, pinj, qinj, pv, pq, ref, nbus,
                             timer = nothing)

    @timeit timer "Before" begin
        @timeit timer "Setup" begin
            npinj = size(pinj , 1)
            nv_m = size(v_m, 1)
            nmap = size(arrays.map, 1)
            n = npinj + nv_m
        end
        @timeit timer "Arrays" begin
            arrays.x[1:nv_m] .= v_m
            arrays.x[nv_m+1:nv_m+npinj] .= pinj
            arrays.t1sx .= arrays.x
            arrays.t1sF .= 0.0
        end
    end
    @timeit timer "Seeding" begin
        seed_kernel!(arrays.t1sseeds, arrays.varx, arrays.t1svarx, nbus)
    end
    @timeit timer "Function" begin
        residual_polar!(
            arrays.t1sF,
            view(arrays.t1sx, 1:nv_m),
            v_a,
            ybus_re, ybus_im,
            view(arrays.t1sx, nv_m+1:nv_m + npinj), qinj,
            pv, pq, nbus
        )
    end

    @timeit timer "Get partials" begin
        getpartials_kernel!(arrays.compressedJ, arrays.t1sF, nbus)
    end
    @timeit timer "Uncompress" begin
        # Uncompress matrix. Sparse matrix elements have different names with CUDA
        uncompress_kernel!(arrays.J, arrays.compressedJ, arrays.coloring)
    end
end

function Base.show(io::IO, jacobian::AbstractJacobian)
    ncolor = size(unique(jacobian.coloring), 1)
    print(io, "Number of Jacobian colors: ", ncolor)
end

end


text:
export Sdd, SddMgr,
    SddLeafNode, SddInnerNode, SddLiteralNode, SddConstantNode,
    Sdd⋀Node, Sdd⋁Node,
    sdd_mgr_for,
    (¬), (∨), (∧), (⇒), (⇐), (⇔)

#############
# Trimmed Sdds
#############

"Root of the trimmed Sdd circuit node hierarchy"
abstract type Sdd <: StructLogicCircuit end

#############
# Elements and XY Partitions
#############

"Represents elements that are not yet compiled into conjunctions"
struct Element
    prime::Sdd
    sub::Sdd
end

"Represent an XY-partition that has not yet been compiled into a disjunction"
const XYPartition = Vector{Element}

"Unique nodes cache for decision nodes"
const Unique⋁Cache = Dict{XYPartition,Sdd}

"Broader definition of an XYPartition, also including vectors of nodes"

Base.hash(x::XYPartition) = mapreduce(e -> hash(e.prime, hash(e.sub)), ⊻, x)

function Base.isequal(x::XYPartition, y::XYPartition)
    length(x) != length(y) && return false
    (x == y) && return true
    # note: the rest of this function could be removed if the XYPartitions were sorted, but that is not advantageous: the sorting is too slow
    return all(x) do e1
        any(y) do e2
            e1.prime === e2.prime && e1.sub === e2.sub
        end
    end
end

#############
# Apply cache
#############

"Representation of the arguments of an Apply call"
struct ApplyArgs
    a1::Sdd
    a2::Sdd
end

Base.hash(aa::ApplyArgs) = hash(aa.a1) ⊻ hash(aa.a2)
Base.isequal(x::ApplyArgs,y::ApplyArgs) =
    (x.a1 === y.a1 && x.a2 === y.a2 ) || (x.a1 === y.a2 && x.a2 === y.a1)

"Apply cache for the result of conjunctions and disjunctions"
const ApplyCache = Dict{ApplyArgs,Sdd}

#############
# Trimmed Sdd managers
#############

"Root of the SDD manager node hierarchy"
abstract type SddMgr <: Vtree end

"SDD manager inner vtree node for trimmed SDD nodes"
mutable struct SddMgrInnerNode <: SddMgr

    left::SddMgr
    right::SddMgr

    parent::Union{SddMgrInnerNode, Nothing}

    variables::BitSet
    unique⋁cache::Unique⋁Cache

    conjoin_cache::ApplyCache

    SddMgrInnerNode(left::SddMgr, right::SddMgr) where D = begin
        @assert isdisjoint(variables(left), variables(right))
        this = new(left, right, nothing,
            union(variables(left), variables(right)),
            Unique⋁Cache(), ApplyCache())
        @assert left.parent === nothing
        left.parent = this
        @assert right.parent === nothing
        right.parent = this
        this
    end

end

"SDD manager leaf vtree node for trimmed SDD nodes"
mutable struct SddMgrLeafNode <: SddMgr

    var::Var
    parent::Union{SddMgrInnerNode, Nothing}

    positive_literal::Sdd
    negative_literal::Sdd

    SddMgrLeafNode(v::Var) = begin
        this = new(v, nothing)
        this.positive_literal = construct_new_sdd_literal(this, var2lit(v))
        this.negative_literal = construct_new_sdd_literal(this, -var2lit(v))
        this
    end

end

@inline NodeType(::SddMgrLeafNode) = Leaf()
@inline NodeType(::SddMgrInnerNode) = Inner()

#############
# Sdd nodes
#############

"A SDD logical leaf node"
abstract type SddLeafNode <: Sdd end

"A SDD logical inner node"
abstract type SddInnerNode <: Sdd end

"A SDD logical literal leaf node, representing the positive or negative literal of its variable"
mutable struct SddLiteralNode <: SddLeafNode
    literal::Lit
    vtree::SddMgrLeafNode
end

"""
A SDD logical constant leaf node, representing true or false.
These are the only structured nodes that don't have an associated vtree node (cf. SDD file format)
"""
struct SddConstantNode <: SddLeafNode
    constant::Bool
end

"Canonical true Sdd node"
const true_sdd = SddConstantNode(true)

"Canonical false Sdd node"
const false_sdd = SddConstantNode(false)

"A SDD logical conjunction node"
mutable struct Sdd⋀Node <: SddInnerNode
    prime::Sdd
    sub::Sdd
    vtree::SddMgrInnerNode
end

"A SDD logical disjunction node"
mutable struct Sdd⋁Node <: SddInnerNode
    children::Vector{Sdd⋀Node}
    vtree::SddMgrInnerNode
    negation::Sdd⋁Node
    Sdd⋁Node(ch,v) = new(ch, v) # leave negation uninitialized
    Sdd⋁Node(ch,v,neg) = new(ch, v, neg)
end

#####################
# traits
#####################

@inline GateType(::Type{<:SddLiteralNode}) = LiteralGate()
@inline GateType(::Type{<:SddConstantNode}) = ConstantGate()
@inline GateType(::Type{<:Sdd⋀Node}) = ⋀Gate()
@inline GateType(::Type{<:Sdd⋁Node}) = ⋁Gate()

#####################
# Constructor
#####################

SddMgr(v::Var) = SddMgrLeafNode(v)
SddMgr(left::SddMgr, right::SddMgr) = SddMgrInnerNode(left, right)

"Obtain an SDD manager that can support compiling the given circuit"
sdd_mgr_for(c::Sdd) = mgr(c)
sdd_mgr_for(c::StructLogicCircuit) =
    (vtree(c) isa SddMgr) ? vtree(c) : SddMgr(vtree(c))
sdd_mgr_for(c::LogicCircuit) =
    SddMgr(SddMgr.(Var.(variables(c))), :balanced) # this could be "smarter" finding a good vtree

"Helper function to construct new SDD literal objects in SddMgrLeafNode constructor"
function construct_new_sdd_literal(n::SddMgrLeafNode, l::Lit)::SddLiteralNode
    @assert n.var == lit2var(l) "Cannot compile literal $l respecting vtree leaf for variable $(n.var)"
    SddLiteralNode(l,n)
end

# logical syntactic sugar

"Logical negation"
(¬)(x::Sdd) = !x
"Logical disjunction"
(∨)(x::Sdd, y::Sdd) = x | y
"Logical conjunction"
(∧)(x::Sdd, y::Sdd) = x & y
"Material logical implication"
(⇒)(x::Sdd, y::Sdd) = ¬x ∨ y
"Material logical implication (reverse)"
(⇐)(x::Sdd, y::Sdd) = (y ⇒ x)
"Bidirectional logical implication"
(⇔)(x::Sdd, y::Sdd) = (x ⇒ y) ∧ (y ⇒ x)

max_issues_repo_name: Juice-jl/LogicCircuits

max_forks_repo_name: Juice-jl/LogicCircuits


text:
using DFWannier
using Optim
using DataStructures
function optimize_l()
    T = Float64

    job = ldj("/home/ponet/HfO2/NSOC/")
    wanjob = add_wan_data(job)

    k_points = qe_read_ks_from_bands_file("/home/ponet/HfO2/SOC/bands.out")[2]
    test_eig, , , = calc_observables(wanjob.structure, kpoints[1])

    bands = qe_read_bands_file("/home/ponet/HfO2/SOC/bands.out", T)[b:e]

    at_ids = getfield.(unique(wanjob.structure.atoms), :id)

    lsocs = OrderedDict{Symbol, T}()
    for id in at_ids
        lsocs[id] = zero(T)
    end
    function f(lambdas)
        for (key, l) in zip(keys(lsocs), lambdas)
            lsocs[key] = l
        end
        set_soc!(wanjob.structure, lsocs...)

        energy, , , = calc_observables(wanjob.structure, k_points)

        out_diff = 0.0
        for i=1:length(bands)
            calcbands = [val[i] for val in energy]
            for (calc, exact) in zip(calcbands[80:120], bands[i].eigvals[80:120])
                out_diff += abs(calc-exact)
            end
        end
        return out_diff
    end
    return optimize(f, [lambdaHf, lambdaO], show_trace = true, show_every = 1, extended_trace=true)
end
results = optimize_l()
println(results)


text:
module MICE

using DataFrames
using GLM: fit, LinearModel, predict
using Statistics: mean
using StatsModels: term, schema, modelcols, apply_schema
import CSV
using StatsBase: sample

export mice

function mice(data::DataFrame; max_iterations = 5)
    data_missings = ismissing.(data)

    # Do naive imputation using means
    data_imputed = naive_imputation(data, mean)

    # Do better imputation using LMs
    for iteration in 1:max_iterations

        # TODO: Add early stopping when abs(max(X_t - X_{t-1}))/abs(max(X[known_vals])) < tol

        data_imputed_temp = copy(data_imputed)
        for response_variable in names(data)
            # The explanatory variables are all the other variables
            explanatory_variables = filter(n -> n != response_variable, names(data))

            # Fit a linear model with an intercept and each explanatory variable
            f = term(response_variable) ~ term(1) + foldl(+, term.(explanatory_variables))

            predicted_values = predictive_mean_matching(data_imputed, data_missings, f)

            # # Fit the model
            # # @info data_train
            # # @info f
            # # CSV.write("df.csv", data_train)
            # model = fit(LinearModel, f, data_train)
            # # Predict
            # predicted_values::Vector = predict(model, data_imputed)

            # Replace missing values with the new imputed values
            data_imputed_temp[:, response_variable] = predicted_values
        end
        data_imputed = copy(data_imputed_temp)
    end
    return data_imputed
end

"""
Perform a naïve imputation of the missing values in `data` using the function `f`.
"""
function naive_imputation(data, f = mean)
    data_imputed = copy(data)
    for n in names(data)
        # Calculate the average of the non-missing values
        imputed_value = f(skipmissing(data_imputed[:, n]))
        # Replace the missing values with the imputed value
        data_imputed[:, n] = coalesce.(data_imputed[:, n], imputed_value)
    end
    return data_imputed
end

function predictive_mean_matching(data, data_missings, formula; n = 5)
    formula_data = apply_schema(formula, schema(formula, data))
    formula_missings = apply_schema(formula, schema(formula, data_missings))

    response_variable = modelcols(formula_data.lhs, data)
    response_missings = modelcols(formula_missings.lhs, data_missings)

    # Only fit the model to rows where the response variable is not missing
    data_train = data[.!response_missings, :]

    @info formula
    CSV.write("df.csv", data_train)
    model = fit(LinearModel, formula_data, data_train)
    predicted_values = predict(model, data)

    output = zeros(length(response_variable))
    for (i, is_missing) in enumerate(response_missings)
        if is_missing
            # Calculate the distance between the predicted value being imputed and the predicted values of the other points
            donor_candidates_distances = abs.(predicted_values[i] .- predicted_values)
            # Filter to only the candiates where the true value is known
            donor_candidates = filter((j, v) -> !response_missings[j], enumerate(donor_candidates_distances))
            donor_candidates = sort(donor_candidates, by = (j, v) -> v)[2:(n + 1)]
            # Choose one of the candidates to be the donor
            donor_index, _ = sample(donor_candidates)
            # Set the value being imputed to the donor value
            output[i] = response_column[donor_index]
        else
            output[i] = response_column[i]
        end
    end
    return output
end

end # module


text:
using Test

using ScottishTaxBenefitModel
using .ModelHousehold: Household, Person, People_Dict, default_bu_allocation
using .Pensions: impute_employer_pension!
using .Definitions

@testset "Employer's Pension Imputation" begin

    hh = ExampleHouseholdGetter.get_household( "mel_c2" )
    cpl= get_example( cpl_w_2_children_hh )
    head = get_head( cpl )

    @test head.employment_status == Full_time_Employee
    @test get(head.income,pension_contributions_employer,0.0) == 0.0
    head.income[wages] = 1_000;
    impute_employer_pension!( head )
    @test head.income[wages]*0.3 > head.income[pension_contributions_employer]

end

@testset "Pension correction test on full dataset" begin
    nhhs,npeople = init_data( reset = true, Settings() )
    itsys_scot :: IncomeTaxSys = get_tax( scotland = true )

    for hno in 1:nhhs

    end
end

max_stars_repo_name: grahamstark/ScottishTaxBenefitModel

max_issues_repo_name: grahamstark/ScottishTaxBenefitModel

max_forks_repo_name: grahamstark/ScottishTaxBenefitModel


text:
const LimbicSystem = BilateralStructure(:limbic_system)

const LimbicLobe = BilateralStructure(:limbic_lobe)

const Parahippocampus = BilateralStructure(:parahippocampus)

const SeptalNuclei = BilateralStructure(:septal_nuclei)

const NucleusAccumbens = BilateralStructure(:nucleus_accumbens)

const PapezCircuit = BilateralStructure(:papez_circuit)