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 = idc Ω 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 = idc Ω 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 = idc Ω 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 = idc Ω 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 idc c)) c zero = 𝗍"
proof -
  have  "(EXISTS c c (eq_pred c c nth_even ×f idc c)) c zero
      = EXISTS c c (eq_pred c c nth_even ×f idc c) c zero"
    by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = EXISTS c c (eq_pred c c (nth_even ×f idc c) c (idc 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 idc c)) c zero = 𝖿"
proof -
  have  "(EXISTS c c (eq_pred c c nth_odd ×f idc c)) c zero = EXISTS c c (eq_pred c c nth_odd ×f idc c) c zero"
    by (typecheck_cfuncs, simp add: comp_associative2)
  also have "... = EXISTS c c (eq_pred c c (nth_odd ×f idc c) c (idc 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 β⇘cc 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 = idc 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 "... = idc 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 "idc c c successor = successor c idc 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 = idc (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 = idc (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 = idc (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 = idc (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 β⇘cc 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 β⇘cc 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 β⇘cc 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 β⇘cc 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 β⇘cc 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 β⇘cc 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