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 "σ ∈
ℛ⇧²"} 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⇩₁, y⇩₁] ≠ eval r_sigma [x⇩₂, y⇩₂] ⟷
      the (eval r_sigma [x⇩₁, y⇩₁]) ≠ the (eval r_sigma [x⇩₂, y⇩₂])"
      for x⇩₁ y⇩₁ x⇩₂ y⇩₂
    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⇩₁ ≤ t⇩₂"
  shows "gap i t⇩₁ ≤ gap i t⇩₂"
proof -
  have "gap i t⇩₁ ≤ gap i (t⇩₁ + 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: "τ ∈ 𝒫⇧²"
  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⇩₀ = (τ i)((gap i t):=Some 0)"
  shows "f⇩₀ ▹ (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⇩₀ 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⇩₁ = (τ i)((gap i t):=Some 1)"
  shows "f⇩₁ ▹ (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⇩₁ 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⇩₁>n. ∃m⇩₂>n. (σ i) ((τ i) ▹ m⇩₁) ≠ (σ i) ((τ i) ▹ m⇩₂)" 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⇩₀ where "f⇩₀ = (τ i)(?k:=Some 0)"
  define f⇩₁ where "f⇩₁ = (τ i)(?k:=Some 1)"
  show ?thesis
  proof (rule same_hyp_for_two_not_Lim)
    show "f⇩₀ ∈ V_bclim i" and "f⇩₁ ∈ V_bclim i"
      using assms V_bclim_def f⇩₀_def f⇩₁_def by (simp_all add: Let_def)
    show "f⇩₀ ≠ f⇩₁" using f⇩₀_def f⇩₁_def by (meson map_upd_eqD1 zero_neq_one)
    show "∀n≥Suc ?t. σ i (f⇩₀ ▹ 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⇩₀ ▹ (T + 1)) = σ i ?b" if "T ≥ ?t" for T
        using filled_gap_0_init_tau[of f⇩₀ i T] f⇩₀_def gap_T that
        by (metis (no_types, lifting))
      then have "σ i (f⇩₀ ▹ 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⇩₁ ▹ 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⇩₁ ▹ (T + 1)) = σ i ?b" if "T ≥ ?t" for T
        using filled_gap_1_init_tau[of f⇩₁ i T] f⇩₁_def gap_T that
        by (metis (no_types, lifting))
      then have "σ i (f⇩₁ ▹ 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: "ψ⇧^τ ∈ 𝒫⇧²"
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⇩₀. ∀n≥n⇩₀. ψ⇧^τ (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