Theory TOTAL_CONS
section ‹TOTAL is a proper subset of CONS\label{s:total_cons}›
theory TOTAL_CONS
imports Lemma_R
CP_FIN_NUM
CONS_LIM
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