Theory Nat_Parity
section ‹Natural Number Parity and Halving›
theory Nat_Parity
imports Nats Quant_Logic
begin
subsection ‹Nth Even Number›
definition nth_even :: "cfunc" where
"nth_even = (THE u. u: ℕ⇩c → ℕ⇩c ∧
u ∘⇩c zero = zero ∧
(successor ∘⇩c successor) ∘⇩c u = u ∘⇩c successor)"
lemma nth_even_def2:
"nth_even: ℕ⇩c → ℕ⇩c ∧ nth_even ∘⇩c zero = zero ∧ (successor ∘⇩c successor) ∘⇩c nth_even = nth_even ∘⇩c successor"
unfolding nth_even_def by (rule theI', etcs_rule natural_number_object_property2)
lemma nth_even_type[type_rule]:
"nth_even: ℕ⇩c → ℕ⇩c"
by (simp add: nth_even_def2)
lemma nth_even_zero:
"nth_even ∘⇩c zero = zero"
by (simp add: nth_even_def2)
lemma nth_even_successor:
"nth_even ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c nth_even"
by (simp add: nth_even_def2)
lemma nth_even_successor2:
"nth_even ∘⇩c successor = successor ∘⇩c successor ∘⇩c nth_even"
using comp_associative2 nth_even_def2 by (typecheck_cfuncs, auto)
subsection ‹Nth Odd Number›
definition nth_odd :: "cfunc" where
"nth_odd = (THE u. u: ℕ⇩c → ℕ⇩c ∧
u ∘⇩c zero = successor ∘⇩c zero ∧
(successor ∘⇩c successor) ∘⇩c u = u ∘⇩c successor)"
lemma nth_odd_def2:
"nth_odd: ℕ⇩c → ℕ⇩c ∧ nth_odd ∘⇩c zero = successor ∘⇩c zero ∧ (successor ∘⇩c successor) ∘⇩c nth_odd = nth_odd ∘⇩c successor"
unfolding nth_odd_def by (rule theI', etcs_rule natural_number_object_property2)
lemma nth_odd_type[type_rule]:
"nth_odd: ℕ⇩c → ℕ⇩c"
by (simp add: nth_odd_def2)
lemma nth_odd_zero:
"nth_odd ∘⇩c zero = successor ∘⇩c zero"
by (simp add: nth_odd_def2)
lemma nth_odd_successor:
"nth_odd ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c nth_odd"
by (simp add: nth_odd_def2)
lemma nth_odd_successor2:
"nth_odd ∘⇩c successor = successor ∘⇩c successor ∘⇩c nth_odd"
using comp_associative2 nth_odd_def2 by (typecheck_cfuncs, auto)
lemma nth_odd_is_succ_nth_even:
"nth_odd = successor ∘⇩c nth_even"
proof (etcs_rule natural_number_object_func_unique[where X="ℕ⇩c", where f="successor ∘⇩c successor"])
show "nth_odd ∘⇩c zero = (successor ∘⇩c nth_even) ∘⇩c zero"
proof -
have "nth_odd ∘⇩c zero = successor ∘⇩c zero"
by (simp add: nth_odd_zero)
also have "... = (successor ∘⇩c nth_even) ∘⇩c zero"
using comp_associative2 nth_even_def2 successor_type zero_type by fastforce
finally show ?thesis.
qed
show "nth_odd ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c nth_odd"
by (simp add: nth_odd_successor)
show "(successor ∘⇩c nth_even) ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c successor ∘⇩c nth_even"
proof -
have "(successor ∘⇩c nth_even) ∘⇩c successor = successor ∘⇩c nth_even ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = successor ∘⇩c successor ∘⇩c successor ∘⇩c nth_even"
by (simp add: nth_even_successor2)
also have "... = (successor ∘⇩c successor) ∘⇩c successor ∘⇩c nth_even"
by (typecheck_cfuncs, simp add: comp_associative2)
finally show ?thesis.
qed
qed
lemma succ_nth_odd_is_nth_even_succ:
"successor ∘⇩c nth_odd = nth_even ∘⇩c successor"
proof (etcs_rule natural_number_object_func_unique[where f="successor ∘⇩c successor"])
show "(successor ∘⇩c nth_odd) ∘⇩c zero = (nth_even ∘⇩c successor) ∘⇩c zero"
by (simp add: nth_even_successor2 nth_odd_is_succ_nth_even)
show "(successor ∘⇩c nth_odd) ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c successor ∘⇩c nth_odd"
by (metis cfunc_type_def codomain_comp comp_associative nth_odd_def2 successor_type)
then show "(nth_even ∘⇩c successor) ∘⇩c successor = (successor ∘⇩c successor) ∘⇩c nth_even ∘⇩c successor"
using nth_even_successor2 nth_odd_is_succ_nth_even by auto
qed
subsection ‹Checking if a Number is Even›
definition is_even :: "cfunc" where
"is_even = (THE u. u: ℕ⇩c → Ω ∧ u ∘⇩c zero = 𝗍 ∧ NOT ∘⇩c u = u ∘⇩c successor)"
lemma is_even_def2:
"is_even : ℕ⇩c → Ω ∧ is_even ∘⇩c zero = 𝗍 ∧ NOT ∘⇩c is_even = is_even ∘⇩c successor"
unfolding is_even_def by (rule theI', etcs_rule natural_number_object_property2)
lemma is_even_type[type_rule]:
"is_even : ℕ⇩c → Ω"
by (simp add: is_even_def2)
lemma is_even_zero:
"is_even ∘⇩c zero = 𝗍"
by (simp add: is_even_def2)
lemma is_even_successor:
"is_even ∘⇩c successor = NOT ∘⇩c is_even"
by (simp add: is_even_def2)
subsection ‹Checking if a Number is Odd›
definition is_odd :: "cfunc" where
"is_odd = (THE u. u: ℕ⇩c → Ω ∧ u ∘⇩c zero = 𝖿 ∧ NOT ∘⇩c u = u ∘⇩c successor)"
lemma is_odd_def2:
"is_odd : ℕ⇩c → Ω ∧ is_odd ∘⇩c zero = 𝖿 ∧ NOT ∘⇩c is_odd = is_odd ∘⇩c successor"
unfolding is_odd_def by (rule theI', etcs_rule natural_number_object_property2)
lemma is_odd_type[type_rule]:
"is_odd : ℕ⇩c → Ω"
by (simp add: is_odd_def2)
lemma is_odd_zero:
"is_odd ∘⇩c zero = 𝖿"
by (simp add: is_odd_def2)
lemma is_odd_successor:
"is_odd ∘⇩c successor = NOT ∘⇩c is_odd"
by (simp add: is_odd_def2)
lemma is_even_not_is_odd:
"is_even = NOT ∘⇩c is_odd"
proof (typecheck_cfuncs, rule natural_number_object_func_unique[where f="NOT", where X="Ω"], clarify)
show "is_even ∘⇩c zero = (NOT ∘⇩c is_odd) ∘⇩c zero"
by (typecheck_cfuncs, metis NOT_false_is_true cfunc_type_def comp_associative is_even_def2 is_odd_def2)
show "is_even ∘⇩c successor = NOT ∘⇩c is_even"
by (simp add: is_even_successor)
show "(NOT ∘⇩c is_odd) ∘⇩c successor = NOT ∘⇩c NOT ∘⇩c is_odd"
by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative is_odd_def2)
qed
lemma is_odd_not_is_even:
"is_odd = NOT ∘⇩c is_even"
proof (typecheck_cfuncs, rule natural_number_object_func_unique[where f="NOT", where X="Ω"], clarify)
show "is_odd ∘⇩c zero = (NOT ∘⇩c is_even) ∘⇩c zero"
by (typecheck_cfuncs, metis NOT_true_is_false cfunc_type_def comp_associative is_even_def2 is_odd_def2)
show "is_odd ∘⇩c successor = NOT ∘⇩c is_odd"
by (simp add: is_odd_successor)
show "(NOT ∘⇩c is_even) ∘⇩c successor = NOT ∘⇩c NOT ∘⇩c is_even"
by (typecheck_cfuncs, simp add: cfunc_type_def comp_associative is_even_def2)
qed
lemma not_even_and_odd:
assumes "m ∈⇩c ℕ⇩c"
shows "¬(is_even ∘⇩c m = 𝗍 ∧ is_odd ∘⇩c m = 𝗍)"
using assms NOT_true_is_false NOT_type comp_associative2 is_even_not_is_odd true_false_distinct by (typecheck_cfuncs, fastforce)
lemma even_or_odd:
assumes "n ∈⇩c ℕ⇩c"
shows "is_even ∘⇩c n = 𝗍 ∨ is_odd ∘⇩c n = 𝗍"
by (typecheck_cfuncs, metis NOT_false_is_true NOT_type comp_associative2 is_even_not_is_odd true_false_only_truth_values assms)
lemma is_even_nth_even_true:
"is_even ∘⇩c nth_even = 𝗍 ∘⇩c β⇘ℕ⇩c⇙"
proof (etcs_rule natural_number_object_func_unique[where f="id Ω", where X=Ω])
show "(is_even ∘⇩c nth_even) ∘⇩c zero = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
proof -
have "(is_even ∘⇩c nth_even) ∘⇩c zero = is_even ∘⇩c nth_even ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = 𝗍"
by (simp add: is_even_zero nth_even_zero)
also have "... = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
by (typecheck_cfuncs, metis comp_associative2 id_right_unit2 terminal_func_comp_elem)
finally show ?thesis.
qed
show "(is_even ∘⇩c nth_even) ∘⇩c successor = id⇩c Ω ∘⇩c is_even ∘⇩c nth_even"
proof -
have "(is_even ∘⇩c nth_even) ∘⇩c successor = is_even ∘⇩c nth_even ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = is_even ∘⇩c successor ∘⇩c successor ∘⇩c nth_even"
by (simp add: nth_even_successor2)
also have "... = ((is_even ∘⇩c successor) ∘⇩c successor) ∘⇩c nth_even"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = is_even ∘⇩c nth_even"
using is_even_def2 is_even_not_is_odd is_odd_def2 is_odd_not_is_even by (typecheck_cfuncs, auto)
also have "... = id Ω ∘⇩c is_even ∘⇩c nth_even"
by (typecheck_cfuncs, simp add: id_left_unit2)
finally show ?thesis.
qed
show "(𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor = id⇩c Ω ∘⇩c 𝗍 ∘⇩c β⇘ℕ⇩c⇙"
by (typecheck_cfuncs, smt comp_associative2 id_left_unit2 terminal_func_comp)
qed
lemma is_odd_nth_odd_true:
"is_odd ∘⇩c nth_odd = 𝗍 ∘⇩c β⇘ℕ⇩c⇙"
proof (etcs_rule natural_number_object_func_unique[where f="id Ω", where X=Ω])
show "(is_odd ∘⇩c nth_odd) ∘⇩c zero = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
proof -
have "(is_odd ∘⇩c nth_odd) ∘⇩c zero = is_odd ∘⇩c nth_odd ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = 𝗍"
using comp_associative2 is_even_not_is_odd is_even_zero is_odd_def2 nth_odd_def2 successor_type zero_type by auto
also have "... = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
by (typecheck_cfuncs, metis comp_associative2 is_even_nth_even_true is_even_type is_even_zero nth_even_def2)
finally show ?thesis.
qed
show "(is_odd ∘⇩c nth_odd) ∘⇩c successor = id⇩c Ω ∘⇩c is_odd ∘⇩c nth_odd"
proof -
have "(is_odd ∘⇩c nth_odd) ∘⇩c successor = is_odd ∘⇩c nth_odd ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = is_odd ∘⇩c successor ∘⇩c successor ∘⇩c nth_odd"
by (simp add: nth_odd_successor2)
also have "... = ((is_odd ∘⇩c successor) ∘⇩c successor) ∘⇩c nth_odd"
by (typecheck_cfuncs, smt comp_associative2)
also have "... = is_odd ∘⇩c nth_odd"
using is_even_def2 is_even_not_is_odd is_odd_def2 is_odd_not_is_even by (typecheck_cfuncs, auto)
also have "... = id Ω ∘⇩c is_odd ∘⇩c nth_odd"
by (typecheck_cfuncs, simp add: id_left_unit2)
finally show ?thesis.
qed
show "(𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor = id⇩c Ω ∘⇩c 𝗍 ∘⇩c β⇘ℕ⇩c⇙"
by (typecheck_cfuncs, smt comp_associative2 id_left_unit2 terminal_func_comp)
qed
lemma is_odd_nth_even_false:
"is_odd ∘⇩c nth_even = 𝖿 ∘⇩c β⇘ℕ⇩c⇙"
by (smt NOT_true_is_false NOT_type comp_associative2 is_even_def2 is_even_nth_even_true
is_odd_not_is_even nth_even_def2 terminal_func_type true_func_type)
lemma is_even_nth_odd_false:
"is_even ∘⇩c nth_odd = 𝖿 ∘⇩c β⇘ℕ⇩c⇙"
by (smt NOT_true_is_false NOT_type comp_associative2 is_odd_def2 is_odd_nth_odd_true
is_even_not_is_odd nth_odd_def2 terminal_func_type true_func_type)
lemma EXISTS_zero_nth_even:
"(EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_even ×⇩f id⇩c ℕ⇩c)⇧♯) ∘⇩c zero = 𝗍"
proof -
have "(EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_even ×⇩f id⇩c ℕ⇩c)⇧♯) ∘⇩c zero
= EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_even ×⇩f id⇩c ℕ⇩c)⇧♯ ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c (nth_even ×⇩f id⇩c ℕ⇩c) ∘⇩c (id⇩c ℕ⇩c ×⇩f zero))⇧♯"
by (typecheck_cfuncs, simp add: comp_associative2 sharp_comp)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c (nth_even ×⇩f zero))⇧♯"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c ⟨nth_even ∘⇩c left_cart_proj ℕ⇩c 𝟭, zero ∘⇩c β⇘ℕ⇩c ×⇩c 𝟭⇙⟩ )⇧♯"
by (typecheck_cfuncs, metis cfunc_cross_prod_def cfunc_type_def right_cart_proj_type terminal_func_unique)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c ⟨nth_even ∘⇩c left_cart_proj ℕ⇩c 𝟭, (zero ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_cart_proj ℕ⇩c 𝟭⟩ )⇧♯"
by (typecheck_cfuncs, smt comp_associative2 terminal_func_comp)
also have "... = EXISTS ℕ⇩c ∘⇩c ((eq_pred ℕ⇩c ∘⇩c ⟨nth_even, zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c left_cart_proj ℕ⇩c 𝟭)⇧♯"
by (typecheck_cfuncs, smt cfunc_prod_comp comp_associative2)
also have "... = 𝗍"
proof (rule exists_true_implies_EXISTS_true)
show "eq_pred ℕ⇩c ∘⇩c ⟨nth_even,zero ∘⇩c β⇘ℕ⇩c⇙⟩ : ℕ⇩c → Ω"
by typecheck_cfuncs
show "∃x. x ∈⇩c ℕ⇩c ∧ (eq_pred ℕ⇩c ∘⇩c ⟨nth_even,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c x = 𝗍"
proof (typecheck_cfuncs, intro exI[where x="zero"], clarify)
have "(eq_pred ℕ⇩c ∘⇩c ⟨nth_even,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c zero
= eq_pred ℕ⇩c ∘⇩c ⟨nth_even,zero ∘⇩c β⇘ℕ⇩c⇙⟩ ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = eq_pred ℕ⇩c ∘⇩c ⟨nth_even ∘⇩c zero, zero⟩"
by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 id_right_unit2 terminal_func_comp_elem)
also have "... = 𝗍"
using eq_pred_iff_eq nth_even_zero by (typecheck_cfuncs, blast)
finally show "(eq_pred ℕ⇩c ∘⇩c ⟨nth_even,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c zero = 𝗍".
qed
qed
finally show ?thesis.
qed
lemma not_EXISTS_zero_nth_odd:
"(EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_odd ×⇩f id⇩c ℕ⇩c)⇧♯) ∘⇩c zero = 𝖿"
proof -
have "(EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_odd ×⇩f id⇩c ℕ⇩c)⇧♯) ∘⇩c zero = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c nth_odd ×⇩f id⇩c ℕ⇩c)⇧♯ ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c (nth_odd ×⇩f id⇩c ℕ⇩c) ∘⇩c (id⇩c ℕ⇩c ×⇩f zero))⇧♯"
by (typecheck_cfuncs, simp add: comp_associative2 sharp_comp)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c (nth_odd ×⇩f zero))⇧♯"
by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_cross_prod id_left_unit2 id_right_unit2)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c ⟨nth_odd ∘⇩c left_cart_proj ℕ⇩c 𝟭, zero ∘⇩c β⇘ℕ⇩c ×⇩c 𝟭⇙⟩ )⇧♯"
by (typecheck_cfuncs, metis cfunc_cross_prod_def cfunc_type_def right_cart_proj_type terminal_func_unique)
also have "... = EXISTS ℕ⇩c ∘⇩c (eq_pred ℕ⇩c ∘⇩c ⟨nth_odd ∘⇩c left_cart_proj ℕ⇩c 𝟭, (zero ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_cart_proj ℕ⇩c 𝟭⟩ )⇧♯"
by (typecheck_cfuncs, smt comp_associative2 terminal_func_comp)
also have "... = EXISTS ℕ⇩c ∘⇩c ((eq_pred ℕ⇩c ∘⇩c ⟨nth_odd, zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c left_cart_proj ℕ⇩c 𝟭)⇧♯"
by (typecheck_cfuncs, smt cfunc_prod_comp comp_associative2)
also have "... = 𝖿"
proof -
have "∄ x. x ∈⇩c ℕ⇩c ∧ (eq_pred ℕ⇩c ∘⇩c ⟨nth_odd, zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c x = 𝗍"
proof clarify
fix x
assume x_type[type_rule]: "x ∈⇩c ℕ⇩c"
assume "(eq_pred ℕ⇩c ∘⇩c ⟨nth_odd,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c x = 𝗍"
then have "eq_pred ℕ⇩c ∘⇩c ⟨nth_odd, zero ∘⇩c β⇘ℕ⇩c⇙⟩ ∘⇩c x = 𝗍"
by (typecheck_cfuncs, simp add: comp_associative2)
then have "eq_pred ℕ⇩c ∘⇩c ⟨nth_odd ∘⇩c x, zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c x⟩ = 𝗍"
by (typecheck_cfuncs_prems, auto simp add: cfunc_prod_comp comp_associative2)
then have "eq_pred ℕ⇩c ∘⇩c ⟨nth_odd ∘⇩c x, zero⟩ = 𝗍"
by (typecheck_cfuncs_prems, metis cfunc_type_def id_right_unit id_type one_unique_element)
then have "nth_odd ∘⇩c x = zero"
using eq_pred_iff_eq by (typecheck_cfuncs_prems, blast)
then show False
by (typecheck_cfuncs_prems, smt comp_associative2 comp_type nth_even_def2 nth_odd_is_succ_nth_even successor_type zero_is_not_successor)
qed
then have "EXISTS ℕ⇩c ∘⇩c ((eq_pred ℕ⇩c ∘⇩c ⟨nth_odd,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c left_cart_proj ℕ⇩c 𝟭)⇧♯ ≠ 𝗍"
using EXISTS_true_implies_exists_true by (typecheck_cfuncs, blast)
then show "EXISTS ℕ⇩c ∘⇩c ((eq_pred ℕ⇩c ∘⇩c ⟨nth_odd,zero ∘⇩c β⇘ℕ⇩c⇙⟩) ∘⇩c left_cart_proj ℕ⇩c 𝟭)⇧♯ = 𝖿"
using true_false_only_truth_values by (typecheck_cfuncs, blast)
qed
finally show ?thesis.
qed
subsection ‹Natural Number Halving›
definition halve_with_parity :: "cfunc" where
"halve_with_parity = (THE u. u: ℕ⇩c → ℕ⇩c ∐ ℕ⇩c ∧
u ∘⇩c zero = left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero ∧
(right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c u = u ∘⇩c successor)"
lemma halve_with_parity_def2:
"halve_with_parity : ℕ⇩c → ℕ⇩c ∐ ℕ⇩c ∧
halve_with_parity ∘⇩c zero = left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero ∧
(right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity = halve_with_parity ∘⇩c successor"
unfolding halve_with_parity_def by (rule theI', etcs_rule natural_number_object_property2)
lemma halve_with_parity_type[type_rule]:
"halve_with_parity : ℕ⇩c → ℕ⇩c ∐ ℕ⇩c"
by (simp add: halve_with_parity_def2)
lemma halve_with_parity_zero:
"halve_with_parity ∘⇩c zero = left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (simp add: halve_with_parity_def2)
lemma halve_with_parity_successor:
"(right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity = halve_with_parity ∘⇩c successor"
by (simp add: halve_with_parity_def2)
lemma halve_with_parity_nth_even:
"halve_with_parity ∘⇩c nth_even = left_coproj ℕ⇩c ℕ⇩c"
proof (etcs_rule natural_number_object_func_unique[where X="ℕ⇩c ∐ ℕ⇩c", where f="(left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)"])
show "(halve_with_parity ∘⇩c nth_even) ∘⇩c zero = left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
proof -
have "(halve_with_parity ∘⇩c nth_even) ∘⇩c zero = halve_with_parity ∘⇩c nth_even ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = halve_with_parity ∘⇩c zero"
by (simp add: nth_even_zero)
also have "... = left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (simp add: halve_with_parity_zero)
finally show ?thesis.
qed
show "(halve_with_parity ∘⇩c nth_even) ∘⇩c successor =
((left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity ∘⇩c nth_even"
proof -
have "(halve_with_parity ∘⇩c nth_even) ∘⇩c successor = halve_with_parity ∘⇩c nth_even ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = halve_with_parity ∘⇩c (successor ∘⇩c successor) ∘⇩c nth_even"
by (simp add: nth_even_successor)
also have "... = ((halve_with_parity ∘⇩c successor) ∘⇩c successor) ∘⇩c nth_even"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (((right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity) ∘⇩c successor) ∘⇩c nth_even"
by (simp add: halve_with_parity_def2)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c (halve_with_parity ∘⇩c successor) ∘⇩c nth_even"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c ((right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity) ∘⇩c nth_even"
by (simp add: halve_with_parity_def2)
also have "... = ((right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)))
∘⇩c halve_with_parity ∘⇩c nth_even"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ((left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c halve_with_parity ∘⇩c nth_even"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2 left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
finally show ?thesis.
qed
show "left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor =
(left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c left_coproj ℕ⇩c ℕ⇩c"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
qed
lemma halve_with_parity_nth_odd:
"halve_with_parity ∘⇩c nth_odd = right_coproj ℕ⇩c ℕ⇩c"
proof (etcs_rule natural_number_object_func_unique[where X="ℕ⇩c ∐ ℕ⇩c", where f="(left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)"])
show "(halve_with_parity ∘⇩c nth_odd) ∘⇩c zero = right_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
proof -
have "(halve_with_parity ∘⇩c nth_odd) ∘⇩c zero = halve_with_parity ∘⇩c nth_odd ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = halve_with_parity ∘⇩c successor ∘⇩c zero"
by (simp add: nth_odd_def2)
also have "... = (halve_with_parity ∘⇩c successor) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity) ∘⇩c zero"
by (simp add: halve_with_parity_def2)
also have "... = right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (simp add: halve_with_parity_def2)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c left_coproj ℕ⇩c ℕ⇩c) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = right_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
finally show ?thesis.
qed
show "(halve_with_parity ∘⇩c nth_odd) ∘⇩c successor =
(left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity ∘⇩c nth_odd"
proof -
have "(halve_with_parity ∘⇩c nth_odd) ∘⇩c successor = halve_with_parity ∘⇩c nth_odd ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = halve_with_parity ∘⇩c (successor ∘⇩c successor) ∘⇩c nth_odd"
by (simp add: nth_odd_successor)
also have "... = ((halve_with_parity ∘⇩c successor) ∘⇩c successor) ∘⇩c nth_odd"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ((right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity)
∘⇩c successor) ∘⇩c nth_odd"
by (simp add: halve_with_parity_successor)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)
∘⇩c (halve_with_parity ∘⇩c successor)) ∘⇩c nth_odd"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)
∘⇩c (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity)) ∘⇩c nth_odd"
by (simp add: halve_with_parity_successor)
also have "... = (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)
∘⇩c right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity ∘⇩c nth_odd"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ((left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity ∘⇩c nth_odd"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2 left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
finally show ?thesis.
qed
show "right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor =
(left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ⨿ (right_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c right_coproj ℕ⇩c ℕ⇩c"
by (typecheck_cfuncs, simp add: right_coproj_cfunc_coprod)
qed
lemma nth_even_nth_odd_halve_with_parity:
"(nth_even ⨿ nth_odd) ∘⇩c halve_with_parity = id ℕ⇩c"
proof (etcs_rule natural_number_object_func_unique[where X="ℕ⇩c", where f="successor"])
show "(nth_even ⨿ nth_odd ∘⇩c halve_with_parity) ∘⇩c zero = id⇩c ℕ⇩c ∘⇩c zero"
proof -
have "(nth_even ⨿ nth_odd ∘⇩c halve_with_parity) ∘⇩c zero = nth_even ⨿ nth_odd ∘⇩c halve_with_parity ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = nth_even ⨿ nth_odd ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (simp add: halve_with_parity_zero)
also have "... = (nth_even ⨿ nth_odd ∘⇩c left_coproj ℕ⇩c ℕ⇩c) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = nth_even ∘⇩c zero"
by (typecheck_cfuncs, simp add: left_coproj_cfunc_coprod)
also have "... = id⇩c ℕ⇩c ∘⇩c zero"
using id_left_unit2 nth_even_def2 zero_type by auto
finally show ?thesis.
qed
show "(nth_even ⨿ nth_odd ∘⇩c halve_with_parity) ∘⇩c successor =
successor ∘⇩c nth_even ⨿ nth_odd ∘⇩c halve_with_parity"
proof -
have "(nth_even ⨿ nth_odd ∘⇩c halve_with_parity) ∘⇩c successor = nth_even ⨿ nth_odd ∘⇩c halve_with_parity ∘⇩c successor"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = nth_even ⨿ nth_odd ∘⇩c right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor) ∘⇩c halve_with_parity"
by (simp add: halve_with_parity_successor)
also have "... = (nth_even ⨿ nth_odd ∘⇩c right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = nth_odd ⨿ (nth_even ∘⇩c successor) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2 left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
also have "... = (successor ∘⇩c nth_even) ⨿ ((successor ∘⇩c successor) ∘⇩c nth_even) ∘⇩c halve_with_parity"
by (simp add: nth_even_successor nth_odd_is_succ_nth_even)
also have "... = (successor ∘⇩c nth_even) ⨿ (successor ∘⇩c successor ∘⇩c nth_even) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = (successor ∘⇩c nth_even) ⨿ (successor ∘⇩c nth_odd) ∘⇩c halve_with_parity"
by (simp add: nth_odd_is_succ_nth_even)
also have "... = successor ∘⇩c nth_even ⨿ nth_odd ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: cfunc_coprod_comp comp_associative2)
finally show ?thesis.
qed
show "id⇩c ℕ⇩c ∘⇩c successor = successor ∘⇩c id⇩c ℕ⇩c"
using id_left_unit2 id_right_unit2 successor_type by auto
qed
lemma halve_with_parity_nth_even_nth_odd:
"halve_with_parity ∘⇩c (nth_even ⨿ nth_odd) = id (ℕ⇩c ∐ ℕ⇩c)"
by (typecheck_cfuncs, smt cfunc_coprod_comp halve_with_parity_nth_even halve_with_parity_nth_odd id_coprod)
lemma even_odd_iso:
"isomorphism (nth_even ⨿ nth_odd)"
unfolding isomorphism_def
proof (intro exI[where x=halve_with_parity], safe)
show "domain halve_with_parity = codomain (nth_even ⨿ nth_odd)"
by (typecheck_cfuncs, unfold cfunc_type_def, auto)
show "codomain halve_with_parity = domain (nth_even ⨿ nth_odd)"
by (typecheck_cfuncs, unfold cfunc_type_def, auto)
show "halve_with_parity ∘⇩c nth_even ⨿ nth_odd = id⇩c (domain (nth_even ⨿ nth_odd))"
by (typecheck_cfuncs, unfold cfunc_type_def, auto simp add: halve_with_parity_nth_even_nth_odd)
show "nth_even ⨿ nth_odd ∘⇩c halve_with_parity = id⇩c (domain halve_with_parity)"
by (typecheck_cfuncs, unfold cfunc_type_def, auto simp add: nth_even_nth_odd_halve_with_parity)
qed
lemma halve_with_parity_iso:
"isomorphism halve_with_parity"
unfolding isomorphism_def
proof (intro exI[where x="nth_even ⨿ nth_odd"], safe)
show "domain (nth_even ⨿ nth_odd) = codomain halve_with_parity"
by (typecheck_cfuncs, unfold cfunc_type_def, auto)
show "codomain (nth_even ⨿ nth_odd) = domain halve_with_parity"
by (typecheck_cfuncs, unfold cfunc_type_def, auto)
show "nth_even ⨿ nth_odd ∘⇩c halve_with_parity = id⇩c (domain halve_with_parity)"
by (typecheck_cfuncs, unfold cfunc_type_def, auto simp add: nth_even_nth_odd_halve_with_parity)
show "halve_with_parity ∘⇩c nth_even ⨿ nth_odd = id⇩c (domain (nth_even ⨿ nth_odd))"
by (typecheck_cfuncs, unfold cfunc_type_def, auto simp add: halve_with_parity_nth_even_nth_odd)
qed
definition halve :: "cfunc" where
"halve = (id ℕ⇩c ⨿ id ℕ⇩c) ∘⇩c halve_with_parity"
lemma halve_type[type_rule]:
"halve : ℕ⇩c → ℕ⇩c"
unfolding halve_def by typecheck_cfuncs
lemma halve_nth_even:
"halve ∘⇩c nth_even = id ℕ⇩c"
unfolding halve_def by (typecheck_cfuncs, smt comp_associative2 halve_with_parity_nth_even left_coproj_cfunc_coprod)
lemma halve_nth_odd:
"halve ∘⇩c nth_odd = id ℕ⇩c"
unfolding halve_def by (typecheck_cfuncs, smt comp_associative2 halve_with_parity_nth_odd right_coproj_cfunc_coprod)
lemma is_even_def3:
"is_even = ((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙)) ∘⇩c halve_with_parity"
proof (etcs_rule natural_number_object_func_unique[where X=Ω, where f=NOT])
show "is_even ∘⇩c zero = ((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c zero"
proof -
have "((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c zero
= (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative halve_with_parity_zero)
also have "... = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
also have "... = 𝗍"
using comp_associative2 is_even_def2 is_even_nth_even_true nth_even_def2 by (typecheck_cfuncs, force)
also have "... = is_even ∘⇩c zero"
by (simp add: is_even_zero)
finally show ?thesis
by simp
qed
show "is_even ∘⇩c successor = NOT ∘⇩c is_even"
by (simp add: is_even_successor)
show "((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c successor =
NOT ∘⇩c (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity"
proof -
have "((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c successor
= (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2 halve_with_parity_successor)
also have "... =
(((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c right_coproj ℕ⇩c ℕ⇩c)
⨿
((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c halve_with_parity"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2)
also have "... = ((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
also have "... = ((NOT ∘⇩c 𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (NOT ∘⇩c 𝖿 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: NOT_false_is_true NOT_true_is_false comp_associative2)
also have "... = NOT ∘⇩c (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2 terminal_func_unique)
finally show ?thesis.
qed
qed
lemma is_odd_def3:
"is_odd = ((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙)) ∘⇩c halve_with_parity"
proof (etcs_rule natural_number_object_func_unique[where X=Ω, where f=NOT])
show "is_odd ∘⇩c zero = ((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c zero"
proof -
have "((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c zero
= (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c zero"
by (typecheck_cfuncs, metis cfunc_type_def comp_associative halve_with_parity_zero)
also have "... = (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod)
also have "... = 𝖿"
using comp_associative2 is_odd_nth_even_false is_odd_type is_odd_zero nth_even_def2 by (typecheck_cfuncs, force)
also have "... = is_odd ∘⇩c zero"
by (simp add: is_odd_def2)
finally show ?thesis
by simp
qed
show "is_odd ∘⇩c successor = NOT ∘⇩c is_odd"
by (simp add: is_odd_successor)
show "((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c successor =
NOT ∘⇩c (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity"
proof -
have "((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity) ∘⇩c successor
= (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c (right_coproj ℕ⇩c ℕ⇩c ⨿ (left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2 halve_with_parity_successor)
also have "... =
(((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c right_coproj ℕ⇩c ℕ⇩c)
⨿
((𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c left_coproj ℕ⇩c ℕ⇩c ∘⇩c successor))
∘⇩c halve_with_parity"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2)
also have "... = ((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝖿 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: comp_associative2 left_coproj_cfunc_coprod right_coproj_cfunc_coprod)
also have "... = ((NOT ∘⇩c 𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (NOT ∘⇩c 𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c successor)) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, simp add: NOT_false_is_true NOT_true_is_false comp_associative2)
also have "... = NOT ∘⇩c (𝖿 ∘⇩c β⇘ℕ⇩c⇙) ⨿ (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c halve_with_parity"
by (typecheck_cfuncs, smt cfunc_coprod_comp comp_associative2 terminal_func_unique)
finally show ?thesis.
qed
qed
lemma nth_even_or_nth_odd:
assumes "n ∈⇩c ℕ⇩c"
shows "(∃ m. m ∈⇩c ℕ⇩c ∧ nth_even ∘⇩c m = n) ∨ (∃ m. m ∈⇩c ℕ⇩c ∧ nth_odd ∘⇩c m = n)"
proof -
have "(∃m. m ∈⇩c ℕ⇩c ∧ halve_with_parity ∘⇩c n = left_coproj ℕ⇩c ℕ⇩c ∘⇩c m)
∨ (∃m. m ∈⇩c ℕ⇩c ∧ halve_with_parity ∘⇩c n = right_coproj ℕ⇩c ℕ⇩c ∘⇩c m)"
by (rule coprojs_jointly_surj, insert assms, typecheck_cfuncs)
then show ?thesis
proof
assume "∃m. m ∈⇩c ℕ⇩c ∧ halve_with_parity ∘⇩c n = left_coproj ℕ⇩c ℕ⇩c ∘⇩c m"
then obtain m where m_type: "m ∈⇩c ℕ⇩c" and m_def: "halve_with_parity ∘⇩c n = left_coproj ℕ⇩c ℕ⇩c ∘⇩c m"
by auto
then have "((nth_even ⨿ nth_odd) ∘⇩c halve_with_parity) ∘⇩c n = ((nth_even ⨿ nth_odd) ∘⇩c left_coproj ℕ⇩c ℕ⇩c) ∘⇩c m"
by (typecheck_cfuncs, smt assms comp_associative2)
then have "n = nth_even ∘⇩c m"
using assms by (typecheck_cfuncs_prems, smt comp_associative2 halve_with_parity_nth_even id_left_unit2 nth_even_nth_odd_halve_with_parity)
then have "∃m. m ∈⇩c ℕ⇩c ∧ nth_even ∘⇩c m = n"
using m_type by auto
then show ?thesis
by simp
next
assume "∃m. m ∈⇩c ℕ⇩c ∧ halve_with_parity ∘⇩c n = right_coproj ℕ⇩c ℕ⇩c ∘⇩c m"
then obtain m where m_type: "m ∈⇩c ℕ⇩c" and m_def: "halve_with_parity ∘⇩c n = right_coproj ℕ⇩c ℕ⇩c ∘⇩c m"
by auto
then have "((nth_even ⨿ nth_odd) ∘⇩c halve_with_parity) ∘⇩c n = ((nth_even ⨿ nth_odd) ∘⇩c right_coproj ℕ⇩c ℕ⇩c) ∘⇩c m"
by (typecheck_cfuncs, smt assms comp_associative2)
then have "n = nth_odd ∘⇩c m"
using assms by (typecheck_cfuncs_prems, smt comp_associative2 halve_with_parity_nth_odd id_left_unit2 nth_even_nth_odd_halve_with_parity)
then show ?thesis
using m_type by auto
qed
qed
lemma is_even_exists_nth_even:
assumes "is_even ∘⇩c n = 𝗍" and n_type[type_rule]: "n ∈⇩c ℕ⇩c"
shows "∃m. m ∈⇩c ℕ⇩c ∧ n = nth_even ∘⇩c m"
proof (rule ccontr)
assume "∄m. m ∈⇩c ℕ⇩c ∧ n = nth_even ∘⇩c m"
then obtain m where m_type[type_rule]: "m ∈⇩c ℕ⇩c" and n_def: "n = nth_odd ∘⇩c m"
using n_type nth_even_or_nth_odd by blast
then have "is_even ∘⇩c nth_odd ∘⇩c m = 𝗍"
using assms(1) by blast
then have "is_odd ∘⇩c nth_odd ∘⇩c m = 𝖿"
using NOT_true_is_false NOT_type comp_associative2 is_even_def2 is_odd_not_is_even n_def n_type by fastforce
then have "𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m = 𝖿"
by (typecheck_cfuncs_prems, smt comp_associative2 is_odd_nth_odd_true terminal_func_type true_func_type)
then have "𝗍 = 𝖿"
by (typecheck_cfuncs_prems, metis id_right_unit2 id_type one_unique_element)
then show False
using true_false_distinct by auto
qed
lemma is_odd_exists_nth_odd:
assumes "is_odd ∘⇩c n = 𝗍" and n_type[type_rule]: "n ∈⇩c ℕ⇩c"
shows "∃m. m ∈⇩c ℕ⇩c ∧ n = nth_odd ∘⇩c m"
proof (rule ccontr)
assume "∄m. m ∈⇩c ℕ⇩c ∧ n = nth_odd ∘⇩c m"
then obtain m where m_type[type_rule]: "m ∈⇩c ℕ⇩c" and n_def: "n = nth_even ∘⇩c m"
using n_type nth_even_or_nth_odd by blast
then have "is_odd ∘⇩c nth_even ∘⇩c m = 𝗍"
using assms(1) by blast
then have "is_even ∘⇩c nth_even ∘⇩c m = 𝖿"
using NOT_true_is_false NOT_type comp_associative2 is_even_not_is_odd is_odd_def2 n_def n_type by fastforce
then have "𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m = 𝖿"
by (typecheck_cfuncs_prems, smt comp_associative2 is_even_nth_even_true terminal_func_type true_func_type)
then have "𝗍 = 𝖿"
by (typecheck_cfuncs_prems, metis id_right_unit2 id_type one_unique_element)
then show False
using true_false_distinct by auto
qed
end