Theory Nats
section ‹Natural Number Object›
theory Nats
imports Exponential_Objects
begin
text ‹The axiomatization below corresponds to Axiom 10 (Natural Number Object) in Halvorson.›
axiomatization
natural_numbers :: "cset" ("ℕ⇩c") and
zero :: "cfunc" and
successor :: "cfunc"
where
zero_type[type_rule]: "zero ∈⇩c ℕ⇩c" and
successor_type[type_rule]: "successor: ℕ⇩c → ℕ⇩c" and
natural_number_object_property:
"q : 𝟭 → X ⟹ f: X → X ⟹
(∃!u. u: ℕ⇩c → X ∧
q = u ∘⇩c zero ∧
f ∘⇩c u = u ∘⇩c successor)"
lemma beta_N_succ_nEqs_Id1:
assumes n_type[type_rule]: "n ∈⇩c ℕ⇩c"
shows "β⇘ℕ⇩c⇙ ∘⇩c successor ∘⇩c n = id 𝟭"
by (typecheck_cfuncs, simp add: terminal_func_comp_elem)
lemma natural_number_object_property2:
assumes "q : 𝟭 → X" "f: X → X"
shows "∃!u. u: ℕ⇩c → X ∧ u ∘⇩c zero = q ∧ f ∘⇩c u = u ∘⇩c successor"
using assms natural_number_object_property[where q=q, where f=f, where X=X]
by metis
lemma natural_number_object_func_unique:
assumes u_type: "u : ℕ⇩c → X" and v_type: "v : ℕ⇩c → X" and f_type: "f: X → X"
assumes zeros_eq: "u ∘⇩c zero = v ∘⇩c zero"
assumes u_successor_eq: "u ∘⇩c successor = f ∘⇩c u"
assumes v_successor_eq: "v ∘⇩c successor = f ∘⇩c v"
shows "u = v"
by (smt (verit, best) comp_type f_type natural_number_object_property2 u_successor_eq u_type v_successor_eq v_type zero_type zeros_eq)
definition is_NNO :: "cset ⇒ cfunc ⇒ cfunc ⇒ bool" where
"is_NNO Y z s ⟷(z: 𝟭 → Y ∧ s: Y → Y ∧ (∀ X f q. ((q : 𝟭 → X) ∧ (f: X → X))⟶
(∃!u. u: Y → X ∧
q = u ∘⇩c z ∧
f ∘⇩c u = u ∘⇩c s)))"
lemma N_is_a_NNO:
"is_NNO ℕ⇩c zero successor"
by (simp add: is_NNO_def natural_number_object_property successor_type zero_type)
text ‹The lemma below corresponds to Exercise 2.6.5 in Halvorson.›
lemma NNOs_are_iso_N:
assumes "is_NNO N z s"
shows "N ≅ ℕ⇩c"
proof-
have z_type[type_rule]: "(z : 𝟭 → N)"
using assms is_NNO_def by blast
have s_type[type_rule]: "(s : N → N)"
using assms is_NNO_def by blast
then obtain u where u_type[type_rule]: "u: ℕ⇩c → N"
and u_triangle: "u ∘⇩c zero = z"
and u_square: "s ∘⇩c u = u ∘⇩c successor"
using natural_number_object_property z_type by blast
obtain v where v_type[type_rule]: "v: N → ℕ⇩c"
and v_triangle: "v ∘⇩c z = zero"
and v_square: "successor ∘⇩c v = v ∘⇩c s"
by (metis assms is_NNO_def successor_type zero_type)
then have vuzeroEqzero: "v ∘⇩c (u ∘⇩c zero) = zero"
by (simp add: u_triangle v_triangle)
have id_facts1: "id(ℕ⇩c): ℕ⇩c → ℕ⇩c∧ id(ℕ⇩c) ∘⇩c zero = zero ∧
(successor ∘⇩c id(ℕ⇩c) = id(ℕ⇩c) ∘⇩c successor)"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
then have vu_facts: "v ∘⇩c u: ℕ⇩c → ℕ⇩c∧ (v ∘⇩c u) ∘⇩c zero = zero ∧
successor ∘⇩c (v ∘⇩c u) = (v ∘⇩c u) ∘⇩c successor"
by (typecheck_cfuncs, smt (verit, best) comp_associative2 s_type u_square v_square vuzeroEqzero)
then have half_isomorphism: "(v ∘⇩c u) = id(ℕ⇩c)"
by (metis id_facts1 natural_number_object_property successor_type vu_facts zero_type)
have uvzEqz: "u ∘⇩c (v ∘⇩c z) = z"
by (simp add: u_triangle v_triangle)
have id_facts2: "id(N): N → N ∧ id(N) ∘⇩c z = z ∧ s ∘⇩c id(N) = id(N) ∘⇩c s"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
then have uv_facts: "u ∘⇩c v: N → N ∧
(u ∘⇩c v) ∘⇩c z = z ∧ s ∘⇩c (u ∘⇩c v) = (u ∘⇩c v) ∘⇩c s"
by (typecheck_cfuncs, smt (verit, best) comp_associative2 successor_type u_square uvzEqz v_square)
then have half_isomorphism2: "(u ∘⇩c v) = id(N)"
by (smt (verit, ccfv_threshold) assms id_facts2 is_NNO_def)
then show "N ≅ ℕ⇩c"
using cfunc_type_def half_isomorphism is_isomorphic_def isomorphism_def u_type v_type by fastforce
qed
text ‹The lemma below is the converse to Exercise 2.6.5 in Halvorson.›
lemma Iso_to_N_is_NNO:
assumes "N ≅ ℕ⇩c"
shows "∃ z s. is_NNO N z s"
proof -
obtain i where i_type[type_rule]: "i: ℕ⇩c → N" and i_iso: "isomorphism(i)"
using assms isomorphic_is_symmetric is_isomorphic_def by blast
obtain z where z_type[type_rule]: "z ∈⇩c N" and z_def: "z = i ∘⇩c zero"
by (typecheck_cfuncs, simp)
obtain s where s_type[type_rule]: "s: N → N" and s_def: "s = (i ∘⇩c successor) ∘⇩c i❙¯"
using i_iso by (typecheck_cfuncs, simp)
have "is_NNO N z s"
unfolding is_NNO_def
proof(typecheck_cfuncs)
fix X q f
assume q_type[type_rule]: "q: 𝟭 → X"
assume f_type[type_rule]: "f: X → X"
obtain u where u_type[type_rule]: "u: ℕ⇩c → X" and u_def: "u ∘⇩c zero = q ∧ f ∘⇩c u = u ∘⇩c successor"
using natural_number_object_property2 by (typecheck_cfuncs, blast)
obtain v where v_type[type_rule]: "v: N → X" and v_def: "v = u ∘⇩c i❙¯"
using i_iso by (typecheck_cfuncs, simp)
then have bottom_triangle: "v ∘⇩c z = q"
unfolding v_def u_def z_def using i_iso
by (typecheck_cfuncs, metis cfunc_type_def comp_associative id_right_unit2 inv_left u_def)
have bottom_square: "v ∘⇩c s = f ∘⇩c v"
unfolding v_def u_def s_def using i_iso
by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 id_right_unit2 inv_left u_def)
show "∃!u. u : N → X ∧ q = u ∘⇩c z ∧ f ∘⇩c u = u ∘⇩c s"
proof safe
show "∃u. u : N → X ∧ q = u ∘⇩c z ∧ f ∘⇩c u = u ∘⇩c s"
by (intro exI[where x=v], auto simp add: bottom_triangle bottom_square v_type)
next
fix w y
assume w_type[type_rule]: "w : N → X"
assume y_type[type_rule]: "y : N → X"
assume f_w: "f ∘⇩c w = w ∘⇩c s"
assume f_y: "f ∘⇩c y = y ∘⇩c s"
assume w_y_z: "w ∘⇩c z = y ∘⇩c z"
assume q_def: "q = w ∘⇩c z"
have "w ∘⇩c i = u"
proof (etcs_rule natural_number_object_func_unique[where f=f])
show "(w ∘⇩c i) ∘⇩c zero = u ∘⇩c zero"
using q_def u_def w_y_z z_def by (etcs_assocr, argo)
show "(w ∘⇩c i) ∘⇩c successor = f ∘⇩c w ∘⇩c i"
using i_iso by (typecheck_cfuncs, smt (verit, best) comp_associative2 comp_type f_w id_right_unit2 inv_left inverse_type s_def)
show "u ∘⇩c successor = f ∘⇩c u"
by (simp add: u_def)
qed
then have w_eq_v: "w = v"
unfolding v_def using i_iso
by (typecheck_cfuncs, smt (verit, best) comp_associative2 id_right_unit2 inv_right)
have "y ∘⇩c i = u"
proof (etcs_rule natural_number_object_func_unique[where f=f])
show "(y ∘⇩c i) ∘⇩c zero = u ∘⇩c zero"
using q_def u_def w_y_z z_def by (etcs_assocr, argo)
show "(y ∘⇩c i) ∘⇩c successor = f ∘⇩c y ∘⇩c i"
using i_iso by (typecheck_cfuncs, smt (verit, best) comp_associative2 comp_type f_y id_right_unit2 inv_left inverse_type s_def)
show "u ∘⇩c successor = f ∘⇩c u"
by (simp add: u_def)
qed
then have y_eq_v: "y = v"
unfolding v_def using i_iso
by (typecheck_cfuncs, smt (verit, best) comp_associative2 id_right_unit2 inv_right)
show "w = y"
using w_eq_v y_eq_v by auto
qed
qed
then show ?thesis
by auto
qed
subsection ‹Zero and Successor›
lemma zero_is_not_successor:
assumes "n ∈⇩c ℕ⇩c"
shows "zero ≠ successor ∘⇩c n"
proof (rule ccontr, clarify)
assume for_contradiction: "zero = successor ∘⇩c n"
have "∃!u. u: ℕ⇩c → Ω ∧ u ∘⇩c zero = 𝗍 ∧ (𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u = u ∘⇩c successor"
by (typecheck_cfuncs, rule natural_number_object_property2)
then obtain u where u_type: "u: ℕ⇩c → Ω" and
u_triangle: "u ∘⇩c zero = 𝗍" and
u_square: "(𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u = u ∘⇩c successor"
by auto
have "𝗍 = 𝖿"
proof -
have "𝗍 = u ∘⇩c zero"
by (simp add: u_triangle)
also have "... = u ∘⇩c successor ∘⇩c n"
by (simp add: for_contradiction)
also have "... = (𝖿 ∘⇩c β⇘Ω⇙) ∘⇩c u ∘⇩c n"
using assms u_type by (typecheck_cfuncs, simp add: comp_associative2 u_square)
also have "... = 𝖿"
using assms u_type by (etcs_assocr,typecheck_cfuncs, simp add: id_right_unit2 terminal_func_comp_elem)
finally show ?thesis.
qed
then show False
using true_false_distinct by blast
qed
text ‹The lemma below corresponds to Proposition 2.6.6 in Halvorson.›
lemma oneUN_iso_N_isomorphism:
"isomorphism(zero ⨿ successor)"
proof -
obtain i0 where i0_type[type_rule]: "i0: 𝟭 → (𝟭 ∐ ℕ⇩c)" and i0_def: "i0 = left_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, simp)
obtain i1 where i1_type[type_rule]: "i1: ℕ⇩c → (𝟭 ∐ ℕ⇩c)" and i1_def: "i1 = right_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, simp)
obtain g where g_type[type_rule]: "g: ℕ⇩c → (𝟭 ∐ ℕ⇩c)" and
g_triangle: " g ∘⇩c zero = i0" and
g_square: "g ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c g"
by (typecheck_cfuncs, metis natural_number_object_property)
then have second_diagram3: "g ∘⇩c (successor ∘⇩c zero) = (i1 ∘⇩c zero)"
by (typecheck_cfuncs, smt (verit, best) cfunc_coprod_type comp_associative2 comp_type i0_def left_coproj_cfunc_coprod)
then have g_s_s_Eqs_i1zUi1s_g_s:
"(g ∘⇩c successor) ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c (g ∘⇩c successor)"
by (typecheck_cfuncs, smt (verit, del_insts) comp_associative2 g_square)
then have g_s_s_zEqs_i1zUi1s_i1z: "((g ∘⇩c successor) ∘⇩c successor)∘⇩c zero =
((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c (i1 ∘⇩c zero)"
by (typecheck_cfuncs, smt (verit, ccfv_SIG) comp_associative2 g_square second_diagram3)
then have i1_sEqs_i1zUi1s_i1: "i1 ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c i1"
by (typecheck_cfuncs, simp add: i1_def right_coproj_cfunc_coprod)
then obtain u where u_type[type_rule]: "(u: ℕ⇩c → (𝟭 ∐ ℕ⇩c))" and
u_triangle: "u ∘⇩c zero = i1 ∘⇩c zero" and
u_square: "u ∘⇩c successor = ((i1 ∘⇩c zero) ⨿ (i1 ∘⇩c successor)) ∘⇩c u "
using i1_sEqs_i1zUi1s_i1 by (typecheck_cfuncs, blast)
then have u_Eqs_i1: "u=i1"
by (typecheck_cfuncs, meson cfunc_coprod_type comp_type i1_sEqs_i1zUi1s_i1 natural_number_object_func_unique successor_type zero_type)
have g_s_type[type_rule]: "g ∘⇩c successor: ℕ⇩c → (𝟭 ∐ ℕ⇩c)"
by typecheck_cfuncs
have g_s_triangle: "(g∘⇩c successor) ∘⇩c zero = i1 ∘⇩c zero"
using comp_associative2 second_diagram3 by (typecheck_cfuncs, force)
then have u_Eqs_g_s: "u= g∘⇩c successor"
by (typecheck_cfuncs, smt (verit, ccfv_SIG) cfunc_coprod_type comp_type g_s_s_Eqs_i1zUi1s_g_s g_s_triangle i1_sEqs_i1zUi1s_i1 natural_number_object_func_unique u_Eqs_i1 zero_type)
then have g_sEqs_i1: "g∘⇩c successor = i1"
using u_Eqs_i1 by blast
have eq1: "(zero ⨿ successor) ∘⇩c g = id(ℕ⇩c)"
by (typecheck_cfuncs, smt (verit, best) cfunc_coprod_comp comp_associative2 g_square g_triangle i0_def i1_def i1_type id_left_unit2 id_right_unit2 left_coproj_cfunc_coprod natural_number_object_func_unique right_coproj_cfunc_coprod)
then have eq2: "g ∘⇩c (zero ⨿ successor) = id(𝟭 ∐ ℕ⇩c)"
by (typecheck_cfuncs, metis cfunc_coprod_comp g_sEqs_i1 g_triangle i0_def i1_def id_coprod)
show "isomorphism(zero ⨿ successor)"
using cfunc_coprod_type eq1 eq2 g_type isomorphism_def3 successor_type zero_type by blast
qed
lemma zUs_epic:
"epimorphism(zero ⨿ successor)"
by (simp add: iso_imp_epi_and_monic oneUN_iso_N_isomorphism)
lemma zUs_surj:
"surjective(zero ⨿ successor)"
by (simp add: cfunc_type_def epi_is_surj zUs_epic)
lemma nonzero_is_succ_aux:
assumes "x ∈⇩c (𝟭 ∐ ℕ⇩c)"
shows "(x = (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭) ∨
(∃n. (n ∈⇩c ℕ⇩c) ∧ (x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n))"
by(clarify, metis assms coprojs_jointly_surj id_type one_unique_element)
lemma nonzero_is_succ:
assumes "k ∈⇩c ℕ⇩c"
assumes "k ≠ zero"
shows "∃n.(n∈⇩c ℕ⇩c ∧ k = successor ∘⇩c n)"
proof -
have x_exists: "∃x. ((x ∈⇩c 𝟭 ∐ ℕ⇩c) ∧ (zero ⨿ successor ∘⇩c x = k))"
using assms cfunc_type_def surjective_def zUs_surj by (typecheck_cfuncs, auto)
obtain x where x_def: "((x ∈⇩c 𝟭 ∐ ℕ⇩c) ∧ (zero ⨿ successor ∘⇩c x = k))"
using x_exists by blast
have cases: "(x = (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭) ∨
(∃n. (n ∈⇩c ℕ⇩c ∧ x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n))"
by (simp add: nonzero_is_succ_aux x_def)
have not_case_1: "x ≠ (left_coproj 𝟭 ℕ⇩c) ∘⇩c id 𝟭"
proof(rule ccontr,clarify)
assume bwoc: "x = left_coproj 𝟭 ℕ⇩c ∘⇩c id⇩c 𝟭"
have contradiction: "k = zero"
by (metis bwoc id_right_unit2 left_coproj_cfunc_coprod left_proj_type successor_type x_def zero_type)
show False
using contradiction assms(2) by force
qed
then obtain n where n_def: "n ∈⇩c ℕ⇩c ∧ x = (right_coproj 𝟭 ℕ⇩c) ∘⇩c n"
using cases by blast
then have "k = zero ⨿ successor ∘⇩c x"
using x_def by blast
also have "... = zero ⨿ successor ∘⇩c right_coproj 𝟭 ℕ⇩c ∘⇩c n"
by (simp add: n_def)
also have "... = (zero ⨿ successor ∘⇩c right_coproj 𝟭 ℕ⇩c) ∘⇩c n"
using cfunc_coprod_type cfunc_type_def comp_associative n_def right_proj_type successor_type zero_type by auto
also have "... = successor ∘⇩c n"
using right_coproj_cfunc_coprod successor_type zero_type by auto
finally show ?thesis
using n_def by auto
qed
subsection ‹Predecessor›
definition predecessor' :: "cfunc" where
"predecessor' = (THE f. f : ℕ⇩c → 𝟭 ∐ ℕ⇩c
∧ f ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c) ∧ (zero ⨿ successor) ∘⇩c f = id ℕ⇩c)"
lemma predecessor'_def2:
"predecessor' : ℕ⇩c → 𝟭 ∐ ℕ⇩c ∧ predecessor' ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c)
∧ (zero ⨿ successor) ∘⇩c predecessor' = id ℕ⇩c"
unfolding predecessor'_def
proof (rule theI', safe)
show "∃x. x : ℕ⇩c → 𝟭 ∐ ℕ⇩c ∧
x ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c) ∧ zero ⨿ successor ∘⇩c x = id⇩c ℕ⇩c"
using oneUN_iso_N_isomorphism by (typecheck_cfuncs, unfold isomorphism_def cfunc_type_def, auto)
next
fix x y
assume x_type[type_rule]: "x : ℕ⇩c → 𝟭 ∐ ℕ⇩c" and y_type[type_rule]: "y : ℕ⇩c → 𝟭 ∐ ℕ⇩c"
assume x_left_inv: "zero ⨿ successor ∘⇩c x = id⇩c ℕ⇩c"
assume "x ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c)" "y ∘⇩c zero ⨿ successor = id⇩c (𝟭 ∐ ℕ⇩c)"
then have "x ∘⇩c zero ⨿ successor = y ∘⇩c zero ⨿ successor"
by auto
then have "x ∘⇩c zero ⨿ successor ∘⇩c x = y ∘⇩c zero ⨿ successor ∘⇩c x"
by (typecheck_cfuncs, auto simp add: comp_associative2)
then show "x = y"
using id_right_unit2 x_left_inv x_type y_type by auto
qed
lemma predecessor'_type[type_rule]:
"predecessor' : ℕ⇩c → 𝟭 ∐ ℕ⇩c"
by (simp add: predecessor'_def2)
lemma predecessor'_left_inv:
"(zero ⨿ successor) ∘⇩c predecessor' = id ℕ⇩c"
by (simp add: predecessor'_def2)
lemma predecessor'_right_inv:
"predecessor' ∘⇩c (zero ⨿ successor) = id (𝟭 ∐ ℕ⇩c)"
by (simp add: predecessor'_def2)
lemma predecessor'_successor:
"predecessor' ∘⇩c successor = right_coproj 𝟭 ℕ⇩c"
proof -
have "predecessor' ∘⇩c successor = predecessor' ∘⇩c (zero ⨿ successor) ∘⇩c right_coproj 𝟭 ℕ⇩c"
using right_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = (predecessor' ∘⇩c (zero ⨿ successor)) ∘⇩c right_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = right_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, simp add: id_left_unit2 predecessor'_def2)
finally show ?thesis.
qed
lemma predecessor'_zero:
"predecessor' ∘⇩c zero = left_coproj 𝟭 ℕ⇩c"
proof -
have "predecessor' ∘⇩c zero = predecessor' ∘⇩c (zero ⨿ successor) ∘⇩c left_coproj 𝟭 ℕ⇩c"
using left_coproj_cfunc_coprod by (typecheck_cfuncs, auto)
also have "... = (predecessor' ∘⇩c (zero ⨿ successor)) ∘⇩c left_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, auto simp add: comp_associative2)
also have "... = left_coproj 𝟭 ℕ⇩c"
by (typecheck_cfuncs, simp add: id_left_unit2 predecessor'_def2)
finally show ?thesis.
qed
definition predecessor :: "cfunc"
where "predecessor = (zero ⨿ id ℕ⇩c) ∘⇩c predecessor'"
lemma predecessor_type[type_rule]:
"predecessor : ℕ⇩c → ℕ⇩c"
unfolding predecessor_def by typecheck_cfuncs
lemma predecessor_zero:
"predecessor ∘⇩c zero = zero"
unfolding predecessor_def
using left_coproj_cfunc_coprod predecessor'_zero by (etcs_assocr, typecheck_cfuncs, presburger)
lemma predecessor_successor:
"predecessor ∘⇩c successor = id ℕ⇩c"
unfolding predecessor_def
by (etcs_assocr, typecheck_cfuncs, metis (full_types) predecessor'_successor right_coproj_cfunc_coprod)
subsection ‹Peano's Axioms and Induction›
text ‹The lemma below corresponds to Proposition 2.6.7 in Halvorson.›
lemma Peano's_Axioms:
"injective successor ∧ ¬ surjective successor"
proof -
have i1_mono: "monomorphism(right_coproj 𝟭 ℕ⇩c)"
by (simp add: right_coproj_are_monomorphisms)
have zUs_iso: "isomorphism(zero ⨿ successor)"
using oneUN_iso_N_isomorphism by blast
have zUsi1EqsS: "(zero ⨿ successor) ∘⇩c (right_coproj 𝟭 ℕ⇩c) = successor"
using right_coproj_cfunc_coprod successor_type zero_type by auto
then have succ_mono: "monomorphism(successor)"
by (metis cfunc_coprod_type cfunc_type_def composition_of_monic_pair_is_monic i1_mono iso_imp_epi_and_monic oneUN_iso_N_isomorphism right_proj_type successor_type zero_type)
obtain u where u_type: "u: ℕ⇩c → Ω" and u_def: "u ∘⇩c zero = 𝗍 ∧ (𝖿∘⇩cβ⇘Ω⇙) ∘⇩c u = u ∘⇩c successor"
by (typecheck_cfuncs, metis natural_number_object_property)
have s_not_surj: "¬ surjective successor"
proof (rule ccontr, clarify)
assume BWOC : "surjective successor"
obtain n where n_type: "n : 𝟭 → ℕ⇩c" and snEqz: "successor ∘⇩c n = zero"
using BWOC cfunc_type_def successor_type surjective_def zero_type by auto
then show False
by (metis zero_is_not_successor)
qed
then show "injective successor ∧ ¬ surjective successor"
using monomorphism_imp_injective succ_mono by blast
qed
lemma succ_inject:
assumes "n ∈⇩c ℕ⇩c" "m ∈⇩c ℕ⇩c"
shows "successor ∘⇩c n = successor ∘⇩c m ⟹ n = m"
by (metis Peano's_Axioms assms cfunc_type_def injective_def successor_type)
theorem nat_induction:
assumes p_type[type_rule]: "p : ℕ⇩c → Ω" and n_type[type_rule]: "n ∈⇩c ℕ⇩c"
assumes base_case: "p ∘⇩c zero = 𝗍"
assumes induction_case: "⋀n. n ∈⇩c ℕ⇩c ⟹ p ∘⇩c n = 𝗍 ⟹ p ∘⇩c successor ∘⇩c n = 𝗍"
shows "p ∘⇩c n = 𝗍"
proof -
obtain p' P where
p'_type[type_rule]: "p' : P → ℕ⇩c" and
p'_equalizer: "p ∘⇩c p' = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c p'" and
p'_uni_prop: "∀ h F. (h : F → ℕ⇩c ∧ p ∘⇩c h = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c h) ⟶ (∃! k. k : F → P ∧ p' ∘⇩c k = h)"
using equalizer_exists2 by (typecheck_cfuncs, blast)
from base_case have "p ∘⇩c zero = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c zero"
by (etcs_assocr, etcs_subst terminal_func_comp_elem id_right_unit2, -)
then obtain z' where
z'_type[type_rule]: "z' ∈⇩c P" and
z'_def: "zero = p' ∘⇩c z'"
using p'_uni_prop by (typecheck_cfuncs, metis)
have "p ∘⇩c successor ∘⇩c p' = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor ∘⇩c p'"
proof (etcs_rule one_separator)
fix m
assume m_type[type_rule]: "m ∈⇩c P"
have "p ∘⇩c p' ∘⇩c m = 𝗍 ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c p' ∘⇩c m"
by (etcs_assocl, simp add: p'_equalizer)
then have "p ∘⇩c p' ∘⇩c m = 𝗍"
by (-, etcs_subst_asm terminal_func_comp_elem id_right_unit2, simp)
then have "p ∘⇩c successor ∘⇩c p' ∘⇩c m = 𝗍"
using induction_case by (typecheck_cfuncs, simp)
then show "(p ∘⇩c successor ∘⇩c p') ∘⇩c m = ((𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c successor ∘⇩c p') ∘⇩c m"
by (etcs_assocr, etcs_subst terminal_func_comp_elem id_right_unit2, -)
qed
then obtain s' where
s'_type[type_rule]: "s' : P → P" and
s'_def: "p' ∘⇩c s' = successor ∘⇩c p'"
using p'_uni_prop by (typecheck_cfuncs, metis)
obtain u where
u_type[type_rule]: "u : ℕ⇩c → P" and
u_zero: "u ∘⇩c zero = z'" and
u_succ: "u ∘⇩c successor = s' ∘⇩c u"
using natural_number_object_property2 by (typecheck_cfuncs, metis s'_type)
have p'_u_is_id: "p' ∘⇩c u = id ℕ⇩c"
proof (etcs_rule natural_number_object_func_unique[where f=successor])
show "(p' ∘⇩c u) ∘⇩c zero = id⇩c ℕ⇩c ∘⇩c zero"
by (etcs_subst id_left_unit2, etcs_assocr, simp add: u_zero sym[OF z'_def])
show "(p' ∘⇩c u) ∘⇩c successor = successor ∘⇩c p' ∘⇩c u"
by (etcs_assocr, subst u_succ, etcs_assocl, simp add: s'_def)
show "id⇩c ℕ⇩c ∘⇩c successor = successor ∘⇩c id⇩c ℕ⇩c"
by (etcs_subst id_right_unit2 id_left_unit2, simp)
qed
have "p ∘⇩c p' ∘⇩c u ∘⇩c n = (𝗍 ∘⇩c β⇘ℕ⇩c⇙) ∘⇩c p' ∘⇩c u ∘⇩c n"
by (typecheck_cfuncs, smt comp_associative2 p'_equalizer)
then show "p ∘⇩c n = 𝗍"
by (typecheck_cfuncs, smt (z3) comp_associative2 id_left_unit2 id_right_unit2 p'_type p'_u_is_id terminal_func_comp_elem terminal_func_type u_type)
qed
subsection ‹Function Iteration›
definition ITER_curried :: "cset ⇒ cfunc" where
"ITER_curried U = (THE u . u : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖ ∧ u ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯ ∧
((meta_comp U U U) ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c u = u ∘⇩c successor)"
lemma ITER_curried_def2:
"ITER_curried U : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖ ∧ ITER_curried U ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯ ∧
((meta_comp U U U) ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U = ITER_curried U ∘⇩c successor"
unfolding ITER_curried_def
by(rule theI', etcs_rule natural_number_object_property2)
lemma ITER_curried_type[type_rule]:
"ITER_curried U : ℕ⇩c → (U⇗U⇖)⇗U⇗U⇖⇖"
by (simp add: ITER_curried_def2)
lemma ITER_curried_zero:
"ITER_curried U ∘⇩c zero = (metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯"
by (simp add: ITER_curried_def2)
lemma ITER_curried_successor:
"ITER_curried U ∘⇩c successor = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U"
using ITER_curried_def2 by simp
definition ITER :: "cset ⇒ cfunc" where
"ITER U = (ITER_curried U)⇧♭"
lemma ITER_type[type_rule]:
"ITER U : ((U⇗U⇖) ×⇩c ℕ⇩c) → (U⇗U⇖)"
unfolding ITER_def by typecheck_cfuncs
lemma ITER_zero:
assumes f_type[type_rule]: "f : Z → (U⇗U⇖)"
shows "ITER U ∘⇩c ⟨f, zero ∘⇩c β⇘Z⇙⟩ = metafunc (id U) ∘⇩c β⇘Z⇙"
proof(etcs_rule one_separator)
fix z
assume z_type[type_rule]: "z ∈⇩c Z"
have "(ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩) ∘⇩c z = ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩ ∘⇩c z"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ITER U ∘⇩c ⟨f ∘⇩c z,zero⟩"
using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2 id_right_unit2 terminal_func_comp_elem)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f ITER_curried U) ∘⇩c ⟨f ∘⇩c z,zero⟩"
using assms ITER_def comp_associative2 inv_transpose_func_def3 by (typecheck_cfuncs, auto)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,ITER_curried U ∘⇩c zero⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,(metafunc (id U) ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯⟩"
using assms by (simp add: ITER_curried_def2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z,((left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯⟩"
using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f ((left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭))⇧♯) ∘⇩c ⟨f ∘⇩c z,id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (left_cart_proj (U) 𝟭)⇧♯ ∘⇩c (right_cart_proj (U⇗U⇖) 𝟭) ∘⇩c ⟨f ∘⇩c z,id⇩c 𝟭⟩"
using assms by (typecheck_cfuncs,simp add: cfunc_type_def comp_associative transpose_func_def)
also have "... = (left_cart_proj (U) 𝟭)⇧♯"
using assms by (typecheck_cfuncs, simp add: id_right_unit2 right_cart_proj_cfunc_prod)
also have "... = (metafunc (id⇩c U))"
using assms by (typecheck_cfuncs, simp add: id_left_unit2 metafunc_def2)
also have "... = (metafunc (id⇩c U) ∘⇩c β⇘Z⇙) ∘⇩c z"
using assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative id_right_unit2 terminal_func_comp_elem)
finally show "(ITER U ∘⇩c ⟨f,zero ∘⇩c β⇘Z⇙⟩) ∘⇩c z = (metafunc (id⇩c U) ∘⇩c β⇘Z⇙) ∘⇩c z".
qed
lemma ITER_zero':
assumes "f ∈⇩c (U⇗U⇖)"
shows "ITER U ∘⇩c ⟨f, zero⟩ = metafunc (id U)"
by (typecheck_cfuncs, metis ITER_zero assms id_right_unit2 id_type one_unique_element terminal_func_type)
lemma ITER_succ:
assumes f_type[type_rule]: "f : Z → (U⇗U⇖)" and n_type[type_rule]: "n : Z → ℕ⇩c"
shows "ITER U ∘⇩c ⟨f, successor ∘⇩c n⟩ = f □ (ITER U ∘⇩c ⟨f, n ⟩)"
proof(etcs_rule one_separator)
fix z
assume z_type[type_rule]: "z ∈⇩c Z"
have "(ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩) ∘⇩c z = ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩ ∘⇩c z"
using assms by (typecheck_cfuncs, simp add: comp_associative2)
also have "... = ITER U ∘⇩c ⟨f ∘⇩c z, successor ∘⇩c (n ∘⇩c z)⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_prod_comp comp_associative2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id⇩c (U⇗U⇖) ×⇩f ITER_curried U) ∘⇩c ⟨f ∘⇩c z, successor ∘⇩c (n ∘⇩c z)⟩"
using assms by (typecheck_cfuncs, simp add: ITER_def comp_associative2 inv_transpose_func_def3)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (successor ∘⇩c (n ∘⇩c z))⟩"
using assms cfunc_cross_prod_comp_cfunc_prod id_left_unit2 by (typecheck_cfuncs, force)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, (ITER_curried U ∘⇩c successor) ∘⇩c (n ∘⇩c z)⟩"
using assms by(typecheck_cfuncs, metis comp_associative2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U) ∘⇩c (n ∘⇩c z)⟩"
using assms ITER_curried_successor by presburger
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id (U⇗U⇖) ×⇩f ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ∘⇩c ITER_curried U) ∘⇩c (n ∘⇩c z))∘⇩c ⟨f ∘⇩c z, id 𝟭⟩"
using assms by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod id_left_unit2 id_right_unit2)
also have "... = (eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (id (U⇗U⇖) ×⇩f ((meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))⇧♯ ))∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n ∘⇩c z)⟩"
using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod comp_associative2 id_right_unit2)
also have "... = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)) ∘⇩c (diagonal(U⇗U⇖)×⇩f id ((U⇗U⇖)⇗U⇗U⇖⇖)))∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n ∘⇩c z)⟩"
using assms by (typecheck_cfuncs, metis cfunc_type_def comp_associative transpose_func_def)
also have "... = (meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c (associate_right (U⇗U⇖) (U⇗U⇖) ((U⇗U⇖)⇗U⇗U⇖⇖)))∘⇩c ⟨⟨f ∘⇩c z,f ∘⇩c z⟩, ITER_curried U ∘⇩c (n ∘⇩c z)⟩"
using assms by (etcs_assocr, typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod diag_on_elements id_left_unit2)
also have "... = meta_comp U U U ∘⇩c (id (U⇗U⇖) ×⇩f eval_func (U⇗U⇖) (U⇗U⇖)) ∘⇩c ⟨f ∘⇩c z, ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n ∘⇩c z)⟩⟩"
using assms by (typecheck_cfuncs, smt (z3) associate_right_ap comp_associative2)
also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, eval_func (U⇗U⇖) (U⇗U⇖) ∘⇩c ⟨f ∘⇩c z, ITER_curried U ∘⇩c (n ∘⇩c z)⟩⟩"
using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, eval_func (U⇗U⇖) (U⇗U⇖) ∘⇩c (id(U⇗U⇖) ×⇩f ITER_curried U)∘⇩c ⟨f ∘⇩c z, n ∘⇩c z⟩⟩"
using assms by (typecheck_cfuncs, smt (z3) cfunc_cross_prod_comp_cfunc_prod id_left_unit2)
also have "... = meta_comp U U U ∘⇩c ⟨f ∘⇩c z, ITER U ∘⇩c ⟨f ∘⇩c z, n ∘⇩c z⟩⟩"
using assms by (typecheck_cfuncs, smt (z3) ITER_def comp_associative2 inv_transpose_func_def3)
also have "... = meta_comp U U U ∘⇩c ⟨f, ITER U ∘⇩c ⟨f , n⟩⟩ ∘⇩c z"
using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
also have "... = (meta_comp U U U ∘⇩c ⟨f, ITER U ∘⇩c ⟨f , n⟩⟩) ∘⇩c z"
using assms by (typecheck_cfuncs, meson comp_associative2)
also have "... = (f □ (ITER U ∘⇩c ⟨f,n⟩)) ∘⇩c z"
using assms by (typecheck_cfuncs, simp add: meta_comp2_def5)
finally show "(ITER U ∘⇩c ⟨f,successor ∘⇩c n⟩) ∘⇩c z = (f □ ITER U ∘⇩c ⟨f,n⟩) ∘⇩c z".
qed
lemma ITER_one:
assumes "f ∈⇩c (U⇗U⇖)"
shows "ITER U ∘⇩c ⟨f, successor ∘⇩c zero⟩ = f □ (metafunc (id U))"
using ITER_succ ITER_zero' assms zero_type by presburger
definition iter_comp :: "cfunc ⇒ cfunc ⇒ cfunc" ("_⇗∘_⇖"[55,0]55) where
"iter_comp g n ≡ cnufatem (ITER (domain g) ∘⇩c ⟨metafunc g,n⟩)"
lemma iter_comp_def2:
"g⇗∘n⇖ ≡ cnufatem(ITER (domain g) ∘⇩c ⟨metafunc g,n⟩)"
by (simp add: iter_comp_def)
lemma iter_comp_type[type_rule]:
assumes "g : X → X"
assumes "n ∈⇩c ℕ⇩c"
shows "g⇗∘n⇖: X → X"
unfolding iter_comp_def2
by (smt (verit, ccfv_SIG) ITER_type assms cfunc_type_def cnufatem_type comp_type metafunc_type right_param_on_el right_param_type)
lemma iter_comp_def3:
assumes "g : X → X"
assumes "n ∈⇩c ℕ⇩c"
shows "g⇗∘n⇖ = cnufatem (ITER X ∘⇩c ⟨metafunc g,n⟩)"
using assms cfunc_type_def iter_comp_def2 by auto
lemma zero_iters:
assumes g_type[type_rule]: "g : X → X"
shows "g⇗∘zero⇖ = id⇩c X"
proof(etcs_rule one_separator)
fix x
assume x_type[type_rule]: "x ∈⇩c X"
have "(g⇗∘zero⇖) ∘⇩c x = (cnufatem (ITER X ∘⇩c ⟨metafunc g,zero⟩)) ∘⇩c x"
using assms iter_comp_def3 by (typecheck_cfuncs, auto)
also have "... = cnufatem (metafunc (id X)) ∘⇩c x"
by (simp add: ITER_zero' assms metafunc_type)
also have "... = id⇩c X ∘⇩c x"
by (metis cnufatem_metafunc id_type)
also have "... = x"
by (typecheck_cfuncs, simp add: id_left_unit2)
ultimately show "(g⇗∘zero⇖) ∘⇩c x = id⇩c X ∘⇩c x"
by simp
qed
lemma succ_iters:
assumes "g : X → X"
assumes "n ∈⇩c ℕ⇩c"
shows "g⇗∘(successor ∘⇩c n)⇖ = g ∘⇩c (g⇗∘n⇖)"
proof -
have "g⇗∘successor ∘⇩c n⇖ = cnufatem(ITER X ∘⇩c ⟨metafunc g,successor ∘⇩c n ⟩)"
using assms by (typecheck_cfuncs, simp add: iter_comp_def3)
also have "... = cnufatem(metafunc g □ ITER X ∘⇩c ⟨metafunc g, n ⟩)"
using assms by (typecheck_cfuncs, simp add: ITER_succ)
also have "... = cnufatem(metafunc g □ metafunc (g⇗∘n⇖))"
using assms by (typecheck_cfuncs, metis iter_comp_def3 metafunc_cnufatem)
also have "... = g ∘⇩c (g⇗∘n⇖)"
using assms by (typecheck_cfuncs, simp add: comp_as_metacomp)
finally show ?thesis.
qed
corollary one_iter:
assumes "g : X → X"
shows "g⇗∘(successor ∘⇩c zero)⇖ = g"
using assms id_right_unit2 succ_iters zero_iters zero_type by force
lemma eval_lemma_for_ITER:
assumes "f : X → X"
assumes "x ∈⇩c X"
assumes "m ∈⇩c ℕ⇩c"
shows "(f⇗∘m⇖) ∘⇩c x = eval_func X X ∘⇩c ⟨x ,ITER X ∘⇩c ⟨metafunc f ,m⟩⟩"
using assms by (typecheck_cfuncs, metis eval_lemma iter_comp_def3 metafunc_cnufatem)
lemma n_accessible_by_succ_iter_aux:
"eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙, ITER ℕ⇩c ∘⇩c ⟨(metafunc successor) ∘⇩c β⇘ℕ⇩c⇙ ,id ℕ⇩c⟩⟩ = id ℕ⇩c"
proof(rule natural_number_object_func_unique[where X="ℕ⇩c", where f = successor])
show "eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩ : ℕ⇩c → ℕ⇩c"
by typecheck_cfuncs
show "id⇩c ℕ⇩c : ℕ⇩c → ℕ⇩c"
by typecheck_cfuncs
show "successor : ℕ⇩c → ℕ⇩c"
by typecheck_cfuncs
next
have "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c zero =
eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c zero,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c zero,id⇩c ℕ⇩c ∘⇩c zero⟩⟩"
by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero,ITER ℕ⇩c ∘⇩c ⟨metafunc successor,zero⟩⟩"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero,metafunc (id ℕ⇩c) ⟩"
by (typecheck_cfuncs, simp add: ITER_zero')
also have "... = id⇩c ℕ⇩c ∘⇩c zero"
using eval_lemma by (typecheck_cfuncs, blast)
finally show "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c zero = id⇩c ℕ⇩c ∘⇩c zero".
show "(eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor =
successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩"
proof(etcs_rule one_separator)
fix m
assume m_type[type_rule]: "m ∈⇩c ℕ⇩c"
have "(successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c m =
successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c m,id⇩c ℕ⇩c ∘⇩c m⟩⟩"
by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
also have "... = successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ,m⟩⟩"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
also have "... = successor ∘⇩c (successor⇗∘m⇖) ∘⇩c zero"
by (typecheck_cfuncs, simp add: eval_lemma_for_ITER)
also have "... = (successor⇗∘successor ∘⇩c m⇖) ∘⇩c zero"
by (typecheck_cfuncs, simp add: comp_associative2 succ_iters)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ,successor ∘⇩c m⟩⟩"
by (typecheck_cfuncs, simp add: eval_lemma_for_ITER)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c (successor ∘⇩c m),ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙∘⇩c (successor ∘⇩c m),id⇩c ℕ⇩c ∘⇩c (successor ∘⇩c m)⟩⟩"
by (typecheck_cfuncs,simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
also have "... = ((eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor) ∘⇩c m"
by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
ultimately show "((eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c successor) ∘⇩c m =
(successor ∘⇩c eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙,ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙,id⇩c ℕ⇩c⟩⟩) ∘⇩c m"
by simp
qed
show "id⇩c ℕ⇩c ∘⇩c successor = successor ∘⇩c id⇩c ℕ⇩c"
by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2)
qed
lemma n_accessible_by_succ_iter:
assumes "n ∈⇩c ℕ⇩c"
shows "(successor⇗∘n⇖) ∘⇩c zero = n"
proof -
have "n = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙, ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙, id ℕ⇩c⟩⟩ ∘⇩c n"
using assms by (typecheck_cfuncs, simp add: comp_associative2 id_left_unit2 n_accessible_by_succ_iter_aux)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c n , ITER ℕ⇩c ∘⇩c ⟨metafunc successor ∘⇩c β⇘ℕ⇩c⇙ ∘⇩c n, id ℕ⇩c ∘⇩c n⟩⟩"
using assms by (typecheck_cfuncs, smt (z3) cfunc_prod_comp comp_associative2)
also have "... = eval_func ℕ⇩c ℕ⇩c ∘⇩c ⟨zero, ITER ℕ⇩c ∘⇩c ⟨metafunc successor, n⟩⟩"
using assms by (typecheck_cfuncs, simp add: id_left_unit2 id_right_unit2 terminal_func_comp_elem)
also have "... = (successor⇗∘n⇖) ∘⇩c zero"
using assms by (typecheck_cfuncs, metis eval_lemma iter_comp_def3 metafunc_cnufatem)
ultimately show ?thesis
by simp
qed
subsection ‹Relation of Nat to Other Sets›
lemma oneUN_iso_N:
"𝟭 ∐ ℕ⇩c ≅ ℕ⇩c"
using cfunc_coprod_type is_isomorphic_def oneUN_iso_N_isomorphism successor_type zero_type by blast
lemma NUone_iso_N:
"ℕ⇩c ∐ 𝟭 ≅ ℕ⇩c"
using coproduct_commutes isomorphic_is_transitive oneUN_iso_N by blast
end