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 (z3) 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 (z3) 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