[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