[STATEMENT]
theorem primorial'_primes_omega_le:
  fixes n :: nat
  assumes n: "n > 0"
  shows "primorial' (primes_omega n) \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' (primes_omega n) \<le> n
[PROOF STEP]
proof (cases "n = 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
 2. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
n = 1

goal (2 subgoals):
 1. n = 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
 2. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 1

goal (1 subgoal):
 1. primorial' (primes_omega n) \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
primorial' (primes_omega n) \<le> n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
n \<noteq> 1

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
n \<noteq> 1
[PROOF STEP]
have "n > 1"
[PROOF STATE]
proof (prove)
using this:
0 < n
n \<noteq> 1

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

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
define m where "m = primes_omega n"
[PROOF STATE]
proof (state)
this:
m = primes_omega n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
define P where "P = {p. prime p \<and> real p \<le> primes_pi n}"
[PROOF STATE]
proof (state)
this:
P = {p. prime p \<and> real p \<le> primes_pi (real n)}

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
define ps where "ps = sorted_list_of_set (prime_factors n)"
[PROOF STATE]
proof (state)
this:
ps = sorted_list_of_set (prime_factors n)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have set_ps: "set ps = prime_factors n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ps = prime_factors n
[PROOF STEP]
by (simp add: ps_def)
[PROOF STATE]
proof (state)
this:
set ps = prime_factors n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have [simp]: "length ps = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ps = m
[PROOF STEP]
by (simp add: ps_def m_def primes_omega_def)
[PROOF STATE]
proof (state)
this:
length ps = m

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "sorted ps" "distinct ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sorted ps &&& distinct ps
[PROOF STEP]
by (simp_all add: ps_def)
[PROOF STATE]
proof (state)
this:
sorted ps
distinct ps

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
hence mono: "strict_mono_on {..<m} (\<lambda>k. ps ! k)"
[PROOF STATE]
proof (prove)
using this:
sorted ps
distinct ps

goal (1 subgoal):
 1. strict_mono_on {..<m} ((!) ps)
[PROOF STEP]
by (intro strict_mono_onI le_neq_trans) (auto simp: sorted_nth_mono distinct_conv_nth)
[PROOF STATE]
proof (state)
this:
strict_mono_on {..<m} ((!) ps)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
from \<open>n > 1\<close>
[PROOF STATE]
proof (chain)
picking this:
1 < n
[PROOF STEP]
have "m > 0"
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. 0 < m
[PROOF STEP]
by (auto simp: m_def prime_factorization_empty_iff intro!: Nat.gr0I)
[PROOF STATE]
proof (state)
this:
0 < m

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "primorial' m = (\<Prod>k<m. nth_prime k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' m = prod nth_prime {..<m}
[PROOF STEP]
using \<open>m > 0\<close>
[PROOF STATE]
proof (prove)
using this:
0 < m

goal (1 subgoal):
 1. primorial' m = prod nth_prime {..<m}
[PROOF STEP]
by (simp add: of_nat_diff primorial'_def m_def)
[PROOF STATE]
proof (state)
this:
primorial' m = prod nth_prime {..<m}

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
primorial' m = prod nth_prime {..<m}

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "(\<Prod>k<m. nth_prime k) \<le> (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod nth_prime {..<m} \<le> (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n)
[PROOF STEP]
proof (intro prod_mono conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
assume i: "i \<in> {..<m}"
[PROOF STATE]
proof (state)
this:
i \<in> {..<m}

goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
hence p: "ps ! i \<in> prime_factors n"
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<m}

goal (1 subgoal):
 1. ps ! i \<in># prime_factorization n
[PROOF STEP]
using set_ps
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<m}
set ps = prime_factors n

goal (1 subgoal):
 1. ps ! i \<in># prime_factorization n
[PROOF STEP]
by (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
ps ! i \<in># prime_factorization n

goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
with i set_ps
[PROOF STATE]
proof (chain)
picking this:
i \<in> {..<m}
set ps = prime_factors n
ps ! i \<in># prime_factorization n
[PROOF STEP]
have "nth_prime i \<le> ps ! i"
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<m}
set ps = prime_factors n
ps ! i \<in># prime_factorization n

goal (1 subgoal):
 1. nth_prime i \<le> ps ! i
[PROOF STEP]
by (intro nth_prime_le_prime_sequence[where n = m] mono) (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
nth_prime i \<le> ps ! i

goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_prime i \<le> ps ! i

goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
have "\<dots> \<le> ps ! i ^ multiplicity (ps ! i) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps ! i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
using p
[PROOF STATE]
proof (prove)
using this:
ps ! i \<in># prime_factorization n

goal (1 subgoal):
 1. ps ! i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
by (intro self_le_power) (auto simp: prime_factors_multiplicity dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
ps ! i \<le> ps ! i ^ multiplicity (ps ! i) n

goal (2 subgoals):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
 2. \<And>i. i \<in> {..<m} \<Longrightarrow> nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
show "nth_prime i \<le> \<dots>"
[PROOF STATE]
proof (prove)
using this:
nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n

goal (1 subgoal):
 1. nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nth_prime i \<le> ps ! i ^ multiplicity (ps ! i) n

goal (1 subgoal):
 1. \<And>i. i \<in> {..<m} \<Longrightarrow> 0 \<le> nth_prime i
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
prod nth_prime {..<m} \<le> (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod nth_prime {..<m} \<le> (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "\<dots> = (\<Prod>p\<in>(\<lambda>i. ps ! i) ` {..<m}. p ^ multiplicity p n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n) = (\<Prod>p\<in>(!) ps ` {..<m}. p ^ multiplicity p n)
[PROOF STEP]
using \<open>distinct ps\<close>
[PROOF STATE]
proof (prove)
using this:
distinct ps

goal (1 subgoal):
 1. (\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n) = (\<Prod>p\<in>(!) ps ` {..<m}. p ^ multiplicity p n)
[PROOF STEP]
by (subst prod.reindex) (auto intro!: inj_onI simp: distinct_conv_nth)
[PROOF STATE]
proof (state)
this:
(\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n) = (\<Prod>p\<in>(!) ps ` {..<m}. p ^ multiplicity p n)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>k<m. ps ! k ^ multiplicity (ps ! k) n) = (\<Prod>p\<in>(!) ps ` {..<m}. p ^ multiplicity p n)

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "(\<lambda>i. ps ! i) ` {..<m} = set ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) ps ` {..<m} = set ps
[PROOF STEP]
by (auto simp: set_conv_nth)
[PROOF STATE]
proof (state)
this:
(!) ps ` {..<m} = set ps

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(!) ps ` {..<m} = set ps

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "set ps = prime_factors n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ps = prime_factors n
[PROOF STEP]
by (simp add: set_ps)
[PROOF STATE]
proof (state)
this:
set ps = prime_factors n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set ps = prime_factors n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
have "(\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n
[PROOF STEP]
using \<open>n > 1\<close>
[PROOF STATE]
proof (prove)
using this:
1 < n

goal (1 subgoal):
 1. (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n
[PROOF STEP]
by (intro prime_factorization_nat [symmetric]) auto
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n

goal (1 subgoal):
 1. n \<noteq> 1 \<Longrightarrow> primorial' (primes_omega n) \<le> n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
primorial' m \<le> n
[PROOF STEP]
show "primorial' m \<le> n"
[PROOF STATE]
proof (prove)
using this:
primorial' m \<le> n

goal (1 subgoal):
 1. primorial' m \<le> n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
primorial' m \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primes_omega_less_primes_omega_primorial:
  fixes n :: nat
  assumes n: "n > 0" and "n < primorial x"
  shows "primes_omega n < primes_omega (primorial x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_omega n < primes_omega (primorial x)
[PROOF STEP]
proof (cases "n > 1")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
 2. \<not> 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 1 < n

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
 2. \<not> 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
have [simp]: "primes_pi 2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_pi 2 = 1
[PROOF STEP]
by (simp add: eval_\<pi>)
[PROOF STATE]
proof (state)
this:
primes_pi 2 = 1

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
 2. \<not> 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
from False assms
[PROOF STATE]
proof (chain)
picking this:
\<not> 1 < n
0 < n
n < primorial x
[PROOF STEP]
have [simp]: "n = 1"
[PROOF STATE]
proof (prove)
using this:
\<not> 1 < n
0 < n
n < primorial x

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

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
 2. \<not> 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
n < primorial x
[PROOF STEP]
have "\<not>(x < 2)"
[PROOF STATE]
proof (prove)
using this:
0 < n
n < primorial x

goal (1 subgoal):
 1. \<not> x < 2
[PROOF STEP]
by (intro notI) (auto simp: primorial_conv_primorial')
[PROOF STATE]
proof (state)
this:
\<not> x < 2

goal (2 subgoals):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
 2. \<not> 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> x < 2

goal (1 subgoal):
 1. primes_omega n < primes_omega (primorial x)
[PROOF STEP]
using assms \<pi>_mono[of 2 x]
[PROOF STATE]
proof (prove)
using this:
\<not> x < 2
0 < n
n < primorial x
2 \<le> x \<Longrightarrow> primes_pi 2 \<le> primes_pi x

goal (1 subgoal):
 1. primes_omega n < primes_omega (primorial x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
primes_omega n < primes_omega (primorial x)

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
define m where "m = primes_omega n"
[PROOF STATE]
proof (state)
this:
m = primes_omega n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
have le: "primorial' m \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' m \<le> n
[PROOF STEP]
using primorial'_primes_omega_le[of n] \<open>n > 1\<close>
[PROOF STATE]
proof (prove)
using this:
0 < n \<Longrightarrow> primorial' (primes_omega n) \<le> n
1 < n

goal (1 subgoal):
 1. primorial' m \<le> n
[PROOF STEP]
by (simp add: m_def primes_omega_def)
[PROOF STATE]
proof (state)
this:
primorial' m \<le> n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
primorial' m \<le> n

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
have "\<dots> < primorial x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < primorial x
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
n < primorial x

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
n < primorial x

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
have "\<dots> = primorial' (nat \<lfloor>primes_pi x\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial x = primorial' (nat \<lfloor>primes_pi x\<rfloor>)
[PROOF STEP]
by (simp add: primorial_conv_primorial')
[PROOF STATE]
proof (state)
this:
primorial x = primorial' (nat \<lfloor>primes_pi x\<rfloor>)

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
primorial' m < primorial' (nat \<lfloor>primes_pi x\<rfloor>)
[PROOF STEP]
have "m < nat \<lfloor>primes_pi x\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
primorial' m < primorial' (nat \<lfloor>primes_pi x\<rfloor>)

goal (1 subgoal):
 1. m < nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
using strict_mono_less[OF strict_mono_primorial']
[PROOF STATE]
proof (prove)
using this:
primorial' m < primorial' (nat \<lfloor>primes_pi x\<rfloor>)
(primorial' ?x < primorial' ?y) = (?x < ?y)

goal (1 subgoal):
 1. m < nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m < nat \<lfloor>primes_pi x\<rfloor>

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
hence "m < primes_pi x"
[PROOF STATE]
proof (prove)
using this:
m < nat \<lfloor>primes_pi x\<rfloor>

goal (1 subgoal):
 1. real m < primes_pi x
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
real m < primes_pi x

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real m < primes_pi x

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
have "\<dots> = primes_omega (primorial x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_pi x = real (primes_omega (primorial x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
primes_pi x = real (primes_omega (primorial x))

goal (1 subgoal):
 1. 1 < n \<Longrightarrow> primes_omega n < primes_omega (primorial x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real m < real (primes_omega (primorial x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real m < real (primes_omega (primorial x))

goal (1 subgoal):
 1. primes_omega n < primes_omega (primorial x)
[PROOF STEP]
unfolding m_def of_nat_less_iff
[PROOF STATE]
proof (prove)
using this:
primes_omega n < primes_omega (primorial x)

goal (1 subgoal):
 1. primes_omega n < primes_omega (primorial x)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
primes_omega n < primes_omega (primorial x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primes_omega_le_primes_omega_primorial:
  fixes n :: nat
  assumes "n \<le> primorial x"
  shows   "primes_omega n \<le> primes_omega (primorial x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_omega n \<le> primes_omega (primorial x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primes_omega n \<le> primes_omega (primorial x)
[PROOF STEP]
consider "n = 0" | "n > 0" "n = primorial x" | "n > 0" "n \<noteq> primorial x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n = 0 \<Longrightarrow> thesis; \<lbrakk>0 < n; n = primorial x\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>0 < n; n \<noteq> primorial x\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; \<lbrakk>0 < n; n = primorial x\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < n; n \<noteq> primorial x\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. primes_omega n \<le> primes_omega (primorial x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>n = 0 \<Longrightarrow> ?thesis; \<lbrakk>0 < n; n = primorial x\<rbrakk> \<Longrightarrow> ?thesis; \<lbrakk>0 < n; n \<noteq> primorial x\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. primes_omega n \<le> primes_omega (primorial x)
[PROOF STEP]
by cases (use primes_omega_less_primes_omega_primorial[of n x] assms in auto)
[PROOF STATE]
proof (state)
this:
primes_omega n \<le> primes_omega (primorial x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_0_components:
  shows "dg_0\<lparr>Obj\<rparr> = 0"
    and "dg_0\<lparr>Arr\<rparr> = 0"
    and "dg_0\<lparr>Dom\<rparr> = 0"
    and "dg_0\<lparr>Cod\<rparr> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dg_0\<lparr>Obj\<rparr> = []\<^sub>\<circ> &&& dg_0\<lparr>Arr\<rparr> = []\<^sub>\<circ>) &&& dg_0\<lparr>Dom\<rparr> = []\<^sub>\<circ> &&& dg_0\<lparr>Cod\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
unfolding dg_0_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>) &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in \<Z>) digraph_dg_0[dg_cs_intros]: "digraph \<alpha> dg_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> dg_0
[PROOF STEP]
proof(intro digraphI)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence dg_0
 3. vsv (dg_0\<lparr>Dom\<rparr>)
 4. vsv (dg_0\<lparr>Cod\<rparr>)
 5. vcard dg_0 = 4\<^sub>\<nat>
 6. \<D>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) = dg_0\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) = dg_0\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 10. dg_0\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence dg_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence dg_0
[PROOF STEP]
unfolding dg_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence dg_0

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_0\<lparr>Dom\<rparr>)
 3. vsv (dg_0\<lparr>Cod\<rparr>)
 4. vcard dg_0 = 4\<^sub>\<nat>
 5. \<D>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) = dg_0\<lparr>Arr\<rparr>
 6. \<R>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 7. \<D>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) = dg_0\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 9. dg_0\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 10. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom dg_0 a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vcard dg_0 = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard dg_0 = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dg_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard dg_0 = 4\<^sub>\<nat>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_0\<lparr>Dom\<rparr>)
 3. vsv (dg_0\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) = dg_0\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_0\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) = dg_0\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_0\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>
 8. dg_0\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 9. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom dg_0 a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
qed (auto simp: dg_0_components)


[STATEMENT]
lemma op_dg_dg_0[dg_op_simps]: "op_dg (dg_0) = dg_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dg dg_0 = dg_0
[PROOF STEP]
proof(rule dg_eqI, unfold dg_op_simps)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. digraph ?\<alpha> (op_dg dg_0)
 2. digraph ?\<alpha> dg_0
 3. dg_0\<lparr>Obj\<rparr> = dg_0\<lparr>Obj\<rparr>
 4. dg_0\<lparr>Arr\<rparr> = dg_0\<lparr>Arr\<rparr>
 5. dg_0\<lparr>Cod\<rparr> = dg_0\<lparr>Dom\<rparr>
 6. dg_0\<lparr>Dom\<rparr> = dg_0\<lparr>Cod\<rparr>
[PROOF STEP]
define \<beta> where "\<beta> = \<omega> + \<omega>"
[PROOF STATE]
proof (state)
this:
\<beta> = \<omega> + \<omega>

goal (6 subgoals):
 1. digraph ?\<alpha> (op_dg dg_0)
 2. digraph ?\<alpha> dg_0
 3. dg_0\<lparr>Obj\<rparr> = dg_0\<lparr>Obj\<rparr>
 4. dg_0\<lparr>Arr\<rparr> = dg_0\<lparr>Arr\<rparr>
 5. dg_0\<lparr>Cod\<rparr> = dg_0\<lparr>Dom\<rparr>
 6. dg_0\<lparr>Dom\<rparr> = dg_0\<lparr>Cod\<rparr>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
unfolding \<beta>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> (\<omega> + \<omega>)
[PROOF STEP]
by (rule \<Z>_\<omega>\<omega>)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. digraph ?\<alpha> (op_dg dg_0)
 2. digraph ?\<alpha> dg_0
 3. dg_0\<lparr>Obj\<rparr> = dg_0\<lparr>Obj\<rparr>
 4. dg_0\<lparr>Arr\<rparr> = dg_0\<lparr>Arr\<rparr>
 5. dg_0\<lparr>Cod\<rparr> = dg_0\<lparr>Dom\<rparr>
 6. dg_0\<lparr>Dom\<rparr> = dg_0\<lparr>Cod\<rparr>
[PROOF STEP]
show "digraph \<beta> (op_dg dg_0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<beta> (op_dg dg_0)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros dg_op_intros)
[PROOF STATE]
proof (state)
this:
digraph \<beta> (op_dg dg_0)

goal (5 subgoals):
 1. digraph (\<omega> + \<omega>) dg_0
 2. dg_0\<lparr>Obj\<rparr> = dg_0\<lparr>Obj\<rparr>
 3. dg_0\<lparr>Arr\<rparr> = dg_0\<lparr>Arr\<rparr>
 4. dg_0\<lparr>Cod\<rparr> = dg_0\<lparr>Dom\<rparr>
 5. dg_0\<lparr>Dom\<rparr> = dg_0\<lparr>Cod\<rparr>
[PROOF STEP]
show "digraph \<beta> dg_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<beta> dg_0
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
digraph \<beta> dg_0

goal (4 subgoals):
 1. dg_0\<lparr>Obj\<rparr> = dg_0\<lparr>Obj\<rparr>
 2. dg_0\<lparr>Arr\<rparr> = dg_0\<lparr>Arr\<rparr>
 3. dg_0\<lparr>Cod\<rparr> = dg_0\<lparr>Dom\<rparr>
 4. dg_0\<lparr>Dom\<rparr> = dg_0\<lparr>Cod\<rparr>
[PROOF STEP]
qed (simp_all add: dg_0_components op_dg_components)


[STATEMENT]
lemma dg_0_is_arr_iff[simp]: "\<FF> : \<AA> \<mapsto>\<^bsub>dg_0\<^esub> \<BB> \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>dg_0\<^esub> \<BB> = False
[PROOF STEP]
by (rule iffI; (elim is_arrE)?) (auto simp: dg_0_components)


[STATEMENT]
lemma (in digraph) dg_dg_0_if_Obj_0:
  assumes "\<CC>\<lparr>Obj\<rparr> = 0"
  shows "\<CC> = dg_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<CC> = dg_0
[PROOF STEP]
by (rule dg_eqI[of \<alpha>])
    (
      auto simp:
        dg_cs_intros
        assms
        digraph_dg_0
        dg_0_components
        dg_Arr_vempty_if_Obj_vempty
        dg_Cod_vempty_if_Arr_vempty
        dg_Dom_vempty_if_Arr_vempty
    )


[STATEMENT]
lemma dghm_0_components:
  shows "dghm_0 \<AA>\<lparr>ObjMap\<rparr> = 0"
    and "dghm_0 \<AA>\<lparr>ArrMap\<rparr> = 0"
    and "dghm_0 \<AA>\<lparr>HomDom\<rparr> = dg_0"
    and "dghm_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_0 \<AA>\<lparr>ObjMap\<rparr> = []\<^sub>\<circ> &&& dghm_0 \<AA>\<lparr>ArrMap\<rparr> = []\<^sub>\<circ>) &&& dghm_0 \<AA>\<lparr>HomDom\<rparr> = dg_0 &&& dghm_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
[PROOF STEP]
unfolding dghm_0_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>) &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = dg_0 &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<AA>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma op_dghm_dghm_0: "op_dghm (dghm_0 \<CC>) = dghm_0 (op_dg \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (dghm_0 \<CC>) = dghm_0 (op_dg \<CC>)
[PROOF STEP]
unfolding
    dghm_0_def op_dg_def op_dghm_def dg_0_def dghm_field_simps dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma dghm_0_ObjMap_vsv[dg_cs_intros]: "vsv (dghm_0 \<CC>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dghm_0 \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding dghm_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_0_ArrMap_vsv[dg_cs_intros]: "vsv (dghm_0 \<CC>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dghm_0 \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding dghm_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in \<Z>) dghm_0_is_ft_dghm:
  assumes "digraph \<alpha> \<AA>"
  shows "dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule is_ft_dghmI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 2. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (dghm_0 \<AA>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom dg_0 a b)
[PROOF STEP]
show "dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule is_dghmI)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dghm_0 \<AA>)
 3. digraph \<alpha> dg_0
 4. digraph \<alpha> \<AA>
 5. vcard (dghm_0 \<AA>) = 4\<^sub>\<nat>
 6. dghm_0 \<AA>\<lparr>HomDom\<rparr> = dg_0
 7. dghm_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 8. vsv (dghm_0 \<AA>\<lparr>ObjMap\<rparr>)
 9. vsv (dghm_0 \<AA>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ObjMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (dghm_0 \<AA>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dghm_0 \<AA>)
[PROOF STEP]
unfolding dghm_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dghm_0 \<AA>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> dg_0
 3. digraph \<alpha> \<AA>
 4. vcard (dghm_0 \<AA>) = 4\<^sub>\<nat>
 5. dghm_0 \<AA>\<lparr>HomDom\<rparr> = dg_0
 6. dghm_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 7. vsv (dghm_0 \<AA>\<lparr>ObjMap\<rparr>)
 8. vsv (dghm_0 \<AA>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ObjMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (dghm_0 \<AA>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dghm_0 \<AA>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [[]\<^sub>\<circ>, []\<^sub>\<circ>, dg_0, \<AA>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dghm_0 \<AA>) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> dg_0
 3. digraph \<alpha> \<AA>
 4. dghm_0 \<AA>\<lparr>HomDom\<rparr> = dg_0
 5. dghm_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 6. vsv (dghm_0 \<AA>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_0 \<AA>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ObjMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (dghm_0 \<AA>\<lparr>ArrMap\<rparr>) = dg_0\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
qed (auto simp: assms digraph_dg_0 dghm_0_components dg_0_components)
[PROOF STATE]
proof (state)
this:
dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>; b \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>\<rbrakk> \<Longrightarrow> v11 (dghm_0 \<AA>\<lparr>ArrMap\<rparr> \<restriction>\<^sup>l\<^sub>\<circ> Hom dg_0 a b)
[PROOF STEP]
qed (auto simp: dg_0_components dghm_0_components)


[STATEMENT]
lemma (in \<Z>) dghm_0_is_ft_dghm'[dghm_cs_intros]:
  assumes "digraph \<alpha> \<AA>"
    and "\<BB>' = \<AA>"
    and "\<AA>' = dg_0"
  shows "dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>

goal (1 subgoal):
 1. dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>

goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule dghm_0_is_ft_dghm)


[STATEMENT]
lemma (in \<Z>) dghm_0_is_dghm:
  assumes "digraph \<alpha> \<AA>"
  shows "dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
using dghm_0_is_ft_dghm[OF assms]
[PROOF STATE]
proof (prove)
using this:
dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in \<Z>) dghm_0_is_dghm'[dg_cs_intros]:
  assumes "digraph \<alpha> \<AA>"
    and "\<BB>' = \<AA>"
    and "\<AA>' = dg_0"
  shows "dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>

goal (1 subgoal):
 1. dghm_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>

goal (1 subgoal):
 1. dghm_0 \<AA> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule dghm_0_is_dghm)


[STATEMENT]
lemma is_dghm_is_dghm_0_if_dg_0:
  assumes "\<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<FF> = dghm_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = dghm_0 \<CC>
[PROOF STEP]
proof(rule dghm_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 4. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
interpret \<FF>: is_dghm \<alpha> dg_0 \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. dghm_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\

 3. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 4. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "\<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
\<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. dghm_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 3. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 4. dg_0 = ?\<CC>
 5. \<CC> = ?\

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = 0" "\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
using this:
\<FF> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ> &&& \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps dg_0_components)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>

goal (5 subgoals):
 1. dghm_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\

 2. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 3. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 4. dg_0 = ?\<CC>
 5. \<CC> = ?\

[PROOF STEP]
show "dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (4 subgoals):
 1. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 2. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 3. dg_0 = dg_0
 4. \<CC> = \<CC>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ObjMap\<rparr>) = 0" "\<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ArrMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
using this:
dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ> &&& \<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps dg_0_components)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (dghm_0 \<CC>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>

goal (4 subgoals):
 1. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
 2. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 3. dg_0 = dg_0
 4. \<CC> = \<CC>
[PROOF STEP]
show "\<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ObjMap\<rparr> = dghm_0 \<CC>\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
 2. dg_0 = dg_0
 3. \<CC> = \<CC>
[PROOF STEP]
show "\<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr> = dghm_0 \<CC>\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. dg_0 = dg_0
 2. \<CC> = \<CC>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma tdghm_0_components:
  shows "tdghm_0 \<CC>\<lparr>NTMap\<rparr> = 0"
    and [dg_cs_simps]: "tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>"
    and [dg_cs_simps]: "tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC>"
    and [dg_cs_simps]: "tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0"
    and [dg_cs_simps]: "tdghm_0  \<CC>\<lparr>NTDGCod\<rparr> = \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (tdghm_0 \<CC>\<lparr>NTMap\<rparr> = []\<^sub>\<circ> &&& tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>) &&& tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC> &&& tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0 &&& tdghm_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
unfolding tdghm_0_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = dghm_0 \<CC>) &&& [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = dghm_0 \<CC> &&& [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = dg_0 &&& [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<CC>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma op_tdghm_tdghm_0: "op_tdghm (tdghm_0 \<CC>) = tdghm_0 (op_dg \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm (tdghm_0 \<CC>) = tdghm_0 (op_dg \<CC>)
[PROOF STEP]
by
    (
      simp_all add:
        tdghm_0_def op_tdghm_def op_dg_def dg_0_def op_dghm_dghm_0
        nt_field_simps dg_field_simps nat_omega_simps
    )


[STATEMENT]
lemma tdghm_0_NTMap_vsv[dg_cs_intros]: "vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)
[PROOF STEP]
unfolding tdghm_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma tdghm_0_NTMap_vdomain[dg_cs_simps]: "\<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
unfolding tdghm_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma tdghm_0_NTMap_vrange[dg_cs_simps]: "\<R>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
unfolding tdghm_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in digraph) dg_tdghm_0_is_tdghmI:
  "tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_tdghmI)
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (tdghm_0 \<CC>)
 3. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 5. vcard (tdghm_0 \<CC>) = 5\<^sub>\<nat>
 6. vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)
 7. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 8. tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>
 9. tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC>
 10. tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0
A total of 12 subgoals...
[PROOF STEP]
show "vfsequence (tdghm_0 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (tdghm_0 \<CC>)
[PROOF STEP]
unfolding tdghm_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (tdghm_0 \<CC>)

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. vcard (tdghm_0 \<CC>) = 5\<^sub>\<nat>
 5. vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)
 6. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 7. tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>
 8. tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC>
 9. tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0
 10. tdghm_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
A total of 11 subgoals...
[PROOF STEP]
show "vcard (tdghm_0 \<CC>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (tdghm_0 \<CC>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding tdghm_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [[]\<^sub>\<circ>, dghm_0 \<CC>, dghm_0 \<CC>, dg_0, \<CC>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (tdghm_0 \<CC>) = 5\<^sub>\<nat>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)
 5. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 6. tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>
 7. tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC>
 8. tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0
 9. tdghm_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
 10. \<And>a. a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr> \<Longrightarrow> tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    if "a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding dg_0_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> []\<^sub>\<circ>

goal (1 subgoal):
 1. tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> dg_0\<lparr>Obj\<rparr> \<Longrightarrow> tdghm_0 \<CC>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> dghm_0 \<CC>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. vsv (tdghm_0 \<CC>\<lparr>NTMap\<rparr>)
 5. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = dg_0\<lparr>Obj\<rparr>
 6. tdghm_0 \<CC>\<lparr>NTDom\<rparr> = dghm_0 \<CC>
 7. tdghm_0 \<CC>\<lparr>NTCod\<rparr> = dghm_0 \<CC>
 8. tdghm_0 \<CC>\<lparr>NTDGDom\<rparr> = dg_0
 9. tdghm_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
qed
  (
    cs_concl cs_shallow
      cs_simp: dg_cs_simps dg_0_components(1) cs_intro: dg_cs_intros
  )+


[STATEMENT]
lemma (in digraph) dg_tdghm_0_is_tdghmI'[dg_cs_intros]:
  assumes "\<FF>' = dghm_0 \<CC>"
    and "\<GG>' = dghm_0 \<CC>"
    and "\<AA>' = dg_0"
    and "\<BB>' = \<CC>"
    and "\<FF>' = \<FF>"
    and "\<GG>' = \<GG>"
  shows "tdghm_0 \<CC> : \<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tdghm_0 \<CC> : \<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule dg_tdghm_0_is_tdghmI)


[STATEMENT]
lemma is_tdghm_is_tdghm_0_if_dg_0:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<NN> = tdghm_0 \<CC>" and "\<FF> = dghm_0 \<CC>" and "\<GG> = dghm_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = tdghm_0 \<CC> &&& \<FF> = dghm_0 \<CC> &&& \<GG> = dghm_0 \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<NN> = tdghm_0 \<CC>
 2. \<FF> = dghm_0 \<CC>
 3. \<GG> = dghm_0 \<CC>
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> dg_0 \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<NN> = tdghm_0 \<CC>
 2. \<FF> = dghm_0 \<CC>
 3. \<GG> = dghm_0 \<CC>
[PROOF STEP]
show \<FF>_def: "\<FF> = dghm_0 \<CC>" and \<GG>_def: "\<GG> = dghm_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = dghm_0 \<CC> &&& \<GG> = dghm_0 \<CC>
[PROOF STEP]
by (auto intro: is_dghm_is_dghm_0_if_dg_0 dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> = dghm_0 \<CC>
\<GG> = dghm_0 \<CC>

goal (1 subgoal):
 1. \<NN> = tdghm_0 \<CC>
[PROOF STEP]
show "\<NN> = tdghm_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = tdghm_0 \<CC>
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. tdghm_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (6 subgoals):
 1. tdghm_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
 3. \<FF> = ?\<FF>'
 4. \<GG> = ?\<GG>'
 5. dg_0 = ?\<AA>'
 6. \<CC> = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps dg_0_components(1))
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>

goal (6 subgoals):
 1. tdghm_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
 3. \<FF> = ?\<FF>'
 4. \<GG> = ?\<GG>'
 5. dg_0 = ?\<AA>'
 6. \<CC> = ?\<BB>'
[PROOF STEP]
show "tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
 2. \<FF> = dghm_0 \<CC>
 3. \<GG> = dghm_0 \<CC>
 4. dg_0 = dg_0
 5. \<CC> = \<CC>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
using this:
tdghm_0 \<CC> : dghm_0 \<CC> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_0 \<CC> : dg_0 \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps dg_0_components(1))
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (tdghm_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>

goal (5 subgoals):
 1. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
 2. \<FF> = dghm_0 \<CC>
 3. \<GG> = dghm_0 \<CC>
 4. dg_0 = dg_0
 5. \<CC> = \<CC>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold dom_lhs dom_rhs) (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr> = tdghm_0 \<CC>\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<FF> = dghm_0 \<CC>
 2. \<GG> = dghm_0 \<CC>
 3. dg_0 = dg_0
 4. \<CC> = \<CC>
[PROOF STEP]
qed (auto simp: \<FF>_def \<GG>_def)
[PROOF STATE]
proof (state)
this:
\<NN> = tdghm_0 \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dg_10_components:
  shows "dg_10 \<aa>\<lparr>Obj\<rparr> = set {\<aa>}"
    and "dg_10 \<aa>\<lparr>Arr\<rparr> = 0"
    and "dg_10 \<aa>\<lparr>Dom\<rparr> = 0"
    and "dg_10 \<aa>\<lparr>Cod\<rparr> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dg_10 \<aa>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {\<aa>} &&& dg_10 \<aa>\<lparr>Arr\<rparr> = []\<^sub>\<circ>) &&& dg_10 \<aa>\<lparr>Dom\<rparr> = []\<^sub>\<circ> &&& dg_10 \<aa>\<lparr>Cod\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
unfolding dg_10_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = ZFC_in_HOL.set {\<aa>} &&& [ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>) &&& [ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = []\<^sub>\<circ> &&& [ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma (in \<Z>) digraph_dg_10:
  assumes "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "digraph \<alpha> (dg_10 \<aa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (dg_10 \<aa>)
[PROOF STEP]
proof(intro digraphI)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dg_10 \<aa>)
 3. vsv (dg_10 \<aa>\<lparr>Dom\<rparr>)
 4. vsv (dg_10 \<aa>\<lparr>Cod\<rparr>)
 5. vcard (dg_10 \<aa>) = 4\<^sub>\<nat>
 6. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 10. dg_10 \<aa>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence (dg_10 \<aa>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dg_10 \<aa>)
[PROOF STEP]
unfolding dg_10_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence (dg_10 \<aa>)

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_10 \<aa>\<lparr>Dom\<rparr>)
 3. vsv (dg_10 \<aa>\<lparr>Cod\<rparr>)
 4. vcard (dg_10 \<aa>) = 4\<^sub>\<nat>
 5. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 6. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 7. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 9. dg_10 \<aa>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 10. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vcard (dg_10 \<aa>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dg_10 \<aa>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dg_10_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [ZFC_in_HOL.set {\<aa>}, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dg_10 \<aa>) = 4\<^sub>\<nat>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_10 \<aa>\<lparr>Dom\<rparr>)
 3. vsv (dg_10 \<aa>\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 8. dg_10 \<aa>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 9. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>a'\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b'\<in>\<^sub>\<circ>B. Hom (dg_10 \<aa>) a' b') \<in>\<^sub>\<circ> Vset \<alpha>" for A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>a'\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b'\<in>\<^sub>\<circ>B. Hom (dg_10 \<aa>) a' b') \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>
[PROOF STEP]
unfolding dg_10_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>
dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>
dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using vempty_is_zet vsubset_in_VsetI
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Arr\<rparr>
dg_10 \<aa>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> []\<^sub>\<circ>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?a \<subseteq>\<^sub>\<circ> ?A; ?A \<in>\<^sub>\<circ> Vset ?i\<rbrakk> \<Longrightarrow> ?a \<in>\<^sub>\<circ> Vset ?i

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>?A. \<Union>\<^sub>\<circ> (VLambda ?B (Hom (dg_10 \<aa>) a) `\<^sub>\<circ> ?B)) `\<^sub>\<circ> ?A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_10 \<aa>\<lparr>Dom\<rparr>)
 3. vsv (dg_10 \<aa>\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) = dg_10 \<aa>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_10 \<aa>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_10 \<aa>\<lparr>Obj\<rparr>
 8. dg_10 \<aa>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
qed (auto simp: assms dg_10_components vsubset_vsingleton_leftI)


[STATEMENT]
lemma dg_10_is_arr_iff: "\<FF> : \<AA> \<mapsto>\<^bsub>dg_10 \<aa>\<^esub> \<BB> \<longleftrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<^bsub>dg_10 \<aa>\<^esub> \<BB> = False
[PROOF STEP]
unfolding is_arr_def dg_10_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<in>\<^sub>\<circ> []\<^sub>\<circ> \<and> []\<^sub>\<circ>\<lparr>\<FF>\<rparr> = \<AA> \<and> []\<^sub>\<circ>\<lparr>\<FF>\<rparr> = \<BB>) = False
[PROOF STEP]
by simp


[STATEMENT]
lemma dg_1_components:
  shows "dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> = set {\<aa>}"
    and "dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> = set {\<ff>}"
    and "dg_1 \<aa> \<ff>\<lparr>Dom\<rparr> = set {\<langle>\<ff>, \<aa>\<rangle>}"
    and "dg_1 \<aa> \<ff>\<lparr>Cod\<rparr> = set {\<langle>\<ff>, \<aa>\<rangle>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {\<aa>} &&& dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {\<ff>}) &&& dg_1 \<aa> \<ff>\<lparr>Dom\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>} &&& dg_1 \<aa> \<ff>\<lparr>Cod\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}
[PROOF STEP]
unfolding dg_1_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = ZFC_in_HOL.set {\<aa>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<ff>}) &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma (in \<Z>) digraph_dg_1:
  assumes "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>" and "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "digraph \<alpha> (dg_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> (dg_1 \<aa> \<ff>)
[PROOF STEP]
proof(intro digraphI)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dg_1 \<aa> \<ff>)
 3. vsv (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>)
 4. vsv (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>)
 5. vcard (dg_1 \<aa> \<ff>) = 4\<^sub>\<nat>
 6. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 9. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 10. dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence (dg_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dg_1 \<aa> \<ff>)
[PROOF STEP]
unfolding dg_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence (dg_1 \<aa> \<ff>)

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>)
 3. vsv (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>)
 4. vcard (dg_1 \<aa> \<ff>) = 4\<^sub>\<nat>
 5. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 6. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 7. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 8. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 9. dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 10. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "vcard (dg_1 \<aa> \<ff>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dg_1 \<aa> \<ff>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dg_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dg_1 \<aa> \<ff>) = 4\<^sub>\<nat>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>)
 3. vsv (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 8. dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 9. \<And>A B. \<lbrakk>A \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>; B \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>; A \<in>\<^sub>\<circ> Vset \<alpha>; B \<in>\<^sub>\<circ> Vset \<alpha>\<rbrakk> \<Longrightarrow> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "(\<Union>\<^sub>\<circ>a'\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b'\<in>\<^sub>\<circ>B. Hom (dg_1 \<aa> \<ff>) a' b') \<in>\<^sub>\<circ> Vset \<alpha>" for A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "(\<Union>\<^sub>\<circ>a'\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ>b'\<in>\<^sub>\<circ>B. Hom (dg_1 \<aa> \<ff>) a' b') \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> set {\<ff>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
unfolding dg_1_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<ff>} \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. ZFC_in_HOL.set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Limit_vsingleton_in_VsetI)
[PROOF STATE]
proof (state)
this:
ZFC_in_HOL.set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
ZFC_in_HOL.set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
dg_1 \<aa> \<ff>\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
ZFC_in_HOL.set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding dg_1_components
[PROOF STATE]
proof (prove)
using this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
ZFC_in_HOL.set {\<ff>} \<subseteq>\<^sub>\<circ> ZFC_in_HOL.set {\<ff>}
ZFC_in_HOL.set {\<ff>} \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (auto simp: vsubset_in_VsetI)
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>A. \<Union>\<^sub>\<circ> (VLambda B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> B)) `\<^sub>\<circ> A) \<in>\<^sub>\<circ> Vset \<alpha>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>?A. \<Union>\<^sub>\<circ> (VLambda ?B (Hom (dg_1 \<aa> \<ff>) a) `\<^sub>\<circ> ?B)) `\<^sub>\<circ> ?A) \<in>\<^sub>\<circ> Vset \<alpha>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vsv (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>)
 3. vsv (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>)
 4. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 5. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Dom\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 6. \<D>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) = dg_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 7. \<R>\<^sub>\<circ> (dg_1 \<aa> \<ff>\<lparr>Cod\<rparr>) \<subseteq>\<^sub>\<circ> dg_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 8. dg_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
qed (auto simp: assms dg_1_components vsubset_vsingleton_leftI)


[STATEMENT]
lemma dg_1_is_arrI:
  assumes "a = \<aa>" and "b = \<aa>" and "f = \<ff>"
  shows "f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a = \<aa>
b = \<aa>
f = \<ff>

goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b
[PROOF STEP]
by (intro is_arrI) (auto simp: dg_1_components)


[STATEMENT]
lemma dg_1_is_arrD:
  assumes "f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b"
  shows "a = \<aa>" and "b = \<aa>" and "f = \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = \<aa> &&& b = \<aa> &&& f = \<ff>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b

goal (1 subgoal):
 1. a = \<aa> &&& b = \<aa> &&& f = \<ff>
[PROOF STEP]
by (all\<open>elim is_arrE\<close>) (auto simp: dg_1_components)


[STATEMENT]
lemma dg_1_is_arrE:
  assumes "f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b"
  obtains "a = \<aa>" and "b = \<aa>" and "f = \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a = \<aa>; b = \<aa>; f = \<ff>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b

goal (1 subgoal):
 1. (\<lbrakk>a = \<aa>; b = \<aa>; f = \<ff>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim is_arrE) (force simp: dg_1_components)


[STATEMENT]
lemma dg_1_is_arr_iff: "f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b \<longleftrightarrow> (a = \<aa> \<and> b = \<aa> \<and> f = \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f : a \<mapsto>\<^bsub>dg_1 \<aa> \<ff>\<^esub> b = (a = \<aa> \<and> b = \<aa> \<and> f = \<ff>)
[PROOF STEP]
by (rule iffI; (elim is_arrE)?)
    (auto simp: dg_1_components intro: dg_1_is_arrI)


[STATEMENT]
lemma conv_invol: "x \<rhd> 1 \<rhd> 1 = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<rhd> (1::'a) \<rhd> (1::'a) = x
[PROOF STEP]
by (metis local.conv1 local.jonsson1b local.mult_onel)


[STATEMENT]
lemma conv_add: "x \<squnion> y \<rhd> 1 = (x \<rhd> 1) \<squnion> (y \<rhd> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<squnion> y \<rhd> (1::'a) = (x \<rhd> (1::'a)) \<squnion> (y \<rhd> (1::'a))
[PROOF STEP]
by (metis local.conjr2_sup)


[STATEMENT]
lemma conv_contrav: "x\<cdot>y \<rhd> 1 = (y \<rhd> 1)\<cdot>(x \<rhd> 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> y \<rhd> (1::'a) = (y \<rhd> (1::'a)) \<cdot> (x \<rhd> (1::'a))
[PROOF STEP]
by (metis local.conv1 local.conv2 local.jonsson1b local.jonsson2c)


[STATEMENT]
lemma conv_res: "(x \<rhd> 1)\<cdot>- (x\<cdot>y) \<le> - y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<rhd> (1::'a)) \<cdot> - (x \<cdot> y) \<le> - y
[PROOF STEP]
by (metis local.comp_anti local.conjugate_r_def local.conv1 local.double_compl local.res_rc1)


[STATEMENT]
lemma conv_invol': "1 \<lhd> (1 \<lhd> x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<lhd> ((1::'a) \<lhd> x) = x
[PROOF STEP]
by (metis local.conv_invol local.jonsson3c)


[STATEMENT]
lemma conv_add': "1 \<lhd> (x \<squnion> y) = (1 \<lhd> x) \<squnion> (1 \<lhd> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<lhd> x \<squnion> y = ((1::'a) \<lhd> x) \<squnion> ((1::'a) \<lhd> y)
[PROOF STEP]
by (metis local.conjl1_sup)


[STATEMENT]
lemma conv_contrav': "1 \<lhd> x\<cdot>y = (1 \<lhd> y)\<cdot>(1 \<lhd> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) \<lhd> x \<cdot> y = ((1::'a) \<lhd> y) \<cdot> ((1::'a) \<lhd> x)
[PROOF STEP]
by (metis local.conv_contrav local.conv_invol local.jonsson3c)


[STATEMENT]
lemma conv_res': "(1 \<lhd> x)\<cdot>- (x\<cdot>y) \<le> - y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((1::'a) \<lhd> x) \<cdot> - (x \<cdot> y) \<le> - y
[PROOF STEP]
by (metis conv_res local.conv_invol local.jonsson3c)


[STATEMENT]
lemma card_subset_ex:
  assumes "finite A" "n \<le> card A"
  shows "\<exists>B \<subseteq> A. card B = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
n \<le> card A

goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = n
[PROOF STEP]
proof (induction A arbitrary: n rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. n \<le> card {} \<Longrightarrow> \<exists>B\<subseteq>{}. card B = n
 2. \<And>x F n. \<lbrakk>finite F; x \<notin> F; \<And>n. n \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = n; n \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = n
[PROOF STEP]
case (insert x A)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
?n \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?n
n \<le> card (insert x A)

goal (2 subgoals):
 1. \<And>n. n \<le> card {} \<Longrightarrow> \<exists>B\<subseteq>{}. card B = n
 2. \<And>x F n. \<lbrakk>finite F; x \<notin> F; \<And>n. n \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = n; n \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
proof (cases n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
 2. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
using card.empty
[PROOF STATE]
proof (prove)
using this:
n = 0
card {} = 0

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = n

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
n = Suc k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc k
[PROOF STEP]
have "\<exists>B \<subseteq> A. card B = k"
[PROOF STATE]
proof (prove)
using this:
n = Suc k

goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = k
[PROOF STEP]
using insert
[PROOF STATE]
proof (prove)
using this:
n = Suc k
finite A
x \<notin> A
?n \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?n
n \<le> card (insert x A)

goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>A. card B = k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>B\<subseteq>A. card B = k
[PROOF STEP]
obtain B where "B \<subseteq> A" "card B = k"
[PROOF STATE]
proof (prove)
using this:
\<exists>B\<subseteq>A. card B = k

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; card B = k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<subseteq> A
card B = k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
B \<subseteq> A
card B = k

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> A
card B = k
[PROOF STEP]
have "finite B"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
card B = k

goal (1 subgoal):
 1. finite B
[PROOF STEP]
using insert.hyps finite_subset
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
card B = k
finite A
x \<notin> A
\<lbrakk>?A \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite ?A

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

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
B \<subseteq> A
card B = k
finite B
[PROOF STEP]
have "card (insert x B) = n"
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
card B = k
finite B

goal (1 subgoal):
 1. card (insert x B) = n
[PROOF STEP]
using Suc insert.hyps card_insert_disjoint
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
card B = k
finite B
n = Suc k
finite A
x \<notin> A
\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk> \<Longrightarrow> card (insert ?x ?A) = Suc (card ?A)

goal (1 subgoal):
 1. card (insert x B) = n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
card (insert x B) = n

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
card (insert x B) = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
card (insert x B) = n

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
using \<open>B \<subseteq> A\<close>
[PROOF STATE]
proof (prove)
using this:
card (insert x B) = n
B \<subseteq> A

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = n

goal (1 subgoal):
 1. \<And>n. n \<le> card {} \<Longrightarrow> \<exists>B\<subseteq>{}. card B = n
[PROOF STEP]
qed auto


[STATEMENT]
lemma augment:
  assumes "indep X" "indep Y" "card Y < card X"
  shows "\<exists>x \<in> X - Y. indep (insert x Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
obtain X' where "X' \<subseteq> X" "card X' = Suc (card Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X' \<subseteq> X; card X' = Suc (card Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms card_subset_ex[of X "Suc (card Y)"] indep_finite
[PROOF STATE]
proof (prove)
using this:
indep X
indep Y
card Y < card X
\<lbrakk>finite X; Suc (card Y) \<le> card X\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>X. card B = Suc (card Y)
indep ?A \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. (\<And>X'. \<lbrakk>X' \<subseteq> X; card X' = Suc (card Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X' \<subseteq> X
card X' = Suc (card Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X' \<subseteq> X
card X' = Suc (card Y)
[PROOF STEP]
obtain x where "x \<in> X' - Y"  "indep (insert x Y)"
[PROOF STATE]
proof (prove)
using this:
X' \<subseteq> X
card X' = Suc (card Y)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X' - Y; indep (insert x Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms augment_aux[of X' Y] indep_subset
[PROOF STATE]
proof (prove)
using this:
X' \<subseteq> X
card X' = Suc (card Y)
indep X
indep Y
card Y < card X
\<lbrakk>indep X'; indep Y; card X' = Suc (card Y)\<rbrakk> \<Longrightarrow> \<exists>x\<in>X' - Y. indep (insert x Y)
\<lbrakk>indep ?X; ?Y \<subseteq> ?X\<rbrakk> \<Longrightarrow> indep ?Y

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> X' - Y; indep (insert x Y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> X' - Y
indep (insert x Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X' - Y
indep (insert x Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> X' - Y
indep (insert x Y)

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
using \<open>X' \<subseteq> X\<close>
[PROOF STATE]
proof (prove)
using this:
x \<in> X' - Y
indep (insert x Y)
X' \<subseteq> X

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>X - Y. indep (insert x Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma augment_psubset:
  assumes "indep X" "indep Y" "Y \<subset> X"
  shows "\<exists>x \<in> X - Y. indep (insert x Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
using assms augment psubset_card_mono indep_finite
[PROOF STATE]
proof (prove)
using this:
indep X
indep Y
Y \<subset> X
\<lbrakk>indep ?X; indep ?Y; card ?Y < card ?X\<rbrakk> \<Longrightarrow> \<exists>x\<in>?X - ?Y. indep (insert x ?Y)
\<lbrakk>finite ?B; ?A \<subset> ?B\<rbrakk> \<Longrightarrow> card ?A < card ?B
indep ?A \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. \<exists>x\<in>X - Y. indep (insert x Y)
[PROOF STEP]
by blast