# Theory LIM_BC

section ‹LIM is a proper subset of BC\label{s:lim_bc}›

theory LIM_BC
imports Lemma_R
begin

text ‹The proper inclusion of LIM in BC has been proved by
Barzdin~\<^cite>‹"b-ttlsf-74"› (see also Case and Smith~\<^cite>‹"cs-cicmii-83"›). The
proof constructs a class $V \in \mathrm{BC} - \mathrm{LIM}$ by
diagonalization against all LIM strategies. Exploiting Lemma~R for LIM, we
can assume that all such strategies are total functions. From the effective
version of this lemma we derive a numbering @{term "σ ∈
ℛ⇧2"} such that for all $U \in \mathrm{LIM}$ there is an $i$ with
$U\in \mathrm{LIM}_\varphi(\sigma_i)$. The idea behind $V$
is for every $i$ to construct a class $V_i$ of cardinality one or two such
that $V_i \notin \mathrm{LIM}_\varphi(\sigma_i)$. It then follows that the
union $V := \bigcup_i V_i$ cannot be learned by any $\sigma_i$ and thus $V \notin \mathrm{LIM}$. At the same time, the construction ensures that the
functions in $V$ are predictable enough'' to be learnable in the BC sense.

At the core is a process that maintains a state $(b, k)$ of a list $b$ of
numbers and an index $k < |b|$ into this list. We imagine $b$ to be the
prefix of the function being constructed, except for position $k$ where
we imagine $b$ to have a gap''; that is, $b_k$ is not defined yet.
Technically, we will always have $b_k = 0$, so $b$ also represents the prefix
after the gap is filled'' with 0, whereas $b_{k:=1}$ represents the prefix
where the gap is filled with 1. For every $i \in \mathbb{N}$, the process
starts in state $(i0, 1)$ and computes the next state from a given state
$(b,k)$ as follows:
\begin{enumerate}
\item if $\sigma_i(b_{<k}) \neq \sigma_i(b)$ then the next state is $(b0, |b|)$,
\item else if $\sigma_i(b_{<k}) \neq \sigma_i(b_{k:=1})$ then the next state is $(b_{k:=1}0, |b|)$,
\item else the next state is $(b0, k)$.
\end{enumerate}
In other words, if $\sigma_i$ changes its hypothesis when the gap in $b$ is
filled with 0 or 1, then the process fills the gap with 0 or 1, respectively, and
appends a gap to $b$. If, however, a hypothesis change cannot be enforced at
this point, the process appends a 0 to $b$ and leaves the gap alone. Now there
are two cases:
\begin{itemize}
\item[Case 1.] Every gap gets filled eventually. Then the process generates
increasing prefixes of a total function $\tau_i$, on which $\sigma_i$ changes
its hypothesis infinitely often. We set $V_i := \{\tau_i\}$, and have $V_i \notin \mathrm{LIM}_\varphi(\sigma_i)$.
\item[Case 2.] Some gap never gets filled. That means a state $(b, k)$ is
reached such that $\sigma_i(b0^t) = \sigma_i(b_{k:=1}0^t) = \sigma_i(b_{<k})$
for all $t$. Then the process describes a function $\tau_i = b_{<k}\uparrow0^\infty$,
where the value at the gap $k$ is undefined.
Replacing the value at $k$ by 0 and 1 yields two functions
$\tau_i^{(0)} = b0^\infty$ and $\tau_i^{(1)} = b_{k:=1}0^\infty$, which differ only at $k$ and on
which $\sigma_i$ converges to the same hypothesis. Thus $\sigma_i$ does not learn the
class $V_i := \{\tau_i^{(0)}, \tau_i^{(1)}\}$ in the limit.
\end{itemize}
Both cases combined imply $V \notin \mathrm{LIM}$.

A BC strategy $S$ for $V = \bigcup_i V_i$ works as follows. Let $f\in V$. On input $f^n$ the
strategy outputs a Gödel number of the function
$g_n(x) = \left\{\begin{array}{ll} f(x) & \mbox{if } x \leq n,\\ \tau_{f(0)}(x) & \mbox{otherwise}. \end{array}\right.$
By definition of $V$, $f$ is generated by the process running for $i = f(0)$.
If $f(0)$ leads to Case~1 then $f = \tau_{f(0)}$, and
$g_n$ equals $f$ for all $n$. If $f(0)$ leads to Case~2 with
a forever unfilled gap at $k$, then
$g_n$ will be equal to the correct one of $\tau_i^{(0)}$ or $\tau_i^{(1)}$ for all $n \geq k$. Intuitively, the prefix received by $S$ eventually grows long enough to
reveal the value $f(k)$.
In both cases $S$ converges to $f$, but it outputs a different Gödel number
for every $f^n$ because $g_n$ contains the hard-coded'' values
$f(0),\dots,f(n)$. Therefore $S$ is a BC strategy but not a LIM
strategy for $V$.›

subsection ‹Enumerating enough total strategies›

text ‹For the construction of $\sigma$ we need the function @{term
r_limr} from the effective version of Lemma~R for LIM.›

definition "r_sigma ≡ Cn 2 r_phi [Cn 2 r_limr [Id 2 0], Id 2 1]"

lemma r_sigma_recfn: "recfn 2 r_sigma"
unfolding r_sigma_def using r_limr_recfn by simp

lemma r_sigma: "eval r_sigma [i, x] = φ (the (eval r_limr [i])) x"
unfolding r_sigma_def phi_def using r_sigma_recfn r_limr_total r_limr_recfn
by simp

lemma r_sigma_total: "total r_sigma"
using r_sigma r_limr r_sigma_recfn totalI2[of r_sigma] by simp

abbreviation sigma :: partial2 ("σ") where
"σ i x ≡ eval r_sigma [i, x]"

lemma sigma: "σ i = φ (the (eval r_limr [i]))"
using r_sigma by simp

text ‹The numbering @{term σ} does indeed enumerate enough total
strategies for every LIM learning problem.›

lemma learn_lim_sigma:
assumes "learn_lim ψ U (φ i)"
shows "learn_lim ψ U (σ i)"
using assms sigma r_limr by simp

subsection ‹The diagonalization process›

text ‹The following function represents the process described above. It
computes the next state from a given state $(b, k)$.›

definition "r_next ≡
Cn 1 r_ifeq
[Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], r_pdec1],
Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_take [r_pdec2, r_pdec1]],
Cn 1 r_ifeq
[Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_update [r_pdec1, r_pdec2, r_const 1]],
Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_take [r_pdec2, r_pdec1]],
Cn 1 r_prod_encode [Cn 1 r_snoc [r_pdec1, Z], r_pdec2],
Cn 1 r_prod_encode
[Cn 1 r_snoc
[Cn 1 r_update [r_pdec1, r_pdec2, r_const 1], Z], Cn 1 r_length [r_pdec1]]],
Cn 1 r_prod_encode [Cn 1 r_snoc [r_pdec1, Z], Cn 1 r_length [r_pdec1]]]"

lemma r_next_recfn: "recfn 1 r_next"
unfolding r_next_def using r_sigma_recfn by simp

text ‹The three conditions distinguished in @{term r_next} correspond
to Steps 1, 2, and 3 of the process: hypothesis change when the gap is
filled with 0; hypothesis change when the gap is filled with 1; or
no hypothesis change either way.›

abbreviation "change_on_0 b k ≡ σ (e_hd b) b ≠ σ (e_hd b) (e_take k b)"

abbreviation "change_on_1 b k ≡
σ (e_hd b) b = σ (e_hd b) (e_take k b) ∧
σ (e_hd b) (e_update b k 1) ≠ σ (e_hd b) (e_take k b)"

abbreviation "change_on_neither b k ≡
σ (e_hd b) b = σ (e_hd b) (e_take k b) ∧
σ (e_hd b) (e_update b k 1) = σ (e_hd b) (e_take k b)"

lemma change_conditions:
obtains
(on_0) "change_on_0 b k"
| (on_1) "change_on_1 b k"
| (neither) "change_on_neither b k"
by auto

lemma r_next:
assumes "arg = prod_encode (b, k)"
shows "change_on_0 b k ⟹ eval r_next [arg] ↓= prod_encode (e_snoc b 0, e_length b)"
and "change_on_1 b k ⟹
eval r_next [arg] ↓= prod_encode (e_snoc (e_update b k 1) 0, e_length b)"
and "change_on_neither b k ⟹ eval r_next [arg] ↓= prod_encode (e_snoc b 0, k)"
proof -
let ?bhd = "Cn 1 r_hd [r_pdec1]"
let ?bup = "Cn 1 r_update [r_pdec1, r_pdec2, r_const 1]"
let ?bk = "Cn 1 r_take [r_pdec2, r_pdec1]"
let ?bap = "Cn 1 r_snoc [r_pdec1, Z]"
let ?len = "Cn 1 r_length [r_pdec1]"
let ?thenthen = "Cn 1 r_prod_encode [?bap, r_pdec2]"
let ?thenelse = "Cn 1 r_prod_encode [Cn 1 r_snoc [?bup, Z], ?len]"
let ?else = "Cn 1 r_prod_encode [?bap, ?len]"
have bhd: "eval ?bhd [arg] ↓= e_hd b"
using assms by simp
have bup: "eval ?bup [arg] ↓= e_update b k 1"
using assms by simp
have bk: "eval ?bk [arg] ↓= e_take k b"
using assms by simp
have bap: "eval ?bap [arg] ↓= e_snoc b 0"
using assms by simp
have len: "eval ?len [arg] ↓= e_length b"
using assms by simp
have else_: "eval ?else [arg] ↓= prod_encode (e_snoc b 0, e_length b)"
using bap len by simp
have thenthen: "eval ?thenthen [arg] ↓= prod_encode (e_snoc b 0, k)"
using bap assms by simp
have thenelse: "eval ?thenelse [arg] ↓= prod_encode (e_snoc (e_update b k 1) 0, e_length b)"
using bup len by simp
have then_:
"eval
(Cn 1 r_ifeq [Cn 1 r_sigma [?bhd, ?bup], Cn 1 r_sigma [?bhd, ?bk], ?thenthen, ?thenelse])
[arg] ↓=
(if the (σ (e_hd b) (e_update b k 1)) = the (σ (e_hd b) (e_take k b))
then prod_encode (e_snoc b 0, k)
else prod_encode (e_snoc (e_update b k 1) 0, e_length b))"
(is "eval ?then [arg] ↓= ?then_eval")
using bhd bup bk thenthen thenelse r_sigma r_sigma_recfn r_limr R1_imp_total1 by simp
have *: "eval r_next [arg] ↓=
(if the (σ (e_hd b) b) = the (σ (e_hd b) (e_take k b))
then ?then_eval
else prod_encode (e_snoc b 0, e_length b))"
unfolding r_next_def
using bhd bk then_ else_ r_sigma r_sigma_recfn r_limr R1_imp_total1 assms
by simp
have r_sigma_neq: "eval r_sigma [x⇩1, y⇩1] ≠ eval r_sigma [x⇩2, y⇩2] ⟷
the (eval r_sigma [x⇩1, y⇩1]) ≠ the (eval r_sigma [x⇩2, y⇩2])"
for x⇩1 y⇩1 x⇩2 y⇩2
using r_sigma r_limr totalE[OF r_sigma_total r_sigma_recfn] r_sigma_recfn r_sigma_total
by (metis One_nat_def Suc_1 length_Cons list.size(3) option.expand)
{
assume "change_on_0 b k"
then show "eval r_next [arg] ↓= prod_encode (e_snoc b 0, e_length b)"
using * r_sigma_neq by simp
next
assume "change_on_1 b k"
then show "eval r_next [arg] ↓= prod_encode (e_snoc (e_update b k 1) 0, e_length b)"
using * r_sigma_neq by simp
next
assume "change_on_neither b k"
then show "eval r_next [arg] ↓= prod_encode (e_snoc b 0, k)"
using * r_sigma_neq by simp
}
qed

lemma r_next_total: "total r_next"
proof (rule totalI1)
show "recfn 1 r_next"
using r_next_recfn by simp
show "eval r_next [x] ↓" for x
proof -
obtain b k where "x = prod_encode (b, k)"
using prod_encode_pdec'[of x] by metis
then show ?thesis using r_next by fast
qed
qed

text ‹The next function computes the state of the process after
any number of iterations.›

definition "r_state ≡
Pr 1
(Cn 1 r_prod_encode [Cn 1 r_snoc [Cn 1 r_singleton_encode [Id 1 0], Z], r_const 1])
(Cn 3 r_next [Id 3 1])"

lemma r_state_recfn: "recfn 2 r_state"
unfolding r_state_def using r_next_recfn by simp

lemma r_state_at_0: "eval r_state [0, i] ↓= prod_encode (list_encode [i, 0], 1)"
proof -
let ?f = "Cn 1 r_prod_encode [Cn 1 r_snoc [Cn 1 r_singleton_encode [Id 1 0], Z], r_const 1]"
have "eval r_state [0, i] = eval ?f [i]"
unfolding r_state_def using r_next_recfn by simp
also have "... ↓= prod_encode (list_encode [i, 0], 1)"
by (simp add: list_decode_singleton)
finally show ?thesis .
qed

lemma r_state_total: "total r_state"
unfolding r_state_def
using r_next_recfn totalE[OF r_next_total r_next_recfn] totalI3[of "Cn 3 r_next [Id 3 1]"]
by (intro Pr_total) auto

text ‹We call the components of a state $(b, k)$ the \emph{block} $b$
and the \emph{gap} $k$.›

definition block :: "nat ⇒ nat ⇒ nat" where
"block i t ≡ pdec1 (the (eval r_state [t, i]))"

definition gap :: "nat ⇒ nat ⇒ nat" where
"gap i t ≡ pdec2 (the (eval r_state [t, i]))"

lemma state_at_0:
"block i 0 = list_encode [i, 0]"
"gap i 0 = 1"
unfolding block_def gap_def r_state_at_0 by simp_all

text ‹Some lemmas describing the behavior of blocks and gaps in
one iteration of the process:›

lemma state_Suc:
assumes "b = block i t" and "k = gap i t"
shows "block i (Suc t) = pdec1 (the (eval r_next [prod_encode (b, k)]))"
and "gap i (Suc t) = pdec2 (the (eval r_next [prod_encode (b, k)]))"
proof -
have "eval r_state [Suc t, i] =
eval (Cn 3 r_next [Id 3 1]) [t, the (eval r_state [t, i]), i]"
using r_state_recfn r_next_recfn totalE[OF r_state_total r_state_recfn, of "[t, i]"]
by (simp add: r_state_def)
also have "... = eval r_next [the (eval r_state [t, i])]"
using r_next_recfn by simp
also have "... = eval r_next [prod_encode (b, k)]"
using assms block_def gap_def by simp
finally have "eval r_state [Suc t, i] = eval r_next [prod_encode (b, k)]" .
then show
"block i (Suc t) = pdec1 (the (eval r_next [prod_encode (b, k)]))"
"gap i (Suc t) = pdec2 (the (eval r_next [prod_encode (b, k)]))"
by (simp add: block_def, simp add: gap_def)
qed

lemma gap_Suc:
assumes "b = block i t" and "k = gap i t"
shows "change_on_0 b k ⟹ gap i (Suc t) = e_length b"
and "change_on_1 b k ⟹ gap i (Suc t) = e_length b"
and "change_on_neither b k⟹ gap i (Suc t) = k"
using assms r_next state_Suc by simp_all

lemma block_Suc:
assumes "b = block i t" and "k = gap i t"
shows "change_on_0 b k ⟹ block i (Suc t) = e_snoc b 0"
and "change_on_1 b k ⟹ block i (Suc t) = e_snoc (e_update b k 1) 0"
and "change_on_neither b k⟹ block i (Suc t) = e_snoc b 0"
using assms r_next state_Suc by simp_all

text ‹Non-gap positions in the block remain unchanged after an
iteration.›

lemma block_stable:
assumes "j < e_length (block i t)" and "j ≠ gap i t"
shows "e_nth (block i t) j = e_nth (block i (Suc t)) j"
proof -
from change_conditions[of "block i t" "gap i t"] show ?thesis
using assms block_Suc gap_Suc
by (cases, (simp_all add: nth_append))
qed

text ‹Next are some properties of @{term block} and @{term gap}.›

lemma gap_in_block: "gap i t < e_length (block i t)"
proof (induction t)
case 0
then show ?case by (simp add: state_at_0)
next
case (Suc t)
with change_conditions[of "block i t" "gap i t"] show ?case
proof (cases)
case on_0
then show ?thesis by (simp add: block_Suc(1) gap_Suc(1))
next
case on_1
then show ?thesis by (simp add: block_Suc(2) gap_Suc(2))
next
case neither
then show ?thesis using Suc.IH block_Suc(3) gap_Suc(3) by force
qed
qed

lemma length_block: "e_length (block i t) = Suc (Suc t)"
proof (induction t)
case 0
then show ?case by (simp add: state_at_0)
next
case (Suc t)
with change_conditions[of "block i t" "gap i t"] show ?case
by (cases, simp_all add: block_Suc gap_Suc)
qed

lemma gap_gr0: "gap i t > 0"
proof (induction t)
case 0
then show ?case by (simp add: state_at_0)
next
case (Suc t)
with change_conditions[of "block i t" "gap i t"] show ?case
using length_block by (cases, simp_all add: block_Suc gap_Suc)
qed

lemma hd_block: "e_hd (block i t) = i"
proof (induction t)
case 0
then show ?case by (simp add: state_at_0)
next
case (Suc t)
from change_conditions[of "block i t" "gap i t"] show ?case
proof (cases)
case on_0
then show ?thesis
using Suc block_Suc(1) length_block by (metis e_hd_snoc gap_Suc(1) gap_gr0)
next
case on_1
let ?b = "block i t" and ?k = "gap i t"
have "?k > 0"
using gap_gr0 Suc by simp
then have "e_nth (e_update ?b ?k 1) 0 = e_nth ?b 0"
by simp
then have *: "e_hd (e_update ?b ?k 1) = e_hd ?b"
using e_hd_nth0 gap_Suc(2)[of _ i t] gap_gr0 on_1 by (metis e_length_update)
from on_1 have "block i (Suc t) = e_snoc (e_update ?b ?k 1) 0"
by (simp add: block_Suc(2))
then show ?thesis
using e_hd_0 e_hd_snoc Suc length_block ‹?k > 0› *
by (metis e_length_update gap_Suc(2) gap_gr0 on_1)
next
case neither
then show ?thesis
by (metis Suc block_stable e_hd_nth0 gap_gr0 length_block not_gr0 zero_less_Suc)
qed
qed

text ‹Formally, a block always ends in zero, even if it ends in a gap.›

lemma last_block: "e_nth (block i t) (gap i t) = 0"
proof (induction t)
case 0
then show ?case by (simp add: state_at_0)
next
case (Suc t)
from change_conditions[of "block i t" "gap i t"] show ?case
proof cases
case on_0
then show ?thesis using Suc by (simp add: block_Suc(1) gap_Suc(1))
next
case on_1
then show ?thesis using Suc by (simp add: block_Suc(2) gap_Suc(2) nth_append)
next
case neither
then have
"block i (Suc t) = e_snoc (block i t) 0"
"gap i (Suc t) = gap i t"
by (simp_all add: gap_Suc(3) block_Suc(3))
then show ?thesis
using Suc gap_in_block by (simp add: nth_append)
qed
qed

lemma gap_le_Suc: "gap i t ≤ gap i (Suc t)"
using change_conditions[of "block i t" "gap i t"]
gap_Suc gap_in_block less_imp_le[of "gap i t" "e_length (block i t)"]
by (cases) simp_all

lemma gap_monotone:
assumes "t⇩1 ≤ t⇩2"
shows "gap i t⇩1 ≤ gap i t⇩2"
proof -
have "gap i t⇩1 ≤ gap i (t⇩1 + j)" for j
proof (induction j)
case 0
then show ?case by simp
next
case (Suc j)
then show ?case using gap_le_Suc dual_order.trans by fastforce
qed
then show ?thesis using assms le_Suc_ex by blast
qed

text ‹We need some lemmas relating the shape of the next state
to the hypothesis change conditions in Steps 1, 2, and 3.›

lemma state_change_on_neither:
assumes "gap i (Suc t) = gap i t"
shows "change_on_neither (block i t) (gap i t)"
and "block i (Suc t) = e_snoc (block i t) 0"
proof -
let ?b = "block i t" and ?k = "gap i t"
have "?k < e_length ?b"
using gap_in_block by simp
from change_conditions[of ?b ?k] show "change_on_neither (block i t) (gap i t)"
proof (cases)
case on_0
then show ?thesis
using ‹?k < e_length ?b› assms gap_Suc(1) by auto
next
case on_1
then show ?thesis using assms gap_Suc(2) by auto
next
case neither
then show ?thesis by simp
qed
then show "block i (Suc t) = e_snoc (block i t) 0"
using block_Suc(3) by simp
qed

lemma state_change_on_either:
assumes "gap i (Suc t) ≠ gap i t"
shows "¬ change_on_neither (block i t) (gap i t)"
and "gap i (Suc t) = e_length (block i t)"
proof -
let ?b = "block i t" and ?k = "gap i t"
show "¬ change_on_neither (block i t) (gap i t)"
proof
assume "change_on_neither (block i t) (gap i t)"
then have "gap i (Suc t) = ?k"
by (simp add: gap_Suc(3))
with assms show False by simp
qed
then show "gap i (Suc t) = e_length (block i t)"
using gap_Suc(1) gap_Suc(2) by blast
qed

text ‹Next up is the definition of $\tau$. In every iteration the
process determines $\tau_i(x)$ for some $x$ either by appending 0 to the
current block $b$, or by filling the current gap $k$. In the former case,
the value is determined for $x = |b|$, in the latter for $x = k$.›

text ‹For $i$ and $x$ the function @{term r_dettime} computes in which
iteration the process for $i$ determines the value $\tau_i(x)$. This is the
first iteration in which the block is long enough to contain position $x$ and
in which $x$ is not the gap. If $\tau_i(x)$ is never determined, because Case~2 is
reached with $k = x$, then @{term r_dettime} diverges.›

abbreviation determined :: "nat ⇒ nat ⇒ bool" where
"determined i x ≡ ∃t. x < e_length (block i t) ∧ x ≠ gap i t"

lemma determined_0: "determined i 0"
using gap_gr0[of i 0] gap_in_block[of i 0] by force

definition "r_dettime ≡
Mn 2
(Cn 3 r_and
[Cn 3 r_less
[Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]],
Cn 3 r_neq
[Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]]])"

lemma r_dettime_recfn: "recfn 2 r_dettime"
unfolding r_dettime_def using r_state_recfn by simp

abbreviation dettime :: partial2 where
"dettime i x ≡ eval r_dettime [i, x]"

lemma r_dettime:
shows "determined i x ⟹ dettime i x ↓= (LEAST t. x < e_length (block i t) ∧ x ≠ gap i t)"
and "¬ determined i x ⟹ dettime i x ↑"
proof -
define f where "f =
(Cn 3 r_and
[Cn 3 r_less
[Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]],
Cn 3 r_neq
[Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]]])"
then have "r_dettime = Mn 2 f"
unfolding f_def r_dettime_def by simp
have "recfn 3 f"
unfolding f_def using r_state_recfn by simp
then have "total f"
unfolding f_def using Cn_total r_state_total Mn_free_imp_total by simp
have f: "eval f [t, i, x] ↓= (if x < e_length (block i t) ∧ x ≠ gap i t then 0 else 1)" for t
proof -
let ?b = "Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]"
let ?k = "Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]"
have "eval ?b [t, i, x] ↓= pdec1 (the (eval r_state [t, i]))"
using r_state_recfn r_state_total by simp
then have b: "eval ?b [t, i, x] ↓= block i t"
using block_def by simp
have "eval ?k [t, i, x] ↓= pdec2 (the (eval r_state [t, i]))"
using r_state_recfn r_state_total by simp
then have k: "eval ?k [t, i, x] ↓= gap i t"
using gap_def by simp
have "eval
(Cn 3 r_neq [Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]])
[t, i, x] ↓=
(if x ≠ gap i t then 0 else 1)"
using b k r_state_recfn r_state_total by simp
moreover have "eval
(Cn 3 r_less
[Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]])
[t, i, x] ↓=
(if x < e_length (block i t) then 0 else 1)"
using b k r_state_recfn r_state_total by simp
ultimately show ?thesis
unfolding f_def using b k r_state_recfn r_state_total by simp
qed
{
assume "determined i x"
with f have "∃t. eval f [t, i, x] ↓= 0" by simp
then have "dettime i x ↓= (LEAST t. eval f [t, i, x] ↓= 0)"
using ‹total f› ‹r_dettime = Mn 2 f› r_dettime_recfn ‹recfn 3 f›
eval_Mn_total[of 2 f "[i, x]"]
by simp
then show "dettime i x ↓= (LEAST t. x < e_length (block i t) ∧ x ≠ gap i t)"
using f by simp
next
assume "¬ determined i x"
with f have "¬ (∃t. eval f [t, i, x] ↓= 0)" by simp
then have "dettime i x ↑"
using ‹total f› ‹r_dettime = Mn 2 f› r_dettime_recfn ‹recfn 3 f›
eval_Mn_total[of 2 f "[i, x]"]
by simp
with f show "dettime i x ↑" by simp
}
qed

lemma r_dettimeI:
assumes "x < e_length (block i t) ∧ x ≠ gap i t"
and "⋀T. x < e_length (block i T) ∧ x ≠ gap i T ⟹ t ≤ T"
shows "dettime i x ↓= t"
proof -
let ?P = "λT. x < e_length (block i T) ∧ x ≠ gap i T"
have "determined i x"
using assms(1) by auto
moreover have "Least ?P = t"
using assms Least_equality[of ?P t] by simp
ultimately show ?thesis using r_dettime by simp
qed

lemma r_dettime_0: "dettime i 0 ↓= 0"
using r_dettimeI[of _ i 0] determined_0 gap_gr0[of i 0] gap_in_block[of i 0]
by fastforce

text ‹Computing the value of $\tau_i(x)$ works by running the process
@{term r_state} for @{term "dettime i x"} iterations and taking the value at
index $x$ of the resulting block.›

definition "r_tau ≡ Cn 2 r_nth [Cn 2 r_pdec1 [Cn 2 r_state [r_dettime, Id 2 0]], Id 2 1]"

lemma r_tau_recfn: "recfn 2 r_tau"
unfolding r_tau_def using r_dettime_recfn r_state_recfn by simp

abbreviation tau :: partial2 ("τ") where
"τ i x ≡ eval r_tau [i, x]"

lemma tau_in_P2: "τ ∈ 𝒫⇧2"
using r_tau_recfn by auto

lemma tau_diverg:
assumes "¬ determined i x"
shows "τ i x ↑"
unfolding r_tau_def using assms r_dettime r_dettime_recfn r_state_recfn by simp

lemma tau_converg:
assumes "determined i x"
shows "τ i x ↓= e_nth (block i (the (dettime i x))) x"
proof -
from assms obtain t where t: "dettime i x ↓= t"
using r_dettime(1) by blast
then have "eval (Cn 2 r_state [r_dettime, Id 2 0]) [i, x] = eval r_state [t, i]"
using r_state_recfn r_dettime_recfn by simp
moreover have "eval r_state [t, i] ↓"
using r_state_total r_state_recfn by simp
ultimately have "eval (Cn 2 r_pdec1 [Cn 2 r_state [r_dettime, Id 2 0]]) [i, x] =
eval r_pdec1 [the (eval r_state [t, i])]"
using r_state_recfn r_dettime_recfn by simp
then show ?thesis
unfolding r_tau_def using r_state_recfn r_dettime_recfn t block_def by simp
qed

lemma tau_converg':
assumes "dettime i x ↓= t"
shows "τ i x ↓= e_nth (block i t) x"
using assms tau_converg[of x i] r_dettime(2)[of x i] by fastforce

lemma tau_at_0: "τ i 0 ↓= i"
proof -
have "τ i 0 ↓= e_nth (block i 0) 0"
using tau_converg'[OF r_dettime_0] by simp
then show ?thesis using block_def by (simp add: r_state_at_0)
qed

lemma state_unchanged:
assumes "gap i t - 1 ≤ y" and "y ≤ t"
shows "gap i t = gap i y"
proof -
have "gap i t = gap i (gap i t - 1)"
proof (induction t)
case 0
then show ?case by (simp add: gap_def r_state_at_0)
next
case (Suc t)
show ?case
proof (cases "gap i (Suc t) = t + 2")
case True
then show ?thesis by simp
next
case False
then show ?thesis
using Suc state_change_on_either(2) length_block by force
qed
qed
moreover have "gap i (gap i t - 1) ≤ gap i y"
using assms(1) gap_monotone by simp
moreover have "gap i y ≤ gap i t"
using assms(2) gap_monotone by simp
ultimately show ?thesis by simp
qed

text ‹The values of the non-gap indices $x$ of every block created in
the diagonalization process equal $\tau_i(x)$.›

lemma tau_eq_state:
assumes "j < e_length (block i t)" and "j ≠ gap i t"
shows "τ i j ↓= e_nth (block i t) j"
using assms
proof (induction t)
case 0
then have "j = 0"
using gap_gr0[of i 0] gap_in_block[of i 0] length_block[of i 0] by simp
then have "τ (e_hd (block i t)) j ↓= e_nth (block i (the (dettime i 0))) 0"
using determined_0 tau_converg hd_block by simp
then have "τ (e_hd (block i t)) j ↓= e_nth (block i 0) 0"
using r_dettime_0 by simp
then show ?case using ‹j = 0› r_dettime_0 tau_converg' by simp
next
case (Suc t)
let ?b = "block i t"
let ?bb = "block i (Suc t)"
let ?k = "gap i t"
let ?kk = "gap i (Suc t)"
show ?case
proof (cases "?kk = ?k")
case kk_eq_k: True
then have bb_b0: "?bb = e_snoc ?b 0"
using state_change_on_neither by simp
show "τ i j ↓= e_nth ?bb j"
proof (cases "j < e_length ?b")
case True
then have "e_nth ?bb j = e_nth ?b j"
using bb_b0 by (simp add: nth_append)
moreover have "j ≠ ?k"
using Suc kk_eq_k by simp
ultimately show ?thesis using Suc True by simp
next
case False
then have j: "j = e_length ?b"
using Suc.prems(1) length_block by auto
then have "e_nth ?bb j = 0"
using bb_b0 by simp
have "dettime i j ↓= Suc t"
proof (rule r_dettimeI)
show "j < e_length ?bb ∧ j ≠ ?kk"
using Suc.prems(1,2) by linarith
show "⋀T. j < e_length (block i T) ∧ j ≠ gap i T ⟹ Suc t ≤ T"
using length_block j by simp
qed
with tau_converg' show ?thesis by simp
qed
next
case False
then have kk_lenb: "?kk = e_length ?b"
using state_change_on_either by simp
then show ?thesis
proof (cases "j = ?k")
case j_eq_k: True
have "dettime i j ↓= Suc t"
proof (rule r_dettimeI)
show "j < e_length ?bb ∧ j ≠ ?kk"
using Suc.prems(1,2) by simp
show "Suc t ≤ T" if "j < e_length (block i T) ∧ j ≠ gap i T" for T
proof (rule ccontr)
assume "¬ (Suc t ≤ T)"
then have "T < Suc t" by simp
then show False
proof (cases "T < ?k - 1")
case True
then have "e_length (block i T) = T + 2"
using length_block by simp
then have "e_length (block i T) < ?k + 1"
using True by simp
then have "e_length (block i T) ≤ ?k" by simp
then have "e_length (block i T) ≤ j"
using j_eq_k by simp
then show False
using that by simp
next
case False
then have "?k - 1 ≤ T" and "T ≤ t"
using ‹T < Suc t› by simp_all
with state_unchanged have "gap i t = gap i T" by blast
then show False
using j_eq_k that by simp
qed
qed
qed
then show ?thesis using tau_converg' by simp
next
case False
then have "j < e_length ?b"
using kk_lenb Suc.prems(1,2) length_block by auto
then show ?thesis using Suc False block_stable by fastforce
qed
qed
qed

lemma tau_eq_state':
assumes "j < t + 2" and " j ≠ gap i t"
shows "τ i j ↓= e_nth (block i t) j"
using assms tau_eq_state length_block by simp

text ‹We now consider the two cases described in the proof sketch.
In Case~2 there is a gap that never gets filled, or equivalently there is
a rightmost gap.›

abbreviation "case_two i ≡ (∃t. ∀T. gap i T ≤ gap i t)"

abbreviation "case_one i ≡ ¬ case_two i"

text ‹Another characterization of Case~2 is that from some iteration on
only @{term change_on_neither} holds.›

lemma case_two_iff_forever_neither:
"case_two i ⟷ (∃t. ∀T≥t. change_on_neither (block i T) (gap i T))"
proof
assume "∃t. ∀T≥t. change_on_neither (block i T) (gap i T)"
then obtain t where t: "∀T≥t. change_on_neither (block i T) (gap i T)"
by auto
have "(gap i T) ≤ (gap i t)" for T
proof (cases "T ≤ t")
case True
then show ?thesis using gap_monotone by simp
next
case False
then show ?thesis
proof (induction T)
case 0
then show ?case by simp
next
case (Suc T)
with t have "change_on_neither ((block i T)) ((gap i T))"
by simp
then show ?case
using Suc.IH state_change_on_either(1)[of i T] gap_monotone[of T t i]
by metis
qed
qed
then show "∃t. ∀T. gap i T ≤ gap i t"
by auto
next
assume "∃t. ∀T. gap i T ≤ gap i t"
then obtain t where t: "∀T. gap i T ≤ gap i t"
by auto
have "change_on_neither (block i T) (gap i T)" if "T≥t" for T
proof -
have T: "(gap i T) ≥ (gap i t)"
using gap_monotone that by simp
show ?thesis
proof (rule ccontr)
assume "¬ change_on_neither (block i T) (gap i T)"
then have "change_on_0 (block i T) (gap i T) ∨ change_on_1 (block i T) (gap i T)"
by simp
then have "gap i (Suc T) > gap i T"
using gap_le_Suc[of i] state_change_on_either(2)[of i] state_change_on_neither(1)[of i]
dual_order.strict_iff_order
by blast
with T have "gap i (Suc T) > gap i t" by simp
with t show False
using not_le by auto
qed
qed
then show "∃t. ∀T≥t. change_on_neither (block i T) (gap i T)"
by auto
qed

text ‹In Case~1, $\tau_i$ is total.›

lemma case_one_tau_total:
assumes "case_one i"
shows "τ i x ↓"
proof (cases "x = gap i x")
case True
from assms have "∀t. ∃T. gap i T > gap i t"
using le_less_linear gap_def[of i x] by blast
then obtain T where T: "gap i T > gap i x"
by auto
then have "T > x"
using gap_monotone leD le_less_linear by blast
then have "x < T + 2" by simp
moreover from T True have "x ≠ gap i T" by simp
ultimately show ?thesis using tau_eq_state' by simp
next
case False
moreover have "x < x + 2" by simp
ultimately show ?thesis using tau_eq_state' by blast
qed

text ‹In Case~2, $\tau_i$ is undefined only at the gap that never gets filled.›

lemma case_two_tau_not_quite_total:
assumes "∀T. gap i T ≤ gap i t"
shows "τ i (gap i t) ↑"
and "x ≠ gap i t ⟹ τ i x ↓"
proof -
let ?k = "gap i t"
have "¬ determined i ?k"
proof
assume "determined i ?k"
then obtain T where T: "?k < e_length (block i T) ∧ ?k ≠ gap i T"
by auto
with assms have snd_le: "gap i T < ?k"
by (simp add: dual_order.strict_iff_order)
then have "T < t"
using gap_monotone by (metis leD le_less_linear)
from T length_block have "?k < T + 2" by simp
moreover have "?k ≠ T + 1"
using T state_change_on_either(2) ‹T < t› state_unchanged
by (metis Suc_eq_plus1 Suc_leI add_diff_cancel_right' le_add1 nat_neq_iff)
ultimately have "?k ≤ T" by simp
then have "gap i T = gap i ?k"
using state_unchanged[of i T "?k"] ‹?k < T + 2› snd_le by simp
then show False
by (metis diff_le_self state_unchanged leD nat_le_linear gap_monotone snd_le)
qed
with tau_diverg show "τ i ?k ↑" by simp

assume "x ≠ ?k"
show "τ i x ↓"
proof (cases "x < t + 2")
case True
with ‹x ≠ ?k› tau_eq_state' show ?thesis by simp
next
case False
then have "gap i x = ?k"
using assms by (simp add: dual_order.antisym gap_monotone)
with ‹x ≠ ?k› have "x ≠ gap i x" by simp
then show ?thesis using tau_eq_state'[of x x] by simp
qed
qed

lemma case_two_tau_almost_total:
assumes "∃t. ∀T. gap i T ≤ gap i t" (is "∃t. ?P t")
shows "τ i (gap i (Least ?P)) ↑"
and "x ≠ gap i (Least ?P) ⟹ τ i x ↓"
proof -
from assms have "?P (Least ?P)"
using LeastI_ex[of ?P] by simp
then show "τ i (gap i (Least ?P)) ↑" and "x ≠ gap i (Least ?P) ⟹ τ i x ↓"
using case_two_tau_not_quite_total by simp_all
qed

text ‹Some more properties of $\tau$.›

lemma init_tau_gap: "(τ i) ▹ (gap i t - 1) = e_take (gap i t) (block i t)"
proof (intro initI')
show 1: "e_length (e_take (gap i t) (block i t)) = Suc (gap i t - 1)"
proof -
have "gap i t > 0"
using gap_gr0 by simp
moreover have "gap i t < e_length (block i t)"
using gap_in_block by simp
ultimately have "e_length (e_take (gap i t) (block i t)) = gap i t"
by simp
then show ?thesis using gap_gr0 by simp
qed
show "τ i x ↓= e_nth (e_take (gap i t) (block i t)) x" if "x < Suc (gap i t - 1)" for x
proof -
have x_le: "x < gap i t"
using that gap_gr0 by simp
then have "x < e_length (block i t)"
using gap_in_block less_trans by blast
then have *: "τ i x ↓= e_nth (block i t) x"
using x_le tau_eq_state by auto
have "x < e_length (e_take (gap i t) (block i t))"
using x_le 1 by simp
then have "e_nth (block i t) x = e_nth (e_take (gap i t) (block i t)) x"
using x_le by simp
then show ?thesis using * by simp
qed
qed

lemma change_on_0_init_tau:
assumes "change_on_0 (block i t) (gap i t)"
shows "(τ i) ▹ (t + 1) = block i t"
proof (intro initI')
let ?b = "block i t" and ?k = "gap i t"
show "e_length (block i t) = Suc (t + 1)"
using length_block by simp
show "(τ i) x ↓= e_nth (block i t) x" if "x < Suc (t + 1)" for x
proof (cases "x = ?k")
case True
have "gap i (Suc t) = e_length ?b" and b: "block i (Suc t) = e_snoc ?b 0"
using gap_Suc(1) block_Suc(1) assms by simp_all
then have "x < e_length (block i (Suc t))" "x ≠ gap i (Suc t)"
using that length_block by simp_all
then have "τ i x ↓= e_nth (block i (Suc t)) x"
using tau_eq_state by simp
then show ?thesis using that assms b by (simp add: nth_append)
next
case False
then show ?thesis using that assms tau_eq_state' by simp
qed
qed

lemma change_on_0_hyp_change:
assumes "change_on_0 (block i t) (gap i t)"
shows "σ i ((τ i) ▹ (t + 1)) ≠ σ i ((τ i) ▹ (gap i t - 1))"
using assms hd_block init_tau_gap change_on_0_init_tau by simp

lemma change_on_1_init_tau:
assumes "change_on_1 (block i t) (gap i t)"
shows "(τ i) ▹  (t + 1) = e_update (block i t) (gap i t) 1"
proof (intro initI')
let ?b = "block i t" and ?k = "gap i t"
show "e_length (e_update ?b ?k 1) = Suc (t + 1)"
using length_block by simp
show "(τ i) x ↓= e_nth (e_update ?b ?k 1) x" if "x < Suc (t + 1)" for x
proof (cases "x = ?k")
case True
have "gap i (Suc t) = e_length ?b" and b: "block i (Suc t) = e_snoc (e_update ?b ?k 1) 0"
using gap_Suc(2) block_Suc(2) assms by simp_all
then have "x < e_length (block i (Suc t))" "x ≠ gap i (Suc t)"
using that length_block by simp_all
then have "τ i x ↓= e_nth (block i (Suc t)) x"
using tau_eq_state by simp
then show ?thesis using that assms b nth_append by (simp add: nth_append)
next
case False
then show ?thesis using that assms tau_eq_state' by simp
qed
qed

lemma change_on_1_hyp_change:
assumes "change_on_1 (block i t) (gap i t)"
shows "σ i ((τ i) ▹ (t + 1)) ≠ σ i ((τ i) ▹ (gap i t - 1))"
using assms hd_block init_tau_gap change_on_1_init_tau by simp

lemma change_on_either_hyp_change:
assumes "¬ change_on_neither (block i t) (gap i t)"
shows "σ i ((τ i) ▹ (t + 1)) ≠ σ i ((τ i) ▹ (gap i t - 1))"
using assms change_on_0_hyp_change change_on_1_hyp_change by auto

lemma filled_gap_0_init_tau:
assumes "f⇩0 = (τ i)((gap i t):=Some 0)"
shows "f⇩0 ▹ (t + 1) = block i t"
proof (intro initI')
show len: "e_length (block i t) = Suc (t + 1)"
using assms length_block by auto
show "f⇩0 x ↓= e_nth (block i t) x" if "x < Suc (t + 1)" for x
proof (cases "x = gap i t")
case True
then show ?thesis using assms last_block by auto
next
case False
then show ?thesis using assms len tau_eq_state that by auto
qed
qed

lemma filled_gap_1_init_tau:
assumes "f⇩1 = (τ i)((gap i t):=Some 1)"
shows "f⇩1 ▹ (t + 1) = e_update (block i t) (gap i t) 1"
proof (intro initI')
show len: "e_length (e_update (block i t) (gap i t) 1) = Suc (t + 1)"
using e_length_update length_block by simp
show "f⇩1 x ↓= e_nth (e_update (block i t) (gap i t) 1) x" if "x < Suc (t + 1)" for x
proof (cases "x = gap i t")
case True
moreover have "gap i t < e_length (block i t)"
using gap_in_block by simp
ultimately show ?thesis using assms by simp
next
case False
then show ?thesis using assms len tau_eq_state that by auto
qed
qed

subsection ‹The separating class›

text ‹Next we define the sets $V_i$ from the introductory proof sketch
(page~\pageref{s:lim_bc}).›

definition V_bclim :: "nat ⇒ partial1 set" where
"V_bclim i ≡
if case_two i
then let k = gap i (LEAST t. ∀T. gap i T ≤ gap i t)
in {(τ i)(k:=Some 0), (τ i)(k:=Some 1)}
else {τ i}"

lemma V_subseteq_R1: "V_bclim i ⊆ ℛ"
proof (cases "case_two i")
case True
define k where "k = gap i (LEAST t. ∀T. gap i T ≤ gap i t)"
have "τ i ∈ 𝒫"
using tau_in_P2 P2_proj_P1 by auto
then have "(τ i)(k:=Some 0) ∈ 𝒫" and "(τ i)(k:=Some 1) ∈ 𝒫"
using P1_update_P1 by simp_all
moreover have "total1 ((τ i)(k:=Some v))" for v
using case_two_tau_almost_total(2)[OF True] k_def total1_def by simp
ultimately have "(τ i)(k:=Some 0) ∈ ℛ" and "(τ i)(k:=Some 1) ∈ ℛ"
using P1_total_imp_R1 by simp_all
moreover have "V_bclim i = {(τ i)(k:=Some 0), (τ i)(k:=Some 1)}"
using True V_bclim_def k_def by (simp add: Let_def)
ultimately show ?thesis by simp
next
case False
have "V_bclim i = {τ i}"
unfolding V_bclim_def by (simp add: False)
moreover have "τ i ∈ ℛ"
using total1I case_one_tau_total[OF False] tau_in_P2 P2_proj_P1[of τ] P1_total_imp_R1
by simp
ultimately show ?thesis by simp
qed

lemma case_one_imp_gap_unbounded:
assumes "case_one i"
shows "∃t. gap i t - 1 > n"
proof (induction n)
case 0
then show ?case
using assms gap_gr0[of i] state_at_0(2)[of i] by (metis diff_is_0_eq gr_zeroI)
next
case (Suc n)
then obtain t where t: "gap i t - 1 > n"
by auto
moreover from assms have "∀t. ∃T. gap i T > gap i t"
using leI by blast
ultimately obtain T where "gap i T > gap i t"
by auto
then have "gap i T - 1 > gap i t - 1"
using gap_gr0[of i] by (simp add: Suc_le_eq diff_less_mono)
with t have "gap i T - 1 > Suc n" by simp
then show ?case by auto
qed

lemma case_one_imp_not_learn_lim_V:
assumes "case_one i"
shows "¬ learn_lim φ (V_bclim i) (σ i)"
proof -
have V_bclim: "V_bclim i = {τ i}"
using assms V_bclim_def by (auto simp add: Let_def)
have "∃m⇩1>n. ∃m⇩2>n. (σ i) ((τ i) ▹ m⇩1) ≠ (σ i) ((τ i) ▹ m⇩2)" for n
proof -
obtain t where t: "gap i t - 1 > n"
using case_one_imp_gap_unbounded[OF assms] by auto
moreover have "∀t. ∃T≥t. ¬ change_on_neither (block i T) (gap i T)"
using assms case_two_iff_forever_neither by blast
ultimately obtain T where T: "T ≥ t" "¬ change_on_neither (block i T) (gap i T)"
by auto
then have "(σ i) ((τ i) ▹ (T + 1)) ≠ (σ i) ((τ i) ▹ (gap i T - 1))"
using change_on_either_hyp_change by simp
moreover have "gap i T - 1 > n"
using t T(1) gap_monotone by (simp add: diff_le_mono less_le_trans)
moreover have "T + 1 > n"
proof -
have "gap i T - 1 ≤ T"
using gap_in_block length_block by (simp add: le_diff_conv less_Suc_eq_le)
then show ?thesis using ‹gap i T - 1 > n› by simp
qed
ultimately show ?thesis by auto
qed
with infinite_hyp_changes_not_Lim V_bclim show ?thesis by simp
qed

lemma case_two_imp_not_learn_lim_V:
assumes "case_two i"
shows "¬ learn_lim φ (V_bclim i) (σ i)"
proof -
let ?P = "λt. ∀T. (gap i T) ≤ (gap i t)"
let ?t = "LEAST t. ?P t"
let ?k = "gap i ?t"
let ?b = "e_take ?k (block i ?t)"
have t: "∀T. gap i T ≤ gap i ?t"
using assms LeastI_ex[of ?P] by simp
then have neither: "∀T≥?t. change_on_neither (block i T) (gap i T)"
using gap_le_Suc gap_monotone state_change_on_neither(1)
by (metis (no_types, lifting) antisym)
have gap_T: "∀T≥?t. gap i T = ?k"
using t gap_monotone antisym_conv by blast
define f⇩0 where "f⇩0 = (τ i)(?k:=Some 0)"
define f⇩1 where "f⇩1 = (τ i)(?k:=Some 1)"
show ?thesis
proof (rule same_hyp_for_two_not_Lim)
show "f⇩0 ∈ V_bclim i" and "f⇩1 ∈ V_bclim i"
using assms V_bclim_def f⇩0_def f⇩1_def by (simp_all add: Let_def)
show "f⇩0 ≠ f⇩1" using f⇩0_def f⇩1_def by (meson map_upd_eqD1 zero_neq_one)
show "∀n≥Suc ?t. σ i (f⇩0 ▹ n) = σ i ?b"
proof -
have "σ i (block i T) = σ i (e_take ?k (block i T))" if "T ≥ ?t" for T
using that gap_T neither hd_block by metis
then have "σ i (block i T) = σ i ?b" if "T ≥ ?t" for T
by (metis (no_types, lifting) init_tau_gap gap_T that)
then have "σ i (f⇩0 ▹ (T + 1)) = σ i ?b" if "T ≥ ?t" for T
using filled_gap_0_init_tau[of f⇩0 i T] f⇩0_def gap_T that
by (metis (no_types, lifting))
then have "σ i (f⇩0 ▹ T) = σ i ?b" if "T ≥ Suc ?t" for T
using that by (metis (no_types, lifting) Suc_eq_plus1 Suc_le_D Suc_le_mono)
then show ?thesis by simp
qed
show "∀n≥Suc ?t. σ i (f⇩1 ▹ n) = σ i ?b"
proof -
have "σ i (e_update (block i T) ?k 1) = σ i (e_take ?k (block i T))" if "T ≥ ?t" for T
using neither by (metis (no_types, lifting) hd_block gap_T that)
then have "σ i (e_update (block i T) ?k 1) = σ i ?b" if "T ≥ ?t" for T
using that init_tau_gap[of i] gap_T by (metis (no_types, lifting))
then have "σ i (f⇩1 ▹ (T + 1)) = σ i ?b" if "T ≥ ?t" for T
using filled_gap_1_init_tau[of f⇩1 i T] f⇩1_def gap_T that
by (metis (no_types, lifting))
then have "σ i (f⇩1 ▹ T) = σ i ?b" if "T ≥ Suc ?t" for T
using that by (metis (no_types, lifting) Suc_eq_plus1 Suc_le_D Suc_le_mono)
then show ?thesis by simp
qed
qed
qed

corollary not_learn_lim_V: "¬ learn_lim φ (V_bclim i) (σ i)"
using case_one_imp_not_learn_lim_V case_two_imp_not_learn_lim_V
by (cases "case_two i") simp_all

text ‹Next we define the separating class.›

definition V_BCLIM :: "partial1 set" ("V⇘BC-LIM⇙") where
"V⇘BC-LIM⇙ ≡ ⋃i. V_bclim i"

lemma V_BCLIM_R1: "V⇘BC-LIM⇙ ⊆ ℛ"
using V_BCLIM_def V_subseteq_R1 by auto

lemma V_BCLIM_not_in_Lim: "V⇘BC-LIM⇙ ∉ LIM"
proof
assume "V⇘BC-LIM⇙ ∈ LIM"
then obtain s where s: "learn_lim φ V⇘BC-LIM⇙ s"
using learn_lim_wrt_goedel[OF goedel_numbering_phi] Lim_def by blast
moreover obtain i where "φ i = s"
using s learn_limE(1) phi_universal by blast
ultimately have "learn_lim φ V⇘BC-LIM⇙ (λx. eval r_sigma [i, x])"
using learn_lim_sigma by simp
moreover have "V_bclim i ⊆ V⇘BC-LIM⇙"
using V_BCLIM_def by auto
ultimately have "learn_lim φ (V_bclim i) (λx. eval r_sigma [i, x])"
using learn_lim_closed_subseteq by simp
then show False
using not_learn_lim_V by simp
qed

subsection ‹The separating class is in BC›

text ‹In order to show @{term "V⇘BC-LIM⇙ ∈ BC"} we
define a hypothesis space that for every function $\tau_i$ and every list $b$
of numbers contains a copy of $\tau_i$ with the first $|b|$ values replaced
by $b$.›

definition psitau :: partial2 ("ψ⇧τ") where
"ψ⇧τ b x ≡ (if x < e_length b then Some (e_nth b x) else τ (e_hd b) x)"

lemma psitau_in_P2: "ψ⇧τ ∈ 𝒫⇧2"
proof -
define r where "r ≡
Cn 2
(r_lifz r_nth (Cn 2 r_tau [Cn 2 r_hd [Id 2 0], Id 2 1]))
[Cn 2 r_less [Id 2 1, Cn 2 r_length [Id 2 0]], Id 2 0, Id 2 1]"
then have "recfn 2 r"
using r_tau_recfn by simp
moreover have "eval r [b, x] = ψ⇧τ b x" for b x
proof -
let ?f = "Cn 2 r_tau [Cn 2 r_hd [Id 2 0], Id 2 1]"
have "recfn 2 r_nth" "recfn 2 ?f"
using r_tau_recfn by simp_all
then have "eval (r_lifz r_nth ?f) [c, b, x] =
(if c = 0 then eval r_nth [b, x] else eval ?f [b, x])" for c
by simp
moreover have "eval r_nth [b, x] ↓= e_nth b x"
by simp
moreover have "eval ?f [b, x] = τ (e_hd b) x"
using r_tau_recfn by simp
ultimately have "eval (r_lifz r_nth ?f) [c, b, x] =
(if c = 0 then Some (e_nth b x) else τ (e_hd b) x)" for c
by simp
moreover have "eval (Cn 2 r_less [Id 2 1, Cn 2 r_length [Id 2 0]]) [b, x] ↓=
(if x < e_length b then 0 else 1)"
by simp
ultimately show ?thesis
unfolding r_def psitau_def using r_tau_recfn by simp
qed
ultimately show ?thesis by auto
qed

lemma psitau_init:
"ψ⇧τ (f ▹ n) x = (if x < Suc n then Some (the (f x)) else τ (the (f 0)) x)"
proof -
let ?e = "f ▹ n"
have "e_length ?e = Suc n" by simp
moreover have "x < Suc n ⟹ e_nth ?e x = the (f x)" by simp
moreover have "e_hd ?e = the (f 0)"
using hd_init by simp
ultimately show ?thesis using psitau_def by simp
qed

text ‹The class @{term V_BCLIM} can be learned BC-style in the
hypothesis space @{term psitau} by the identity function.›

lemma learn_bc_V_BCLIM: "learn_bc ψ⇧τ V⇘BC-LIM⇙ Some"
proof (rule learn_bcI)
show "environment ψ⇧τ V⇘BC-LIM⇙ Some"
using identity_in_R1 V_BCLIM_R1 psitau_in_P2 by auto
show "∃n⇩0. ∀n≥n⇩0. ψ⇧τ (the (Some (f ▹ n))) = f" if "f ∈ V⇘BC-LIM⇙" for f
proof -
from that V_BCLIM_def obtain i where i: "f ∈ V_bclim i"
by auto
show ?thesis
proof (cases "case_two i")
case True
let ?P = "λt. ∀T. (gap i T) ≤ (gap i t)"
let ?lmin = "LEAST t. ?P t"
define k where "k ≡ gap i ?lmin"
have V_bclim: "V_bclim i = {(τ i)(k:=Some 0), (τ i)(k:=Some 1)}"
using True V_bclim_def k_def by (simp add: Let_def)
moreover have "0 < k"
using gap_gr0[of i] k_def by simp
ultimately have "f 0 ↓= i"
using tau_at_0[of i] i by auto
have "ψ⇧τ (f ▹ n) = f" if "n ≥ k" for n
proof
fix x
show "ψ⇧τ (f ▹ n) x = f x"
proof (cases "x ≤ n")
case True
then show ?thesis
using R1_imp_total1 V_subseteq_R1 i psitau_init by fastforce
next
case False
then have "ψ⇧τ (f ▹ n) x = τ (the (f 0)) x"
using psitau_init by simp
then have "ψ⇧τ (f ▹ n) x = τ i x"
using ‹f 0 ↓= i› by simp
moreover have "f x = τ i x"
using False V_bclim i that by auto
ultimately show ?thesis by simp
qed
qed
then show ?thesis by auto
next
case False
then have "V_bclim i = {τ i}"
using V_bclim_def by (auto simp add: Let_def)
then have f: "f = τ i"
using i by simp
have "ψ⇧τ (f ▹ n) = f" for n
proof
fix x
show "ψ⇧τ (f ▹ n) x = f x"
proof (cases "x ≤ n")
case True
then show ?thesis
using R1_imp_total1 V_BCLIM_R1 psitau_init that by auto
next
case False
then show ?thesis by (simp add: f psitau_init tau_at_0)
qed
qed
then show ?thesis by simp
qed
qed
qed

text ‹Finally, the main result of this section:›

theorem Lim_subset_BC: "LIM ⊂ BC"
using learn_bc_V_BCLIM BC_def Lim_subseteq_BC V_BCLIM_not_in_Lim by auto

end