section ‹TOTAL is a proper subset of CONS\label{s:total_cons}› theory TOTAL_CONS imports Lemma_R (* for r_auxhyp *) CP_FIN_NUM (* for r_consistent *) CONS_LIM (* for rmge2, goedel_at *) begin text ‹We first show that TOTAL is a subset of CONS. Then we present a separating class.› subsection ‹TOTAL is a subset of CONS› text ‹A TOTAL strategy hypothesizes only total functions, for which the consistency with the input prefix is decidable. A CONS strategy can thus run a TOTAL strategy and check if its hypothesis is consistent. If so, it outputs this hypothesis, otherwise some arbitrary consistent one. Since the TOTAL strategy converges to a correct hypothesis, which is consistent, the CONS strategy will converge to the same hypothesis.› text ‹Without loss of generality we can assume that learning takes place with respect to our Gödel numbering $\varphi$. So we need to decide consistency only for this numbering.› abbreviation r_consist_phi where "r_consist_phi ≡ r_consistent r_phi" lemma r_consist_phi_recfn [simp]: "recfn 2 r_consist_phi" by simp lemma r_consist_phi: assumes "∀k<e_length e. φ i k ↓" shows "eval r_consist_phi [i, e] ↓= (if ∀k<e_length e. φ i k ↓= e_nth e k then 0 else 1)" proof - have "∀k<e_length e. eval r_phi [i, k] ↓" using assms phi_def by simp moreover have "recfn 2 r_phi" by simp ultimately have "eval (r_consistent r_phi) [i, e] ↓= (if ∀k<e_length e. eval r_phi [i, k] ↓= e_nth e k then 0 else 1)" using r_consistent_converg assms by simp then show ?thesis using phi_def by simp qed lemma r_consist_phi_init: assumes "f ∈ ℛ" and "φ i ∈ ℛ" shows "eval r_consist_phi [i, f ▹ n] ↓= (if ∀k≤n. φ i k = f k then 0 else 1)" using assms r_consist_phi R1_imp_total1 total1E by (simp add: r_consist_phi) lemma TOTAL_subseteq_CONS: "TOTAL ⊆ CONS" proof fix U assume "U ∈ TOTAL" then have "U ∈ TOTAL_wrt φ" using TOTAL_wrt_phi_eq_TOTAL by blast then obtain t' where t': "learn_total φ U t'" using TOTAL_wrt_def by auto then obtain t where t: "recfn 1 t" "⋀x. eval t [x] = t' x" using learn_totalE(1) P1E by blast then have t_converg: "eval t [f ▹ n] ↓" if "f ∈ U" for f n using t' learn_totalE(1) that by auto define s where "s ≡ Cn 1 r_ifz [Cn 1 r_consist_phi [t, Id 1 0], t, r_auxhyp]" then have "recfn 1 s" using r_consist_phi_recfn r_auxhyp_prim t(1) by simp have consist: "eval r_consist_phi [the (eval t [f ▹ n]), f ▹ n] ↓= (if ∀k≤n. φ (the (eval t [f ▹ n])) k = f k then 0 else 1)" if "f ∈ U" for f n proof - have "eval r_consist_phi [the (eval t [f ▹ n]), f ▹ n] = eval (Cn 1 r_consist_phi [t, Id 1 0]) [f ▹ n]" using that t_converg t(1) by simp also have "... ↓= (if ∀k≤n. φ (the (eval t [f ▹ n])) k = f k then 0 else 1)" proof - from that have "f ∈ ℛ" using learn_totalE(1) t' by blast moreover have "φ (the (eval t [f ▹ n])) ∈ ℛ" using t' t learn_totalE t_converg that by simp ultimately show ?thesis using r_consist_phi_init t_converg t(1) that by simp qed finally show ?thesis . qed have s_eq_t: "eval s [f ▹ n] = eval t [f ▹ n]" if "∀k≤n. φ (the (eval t [f ▹ n])) k = f k" and "f ∈ U" for f n using that consist s_def t r_auxhyp_prim prim_recfn_total by simp have s_eq_aux: "eval s [f ▹ n] = eval r_auxhyp [f ▹ n]" if "¬ (∀k≤n. φ (the (eval t [f ▹ n])) k = f k)" and "f ∈ U" for f n proof - from that have "eval r_consist_phi [the (eval t [f ▹ n]), f ▹ n] ↓= 1" using consist by simp moreover have "t' (f ▹ n) ↓" using t' learn_totalE(1) that(2) by blast ultimately show ?thesis using s_def t r_auxhyp_prim t' learn_totalE by simp qed have "learn_cons φ U (λe. eval s [e])" proof (rule learn_consI) have "eval s [f ▹ n] ↓" if "f ∈ U" for f n using that t_converg[OF that, of n] s_eq_t[of n f] prim_recfn_total[of r_auxhyp 1] r_auxhyp_prim s_eq_aux[OF _ that, of n] totalE by fastforce then show "environment φ U (λe. eval s [e])" using t' ‹recfn 1 s› learn_totalE(1) by blast show "∃i. φ i = f ∧ (∀⇧^{∞}n. eval s [f ▹ n] ↓= i)" if "f ∈ U" for f proof - from that t' t learn_totalE obtain i n⇩_{0}where i_n0: "φ i = f ∧ (∀n≥n⇩_{0}. eval t [f ▹ n] ↓= i)" by metis then have "⋀n. n ≥ n⇩_{0}⟹ ∀k≤n. φ (the (eval t [f ▹ n])) k = f k" by simp with s_eq_t have "⋀n. n ≥ n⇩_{0}⟹ eval s [f ▹ n] = eval t [f ▹ n]" using that by simp with i_n0 have "⋀n. n ≥ n⇩_{0}⟹ eval s [f ▹ n] ↓= i" by auto with i_n0 show ?thesis by auto qed show "∀k≤n. φ (the (eval s [f ▹ n])) k = f k" if "f ∈ U" for f n proof (cases "∀k≤n. φ (the (eval t [f ▹ n])) k = f k") case True with that s_eq_t show ?thesis by simp next case False then have "eval s [f ▹ n] = eval r_auxhyp [f ▹ n]" using that s_eq_aux by simp moreover have "f ∈ ℛ" using learn_totalE(1)[OF t'] that by auto ultimately show ?thesis using r_auxhyp by simp qed qed then show "U ∈ CONS" using CONS_def by auto qed subsection ‹The separating class› subsubsection ‹Definition of the class› text ‹The class that will be shown to be in @{term "CONS - TOTAL"} is the union of the following two classes.› definition V_constotal_1 :: "partial1 set" where "V_constotal_1 ≡ {f. ∃j p. f = [j] ⊙ p ∧ j ≥ 2 ∧ p ∈ ℛ⇩_{0}⇩_{1}∧ φ j = f}" definition V_constotal_2 :: "partial1 set" where "V_constotal_2 ≡ {f. ∃j a k. f = j # a @ [k] ⊙ 0⇧^{∞}∧ j ≥ 2 ∧ (∀i<length a. a ! i ≤ 1) ∧ k ≥ 2 ∧ φ j = j # a ⊙ ↑⇧^{∞}∧ φ k = f}" definition V_constotal :: "partial1 set" where "V_constotal ≡ V_constotal_1 ∪ V_constotal_2" lemma V_constotal_2I: assumes "f = j # a @ [k] ⊙ 0⇧^{∞}" and "j ≥ 2" and "∀i<length a. a ! i ≤ 1" and "k ≥ 2" and "φ j = j # a ⊙ ↑⇧^{∞}" and "φ k = f" shows "f ∈ V_constotal_2" using assms V_constotal_2_def by blast lemma V_subseteq_R1: "V_constotal ⊆ ℛ" proof fix f assume "f ∈ V_constotal" then have "f ∈ V_constotal_1 ∨ f ∈ V_constotal_2" using V_constotal_def by auto then show "f ∈ ℛ" proof assume "f ∈ V_constotal_1" then obtain j p where "f = [j] ⊙ p" "p ∈ ℛ⇩_{0}⇩_{1}" using V_constotal_1_def by blast then show ?thesis using prepend_in_R1 RPred1_subseteq_R1 by auto next assume "f ∈ V_constotal_2" then obtain j a k where "f = j # a @ [k] ⊙ 0⇧^{∞}" using V_constotal_2_def by blast then show ?thesis using almost0_in_R1 by auto qed qed subsubsection ‹The class is in CONS› text ‹The class can be learned by the strategy @{term rmge2}, which outputs the rightmost value greater or equal two in the input $f^n$. If $f$ is from $V_1$ then the strategy is correct right from the start. If $f$ is from $V_2$ the strategy outputs the consistent hypothesis $j$ until it encounters the correct hypothesis $k$, to which it converges.› lemma V_in_CONS: "learn_cons φ V_constotal rmge2" proof (rule learn_consI) show "environment φ V_constotal rmge2" using V_subseteq_R1 rmge2_in_R1 R1_imp_total1 phi_in_P2 by simp have "(∃i. φ i = f ∧ (∀⇧^{∞}n. rmge2 (f ▹ n) ↓= i)) ∧ (∀n. ∀k≤n. φ (the (rmge2 (f ▹ n))) k = f k)" if "f ∈ V_constotal" for f proof (cases "f ∈ V_constotal_1") case True then obtain j p where f: "f = [j] ⊙ p" and j: "j ≥ 2" and p: "p ∈ ℛ⇩_{0}⇩_{1}" and phi_j: "φ j = f" using V_constotal_1_def by blast then have "f 0 ↓= j" by (simp add: prepend_at_less) then have f_at_0: "the (f 0) ≥ 2" by (simp add: j) have f_at_gr0: "the (f x) ≤ 1" if "x > 0" for x using that f p by (simp add: RPred1_altdef Suc_leI prepend_at_ge) have "total1 f" using V_subseteq_R1 that R1_imp_total1 total1_def by auto have "rmge2 (f ▹ n) ↓= j" for n proof - let ?P = "λi. i < Suc n ∧ the (f i) ≥ 2" have "Greatest ?P = 0" proof (rule Greatest_equality) show "0 < Suc n ∧ 2 ≤ the (f 0)" using f_at_0 by simp show "⋀y. y < Suc n ∧ 2 ≤ the (f y) ⟹ y ≤ 0" using f_at_gr0 by fastforce qed then have "rmge2 (f ▹ n) = f 0" using f_at_0 rmge2_init_total[of f n, OF ‹total1 f›] by auto then show "rmge2 (f ▹ n) ↓= j" by (simp add: ‹f 0 ↓= j›) qed then show ?thesis using phi_j by auto next case False then have "f ∈ V_constotal_2" using V_constotal_def that by auto then obtain j a k where jak: "f = j # a @ [k] ⊙ 0⇧^{∞}" "j ≥ 2" "∀i<length a. a ! i ≤ 1" "k ≥ 2" "φ j = j # a ⊙ ↑⇧^{∞}" "φ k = f" using V_constotal_2_def by blast then have f_at_0: "f 0 ↓= j" by simp have f_eq_a: "f x ↓= a ! (x - 1)" if "0 < x ∧ x < Suc (length a)" for x proof - have "x - 1 < length a" using that by auto then show ?thesis by (simp add: jak(1) less_SucI nth_append that) qed then have f_at_a: "the (f x) ≤ 1" if "0 < x ∧ x < Suc (length a)" for x using jak(3) that by auto from jak have f_k: "f (Suc (length a)) ↓= k" by auto from jak have f_at_big: "f x ↓= 0" if "x > Suc (length a)" for x using that by simp let ?P = "λn i. i < Suc n ∧ the (f i) ≥ 2" have rmge2: "rmge2 (f ▹ n) = f (Greatest (?P n))" for n proof - have "¬ (∀i<Suc n. the (f i) < 2)" for n using jak(2) f_at_0 by auto moreover have "total1 f" using V_subseteq_R1 R1_imp_total1 that total1_def by auto ultimately show ?thesis using rmge2_init_total[of f n] by auto qed have "Greatest (?P n) = 0" if "n < Suc (length a)" for n proof (rule Greatest_equality) show "0 < Suc n ∧ 2 ≤ the (f 0)" using that by (simp add: jak(2) f_at_0) show "⋀y. y < Suc n ∧ 2 ≤ the (f y) ⟹ y ≤ 0" using that f_at_a by (metis Suc_1 dual_order.strict_trans leI less_Suc_eq not_less_eq_eq) qed with rmge2 f_at_0 have rmge2_small: "rmge2 (f ▹ n) ↓= j" if "n < Suc (length a)" for n using that by simp have "Greatest (?P n) = Suc (length a)" if "n ≥ Suc (length a)" for n proof (rule Greatest_equality) show "Suc (length a) < Suc n ∧ 2 ≤ the (f (Suc (length a)))" using that f_k by (simp add: jak(4) less_Suc_eq_le) show "⋀y. y < Suc n ∧ 2 ≤ the (f y) ⟹ y ≤ Suc (length a)" using that f_at_big by (metis leI le_SucI not_less_eq_eq numeral_2_eq_2 option.sel) qed with rmge2 f_at_big f_k have rmge2_big: "rmge2 (f ▹ n) ↓= k" if "n ≥ Suc (length a)" for n using that by simp then have "∃i n⇩_{0}. φ i = f ∧ (∀n≥n⇩_{0}. rmge2 (f ▹ n) ↓= i)" using jak(6) by auto moreover have "∀k≤n. φ (the (rmge2 (f ▹ n))) k = f k" for n proof (cases "n < Suc (length a)") case True then have "rmge2 (f ▹ n) ↓= j" using rmge2_small by simp then have "φ (the (rmge2 (f ▹ n))) = φ j" by simp with True show ?thesis using rmge2_small f_at_0 f_eq_a jak(5) prepend_at_less by (metis le_less_trans le_zero_eq length_Cons not_le_imp_less nth_Cons_0 nth_Cons_pos) next case False then show ?thesis using rmge2_big jak by simp qed ultimately show ?thesis by simp qed then show "⋀f. f ∈ V_constotal ⟹ ∃i. φ i = f ∧ (∀⇧^{∞}n. rmge2 (f ▹ n) ↓= i)" and "⋀f n. f ∈ V_constotal ⟹ ∀k≤n. φ (the (rmge2 (f ▹ n))) k = f k" by simp_all qed subsubsection ‹The class is not in TOTAL› text ‹Recall that $V$ is the union of $V_1 = \{jp \mid j\geq2 \land p \in \mathcal{R}_{01} \land \varphi_j = jp\}$ and $V_2 = \{jak0^\infty \mid j\geq 2 \land a \in \{0, 1\}^* \land k\geq 2 \land \varphi_j = ja\uparrow^\infty \land\ \varphi_k = jak0^\infty\}$.› text ‹The proof is adapted from a proof of a stronger result by Freivalds, Kinber, and Wiehagen~\<^cite>‹‹Theorem~27› in "fkw-iisde-95"› concerning an inference type not defined here. The proof is by contradiction. If $V$ was in TOTAL, there would be a strategy $S$ learning $V$ in our standard Gödel numbering $\varphi$. By Lemma R for TOTAL we can assume $S$ to be total. In order to construct a function $f\in V$ for which $S$ fails we employ a computable process iteratively building function prefixes. For every $j$ the process builds a function $\psi_j$. The initial prefix is the singleton $[j]$. Given a prefix $b$, the next prefix is determined as follows: \begin{enumerate} \item Search for a $y \geq |b|$ with $\varphi_{S(b)}(y) \downarrow= v$ for some $v$. \item Set the new prefix $b0^{y - |b|}\bar{v}$, where $\bar v = 1 - v$. \end{enumerate} Step~1 can diverge, for example, if $\varphi_{S(b)}$ is the empty function. In this case $\psi_j$ will only be defined for a finite prefix. If, however, Step~2 is reached, the prefix $b$ is extended to a $b'$ such that $\varphi_{S(b)}(y) \neq b'_y$, which implies $S(b)$ is a wrong hypothesis for every function starting with $b'$, in particular for $\psi_j$. Since $\bar v \in \{0, 1\}$, Step~2 only appends zeros and ones, which is important for showing membership in $V$. This process defines a numbering $\psi \in \mathcal{P}^2$, and by Kleene's fixed-point theorem there is a $j \geq 2$ with $\varphi_j = \psi_j$. For this $j$ there are two cases: \begin{enumerate} \item[Case 1.] Step~1 always succeeds. Then $\psi_j$ is total and $\psi_j \in V_1$. But $S$ outputs wrong hypotheses on infinitely many prefixes of $\psi_j$ (namely every prefix constructed by the process). \item[Case 2.] Step~1 diverges at some iteration, say when the state is $b = ja$ for some $a \in \{0, 1\}^*$. Then $\psi_j$ has the form $ja\uparrow^\infty$. The numbering $\chi$ with $\chi_k = jak0^\infty$ is in $\mathcal{P}^2$, and by Kleene's fixed-point theorem there is a $k\geq 2$ with $\varphi_k = \chi_k = jak0^\infty$. This $jak0^\infty$ is in $V_2$ and has the prefix $ja$. But Step~1 diverged on this prefix, which means there is no $y \geq |ja|$ with $\varphi_{S(ja)}(y)\downarrow$. In other words $S$ hypothesizes a non-total function. \end{enumerate} Thus, in both cases there is a function in $V$ where $S$ does not behave like a TOTAL strategy. This is the desired contradiction. The following locale formalizes this proof sketch.› locale total_cons = fixes s :: partial1 assumes s_in_R1: "s ∈ ℛ" begin definition r_s :: recf where "r_s ≡ SOME r_s. recfn 1 r_s ∧ total r_s ∧ s = (λx. eval r_s [x])" lemma rs_recfn [simp]: "recfn 1 r_s" and rs_total [simp]: "⋀x. eval r_s [x] ↓" and eval_rs: "⋀x. s x = eval r_s [x]" using r_s_def R1_SOME[OF s_in_R1, of r_s] by simp_all text ‹Performing Step~1 means enumerating the domain of $\varphi_{S(b)}$ until a $y \geq |b|$ is found. The next function enumerates all domain values and checks the condition for them.› definition "r_search_enum ≡ Cn 2 r_le [Cn 2 r_length [Id 2 1], Cn 2 r_enumdom [Cn 2 r_s [Id 2 1], Id 2 0]]" lemma r_search_enum_recfn [simp]: "recfn 2 r_search_enum" by (simp add: r_search_enum_def Let_def) abbreviation search_enum :: partial2 where "search_enum x b ≡ eval r_search_enum [x, b]" abbreviation enumdom :: partial2 where "enumdom i y ≡ eval r_enumdom [i, y]" lemma enumdom_empty_domain: assumes "⋀x. φ i x ↑" shows "⋀y. enumdom i y ↑" using assms r_enumdom_empty_domain by (simp add: phi_def) lemma enumdom_nonempty_domain: assumes "φ i x⇩_{0}↓" shows "⋀y. enumdom i y ↓" and "⋀x. φ i x ↓ ⟷ (∃y. enumdom i y ↓= x)" using assms r_enumdom_nonempty_domain phi_def by metis+ text ‹Enumerating the empty domain yields the empty function.› lemma search_enum_empty: fixes b :: nat assumes "s b ↓= i" and "⋀x. φ i x ↑" shows "⋀x. search_enum x b ↑" using assms r_search_enum_def enumdom_empty_domain eval_rs by simp text ‹Enumerating a non-empty domain yields a total function.› lemma search_enum_nonempty: fixes b y0 :: nat assumes "s b ↓= i" and "φ i y⇩_{0}↓" and "e = the (enumdom i x)" shows "search_enum x b ↓= (if e_length b ≤ e then 0 else 1)" proof - let ?e = "λx. the (enumdom i x)" let ?y = "Cn 2 r_enumdom [Cn 2 r_s [Id 2 1], Id 2 0]" have "recfn 2 ?y" using assms(1) by simp moreover have "⋀x. eval ?y [x, b] = enumdom i x" using assms(1,2) eval_rs by auto moreover from this have "⋀x. eval ?y [x, b] ↓" using enumdom_nonempty_domain(1)[OF assms(2)] by simp ultimately have "eval (Cn 2 r_le [Cn 2 r_length [Id 2 1], ?y]) [x, b] ↓= (if e_length b ≤ ?e x then 0 else 1)" by simp then show ?thesis using assms by (simp add: r_search_enum_def) qed text ‹If there is a $y$ as desired, the enumeration will eventually return zero (representing ``true'').› lemma search_enum_nonempty_eq0: fixes b y :: nat assumes "s b ↓= i" and "φ i y ↓" and "y ≥ e_length b" shows "∃x. search_enum x b ↓= 0" proof - obtain x where x: "enumdom i x ↓= y" using enumdom_nonempty_domain(2)[OF assms(2)] assms(2) by auto from assms(2) have "φ i y ↓" by simp with x have "search_enum x b ↓= 0" using search_enum_nonempty[where ?e=y] assms by auto then show ?thesis by auto qed text ‹If there is no $y$ as desired, the enumeration will never return zero.› lemma search_enum_nonempty_neq0: fixes b y0 :: nat assumes "s b ↓= i" and "φ i y⇩_{0}↓" and "¬ (∃y. φ i y ↓ ∧ y ≥ e_length b)" shows "¬ (∃x. search_enum x b ↓= 0)" proof assume "∃x. search_enum x b ↓= 0" then obtain x where x: "search_enum x b ↓= 0" by auto obtain y where y: "enumdom i x ↓= y" using enumdom_nonempty_domain[OF assms(2)] by blast then have "search_enum x b ↓= (if e_length b ≤ y then 0 else 1)" using assms(1-2) search_enum_nonempty by simp with x have "e_length b ≤ y" using option.inject by fastforce moreover have "φ i y ↓" using assms(2) enumdom_nonempty_domain(2) y by blast ultimately show False using assms(3) by force qed text ‹The next function corresponds to Step~1. Given a prefix $b$ it computes a $y \geq |b|$ with $\varphi_{S(b)}(y)\downarrow$ if such a $y$ exists; otherwise it diverges.› definition "r_search ≡ Cn 1 r_enumdom [r_s, Mn 1 r_search_enum]" lemma r_search_recfn [simp]: "recfn 1 r_search" using r_search_def by simp abbreviation search :: partial1 where "search b ≡ eval r_search [b]" text ‹If $\varphi_{S(b)}$ is the empty function, the search process diverges because already the enumeration of the domain diverges.› lemma search_empty: assumes "s b ↓= i" and "⋀x. φ i x ↑" shows "search b ↑" proof - have "⋀x. search_enum x b ↑" using search_enum_empty[OF assms] by simp then have "eval (Mn 1 r_search_enum) [b] ↑" by simp then show "search b ↑" unfolding r_search_def by simp qed text ‹If $\varphi_{S(b)}$ is non-empty, but there is no $y$ with the desired properties, the search process diverges.› lemma search_nonempty_neq0: fixes b y0 :: nat assumes "s b ↓= i" and "φ i y⇩_{0}↓" and "¬ (∃y. φ i y ↓ ∧ y ≥ e_length b)" shows "search b ↑" proof - have "¬ (∃x. search_enum x b ↓= 0)" using assms search_enum_nonempty_neq0 by simp moreover have "recfn 1 (Mn 1 r_search_enum)" by (simp add: assms(1)) ultimately have "eval (Mn 1 r_search_enum) [b] ↑" by simp then show ?thesis using r_search_def by auto qed text ‹If there is a $y$ as desired, the search process will return one such $y$.› lemma search_nonempty_eq0: fixes b y :: nat assumes "s b ↓= i" and "φ i y ↓" and "y ≥ e_length b" shows "search b ↓" and "φ i (the (search b)) ↓" and "the (search b) ≥ e_length b" proof - have "∃x. search_enum x b ↓= 0" using assms search_enum_nonempty_eq0 by simp moreover have "∀x. search_enum x b ↓" using assms search_enum_nonempty by simp moreover have "recfn 1 (Mn 1 r_search_enum)" by simp ultimately have 1: "search_enum (the (eval (Mn 1 r_search_enum) [b])) b ↓= 0" and 2: "eval (Mn 1 r_search_enum) [b] ↓" using eval_Mn_diverg eval_Mn_convergE[of 1 "r_search_enum" "[b]"] by (metis (no_types, lifting) One_nat_def length_Cons list.size(3) option.collapse, metis (no_types, lifting) One_nat_def length_Cons list.size(3)) let ?x = "the (eval (Mn 1 r_search_enum) [b])" have "search b = eval (Cn 1 r_enumdom [r_s, Mn 1 r_search_enum]) [b]" unfolding r_search_def by simp then have 3: "search b = enumdom i ?x" using assms 2 eval_rs by simp then have "the (search b) = the (enumdom i ?x)" (is "?y = _") by simp then have 4: "search_enum ?x b ↓= (if e_length b ≤ ?y then 0 else 1)" using search_enum_nonempty assms by simp from 3 have "φ i ?y ↓" using enumdom_nonempty_domain assms(2) by (metis option.collapse) then show "φ i ?y ↓" using phi_def by simp then show "?y ≥ e_length b" using assms 4 1 option.inject by fastforce show "search b ↓" using 3 assms(2) enumdom_nonempty_domain(1) by auto qed text ‹The converse of the previous lemma states that whenever the search process returns a value it will be one with the desired properties.› lemma search_converg: assumes "s b ↓= i" and "search b ↓" (is "?y ↓") shows "φ i (the ?y) ↓" and "the ?y ≥ e_length b" proof - have "∃y. φ i y ↓" using assms search_empty by meson then have "∃y. y ≥ e_length b ∧ φ i y ↓" using search_nonempty_neq0 assms by meson then obtain y where y: "y ≥ e_length b ∧ φ i y ↓" by auto then have "φ i y ↓" using phi_def by simp then show "φ i (the (search b)) ↓" and "(the (search b)) ≥ e_length b" using y assms search_nonempty_eq0[OF assms(1) ‹φ i y ↓›] by simp_all qed text ‹Likewise, if the search diverges, there is no appropriate $y$.› lemma search_diverg: assumes "s b ↓= i" and "search b ↑" shows "¬ (∃y. φ i y ↓ ∧ y ≥ e_length b)" proof assume "∃y. φ i y ↓ ∧ y ≥ e_length b" then obtain y where y: "φ i y ↓" "y ≥ e_length b" by auto from y(1) have "φ i y ↓" by (simp add: phi_def) with y(2) search_nonempty_eq0 have "search b ↓" using assms by blast with assms(2) show False by simp qed text ‹Step~2 extends the prefix by a block of the shape $0^n\bar v$. The next function constructs such a block for given $n$ and $v$.› definition "r_badblock ≡ let f = Cn 1 r_singleton_encode [r_not]; g = Cn 3 r_cons [r_constn 2 0, Id 3 1] in Pr 1 f g" lemma r_badblock_prim [simp]: "recfn 2 r_badblock" unfolding r_badblock_def by simp lemma r_badblock: "eval r_badblock [n, v] ↓= list_encode (replicate n 0 @ [1 - v])" proof (induction n) case 0 let ?f = "Cn 1 r_singleton_encode [r_not]" have "eval r_badblock [0, v] = eval ?f [v]" unfolding r_badblock_def by simp also have "... = eval r_singleton_encode [the (eval r_not [v])]" by simp also have "... ↓= list_encode [1 - v]" by simp finally show ?case by simp next case (Suc n) let ?g = "Cn 3 r_cons [r_constn 2 0, Id 3 1]" have "recfn 3 ?g" by simp have "eval r_badblock [(Suc n), v] = eval ?g [n, the (eval r_badblock [n , v]), v]" using ‹recfn 3 ?g› Suc by (simp add: r_badblock_def) also have "... = eval ?g [n, list_encode (replicate n 0 @ [1 - v]), v]" using Suc by simp also have "... = eval r_cons [0, list_encode (replicate n 0 @ [1 - v])]" by simp also have "... ↓= e_cons 0 (list_encode (replicate n 0 @ [1 - v]))" by simp also have "... ↓= list_encode (0 # (replicate n 0 @ [1 - v]))" by simp also have "... ↓= list_encode (replicate (Suc n) 0 @ [1 - v])" by simp finally show ?case by simp qed lemma r_badblock_only_01: "e_nth (the (eval r_badblock [n, v])) i ≤ 1" using r_badblock by (simp add: nth_append) lemma r_badblock_last: "e_nth (the (eval r_badblock [n, v])) n = 1 - v" using r_badblock by (simp add: nth_append) text ‹The following function computes the next prefix from the current one. In other words, it performs Steps~1 and~2.› definition "r_next ≡ Cn 1 r_append [Id 1 0, Cn 1 r_badblock [Cn 1 r_sub [r_search, r_length], Cn 1 r_phi [r_s, r_search]]]" lemma r_next_recfn [simp]: "recfn 1 r_next" unfolding r_next_def by simp text ‹The name @{text next} is unavailable, so we go for @{term nxt}.› abbreviation nxt :: partial1 where "nxt b ≡ eval r_next [b]" lemma nxt_diverg: assumes "search b ↑" shows "nxt b ↑" unfolding r_next_def using assms by (simp add: Let_def) lemma nxt_converg: assumes "search b ↓= y" shows "nxt b ↓= e_append b (list_encode (replicate (y - e_length b) 0 @ [1 - the (φ (the (s b)) y)]))" unfolding r_next_def using assms r_badblock search_converg phi_def eval_rs by fastforce lemma nxt_search_diverg: assumes "nxt b ↑" shows "search b ↑" proof (rule ccontr) assume "search b ↓" then obtain y where "search b ↓= y" by auto then show False using nxt_converg assms by simp qed text ‹If Step~1 finds a $y$, the hypothesis $S(b)$ is incorrect for the new prefix.› lemma nxt_wrong_hyp: assumes "nxt b ↓= b'" and "s b ↓= i" shows "∃y<e_length b'. φ i y ↓≠ e_nth b' y" proof - obtain y where y: "search b ↓= y" using assms nxt_diverg by fastforce then have y_len: "y ≥ e_length b" using assms search_converg(2) by fastforce then have b': "b' = (e_append b (list_encode (replicate (y - e_length b) 0 @ [1 - the (φ i y)])))" using y assms nxt_converg by simp then have "e_nth b' y = 1 - the (φ i y)" using y_len e_nth_append_big r_badblock r_badblock_last by auto moreover have "φ i y ↓" using search_converg y y_len assms(2) by fastforce ultimately have "φ i y ↓≠ e_nth b' y" by (metis gr_zeroI less_numeral_extra(4) less_one option.sel zero_less_diff) moreover have "e_length b' = Suc y" using y_len e_length_append b' by auto ultimately show ?thesis by auto qed text ‹If Step~1 diverges, the hypothesis $S(b)$ refers to a non-total function.› lemma nxt_nontotal_hyp: assumes "nxt b ↑" and "s b ↓= i" shows "∃x. φ i x ↑" using nxt_search_diverg[OF assms(1)] search_diverg[OF assms(2)] by auto text ‹The process only ever extends the given prefix.› lemma nxt_stable: assumes "nxt b ↓= b'" shows "∀x<e_length b. e_nth b x = e_nth b' x" proof - obtain y where y: "search b ↓= y" using assms nxt_diverg by fastforce then have "y ≥ e_length b" using search_converg(2) eval_rs rs_total by fastforce show ?thesis proof (rule allI, rule impI) fix x assume "x < e_length b" let ?i = "the (s b)" have b': "b' = (e_append b (list_encode (replicate (y - e_length b) 0 @ [1 - the (φ ?i y)])))" using assms nxt_converg[OF y] by auto then show "e_nth b x = e_nth b' x" using e_nth_append_small ‹x < e_length b› by auto qed qed text ‹The following properties of @{term r_next} will be used to show that some of the constructed functions are in the class $V$.› lemma nxt_append_01: assumes "nxt b ↓= b'" shows "∀x. x ≥ e_length b ∧ x < e_length b' ⟶ e_nth b' x = 0 ∨ e_nth b' x = 1" proof - obtain y where y: "search b ↓= y" using assms nxt_diverg by fastforce let ?i = "the (s b)" have b': "b' = (e_append b (list_encode (replicate (y - e_length b) 0 @ [1 - the (φ ?i y)])))" (is "b' = (e_append b ?z)") using assms y nxt_converg prod_encode_eq by auto show ?thesis proof (rule allI, rule impI) fix x assume x: "e_length b ≤ x ∧ x < e_length b'" then have "e_nth b' x = e_nth ?z (x - e_length b)" using b' e_nth_append_big by blast then show "e_nth b' x = 0 ∨ e_nth b' x = 1" by (metis less_one nat_less_le option.sel r_badblock r_badblock_only_01) qed qed lemma nxt_monotone: assumes "nxt b ↓= b'" shows "e_length b < e_length b'" proof - obtain y where y: "search b ↓= y" using assms nxt_diverg by fastforce let ?i = "the (s b)" have b': "b' = (e_append b (list_encode (replicate (y - e_length b) 0 @ [1 - the (φ ?i y)])))" using assms y nxt_converg prod_encode_eq by auto then show ?thesis using e_length_append by auto qed text ‹The next function computes the prefixes after each iteration of the process @{term r_next} when started with the list $[j]$.› definition r_prefixes :: recf where "r_prefixes ≡ Pr 1 r_singleton_encode (Cn 3 r_next [Id 3 1])" lemma r_prefixes_recfn [simp]: "recfn 2 r_prefixes" unfolding r_prefixes_def by (simp add: Let_def) abbreviation prefixes :: partial2 where "prefixes t j ≡ eval r_prefixes [t, j]" lemma prefixes_at_0: "prefixes 0 j ↓= list_encode [j]" unfolding r_prefixes_def by simp lemma prefixes_at_Suc: assumes "prefixes t j ↓" (is "?b ↓") shows "prefixes (Suc t) j = nxt (the ?b)" using r_prefixes_def assms by auto lemma prefixes_at_Suc': assumes "prefixes t j ↓= b" shows "prefixes (Suc t) j = nxt b" using r_prefixes_def assms by auto lemma prefixes_prod_encode: assumes "prefixes t j ↓" obtains b where "prefixes t j ↓= b" using assms surj_prod_encode by force lemma prefixes_converg_le: assumes "prefixes t j ↓" and "t' ≤ t" shows "prefixes t' j ↓" using r_prefixes_def assms eval_Pr_converg_le[of 1 _ _ "[j]"] by simp lemma prefixes_diverg_add: assumes "prefixes t j ↑" shows "prefixes (t + d) j ↑" using r_prefixes_def assms eval_Pr_diverg_add[of 1 _ _ "[j]"] by simp text ‹Many properties of @{term r_prefixes} can be derived from similar properties of @{term r_next}.› lemma prefixes_length: assumes "prefixes t j ↓= b" shows "e_length b > t" proof (insert assms, induction t arbitrary: b) case 0 then show ?case using prefixes_at_0 prod_encode_eq by auto next case (Suc t) then have "prefixes t j ↓" using prefixes_converg_le Suc_n_not_le_n nat_le_linear by blast then obtain b' where b': "prefixes t j ↓= b'" using prefixes_prod_encode by blast with Suc have "e_length b' > t" by simp have "prefixes (Suc t) j = nxt b'" using b' prefixes_at_Suc' by simp with Suc have "nxt b' ↓= b" by simp then have "e_length b' < e_length b" using nxt_monotone by simp then show ?case using ‹e_length b' > t› by simp qed lemma prefixes_monotone: assumes "prefixes t j ↓= b" and "prefixes (t + d) j ↓= b'" shows "e_length b ≤ e_length b'" proof (insert assms, induction d arbitrary: b') case 0 then show ?case using prod_encode_eq by simp next case (Suc d) moreover have "t + d ≤ t + Suc d" by simp ultimately have "prefixes (t + d) j ↓" using prefixes_converg_le by blast then obtain b'' where b'': "prefixes (t + d) j ↓= b''" using prefixes_prod_encode by blast with Suc have "prefixes (t + Suc d) j = nxt b''" by (simp add: prefixes_at_Suc') with Suc have "nxt b'' ↓= b'" by simp then show ?case using nxt_monotone Suc b'' by fastforce qed lemma prefixes_stable: assumes "prefixes t j ↓= b" and "prefixes (t + d) j ↓= b'" shows "∀x<e_length b. e_nth b x = e_nth b' x" proof (insert assms, induction d arbitrary: b') case 0 then show ?case using prod_encode_eq by simp next case (Suc d) moreover have "t + d ≤ t + Suc d" by simp ultimately have "prefixes (t + d) j ↓" using prefixes_converg_le by blast then obtain b'' where b'': "prefixes (t + d) j ↓= b''" using prefixes_prod_encode by blast with Suc have "prefixes (t + Suc d) j = nxt b''" by (simp add: prefixes_at_Suc') with Suc have b': "nxt b'' ↓= b'" by simp show "∀x<e_length b. e_nth b x = e_nth b' x" proof (rule allI, rule impI) fix x assume x: "x < e_length b" then have "e_nth b x = e_nth b'' x" using Suc b'' by simp moreover have "x ≤ e_length b''" using x prefixes_monotone b'' Suc by fastforce ultimately show "e_nth b x = e_nth b' x" using b'' nxt_stable Suc b' prefixes_monotone x by (metis leD le_neq_implies_less) qed qed lemma prefixes_tl_only_01: assumes "prefixes t j ↓= b" shows "∀x>0. e_nth b x = 0 ∨ e_nth b x = 1" proof (insert assms, induction t arbitrary: b) case 0 then show ?case using prefixes_at_0 prod_encode_eq by auto next case (Suc t) then have "prefixes t j ↓" using prefixes_converg_le Suc_n_not_le_n nat_le_linear by blast then obtain b' where b': "prefixes t j ↓= b'" using prefixes_prod_encode by blast show "∀x>0. e_nth b x = 0 ∨ e_nth b x = 1" proof (rule allI, rule impI) fix x :: nat assume x: "x > 0" show "e_nth b x = 0 ∨ e_nth b x = 1" proof (cases "x < e_length b'") case True then show ?thesis using Suc b' prefixes_at_Suc' nxt_stable x by metis next case False then show ?thesis using Suc.prems b' prefixes_at_Suc' nxt_append_01 by auto qed qed qed lemma prefixes_hd: assumes "prefixes t j ↓= b" shows "e_nth b 0 = j" proof - obtain b' where b': "prefixes 0 j ↓= b'" by (simp add: prefixes_at_0) then have "b' = list_encode [j]" by (simp add: prod_encode_eq prefixes_at_0) then have "e_nth b' 0 = j" by simp then show "e_nth b 0 = j" using assms prefixes_stable[OF b', of t b] prefixes_length[OF b'] by simp qed lemma prefixes_nontotal_hyp: assumes "prefixes t j ↓= b" and "prefixes (Suc t) j ↑" and "s b ↓= i" shows "∃x. φ i x ↑" using nxt_nontotal_hyp[OF _ assms(3)] assms(2) prefixes_at_Suc'[OF assms(1)] by simp text ‹We now consider the two cases from the proof sketch.› abbreviation "case_two j ≡ ∃t. prefixes t j ↑" abbreviation "case_one j ≡ ¬ case_two j" text ‹In Case~2 there is a maximum convergent iteration because iteration 0 converges.› lemma case_two: assumes "case_two j" shows "∃t. (∀t'≤t. prefixes t' j ↓) ∧ (∀t'>t. prefixes t' j ↑)" proof - let ?P = "λt. prefixes t j ↑" define t⇩_{0}where "t⇩_{0}= Least ?P" then have "?P t⇩_{0}" using assms LeastI_ex[of ?P] by simp then have diverg: "?P t" if "t ≥ t⇩_{0}" for t using prefixes_converg_le that by blast from t⇩_{0}_def have converg: "¬ ?P t" if "t < t⇩_{0}" for t using Least_le[of ?P] that not_less by blast have "t⇩_{0}> 0" proof (rule ccontr) assume "¬ 0 < t⇩_{0}" then have "t⇩_{0}= 0" by simp with ‹?P t⇩_{0}› prefixes_at_0 show False by simp qed let ?t = "t⇩_{0}- 1" have "∀t'≤?t. prefixes t' j ↓" using converg ‹0 < t⇩_{0}› by auto moreover have "∀t'>?t. prefixes t' j ↑" using diverg by simp ultimately show ?thesis by auto qed text ‹Having completed the modelling of the process, we can now define the functions $\psi_j$ it computes. The value $\psi_j(x)$ is computed by running @{term r_prefixes} until the prefix is longer than $x$ and then taking the $x$-th element of the prefix.› definition "r_psi ≡ let f = Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_prefixes [Id 3 0, Id 3 1]]] in Cn 2 r_nth [Cn 2 r_prefixes [Mn 2 f, Id 2 0], Id 2 1]" lemma r_psi_recfn: "recfn 2 r_psi" unfolding r_psi_def by simp abbreviation psi :: partial2 ("ψ") where "ψ j x ≡ eval r_psi [j, x]" lemma psi_in_P2: "ψ ∈ 𝒫⇧^{2}" using r_psi_recfn by auto text ‹The values of @{term "ψ"} can be read off the prefixes.› lemma psi_eq_nth_prefix: assumes "prefixes t j ↓= b" and "e_length b > x" shows "ψ j x ↓= e_nth b x" proof - let ?f = "Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_prefixes [Id 3 0, Id 3 1]]]" let ?P = "λt. prefixes t j ↓ ∧ e_length (the (prefixes t j)) > x" from assms have ex_t: "∃t. ?P t" by auto define t⇩_{0}where "t⇩_{0}= Least ?P" then have "?P t⇩_{0}" using LeastI_ex[OF ex_t] by simp from ex_t have not_P: "¬ ?P t" if "t < t⇩_{0}" for t using ex_t that Least_le[of ?P] not_le t⇩_{0}_def by auto have "?P t" using assms by simp with not_P have "t⇩_{0}≤ t" using leI by blast then obtain b⇩_{0}where b0: "prefixes t⇩_{0}j ↓= b⇩_{0}" using assms(1) prefixes_converg_le by blast have "eval ?f [t⇩_{0}, j, x] ↓= 0" proof - have "eval (Cn 3 r_prefixes [Id 3 0, Id 3 1]) [t⇩_{0}, j, x] ↓= b⇩_{0}" using b0 by simp then show ?thesis using ‹?P t⇩_{0}› by simp qed moreover have "eval ?f [t, j, x] ↓≠ 0" if "t < t⇩_{0}" for t proof - obtain bt where bt: "prefixes t j ↓= bt" using prefixes_converg_le[of t⇩_{0}j t] b0 ‹t < t⇩_{0}› by auto moreover have "¬ ?P t" using that not_P by simp ultimately have "e_length bt ≤ x" by simp moreover have "eval (Cn 3 r_prefixes [Id 3 0, Id 3 1]) [t, j, x] ↓= bt" using bt by simp ultimately show ?thesis by simp qed ultimately have "eval (Mn 2 ?f) [j, x] ↓= t⇩_{0}" using eval_Mn_convergI[of 2 ?f "[j, x]" t⇩_{0}] by simp then have "ψ j x ↓= e_nth b⇩_{0}x" unfolding r_psi_def using b0 by simp then show ?thesis using ‹t⇩_{0}≤ t› assms(1) prefixes_stable[of t⇩_{0}j b⇩_{0}"t - t⇩_{0}" b] b0 ‹?P t⇩_{0}› by simp qed lemma psi_converg_imp_prefix: assumes "ψ j x ↓" shows "∃t b. prefixes t j ↓= b ∧ e_length b > x" proof - let ?f = "Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_prefixes [Id 3 0, Id 3 1]]]" have "eval (Mn 2 ?f) [j, x] ↓" proof (rule ccontr) assume "¬ eval (Mn 2 ?f) [j, x] ↓" then have "eval (Mn 2 ?f) [j, x] ↑" by simp then have "ψ j x ↑" unfolding r_psi_def by simp then show False using assms by simp qed then obtain t where t: "eval (Mn 2 ?f) [j, x] ↓= t" by blast have "recfn 2 (Mn 2 ?f)" by simp then have f_zero: "eval ?f [t, j, x] ↓= 0" using eval_Mn_convergE[OF _ t] by (metis (no_types, lifting) One_nat_def Suc_1 length_Cons list.size(3)) have "prefixes t j ↓" proof (rule ccontr) assume "¬ prefixes t j ↓" then have "prefixes t j ↑" by simp then have "eval ?f [t, j, x] ↑" by simp with f_zero show False by simp qed then obtain b' where b': "prefixes t j ↓= b'" by auto moreover have "e_length b' > x" proof (rule ccontr) assume "¬ e_length b' > x" then have "eval ?f [t, j, x] ↓= 1" using b' by simp with f_zero show False by simp qed ultimately show ?thesis by auto qed lemma psi_converg_imp_prefix': assumes "ψ j x ↓" shows "∃t b. prefixes t j ↓= b ∧ e_length b > x ∧ ψ j x ↓= e_nth b x" using psi_converg_imp_prefix[OF assms] psi_eq_nth_prefix by blast text ‹In both Case~1 and~2, $\psi_j$ starts with $j$.› lemma psi_at_0: "ψ j 0 ↓= j" using prefixes_hd prefixes_length psi_eq_nth_prefix prefixes_at_0 by fastforce text ‹In Case~1, $\psi_j$ is total and made up of $j$ followed by zeros and ones, just as required by the definition of $V_1$.› lemma case_one_psi_total: assumes "case_one j" and "x > 0" shows "ψ j x ↓= 0 ∨ ψ j x ↓= 1" proof - obtain b where b: "prefixes x j ↓= b" using assms(1) by auto then have "e_length b > x" using prefixes_length by simp then have "ψ j x ↓= e_nth b x" using b psi_eq_nth_prefix by simp moreover have "e_nth b x = 0 ∨ e_nth b x = 1" using prefixes_tl_only_01[OF b] assms(2) by simp ultimately show "ψ j x ↓= 0 ∨ ψ j x ↓= 1" by simp qed text ‹In Case~2, $\psi_j$ is defined only for a prefix starting with $j$ and continuing with zeros and ones. This prefix corresponds to $ja$ from the definition of $V_2$.› lemma case_two_psi_only_prefix: assumes "case_two j" shows "∃y. (∀x. 0 < x ∧ x < y ⟶ ψ j x ↓= 0 ∨ ψ j x ↓= 1) ∧ (∀x ≥ y. ψ j x ↑)" proof - obtain t where t_le: "∀t'≤t. prefixes t' j ↓" and t_gr: "∀t'>t. prefixes t' j ↑" using assms case_two by blast then obtain b where b: "prefixes t j ↓= b" by auto let ?y = "e_length b" have "ψ j x ↓= 0 ∨ ψ j x ↓= 1" if "x > 0 ∧ x < ?y" for x using t_le b that by (metis prefixes_tl_only_01 psi_eq_nth_prefix) moreover have "ψ j x ↑" if "x ≥ ?y" for x proof (rule ccontr) assume "ψ j x ↓" then obtain t' b' where t': "prefixes t' j ↓= b'" and "e_length b' > x" using psi_converg_imp_prefix by blast then have "e_length b' > ?y" using that by simp with t' have "t' > t" using prefixes_monotone b by (metis add_diff_inverse_nat leD) with t' t_gr show False by simp qed ultimately show ?thesis by auto qed definition longest_prefix :: "nat ⇒ nat" where "longest_prefix j ≡ THE y. (∀x<y. ψ j x ↓) ∧ (∀x≥y. ψ j x ↑)" lemma longest_prefix: assumes "case_two j" and "z = longest_prefix j" shows "(∀x<z. ψ j x ↓) ∧ (∀x≥z. ψ j x ↑)" proof - let ?P = "λz. (∀x<z. ψ j x ↓) ∧ (∀x≥z. ψ j x ↑)" obtain y where y: "∀x. 0 < x ∧ x < y ⟶ ψ j x ↓= 0 ∨ ψ j x ↓= 1" "∀x≥y. ψ j x ↑" using case_two_psi_only_prefix[OF assms(1)] by auto have "?P (THE z. ?P z)" proof (rule theI[of ?P y]) show "?P y" proof show "∀x<y. ψ j x ↓" proof (rule allI, rule impI) fix x assume "x < y" show "ψ j x ↓" proof (cases "x = 0") case True then show ?thesis using psi_at_0 by simp next case False then show ?thesis using y(1) ‹x < y› by auto qed qed show "∀x≥y. ψ j x ↑" using y(2) by simp qed show "z = y" if "?P z" for z proof (rule ccontr, cases "z < y") case True moreover assume "z ≠ y" ultimately show False using that ‹?P y› by auto next case False moreover assume "z ≠ y" then show False using that ‹?P y› y(2) by (meson linorder_cases order_refl) qed qed then have "(∀x<(THE z. ?P z). ψ j x ↓) ∧ (∀x≥(THE z. ?P z). ψ j x ↑)" by blast moreover have "longest_prefix j = (THE z. ?P z)" unfolding longest_prefix_def by simp ultimately show ?thesis using assms(2) by metis qed lemma case_two_psi_longest_prefix: assumes "case_two j" and "y = longest_prefix j" shows "(∀x. 0 < x ∧ x < y ⟶ ψ j x ↓= 0 ∨ ψ j x ↓= 1) ∧ (∀x ≥ y. ψ j x ↑)" using assms longest_prefix case_two_psi_only_prefix by (metis prefixes_tl_only_01 psi_converg_imp_prefix') text ‹The prefix cannot be empty because the process starts with prefix $[j]$.› lemma longest_prefix_gr_0: assumes "case_two j" shows "longest_prefix j > 0" using assms case_two_psi_longest_prefix psi_at_0 by force lemma psi_not_divergent_init: assumes "prefixes t j ↓= b" shows "(ψ j) ▹ (e_length b - 1) = b" proof (intro initI) show "0 < e_length b" using assms prefixes_length by fastforce show "ψ j x ↓= e_nth b x" if "x < e_length b" for x using that assms psi_eq_nth_prefix by simp qed text ‹In Case~2, the strategy $S$ outputs a non-total hypothesis on some prefix of $\psi_j$.› lemma case_two_nontotal_hyp: assumes "case_two j" shows "∃n<longest_prefix j. ¬ total1 (φ (the (s ((ψ j) ▹ n))))" proof - obtain t where "∀t'≤t. prefixes t' j ↓" and t_gr: "∀t'>t. prefixes t' j ↑" using assms case_two by blast then obtain b where b: "prefixes t j ↓= b" by auto moreover obtain i where i: "s b ↓= i" using eval_rs by fastforce moreover have div: "prefixes (Suc t) j ↑" using t_gr by simp ultimately have "∃x. φ i x ↑" using prefixes_nontotal_hyp by simp then obtain x where "φ i x ↑" by auto moreover have init: "ψ j ▹ (e_length b - 1) = b" (is "_ ▹ ?n = b") using psi_not_divergent_init[OF b] by simp ultimately have "φ (the (s (ψ j ▹ ?n))) x ↑" using i by simp then have "¬ total1 (φ (the (s (ψ j ▹ ?n))))" by auto moreover have "?n < longest_prefix j" using case_two_psi_longest_prefix init b div psi_eq_nth_prefix by (metis length_init lessI not_le_imp_less option.simps(3)) ultimately show ?thesis by auto qed text ‹Consequently, in Case~2 the strategy does not TOTAL-learn any function starting with the longest prefix of $\psi_j$.› lemma case_two_not_learn: assumes "case_two j" and "f ∈ ℛ" and "⋀x. x < longest_prefix j ⟹ f x = ψ j x" shows "¬ learn_total φ {f} s" proof - obtain n where n: "n < longest_prefix j" "¬ total1 (φ (the (s (ψ j ▹ n))))" using case_two_nontotal_hyp[OF assms(1)] by auto have "f ▹ n = ψ j ▹ n" using assms(3) n(1) by (intro init_eqI) auto with n(2) show ?thesis by (metis R1_imp_total1 learn_totalE(3) singletonI) qed text ‹In Case~1 the strategy outputs a wrong hypothesis on infinitely many prefixes of $\psi_j$ and thus does not learn $\psi_j$ in the limit, much less in the sense of TOTAL.› lemma case_one_wrong_hyp: assumes "case_one j" shows "∃n>k. φ (the (s ((ψ j) ▹ n))) ≠ ψ j" proof - have all_t: "∀t. prefixes t j ↓" using assms by simp then obtain b where b: "prefixes (Suc k) j ↓= b" by auto then have length: "e_length b > Suc k" using prefixes_length by simp then have init: "ψ j ▹ (e_length b - 1) = b" using psi_not_divergent_init b by simp obtain i where i: "s b ↓= i" using eval_rs by fastforce from all_t obtain b' where b': "prefixes (Suc (Suc k)) j ↓= b'" by auto then have "ψ j ▹ (e_length b' - 1) = b'" using psi_not_divergent_init by simp moreover have "∃y<e_length b'. φ i y ↓≠ e_nth b' y" using nxt_wrong_hyp b b' i prefixes_at_Suc by auto ultimately have "∃y<e_length b'. φ i y ≠ ψ j y" using b' psi_eq_nth_prefix by auto then have "φ i ≠ ψ j" by auto then show ?thesis using init length i by (metis Suc_less_eq length_init option.sel) qed lemma case_one_not_learn: assumes "case_one j" shows "¬ learn_lim φ {ψ j} s" proof (rule infinite_hyp_wrong_not_Lim[of "ψ j"]) show "ψ j ∈ {ψ j}" by simp show "∀n. ∃m>n. φ (the (s (ψ j ▹ m))) ≠ ψ j" using case_one_wrong_hyp[OF assms] by simp qed lemma case_one_not_learn_V: assumes "case_one j" and "j ≥ 2" and "φ j = ψ j" shows "¬ learn_lim φ V_constotal s" proof - have "ψ j ∈ V_constotal_1" proof - define p where "p = (λx. (ψ j) (x + 1))" have "p ∈ ℛ⇩_{0}⇩_{1}" proof - from p_def have "p ∈ 𝒫" using skip_P1[of "ψ j" 1] psi_in_P2 P2_proj_P1 by blast moreover have "p x ↓= 0 ∨ p x ↓= 1" for x using p_def assms(1) case_one_psi_total by auto moreover from this have "total1 p" by fast ultimately show ?thesis using RPred1_def by auto qed moreover have "ψ j = [j] ⊙ p" by (intro prepend_eqI, simp add: psi_at_0, simp add: p_def) ultimately show ?thesis using assms(2,3) V_constotal_1_def by blast qed then have "ψ j ∈ V_constotal" using V_constotal_def by auto moreover have "¬ learn_lim φ {ψ j} s" using case_one_not_learn assms(1) by simp ultimately show ?thesis using learn_lim_closed_subseteq by auto qed text ‹The next lemma embodies the construction of $\chi$ followed by the application of Kleene's fixed-point theorem as described in the proof sketch.› lemma goedel_after_prefixes: fixes vs :: "nat list" and m :: nat shows "∃n≥m. φ n = vs @ [n] ⊙ 0⇧^{∞}" proof - define f :: partial1 where "f ≡ vs ⊙ 0⇧^{∞}" then have "f ∈ ℛ" using almost0_in_R1 by auto then obtain n where n: "n ≥ m" "φ n = (λx. if x = length vs then Some n else f x)" using goedel_at[of f m "length vs"] by auto moreover have "φ n x = (vs @ [n] ⊙ 0⇧^{∞}) x" for x proof - consider "x < length vs" | "x = length vs" | "x > length vs" by linarith then show ?thesis using n f_def by (cases) (auto simp add: prepend_associative) qed ultimately show ?thesis by blast qed text ‹If Case~2 holds for a $j\geq 2$ with $\varphi_j = \psi_j$, that is, if $\psi_j\in V_1$, then there is a function in $V$, namely $\psi_j$, on which $S$ fails. Therefore $S$ does not learn $V$.› lemma case_two_not_learn_V: assumes "case_two j" and "j ≥ 2" and "φ j = ψ j" shows "¬ learn_total φ V_constotal s" proof - define z where "z = longest_prefix j" then have "z > 0" using longest_prefix_gr_0[OF assms(1)] by simp define vs where "vs = prefix (ψ j) (z - 1)" then have "vs ! 0 = j" using psi_at_0 ‹z > 0› by simp define a where "a = tl vs" then have vs: "vs = j # a" using vs_def ‹vs ! 0 = j› by (metis length_Suc_conv length_prefix list.sel(3) nth_Cons_0) obtain k where k: "k ≥ 2" and phi_k: "φ k = j # a @ [k] ⊙ 0⇧^{∞}" using goedel_after_prefixes[of 2 "j # a"] by auto have phi_j: "φ j = j # a ⊙ ↑⇧^{∞}" proof (rule prepend_eqI) show "⋀x. x < length (j # a) ⟹ φ j x ↓= (j # a) ! x" using assms(1,3) vs vs_def ‹0 < z› length_prefix[of "ψ j" "z - 1"] prefix_nth[of _ _ "ψ j"] psi_at_0[of j] case_two_psi_longest_prefix[OF _ z_def] longest_prefix[OF _ z_def] by (metis One_nat_def Suc_pred option.collapse) show "⋀x. φ j (length (j # a) + x) ↑" using assms(3) vs_def by (simp add: vs assms(1) case_two_psi_longest_prefix z_def) qed moreover have "φ k ∈ V_constotal_2" proof (intro V_constotal_2I[of _ j a k]) show "φ k = j # a @ [k] ⊙ 0⇧^{∞}" using phi_k . show "2 ≤ j" using ‹2 ≤ j› . show "2 ≤ k" using ‹2 ≤ k› . show "∀i<length a. a ! i ≤ 1" proof (rule allI, rule impI) fix i assume i: "i < length a" then have "Suc i < z" using z_def vs_def length_prefix ‹0 < z› vs by (metis One_nat_def Suc_mono Suc_pred length_Cons) have "a ! i = vs ! (Suc i)" using vs by simp also have "... = the (ψ j (Suc i))" using vs_def vs i length_Cons length_prefix prefix_nth by (metis Suc_mono) finally show "a ! i ≤ 1" using case_two_psi_longest_prefix ‹Suc i < z› z_def by (metis assms(1) less_or_eq_imp_le not_le_imp_less not_one_less_zero option.sel zero_less_Suc) qed qed (auto simp add: phi_j) then have "φ k ∈ V_constotal" using V_constotal_def by auto moreover have "¬ learn_total φ {φ k} s" proof - have "φ k ∈ ℛ" by (simp add: phi_k almost0_in_R1) moreover have "⋀x. x < longest_prefix j ⟹ φ k x = ψ j x" using phi_k vs_def z_def length_prefix phi_j prepend_associative prepend_at_less by (metis One_nat_def Suc_pred ‹0 < z› ‹vs = j # a› append_Cons assms(3)) ultimately show ?thesis using case_two_not_learn[OF assms(1)] by simp qed ultimately show "¬ learn_total φ V_constotal s" using learn_total_closed_subseteq by auto qed text ‹The strategy $S$ does not learn $V$ in either case.› lemma not_learn_total_V: "¬ learn_total φ V_constotal s" proof - obtain j where "j ≥ 2" "φ j = ψ j" using kleene_fixed_point psi_in_P2 by auto then show ?thesis using case_one_not_learn_V learn_total_def case_two_not_learn_V by (cases "case_two j") auto qed end lemma V_not_in_TOTAL: "V_constotal ∉ TOTAL" proof (rule ccontr) assume "¬ V_constotal ∉ TOTAL" then have "V_constotal ∈ TOTAL" by simp then have "V_constotal ∈ TOTAL_wrt φ" by (simp add: TOTAL_wrt_phi_eq_TOTAL) then obtain s where "learn_total φ V_constotal s" using TOTAL_wrt_def by auto then obtain s' where s': "s' ∈ ℛ" "learn_total φ V_constotal s'" using lemma_R_for_TOTAL_simple by blast then interpret total_cons s' by (simp add: total_cons_def) have "¬ learn_total φ V_constotal s'" by (simp add: not_learn_total_V) with s'(2) show False by simp qed lemma TOTAL_neq_CONS: "TOTAL ≠ CONS" using V_not_in_TOTAL V_in_CONS CONS_def by auto text ‹The main result of this section:› theorem TOTAL_subset_CONS: "TOTAL ⊂ CONS" using TOTAL_subseteq_CONS TOTAL_neq_CONS by simp end