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