diff --git a/thys/Inductive_Inference/Lemma_R.thy b/thys/Inductive_Inference/Lemma_R.thy --- a/thys/Inductive_Inference/Lemma_R.thy +++ b/thys/Inductive_Inference/Lemma_R.thy @@ -1,2114 +1,2114 @@ section \Lemma R\label{s:lemma_r}\ theory Lemma_R imports Inductive_Inference_Basics begin text \A common technique for constructing a class that cannot be learned is diagonalization against all strategies (see, for instance, Section~\ref{s:lim_bc}). Similarly, the typical way of proving that a class cannot be learned is by assuming there is a strategy and deriving a contradiction. Both techniques are easier to carry out if one has to consider only \emph{total} recursive strategies. This is not possible in general, since after all the definitions of the inference types admit strictly partial strategies. However, for many inference types one can show that for every strategy there is a total strategy with at least the same ``learning power''. Results to that effect are called Lemma~R. Lemma~R comes in different strengths depending on how general the construction of the total recursive strategy is. CONS is the only inference type considered here for which not even a weak form of Lemma~R holds.\ subsection \Strong Lemma R for LIM, FIN, and BC\ text \In its strong form Lemma~R says that for any strategy $S$, there is a total strategy $T$ that learns all classes $S$ learns regardless of hypothesis space. The strategy $T$ can be derived from $S$ by a delayed simulation of $S$. More precisely, for input $f^n$, $T$ simulates $S$ for prefixes $f^0, f^1, \ldots, f^n$ for at most $n$ steps. If $S$ halts on none of the prefixes, $T$ outputs an arbitrary hypothesis. Otherwise let $k \leq n$ be maximal such that $S$ halts on $f^k$ in at most $n$ steps. Then $T$ outputs $S(f^k)$. \ text \We reformulate some lemmas for @{term r_result1} to make it easier to use them with @{term "\"}.\ lemma r_result1_converg_phi: assumes "\ i x \= v" shows "\t. (\t'\t. eval r_result1 [t', i, x] \= Suc v) \ (\t'= 0)" using assms r_result1_converg' phi_def by simp_all lemma r_result1_bivalent': assumes "eval r_phi [i, x] \= v" shows "eval r_result1 [t, i, x] \= Suc v \ eval r_result1 [t, i, x] \= 0" using assms r_result1 r_result_bivalent' r_phi'' by simp lemma r_result1_bivalent_phi: assumes "\ i x \= v" shows "eval r_result1 [t, i, x] \= Suc v \ eval r_result1 [t, i, x] \= 0" using assms r_result1_bivalent' phi_def by simp_all lemma r_result1_diverg_phi: assumes "\ i x \" shows "eval r_result1 [t, i, x] \= 0" using assms phi_def r_result1_diverg' by simp lemma r_result1_some_phi: assumes "eval r_result1 [t, i, x] \= Suc v" shows "\ i x \= v" using assms phi_def r_result1_Some' by simp lemma r_result1_saturating': assumes "eval r_result1 [t, i, x] \= Suc v" shows "eval r_result1 [t + d, i, x] \= Suc v" using assms r_result1 r_result_saturating r_phi'' by simp lemma r_result1_saturating_the: assumes "the (eval r_result1 [t, i, x]) > 0" and "t' \ t" shows "the (eval r_result1 [t', i, x]) > 0" proof - from assms(1) obtain v where "eval r_result1 [t, i, x] \= Suc v" using r_result1_bivalent_phi r_result1_diverg_phi by (metis inc_induct le_0_eq not_less_zero option.discI option.expand option.sel) with assms have "eval r_result1 [t', i, x] \= Suc v" using r_result1_saturating' le_Suc_ex by blast then show ?thesis by simp qed lemma Greatest_bounded_Suc: fixes P :: "nat \ nat" shows "(if P n > 0 then Suc n else if \j 0 then Suc (GREATEST j. j < n \ P j > 0) else 0) = (if \j 0 then Suc (GREATEST j. j < Suc n \ P j > 0) else 0)" (is "?lhs = ?rhs") proof (cases "\j 0") case 1: True show ?thesis proof (cases "P n > 0") case True then have "(GREATEST j. j < Suc n \ P j > 0) = n" using Greatest_equality[of "\j. j < Suc n \ P j > 0"] by simp moreover have "?rhs = Suc (GREATEST j. j < Suc n \ P j > 0)" using 1 by simp ultimately have "?rhs = Suc n" by simp then show ?thesis using True by simp next case False then have "?lhs = Suc (GREATEST j. j < n \ P j > 0)" using 1 by (metis less_SucE) moreover have "?rhs = Suc (GREATEST j. j < Suc n \ P j > 0)" using 1 by simp moreover have "(GREATEST j. j < n \ P j > 0) = (GREATEST j. j < Suc n \ P j > 0)" using 1 False by (metis less_SucI less_Suc_eq) ultimately show ?thesis by simp qed next case False then show ?thesis by auto qed text \For $n$, $i$, $x$, the next function simulates $\varphi_i$ on all non-empty prefixes of at most length $n$ of the list $x$ for at most $n$ steps. It returns the length of the longest such prefix for which $\varphi_i$ halts, or zero if $\varphi_i$ does not halt for any prefix.\ definition "r_delay_aux \ Pr 2 (r_constn 1 0) (Cn 4 r_ifz [Cn 4 r_result1 [Cn 4 r_length [Id 4 3], Id 4 2, Cn 4 r_take [Cn 4 S [Id 4 0], Id 4 3]], Id 4 1, Cn 4 S [Id 4 0]])" lemma r_delay_aux_prim: "prim_recfn 3 r_delay_aux" unfolding r_delay_aux_def by simp_all lemma r_delay_aux_total: "total r_delay_aux" using prim_recfn_total[OF r_delay_aux_prim] . lemma r_delay_aux: assumes "n \ e_length x" shows "eval r_delay_aux [n, i, x] \= (if \j 0 then Suc (GREATEST j. j < n \ the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0) else 0)" proof - define z where "z \ Cn 4 r_result1 [Cn 4 r_length [Id 4 3], Id 4 2, Cn 4 r_take [Cn 4 S [Id 4 0], Id 4 3]]" then have z_recfn: "recfn 4 z" by simp have z: "eval z [j, r, i, x] = eval r_result1 [e_length x, i, e_take (Suc j) x]" if "j < e_length x" for j r i x unfolding z_def using that by simp define g where "g \ Cn 4 r_ifz [z, Id 4 1, Cn 4 S [Id 4 0]]" then have g: "eval g [j, r, i, x] \= (if the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0 then Suc j else r)" if "j < e_length x" for j r i x using that z prim_recfn_total z_recfn by simp show ?thesis using assms proof (induction n) case 0 moreover have "eval r_delay_aux [0, i, x] \= 0" using eval_Pr_0 r_delay_aux_def r_delay_aux_prim r_constn by (simp add: r_delay_aux_def) ultimately show ?case by simp next case (Suc n) let ?P = "\j. the (eval r_result1 [e_length x, i, e_take (Suc j) x])" have "eval r_delay_aux [n, i, x] \" using Suc by simp moreover have "eval r_delay_aux [Suc n, i, x] = eval (Pr 2 (r_constn 1 0) g) [Suc n, i, x]" unfolding r_delay_aux_def g_def z_def by simp ultimately have "eval r_delay_aux [Suc n, i, x] = eval g [n, the (eval r_delay_aux [n, i, x]), i, x]" using r_delay_aux_prim Suc eval_Pr_converg_Suc by (simp add: r_delay_aux_def g_def z_def numeral_3_eq_3) then have "eval r_delay_aux [Suc n, i, x] \= (if ?P n > 0 then Suc n else if \j 0 then Suc (GREATEST j. j < n \ ?P j > 0) else 0)" using g Suc by simp then have "eval r_delay_aux [Suc n, i, x] \= (if \j 0 then Suc (GREATEST j. j < Suc n \ ?P j > 0) else 0)" using Greatest_bounded_Suc[where ?P="?P"] by simp then show ?case by simp qed qed text \The next function simulates $\varphi_i$ on all non-empty prefixes of a list $x$ of length $n$ for at most $n$ steps and outputs the length of the longest prefix for which $\varphi_i$ halts, or zero if $\varphi_i$ does not halt for any such prefix.\ definition "r_delay \ Cn 2 r_delay_aux [Cn 2 r_length [Id 2 1], Id 2 0, Id 2 1]" lemma r_delay_recfn [simp]: "recfn 2 r_delay" unfolding r_delay_def by (simp add: r_delay_aux_prim) lemma r_delay: "eval r_delay [i, x] \= (if \j 0 then Suc (GREATEST j. j < e_length x \ the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0) else 0)" unfolding r_delay_def using r_delay_aux r_delay_aux_prim by simp definition "delay i x \ Some (if \j 0 then Suc (GREATEST j. j < e_length x \ the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0) else 0)" lemma delay_in_R2: "delay \ \\<^sup>2" using r_delay totalI2 R2I delay_def r_delay_recfn by (metis (no_types, lifting) numeral_2_eq_2 option.simps(3)) lemma delay_le_length: "the (delay i x) \ e_length x" proof (cases "\j 0") case True let ?P = "\j. j < e_length x \ the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0" from True have "\j. ?P j" by simp moreover have "\y. ?P y \ y \ e_length x" by simp ultimately have "?P (Greatest ?P)" using GreatestI_ex_nat[where ?P="?P"] by blast then have "Greatest ?P < e_length x" by simp moreover have "delay i x \= Suc (Greatest ?P)" using delay_def True by simp ultimately show ?thesis by auto next case False then show ?thesis using delay_def by auto qed lemma e_take_delay_init: assumes "f \ \" and "the (delay i (f \ n)) > 0" shows "e_take (the (delay i (f \ n))) (f \ n) = f \ (the (delay i (f \ n)) - 1)" using assms e_take_init[of f _ n] length_init[of f n] delay_le_length[of i "f \ n"] by (metis One_nat_def Suc_le_lessD Suc_pred) lemma delay_gr0_converg: assumes "the (delay i x) > 0" shows "\ i (e_take (the (delay i x)) x) \" proof - let ?P = "\j. j < e_length x \ the (eval r_result1 [e_length x, i, e_take (Suc j) x]) > 0" have "\j. ?P j" proof (rule ccontr) assume "\ (\j. ?P j)" then have "delay i x \= 0" using delay_def by simp with assms show False by simp qed then have d: "the (delay i x) = Suc (Greatest ?P)" using delay_def by simp moreover have "\y. ?P y \ y \ e_length x" by simp ultimately have "?P (Greatest ?P)" using `\j. ?P j` GreatestI_ex_nat[where ?P="?P"] by blast then have "the (eval r_result1 [e_length x, i, e_take (Suc (Greatest ?P)) x]) > 0" by simp then have "the (eval r_result1 [e_length x, i, e_take (the (delay i x)) x]) > 0" using d by simp then show ?thesis using r_result1_diverg_phi by fastforce qed lemma delay_unbounded: fixes n :: nat assumes "f \ \" and "\n. \ i (f \ n) \" shows "\m. the (delay i (f \ m)) > n" proof - from assms have "\t. the (eval r_result1 [t, i, f \ n]) > 0" using r_result1_converg_phi by (metis le_refl option.exhaust_sel option.sel zero_less_Suc) then obtain t where t: "the (eval r_result1 [t, i, f \ n]) > 0" by auto let ?m = "max n t" have "Suc ?m \ t" by simp have m: "the (eval r_result1 [Suc ?m, i, f \ n]) > 0" proof - let ?w = "eval r_result1 [t, i, f \ n]" obtain v where v: "?w \= Suc v" using t assms(2) r_result1_bivalent_phi by fastforce have "eval r_result1 [Suc ?m, i, f \ n] = ?w" using v t r_result1_saturating' `Suc ?m \ t` le_Suc_ex by fastforce then show ?thesis using t by simp qed let ?x = "f \ ?m" have "the (delay i ?x) > n" proof - let ?P = "\j. j < e_length ?x \ the (eval r_result1 [e_length ?x, i, e_take (Suc j) ?x]) > 0" have "e_length ?x = Suc ?m" by simp moreover have "e_take (Suc n) ?x = f \ n" using assms(1) e_take_init by auto ultimately have "?P n" using m by simp have "\y. ?P y \ y \ e_length ?x" by simp with `?P n` have "n \ (Greatest ?P)" using Greatest_le_nat[of ?P n "e_length ?x"] by simp moreover have "the (delay i ?x) = Suc (Greatest ?P)" using delay_def `?P n` by auto ultimately show ?thesis by simp qed then show ?thesis by auto qed lemma delay_monotone: assumes "f \ \" and "n\<^sub>1 \ n\<^sub>2" shows "the (delay i (f \ n\<^sub>1)) \ the (delay i (f \ n\<^sub>2))" (is "the (delay i ?x1) \ the (delay i ?x2)") proof (cases "the (delay i (f \ n\<^sub>1)) = 0") case True then show ?thesis by simp next case False let ?P1 = "\j. j < e_length ?x1 \ the (eval r_result1 [e_length ?x1, i, e_take (Suc j) ?x1]) > 0" let ?P2 = "\j. j < e_length ?x2 \ the (eval r_result1 [e_length ?x2, i, e_take (Suc j) ?x2]) > 0" from False have d1: "the (delay i ?x1) = Suc (Greatest ?P1)" "\j. ?P1 j" using delay_def option.collapse by fastforce+ moreover have "\y. ?P1 y \ y \ e_length ?x1" by simp ultimately have *: "?P1 (Greatest ?P1)" using GreatestI_ex_nat[of ?P1] by blast let ?j = "Greatest ?P1" from * have "?j < e_length ?x1" by auto then have 1: "e_take (Suc ?j) ?x1 = e_take (Suc ?j) ?x2" using assms e_take_init by auto from * have 2: "?j < e_length ?x2" using assms(2) by auto with 1 * have "the (eval r_result1 [e_length ?x1, i, e_take (Suc ?j) ?x2]) > 0" by simp moreover have "e_length ?x1 \ e_length ?x2" using assms(2) by auto ultimately have "the (eval r_result1 [e_length ?x2, i, e_take (Suc ?j) ?x2]) > 0" using r_result1_saturating_the by simp with 2 have "?P2 ?j" by simp then have d2: "the (delay i ?x2) = Suc (Greatest ?P2)" using delay_def by auto have "\y. ?P2 y \ y \ e_length ?x2" by simp with `?P2 ?j` have "?j \ (Greatest ?P2)" using Greatest_le_nat[of ?P2] by blast with d1 d2 show ?thesis by simp qed lemma delay_unbounded_monotone: fixes n :: nat assumes "f \ \" and "\n. \ i (f \ n) \" shows "\m\<^sub>0. \m\m\<^sub>0. the (delay i (f \ m)) > n" proof - from assms delay_unbounded obtain m\<^sub>0 where "the (delay i (f \ m\<^sub>0)) > n" by blast then have "\m\m\<^sub>0. the (delay i (f \ m)) > n" using assms(1) delay_monotone order.strict_trans2 by blast then show ?thesis by auto qed text \Now we can define a function that simulates an arbitrary strategy $\varphi_i$ in a delayed way. The parameter $d$ is the default hypothesis for when $\varphi_i$ does not halt within the time bound for any prefix.\ definition r_totalizer :: "nat \ recf" where "r_totalizer d \ Cn 2 (r_lifz (r_constn 1 d) (Cn 2 r_phi [Id 2 0, Cn 2 r_take [Cn 2 r_delay [Id 2 0, Id 2 1], Id 2 1]])) [Cn 2 r_delay [Id 2 0, Id 2 1], Id 2 0, Id 2 1]" lemma r_totalizer_recfn: "recfn 2 (r_totalizer d)" unfolding r_totalizer_def by simp lemma r_totalizer: "eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then Some d else \ i (e_take (the (delay i x)) x))" proof - let ?i = "Cn 2 r_delay [Id 2 0, Id 2 1]" have "eval ?i [i, x] = eval r_delay [i, x]" for i x using r_delay_recfn by simp then have i: "eval ?i [i, x] = delay i x" for i x using r_delay by (simp add: delay_def) let ?t = "r_constn 1 d" have t: "eval ?t [i, x] \= d" for i x by simp let ?e1 = "Cn 2 r_take [?i, Id 2 1]" let ?e = "Cn 2 r_phi [Id 2 0, ?e1]" have "eval ?e1 [i, x] = eval r_take [the (delay i x), x]" for i x using r_delay i delay_def by simp then have "eval ?e1 [i, x] \= e_take (the (delay i x)) x" for i x using delay_le_length by simp then have e: "eval ?e [i, x] = \ i (e_take (the (delay i x)) x)" using phi_def by simp let ?z = "r_lifz ?t ?e" have recfn_te: "recfn 2 ?t" "recfn 2 ?e" by simp_all then have "eval (r_totalizer d) [i, x] = eval (r_lifz ?t ?e) [the (delay i x), i, x]" for i x unfolding r_totalizer_def using i r_totalizer_recfn delay_def by simp then have "eval (r_totalizer d) [i, x] = (if the (delay i x) = 0 then eval ?t [i, x] else eval ?e [i, x])" for i x using recfn_te by simp then show ?thesis using t e by simp qed lemma r_totalizer_total: "total (r_totalizer d)" proof (rule totalI2) show "recfn 2 (r_totalizer d)" using r_totalizer_recfn by simp show "\x y. eval (r_totalizer d) [x, y] \" using r_totalizer delay_gr0_converg by simp qed definition totalizer :: "nat \ partial2" where "totalizer d i x \ if the (delay i x) = 0 then Some d else \ i (e_take (the (delay i x)) x)" lemma totalizer_init: assumes "f \ \" shows "totalizer d i (f \ n) = (if the (delay i (f \ n)) = 0 then Some d else \ i (f \ (the (delay i (f \ n)) - 1)))" using assms e_take_delay_init by (simp add: totalizer_def) lemma totalizer_in_R2: "totalizer d \ \\<^sup>2" using totalizer_def r_totalizer r_totalizer_total R2I r_totalizer_recfn by metis text \For LIM, @{term totalizer} works with every default hypothesis $d$.\ lemma lemma_R_for_Lim: assumes "learn_lim \ U (\ i)" shows "learn_lim \ U (totalizer d i)" proof (rule learn_limI) show env: "environment \ U (totalizer d i)" using assms learn_limE(1) totalizer_in_R2 by auto show "\j. \ j = f \ (\\<^sup>\n. totalizer d i (f \ n) \= j)" if "f \ U" for f proof - have "f \ \" using assms env that by auto from assms learn_limE obtain j n\<^sub>0 where j: "\ j = f" and n0: "\n\n\<^sub>0. (\ i) (f \ n) \= j" using `f \ U` by metis obtain m\<^sub>0 where m0: "\m\m\<^sub>0. the (delay i (f \ m)) > n\<^sub>0" using delay_unbounded_monotone `f \ \` \f \ U\ assms learn_limE(1) by blast then have "\m\m\<^sub>0. totalizer d i (f \ m) = \ i (e_take (the (delay i (f \ m))) (f \ m))" using totalizer_def by auto then have "\m\m\<^sub>0. totalizer d i (f \ m) = \ i (f \ (the (delay i (f \ m)) - 1))" using e_take_delay_init m0 `f \ \` by auto with m0 n0 have "\m\m\<^sub>0. totalizer d i (f \ m) \= j" by auto with j show ?thesis by auto qed qed text \The effective version of Lemma~R for LIM states that there is a total recursive function computing Gödel numbers of total strategies from those of arbitrary strategies.\ lemma lemma_R_for_Lim_effective: "\g\\. \i. \ (the (g i)) \ \ \ (\U \. learn_lim \ U (\ i) \ learn_lim \ U (\ (the (g i))))" proof - have "totalizer 0 \ \

\<^sup>2" using totalizer_in_R2 by auto then obtain g where g: "g \ \" "\i. (totalizer 0) i = \ (the (g i))" using numbering_translation_for_phi by blast with totalizer_in_R2 have "\i. \ (the (g i)) \ \" by (metis R2_proj_R1) moreover from g(2) lemma_R_for_Lim[where ?d=0] have "\i U \. learn_lim \ U (\ i) \ learn_lim \ U (\ (the (g i)))" by simp ultimately show ?thesis using g(1) by blast qed text \In order for us to use the previous lemma, we need a function that performs the actual computation:\ definition "r_limr \ SOME g. recfn 1 g \ total g \ (\i. \ (the (eval g [i])) \ \ \ (\U \. learn_lim \ U (\ i) \ learn_lim \ U (\ (the (eval g [i])))))" lemma r_limr_recfn: "recfn 1 r_limr" and r_limr_total: "total r_limr" and r_limr: "\ (the (eval r_limr [i])) \ \" "learn_lim \ U (\ i) \ learn_lim \ U (\ (the (eval r_limr [i])))" proof - let ?P = "\g. g \ \ \ (\i. \ (the (g i)) \ \ \ (\U \. learn_lim \ U (\ i) \ learn_lim \ U (\ (the (g i)))))" let ?Q = "\g. recfn 1 g \ total g \ (\i. \ (the (eval g [i])) \ \ \ (\U \. learn_lim \ U (\ i) \ learn_lim \ U (\ (the (eval g [i])))))" have "\g. ?P g" using lemma_R_for_Lim_effective by auto then obtain g where "?P g" by auto then obtain g' where g': "recfn 1 g'" "total g'" "\i. eval g' [i] = g i" by blast with `?P g` have "?Q g'" by simp with r_limr_def someI_ex[of ?Q] show "recfn 1 r_limr" "total r_limr" "\ (the (eval r_limr [i])) \ \" "learn_lim \ U (\ i) \ learn_lim \ U (\ (the (eval r_limr [i])))" by auto qed text \For BC, too, @{term totalizer} works with every default hypothesis $d$.\ lemma lemma_R_for_BC: assumes "learn_bc \ U (\ i)" shows "learn_bc \ U (totalizer d i)" proof (rule learn_bcI) show env: "environment \ U (totalizer d i)" using assms learn_bcE(1) totalizer_in_R2 by auto show "\n\<^sub>0. \n\n\<^sub>0. \ (the (totalizer d i (f \ n))) = f" if "f \ U" for f proof - have "f \ \" using assms env that by auto obtain n\<^sub>0 where n0: "\n\n\<^sub>0. \ (the ((\ i) (f \ n))) = f" using assms learn_bcE `f \ U` by metis obtain m\<^sub>0 where m0: "\m\m\<^sub>0. the (delay i (f \ m)) > n\<^sub>0" using delay_unbounded_monotone `f \ \` \f \ U\ assms learn_bcE(1) by blast then have "\m\m\<^sub>0. totalizer d i (f \ m) = \ i (e_take (the (delay i (f \ m))) (f \ m))" using totalizer_def by auto then have "\m\m\<^sub>0. totalizer d i (f \ m) = \ i (f \ (the (delay i (f \ m)) - 1))" using e_take_delay_init m0 `f \ \` by auto with m0 n0 have "\m\m\<^sub>0. \ (the (totalizer d i (f \ m))) = f" by auto then show ?thesis by auto qed qed corollary lemma_R_for_BC_simple: assumes "learn_bc \ U s" shows "\s'\\. learn_bc \ U s'" using assms lemma_R_for_BC totalizer_in_R2 learn_bcE by (metis R2_proj_R1 learn_bcE(1) phi_universal) text \For FIN the default hypothesis of @{term totalizer} must be zero, signalling ``don't know yet''.\ lemma lemma_R_for_FIN: assumes "learn_fin \ U (\ i)" shows "learn_fin \ U (totalizer 0 i)" proof (rule learn_finI) show env: "environment \ U (totalizer 0 i)" using assms learn_finE(1) totalizer_in_R2 by auto show "\j n\<^sub>0. \ j = f \ (\n0. totalizer 0 i (f \ n) \= 0) \ (\n\n\<^sub>0. totalizer 0 i (f \ n) \= Suc j)" if "f \ U" for f proof - have "f \ \" using assms env that by auto from assms learn_finE[of \ U "\ i"] obtain j where j: "\ j = f" and ex_n0: "\n\<^sub>0. (\n0. (\ i) (f \ n) \= 0) \ (\n\n\<^sub>0. (\ i) (f \ n) \= Suc j)" using `f \ U` by blast let ?Q = "\n\<^sub>0. (\n0. (\ i) (f \ n) \= 0) \ (\n\n\<^sub>0. (\ i) (f \ n) \= Suc j)" define n\<^sub>0 where "n\<^sub>0 = Least ?Q" with ex_n0 have n0: "?Q n\<^sub>0" "\n0. \ ?Q n" using LeastI_ex[of ?Q] not_less_Least[of _ ?Q] by blast+ define m\<^sub>0 where "m\<^sub>0 = (LEAST m\<^sub>0. \m\m\<^sub>0. the (delay i (f \ m)) > n\<^sub>0)" (is "m\<^sub>0 = Least ?P") moreover have "\m\<^sub>0. \m\m\<^sub>0. the (delay i (f \ m)) > n\<^sub>0" using delay_unbounded_monotone `f\\` \f \ U\ assms learn_finE(1) by simp ultimately have m0: "?P m\<^sub>0" "\m0. \ ?P m" using LeastI_ex[of ?P] not_less_Least[of _ ?P] by blast+ then have "\m\m\<^sub>0. totalizer 0 i (f \ m) = \ i (e_take (the (delay i (f \ m))) (f \ m))" using totalizer_def by auto then have "\m\m\<^sub>0. totalizer 0 i (f \ m) = \ i (f \ (the (delay i (f \ m)) - 1))" using e_take_delay_init m0 `f\\` by auto with m0 n0 have "\m\m\<^sub>0. totalizer 0 i (f \ m) \= Suc j" by auto moreover have "totalizer 0 i (f \ m) \= 0" if "m < m\<^sub>0" for m proof (cases "the (delay i (f \ m)) = 0") case True then show ?thesis by (simp add: totalizer_def) next case False then have "the (delay i (f \ m)) \ n\<^sub>0" using m0 that `f \ \` delay_monotone by (meson leI order.strict_trans2) then show ?thesis using \f \ \\ n0(1) totalizer_init by (simp add: Suc_le_lessD) qed ultimately show ?thesis using j by auto qed qed subsection \Weaker Lemma R for CP and TOTAL\ text \For TOTAL the default hypothesis used by @{term totalizer} depends on the hypothesis space, because it must refer to a total function in that space. Consequently the total strategy depends on the hypothesis space, which makes this form of Lemma~R weaker than the ones in the previous section.\ lemma lemma_R_for_TOTAL: fixes \ :: partial2 shows "\d. \U. \i. learn_total \ U (\ i) \ learn_total \ U (totalizer d i)" proof (cases "\d. \ d \ \") case True then obtain d where "\ d \ \" by auto have "learn_total \ U (totalizer d i)" if "learn_total \ U (\ i)" for U i proof (rule learn_totalI) show env: "environment \ U (totalizer d i)" using that learn_totalE(1) totalizer_in_R2 by auto show "\f. f \ U \ \j. \ j = f \ (\\<^sup>\n. totalizer d i (f \ n) \= j)" using that learn_total_def lemma_R_for_Lim[where ?d=d] learn_limE(2) by metis show "\ (the (totalizer d i (f \ n))) \ \" if "f \ U" for f n proof (cases "the (delay i (f \ n)) = 0") case True then show ?thesis using totalizer_def `\ d \ \` by simp next case False have "f \ \" using that env by auto then show ?thesis using False that `learn_total \ U (\ i)` totalizer_init learn_totalE(3) by simp qed qed then show ?thesis by auto next case False then show ?thesis using learn_total_def lemma_R_for_Lim by auto qed corollary lemma_R_for_TOTAL_simple: assumes "learn_total \ U s" shows "\s'\\. learn_total \ U s'" using assms lemma_R_for_TOTAL totalizer_in_R2 by (metis R2_proj_R1 learn_totalE(1) phi_universal) text \For CP the default hypothesis used by @{term totalizer} depends on both the hypothesis space and the class. Therefore the total strategy depends on both the the hypothesis space and the class, which makes Lemma~R for CP even weaker than the one for TOTAL.\ lemma lemma_R_for_CP: fixes \ :: partial2 and U :: "partial1 set" assumes "learn_cp \ U (\ i)" shows "\d. learn_cp \ U (totalizer d i)" proof (cases "U = {}") case True then show ?thesis using assms learn_cp_def lemma_R_for_Lim by auto next case False then obtain f where "f \ U" by auto from `f \ U` obtain d where "\ d = f" using learn_cpE(2)[OF assms] by auto with `f \ U` have "\ d \ U" by simp have "learn_cp \ U (totalizer d i)" proof (rule learn_cpI) show env: "environment \ U (totalizer d i)" using assms learn_cpE(1) totalizer_in_R2 by auto show "\f. f \ U \ \j. \ j = f \ (\\<^sup>\n. totalizer d i (f \ n) \= j)" using assms learn_cp_def lemma_R_for_Lim[where ?d=d] learn_limE(2) by metis show "\ (the (totalizer d i (f \ n))) \ U" if "f \ U" for f n proof (cases "the (delay i (f \ n)) = 0") case True then show ?thesis using totalizer_def `\ d \ U` by simp next case False then show ?thesis using that env assms totalizer_init learn_cpE(3) by auto qed qed then show ?thesis by auto qed subsection \No Lemma R for CONS\ text \This section demonstrates that the class $V_{01}$ of all total recursive functions $f$ where $f(0)$ or $f(1)$ is a Gödel number of $f$ can be consistently learned in the limit, but not by a total strategy. This implies that Lemma~R does not hold for CONS.\ definition V01 :: "partial1 set" ("V\<^sub>0\<^sub>1") where "V\<^sub>0\<^sub>1 = {f. f \ \ \ (\ (the (f 0)) = f \ \ (the (f 1)) = f)}" subsubsection \No total CONS strategy for @{term "V\<^sub>0\<^sub>1"}\label{s:v01_not_total}\ text \In order to show that no total strategy can learn @{term "V\<^sub>0\<^sub>1"} we construct, for each total strategy $S$, one or two functions in @{term "V\<^sub>0\<^sub>1"} such that $S$ fails for at least one of them. At the core of this construction is a process that given a total recursive strategy $S$ and numbers $z, i, j \in \mathbb{N}$ builds a function $f$ as follows: Set $f(0) = i$ and $f(1) = j$. For $x\geq1$: \begin{enumerate} \item[(a)] Check whether $S$ changes its hypothesis when $f^x$ is extended by 0, that is, if $S(f^x) \neq S(f^x0)$. If so, set $f(x+1) = 0$. \item[(b)] Otherwise check if $S$ changes its hypothesis when $f^x$ is extended by $1$, that is, if $S(f^x) \neq S(f^x1)$. If so, set $f(x+1) = 1$. \item[(c)] If neither happens, set $f(x+1) = z$. \end{enumerate} In other words, as long as we can force $S$ to change its hypothesis by extending the function by 0 or 1, we do just that. Now there are two cases: \begin{enumerate} \item[Case 1.] For all $x\geq1$ either (a) or (b) occurs; then $S$ changes its hypothesis on $f$ all the time and thus does not learn $f$ in the limit (not to mention consistently). The value of $z$ makes no difference in this case. \item[Case 2.] For some minimal $x$, (c) occurs, that is, there is an $f^x$ such that $h := S(f^x) = S(f^x0) = S(f^x1)$. But the hypothesis $h$ cannot be consistent with both prefixes $f^x0$ and $f^x1$. Running the process once with $z = 0$ and once with $z = 1$ yields two functions starting with $f^x0$ and $f^x1$, respectively, such that $S$ outputs the same hypothesis, $h$, on both prefixes and thus cannot be consistent for both functions. \end{enumerate} This process is computable because $S$ is total. The construction does not work if we only assume $S$ to be a CONS strategy for $V_{01}$, because we need to be able to apply $S$ to prefixes not in $V_{01}$. The parameters $i$ and $j$ provide flexibility to find functions built by the above process that are actually in $V_{01}$. To this end we will use Smullyan's double fixed-point theorem.\ context fixes s :: partial1 assumes s_in_R1 [simp, intro]: "s \ \" begin text \The function @{term prefixes} constructs prefixes according to the aforementioned process.\ fun prefixes :: "nat \ nat \ nat \ nat \ nat list" where "prefixes z i j 0 = [i]" | "prefixes z i j (Suc x) = prefixes z i j x @ [if x = 0 then j else if s (list_encode (prefixes z i j x @ [0])) \ s (list_encode (prefixes z i j x)) then 0 else if s (list_encode (prefixes z i j x @ [1])) \ s (list_encode (prefixes z i j x)) then 1 else z]" lemma prefixes_length: "length (prefixes z i j x) = Suc x" by (induction x) simp_all text \The functions @{term[names_short] "adverse z i j"} are the functions constructed by @{term[names_short] "prefixes"}.\ definition adverse :: "nat \ nat \ nat \ nat \ nat option" where "adverse z i j x \ Some (last (prefixes z i j x))" lemma init_adverse_eq_prefixes: "(adverse z i j) \ n = list_encode (prefixes z i j n)" proof - have "prefix (adverse z i j) n = prefixes z i j n" proof (induction n) case 0 then show ?case using adverse_def prefixes_length prefixI' by fastforce next case (Suc n) then show ?case using adverse_def by (simp add: prefix_Suc) qed then show ?thesis by (simp add: init_def) qed lemma adverse_at_01: "adverse z i j 0 \= i" "adverse z i j 1 \= j" by (auto simp add: adverse_def) text \Had we introduced ternary partial recursive functions, the @{term[names_short] "adverse z"} functions would be among them.\ lemma adverse_in_R3: "\r. recfn 3 r \ total r \ (\i j x. eval r [i, j, x]) = adverse z" proof - obtain rs where rs: "recfn 1 rs" "total rs" "(\x. eval rs [x]) = s" using R1E by auto have s_total: "\x. s x \" by simp define f where "f = Cn 2 r_singleton_encode [Id 2 0]" then have "recfn 2 f" by simp have f: "\i j. eval f [i, j] \= list_encode [i]" unfolding f_def by simp define ch1 where "ch1 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [Id 4 1, r_constn 3 1]], Cn 4 rs [Id 4 1], r_dummy 3 (r_const z), r_constn 3 1]" then have ch1: "recfn 4 ch1" "total ch1" using Cn_total prim_recfn_total rs by auto define ch0 where "ch0 = Cn 4 r_ifeq [Cn 4 rs [Cn 4 r_snoc [Id 4 1, r_constn 3 0]], Cn 4 rs [Id 4 1], ch1, r_constn 3 0]" then have ch0_total: "total ch0" "recfn 4 ch0" using Cn_total prim_recfn_total rs ch1 by auto have "eval ch1 [l, v, i, j] \= (if s (e_snoc v 1) = s v then z else 1)" for l v i j proof - have "eval ch1 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 1)), the (s v), z, 1]" unfolding ch1_def using rs by auto then show ?thesis by (simp add: s_total option.expand) qed moreover have "eval ch0 [l, v, i, j] \= (if s (e_snoc v 0) = s v then the (eval ch1 [l, v, i, j]) else 0)" for l v i j proof - have "eval ch0 [l, v, i, j] = eval r_ifeq [the (s (e_snoc v 0)), the (s v), the (eval ch1 [l, v, i, j]), 0]" unfolding ch0_def using rs ch1 by auto then show ?thesis by (simp add: s_total option.expand) qed ultimately have ch0: "\l v i j. eval ch0 [l, v, i, j] \= (if s (e_snoc v 0) \ s v then 0 else if s (e_snoc v 1) \ s v then 1 else z)" by simp define app where "app = Cn 4 r_ifz [Id 4 0, Id 4 3, ch0]" then have "recfn 4 app" "total app" using ch0_total totalI4 by auto have "eval app [l, v, i, j] \= (if l = 0 then j else the (eval ch0 [l, v, i, j]))" for l v i j unfolding app_def using ch0_total by simp with ch0 have app: "\l v i j. eval app [l, v, i, j] \= (if l = 0 then j else if s (e_snoc v 0) \ s v then 0 else if s (e_snoc v 1) \ s v then 1 else z)" by simp define g where "g = Cn 4 r_snoc [Id 4 1, app]" with app have g: "\l v i j. eval g [l, v, i, j] \= e_snoc v (if l = 0 then j else if s (e_snoc v 0) \ s v then 0 else if s (e_snoc v 1) \ s v then 1 else z)" using `recfn 4 app` by auto from g_def have "recfn 4 g" "total g" using `recfn 4 app` `total app` Cn_total Mn_free_imp_total by auto define b where "b = Pr 2 f g" then have "recfn 3 b" using `recfn 2 f` `recfn 4 g` by simp have b: "eval b [x, i, j] \= list_encode (prefixes z i j x)" for x i j proof (induction x) case 0 then show ?case unfolding b_def using f `recfn 2 f` \recfn 4 g\ by simp next case (Suc x) then have "eval b [Suc x, i, j] = eval g [x, the (eval b [x, i, j]), i, j]" using b_def `recfn 3 b` by simp also have "... \= (let v = list_encode (prefixes z i j x) in e_snoc v (if x = 0 then j else if s (e_snoc v 0) \ s v then 0 else if s (e_snoc v 1) \ s v then 1 else z))" using g Suc by simp also have "... \= (let v = list_encode (prefixes z i j x) in e_snoc v (if x = 0 then j else if s (list_encode (prefixes z i j x @ [0])) \ s v then 0 else if s (list_encode (prefixes z i j x @ [1])) \ s v then 1 else z))" using list_decode_encode by presburger finally show ?case by simp qed define b' where "b' = Cn 3 b [Id 3 2, Id 3 0, Id 3 1]" then have "recfn 3 b'" using `recfn 3 b` by simp with b have b': "\i j x. eval b' [i, j, x] \= list_encode (prefixes z i j x)" using b'_def by simp define r where "r = Cn 3 r_last [b']" then have "recfn 3 r" using `recfn 3 b'` by simp with b' have "\i j x. eval r [i, j, x] \= last (prefixes z i j x)" using r_def prefixes_length by auto moreover from this have "total r" using totalI3 `recfn 3 r` by simp ultimately have "(\i j x. eval r [i, j, x]) = adverse z" unfolding adverse_def by simp with `recfn 3 r` `total r` show ?thesis by auto qed lemma adverse_in_R1: "adverse z i j \ \" proof - from adverse_in_R3 obtain r where r: "recfn 3 r" "total r" "(\i j x. eval r [i, j, x]) = adverse z" by blast define rij where "rij = Cn 1 r [r_const i, r_const j, Id 1 0]" then have "recfn 1 rij" "total rij" using r(1,2) Cn_total Mn_free_imp_total by auto from rij_def have "\x. eval rij [x] = eval r [i, j, x]" using r(1) by auto with r(3) have "\x. eval rij [x] = adverse z i j x" by metis with `recfn 1 rij` `total rij` show ?thesis by auto qed text \Next we show that for every $z$ there are $i$, $j$ such that @{term[names_short] "adverse z i j \ V\<^sub>0\<^sub>1"}. The first step is to show that for every $z$, Gödel numbers for @{term[names_short] "adverse z i j"} can be computed uniformly from $i$ and $j$.\ lemma phi_translate_adverse: "\f\\\<^sup>2.\i j. \ (the (f i j)) = adverse z i j" proof - obtain r where r: "recfn 3 r" "total r" "(\i j x. eval r [i, j, x]) = adverse z" using adverse_in_R3 by blast let ?p = "encode r" define rf where "rf = Cn 2 (r_smn 1 2) [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]" then have "recfn 2 rf" and "total rf" using Mn_free_imp_total by simp_all define f where "f \ \i j. eval rf [i, j]" with `recfn 2 rf` `total rf` have "f \ \\<^sup>2" by auto have rf: "eval rf [i, j] = eval (r_smn 1 2) [?p, i, j]" for i j unfolding rf_def by simp { fix i j x have "\ (the (f i j)) x = eval r_phi [the (f i j), x]" using phi_def by simp also have "... = eval r_phi [the (eval rf [i, j]), x]" using f_def by simp also have "... = eval (r_universal 1) [the (eval (r_smn 1 2) [?p, i, j]), x]" using rf r_phi_def by simp also have "... = eval (r_universal (2 + 1)) (?p # [i, j] @ [x])" using smn_lemma[of 1 "[i, j]" 2 "[x]"] by simp also have "... = eval (r_universal 3) [?p, i, j, x]" by simp also have "... = eval r [i, j, x]" - using r_universal r by simp + using r_universal r by force also have "... = adverse z i j x" using r(3) by metis finally have "\ (the (f i j)) x = adverse z i j x" . } with `f \ \\<^sup>2` show ?thesis by blast qed text \The second, and final, step is to apply Smullyan's double fixed-point theorem to show the existence of @{term[names_short] adverse} functions in @{term "V\<^sub>0\<^sub>1"}.\ lemma adverse_in_V01: "\m n. adverse 0 m n \ V\<^sub>0\<^sub>1 \ adverse 1 m n \ V\<^sub>0\<^sub>1" proof - obtain f\<^sub>0 where f0: "f\<^sub>0 \ \\<^sup>2" "\i j. \ (the (f\<^sub>0 i j)) = adverse 0 i j" using phi_translate_adverse[of 0] by auto obtain f\<^sub>1 where f1: "f\<^sub>1 \ \\<^sup>2" "\i j. \ (the (f\<^sub>1 i j)) = adverse 1 i j" using phi_translate_adverse[of 1] by auto obtain m n where "\ m = \ (the (f\<^sub>0 m n))" and "\ n = \ (the (f\<^sub>1 m n))" using smullyan_double_fixed_point[OF f0(1) f1(1)] by blast with f0(2) f1(2) have "\ m = adverse 0 m n" and "\ n = adverse 1 m n" by simp_all moreover have "the (adverse 0 m n 0) = m" and "the (adverse 1 m n 1) = n" using adverse_at_01 by simp_all ultimately have "\ (the (adverse 0 m n 0)) = adverse 0 m n" "\ (the (adverse 1 m n 1)) = adverse 1 m n" by simp_all moreover have "adverse 0 m n \ \" and "adverse 1 m n \ \" using adverse_in_R1 by simp_all ultimately show ?thesis using V01_def by auto qed text \Before we prove the main result of this section we need some lemmas regarding the shape of the @{term[names_short] adverse} functions and hypothesis changes of the strategy.\ lemma adverse_Suc: assumes "x > 0" shows "adverse z i j (Suc x) \= (if s (e_snoc ((adverse z i j) \ x) 0) \ s ((adverse z i j) \ x) then 0 else if s (e_snoc ((adverse z i j) \ x) 1) \ s ((adverse z i j) \ x) then 1 else z)" proof - have "adverse z i j (Suc x) \= (if s (list_encode (prefixes z i j x @ [0])) \ s (list_encode (prefixes z i j x)) then 0 else if s (list_encode (prefixes z i j x @ [1])) \ s (list_encode (prefixes z i j x)) then 1 else z)" using assms adverse_def by simp then show ?thesis by (simp add: init_adverse_eq_prefixes) qed text \The process in the proof sketch (page~\pageref{s:v01_not_total}) consists of steps (a), (b), and (c). The next abbreviation is true iff.\ step (a) or (b) applies.\ abbreviation "hyp_change z i j x \ s (e_snoc ((adverse z i j) \ x) 0) \ s ((adverse z i j) \ x) \ s (e_snoc ((adverse z i j) \ x) 1) \ s ((adverse z i j) \ x)" text \If step (c) applies, the process appends $z$.\ lemma adverse_Suc_not_hyp_change: assumes "x > 0" and "\ hyp_change z i j x" shows "adverse z i j (Suc x) \= z" using assms adverse_Suc by simp text \While (a) or (b) applies, the process appends a value that forces $S$ to change its hypothesis.\ lemma while_hyp_change: assumes "\x\n. x > 0 \ hyp_change z i j x" shows "\x\Suc n. adverse z i j x = adverse z' i j x" using assms proof (induction n) case 0 then show ?case by (simp add: adverse_def le_Suc_eq) next case (Suc n) then have "\x\n. x > 0 \ hyp_change z i j x" by simp with Suc have "\x\Suc n. x > 0 \ adverse z i j x = adverse z' i j x" by simp moreover have "adverse z i j 0 = adverse z' i j 0" using adverse_at_01 by simp ultimately have zz': "\x\Suc n. adverse z i j x = adverse z' i j x" by auto moreover have "adverse z i j \ \" "adverse z' i j \ \" using adverse_in_R1 by simp_all ultimately have init_zz': "(adverse z i j) \ (Suc n) = (adverse z' i j) \ (Suc n)" using init_eqI by blast have "adverse z i j (Suc (Suc n)) = adverse z' i j (Suc (Suc n))" proof (cases "s (e_snoc ((adverse z i j) \ (Suc n)) 0) \ s ((adverse z i j) \ (Suc n))") case True then have "s (e_snoc ((adverse z' i j) \ (Suc n)) 0) \ s ((adverse z' i j) \ (Suc n))" using init_zz' by simp then have "adverse z' i j (Suc (Suc n)) \= 0" by (simp add: adverse_Suc) moreover have "adverse z i j (Suc (Suc n)) \= 0" using True by (simp add: adverse_Suc) ultimately show ?thesis by simp next case False then have "s (e_snoc ((adverse z' i j) \ (Suc n)) 0) = s ((adverse z' i j) \ (Suc n))" using init_zz' by simp then have "adverse z' i j (Suc (Suc n)) \= 1" using init_zz' Suc.prems adverse_Suc by (smt le_refl zero_less_Suc) moreover have "adverse z i j (Suc (Suc n)) \= 1" using False Suc.prems adverse_Suc by auto ultimately show ?thesis by simp qed with zz' show ?case using le_SucE by blast qed text \The next result corresponds to Case~1 from the proof sketch.\ lemma always_hyp_change_no_lim: assumes "\x>0. hyp_change z i j x" shows "\ learn_lim \ {adverse z i j} s" proof (rule infinite_hyp_changes_not_Lim[of "adverse z i j"]) show "adverse z i j \ {adverse z i j}" by simp show "\n. \m\<^sub>1>n. \m\<^sub>2>n. s (adverse z i j \ m\<^sub>1) \ s (adverse z i j \ m\<^sub>2)" proof fix n from assms obtain m\<^sub>1 where m1: "m\<^sub>1 > n" "hyp_change z i j m\<^sub>1" by auto have "s (adverse z i j \ m\<^sub>1) \ s (adverse z i j \ (Suc m\<^sub>1))" proof (cases "s (e_snoc ((adverse z i j) \ m\<^sub>1) 0) \ s ((adverse z i j) \ m\<^sub>1)") case True then have "adverse z i j (Suc m\<^sub>1) \= 0" using m1 adverse_Suc by simp then have "(adverse z i j) \ (Suc m\<^sub>1) = e_snoc ((adverse z i j) \ m\<^sub>1) 0" by (simp add: init_Suc_snoc) with True show ?thesis by simp next case False then have "adverse z i j (Suc m\<^sub>1) \= 1" using m1 adverse_Suc by simp then have "(adverse z i j) \ (Suc m\<^sub>1) = e_snoc ((adverse z i j) \ m\<^sub>1) 1" by (simp add: init_Suc_snoc) with False m1(2) show ?thesis by simp qed then show "\m\<^sub>1>n. \m\<^sub>2>n. s (adverse z i j \ m\<^sub>1) \ s (adverse z i j \ m\<^sub>2)" using less_SucI m1(1) by blast qed qed text \The next result corresponds to Case~2 from the proof sketch.\ lemma no_hyp_change_no_cons: assumes "x > 0" and "\ hyp_change z i j x" shows "\ learn_cons \ {adverse 0 i j, adverse 1 i j} s" proof - let ?P = "\x. x > 0 \ \ hyp_change z i j x" define xmin where "xmin = Least ?P" with assms have xmin: "?P xmin" "\x. x < xmin \ \ ?P x" using LeastI[of ?P] not_less_Least[of _ ?P] by simp_all then have "xmin > 0" by simp have "\x\xmin - 1. x > 0 \ hyp_change z i j x" using xmin by (metis One_nat_def Suc_pred le_imp_less_Suc) then have "\x\xmin. adverse z i j x = adverse 0 i j x" "\x\xmin. adverse z i j x = adverse 1 i j x" using while_hyp_change[of "xmin - 1" z i j 0] using while_hyp_change[of "xmin - 1" z i j 1] by simp_all then have init_z0: "(adverse z i j) \ xmin = (adverse 0 i j) \ xmin" and init_z1: "(adverse z i j) \ xmin = (adverse 1 i j) \ xmin" using adverse_in_R1 init_eqI by blast+ then have a0: "adverse 0 i j (Suc xmin) \= 0" and a1: "adverse 1 i j (Suc xmin) \= 1" using adverse_Suc_not_hyp_change xmin(1) init_z1 by metis+ then have i0: "(adverse 0 i j) \ (Suc xmin) = e_snoc ((adverse z i j) \ xmin) 0" and i1: "(adverse 1 i j) \ (Suc xmin) = e_snoc ((adverse z i j) \ xmin) 1" using init_z0 init_z1 by (simp_all add: init_Suc_snoc) moreover have "s (e_snoc ((adverse z i j) \ xmin) 0) = s ((adverse z i j) \ xmin)" "s (e_snoc ((adverse z i j) \ xmin) 1) = s ((adverse z i j) \ xmin)" using xmin by simp_all ultimately have "s ((adverse 0 i j) \ (Suc xmin)) = s ((adverse z i j) \ xmin)" "s ((adverse 1 i j) \ (Suc xmin)) = s ((adverse z i j) \ xmin)" by simp_all then have "s ((adverse 0 i j) \ (Suc xmin)) = s ((adverse 1 i j) \ (Suc xmin))" by simp moreover have "(adverse 0 i j) \ (Suc xmin) \ (adverse 1 i j) \ (Suc xmin)" using a0 a1 i0 i1 by (metis append1_eq_conv list_decode_encode zero_neq_one) ultimately show "\ learn_cons \ {adverse 0 i j, adverse 1 i j} s" using same_hyp_different_init_not_cons by blast qed text \Combining the previous two lemmas shows that @{term "V\<^sub>0\<^sub>1"} cannot be learned consistently in the limit by the total strategy $S$.\ lemma V01_not_in_R_cons: "\ learn_cons \ V\<^sub>0\<^sub>1 s" proof - obtain m n where mn0: "adverse 0 m n \ V\<^sub>0\<^sub>1" and mn1: "adverse 1 m n \ V\<^sub>0\<^sub>1" using adverse_in_V01 by auto show "\ learn_cons \ V\<^sub>0\<^sub>1 s" proof (cases "\x>0. hyp_change 0 m n x") case True then have "\ learn_lim \ {adverse 0 m n} s" using always_hyp_change_no_lim by simp with mn0 show ?thesis using learn_cons_def learn_lim_closed_subseteq by auto next case False then obtain x where x: "x > 0" "\ hyp_change 0 m n x" by auto then have "\ learn_cons \ {adverse 0 m n, adverse 1 m n} s" using no_hyp_change_no_cons[OF x] by simp with mn0 mn1 show ?thesis using learn_cons_closed_subseteq by auto qed qed end subsubsection \@{term "V\<^sub>0\<^sub>1"} is in CONS\ text \At first glance, consistently learning @{term "V\<^sub>0\<^sub>1"} looks fairly easy. After all every @{term "f \ V\<^sub>0\<^sub>1"} provides a Gödel number of itself either at argument 0 or 1. A strategy only has to figure out which one is right. However, the strategy $S$ we are going to devise does not always converge to $f(0)$ or $f(1)$. Instead it uses a technique called ``amalgamation''. The amalgamation of two Gödel numbers $i$ and $j$ is a function whose value at $x$ is determined by simulating $\varphi_i(x)$ and $\varphi_j(x)$ in parallel and outputting the value of the first one to halt. If neither halts the value is undefined. There is a function $a\in\mathcal{R}^2$ such that $\varphi_{a(i,j)}$ is the amalgamation of $i$ and $j$. If @{term "f \ V\<^sub>0\<^sub>1"} then $\varphi_{a(f(0), f(1))}$ is total because by definition of @{term "V\<^sub>0\<^sub>1"} we have $\varphi_{f(0)} = f$ or $\varphi_{f(1)} = f$ and $f$ is total. Given a prefix $f^n$ of an @{term "f \ V\<^sub>0\<^sub>1"} the strategy $S$ first computes $\varphi_{a(f(0), f(1))}(x)$ for $x = 0, \ldots, n$. For the resulting prefix $\varphi^n_{a(f(0), f(1))}$ there are two cases: \begin{enumerate} \item[Case 1.] It differs from $f^n$, say at minimum index $x$. Then for either $z = 0$ or $z = 1$ we have $\varphi_{f(z)}(x) \neq f(x)$ by definition of amalgamation. This implies $\varphi_{f(z)} \neq f$, and thus $\varphi_{f(1-z)} = f$ by definition of @{term "V\<^sub>0\<^sub>1"}. We set $S(f^n) = f(1 - z)$. This hypothesis is correct and hence consistent. \item[Case 2.] It equals $f^n$. Then we set $S(f^n) = a(f(0), f(1))$. This hypothesis is consistent by definition of this case. \end{enumerate} In both cases the hypothesis is consistent. If Case~1 holds for some $n$, the same $x$ and $z$ will be found also for all larger values of $n$. Therefore $S$ converges to the correct hypothesis $f(1 - z)$. If Case~2 holds for all $n$, then $S$ always outputs the same hypothesis $a(f(0), f(1))$ and thus also converges. The above discussion tacitly assumes $n \geq 1$, such that both $f(0)$ and $f(1)$ are available to $S$. For $n = 0$ the strategy outputs an arbitrary consistent hypothesis.\ text \Amalgamation uses the concurrent simulation of functions.\ definition parallel :: "nat \ nat \ nat \ nat option" where "parallel i j x \ eval r_parallel [i, j, x]" lemma r_parallel': "eval r_parallel [i, j, x] = parallel i j x" using parallel_def by simp lemma r_parallel'': shows "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \" and "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval r_phi [i, x]))" and "eval r_phi [j, x] \ \ eval r_phi [i, x] \ \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval r_phi [j, x]))" and "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval r_phi [i, x])) \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval r_phi [j, x]))" proof - let ?f = "Cn 1 r_phi [r_const i, Id 1 0]" let ?g = "Cn 1 r_phi [r_const j, Id 1 0]" have *: "\x. eval r_phi [i, x] = eval ?f [x]" "\x. eval r_phi [j, x] = eval ?g [x]" by simp_all show "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \" and "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval r_phi [i, x]))" and "eval r_phi [j, x] \ \ eval r_phi [i, x] \ \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval r_phi [j, x]))" and "eval r_phi [i, x] \ \ eval r_phi [j, x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval r_phi [i, x])) \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval r_phi [j, x]))" using r_parallel[OF *] by simp_all qed lemma parallel: "\ i x \ \ \ j x \ \ parallel i j x \" "\ i x \ \ \ j x \ \ parallel i j x \= prod_encode (0, the (\ i x))" "\ j x \ \ \ i x \ \ parallel i j x \= prod_encode (1, the (\ j x))" "\ i x \ \ \ j x \ \ parallel i j x \= prod_encode (0, the (\ i x)) \ parallel i j x \= prod_encode (1, the (\ j x))" using phi_def r_parallel'' r_parallel parallel_def by simp_all lemma parallel_converg_pdec1_0_or_1: assumes "parallel i j x \" shows "pdec1 (the (parallel i j x)) = 0 \ pdec1 (the (parallel i j x)) = 1" using assms parallel[of i x j] parallel(3)[of j x i] by (metis fst_eqD option.sel prod_encode_inverse) lemma parallel_converg_either: "(\ i x \ \ \ j x \) = (parallel i j x \)" using parallel by (metis option.simps(3)) lemma parallel_0: assumes "parallel i j x \= prod_encode (0, v)" shows "\ i x \= v" using parallel assms by (smt option.collapse option.sel option.simps(3) prod.inject prod_encode_eq zero_neq_one) lemma parallel_1: assumes "parallel i j x \= prod_encode (1, v)" shows "\ j x \= v" using parallel assms by (smt option.collapse option.sel option.simps(3) prod.inject prod_encode_eq zero_neq_one) lemma parallel_converg_V01: assumes "f \ V\<^sub>0\<^sub>1" shows "parallel (the (f 0)) (the (f 1)) x \" proof - have "f \ \ \ (\ (the (f 0)) = f \ \ (the (f 1)) = f)" using assms V01_def by auto then have "\ (the (f 0)) \ \ \ \ (the (f 1)) \ \" by auto then have "\ (the (f 0)) x \ \ \ (the (f 1)) x \" using R1_imp_total1 by auto then show ?thesis using parallel_converg_either by simp qed text \The amalgamation of two Gödel numbers can then be described in terms of @{term "parallel"}.\ definition amalgamation :: "nat \ nat \ partial1" where "amalgamation i j x \ if parallel i j x \ then None else Some (pdec2 (the (parallel i j x)))" lemma amalgamation_diverg: "amalgamation i j x \ \ \ i x \ \ \ j x \" using amalgamation_def parallel by (metis option.simps(3)) lemma amalgamation_total: assumes "total1 (\ i) \ total1 (\ j)" shows "total1 (amalgamation i j)" using assms amalgamation_diverg[of i j] total_def by auto lemma amalgamation_V01_total: assumes "f \ V\<^sub>0\<^sub>1" shows "total1 (amalgamation (the (f 0)) (the (f 1)))" using assms V01_def amalgamation_total R1_imp_total1 total1_def by (metis (mono_tags, lifting) mem_Collect_eq) definition "r_amalgamation \ Cn 3 r_pdec2 [r_parallel]" lemma r_amalgamation_recfn: "recfn 3 r_amalgamation" unfolding r_amalgamation_def by simp lemma r_amalgamation: "eval r_amalgamation [i, j, x] = amalgamation i j x" proof (cases "parallel i j x \") case True then have "eval r_parallel [i, j, x] \" by (simp add: r_parallel') then have "eval r_amalgamation [i, j, x] \" unfolding r_amalgamation_def by simp moreover from True have "amalgamation i j x \" using amalgamation_def by simp ultimately show ?thesis by simp next case False then have "eval r_parallel [i, j, x] \" by (simp add: r_parallel') then have "eval r_amalgamation [i, j, x] = eval r_pdec2 [the (eval r_parallel [i, j, x])]" unfolding r_amalgamation_def by simp also have "... \= pdec2 (the (eval r_parallel [i, j, x]))" by simp finally show ?thesis by (simp add: False amalgamation_def r_parallel') qed text \The function @{term "amalgamate"} computes Gödel numbers of amalgamations. It corresponds to the function $a$ from the proof sketch.\ definition amalgamate :: "nat \ nat \ nat" where "amalgamate i j \ smn 1 (encode r_amalgamation) [i, j]" lemma amalgamate: "\ (amalgamate i j) = amalgamation i j" proof fix x have "\ (amalgamate i j) x = eval r_phi [amalgamate i j, x]" by (simp add: phi_def) also have "... = eval r_phi [smn 1 (encode r_amalgamation) [i, j], x]" using amalgamate_def by simp also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 (encode r_amalgamation) # map (r_constn 0) [i, j] @ map (Id 1) [0])), x]" using smn[of 1 "encode r_amalgamation" "[i, j]"] by (simp add: numeral_3_eq_3) also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_const (encode r_amalgamation) # [r_const i, r_const j, Id 1 0])), x]" (is "... = eval r_phi [encode ?f, x]") by (simp add: r_constn_def) finally have "\ (amalgamate i j) x = eval r_phi [encode (Cn 1 (r_universal 3) (r_const (encode r_amalgamation) # [r_const i, r_const j, Id 1 0])), x]" . then have "\ (amalgamate i j) x = eval (r_universal 3) [encode r_amalgamation, i, j, x]" unfolding r_phi_def using r_universal[of ?f 1] r_amalgamation_recfn by simp then show "\ (amalgamate i j) x = amalgamation i j x" using r_amalgamation by (simp add: r_amalgamation_recfn r_universal) qed lemma amalgamation_in_P1: "amalgamation i j \ \

" using amalgamate by (metis P2_proj_P1 phi_in_P2) lemma amalgamation_V01_R1: assumes "f \ V\<^sub>0\<^sub>1" shows "amalgamation (the (f 0)) (the (f 1)) \ \" using assms amalgamation_V01_total amalgamation_in_P1 by (simp add: P1_total_imp_R1) definition "r_amalgamate \ Cn 2 (r_smn 1 2) [r_dummy 1 (r_const (encode r_amalgamation)), Id 2 0, Id 2 1]" lemma r_amalgamate_recfn: "recfn 2 r_amalgamate" unfolding r_amalgamate_def by simp lemma r_amalgamate: "eval r_amalgamate [i, j] \= amalgamate i j" proof - let ?p = "encode r_amalgamation" have rs21: "eval (r_smn 1 2) [?p, i, j] \= smn 1 ?p [i, j]" using r_smn by simp moreover have "eval r_amalgamate [i, j] = eval (r_smn 1 2) [?p, i, j]" unfolding r_amalgamate_def by auto ultimately have "eval r_amalgamate [i, j] \= smn 1 ?p [i, j]" by simp then show ?thesis using amalgamate_def by simp qed text \The strategy $S$ distinguishes the two cases from the proof sketch with the help of the next function, which checks if a hypothesis $\varphi_i$ is inconsistent with a prefix $e$. If so, it returns the least $x < |e|$ witnessing the inconsistency; otherwise it returns the length $|e|$. If $\varphi_i$ diverges for some $x < |e|$, so does the function.\ definition inconsist :: partial2 where "inconsist i e \ (if \x i x \ then None else if \x i x \\ e_nth e x then Some (LEAST x. x < e_length e \ \ i x \\ e_nth e x) else Some (e_length e))" lemma inconsist_converg: assumes "inconsist i e \" shows "inconsist i e = (if \x i x \\ e_nth e x then Some (LEAST x. x < e_length e \ \ i x \\ e_nth e x) else Some (e_length e))" and "\x i x \" using inconsist_def assms by (presburger, meson) lemma inconsist_bounded: assumes "inconsist i e \" shows "the (inconsist i e) \ e_length e" proof (cases "\x i x \\ e_nth e x") case True then show ?thesis using inconsist_converg[OF assms] by (smt Least_le dual_order.strict_implies_order dual_order.strict_trans2 option.sel) next case False then show ?thesis using inconsist_converg[OF assms] by auto qed lemma inconsist_consistent: assumes "inconsist i e \" shows "inconsist i e \= e_length e \ (\x i x \= e_nth e x)" proof show "\x i x \= e_nth e x" if "inconsist i e \= e_length e" proof (cases "\x i x \\ e_nth e x") case True then show ?thesis using that inconsist_converg[OF assms] by (metis (mono_tags, lifting) not_less_Least option.inject) next case False then show ?thesis using that inconsist_converg[OF assms] by simp qed show "\x i x \= e_nth e x \ inconsist i e \= e_length e" unfolding inconsist_def using assms by auto qed lemma inconsist_converg_eq: assumes "inconsist i e \= e_length e" shows "\x i x \= e_nth e x" using assms inconsist_consistent by auto lemma inconsist_converg_less: assumes "inconsist i e \" and "the (inconsist i e) < e_length e" shows "\x i x \\ e_nth e x" and "inconsist i e \= (LEAST x. x < e_length e \ \ i x \\ e_nth e x)" proof - show "\x i x \\ e_nth e x" using assms by (metis (no_types, lifting) inconsist_converg(1) nat_neq_iff option.sel) then show "inconsist i e \= (LEAST x. x < e_length e \ \ i x \\ e_nth e x)" using assms inconsist_converg by presburger qed lemma least_bounded_Suc: assumes "\x. x < upper \ P x" shows "(LEAST x. x < upper \ P x) = (LEAST x. x < Suc upper \ P x)" proof - let ?Q = "\x. x < upper \ P x" let ?x = "Least ?Q" from assms have "?x < upper \ P ?x" using LeastI_ex[of ?Q] by simp then have 1: "?x < Suc upper \ P ?x" by simp from assms have 2: "\y P y" using Least_le[of ?Q] not_less_Least by fastforce have "(LEAST x. x < Suc upper \ P x) = ?x" proof (rule Least_equality) show "?x < Suc upper \ P ?x" using 1 2 by blast show "\y. y < Suc upper \ P y \ ?x \ y" using 1 2 leI by blast qed then show ?thesis .. qed lemma least_bounded_gr: fixes P :: "nat \ bool" and m :: nat assumes "\x. x < upper \ P x" shows "(LEAST x. x < upper \ P x) = (LEAST x. x < upper + m \ P x)" proof (induction m) case 0 then show ?case by simp next case (Suc m) moreover have "\x. x < upper + m \ P x" using assms trans_less_add1 by blast ultimately show ?case using least_bounded_Suc by simp qed lemma inconsist_init_converg_less: assumes "f \ \" and "\ i \ \" and "inconsist i (f \ n) \" and "the (inconsist i (f \ n)) < Suc n" shows "inconsist i (f \ (n + m)) = inconsist i (f \ n)" proof - have phi_i_total: "\ i x \" for x using assms by simp moreover have f_nth: "f x \= e_nth (f \ n) x" if "x < Suc n" for x n using that assms(1) by simp ultimately have "(\ i x \ f x) = (\ i x \\ e_nth (f \ n) x)" if "x < Suc n" for x n using that by simp then have cond: "(x < Suc n \ \ i x \ f x) = (x < e_length (f \ n) \ \ i x \\ e_nth (f \ n) x)" for x n using length_init by metis then have 1: "\x i x \ f x" and 2: "inconsist i (f \ n) \= (LEAST x. x < Suc n \ \ i x \ f x)" using assms(3,4) inconsist_converg_less[of i "f \ n"] by simp_all then have 3: "\x i x \ f x" using not_add_less1 by fastforce then have "\x i x \\ e_nth (f \ (n + m)) x" using cond by blast then have "\x (n + m)). \ i x \\ e_nth (f \ (n + m)) x" by simp moreover have 4: "inconsist i (f \ (n + m)) \" using assms(2) R1_imp_total1 inconsist_def by simp ultimately have "inconsist i (f \ (n + m)) \= (LEAST x. x < e_length (f \ (n + m)) \ \ i x \\ e_nth (f \ (n + m)) x)" using inconsist_converg[OF 4] by simp then have 5: "inconsist i (f \ (n + m)) \= (LEAST x. x < Suc (n + m) \ \ i x \ f x)" using cond[of _ "n + m"] by simp then have "(LEAST x. x < Suc n \ \ i x \ f x) = (LEAST x. x < Suc n + m \ \ i x \ f x)" using least_bounded_gr[where ?upper="Suc n"] 1 3 by simp then show ?thesis using 2 5 by simp qed definition "r_inconsist \ let f = Cn 2 r_length [Id 2 1]; g = Cn 4 r_ifless [Id 4 1, Cn 4 r_length [Id 4 3], Id 4 1, Cn 4 r_ifeq [Cn 4 r_phi [Id 4 2, Id 4 0], Cn 4 r_nth [Id 4 3, Id 4 0], Id 4 1, Id 4 0]] in Cn 2 (Pr 2 f g) [Cn 2 r_length [Id 2 1], Id 2 0, Id 2 1]" lemma r_inconsist_recfn: "recfn 2 r_inconsist" unfolding r_inconsist_def by simp lemma r_inconsist: "eval r_inconsist [i, e] = inconsist i e" proof - define f where "f = Cn 2 r_length [Id 2 1]" define len where "len = Cn 4 r_length [Id 4 3]" define nth where "nth = Cn 4 r_nth [Id 4 3, Id 4 0]" define ph where "ph = Cn 4 r_phi [Id 4 2, Id 4 0]" define g where "g = Cn 4 r_ifless [Id 4 1, len, Id 4 1, Cn 4 r_ifeq [ph, nth, Id 4 1, Id 4 0]]" have "recfn 2 f" unfolding f_def by simp have f: "eval f [i, e] \= e_length e" unfolding f_def by simp have "recfn 4 len" unfolding len_def by simp have len: "eval len [j, v, i, e] \= e_length e" for j v unfolding len_def by simp have "recfn 4 nth" unfolding nth_def by simp have nth: "eval nth [j, v, i, e] \= e_nth e j" for j v unfolding nth_def by simp have "recfn 4 ph" unfolding ph_def by simp have ph: "eval ph [j, v, i, e] = \ i j" for j v unfolding ph_def using phi_def by simp have "recfn 4 g" unfolding g_def using `recfn 4 nth` `recfn 4 ph` `recfn 4 len` by simp have g_diverg: "eval g [j, v, i, e] \" if "eval ph [j, v, i, e] \" for j v unfolding g_def using that `recfn 4 nth` `recfn 4 ph` `recfn 4 len` by simp have g_converg: "eval g [j, v, i, e] \= (if v < e_length e then v else if \ i j \= e_nth e j then v else j)" if "eval ph [j, v, i, e] \" for j v unfolding g_def using that `recfn 4 nth` `recfn 4 ph` `recfn 4 len` len nth ph by auto define h where "h \ Pr 2 f g" then have "recfn 3 h" by (simp add: \recfn 2 f\ \recfn 4 g\) let ?invariant = "\j i e. (if \x i x \ then None else if \x i x \\ e_nth e x then Some (LEAST x. x < j \ \ i x \\ e_nth e x) else Some (e_length e))" have "eval h [j, i, e] = ?invariant j i e" if "j \ e_length e" for j using that proof (induction j) case 0 then show ?case unfolding h_def using `recfn 2 f` f `recfn 4 g` by simp next case (Suc j) then have j_less: "j < e_length e" by simp then have j_le: "j \ e_length e" by simp show ?case proof (cases "eval h [j, i, e] \") case True then have "\x i x \" using j_le Suc.IH by (metis option.simps(3)) then have "\x i x \" using less_SucI by blast moreover have h: "eval h [Suc j, i, e] \" using True h_def `recfn 3 h` by simp ultimately show ?thesis by simp next case False with Suc.IH j_le have h_j: "eval h [j, i, e] = (if \x i x \\ e_nth e x then Some (LEAST x. x < j \ \ i x \\ e_nth e x) else Some (e_length e))" by presburger then have the_h_j: "the (eval h [j, i, e]) = (if \x i x \\ e_nth e x then LEAST x. x < j \ \ i x \\ e_nth e x else e_length e)" (is "_ = ?v") by auto have h_Suc: "eval h [Suc j, i, e] = eval g [j, the (eval h [j, i, e]), i, e]" using False h_def `recfn 4 g` `recfn 2 f` by auto show ?thesis proof (cases "\ i j \") case True with ph g_diverg h_Suc show ?thesis by auto next case False with h_Suc have "eval h [Suc j, i, e] \= (if ?v < e_length e then ?v else if \ i j \= e_nth e j then ?v else j)" (is "_ \= ?lhs") using g_converg ph the_h_j by simp moreover have "?invariant (Suc j) i e \= (if \x i x \\ e_nth e x then LEAST x. x < Suc j \ \ i x \\ e_nth e x else e_length e)" (is "_ \= ?rhs") proof - from False have "\ i j \" by simp moreover have "\ (\x i x \)" by (metis (no_types, lifting) Suc.IH h_j j_le option.simps(3)) ultimately have "\ (\x i x \)" using less_Suc_eq by auto then show ?thesis by auto qed moreover have "?lhs = ?rhs" proof (cases "?v < e_length e") case True then have ex_j: "\x i x \\ e_nth e x" and v_eq: "?v = (LEAST x. x < j \ \ i x \\ e_nth e x)" by presburger+ with True have "?lhs = ?v" by simp from ex_j have "\x i x \\ e_nth e x" using less_SucI by blast then have "?rhs = (LEAST x. x < Suc j \ \ i x \\ e_nth e x)" by simp with True v_eq ex_j show ?thesis using least_bounded_Suc[of j "\x. \ i x \\ e_nth e x"] by simp next case False then have not_ex: "\ (\x i x \\ e_nth e x)" using Least_le[of "\x. x < j \ \ i x \\ e_nth e x"] j_le by (smt leD le_less_linear le_trans) then have "?v = e_length e" by argo with False have lhs: "?lhs = (if \ i j \= e_nth e j then e_length e else j)" by simp show ?thesis proof (cases "\ i j \= e_nth e j") case True then have "\ (\x i x \\ e_nth e x)" using less_SucE not_ex by blast then have "?rhs = e_length e" by argo moreover from True have "?lhs = e_length e" using lhs by simp ultimately show ?thesis by simp next case False then have "\ i j \\ e_nth e j" using `\ i j \` by simp with not_ex have "(LEAST x. x \ i x \\ e_nth e x) = j" using LeastI[of "\x. x \ i x \\ e_nth e x" j] less_Suc_eq by blast then have "?rhs = j" using \\ i j \\ e_nth e j\ by (meson lessI) moreover from False lhs have "?lhs = j" by simp ultimately show ?thesis by simp qed qed ultimately show ?thesis by simp qed qed qed then have "eval h [e_length e, i, e] = ?invariant (e_length e) i e" by auto then have "eval h [e_length e, i, e] = inconsist i e" using inconsist_def by simp moreover have "eval (Cn 2 (Pr 2 f g) [Cn 2 r_length [Id 2 1], Id 2 0, Id 2 1]) [i, e] = eval h [e_length e, i, e]" using `recfn 4 g` `recfn 2 f` h_def by auto ultimately show ?thesis unfolding r_inconsist_def by (simp add: f_def g_def len_def nth_def ph_def) qed lemma inconsist_for_total: assumes "total1 (\ i)" shows "inconsist i e \= (if \x i x \\ e_nth e x then LEAST x. x < e_length e \ \ i x \\ e_nth e x else e_length e)" unfolding inconsist_def using assms total1_def by (auto; blast) lemma inconsist_for_V01: assumes "f \ V\<^sub>0\<^sub>1" and "k = amalgamate (the (f 0)) (the (f 1))" shows "inconsist k e \= (if \x k x \\ e_nth e x then LEAST x. x < e_length e \ \ k x \\ e_nth e x else e_length e)" proof - have "\ k \ \" using amalgamation_V01_R1[OF assms(1)] assms(2) amalgamate by simp then have "total1 (\ k)" by simp with inconsist_for_total[of k] show ?thesis by simp qed text \The next function computes Gödel numbers of functions consistent with a given prefix. The strategy will use these as consistent auxiliary hypotheses when receiving a prefix of length one.\ definition "r_auxhyp \ Cn 1 (r_smn 1 1) [r_const (encode r_prenum), Id 1 0]" lemma r_auxhyp_prim: "prim_recfn 1 r_auxhyp" unfolding r_auxhyp_def by simp lemma r_auxhyp: "\ (the (eval r_auxhyp [e])) = prenum e" proof fix x let ?p = "encode r_prenum" let ?p = "encode r_prenum" have "eval r_auxhyp [e] = eval (r_smn 1 1) [?p, e]" unfolding r_auxhyp_def by simp then have "eval r_auxhyp [e] \= smn 1 ?p [e]" by (simp add: r_smn) also have "... \= encode (Cn 1 (r_universal (1 + length [e])) (r_constn (1 - 1) ?p # map (r_constn (1 - 1)) [e] @ map (recf.Id 1) [0..<1]))" using smn[of 1 ?p "[e]"] by simp also have "... \= encode (Cn 1 (r_universal (1 + 1)) (r_constn 0 ?p # map (r_constn 0) [e] @ [Id 1 0]))" by simp also have "... \= encode (Cn 1 (r_universal 2) (r_constn 0 ?p # map (r_constn 0) [e] @ [Id 1 0]))" by (metis one_add_one) also have "... \= encode (Cn 1 (r_universal 2) [r_constn 0 ?p, r_constn 0 e, Id 1 0])" by simp also have "... \= encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0])" using r_constn_def by simp finally have "eval r_auxhyp [e] \= encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0])" . moreover have "\ (the (eval r_auxhyp [e])) x = eval r_phi [the (eval r_auxhyp [e]), x]" by (simp add: phi_def) ultimately have "\ (the (eval r_auxhyp [e])) x = eval r_phi [encode (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0]), x]" (is "_ = eval r_phi [encode ?f, x]") by simp then have "\ (the (eval r_auxhyp [e])) x = eval (Cn 1 (r_universal 2) [r_const ?p, r_const e, Id 1 0]) [x]" using r_phi_def r_universal[of ?f 1 "[x]"] by simp then have "\ (the (eval r_auxhyp [e])) x = eval (r_universal 2) [?p, e, x]" by simp then have "\ (the (eval r_auxhyp [e])) x = eval r_prenum [e, x]" using r_universal by simp then show "\ (the (eval r_auxhyp [e])) x = prenum e x" by simp qed definition auxhyp :: partial1 where "auxhyp e \ eval r_auxhyp [e]" lemma auxhyp_prenum: "\ (the (auxhyp e)) = prenum e" using auxhyp_def r_auxhyp by metis lemma auxhyp_in_R1: "auxhyp \ \" using auxhyp_def Mn_free_imp_total R1I r_auxhyp_prim by metis text \Now we can define our consistent learning strategy for @{term "V\<^sub>0\<^sub>1"}.\ definition "r_sv01 \ let at0 = Cn 1 r_nth [Id 1 0, Z]; at1 = Cn 1 r_nth [Id 1 0, r_const 1]; m = Cn 1 r_amalgamate [at0, at1]; c = Cn 1 r_inconsist [m, Id 1 0]; p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]; g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]] in Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], Id 1 0]" lemma r_sv01_recfn: "recfn 1 r_sv01" unfolding r_sv01_def using r_auxhyp_prim r_inconsist_recfn r_amalgamate_recfn by (simp add: Let_def) definition sv01 :: partial1 ("s\<^bsub>01\<^esub>")where "sv01 e \ eval r_sv01 [e]" lemma sv01_in_P1: "s\<^bsub>01\<^esub> \ \

" using sv01_def r_sv01_recfn P1I by presburger text \We are interested in the behavior of @{term "s\<^bsub>01\<^esub>"} only on prefixes of functions in @{term "V\<^sub>0\<^sub>1"}. This behavior is linked to the amalgamation of $f(0)$ and $f(1)$, where $f$ is the function to be learned.\ abbreviation amalg01 :: "partial1 \ nat" where "amalg01 f \ amalgamate (the (f 0)) (the (f 1))" lemma sv01: assumes "f \ V\<^sub>0\<^sub>1" shows "s\<^bsub>01\<^esub> (f \ 0) = auxhyp (f \ 0)" and "n \ 0 \ inconsist (amalg01 f) (f \ n) \= Suc n \ s\<^bsub>01\<^esub> (f \ n) \= amalg01 f" and "n \ 0 \ the (inconsist (amalg01 f) (f \ n)) < Suc n \ pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \ n))))) = 0 \ s\<^bsub>01\<^esub> (f \ n) = f 1" and "n \ 0 \ the (inconsist (amalg01 f) (f \ n)) < Suc n \ pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist (amalg01 f) (f \ n))))) \ 0 \ s\<^bsub>01\<^esub> (f \ n) = f 0" proof - have f_total: "\x. f x \" using assms V01_def R1_imp_total1 by blast define at0 where "at0 = Cn 1 r_nth [Id 1 0, Z]" define at1 where "at1 = Cn 1 r_nth [Id 1 0, r_const 1]" define m where "m = Cn 1 r_amalgamate [at0, at1]" define c where "c = Cn 1 r_inconsist [m, Id 1 0]" define p where "p = Cn 1 r_pdec1 [Cn 1 r_parallel [at0, at1, c]]" define g where "g = Cn 1 r_ifeq [c, r_length, m, Cn 1 r_ifz [p, at1, at0]]" have "recfn 1 g" unfolding g_def p_def c_def m_def at1_def at0_def using r_auxhyp_prim r_inconsist_recfn r_amalgamate_recfn by simp have "eval (Cn 1 r_eq [r_length, r_const 1]) [f \ 0] \= 0" by simp then have "eval r_sv01 [f \ 0] = eval r_auxhyp [f \ 0]" unfolding r_sv01_def using `recfn 1 g` c_def g_def m_def p_def r_auxhyp_prim by (auto simp add: Let_def) then show "s\<^bsub>01\<^esub> (f \ 0) = auxhyp (f \ 0)" by (simp add: auxhyp_def sv01_def) have sv01: "s\<^bsub>01\<^esub> (f \ n) = eval g [f \ n]" if "n \ 0" proof - have *: "eval (Cn 1 r_eq [r_length, r_const 1]) [f \ n] \\ 0" (is "?r_eq \\ 0") using that by simp moreover have "recfn 2 (r_lifz r_auxhyp g)" using `recfn 1 g` r_auxhyp_prim by simp moreover have "eval r_sv01 [f \ n] = eval (Cn 1 (r_lifz r_auxhyp g) [Cn 1 r_eq [r_length, r_const 1], Id 1 0]) [f \ n]" using r_sv01_def by (metis at0_def at1_def c_def g_def m_def p_def) ultimately have "eval r_sv01 [f \ n] = eval (r_lifz r_auxhyp g) [the ?r_eq, f \ n]" by simp then have "eval r_sv01 [f \ n] = eval g [f \ n]" using "*" \recfn 1 g\ r_auxhyp_prim by auto then show ?thesis by (simp add: sv01_def that) qed have "recfn 1 at0" unfolding at0_def by simp have at0: "eval at0 [f \ n] \= the (f 0)" unfolding at0_def by simp have "recfn 1 at1" unfolding at1_def by simp have at1: "n \ 0 \ eval at1 [f \ n] \= the (f 1)" unfolding at1_def by simp have "recfn 1 m" unfolding m_def at0_def at1_def using r_amalgamate_recfn by simp have m: "n \ 0 \ eval m [f \ n] \= amalg01 f" (is "_ \ _ \= ?m") unfolding m_def at0_def at1_def using at0 at1 amalgamate r_amalgamate r_amalgamate_recfn by simp then have c: "n \ 0 \ eval c [f \ n] = inconsist (amalg01 f) (f \ n)" (is "_ \ _ = ?c") unfolding c_def using r_inconsist_recfn `recfn 1 m` r_inconsist by auto then have c_converg: "n \ 0 \ eval c [f \ n] \" using inconsist_for_V01[OF assms] by simp have "recfn 1 c" unfolding c_def using `recfn 1 m` r_inconsist_recfn by simp have par: "n \ 0 \ eval (Cn 1 r_parallel [at0, at1, c]) [f \ n] = parallel (the (f 0)) (the (f 1)) (the ?c)" (is "_ \ _ = ?par") using at0 at1 c c_converg m r_parallel' `recfn 1 at0` `recfn 1 at1` `recfn 1 c` by simp with parallel_converg_V01[OF assms] have par_converg: "n \ 0 \ eval (Cn 1 r_parallel [at0, at1, c]) [f \ n] \" by simp then have p_converg: "n \ 0 \ eval p [f \ n] \" unfolding p_def using at0 at1 c_converg `recfn 1 at0` `recfn 1 at1` `recfn 1 c` by simp have p: "n \ 0 \ eval p [f \ n] \= pdec1 (the ?par)" unfolding p_def using at0 at1 c_converg `recfn 1 at0` `recfn 1 at1` `recfn 1 c` par par_converg by simp have "recfn 1 p" unfolding p_def using `recfn 1 at0` `recfn 1 at1` `recfn 1 m` `recfn 1 c` by simp let ?r = "Cn 1 r_ifz [p, at1, at0]" have r: "n \ 0 \ eval ?r [f \ n] = (if pdec1 (the ?par) = 0 then f 1 else f 0)" using at0 at1 c_converg `recfn 1 at0` `recfn 1 at1` `recfn 1 c` `recfn 1 m` `recfn 1 p` p f_total by fastforce have g: "n \ 0 \ eval g [f \ n] \= (if the ?c = e_length (f \ n) then ?m else the (eval (Cn 1 r_ifz [p, at1, at0]) [f \ n]))" unfolding g_def using `recfn 1 p` `recfn 1 at0` `recfn 1 at1` `recfn 1 c` `recfn 1 m` p_converg at1 at0 c c_converg m by simp { assume "n \ 0" and "?c \= Suc n" moreover have "e_length (f \ n) = Suc n" by simp ultimately have "eval g [f \ n] \= ?m" using g by simp then show "s\<^bsub>01\<^esub> (f \ n) \= amalg01 f" using sv01[OF `n \ 0`] by simp next assume "n \ 0" and "the ?c < Suc n" and "pdec1 (the ?par) = 0" with g r f_total have "eval g [f \ n] = f 1" by simp then show "s\<^bsub>01\<^esub> (f \ n) = f 1" using sv01[OF `n \ 0`] by simp next assume "n \ 0" and "the ?c < Suc n" and "pdec1 (the ?par) \ 0" with g r f_total have "eval g [f \ n] = f 0" by simp then show "s\<^bsub>01\<^esub> (f \ n) = f 0" using sv01[OF `n \ 0`] by simp } qed text \Part of the correctness of @{term sv01} is convergence on prefixes of functions in @{term "V\<^sub>0\<^sub>1"}.\ lemma sv01_converg_V01: assumes "f \ V\<^sub>0\<^sub>1" shows "s\<^bsub>01\<^esub> (f \ n) \" proof (cases "n = 0") case True then show ?thesis using assms sv01 R1_imp_total1 auxhyp_in_R1 by simp next case n_gr_0: False show ?thesis proof (cases "inconsist (amalg01 f) (f \ n) \= Suc n") case True then show ?thesis using n_gr_0 assms sv01 by simp next case False then have "the (inconsist (amalg01 f) (f \ n)) < Suc n" using assms inconsist_bounded inconsist_for_V01 length_init by (metis (no_types, lifting) le_neq_implies_less option.collapse option.simps(3)) then show ?thesis using n_gr_0 assms sv01 R1_imp_total1 total1E V01_def by (metis (no_types, lifting) mem_Collect_eq) qed qed text \Another part of the correctness of @{term sv01} is its hypotheses being consistent on prefixes of functions in @{term "V\<^sub>0\<^sub>1"}.\ lemma sv01_consistent_V01: assumes "f \ V\<^sub>0\<^sub>1" shows "\x\n. \ (the (s\<^bsub>01\<^esub> (f \ n))) x = f x" proof (cases "n = 0") case True then have "s\<^bsub>01\<^esub> (f \ n) = auxhyp (f \ n)" using sv01[OF assms] by simp then have "\ (the (s\<^bsub>01\<^esub> (f \ n))) = prenum (f \ n)" using auxhyp_prenum by simp then show ?thesis using R1_imp_total1 total1E assms by (simp add: V01_def) next case n_gr_0: False let ?m = "amalg01 f" let ?e = "f \ n" let ?c = "the (inconsist ?m ?e)" have c: "inconsist ?m ?e \" using assms inconsist_for_V01 by blast show ?thesis proof (cases "inconsist ?m ?e \= Suc n") case True then show ?thesis using assms n_gr_0 sv01 R1_imp_total1 total1E V01_def is_init_of_def inconsist_consistent not_initial_imp_not_eq length_init inconsist_converg_eq by (metis (no_types, lifting) le_imp_less_Suc mem_Collect_eq option.sel) next case False then have less: "the (inconsist ?m ?e) < Suc n" using c assms inconsist_bounded inconsist_for_V01 length_init by (metis le_neq_implies_less option.collapse) then have "the (inconsist ?m ?e) < e_length ?e" by auto then have "\x ?m x \\ e_nth ?e x" "inconsist ?m ?e \= (LEAST x. x < e_length ?e \ \ ?m x \\ e_nth ?e x)" (is "_ \= Least ?P") using inconsist_converg_less[OF c] by simp_all then have "?P ?c" and "\x. x < ?c \ \ ?P x" using LeastI_ex[of ?P] not_less_Least[of _ ?P] by (auto simp del: e_nth) then have "\ ?m ?c \ f ?c" by auto then have "amalgamation (the (f 0)) (the (f 1)) ?c \ f ?c" using amalgamate by simp then have *: "Some (pdec2 (the (parallel (the (f 0)) (the (f 1)) ?c))) \ f ?c" using amalgamation_def by (metis assms parallel_converg_V01) let ?p = "parallel (the (f 0)) (the (f 1)) ?c" show ?thesis proof (cases "pdec1 (the ?p) = 0") case True then have "\ (the (f 0)) ?c \= pdec2 (the ?p)" using assms parallel_0 parallel_converg_V01 by (metis option.collapse prod.collapse prod_decode_inverse) then have "\ (the (f 0)) ?c \ f ?c" using * by simp then have "\ (the (f 0)) \ f" by auto then have "\ (the (f 1)) = f" using assms V01_def by auto moreover have "s\<^bsub>01\<^esub> (f \ n) = f 1" using True less n_gr_0 sv01 assms by simp ultimately show ?thesis by simp next case False then have "pdec1 (the ?p) = 1" by (meson assms parallel_converg_V01 parallel_converg_pdec1_0_or_1) then have "\ (the (f 1)) ?c \= pdec2 (the ?p)" using assms parallel_1 parallel_converg_V01 by (metis option.collapse prod.collapse prod_decode_inverse) then have "\ (the (f 1)) ?c \ f ?c" using * by simp then have "\ (the (f 1)) \ f" by auto then have "\ (the (f 0)) = f" using assms V01_def by auto moreover from False less n_gr_0 sv01 assms have "s\<^bsub>01\<^esub> (f \ n) = f 0" by simp ultimately show ?thesis by simp qed qed qed text \The final part of the correctness is @{term "sv01"} converging for all functions in @{term "V\<^sub>0\<^sub>1"}.\ lemma sv01_limit_V01: assumes "f \ V\<^sub>0\<^sub>1" shows "\i. \\<^sup>\n. s\<^bsub>01\<^esub> (f \ n) \= i" proof (cases "\n>0. s\<^bsub>01\<^esub> (f \ n) \= amalgamate (the (f 0)) (the (f 1))") case True then show ?thesis by (meson less_le_trans zero_less_one) next case False then obtain n\<^sub>0 where n0: "n\<^sub>0 \ 0" "s\<^bsub>01\<^esub> (f \ n\<^sub>0) \\ amalg01 f" using \f \ V\<^sub>0\<^sub>1\ sv01_converg_V01 by blast then have *: "the (inconsist (amalg01 f) (f \ n\<^sub>0)) < Suc n\<^sub>0" (is "the (inconsist ?m (f \ n\<^sub>0)) < Suc n\<^sub>0") using assms `n\<^sub>0 \ 0` sv01(2) inconsist_bounded inconsist_for_V01 length_init by (metis (no_types, lifting) le_neq_implies_less option.collapse option.simps(3)) moreover have "f \ \" using assms V01_def by auto moreover have "\ ?m \ \" using amalgamate amalgamation_V01_R1 assms by auto moreover have "inconsist ?m (f \ n\<^sub>0) \" using inconsist_for_V01 assms by blast ultimately have **: "inconsist ?m (f \ (n\<^sub>0 + m)) = inconsist ?m (f \ n\<^sub>0)" for m using inconsist_init_converg_less[of f ?m] by simp then have "the (inconsist ?m (f \ (n\<^sub>0 + m))) < Suc n\<^sub>0 + m" for m using * by auto moreover have "pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist ?m (f \ (n\<^sub>0 + m)))))) = pdec1 (the (parallel (the (f 0)) (the (f 1)) (the (inconsist ?m (f \ n\<^sub>0)))))" for m using ** by auto moreover have "n\<^sub>0 + m \ 0" for m using `n\<^sub>0 \ 0` by simp ultimately have "s\<^bsub>01\<^esub> (f \ (n\<^sub>0 + m)) = s\<^bsub>01\<^esub> (f \ n\<^sub>0)" for m using assms sv01 * \n\<^sub>0 \ 0\ by (metis add_Suc) moreover define i where "i = s\<^bsub>01\<^esub> (f \ n\<^sub>0)" ultimately have "\n\n\<^sub>0. s\<^bsub>01\<^esub> (f \ n) = i" using nat_le_iff_add by auto then have "\n\n\<^sub>0. s\<^bsub>01\<^esub> (f \ n) \= the i" using n0(2) by simp then show ?thesis by auto qed lemma V01_learn_cons: "learn_cons \ V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>" proof (rule learn_consI2) show "environment \ V\<^sub>0\<^sub>1 s\<^bsub>01\<^esub>" by (simp add: Collect_mono V01_def phi_in_P2 sv01_in_P1 sv01_converg_V01) show "\f n. f \ V\<^sub>0\<^sub>1 \ \k\n. \ (the (s\<^bsub>01\<^esub> (f \ n))) k = f k" using sv01_consistent_V01 . show "\i n\<^sub>0. \n\n\<^sub>0. s\<^bsub>01\<^esub> (f \ n) \= i" if "f \ V\<^sub>0\<^sub>1" for f using sv01_limit_V01 that by simp qed corollary V01_in_CONS: "V\<^sub>0\<^sub>1 \ CONS" using V01_learn_cons CONS_def by auto text \Now we can show the main result of this section, namely that there is a consistently learnable class that cannot be learned consistently by a total strategy. In other words, there is no Lemma~R for CONS.\ lemma no_lemma_R_for_CONS: "\U. U \ CONS \ (\ (\s. s \ \ \ learn_cons \ U s))" using V01_in_CONS V01_not_in_R_cons by auto end \ No newline at end of file diff --git a/thys/Inductive_Inference/Standard_Results.thy b/thys/Inductive_Inference/Standard_Results.thy --- a/thys/Inductive_Inference/Standard_Results.thy +++ b/thys/Inductive_Inference/Standard_Results.thy @@ -1,1594 +1,1595 @@ theory Standard_Results imports Universal begin section \Kleene normal form and the number of $\mu$-operations\ text \Kleene's original normal form theorem~\cite{Kleene43} states that every partial recursive $f$ can be expressed as $f(x) = u(\mu y[t(i, x, y) = 0]$ for some $i$, where $u$ and $t$ are specially crafted primitive recursive functions tied to Kleene's definition of partial recursive functions. Rogers~\cite[p.~29f.]{Rogers87} relaxes the theorem by allowing $u$ and $t$ to be any primitive recursive functions of arity one and three, respectively. Both versions require a separate $t$-predicate for every arity. We will show a unified version for all arities by treating $x$ as an encoded list of arguments. Our universal function @{thm[display,names_short] "r_univ_def"} can represent all partial recursive functions (see theorem @{thm[source] r_univ}). Moreover @{term "r_result"}, @{term "r_dec"}, and @{term "r_not"} are primitive recursive. As such @{term r_univ} could almost serve as the right-hand side $u(\mu y[t(i, x, y) = 0]$. Its only flaw is that the outer function, the composition of @{term r_dec} and @{term r_result}, is ternary rather than unary.\ lemma r_univ_almost_kleene_nf: "r_univ \ (let u = Cn 3 r_dec [r_result]; t = Cn 3 r_not [r_result] in Cn 2 u [Mn 2 t, Id 2 0, Id 2 1])" unfolding r_univ_def by (rule exteqI) simp_all text \We can remedy the wrong arity with some encoding and projecting.\ definition r_nf_t :: recf where "r_nf_t \ Cn 3 r_and [Cn 3 r_eq [Cn 3 r_pdec2 [Id 3 0], Cn 3 r_prod_encode [Id 3 1, Id 3 2]], Cn 3 r_not [Cn 3 r_result [Cn 3 r_pdec1 [Id 3 0], Cn 3 r_pdec12 [Id 3 0], Cn 3 r_pdec22 [Id 3 0]]]]" lemma r_nf_t_prim: "prim_recfn 3 r_nf_t" unfolding r_nf_t_def by simp definition r_nf_u :: recf where "r_nf_u \ Cn 1 r_dec [Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]]" lemma r_nf_u_prim: "prim_recfn 1 r_nf_u" unfolding r_nf_u_def by simp lemma r_nf_t_0: assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] \\ 0" and "pdec2 y = prod_encode (i, x)" shows "eval r_nf_t [y, i, x] \= 0" unfolding r_nf_t_def using assms by auto lemma r_nf_t_1: assumes "eval r_result [pdec1 y, pdec12 y, pdec22 y] \= 0 \ pdec2 y \ prod_encode (i, x)" shows "eval r_nf_t [y, i, x] \= 1" unfolding r_nf_t_def using assms r_result_total by auto text \The next function is just as universal as @{term r_univ}, but satisfies the conditions of the Kleene normal form theorem because the outer funtion @{term r_nf_u} is unary.\ definition "r_normal_form \ Cn 2 r_nf_u [Mn 2 r_nf_t]" lemma r_normal_form_recfn: "recfn 2 r_normal_form" unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp lemma r_univ_exteq_r_normal_form: "r_univ \ r_normal_form" proof (rule exteqI) show arity: "arity r_univ = arity r_normal_form" using r_normal_form_recfn by simp show "eval r_univ xs = eval r_normal_form xs" if "length xs = arity r_univ" for xs proof - have "length xs = 2" using that by simp then obtain i x where ix: "[i, x] = xs" - by (metis length_0_conv length_Suc_conv numeral_2_eq_2) + by (smt Suc_length_conv length_0_conv numeral_2_eq_2) have "eval r_univ [i, x] = eval r_normal_form [i, x]" proof (cases "\t. eval r_result [t, i, x] \= 0") case True then have "eval r_univ [i, x] \" unfolding r_univ_def by simp moreover have "eval r_normal_form [i, x] \" proof - have "eval r_nf_t [y, i, x] \= 1" for y using True r_nf_t_1[of y i x] by fastforce then show ?thesis unfolding r_normal_form_def using r_nf_u_prim r_nf_t_prim by simp qed ultimately show ?thesis by simp next case False then have "\t. eval r_result [t, i, x] \\ 0" by (simp add: r_result_total) then obtain t where "eval r_result [t, i, x] \\ 0" by auto then have "eval r_nf_t [triple_encode t i x, i, x] \= 0" using r_nf_t_0 by simp then obtain y where y: "eval (Mn 2 r_nf_t) [i, x] \= y" using r_nf_t_prim Mn_free_imp_total by fastforce then have "eval r_nf_t [y, i, x] \= 0" using r_nf_t_prim Mn_free_imp_total eval_Mn_convergE(2)[of 2 r_nf_t "[i, x]" y] by simp then have r_result: "eval r_result [pdec1 y, pdec12 y, pdec22 y] \\ 0" and pdec2: "pdec2 y = prod_encode (i, x)" using r_nf_t_0[of y i x] r_nf_t_1[of y i x] r_result_total by auto then have "eval r_result [pdec1 y, i, x] \\ 0" by simp then obtain v where v: "eval r_univ [pdec12 y, pdec22 y] \= v" "eval r_result [pdec1 y, pdec12 y, pdec22 y] \= Suc v" using r_result r_result_bivalent'[of "pdec12 y" "pdec22 y" _ "pdec1 y"] r_result_diverg'[of "pdec12 y" "pdec22 y" "pdec1 y"] by auto have "eval r_normal_form [i, x] = eval r_nf_u [y]" unfolding r_normal_form_def using y r_nf_t_prim r_nf_u_prim by simp also have "... = eval r_dec [the (eval (Cn 1 r_result [r_pdec1, r_pdec12, r_pdec22]) [y])]" unfolding r_nf_u_def using r_result by simp also have "... = eval r_dec [Suc v]" using v by simp also have "... \= v" by simp finally have "eval r_normal_form [i, x] \= v" . moreover have "eval r_univ [i, x] \= v" using v(1) pdec2 by simp ultimately show ?thesis by simp qed with ix show ?thesis by simp qed qed theorem normal_form: assumes "recfn n f" obtains i where "\x. e_length x = n \ eval r_normal_form [i, x] = eval f (list_decode x)" proof - have "eval r_normal_form [encode f, x] = eval f (list_decode x)" if "e_length x = n" for x using r_univ_exteq_r_normal_form assms that exteq_def r_univ' by auto then show ?thesis using that by auto qed text \As a consequence of the normal form theorem every partial recursive function can be represented with exactly one application of the $\mu$-operator.\ fun count_Mn :: "recf \ nat" where "count_Mn Z = 0" | "count_Mn S = 0" | "count_Mn (Id m n) = 0" | "count_Mn (Cn n f gs) = count_Mn f + sum_list (map count_Mn gs)" | "count_Mn (Pr n f g) = count_Mn f + count_Mn g" | "count_Mn (Mn n f) = Suc (count_Mn f)" lemma count_Mn_zero_iff_prim: "count_Mn f = 0 \ Mn_free f" by (induction f) auto text \The normal form has only one $\mu$-recursion.\ lemma count_Mn_normal_form: "count_Mn r_normal_form = 1" unfolding r_normal_form_def r_nf_u_def r_nf_t_def using count_Mn_zero_iff_prim by simp lemma one_Mn_suffices: assumes "recfn n f" shows "\g. count_Mn g = 1 \ g \ f" proof - have "n > 0" using assms wellf_arity_nonzero by auto obtain i where i: "\x. e_length x = n \ eval r_normal_form [i, x] = eval f (list_decode x)" using normal_form[OF assms(1)] by auto define g where "g \ Cn n r_normal_form [r_constn (n - 1) i, r_list_encode (n - 1)]" then have "recfn n g" using r_normal_form_recfn `n > 0` by simp then have "g \ f" using g_def r_list_encode i assms by (intro exteqI) simp_all moreover have "count_Mn g = 1" unfolding g_def using count_Mn_normal_form count_Mn_zero_iff_prim by simp ultimately show ?thesis by auto qed text \The previous lemma could have been obtained without @{term "r_normal_form"} directly from @{term "r_univ"}.\ section \The $s$-$m$-$n$ theorem\ text \For all $m, n > 0$ there is an $(m + 1)$-ary primitive recursive function $s^m_n$ with \[ \varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n) \] for all $p, c_1, \ldots, c_m, x_1, \ldots, x_n$. Here, $\varphi^{(n)}$ is a function universal for $n$-ary partial recursive functions, which we will represent by @{term "r_universal n"}\ text \The $s^m_n$ functions compute codes of functions. We start simple: computing codes of the unary constant functions.\ fun code_const1 :: "nat \ nat" where "code_const1 0 = 0" | "code_const1 (Suc c) = quad_encode 3 1 1 (singleton_encode (code_const1 c))" lemma code_const1: "code_const1 c = encode (r_const c)" by (induction c) simp_all definition "r_code_const1_aux \ Cn 3 r_prod_encode [r_constn 2 3, Cn 3 r_prod_encode [r_constn 2 1, Cn 3 r_prod_encode [r_constn 2 1, Cn 3 r_singleton_encode [Id 3 1]]]]" lemma r_code_const1_aux_prim: "prim_recfn 3 r_code_const1_aux" by (simp_all add: r_code_const1_aux_def) lemma r_code_const1_aux: "eval r_code_const1_aux [i, r, c] \= quad_encode 3 1 1 (singleton_encode r)" by (simp add: r_code_const1_aux_def) definition "r_code_const1 \ r_shrink (Pr 1 Z r_code_const1_aux)" lemma r_code_const1_prim: "prim_recfn 1 r_code_const1" by (simp_all add: r_code_const1_def r_code_const1_aux_prim) lemma r_code_const1: "eval r_code_const1 [c] \= code_const1 c" proof - let ?h = "Pr 1 Z r_code_const1_aux" have "eval ?h [c, x] \= code_const1 c" for x using r_code_const1_aux r_code_const1_def by (induction c) (simp_all add: r_code_const1_aux_prim) then show ?thesis by (simp add: r_code_const1_def r_code_const1_aux_prim) qed text \Functions that compute codes of higher-arity constant functions:\ definition code_constn :: "nat \ nat \ nat" where "code_constn n c \ if n = 1 then code_const1 c else quad_encode 3 n (code_const1 c) (singleton_encode (triple_encode 2 n 0))" lemma code_constn: "code_constn (Suc n) c = encode (r_constn n c)" unfolding code_constn_def using code_const1 r_constn_def by (cases "n = 0") simp_all definition r_code_constn :: "nat \ recf" where "r_code_constn n \ if n = 1 then r_code_const1 else Cn 1 r_prod_encode [r_const 3, Cn 1 r_prod_encode [r_const n, Cn 1 r_prod_encode [r_code_const1, Cn 1 r_singleton_encode [Cn 1 r_prod_encode [r_const 2, Cn 1 r_prod_encode [r_const n, Z]]]]]]" lemma r_code_constn_prim: "prim_recfn 1 (r_code_constn n)" by (simp_all add: r_code_constn_def r_code_const1_prim) lemma r_code_constn: "eval (r_code_constn n) [c] \= code_constn n c" by (auto simp add: r_code_constn_def r_code_const1 code_constn_def r_code_const1_prim) text \Computing codes of $m$-ary projections:\ definition code_id :: "nat \ nat \ nat" where "code_id m n \ triple_encode 2 m n" lemma code_id: "encode (Id m n) = code_id m n" unfolding code_id_def by simp text \The functions $s^m_n$ are represented by the following function. The value $m$ corresponds to the length of @{term "cs"}.\ definition smn :: "nat \ nat \ nat list \ nat" where "smn n p cs \ quad_encode 3 n (encode (r_universal (n + length cs))) (list_encode (code_constn n p # map (code_constn n) cs @ map (code_id n) [0.. 0" shows "smn n p cs = encode (Cn n (r_universal (n + length cs)) (r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..The next function is to help us define @{typ recf}s corresponding to the $s^m_n$ functions. It maps $m + 1$ arguments $p, c_1, \ldots, c_m$ to an encoded list of length $m + n + 1$. The list comprises the $m + 1$ codes of the $n$-ary constants $p, c_1, \ldots, c_m$ and the $n$ codes for all $n$-ary projections.\ definition r_smn_aux :: "nat \ nat \ recf" where "r_smn_aux n m \ Cn (Suc m) (r_list_encode (m + n)) (map (\i. Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) [0..i. r_constn m (code_id n i)) [0.. 0 \ prim_recfn (Suc m) (r_smn_aux n m)" by (auto simp add: r_smn_aux_def r_code_constn_prim) lemma r_smn_aux: assumes "n > 0" and "length cs = m" shows "eval (r_smn_aux n m) (p # cs) \= list_encode (map (code_constn n) (p # cs) @ map (code_id n) [0..g. eval g (p # cs)) ?xs = map Some (map (code_constn n) (p # cs))" proof (intro nth_equalityI) show len: "length (map (\g. eval g (p # cs)) ?xs) = length (map Some (map (code_constn n) (p # cs)))" by (simp add: assms(2)) have "map (\g. eval g (p # cs)) ?xs ! i = map Some (map (code_constn n) (p # cs)) ! i" if "i < Suc m" for i proof - have "map (\g. eval g (p # cs)) ?xs ! i = (\g. eval g (p # cs)) (?xs ! i)" using len_xs that by (metis nth_map) also have "... = eval (Cn (Suc m) (r_code_constn n) [Id (Suc m) i]) (p # cs)" using that len_xs by (metis (no_types, lifting) add.left_neutral length_map nth_map nth_upt) also have "... = eval (r_code_constn n) [the (eval (Id (Suc m) i) (p # cs))]" using r_code_constn_prim assms(2) that by simp also have "... = eval (r_code_constn n) [(p # cs) ! i]" using len that by simp finally have "map (\g. eval g (p # cs)) ?xs ! i \= code_constn n ((p # cs) ! i)" using r_code_constn by simp then show ?thesis using len_xs len that by (metis length_map nth_map) qed moreover have "length (map (\g. eval g (p # cs)) ?xs) = Suc m" by simp ultimately show "\i. i < length (map (\g. eval g (p # cs)) ?xs) \ map (\g. eval g (p # cs)) ?xs ! i = map Some (map (code_constn n) (p # cs)) ! i" by simp qed moreover have "map (\g. eval g (p # cs)) ?ys = map Some (map (code_id n) [0..g. eval g (p # cs)) (?xs @ ?ys) = map Some (map (code_constn n) (p # cs) @ map (code_id n) [0..x. the (eval x (p # cs))) (?xs @ ?ys) = map the (map (\x. eval x (p # cs)) (?xs @ ?ys))" by simp ultimately have *: "map (\g. the (eval g (p # cs))) (?xs @ ?ys) = (map (code_constn n) (p # cs) @ map (code_id n) [0..ig. eval g (p # cs)) ?xs ! i" by (metis nth_map) then have "\ii" using assms map_xs by (metis length_map nth_map option.simps(3)) then have xs_converg: "\z\set ?xs. eval z (p # cs) \" by (metis in_set_conv_nth) have "\ix. eval x (p # cs)) ?ys ! i" by simp then have "\ii" by simp then have "\z\set (?xs @ ?ys). eval z (p # cs) \" using xs_converg by auto moreover have "recfn (length (p # cs)) (Cn (Suc m) (r_list_encode (m + n)) (?xs @ ?ys))" using assms r_code_constn_prim by auto ultimately have "eval (r_smn_aux n m) (p # cs) = eval (r_list_encode (m + n)) (map (\g. the (eval g (p # cs))) (?xs @ ?ys))" unfolding r_smn_aux_def using assms by simp then have "eval (r_smn_aux n m) (p # cs) = eval (r_list_encode (m + n)) (map (code_constn n) (p # cs) @ map (code_id n) [0..For all $m, n > 0$, the @{typ recf} corresponding to $s^m_n$ is given by the next function.\ definition r_smn :: "nat \ nat \ recf" where "r_smn n m \ Cn (Suc m) r_prod_encode [r_constn m 3, Cn (Suc m) r_prod_encode [r_constn m n, Cn (Suc m) r_prod_encode [r_constn m (encode (r_universal (n + m))), r_smn_aux n m]]]" lemma r_smn_prim [simp]: "n > 0 \ prim_recfn (Suc m) (r_smn n m)" by (simp_all add: r_smn_def r_smn_aux_prim) lemma r_smn: assumes "n > 0" and "length cs = m" shows "eval (r_smn n m) (p # cs) \= smn n p cs" using assms r_smn_def r_smn_aux smn_def r_smn_aux_prim by simp lemma map_eval_Some_the: assumes "map (\g. eval g xs) gs = map Some ys" shows "map (\g. the (eval g xs)) gs = ys" using assms by (metis (no_types, lifting) length_map nth_equalityI nth_map option.sel) text \The essential part of the $s$-$m$-$n$ theorem: For all $m, n > 0$ the function $s^m_n$ satisfies \[ \varphi_p^{(m + n)}(c_1, \dots,c_m, x_1, \dots, x_n) = \varphi_{s^m_n(p, c_1, \dots,c_m)}^{(n)}(x_1, \dots, x_n) \] for all $p, c_i, x_j$.\ lemma smn_lemma: assumes "n > 0" and len_cs: "length cs = m" and len_xs: "length xs = n" shows "eval (r_universal (m + n)) (p # cs @ xs) = eval (r_universal n) ((the (eval (r_smn n m) (p # cs))) # xs)" proof - let ?s = "r_smn n m" let ?f = "Cn n (r_universal (n + length cs)) (r_constn (n - 1) p # map (r_constn (n - 1)) cs @ (map (Id n) [0..= smn n p cs" using assms r_smn by simp then have eval_s: "eval ?s (p # cs) \= encode ?f" by (simp add: assms(1) smn) have "recfn n ?f" using len_cs assms by auto then have *: "eval (r_universal n) ((encode ?f) # xs) = eval ?f xs" using r_universal[of ?f n, OF _ len_xs] by simp let ?gs = "r_constn (n - 1) p # map (r_constn (n - 1)) cs @ map (Id n) [0..g\set ?gs. eval g xs \" using len_cs len_xs assms by auto then have "eval ?f xs = eval (r_universal (n + length cs)) (map (\g. the (eval g xs)) ?gs)" using len_cs len_xs assms `recfn n ?f` by simp then have "eval ?f xs = eval (r_universal (m + n)) (map (\g. the (eval g xs)) ?gs)" by (simp add: len_cs add.commute) then have "eval (r_universal n) ((the (eval ?s (p # cs))) # xs) = eval (r_universal (m + n)) (map (\g. the (eval g xs)) ?gs)" using eval_s * by simp moreover have "map (\g. the (eval g xs)) ?gs = p # cs @ xs" proof (intro nth_equalityI) show "length (map (\g. the (eval g xs)) ?gs) = length (p # cs @ xs)" by (simp add: len_xs) have len: "length (map (\g. the (eval g xs)) ?gs) = Suc (m + n)" by (simp add: len_cs) moreover have "map (\g. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i" if "i < Suc (m + n)" for i proof - from that consider "i = 0" | "i > 0 \ i < Suc m" | "Suc m \ i \ i < Suc (m + n)" using not_le_imp_less by auto then show ?thesis proof (cases) case 1 then show ?thesis using assms(1) len_xs by simp next case 2 then have "?gs ! i = (map (r_constn (n - 1)) cs) ! (i - 1)" using len_cs by (metis One_nat_def Suc_less_eq Suc_pred length_map less_numeral_extra(3) nth_Cons' nth_append) then have "map (\g. the (eval g xs)) ?gs ! i = (\g. the (eval g xs)) ((map (r_constn (n - 1)) cs) ! (i - 1))" using len by (metis length_map nth_map that) also have "... = the (eval ((r_constn (n - 1) (cs ! (i - 1)))) xs)" using 2 len_cs by auto also have "... = cs ! (i - 1)" using r_constn len_xs assms(1) by simp also have "... = (p # cs @ xs) ! i" using 2 len_cs by (metis diff_Suc_1 less_Suc_eq_0_disj less_numeral_extra(3) nth_Cons' nth_append) finally show ?thesis . next case 3 then have "?gs ! i = (map (Id n) [0..g. the (eval g xs)) ?gs ! i = (\g. the (eval g xs)) ((map (Id n) [0..g. the (eval g xs)) ?gs ! i = (p # cs @ xs) ! i" if "i < length (map (\g. the (eval g xs)) ?gs)" for i using that by simp qed ultimately show ?thesis by simp qed theorem smn_theorem: assumes "n > 0" shows "\s. prim_recfn (Suc m) s \ (\p cs xs. length cs = m \ length xs = n \ eval (r_universal (m + n)) (p # cs @ xs) = eval (r_universal n) ((the (eval s (p # cs))) # xs))" using smn_lemma exI[of _ "r_smn n m"] assms by simp text \For every numbering, that is, binary partial recursive function, $\psi$ there is a total recursive function $c$ that translates $\psi$-indices into $\varphi$-indices.\ lemma numbering_translation: assumes "recfn 2 psi" obtains c where "recfn 1 c" "total c" "\i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]" proof - let ?p = "encode psi" define c where "c = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]" then have "prim_recfn 1 c" by simp moreover from this have "total c" by auto moreover have "eval r_phi [the (eval c [i]), x] = eval psi [i, x]" for i x proof - have "eval c [i] = eval (r_smn 1 1) [?p, i]" using c_def by simp then have "eval (r_universal 1) [the (eval c [i]), x] = eval (r_universal 1) [the (eval (r_smn 1 1) [?p, i]), x]" by simp also have "... = eval (r_universal (1 + 1)) (?p # [i] @ [x])" using smn_lemma[of 1 "[i]" 1 "[x]" ?p] by simp also have "... = eval (r_universal 2) [?p, i, x]" by (metis append_eq_Cons_conv nat_1_add_1) also have "... = eval psi [i, x]" using r_universal[OF assms, of "[i, x]"] by simp finally have "eval (r_universal 1) [the (eval c [i]), x] = eval psi [i, x]" . then show ?thesis using r_phi_def by simp qed ultimately show ?thesis using that by auto qed section \Fixed-point theorems\ text \Fixed-point theorems (also known as recursion theorems) come in many shapes. We prove the minimum we need for Chapter~\ref{c:iirf}.\ subsection \Rogers's fixed-point theorem\ text \In this section we prove a theorem that Rogers~\cite{Rogers87} credits to Kleene, but admits that it is a special case and not the original formulation. We follow Wikipedia~\cite{wiki-krt} and call it the Rogers's fixed-point theorem.\ lemma s11_inj: "inj (\x. smn 1 p [x])" proof fix x\<^sub>1 x\<^sub>2 :: nat assume "smn 1 p [x\<^sub>1] = smn 1 p [x\<^sub>2]" then have "list_encode [code_constn 1 p, code_constn 1 x\<^sub>1, code_id 1 0] = list_encode [code_constn 1 p, code_constn 1 x\<^sub>2, code_id 1 0]" using smn_def by (simp add: prod_encode_eq) then have "[code_constn 1 p, code_constn 1 x\<^sub>1, code_id 1 0] = [code_constn 1 p, code_constn 1 x\<^sub>2, code_id 1 0]" using list_decode_encode by metis then have "code_constn 1 x\<^sub>1 = code_constn 1 x\<^sub>2" by simp then show "x\<^sub>1 = x\<^sub>2" using code_const1 code_constn code_constn_def encode_injective r_constn by (metis One_nat_def length_Cons list.size(3) option.simps(1)) qed definition "r_univuniv \ Cn 2 r_phi [Cn 2 r_phi [Id 2 0, Id 2 0], Id 2 1]" lemma r_univuniv_recfn: "recfn 2 r_univuniv" by (simp add: r_univuniv_def) lemma r_univuniv_converg: assumes "eval r_phi [x, x] \" shows "eval r_univuniv [x, y] = eval r_phi [the (eval r_phi [x, x]), y]" unfolding r_univuniv_def using assms r_univuniv_recfn r_phi_recfn by simp text \Strictly speaking this is a generalization of Rogers's theorem in that it shows the existence of infinitely many fixed-points. In conventional terms it says that for every total recursive $f$ and $k \in \mathbb{N}$ there is an $n \geq k$ with $\varphi_n = \varphi_{f(n)}$.\ theorem rogers_fixed_point_theorem: fixes k :: nat assumes "recfn 1 f" and "total f" shows "\n\k. \x. eval r_phi [n, x] = eval r_phi [the (eval f [n]), x]" proof - let ?p = "encode r_univuniv" define h where "h = Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]" then have "prim_recfn 1 h" by simp then have "total h" by blast have "eval h [x] = eval (Cn 1 (r_smn 1 1) [r_const ?p, Id 1 0]) [x]" for x unfolding h_def by simp then have h: "the (eval h [x]) = smn 1 ?p [x]" for x by (simp add: r_smn) have "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]" for x y proof - have "eval r_phi [the (eval h [x]), y] = eval r_phi [smn 1 ?p [x], y]" using h by simp also have "... = eval r_phi [the (eval (r_smn 1 1) [?p, x]), y]" by (simp add: r_smn) also have "... = eval (r_universal 2) [?p, x, y]" using r_phi_def smn_lemma[of 1 "[x]" 1 "[y]" ?p] by (metis Cons_eq_append_conv One_nat_def Suc_1 length_Cons less_numeral_extra(1) list.size(3) plus_1_eq_Suc) finally show "eval r_phi [the (eval h [x]), y] = eval r_univuniv [x, y]" using r_universal r_univuniv_recfn by simp qed then have *: "eval r_phi [the (eval h [x]), y] = eval r_phi [the (eval r_phi [x, x]), y]" if "eval r_phi [x, x] \" for x y using r_univuniv_converg that by simp let ?fh = "Cn 1 f [h]" have "recfn 1 ?fh" using `prim_recfn 1 h` assms by simp then have "infinite {r. recfn 1 r \ r \ ?fh}" using exteq_infinite[of ?fh 1] by simp then have "infinite (encode ` {r. recfn 1 r \ r \ ?fh})" (is "infinite ?E") using encode_injective by (meson finite_imageD inj_onI) then have "infinite ((\x. smn 1 ?p [x]) ` ?E)" using s11_inj[of ?p] by (simp add: finite_image_iff inj_on_subset) moreover have "(\x. smn 1 ?p [x]) ` ?E = {smn 1 ?p [encode r] |r. recfn 1 r \ r \ ?fh}" by auto ultimately have "infinite {smn 1 ?p [encode r] |r. recfn 1 r \ r \ ?fh}" by simp then obtain n where "n \ k" "n \ {smn 1 ?p [encode r] |r. recfn 1 r \ r \ ?fh}" by (meson finite_nat_set_iff_bounded_le le_cases) then obtain r where r: "recfn 1 r" "n = smn 1 ?p [encode r]" "recfn 1 r \ r \ ?fh" by auto then have eval_r: "eval r [encode r] = eval ?fh [encode r]" by (simp add: exteq_def) then have eval_r': "eval r [encode r] = eval f [the (eval h [encode r])]" using assms `total h` `prim_recfn 1 h` by simp then have "eval r [encode r] \" using `prim_recfn 1 h` assms(1,2) by simp then have "eval r_phi [encode r, encode r] \" by (simp add: \recfn 1 r\ r_phi) then have "eval r_phi [the (eval h [encode r]), y] = eval r_phi [(the (eval r_phi [encode r, encode r])), y]" for y using * by simp then have "eval r_phi [the (eval h [encode r]), y] = eval r_phi [(the (eval r [encode r])), y]" for y by (simp add: \recfn 1 r\ r_phi) moreover have "n = the (eval h [encode r])" by (simp add: h r(2)) ultimately have "eval r_phi [n, y] = eval r_phi [the (eval r [encode r]), y]" for y by simp then have "eval r_phi [n, y] = eval r_phi [the (eval ?fh [encode r]), y]" for y using r by (simp add: eval_r) moreover have "eval ?fh [encode r] = eval f [n]" using eval_r eval_r' \n = the (eval h [encode r])\ by auto ultimately have "eval r_phi [n, y] = eval r_phi [the (eval f [n]), y]" for y by simp with `n \ k` show ?thesis by auto qed subsection \Kleene's fixed-point theorem\ text \The next theorem is what Rogers~\cite[p.~214]{Rogers87} calls Kleene's version of what we call Rogers's fixed-point theorem. More precisely this would be Kleene's \emph{second} fixed-point theorem, but since we do not cover the first one, we leave out the number.\ theorem kleene_fixed_point_theorem: fixes k :: nat assumes "recfn 2 psi" shows "\n\k. \x. eval r_phi [n, x] = eval psi [n, x]" proof - from numbering_translation[OF assms] obtain c where c: "recfn 1 c" "total c" "\i x. eval psi [i, x] = eval r_phi [the (eval c [i]), x]" by auto then obtain n where "n \ k" and "\x. eval r_phi [n, x] = eval r_phi [the (eval c [n]), x]" using rogers_fixed_point_theorem by blast with c(3) have "\x. eval r_phi [n, x] = eval psi [n, x]" by simp with `n \ k` show ?thesis by auto qed text \Kleene's fixed-point theorem can be generalized to arbitrary arities. But we need to generalize it only to binary functions in order to show Smullyan's double fixed-point theorem in Section~\ref{s:smullyan}.\ definition "r_univuniv2 \ Cn 3 r_phi [Cn 3 (r_universal 2) [Id 3 0, Id 3 0, Id 3 1], Id 3 2]" lemma r_univuniv2_recfn: "recfn 3 r_univuniv2" by (simp add: r_univuniv2_def) lemma r_univuniv2_converg: assumes "eval (r_universal 2) [u, u, x] \" shows "eval r_univuniv2 [u, x, y] = eval r_phi [the (eval (r_universal 2) [u, u, x]), y]" unfolding r_univuniv2_def using assms r_univuniv2_recfn by simp theorem kleene_fixed_point_theorem_2: assumes "recfn 2 f" and "total f" shows "\n. recfn 1 n \ total n \ (\x y. eval r_phi [(the (eval n [x])), y] = eval r_phi [(the (eval f [the (eval n [x]), x])), y])" proof - let ?p = "encode r_univuniv2" let ?s = "r_smn 1 2" define h where "h = Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]" then have [simp]: "prim_recfn 2 h" by simp { fix u x y have "eval h [u, x] = eval (Cn 2 ?s [r_dummy 1 (r_const ?p), Id 2 0, Id 2 1]) [u, x]" using h_def by simp then have "the (eval h [u, x]) = smn 1 ?p [u, x]" by (simp add: r_smn) then have "eval r_phi [the (eval h [u, x]), y] = eval r_phi [smn 1 ?p [u, x], y]" by simp also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_constn 0 ?p # r_constn 0 u # r_constn 0 x # [Id 1 0])), y]" using smn[of 1 ?p "[u, x]"] by (simp add: numeral_3_eq_3) also have "... = eval r_phi [encode (Cn 1 (r_universal 3) (r_const ?p # r_const u # r_const x # [Id 1 0])), y]" (is "_ = eval r_phi [encode ?f, y]") by (simp add: r_constn_def) also have "... = eval ?f [y]" using r_phi'[of ?f] by auto also have "... = eval (r_universal 3) [?p, u, x, y]" using r_univuniv2_recfn r_universal r_phi by auto also have "... = eval r_univuniv2 [u, x, y]" - using r_universal by (simp add: r_univuniv2_recfn) + using r_universal + by (simp add: r_universal r_univuniv2_recfn) finally have "eval r_phi [the (eval h [u, x]), y] = eval r_univuniv2 [u, x, y]" . } then have *: "eval r_phi [the (eval h [u, x]), y] = eval r_phi [the (eval (r_universal 2) [u, u, x]), y]" if "eval (r_universal 2) [u, u, x] \" for u x y using r_univuniv2_converg that by simp let ?fh = "Cn 2 f [h, Id 2 1]" let ?e = "encode ?fh" have "recfn 2 ?fh" using assms by simp have "total h" by auto then have "total ?fh" using assms Cn_total totalI2[of ?fh] by fastforce let ?n = "Cn 1 h [r_const ?e, Id 1 0]" have "recfn 1 ?n" using assms by simp moreover have "total ?n" using `total h` totalI1[of ?n] by simp moreover { fix x y have "eval r_phi [(the (eval ?n [x])), y] = eval r_phi [(the (eval h [?e, x])), y]" by simp also have "... = eval r_phi [the (eval (r_universal 2) [?e, ?e, x]), y]" using * r_universal[of _ 2] totalE[of ?fh 2] \total ?fh\ \recfn 2 ?fh\ by (metis length_Cons list.size(3) numeral_2_eq_2) also have "... = eval r_phi [the (eval f [the (eval h [?e, x]), x]), y]" proof - have "eval (r_universal 2) [?e, ?e, x] \" using totalE[OF `total ?fh`] `recfn 2 ?fh` r_universal by (metis length_Cons list.size(3) numeral_2_eq_2) moreover have "eval (r_universal 2) [?e, ?e, x] = eval ?fh [?e, x]" by (metis \recfn 2 ?fh\ length_Cons list.size(3) numeral_2_eq_2 r_universal) then show ?thesis using assms `total h` by simp qed also have "... = eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]" by simp finally have "eval r_phi [(the (eval ?n [x])), y] = eval r_phi [(the (eval f [the (eval ?n [x]), x])), y]" . } ultimately show ?thesis by blast qed subsection \Smullyan's double fixed-point theorem\label{s:smullyan}\ theorem smullyan_double_fixed_point_theorem: assumes "recfn 2 g" and "total g" and "recfn 2 h" and "total h" shows "\m n. (\x. eval r_phi [m, x] = eval r_phi [the (eval g [m, n]), x]) \ (\x. eval r_phi [n, x] = eval r_phi [the (eval h [m, n]), x])" proof - obtain m where "recfn 1 m" and "total m" and m: "\x y. eval r_phi [the (eval m [x]), y] = eval r_phi [the (eval g [the (eval m [x]), x]), y]" using kleene_fixed_point_theorem_2[of g] assms(1,2) by auto define k where "k = Cn 1 h [m, Id 1 0]" then have "recfn 1 k" using `recfn 1 m` assms(3) by simp have "total (Id 1 0)" by (simp add: Mn_free_imp_total) then have "total k" using `total m` assms(4) Cn_total k_def `recfn 1 k` by simp obtain n where n: "\x. eval r_phi [n, x] = eval r_phi [the (eval k [n]), x]" using rogers_fixed_point_theorem[of k] `recfn 1 k` `total k` by blast obtain mm where mm: "eval m [n] \= mm" using `total m` `recfn 1 m` by fastforce then have "\x. eval r_phi [mm, x] = eval r_phi [the (eval g [mm, n]), x]" by (metis m option.sel) moreover have "\x. eval r_phi [n, x] = eval r_phi [the (eval h [mm, n]), x]" using k_def assms(3) `total m` `recfn 1 m` mm n by simp ultimately show ?thesis by blast qed section \Decidable and recursively enumerable sets\label{s:decidable}\ text \We defined @{term decidable} already back in Section~\ref{s:halting}: @{thm[display] decidable_def}\ text \The next theorem is adapted from @{thm[source] halting_problem_undecidable}.\ theorem halting_problem_phi_undecidable: "\ decidable {x. eval r_phi [x, x] \}" (is "\ decidable ?K") proof assume "decidable ?K" then obtain f where "recfn 1 f" and f: "\x. eval f [x] \= (if x \ ?K then 1 else 0)" using decidable_def by auto define g where "g \ Cn 1 r_ifeq_else_diverg [f, Z, Z]" then have "recfn 1 g" using `recfn 1 f` r_ifeq_else_diverg_recfn by simp then obtain i where i: "eval r_phi [i, x] = eval g [x]" for x using r_phi' by auto from g_def have "eval g [x] = (if x \ ?K then Some 0 else None)" for x using r_ifeq_else_diverg_recfn `recfn 1 f` f by simp then have "eval g [i] \ \ i \ ?K" by simp also have "... \ eval r_phi [i, i] \" by simp also have "... \ eval g [i] \" using i by simp finally have "eval g [i] \ \ eval g [i] \" . then show False by auto qed lemma decidable_complement: "decidable X \ decidable (- X)" proof - assume "decidable X" then obtain f where f: "recfn 1 f" "\x. eval f [x] \= (if x \ X then 1 else 0)" using decidable_def by auto define g where "g = Cn 1 r_not [f]" then have "recfn 1 g" by (simp add: f(1)) moreover have "eval g [x] \= (if x \ X then 0 else 1)" for x by (simp add: g_def f) ultimately show ?thesis using decidable_def by auto qed text \Finite sets are decidable.\ fun r_contains :: "nat list \ recf" where "r_contains [] = Z" | "r_contains (x # xs) = Cn 1 r_ifeq [Id 1 0, r_const x, r_const 1, r_contains xs]" lemma r_contains_prim: "prim_recfn 1 (r_contains xs)" by (induction xs) auto lemma r_contains: "eval (r_contains xs) [x] \= (if x \ set xs then 1 else 0)" proof (induction xs arbitrary: x) case Nil then show ?case by simp next case (Cons a xs) have "eval (r_contains (a # xs)) [x] = eval r_ifeq [x, a, 1, the (eval (r_contains xs) [x])]" using r_contains_prim prim_recfn_total by simp also have "... \= (if x = a then 1 else if x \ set xs then 1 else 0)" using Cons.IH by simp also have "... \= (if x = a \ x \ set xs then 1 else 0)" by simp finally show ?case by simp qed lemma finite_set_decidable: "finite X \ decidable X" proof - fix X :: "nat set" assume "finite X" then obtain xs where "X = set xs" using finite_list by auto then have "\x. eval (r_contains xs) [x] \= (if x \ X then 1 else 0)" using r_contains by simp then show "decidable X" using decidable_def r_contains_prim by blast qed definition semidecidable :: "nat set \ bool" where "semidecidable X \ (\f. recfn 1 f \ (\x. eval f [x] = (if x \ X then Some 1 else None)))" text \The semidecidable sets are the domains of partial recursive functions.\ lemma semidecidable_iff_domain: "semidecidable X \ (\f. recfn 1 f \ (\x. eval f [x] \ \ x \ X))" proof show "semidecidable X \ \f. recfn 1 f \ (\x. (eval f [x] \) = (x \ X))" using semidecidable_def by (metis option.distinct(1)) show "semidecidable X" if "\f. recfn 1 f \ (\x. (eval f [x] \) = (x \ X))" for X proof - from that obtain f where f: "recfn 1 f" "\x. (eval f [x] \) = (x \ X)" by auto let ?g = "Cn 1 (r_const 1) [f]" have "recfn 1 ?g" using f(1) by simp moreover have "\x. eval ?g [x] = (if x \ X then Some 1 else None)" using f by simp ultimately show "semidecidable X" using semidecidable_def by blast qed qed lemma decidable_imp_semidecidable: "decidable X \ semidecidable X" proof - assume "decidable X" then obtain f where f: "recfn 1 f" "\x. eval f [x] \= (if x \ X then 1 else 0)" using decidable_def by auto define g where "g = Cn 1 r_ifeq_else_diverg [f, r_const 1, r_const 1]" then have "recfn 1 g" by (simp add: f(1)) have "eval g [x] = eval r_ifeq_else_diverg [if x \ X then 1 else 0, 1, 1]" for x by (simp add: g_def f) then have "\x. x \ X \ eval g [x] \= 1" and "\x. x \ X \ eval g [x] \" by simp_all then show ?thesis using `recfn 1 g` semidecidable_def by auto qed text \A set is recursively enumerable if it is empty or the image of a total recursive function.\ definition recursively_enumerable :: "nat set \ bool" where "recursively_enumerable X \ X = {} \ (\f. recfn 1 f \ total f \ X = {the (eval f [x]) |x. x \ UNIV})" theorem recursively_enumerable_iff_semidecidable: "recursively_enumerable X \ semidecidable X" proof show "semidecidable X" if "recursively_enumerable X" for X proof (cases) assume "X = {}" then show ?thesis using finite_set_decidable decidable_imp_semidecidable recursively_enumerable_def semidecidable_def by blast next assume "X \ {}" with that obtain f where f: "recfn 1 f" "total f" "X = {the (eval f [x]) |x. x \ UNIV}" using recursively_enumerable_def by blast define h where "h = Cn 2 r_eq [Cn 2 f [Id 2 0], Id 2 1]" then have "recfn 2 h" using f(1) by simp from h_def have h: "eval h [x, y] \= 0 \ the (eval f [x]) = y" for x y using f(1,2) by simp from h_def `recfn 2 h` totalI2 f(2) have "total h" by simp define g where "g = Mn 1 h" then have "recfn 1 g" using h_def f(1) by simp then have "eval g [y] = (if (\x. eval h [x, y] \= 0 \ (\x')) then Some (LEAST x. eval h [x, y] \= 0) else None)" for y using g_def `total h` f(2) by simp then have "eval g [y] = (if \x. eval h [x, y] \= 0 then Some (LEAST x. eval h [x, y] \= 0) else None)" for y using `total h` `recfn 2 h` by simp then have "eval g [y] \ \ (\x. eval h [x, y] \= 0)" for y by simp with h have "eval g [y] \ \ (\x. the (eval f [x]) = y)" for y by simp with f(3) have "eval g [y] \ \ y \ X" for y by auto with `recfn 1 g` semidecidable_iff_domain show ?thesis by auto qed show "recursively_enumerable X" if "semidecidable X" for X proof (cases) assume "X = {}" then show ?thesis using recursively_enumerable_def by simp next assume "X \ {}" then obtain x\<^sub>0 where "x\<^sub>0 \ X" by auto from that semidecidable_iff_domain obtain f where f: "recfn 1 f" "\x. eval f [x] \ \ x \ X" by auto let ?i = "encode f" have i: "\x. eval f [x] = eval r_phi [?i, x]" using r_phi' f(1) by simp with `x\<^sub>0 \ X` f(2) have "eval r_phi [?i, x\<^sub>0] \" by simp then obtain g where g: "recfn 1 g" "total g" "\x. eval r_phi [?i, x] \ = (\y. eval g [y] \= x)" using f(1) nonempty_domain_enumerable by blast with f(2) i have "\x. x \ X = (\y. eval g [y] \= x)" by simp then have "\x. x \ X = (\y. the (eval g [y]) = x)" using totalE[OF g(2) g(1)] by (metis One_nat_def length_Cons list.size(3) option.collapse option.sel) then have "X = {the (eval g [y]) |y. y \ UNIV}" by auto with g(1,2) show ?thesis using recursively_enumerable_def by auto qed qed text \The next goal is to show that a set is decidable iff. it and its complement are semidecidable. For this we use the concurrent evaluation function.\ lemma semidecidable_decidable: assumes "semidecidable X" and "semidecidable (- X)" shows "decidable X" proof - obtain f where f: "recfn 1 f \ (\x. eval f [x] \ \ x \ X)" using assms(1) semidecidable_iff_domain by auto let ?i = "encode f" obtain g where g: "recfn 1 g \ (\x. eval g [x] \ \ x \ (- X))" using assms(2) semidecidable_iff_domain by auto let ?j = "encode g" define d where "d = Cn 1 r_pdec1 [Cn 1 r_parallel [r_const ?j, r_const ?i, Id 1 0]]" then have "recfn 1 d" by (simp add: d_def) have *: "\x. eval r_phi [?i, x] = eval f [x]" "\x. eval r_phi [?j, x] = eval g [x]" using f g r_phi' by simp_all have "eval d [x] \= 1" if "x \ X" for x proof - have "eval f [x] \" using f that by simp moreover have "eval g [x] \" using g that by blast ultimately have "eval r_parallel [?j, ?i, x] \= prod_encode (1, the (eval f [x]))" using * r_parallel(3) by simp with d_def show ?thesis by simp qed moreover have "eval d [x] \= 0" if "x \ X" for x proof - have "eval g [x] \" using g that by simp moreover have "eval f [x] \" using f that by blast ultimately have "eval r_parallel [?j, ?i, x] \= prod_encode (0, the (eval g [x]))" using * r_parallel(2) by blast with d_def show ?thesis by simp qed ultimately show ?thesis using decidable_def `recfn 1 d` by auto qed theorem decidable_iff_semidecidable_complement: "decidable X \ semidecidable X \ semidecidable (- X)" using semidecidable_decidable decidable_imp_semidecidable decidable_complement by blast section \Rice's theorem\ definition index_set :: "nat set \ bool" where "index_set I \ \i j. i \ I \ (\x. eval r_phi [i, x] = eval r_phi [j, x]) \ j \ I" lemma index_set_closed_in: assumes "index_set I" and "i \ I" and "\x. eval r_phi [i, x] = eval r_phi [j, x]" shows "j \ I" using index_set_def assms by simp lemma index_set_closed_not_in: assumes "index_set I" and "i \ I" and "\x. eval r_phi [i, x] = eval r_phi [j, x]" shows "j \ I" using index_set_def assms by metis theorem rice_theorem: assumes "index_set I" and "I \ UNIV" and "I \ {}" shows "\ decidable I" proof assume "decidable I" then obtain d where d: "recfn 1 d" "\i. eval d [i] \= (if i \ I then 1 else 0)" using decidable_def by auto obtain j\<^sub>1 j\<^sub>2 where "j\<^sub>1 \ I" and "j\<^sub>2 \ I" using assms(2,3) by auto let ?if = "Cn 2 r_ifz [Cn 2 d [Id 2 0], r_dummy 1 (r_const j\<^sub>2), r_dummy 1 (r_const j\<^sub>1)]" define psi where "psi = Cn 2 r_phi [?if, Id 2 1] " then have "recfn 2 psi" by (simp add: d) have "eval ?if [x, y] = Some (if x \ I then j\<^sub>1 else j\<^sub>2)" for x y by (simp add: d) moreover have "eval psi [x, y] = eval (Cn 2 r_phi [?if, Id 2 1]) [x, y]" for x y using psi_def by simp ultimately have psi: "eval psi [x, y] = eval r_phi [if x \ I then j\<^sub>1 else j\<^sub>2, y]" for x y by (simp add: d) then have in_I: "eval psi [x, y] = eval r_phi [j\<^sub>1, y]" if "x \ I" for x y by (simp add: that) have not_in_I: "eval psi [x, y] = eval r_phi [j\<^sub>2, y]" if "x \ I" for x y by (simp add: psi that) obtain n where n: "\x. eval r_phi [n, x] = eval psi [n, x]" using kleene_fixed_point_theorem[OF `recfn 2 psi`] by auto show False proof cases assume "n \ I" then have "\x. eval r_phi [n, x] = eval r_phi [j\<^sub>1, x]" using n in_I by simp then have "n \ I" using `j\<^sub>1 \ I` index_set_closed_not_in[OF assms(1)] by simp with `n \ I` show False by simp next assume "n \ I" then have "\x. eval r_phi [n, x] = eval r_phi [j\<^sub>2, x]" using n not_in_I by simp then have "n \ I" using `j\<^sub>2 \ I` index_set_closed_in[OF assms(1)] by simp with `n \ I` show False by simp qed qed section \Partial recursive functions as actual functions\label{s:alternative}\ text \A well-formed @{typ recf} describes an algorithm. Usually, however, partial recursive functions are considered to be partial functions, that is, right-unique binary relations. This distinction did not matter much until now, because we were mostly concerned with the \emph{existence} of partial recursive functions, which is equivalent to the existence of algorithms. Whenever it did matter, we could use the extensional equivalence @{term "exteq"}. In Chapter~\ref{c:iirf}, however, we will deal with sets of functions and sets of sets of functions. For illustration consider the singleton set containing only the unary zero function. It could be expressed by @{term "{Z}"}, but this would not contain @{term[names_short] "Cn 1 (Id 1 0) [Z]"}, which computes the same function. The alternative representation as @{term "{f. f \ Z}"} is not a singleton set. Another alternative would be to identify partial recursive functions with the equivalence classes of @{term "exteq"}. This would work for all arities. But since we will only need unary and binary functions, we can go for the less general but simpler alternative of regarding partial recursive functions as certain functions of types @{typ "nat \ nat option"} and @{typ "nat \ nat \ nat option"}. With this notation we can represent the aforementioned set by @{term "{\_. Some (0::nat)}"} and express that the function @{term "\_. Some (0::nat)"} is total recursive. In addition terms get shorter, for instance, @{term "eval r_func [i, x]"} becomes @{term "func i x"}.\ subsection \The definitions\ type_synonym partial1 = "nat \ nat option" type_synonym partial2 = "nat \ nat \ nat option" definition total1 :: "partial1 \ bool" where "total1 f \ \x. f x \" definition total2 :: "partial2 \ bool" where "total2 f \ \x y. f x y \" lemma total1I [intro]: "(\x. f x \) \ total1 f" using total1_def by simp lemma total2I [intro]: "(\x y. f x y \) \ total2 f" using total2_def by simp lemma total1E [dest, simp]: "total1 f \ f x \" using total1_def by simp lemma total2E [dest, simp]: "total2 f \ f x y \" using total2_def by simp definition P1 :: "partial1 set" ("\

") where "\

\ {\x. eval r [x] |r. recfn 1 r}" definition P2 :: "partial2 set" ("\

\<^sup>2") where "\

\<^sup>2 \ {\x y. eval r [x, y] |r. recfn 2 r}" definition R1 :: "partial1 set" ("\") where "\ \ {\x. eval r [x] |r. recfn 1 r \ total r}" definition R2 :: "partial2 set" ("\\<^sup>2") where "\\<^sup>2 \ {\x y. eval r [x, y] |r. recfn 2 r \ total r}" definition Prim1 :: "partial1 set" where "Prim1 \ {\x. eval r [x] |r. prim_recfn 1 r}" definition Prim2 :: "partial2 set" where "Prim2 \ {\x y. eval r [x, y] |r. prim_recfn 2 r}" lemma R1_imp_P1 [simp, elim]: "f \ \ \ f \ \

" using R1_def P1_def by auto lemma R2_imp_P2 [simp, elim]: "f \ \\<^sup>2 \ f \ \

\<^sup>2" using R2_def P2_def by auto lemma Prim1_imp_R1 [simp, elim]: "f \ Prim1 \ f \ \" unfolding Prim1_def R1_def by auto lemma Prim2_imp_R2 [simp, elim]: "f \ Prim2 \ f \ \\<^sup>2" unfolding Prim2_def R2_def by auto lemma P1E [elim]: assumes "f \ \

" obtains r where "recfn 1 r" and "\x. eval r [x] = f x" using assms P1_def by force lemma P2E [elim]: assumes "f \ \

\<^sup>2" obtains r where "recfn 2 r" and "\x y. eval r [x, y] = f x y" using assms P2_def by force lemma P1I [intro]: assumes "recfn 1 r" and "(\x. eval r [x]) = f" shows "f \ \

" using assms P1_def by auto lemma P2I [intro]: assumes "recfn 2 r" and "\x y. eval r [x, y] = f x y" shows "f \ \

\<^sup>2" proof - have "(\x y. eval r [x, y]) = f" using assms(2) by simp then show ?thesis using assms(1) P2_def by auto qed lemma R1I [intro]: assumes "recfn 1 r" and "total r" and "\x. eval r [x] = f x" shows "f \ \" unfolding R1_def using CollectI[of "\f. \r. f = (\x. eval r [x]) \ recfn 1 r \ total r" f] assms by metis lemma R1E [elim]: assumes "f \ \" obtains r where "recfn 1 r" and "total r" and "f = (\x. eval r [x])" using assms R1_def by auto lemma R2I [intro]: assumes "recfn 2 r" and "total r" and "\x y. eval r [x, y] = f x y" shows "f \ \\<^sup>2" unfolding R2_def using CollectI[of "\f. \r. f = (\x y. eval r [x, y]) \ recfn 2 r \ total r" f] assms by metis lemma R1_SOME: assumes "f \ \" and "r = (SOME r'. recfn 1 r' \ total r' \ f = (\x. eval r' [x]))" (is "r = (SOME r'. ?P r')") shows "recfn 1 r" and "\x. eval r [x] \" and "\x. f x = eval r [x]" and "f = (\x. eval r [x])" proof - obtain r' where "?P r'" using R1E[OF assms(1)] by auto then show "recfn 1 r" "\b. eval r [b] \" "\x. f x = eval r [x]" using someI[of ?P r'] assms(2) totalE[of r] by (auto, metis) then show "f = (\x. eval r [x])" by auto qed lemma R2E [elim]: assumes "f \ \\<^sup>2" obtains r where "recfn 2 r" and "total r" and "f = (\x\<^sub>1 x\<^sub>2. eval r [x\<^sub>1, x\<^sub>2])" using assms R2_def by auto lemma R1_imp_total1 [simp]: "f \ \ \ total1 f" using total1I by fastforce lemma R2_imp_total2 [simp]: "f \ \\<^sup>2 \ total2 f" using totalE by fastforce lemma Prim1I [intro]: assumes "prim_recfn 1 r" and "\x. f x = eval r [x]" shows "f \ Prim1" using assms Prim1_def by blast lemma Prim2I [intro]: assumes "prim_recfn 2 r" and "\x y. f x y = eval r [x, y]" shows "f \ Prim2" using assms Prim2_def by blast lemma P1_total_imp_R1 [intro]: assumes "f \ \

" and "total1 f" shows "f \ \" using assms totalI1 by force lemma P2_total_imp_R2 [intro]: assumes "f \ \

\<^sup>2 " and "total2 f" shows "f \ \\<^sup>2" using assms totalI2 by force subsection \Some simple properties\ text \In order to show that a @{typ partial1} or @{typ partial2} function is in @{term "\

"}, @{term "\

\<^sup>2"}, @{term "\"}, @{term "\\<^sup>2"}, @{term "Prim1"}, or @{term "Prim2"} we will usually have to find a suitable @{typ recf}. But for some simple or frequent cases this section provides shortcuts.\ lemma identity_in_R1: "Some \ \" proof - have "\x. eval (Id 1 0) [x] \= x" by simp moreover have "recfn 1 (Id 1 0)" by simp moreover have "total (Id 1 0)" by (simp add: totalI1) ultimately show ?thesis by blast qed lemma P2_proj_P1 [simp, elim]: assumes "\ \ \

\<^sup>2" shows "\ i \ \

" proof - from assms obtain u where u: "recfn 2 u" "(\x\<^sub>1 x\<^sub>2. eval u [x\<^sub>1, x\<^sub>2]) = \" by auto define v where "v \ Cn 1 u [r_const i, Id 1 0]" then have "recfn 1 v" "(\x. eval v [x]) = \ i" using u by auto then show ?thesis by auto qed lemma R2_proj_R1 [simp, elim]: assumes "\ \ \\<^sup>2" shows "\ i \ \" proof - from assms have "\ \ \

\<^sup>2" by simp then have "\ i \ \

" by auto moreover have "total1 (\ i)" using assms by (simp add: total1I) ultimately show ?thesis by auto qed lemma const_in_Prim1: "(\_. Some c) \ Prim1" proof - define r where "r = r_const c" then have "\x. eval r [x] = Some c" by simp moreover have "recfn 1 r" "Mn_free r" using r_def by simp_all ultimately show ?thesis by auto qed lemma concat_P1_P1: assumes "f \ \

" and "g \ \

" shows "(\x. if g x \ \ f (the (g x)) \ then Some (the (f (the (g x)))) else None) \ \

" (is "?h \ \

") proof - obtain rf where rf: "recfn 1 rf" "\x. eval rf [x] = f x" using assms(1) by auto obtain rg where rg: "recfn 1 rg" "\x. eval rg [x] = g x" using assms(2) by auto let ?rh = "Cn 1 rf [rg]" have "recfn 1 ?rh" using rf(1) rg(1) by simp moreover have "eval ?rh [x] = ?h x" for x using rf rg by simp ultimately show ?thesis by blast qed lemma P1_update_P1: assumes "f \ \

" shows "f(x:=z) \ \

" proof (cases z) case None define re where "re \ Mn 1 (r_constn 1 1)" from assms obtain r where r: "recfn 1 r" "(\u. eval r [u]) = f" by auto define r' where "r' = Cn 1 (r_lifz re r) [Cn 1 r_eq [Id 1 0, r_const x], Id 1 0]" have "recfn 1 r'" using r(1) r'_def re_def by simp then have "eval r' [u] = eval (r_lifz re r) [if u = x then 0 else 1, u]" for u using r'_def by simp with r(1) have "eval r' [u] = (if u = x then None else eval r [u])" for u using re_def re_def by simp with r(2) have "eval r' [u] = (f(x:=None)) u" for u by auto then have "(\u. eval r' [u]) = f(x:=None)" by auto with None `recfn 1 r'` show ?thesis by auto next case (Some y) from assms obtain r where r: "recfn 1 r" "(\u. eval r [u]) = f" by auto define r' where "r' \ Cn 1 (r_lifz (r_const y) r) [Cn 1 r_eq [Id 1 0, r_const x], Id 1 0]" have "recfn 1 r'" using r(1) r'_def by simp then have "eval r' [u] = eval (r_lifz (r_const y) r) [if u = x then 0 else 1, u]" for u using r'_def by simp with r(1) have "eval r' [u] = (if u = x then Some y else eval r [u])" for u by simp with r(2) have "eval r' [u] = (f(x:=Some y)) u" for u by auto then have "(\u. eval r' [u]) = f(x:=Some y)" by auto with Some `recfn 1 r'` show ?thesis by auto qed lemma swap_P2: assumes "f \ \

\<^sup>2" shows "(\x y. f y x) \ \

\<^sup>2" proof - obtain r where r: "recfn 2 r" "\x y. eval r [x, y] = f x y" using assms by auto then have "eval (r_swap r) [x, y] = f y x" for x y by simp moreover have "recfn 2 (r_swap r)" using r_swap_recfn r(1) by simp ultimately show ?thesis by auto qed lemma swap_R2: assumes "f \ \\<^sup>2" shows "(\x y. f y x) \ \\<^sup>2" using swap_P2[of f] assms by (meson P2_total_imp_R2 R2_imp_P2 R2_imp_total2 total2E total2I) lemma skip_P1: assumes "f \ \

" shows "(\x. f (x + n)) \ \

" proof - obtain r where r: "recfn 1 r" "\x. eval r [x] = f x" using assms by auto let ?s = "Cn 1 r [Cn 1 r_add [Id 1 0, r_const n]]" have "recfn 1 ?s" using r by simp have "eval ?s [x] = eval r [x + n]" for x using r by simp with r have "eval ?s [x] = f (x + n)" for x by simp with `recfn 1 ?s` show ?thesis by blast qed lemma skip_R1: assumes "f \ \" shows "(\x. f (x + n)) \ \" using assms skip_P1 R1_imp_total1 total1_def by auto subsection \The Gödel numbering @{term \}\label{s:goedel_numbering}\ text \While the term \emph{Gödel numbering} is often used generically for mappings between natural numbers and mathematical concepts, the inductive inference literature uses it in a more specific sense. There it is equivalent to the notion of acceptable numbering~\cite{Rogers87}: For every numbering there is a recursive function mapping the numbering's indices to equivalent ones of a Gödel numbering.\ definition goedel_numbering :: "partial2 \ bool" where "goedel_numbering \ \ \ \ \

\<^sup>2 \ (\\\\

\<^sup>2. \c\\. \i. \ i = \ (the (c i)))" lemma goedel_numbering_P2: assumes "goedel_numbering \" shows "\ \ \

\<^sup>2" using goedel_numbering_def assms by simp lemma goedel_numberingE: assumes "goedel_numbering \" and "\ \ \

\<^sup>2" obtains c where "c \ \" and "\i. \ i = \ (the (c i))" using assms goedel_numbering_def by blast lemma goedel_numbering_universal: assumes "goedel_numbering \" and "f \ \

" shows "\i. \ i = f" proof - define \ :: partial2 where "\ = (\i. f)" have "\ \ \

\<^sup>2" proof - obtain rf where rf: "recfn 1 rf" "\x. eval rf [x] = f x" using assms(2) by auto define r where "r = Cn 2 rf [Id 2 1]" then have r: "recfn 2 r" "\i x. eval r [i, x] = eval rf [x]" using rf(1) by simp_all with rf(2) have "\i x. eval r [i, x] = f x" by simp with r(1) show ?thesis using \_def by auto qed then obtain c where "c \ \" and "\i. \ i = \ (the (c i))" using goedel_numbering_def assms(1) by auto with \_def show ?thesis by auto qed text \Our standard Gödel numbering is based on @{term r_phi}:\ definition phi :: partial2 ("\") where "\ i x \ eval r_phi [i, x]" lemma phi_in_P2: "\ \ \

\<^sup>2" unfolding phi_def using r_phi_recfn by blast text \Indices of any numbering can be translated into equivalent indices of @{term phi}, which thus is a Gödel numbering.\ lemma numbering_translation_for_phi: assumes "\ \ \

\<^sup>2" shows "\c\\. \i. \ i = \ (the (c i))" proof - obtain psi where psi: "recfn 2 psi" "\i x. eval psi [i, x] = \ i x" using assms by auto with numbering_translation obtain b where "recfn 1 b" "total b" "\i x. eval psi [i, x] = eval r_phi [the (eval b [i]), x]" by blast moreover from this obtain c where c: "c \ \" "\i. c i = eval b [i]" by fast ultimately have "\ i x = \ (the (c i)) x" for i x using phi_def psi(2) by presburger then have "\ i = \ (the (c i))" for i by auto then show ?thesis using c(1) by blast qed corollary goedel_numbering_phi: "goedel_numbering \" unfolding goedel_numbering_def using numbering_translation_for_phi phi_in_P2 by simp corollary phi_universal: assumes "f \ \

" obtains i where "\ i = f" using goedel_numbering_universal[OF goedel_numbering_phi assms] by auto subsection \Fixed-point theorems\ text \The fixed-point theorems look somewhat cleaner in the new notation. We will only need the following ones in the next chapter.\ theorem kleene_fixed_point: fixes k :: nat assumes "\ \ \

\<^sup>2" obtains i where "i \ k" and "\ i = \ i" proof - obtain r_psi where r_psi: "recfn 2 r_psi" "\i x. eval r_psi [i, x] = \ i x" using assms by auto then obtain i where i: "i \ k" "\x. eval r_phi [i, x] = eval r_psi [i, x]" using kleene_fixed_point_theorem by blast then have "\x. \ i x = \ i x" using phi_def r_psi by simp then show ?thesis using i that by blast qed theorem smullyan_double_fixed_point: assumes "g \ \\<^sup>2" and "h \ \\<^sup>2" obtains m n where "\ m = \ (the (g m n))" and "\ n = \ (the (h m n))" proof - obtain rg where rg: "recfn 2 rg" "total rg" "g = (\x y. eval rg [x, y])" using R2E[OF assms(1)] by auto moreover obtain rh where rh: "recfn 2 rh" "total rh" "h = (\x y. eval rh [x, y])" using R2E[OF assms(2)] by auto ultimately obtain m n where "\x. eval r_phi [m, x] = eval r_phi [the (eval rg [m, n]), x]" "\x. eval r_phi [n, x] = eval r_phi [the (eval rh [m, n]), x]" using smullyan_double_fixed_point_theorem[of rg rh] by blast then have "\ m = \ (the (g m n))" and "\ n = \ (the (h m n))" using phi_def rg rh by auto then show ?thesis using that by simp qed end \ No newline at end of file diff --git a/thys/Inductive_Inference/Universal.thy b/thys/Inductive_Inference/Universal.thy --- a/thys/Inductive_Inference/Universal.thy +++ b/thys/Inductive_Inference/Universal.thy @@ -1,2537 +1,2538 @@ section \A universal partial recursive function\ theory Universal imports Partial_Recursive begin text \The main product of this section is a universal partial recursive function, which given a code $i$ of an $n$-ary partial recursive function $f$ and an encoded list @{term xs} of $n$ arguments, computes @{term "eval f xs"}. From this we can derive fixed-arity universal functions satisfying the usual results such as the $s$-$m$-$n$ theorem. To represent the code $i$, we need a way to encode @{typ recf}s as natural numbers (Section~\ref{s:recf_enc}). To construct the universal function, we devise a ternary function taking $i$, $xs$, and a step bound $t$ and simulating the execution of $f$ on input $xs$ for $t$ steps. This function is useful in its own right, enabling techniques like dovetailing or ``concurrent'' evaluation of partial recursive functions. The notion of a ``step'' is not part of the definition of (the evaluation of) partial recursive functions, but one can simulate the evaluation on an abstract machine (Section~\ref{s:step}). This machine's configurations can be encoded as natural numbers, and this leads us to a step function @{typ "nat \ nat"} on encoded configurations (Section~\ref{s:step_enc}). This function in turn can be computed by a primitive recursive function, from which we develop the aforementioned ternary function of $i$, @{term xs}, and $t$ (Section~\ref{s:step_recf}). From this we can finally derive a universal function (Section~\ref{s:the_universal}).\ subsection \A step function\label{s:step}\ text \We simulate the stepwise execution of a partial recursive function in a fairly straightforward way reminiscent of the execution of function calls in an imperative programming language. A configuration of the abstract machine is a pair consisting of: \begin{enumerate} \item A stack of frames. A frame represents the execution of a function and is a triple @{term "(f, xs, locals)"} of \begin{enumerate} \item a @{typ recf} @{term f} being executed, \item a @{typ "nat list"} of arguments of @{term f}, \item a @{typ "nat list"} of local variables, which holds intermediate values when @{term f} is of the form @{term Cn}, @{term Pr}, or @{term Mn}. \end{enumerate} \item A register of type @{typ "nat option"} representing the return value of the last function call: @{term None} signals that in the previous step the stack was not popped and hence no value was returned, whereas @{term "Some v"} means that in the previous step a function returned @{term v}. \end{enumerate} For computing @{term h} on input @{term xs}, the initial configuration is @{term "([(h, xs, [])], None)"}. When the computation for a frame ends, it is popped off the stack, and its return value is put in the register. The entire computation ends when the stack is empty. In such a final configuration the register contains the value of @{term h} at @{term xs}. If no final configuration is ever reached, @{term h} diverges at @{term xs}. The execution of one step depends on the topmost (that is, active) frame. In the step when a frame @{term "(h, xs, locals)"} is pushed onto the stack, the local variables are @{term "locals = []"}. The following happens until the frame is popped off the stack again (if it ever is): \begin{itemize} \item For the base functions @{term "h = Z"}, @{term "h = S"}, @{term[names_short] "h = Id m n"}, the frame is popped off the stack right away, and the return value is placed in the register. \item For @{term "h = Cn n f gs"}, for each function $g$ in @{term gs}: \begin{enumerate} \item A new frame of the form @{term "(g, xs, [])"} is pushed onto the stack. \item When (and if) this frame is eventually popped, the value in the register is @{term "eval g xs"}. This value is appended to the list @{term locals} of local variables. \end{enumerate} When all $g$ in $gs$ have been evaluated in this manner, $f$ is evaluated on the local variables by pushing @{term "(f, locals, [])"}. The resulting register value is kept and the active frame for $h$ is popped off the stack. \item For @{text "h = Pr n f g"}, let @{term "xs = y # ys"}. First @{term "(f, ys, [])"} is pushed and the return value stored in the @{term locals}. Then @{term "(g, x # v # ys, [])"} is pushed, where $x$ is the length of @{term locals} and $v$ the most recently appended value. The return value is appended to @{term locals}. This is repeated until the length of @{term locals} reaches @{term y}. Then the most recently appended local is placed in the register, and the stack is popped. \item For @{text "h = Mn n f"}, frames @{term "(f, x # xs, [])"} are pushed for $x = 0, 1, 2, \ldots$ until one of them returns $0$. Then this $x$ is placed in the register and the stack is popped. Until then $x$ is stored in @{term locals}. If none of these evaluations return $0$, the stack never shrinks, and thus the machine never reaches a final state. \end{itemize}\ type_synonym frame = "recf \ nat list \ nat list" type_synonym configuration = "frame list \ nat option" subsubsection \Definition of the step function\ fun step :: "configuration \ configuration" where "step ([], rv) = ([], rv)" | "step (((Z, _, _) # fs), rv) = (fs, Some 0)" | "step (((S, xs, _) # fs), rv) = (fs, Some (Suc (hd xs)))" | "step (((Id m n, xs, _) # fs), rv) = (fs, Some (xs ! n))" | "step (((Cn n f gs, xs, ls) # fs), rv) = (if length ls = length gs then if rv = None then ((f, ls, []) # (Cn n f gs, xs, ls) # fs, None) else (fs, rv) else if rv = None then if length ls < length gs then ((gs ! (length ls), xs, []) # (Cn n f gs, xs, ls) # fs, None) else (fs, rv) \\cannot occur, so don't-care term\ else ((Cn n f gs, xs, ls @ [the rv]) # fs, None))" | "step (((Pr n f g, xs, ls) # fs), rv) = (if ls = [] then if rv = None then ((f, tl xs, []) # (Pr n f g, xs, ls) # fs, None) else ((Pr n f g, xs, [the rv]) # fs, None) else if length ls = Suc (hd xs) then (fs, Some (hd ls)) else if rv = None then ((g, (length ls - 1) # hd ls # tl xs, []) # (Pr n f g, xs, ls) # fs, None) else ((Pr n f g, xs, (the rv) # ls) # fs, None))" | "step (((Mn n f, xs, ls) # fs), rv) = (if ls = [] then ((f, 0 # xs, []) # (Mn n f, xs, [0]) # fs, None) else if rv = Some 0 then (fs, Some (hd ls)) else ((f, (Suc (hd ls)) # xs, []) # (Mn n f, xs, [Suc (hd ls)]) # fs, None))" definition reachable :: "configuration \ configuration \ bool" where "reachable x y \ \t. iterate t step x = y" lemma step_reachable [intro]: assumes "step x = y" shows "reachable x y" unfolding reachable_def using assms by (metis iterate.simps(1,2) comp_id) lemma reachable_transitive [trans]: assumes "reachable x y" and "reachable y z" shows "reachable x z" using assms iterate_additive[where ?f=step] reachable_def by metis lemma reachable_refl: "reachable x x" unfolding reachable_def by (metis iterate.simps(1) eq_id_iff) text \From a final configuration, that is, when the stack is empty, only final configurations are reachable.\ lemma step_empty_stack: assumes "fst x = []" shows "fst (step x) = []" using assms by (metis prod.collapse step.simps(1)) lemma reachable_empty_stack: assumes "fst x = []" and "reachable x y" shows "fst y = []" proof - have "fst (iterate t step x) = []" for t using assms step_empty_stack by (induction t) simp_all then show ?thesis using reachable_def assms(2) by auto qed abbreviation nonterminating :: "configuration \ bool" where "nonterminating x \ \t. fst (iterate t step x) \ []" lemma reachable_nonterminating: assumes "reachable x y" and "nonterminating y" shows "nonterminating x" proof - from assms(1) obtain t\<^sub>1 where t1: "iterate t\<^sub>1 step x = y" using reachable_def by auto have "fst (iterate t step x) \ []" for t proof (cases "t \ t\<^sub>1") case True then show ?thesis using t1 assms(2) reachable_def reachable_empty_stack iterate_additive' by (metis le_Suc_ex) next case False then have "iterate t step x = iterate (t\<^sub>1 + (t - t\<^sub>1)) step x" by simp then have "iterate t step x = iterate (t - t\<^sub>1) step (iterate t\<^sub>1 step x)" by (simp add: iterate_additive') then have "iterate t step x = iterate (t - t\<^sub>1) step y" using t1 by simp then show "fst (iterate t step x) \ []" using assms(2) by simp qed then show ?thesis .. qed text \The function @{term step} is underdefined, for example, when the top frame contains a non-well-formed @{typ recf} or too few arguments. All is well, though, if every frame contains a well-formed @{typ recf} whose arity matches the number of arguments. Such stacks will be called \emph{valid}.\ definition valid :: "frame list \ bool" where "valid stack \ \s\set stack. recfn (length (fst (snd s))) (fst s)" lemma valid_frame: "valid (s # ss) \ valid ss \ recfn (length (fst (snd s))) (fst s)" using valid_def by simp lemma valid_ConsE: "valid ((f, xs, locs) # rest) \ valid rest \ recfn (length xs) f" using valid_def by simp lemma valid_ConsI: "valid rest \ recfn (length xs) f \ valid ((f, xs, locs) # rest)" using valid_def by simp text \Stacks in initial configurations are valid, and performing a step maintains the validity of the stack.\ lemma step_valid: "valid stack \ valid (fst (step (stack, rv)))" proof (cases stack) case Nil then show ?thesis using valid_def by simp next case (Cons s ss) assume valid: "valid stack" then have *: "valid ss \ recfn (length (fst (snd s))) (fst s)" using valid_frame Cons by simp show ?thesis proof (cases "fst s") case Z then show ?thesis using Cons valid * by (metis fstI prod.collapse step.simps(2)) next case S then show ?thesis using Cons valid * by (metis fst_conv prod.collapse step.simps(3)) next case Id then show ?thesis using Cons valid * by (metis fstI prod.collapse step.simps(4)) next case (Cn n f gs) then obtain xs ls where "s = (Cn n f gs, xs, ls)" using Cons by (metis prod.collapse) moreover consider "length ls = length gs \ rv \" | "length ls = length gs \ rv \" | "length ls < length gs \ rv \" | "length ls \ length gs \ rv \" | "length ls > length gs \ rv \" by linarith ultimately show ?thesis using valid Cons valid_def by (cases) auto next case (Pr n f g) then obtain xs ls where s: "s = (Pr n f g, xs, ls)" using Cons by (metis prod.collapse) consider "length ls = 0 \ rv \" | "length ls = 0 \ rv \" | "length ls \ 0 \ length ls = Suc (hd xs)" | "length ls \ 0 \ length ls \ Suc (hd xs) \ rv \" | "length ls \ 0 \ length ls \ Suc (hd xs) \ rv \" by linarith then show ?thesis using Cons * valid_def s by (cases) auto next case (Mn n f) then obtain xs ls where s: "s = (Mn n f, xs, ls)" using Cons by (metis prod.collapse) consider "length ls = 0" | "length ls \ 0 \ rv \" | "length ls \ 0 \ rv \" by linarith then show ?thesis using Cons * valid_def s by (cases) auto qed qed corollary iterate_step_valid: assumes "valid stack" shows "valid (fst (iterate t step (stack, rv)))" using assms proof (induction t) case 0 then show ?case by simp next case (Suc t) moreover have "iterate (Suc t) step (stack, rv) = step (iterate t step (stack, rv))" by simp ultimately show ?case using step_valid valid_def by (metis prod.collapse) qed subsubsection \Correctness of the step function\ text \The function @{term step} works correctly for a @{typ recf} $f$ on arguments @{term xs} in some configuration if (1) in case $f$ converges, @{term step} reaches a configuration with the topmost frame popped and @{term "eval f xs"} in the register, and (2) in case $f$ diverges, @{term step} does not reach a final configuration.\ fun correct :: "configuration \ bool" where "correct ([], r) = True" | "correct ((f, xs, ls) # rest, r) = (if eval f xs \ then reachable ((f, xs, ls) # rest, r) (rest, eval f xs) else nonterminating ((f, xs, ls) # rest, None))" lemma correct_convergI: assumes "eval f xs \" and "reachable ((f, xs, ls) # rest, None) (rest, eval f xs)" shows "correct ((f, xs, ls) # rest, None)" using assms by auto lemma correct_convergE: assumes "correct ((f, xs, ls) # rest, None)" and "eval f xs \" shows "reachable ((f, xs, ls) # rest, None) (rest, eval f xs)" using assms by simp text \The correctness proof for @{term step} is by structural induction on the @{typ recf} in the top frame. The base cases @{term Z}, @{term S}, and @{term[names_short] Id} are simple. For @{text "X = Cn, Pr, Mn"}, the lemmas named @{text reachable_X} show which configurations are reachable for @{typ recf}s of shape @{text X}. Building on those, the lemmas named @{text step_X_correct} show @{term step}'s correctness for @{text X}.\ lemma reachable_Cn: assumes "valid (((Cn n f gs), xs, []) # rest)" (is "valid ?stack") and "\xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" and "\g xs rest. g \ set gs \ valid ((g, xs, []) # rest) \ correct ((g, xs, []) # rest, None)" and "\i" and "k \ length gs" shows "reachable (?stack, None) ((Cn n f gs, xs, take k (map (\g. the (eval g xs)) gs)) # rest, None)" using assms(4,5) proof (induction k) case 0 then show ?case using reachable_refl by simp next case (Suc k) let ?ys = "map (\g. the (eval g xs)) gs" from Suc have "k < length gs" by simp have valid: "recfn (length xs) (Cn n f gs)" "valid rest" using assms(1) valid_ConsE[of "(Cn n f gs)"] by simp_all from Suc have "reachable (?stack, None) ((Cn n f gs, xs, take k ?ys) # rest, None)" (is "_ (?stack1, None)") by simp also have "reachable ... ((gs ! k, xs, []) # ?stack1, None)" - using step_reachable `k < length gs` by (simp add: min_absorb2) + using step_reachable `k < length gs` + by (auto simp: min_absorb2) also have "reachable ... (?stack1, eval (gs ! k) xs)" (is "_ (_, ?rv)") using Suc.prems(1) \k < length gs\ assms(3) valid valid_ConsI by auto also have "reachable ... ((Cn n f gs, xs, (take (Suc k) ?ys)) # rest, None)" (is "_ (?stack2, None)") proof - have "step (?stack1, ?rv) = ((Cn n f gs, xs, (take k ?ys) @ [the ?rv]) # rest, None)" using Suc by auto also have "... = ((Cn n f gs, xs, (take (Suc k) ?ys)) # rest, None)" by (simp add: \k < length gs\ take_Suc_conv_app_nth) finally show ?thesis - using step_reachable by simp + using step_reachable by auto qed finally show "reachable (?stack, None) (?stack2, None)" . qed lemma step_Cn_correct: assumes "valid (((Cn n f gs), xs, []) # rest)" (is "valid ?stack") and "\xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" and "\g xs rest. g \ set gs \ valid ((g, xs, []) # rest) \ correct ((g, xs, []) # rest, None)" shows "correct (?stack, None)" proof - have valid: "recfn (length xs) (Cn n f gs)" "valid rest" using valid_ConsE[OF assms(1)] by auto let ?ys = "map (\g. the (eval g xs)) gs" consider (diverg_f) "\g\set gs. eval g xs \" and "eval f ?ys \" | (diverg_gs) "\g\set gs. eval g xs \" | (converg) "eval (Cn n f gs) xs \" using valid_ConsE[OF assms(1)] by fastforce then show ?thesis proof (cases) case diverg_f then have "\i" by simp then have "reachable (?stack, None) ((Cn n f gs, xs, ?ys) # rest, None)" (is "_ (?stack1, None)") using reachable_Cn[OF assms, where ?k="length gs"] by simp also have "reachable ... ((f, ?ys, []) # ?stack1, None)" (is "_ (?stack2, None)") by (simp add: step_reachable) finally have "reachable (?stack, None) (?stack2, None)" . moreover have "nonterminating (?stack2, None)" using diverg_f(2) assms(2)[of ?ys ?stack1] valid_ConsE[OF assms(1)] valid_ConsI by auto ultimately have "nonterminating (?stack, None)" using reachable_nonterminating by simp moreover have "eval (Cn n f gs) xs \" using diverg_f(2) assms(1) eval_Cn valid_ConsE by presburger ultimately show ?thesis by simp next case diverg_gs then have ex_i: "\i" using in_set_conv_nth[of _ gs] by auto define k where "k = (LEAST i. i < length gs \ eval (gs ! i) xs \)" (is "_ = Least ?P") then have gs_k: "eval (gs ! k) xs \" using LeastI_ex[OF ex_i] by simp have "\i" using k_def not_less_Least[of _ ?P] LeastI_ex[OF ex_i] by simp moreover from this have "k < length gs" using ex_i less_le_trans not_le by blast ultimately have "reachable (?stack, None) ((Cn n f gs, xs, take k ?ys) # rest, None)" using reachable_Cn[OF assms] by simp also have "reachable ... ((gs ! (length (take k ?ys)), xs, []) # (Cn n f gs, xs, take k ?ys) # rest, None)" (is "_ (?stack1, None)") proof - have "length (take k ?ys) < length gs" by (simp add: \k < length gs\ less_imp_le_nat min_less_iff_disj) - then show ?thesis using step_reachable by simp + then show ?thesis using step_reachable by auto qed finally have "reachable (?stack, None) (?stack1, None)" . moreover have "nonterminating (?stack1, None)" proof - have "recfn (length xs) (gs ! k)" using \k < length gs\ valid(1) by simp then have "correct (?stack1, None)" using \k < length gs\ nth_mem valid valid_ConsI assms(3)[of "gs ! (length (take k ?ys))" xs] by auto moreover have "length (take k ?ys) = k" by (simp add: \k < length gs\ less_imp_le_nat min_absorb2) ultimately show ?thesis using gs_k by simp qed ultimately have "nonterminating (?stack, None)" using reachable_nonterminating by simp moreover have "eval (Cn n f gs) xs \" using diverg_gs valid by fastforce ultimately show ?thesis by simp next case converg then have f: "eval f ?ys \" and g: "\g. g \ set gs \ eval g xs \" using valid(1) by (metis eval_Cn)+ then have "\i" by simp then have "reachable (?stack, None) ((Cn n f gs, xs, take (length gs) ?ys) # rest, None)" using reachable_Cn assms by blast also have "reachable ... ((Cn n f gs, xs, ?ys) # rest, None)" (is "_ (?stack1, None)") by (simp add: reachable_refl) also have "reachable ... ((f, ?ys, []) # ?stack1, None)" - using step_reachable by simp + using step_reachable by auto also have "reachable ... (?stack1, eval f ?ys)" using assms(2)[of "?ys"] correct_convergE valid f valid_ConsI by auto also have "reachable (?stack1, eval f ?ys) (rest, eval f ?ys)" using f by auto finally have "reachable (?stack, None) (rest, eval f ?ys)" . moreover have "eval (Cn n f gs) xs = eval f ?ys" using g valid(1) by auto ultimately show ?thesis using converg correct_convergI by auto qed qed text \During the execution of a frame with a partial recursive function of shape @{term "Pr n f g"} and arguments @{term "x # xs"}, the list of local variables collects all the function values up to @{term x} in reversed order. We call such a list a @{term trace} for short.\ definition trace :: "nat \ recf \ recf \ nat list \ nat \ nat list" where "trace n f g xs x \ map (\y. the (eval (Pr n f g) (y # xs))) (rev [0..xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" and "\xs rest. valid ((g, xs, []) # rest) \ correct ((g, xs, []) # rest, None)" and "y \ x" and "eval (Pr n f g) (y # xs) \" shows "reachable (?stack, None) ((Pr n f g, x # xs, trace n f g xs y) # rest, None)" using assms(4,5) proof (induction y) case 0 have valid: "recfn (length (x # xs)) (Pr n f g)" "valid rest" using valid_ConsE[OF assms(1)] by simp_all then have f: "eval f xs \" using 0 by simp let ?as = "x # xs" have "reachable (?stack, None) ((f, xs, []) # ((Pr n f g), ?as, []) # rest, None)" - using step_reachable by simp + using step_reachable by auto also have "reachable ... (?stack, eval f xs)" using assms(2)[of xs "((Pr n f g), ?as, []) # rest"] correct_convergE[OF _ f] f valid valid_ConsI by simp also have "reachable ... ((Pr n f g, ?as, [the (eval f xs)]) # rest, None)" - using step_reachable valid(1) f by simp + using step_reachable valid(1) f by auto finally have "reachable (?stack, None) ((Pr n f g, ?as, [the (eval f xs)]) # rest, None)" . then show ?case using trace_def valid(1) by simp next case (Suc y) have valid: "recfn (length (x # xs)) (Pr n f g)" "valid rest" using valid_ConsE[OF assms(1)] by simp_all let ?ls = "trace n f g xs y" have lenls: "length ?ls = Suc y" using trace_length by auto moreover have hdls: "hd ?ls = the (eval (Pr n f g) (y # xs))" using Suc trace_hd by auto ultimately have g: "eval g (y # hd ?ls # xs) \" "eval (Pr n f g) (Suc y # xs) = eval g (y # hd ?ls # xs)" using eval_Pr_Suc_converg hdls valid(1) Suc by simp_all then have "reachable (?stack, None) ((Pr n f g, x # xs, ?ls) # rest, None)" (is "_ (?stack1, None)") using Suc valid(1) by fastforce also have "reachable ... ((g, y # hd ?ls # xs, []) # (Pr n f g, x # xs, ?ls) # rest, None)" using Suc.prems lenls by fastforce also have "reachable ... (?stack1, eval g (y # hd ?ls # xs))" (is "_ (_, ?rv)") using assms(3) g(1) valid valid_ConsI by auto also have "reachable ... ((Pr n f g, x # xs, (the ?rv) # ?ls) # rest, None)" using Suc.prems(1) g(1) lenls by auto finally have "reachable (?stack, None) ((Pr n f g, x # xs, (the ?rv) # ?ls) # rest, None)" . moreover have "trace n f g xs (Suc y) = (the ?rv) # ?ls" using g(2) trace_Suc by simp ultimately show ?case by simp qed lemma step_Pr_correct: assumes "valid (((Pr n f g), xs, []) # rest)" (is "valid ?stack") and "\xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" and "\xs rest. valid ((g, xs, []) # rest) \ correct ((g, xs, []) # rest, None)" shows "correct (?stack, None)" proof - have valid: "valid rest" "recfn (length xs) (Pr n f g)" using valid_ConsE[OF assms(1)] by simp_all then have "length xs > 0" by auto then obtain y ys where y_ys: "xs = y # ys" using list.exhaust_sel by auto let ?t = "trace n f g ys" consider (converg) "eval (Pr n f g) xs \" | (diverg_f) "eval (Pr n f g) xs \" and "eval f ys \" | (diverg) "eval (Pr n f g) xs \" and "eval f ys \" by auto then show ?thesis proof (cases) case converg then have "\z. z \ y \ reachable (?stack, None) (((Pr n f g), xs, ?t z) # rest, None)" using assms valid by (simp add: eval_Pr_converg_le reachable_Pr y_ys) then have "reachable (?stack, None) (((Pr n f g), xs, ?t y) # rest, None)" by simp moreover have "reachable (((Pr n f g), xs, ?t y) # rest, None) (rest, Some (hd (?t y)))" using trace_length step_reachable y_ys by fastforce ultimately have "reachable (?stack, None) (rest, Some (hd (?t y)))" using reachable_transitive by blast then show ?thesis using assms(1) trace_hd converg y_ys by simp next case diverg_f have *: "step (?stack, None) = ((f, ys, []) # ((Pr n f g), xs, []) # tl ?stack, None)" (is "_ = (?stack1, None)") using assms(1,2) y_ys by simp then have "reachable (?stack, None) (?stack1, None)" - using step_reachable by simp + using step_reachable by force moreover have "nonterminating (?stack1, None)" using assms diverg_f valid valid_ConsI * by auto ultimately have "nonterminating (?stack, None)" using reachable_nonterminating by blast then show ?thesis using diverg_f(1) assms(1) by simp next case diverg let ?h = "\z. the (eval (Pr n f g) (z # ys))" let ?Q = "\z. z < y \ eval (Pr n f g) (z # ys) \" have "?Q 0" using assms diverg neq0_conv y_ys valid by fastforce define zmax where "zmax = Greatest ?Q" then have "?Q zmax" using `?Q 0` GreatestI_nat[of ?Q 0 y] by simp have le_zmax: "\z. ?Q z \ z \ zmax" using Greatest_le_nat[of ?Q _ y] zmax_def by simp have len: "length (?t zmax) < Suc y" by (simp add: \?Q zmax\ trace_length) have "eval (Pr n f g) (y # ys) \" if "y \ zmax" for y using that zmax_def `?Q zmax` assms eval_Pr_converg_le[of n f g ys zmax y] valid y_ys by simp then have "reachable (?stack, None) (((Pr n f g), xs, ?t y) # rest, None)" if "y \ zmax" for y using that `?Q zmax` diverg y_ys assms reachable_Pr by simp then have "reachable (?stack, None) (((Pr n f g), xs, ?t zmax) # rest, None)" (is "reachable _ (?stack1, None)") by simp also have "reachable ... ((g, zmax # ?h zmax # tl xs, []) # (Pr n f g, xs, ?t zmax) # rest, None)" (is "_ (?stack2, None)") proof (rule step_reachable) have "length (?t zmax) \ Suc (hd xs)" using len y_ys by simp moreover have "hd (?t zmax) = ?h zmax" using trace_hd by auto moreover have "length (?t zmax) = Suc zmax" using trace_length by simp ultimately show "step (?stack1, None) = (?stack2, None)" by auto qed finally have "reachable (?stack, None) (?stack2, None)" . moreover have "nonterminating (?stack2, None)" proof - have "correct (?stack2, None)" using y_ys assms valid_ConsI valid by simp moreover have "eval g (zmax # ?h zmax # ys) \" using \?Q zmax\ diverg le_zmax len less_Suc_eq trace_length y_ys valid by fastforce ultimately show ?thesis using y_ys by simp qed ultimately have "nonterminating (?stack, None)" using reachable_nonterminating by simp then show ?thesis using diverg assms(1) by simp qed qed lemma reachable_Mn: assumes "valid ((Mn n f, xs, []) # rest)" (is "valid ?stack") and "\xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" and "\y {None, Some 0}" shows "reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" using assms(3) proof (induction z) case 0 then have "step (?stack, None) = ((f, 0 # xs, []) # (Mn n f, xs, [0]) # rest, None)" using assms by simp then show ?case - using step_reachable assms(1) by simp + using step_reachable assms(1) by force next case (Suc z) have valid: "valid rest" "recfn (length xs) (Mn n f)" using valid_ConsE[OF assms(1)] by auto have f: "eval f (z # xs) \ {None, Some 0}" using Suc by simp have "reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" using Suc by simp also have "reachable ... ((Mn n f, xs, [z]) # rest, eval f (z # xs))" using f assms(2)[of "z # xs"] valid correct_convergE valid_ConsI by auto also have "reachable ... ((f, (Suc z) # xs, []) # (Mn n f, xs, [Suc z]) # rest, None)" (is "_ (?stack1, None)") - using step_reachable f by simp + using step_reachable f by force finally have "reachable (?stack, None) (?stack1, None)" . then show ?case by simp qed lemma iterate_step_empty_stack: "iterate t step ([], rv) = ([], rv)" using step_empty_stack by (induction t) simp_all lemma reachable_iterate_step_empty_stack: assumes "reachable cfg ([], rv)" shows "\t. iterate t step cfg = ([], rv) \ (\t' [])" proof - let ?P = "\t. iterate t step cfg = ([], rv)" from assms have "\t. ?P t" by (simp add: reachable_def) moreover define tmin where "tmin = Least ?P" ultimately have "?P tmin" using LeastI_ex[of ?P] by simp have "fst (iterate t' step cfg) \ []" if "t' < tmin" for t' proof assume "fst (iterate t' step cfg) = []" then obtain v where v: "iterate t' step cfg = ([], v)" by (metis prod.exhaust_sel) then have "iterate t'' step ([], v) = ([], v)" for t'' using iterate_step_empty_stack by simp then have "iterate (t' + t'') step cfg = ([], v)" for t'' using v iterate_additive by fast moreover obtain t'' where "t' + t'' = tmin" using \t' < tmin\ less_imp_add_positive by auto ultimately have "iterate tmin step cfg = ([], v)" by auto then have "v = rv" using `?P tmin` by simp then have "iterate t' step cfg = ([], rv)" using v by simp moreover have "\t' ?P t'" unfolding tmin_def using not_less_Least[of _ ?P] by simp ultimately show False using that by simp qed then show ?thesis using `?P tmin` by auto qed lemma step_Mn_correct: assumes "valid ((Mn n f, xs, []) # rest)" (is "valid ?stack") and "\xs rest. valid ((f, xs, []) # rest) \ correct ((f, xs, []) # rest, None)" shows "correct (?stack, None)" proof - have valid: "valid rest" "recfn (length xs) (Mn n f)" using valid_ConsE[OF assms(1)] by auto consider (diverg) "eval (Mn n f) xs \" and "\z. eval f (z # xs) \" | (diverg_f) "eval (Mn n f) xs \" and "\z. eval f (z # xs) \" | (converg) "eval (Mn n f) xs \" by fast then show ?thesis proof (cases) case diverg then have "\z. eval f (z # xs) \ Some 0" using eval_Mn_diverg[OF valid(2)] by simp then have "\y {None, Some 0}" for z using diverg by simp then have reach_z: "\z. reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" using reachable_Mn[OF assms] diverg by simp define h :: "nat \ configuration" where "h z \ ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" for z then have h_inj: "\x y. x \ y \ h x \ h y" and z_neq_Nil: "\z. fst (h z) \ []" by simp_all have z: "\z\<^sub>0. \z>z\<^sub>0. \ (\t'\t. iterate t' step (?stack, None) = h z)" for t proof (induction t) case 0 then show ?case by (metis h_inj le_zero_eq less_not_refl3) next case (Suc t) then show ?case using h_inj by (metis (no_types, hide_lams) le_Suc_eq less_not_refl3 less_trans) qed have "nonterminating (?stack, None)" proof (rule ccontr) assume "\ nonterminating (?stack, None)" then obtain t where t: "fst (iterate t step (?stack, None)) = []" by auto then obtain z\<^sub>0 where "\z>z\<^sub>0. \ (\t'\t. iterate t' step (?stack, None) = h z)" using z by auto then have not_h: "\t'\t. iterate t' step (?stack, None) \ h (Suc z\<^sub>0)" by simp have "\t'\t. fst (iterate t' step (?stack, None)) = []" using t iterate_step_empty_stack iterate_additive'[of t] by (metis le_Suc_ex prod.exhaust_sel) then have "\t'\t. iterate t' step (?stack, None) \ h (Suc z\<^sub>0)" using z_neq_Nil by auto then have "\t'. iterate t' step (?stack, None) \ h (Suc z\<^sub>0)" using not_h nat_le_linear by auto then have "\ reachable (?stack, None) (h (Suc z\<^sub>0))" using reachable_def by simp then show False using reach_z[of "Suc z\<^sub>0"] h_def by simp qed then show ?thesis using diverg by simp next case diverg_f let ?P = "\z. eval f (z # xs) \" define zmin where "zmin \ Least ?P" then have "\y {None, Some 0}" using diverg_f eval_Mn_diverg[OF valid(2)] less_trans not_less_Least[of _ ?P] by blast moreover have f_zmin: "eval f (zmin # xs) \" using diverg_f LeastI_ex[of ?P] zmin_def by simp ultimately have "reachable (?stack, None) ((f, zmin # xs, []) # (Mn n f, xs, [zmin]) # rest, None)" (is "reachable _ (?stack1, None)") using reachable_Mn[OF assms] by simp moreover have "nonterminating (?stack1, None)" using f_zmin assms valid diverg_f valid_ConsI by auto ultimately have "nonterminating (?stack, None)" using reachable_nonterminating by simp then show ?thesis using diverg_f by simp next case converg then obtain z where z: "eval (Mn n f) xs \= z" by auto have f_z: "eval f (z # xs) \= 0" and f_less_z: "\y. y < z \ eval f (y # xs) \\ 0" using eval_Mn_convergE(2,3)[OF valid(2) z] by simp_all then have "reachable (?stack, None) ((f, z # xs, []) # (Mn n f, xs, [z]) # rest, None)" using reachable_Mn[OF assms] by simp also have "reachable ... ((Mn n f, xs, [z]) # rest, eval f (z # xs))" using assms(2)[of "z # xs"] valid f_z valid_ConsI correct_convergE by auto also have "reachable ... (rest, Some z)" - using f_z f_less_z step_reachable by simp + using f_z f_less_z step_reachable by auto finally have "reachable (?stack, None) (rest, Some z)" . then show ?thesis using z by simp qed qed theorem step_correct: assumes "valid ((f, xs, []) # rest)" shows "correct ((f, xs, []) # rest, None)" using assms proof (induction f arbitrary: xs rest) case Z - then show ?case using valid_ConsE[of Z] step_reachable by simp + then show ?case using valid_ConsE[of Z] step_reachable by auto next case S - then show ?case using valid_ConsE[of S] step_reachable by simp + then show ?case using valid_ConsE[of S] step_reachable by auto next case (Id m n) then show ?case using valid_ConsE[of "Id m n"] by auto next case Cn then show ?case using step_Cn_correct by presburger next case Pr then show ?case using step_Pr_correct by simp next case Mn then show ?case using step_Mn_correct by presburger qed subsection \Encoding partial recursive functions\label{s:recf_enc}\ text \In this section we define an injective, but not surjective, mapping from @{typ recf}s to natural numbers.\ abbreviation triple_encode :: "nat \ nat \ nat \ nat" where "triple_encode x y z \ prod_encode (x, prod_encode (y, z))" abbreviation quad_encode :: "nat \ nat \ nat \ nat \ nat" where "quad_encode w x y z \ prod_encode (w, prod_encode (x, prod_encode (y, z)))" fun encode :: "recf \ nat" where "encode Z = 0" | "encode S = 1" | "encode (Id m n) = triple_encode 2 m n" | "encode (Cn n f gs) = quad_encode 3 n (encode f) (list_encode (map encode gs))" | "encode (Pr n f g) = quad_encode 4 n (encode f) (encode g)" | "encode (Mn n f) = triple_encode 5 n (encode f)" lemma prod_encode_gr1: "a > 1 \ prod_encode (a, x) > 1" using le_prod_encode_1 less_le_trans by blast lemma encode_not_Z_or_S: "encode f = prod_encode (a, b) \ a > 1 \ f \ Z \ f \ S" by (metis encode.simps(1) encode.simps(2) less_numeral_extra(4) not_one_less_zero prod_encode_gr1) lemma encode_injective: "encode f = encode g \ f = g" proof (induction g arbitrary: f) case Z have "\a x. a > 1 \ prod_encode (a, x) > 0" using prod_encode_gr1 by (meson less_one less_trans) then have "f \ Z \ encode f > 0" by (cases f) auto then have "encode f = 0 \ f = Z" by fastforce then show ?case using Z by simp next case S have "\a x. a > 1 \ prod_encode (a, x) \ Suc 0" using prod_encode_gr1 by (metis One_nat_def less_numeral_extra(4)) then have "encode f = 1 \ f = S" by (cases f) auto then show ?case using S by simp next case Id then obtain z where *: "encode f = prod_encode (2, z)" by simp show ?case using Id by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq) next case Cn then obtain z where *: "encode f = prod_encode (3, z)" by simp show ?case proof (cases f) case Z then show ?thesis using * encode_not_Z_or_S by simp next case S then show ?thesis using * encode_not_Z_or_S by simp next case Id then show ?thesis using * by (simp add: prod_encode_eq) next case Cn then show ?thesis using * Cn.IH Cn.prems list_decode_encode by (smt encode.simps(4) fst_conv list.inj_map_strong prod_encode_eq snd_conv) next case Pr then show ?thesis using * by (simp add: prod_encode_eq) next case Mn then show ?thesis using * by (simp add: prod_encode_eq) qed next case Pr then obtain z where *: "encode f = prod_encode (4, z)" by simp show ?case using Pr by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq) next case Mn then obtain z where *: "encode f = prod_encode (5, z)" by simp show ?case using Mn by (cases f) (simp_all add: * encode_not_Z_or_S prod_encode_eq) qed definition encode_kind :: "nat \ nat" where "encode_kind e \ if e = 0 then 0 else if e = 1 then 1 else pdec1 e" lemma encode_kind_0: "encode_kind (encode Z) = 0" unfolding encode_kind_def by simp lemma encode_kind_1: "encode_kind (encode S) = 1" unfolding encode_kind_def by simp lemma encode_kind_2: "encode_kind (encode (Id m n)) = 2" unfolding encode_kind_def by (metis encode.simps(1-3) encode_injective fst_conv prod_encode_inverse recf.simps(16) recf.simps(8)) lemma encode_kind_3: "encode_kind (encode (Cn n f gs)) = 3" unfolding encode_kind_def by (metis encode.simps(1,2,4) encode_injective fst_conv prod_encode_inverse recf.simps(10) recf.simps(18)) lemma encode_kind_4: "encode_kind (encode (Pr n f g)) = 4" unfolding encode_kind_def by (metis encode.simps(1,2,5) encode_injective fst_conv prod_encode_inverse recf.simps(12) recf.simps(20)) lemma encode_kind_5: "encode_kind (encode (Mn n f)) = 5" unfolding encode_kind_def by (metis encode.simps(1,2,6) encode_injective fst_conv prod_encode_inverse recf.simps(14) recf.simps(22)) lemmas encode_kind_n = encode_kind_0 encode_kind_1 encode_kind_2 encode_kind_3 encode_kind_4 encode_kind_5 lemma encode_kind_Cn: assumes "encode_kind (encode f) = 3" shows "\n f' gs. f = Cn n f' gs" using assms encode_kind_n by (cases f) auto lemma encode_kind_Pr: assumes "encode_kind (encode f) = 4" shows "\n f' g. f = Pr n f' g" using assms encode_kind_n by (cases f) auto lemma encode_kind_Mn: assumes "encode_kind (encode f) = 5" shows "\n g. f = Mn n g" using assms encode_kind_n by (cases f) auto lemma pdec2_encode_Id: "pdec2 (encode (Id m n)) = prod_encode (m, n)" by simp lemma pdec2_encode_Pr: "pdec2 (encode (Pr n f g)) = triple_encode n (encode f) (encode g)" by simp subsection \The step function on encoded configurations\label{s:step_enc}\ text \In this section we construct a function @{text "estep :: nat \ nat"} that is equivalent to the function @{text "step :: configuration \ configuration"} except that it applies to encoded configurations. We start by defining an encoding for configurations.\ definition encode_frame :: "frame \ nat" where "encode_frame s \ triple_encode (encode (fst s)) (list_encode (fst (snd s))) (list_encode (snd (snd s)))" lemma encode_frame: "encode_frame (f, xs, ls) = triple_encode (encode f) (list_encode xs) (list_encode ls)" unfolding encode_frame_def by simp abbreviation encode_option :: "nat option \ nat" where "encode_option x \ if x = None then 0 else Suc (the x)" definition encode_config :: "configuration \ nat" where "encode_config cfg \ prod_encode (list_encode (map encode_frame (fst cfg)), encode_option (snd cfg))" lemma encode_config: "encode_config (ss, rv) = prod_encode (list_encode (map encode_frame ss), encode_option rv)" unfolding encode_config_def by simp text \Various projections from encoded configurations:\ definition e2stack where "e2stack e \ pdec1 e" definition e2rv where "e2rv e \ pdec2 e" definition e2tail where "e2tail e \ e_tl (e2stack e)" definition e2frame where "e2frame e \ e_hd (e2stack e)" definition e2i where "e2i e \ pdec1 (e2frame e)" definition e2xs where "e2xs e \ pdec12 (e2frame e)" definition e2ls where "e2ls e \ pdec22 (e2frame e)" definition e2lenas where "e2lenas e \ e_length (e2xs e)" definition e2lenls where "e2lenls e \ e_length (e2ls e)" lemma e2rv_rv [simp]: "e2rv (encode_config (ss, rv)) = (if rv \ then 0 else Suc (the rv))" unfolding e2rv_def using encode_config by simp lemma e2stack_stack [simp]: "e2stack (encode_config (ss, rv)) = list_encode (map encode_frame ss)" unfolding e2stack_def using encode_config by simp lemma e2tail_tail [simp]: "e2tail (encode_config (s # ss, rv)) = list_encode (map encode_frame ss)" unfolding e2tail_def using encode_config by fastforce lemma e2frame_frame [simp]: "e2frame (encode_config (s # ss, rv)) = encode_frame s" unfolding e2frame_def using encode_config by fastforce lemma e2i_f [simp]: "e2i (encode_config ((f, xs, ls) # ss, rv)) = encode f" unfolding e2i_def using encode_config e2frame_frame encode_frame by force lemma e2xs_xs [simp]: "e2xs (encode_config ((f, xs, ls) # ss, rv)) = list_encode xs" using e2xs_def e2frame_frame encode_frame by force lemma e2ls_ls [simp]: "e2ls (encode_config ((f, xs, ls) # ss, rv)) = list_encode ls" using e2ls_def e2frame_frame encode_frame by force lemma e2lenas_lenas [simp]: "e2lenas (encode_config ((f, xs, ls) # ss, rv)) = length xs" using e2lenas_def e2frame_frame encode_frame by simp lemma e2lenls_lenls [simp]: "e2lenls (encode_config ((f, xs, ls) # ss, rv)) = length ls" using e2lenls_def e2frame_frame encode_frame by simp lemma e2stack_0_iff_Nil: assumes "e = encode_config (ss, rv)" shows "e2stack e = 0 \ ss = []" using assms by (metis list_encode.simps(1) e2stack_stack list_encode_0 map_is_Nil_conv) lemma e2ls_0_iff_Nil [simp]: "list_decode (e2ls e) = [] \ e2ls e = 0" by (metis list_decode.simps(1) list_encode_decode) text \We now define @{text eterm} piecemeal by considering the more complicated cases @{text Cn}, @{text Pr}, and @{text Mn} separately.\ definition "estep_Cn e \ if e2lenls e = e_length (pdec222 (e2i e)) then if e2rv e = 0 then prod_encode (e_cons (triple_encode (pdec122 (e2i e)) (e2ls e) 0) (e2stack e), 0) else prod_encode (e2tail e, e2rv e) else if e2rv e = 0 then if e2lenls e < e_length (pdec222 (e2i e)) then prod_encode (e_cons (triple_encode (e_nth (pdec222 (e2i e)) (e2lenls e)) (e2xs e) 0) (e2stack e), 0) else prod_encode (e2tail e, e2rv e) else prod_encode (e_cons (triple_encode (e2i e) (e2xs e) (e_snoc (e2ls e) (e2rv e - 1))) (e2tail e), 0)" lemma estep_Cn: assumes "c = (((Cn n f gs, xs, ls) # fs), rv)" shows "estep_Cn (encode_config c) = encode_config (step c)" using encode_frame by (simp add: assms estep_Cn_def, simp add: encode_config assms) definition "estep_Pr e \ if e2ls e = 0 then if e2rv e = 0 then prod_encode (e_cons (triple_encode (pdec122 (e2i e)) (e_tl (e2xs e)) 0) (e2stack e), 0) else prod_encode (e_cons (triple_encode (e2i e) (e2xs e) (singleton_encode (e2rv e - 1))) (e2tail e), 0) else if e2lenls e = Suc (e_hd (e2xs e)) then prod_encode (e2tail e, Suc (e_hd (e2ls e))) else if e2rv e = 0 then prod_encode (e_cons (triple_encode (pdec222 (e2i e)) (e_cons (e2lenls e - 1) (e_cons (e_hd (e2ls e)) (e_tl (e2xs e)))) 0) (e2stack e), 0) else prod_encode (e_cons (triple_encode (e2i e) (e2xs e) (e_cons (e2rv e - 1) (e2ls e))) (e2tail e), 0)" lemma estep_Pr1: assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "ls \ []" and "length ls \ Suc (hd xs)" and "rv \ None" and "recfn (length xs) (Pr n f g)" shows "estep_Pr (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" from assms(5) have "length xs > 0" by auto then have eq: "hd xs = e_hd (e2xs ?e)" using assms e_hd_def by auto have "step c = ((Pr n f g, xs, (the rv) # ls) # fs, None)" (is "step c = (?t # ?ss, None)") using assms by simp then have "encode_config (step c) = prod_encode (list_encode (map encode_frame (?t # ?ss)), 0)" using encode_config by simp also have "... = prod_encode (e_cons (encode_frame ?t) (list_encode (map encode_frame (?ss))), 0)" by simp also have "... = prod_encode (e_cons (encode_frame ?t) (e2tail ?e), 0)" using assms(1) by simp also have "... = prod_encode (e_cons (triple_encode (e2i ?e) (e2xs ?e) (e_cons (e2rv ?e - 1) (e2ls ?e))) (e2tail ?e), 0)" by (simp add: assms encode_frame) finally show ?thesis using assms eq estep_Pr_def by auto qed lemma estep_Pr2: assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "ls \ []" and "length ls \ Suc (hd xs)" and "rv = None" and "recfn (length xs) (Pr n f g)" shows "estep_Pr (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" from assms(5) have "length xs > 0" by auto then have eq: "hd xs = e_hd (e2xs ?e)" using assms e_hd_def by auto have "step c = ((g, (length ls - 1) # hd ls # tl xs, []) # (Pr n f g, xs, ls) # fs, None)" (is "step c = (?t # ?ss, None)") using assms by simp then have "encode_config (step c) = prod_encode (list_encode (map encode_frame (?t # ?ss)), 0)" using encode_config by simp also have "... = prod_encode (e_cons (encode_frame ?t) (list_encode (map encode_frame (?ss))), 0)" by simp also have "... = prod_encode (e_cons (encode_frame ?t) (e2stack ?e), 0)" using assms(1) by simp also have "... = prod_encode (e_cons (triple_encode (pdec222 (e2i ?e)) (e_cons (e2lenls ?e - 1) (e_cons (e_hd (e2ls ?e)) (e_tl (e2xs ?e)))) 0) (e2stack ?e), 0)" using assms(1,2) encode_frame[of g "(length ls - 1) # hd ls # tl xs" "[]"] pdec2_encode_Pr[of n f g] e2xs_xs e2i_f e2lenls_lenls e2ls_ls e_hd by (metis list_encode.simps(1) list.collapse list_decode_encode prod_encode_inverse snd_conv) finally show ?thesis using assms eq estep_Pr_def by auto qed lemma estep_Pr3: assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "ls \ []" and "length ls = Suc (hd xs)" and "recfn (length xs) (Pr n f g)" shows "estep_Pr (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" from assms(4) have "length xs > 0" by auto then have "hd xs = e_hd (e2xs ?e)" using assms e_hd_def by auto then have "(length ls = Suc (hd xs)) = (e2lenls ?e = Suc (e_hd (e2xs ?e)))" using assms by simp then have *: "estep_Pr ?e = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))" using assms estep_Pr_def by auto have "step c = (fs, Some (hd ls))" using assms(1,2,3) by simp then have "encode_config (step c) = prod_encode (list_encode (map encode_frame fs), encode_option (Some (hd ls)))" using encode_config by simp also have "... = prod_encode (list_encode (map encode_frame fs), encode_option (Some (e_hd (e2ls ?e))))" using assms(1,2) e_hd_def by auto also have "... = prod_encode (list_encode (map encode_frame fs), Suc (e_hd (e2ls ?e)))" by simp also have "... = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))" using assms(1) by simp finally have "encode_config (step c) = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))" . then show ?thesis using estep_Pr_def * by presburger qed lemma estep_Pr4: assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "ls = []" shows "estep_Pr (encode_config c) = encode_config (step c)" using encode_frame by (simp add: assms estep_Pr_def, simp add: encode_config assms) lemma estep_Pr: assumes "c = (((Pr n f g, xs, ls) # fs), rv)" and "recfn (length xs) (Pr n f g)" shows "estep_Pr (encode_config c) = encode_config (step c)" - using assms estep_Pr1 estep_Pr2 estep_Pr3 estep_Pr4 by simp + using assms estep_Pr1 estep_Pr2 estep_Pr3 estep_Pr4 by auto definition "estep_Mn e \ if e2ls e = 0 then prod_encode (e_cons (triple_encode (pdec22 (e2i e)) (e_cons 0 (e2xs e)) 0) (e_cons (triple_encode (e2i e) (e2xs e) (singleton_encode 0)) (e2tail e)), 0) else if e2rv e = 1 then prod_encode (e2tail e, Suc (e_hd (e2ls e))) else prod_encode (e_cons (triple_encode (pdec22 (e2i e)) (e_cons (Suc (e_hd (e2ls e))) (e2xs e)) 0) (e_cons (triple_encode (e2i e) (e2xs e) (singleton_encode (Suc (e_hd (e2ls e))))) (e2tail e)), 0)" lemma estep_Mn: assumes "c = (((Mn n f, xs, ls) # fs), rv)" shows "estep_Mn (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" consider "ls \ []" and "rv \ Some 0" | "ls \ []" and "rv = Some 0" | "ls = []" by auto then show ?thesis proof (cases) case 1 then have step_c: "step c = ((f, (Suc (hd ls)) # xs, []) # (Mn n f, xs, [Suc (hd ls)]) # fs, None)" (is "step c = ?cfg") using assms by simp have "estep_Mn ?e = prod_encode (e_cons (triple_encode (encode f) (e_cons (Suc (hd ls)) (list_encode xs)) 0) (e_cons (triple_encode (encode (Mn n f)) (list_encode xs) (singleton_encode (Suc (hd ls)))) (list_encode (map encode_frame fs))), 0)" using 1 assms e_hd_def estep_Mn_def by auto also have "... = encode_config ?cfg" using encode_config by (simp add: encode_frame) finally show ?thesis using step_c by simp next case 2 have "estep_Mn ?e = prod_encode (e2tail ?e, Suc (e_hd (e2ls ?e)))" using 2 assms estep_Mn_def by auto also have "... = prod_encode (e2tail ?e, Suc (hd ls))" using 2 assms e_hd_def by auto also have "... = prod_encode (list_encode (map encode_frame fs), Suc (hd ls))" using assms by simp also have "... = encode_config (fs, Some (hd ls))" using encode_config by simp finally show ?thesis using 2 assms by simp next case 3 then show ?thesis using assms encode_frame by (simp add: estep_Mn_def, simp add: encode_config) qed qed definition "estep e \ if e2stack e = 0 then prod_encode (0, e2rv e) else if e2i e = 0 then prod_encode (e2tail e, 1) else if e2i e = 1 then prod_encode (e2tail e, Suc (Suc (e_hd (e2xs e)))) else if encode_kind (e2i e) = 2 then prod_encode (e2tail e, Suc (e_nth (e2xs e) (pdec22 (e2i e)))) else if encode_kind (e2i e) = 3 then estep_Cn e else if encode_kind (e2i e) = 4 then estep_Pr e else if encode_kind (e2i e) = 5 then estep_Mn e else 0" lemma estep_Z: assumes "c = (((Z, xs, ls) # fs), rv)" shows "estep (encode_config c) = encode_config (step c)" using encode_frame by (simp add: assms estep_def, simp add: encode_config assms) lemma estep_S: assumes "c = (((S, xs, ls) # fs), rv)" and "recfn (length xs) (fst (hd (fst c)))" shows "estep (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" from assms have "length xs > 0" by auto then have eq: "hd xs = e_hd (e2xs ?e)" using assms(1) e_hd_def by auto then have "estep ?e = prod_encode (e2tail ?e, Suc (Suc (e_hd (e2xs ?e))))" using assms(1) estep_def by simp moreover have "step c = (fs, Some (Suc (hd xs)))" using assms(1) by simp ultimately show ?thesis using assms(1) eq estep_def encode_config[of fs "Some (Suc (hd xs))"] by simp qed lemma estep_Id: assumes "c = (((Id m n, xs, ls) # fs), rv)" and "recfn (length xs) (fst (hd (fst c)))" shows "estep (encode_config c) = encode_config (step c)" proof - let ?e = "encode_config c" from assms have "length xs = m" and "m > 0" by auto then have eq: "xs ! n = e_nth (e2xs ?e) n" using assms e_hd_def by auto moreover have "encode_kind (e2i ?e) = 2" using assms(1) encode_kind_2 by auto ultimately have "estep ?e = prod_encode (e2tail ?e, Suc (e_nth (e2xs ?e) (pdec22 (e2i ?e))))" using assms estep_def encode_kind_def by auto moreover have "step c = (fs, Some (xs ! n))" using assms(1) by simp ultimately show ?thesis using assms(1) eq encode_config[of fs "Some (xs ! n)"] by simp qed lemma estep: assumes "valid (fst c)" shows "estep (encode_config c) = encode_config (step c)" proof (cases "fst c") case Nil then show ?thesis using estep_def by (metis list_encode.simps(1) e2rv_def e2stack_stack encode_config_def map_is_Nil_conv prod.collapse prod_encode_inverse snd_conv step.simps(1)) next case (Cons s fs) then obtain f xs ls rv where c: "c = ((f, xs, ls) # fs, rv)" by (metis prod.exhaust_sel) with assms valid_def have lenas: "recfn (length xs) f" by simp show ?thesis proof (cases f) case Z then show ?thesis using estep_Z c by simp next case S then show ?thesis using estep_S c lenas by simp next case Id then show ?thesis using estep_Id c lenas by simp next case Cn then show ?thesis using estep_Cn c by (metis e2i_f e2stack_0_iff_Nil encode.simps(1) encode.simps(2) encode_kind_2 encode_kind_3 encode_kind_Cn estep_def list.distinct(1) recf.distinct(13) recf.distinct(19) recf.distinct(5)) next case Pr then show ?thesis using estep_Pr c lenas by (metis e2i_f e2stack_0_iff_Nil encode.simps(1) encode.simps(2) encode_kind_2 encode_kind_4 encode_kind_Cn encode_kind_Pr estep_def list.distinct(1) recf.distinct(15) recf.distinct(21) recf.distinct(25) recf.distinct(7)) next case Mn then show ?thesis using estep_Pr c lenas by (metis (no_types, lifting) e2i_f e2stack_0_iff_Nil encode.simps(1) encode.simps(2) encode_kind_2 encode_kind_5 encode_kind_Cn encode_kind_Mn encode_kind_Pr estep_Mn estep_def list.distinct(1) recf.distinct(17) recf.distinct(23) recf.distinct(27) recf.distinct(9)) qed qed subsection \The step function as a partial recursive function\label{s:step_recf}\ text \In this section we construct a primitive recursive function @{term r_step} computing @{term estep}. This will entail defining @{typ recf}s for many functions defined in the previous section.\ definition "r_e2stack \ r_pdec1" lemma r_e2stack_prim: "prim_recfn 1 r_e2stack" unfolding r_e2stack_def using r_pdec1_prim by simp lemma r_e2stack [simp]: "eval r_e2stack [e] \= e2stack e" unfolding r_e2stack_def e2stack_def using r_pdec1_prim by simp definition "r_e2rv \ r_pdec2" lemma r_e2rv_prim: "prim_recfn 1 r_e2rv" unfolding r_e2rv_def using r_pdec2_prim by simp lemma r_e2rv [simp]: "eval r_e2rv [e] \= e2rv e" unfolding r_e2rv_def e2rv_def using r_pdec2_prim by simp definition "r_e2tail \ Cn 1 r_tl [r_e2stack]" lemma r_e2tail_prim: "prim_recfn 1 r_e2tail" unfolding r_e2tail_def using r_e2stack_prim r_tl_prim by simp lemma r_e2tail [simp]: "eval r_e2tail [e] \= e2tail e" unfolding r_e2tail_def e2tail_def using r_e2stack_prim r_tl_prim by simp definition "r_e2frame \ Cn 1 r_hd [r_e2stack]" lemma r_e2frame_prim: "prim_recfn 1 r_e2frame" unfolding r_e2frame_def using r_hd_prim r_e2stack_prim by simp lemma r_e2frame [simp]: "eval r_e2frame [e] \= e2frame e" unfolding r_e2frame_def e2frame_def using r_hd_prim r_e2stack_prim by simp definition "r_e2i \ Cn 1 r_pdec1 [r_e2frame]" lemma r_e2i_prim: "prim_recfn 1 r_e2i" unfolding r_e2i_def using r_pdec12_prim r_e2frame_prim by simp lemma r_e2i [simp]: "eval r_e2i [e] \= e2i e" unfolding r_e2i_def e2i_def using r_pdec12_prim r_e2frame_prim by simp definition "r_e2xs \ Cn 1 r_pdec12 [r_e2frame]" lemma r_e2xs_prim: "prim_recfn 1 r_e2xs" unfolding r_e2xs_def using r_pdec122_prim r_e2frame_prim by simp lemma r_e2xs [simp]: "eval r_e2xs [e] \= e2xs e" unfolding r_e2xs_def e2xs_def using r_pdec122_prim r_e2frame_prim by simp definition "r_e2ls \ Cn 1 r_pdec22 [r_e2frame]" lemma r_e2ls_prim: "prim_recfn 1 r_e2ls" unfolding r_e2ls_def using r_pdec222_prim r_e2frame_prim by simp lemma r_e2ls [simp]: "eval r_e2ls [e] \= e2ls e" unfolding r_e2ls_def e2ls_def using r_pdec222_prim r_e2frame_prim by simp definition "r_e2lenls \ Cn 1 r_length [r_e2ls]" lemma r_e2lenls_prim: "prim_recfn 1 r_e2lenls" unfolding r_e2lenls_def using r_length_prim r_e2ls_prim by simp lemma r_e2lenls [simp]: "eval r_e2lenls [e] \= e2lenls e" unfolding r_e2lenls_def e2lenls_def using r_length_prim r_e2ls_prim by simp definition "r_kind \ Cn 1 r_ifz [Id 1 0, Z, Cn 1 r_ifeq [Id 1 0, r_const 1, r_const 1, r_pdec1]]" lemma r_kind_prim: "prim_recfn 1 r_kind" unfolding r_kind_def by simp lemma r_kind: "eval r_kind [e] \= encode_kind e" unfolding r_kind_def encode_kind_def by simp lemmas helpers_for_r_step_prim = r_e2i_prim r_e2lenls_prim r_e2ls_prim r_e2rv_prim r_e2xs_prim r_e2stack_prim r_e2tail_prim r_e2frame_prim text \We define primitive recursive functions @{term r_step_Id}, @{term r_step_Cn}, @{term r_step_Pr}, and @{term r_step_Mn}. The last three correspond to @{term estep_Cn}, @{term estep_Pr}, and @{term estep_Mn} from the previous section.\ definition "r_step_Id \ Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_nth [r_e2xs, Cn 1 r_pdec22 [r_e2i]]]]" lemma r_step_Id: "eval r_step_Id [e] \= prod_encode (e2tail e, Suc (e_nth (e2xs e) (pdec22 (e2i e))))" unfolding r_step_Id_def using helpers_for_r_step_prim by simp abbreviation r_triple_encode :: "recf \ recf \ recf \ recf" where "r_triple_encode x y z \ Cn 1 r_prod_encode [x, Cn 1 r_prod_encode [y, z]]" definition "r_step_Cn \ Cn 1 r_ifeq [r_e2lenls, Cn 1 r_length [Cn 1 r_pdec222 [r_e2i]], Cn 1 r_ifz [r_e2rv, Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec122 [r_e2i]) r_e2ls Z, r_e2stack], Z], Cn 1 r_prod_encode [r_e2tail, r_e2rv]], Cn 1 r_ifz [r_e2rv, Cn 1 r_ifless [r_e2lenls, Cn 1 r_length [Cn 1 r_pdec222 [r_e2i]], Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_nth [Cn 1 r_pdec222 [r_e2i], r_e2lenls]) r_e2xs Z, r_e2stack], Z], Cn 1 r_prod_encode [r_e2tail, r_e2rv]], Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode r_e2i r_e2xs (Cn 1 r_snoc [r_e2ls, Cn 1 r_dec [r_e2rv]]), r_e2tail], Z]]]" lemma r_step_Cn_prim: "prim_recfn 1 r_step_Cn" unfolding r_step_Cn_def using helpers_for_r_step_prim by simp lemma r_step_Cn: "eval r_step_Cn [e] \= estep_Cn e" unfolding r_step_Cn_def estep_Cn_def using helpers_for_r_step_prim by simp definition "r_step_Pr \ Cn 1 r_ifz [r_e2ls, Cn 1 r_ifz [r_e2rv, Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec122 [r_e2i]) (Cn 1 r_tl [r_e2xs]) Z, r_e2stack], Z], Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Cn 1 r_dec [r_e2rv]]), r_e2tail], Z]], Cn 1 r_ifeq [r_e2lenls, Cn 1 S [Cn 1 r_hd [r_e2xs]], Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_hd [r_e2ls]]], Cn 1 r_ifz [r_e2rv, Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec222 [r_e2i]) (Cn 1 r_cons [Cn 1 r_dec [r_e2lenls], Cn 1 r_cons [Cn 1 r_hd [r_e2ls], Cn 1 r_tl [r_e2xs]]]) Z, r_e2stack], Z], Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode r_e2i r_e2xs (Cn 1 r_cons [Cn 1 r_dec [r_e2rv], r_e2ls]), r_e2tail], Z]]]]" lemma r_step_Pr_prim: "prim_recfn 1 r_step_Pr" unfolding r_step_Pr_def using helpers_for_r_step_prim by simp lemma r_step_Pr: "eval r_step_Pr [e] \= estep_Pr e" unfolding r_step_Pr_def estep_Pr_def using helpers_for_r_step_prim by simp definition "r_step_Mn \ Cn 1 r_ifz [r_e2ls, Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec22 [r_e2i]) (Cn 1 r_cons [Z, r_e2xs]) Z, Cn 1 r_cons [r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Z]), r_e2tail]], Z], Cn 1 r_ifeq [r_e2rv, r_const 1, Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_hd [r_e2ls]]], Cn 1 r_prod_encode [Cn 1 r_cons [r_triple_encode (Cn 1 r_pdec22 [r_e2i]) (Cn 1 r_cons [Cn 1 S [Cn 1 r_hd [r_e2ls]], r_e2xs]) Z, Cn 1 r_cons [r_triple_encode r_e2i r_e2xs (Cn 1 r_singleton_encode [Cn 1 S [Cn 1 r_hd [r_e2ls]]]), r_e2tail]], Z]]]" lemma r_step_Mn_prim: "prim_recfn 1 r_step_Mn" unfolding r_step_Mn_def using helpers_for_r_step_prim by simp lemma r_step_Mn: "eval r_step_Mn [e] \= estep_Mn e" unfolding r_step_Mn_def estep_Mn_def using helpers_for_r_step_prim by simp definition "r_step \ Cn 1 r_ifz [r_e2stack, Cn 1 r_prod_encode [Z, r_e2rv], Cn 1 r_ifz [r_e2i, Cn 1 r_prod_encode [r_e2tail, r_const 1], Cn 1 r_ifeq [r_e2i, r_const 1, Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 S [Cn 1 r_hd [r_e2xs]]]], Cn 1 r_ifeq [Cn 1 r_kind [r_e2i], r_const 2, Cn 1 r_prod_encode [r_e2tail, Cn 1 S [Cn 1 r_nth [r_e2xs, Cn 1 r_pdec22 [r_e2i]]]], Cn 1 r_ifeq [Cn 1 r_kind [r_e2i], r_const 3, r_step_Cn, Cn 1 r_ifeq [Cn 1 r_kind [r_e2i], r_const 4, r_step_Pr, Cn 1 r_ifeq [Cn 1 r_kind [r_e2i], r_const 5, r_step_Mn, Z]]]]]]]" lemma r_step_prim: "prim_recfn 1 r_step" unfolding r_step_def using r_kind_prim r_step_Mn_prim r_step_Pr_prim r_step_Cn_prim helpers_for_r_step_prim by simp lemma r_step: "eval r_step [e] \= estep e" unfolding r_step_def estep_def using r_kind_prim r_step_Mn_prim r_step_Pr_prim r_step_Cn_prim helpers_for_r_step_prim r_kind r_step_Cn r_step_Pr r_step_Mn by simp theorem r_step_equiv_step: assumes "valid (fst c)" shows "eval r_step [encode_config c] \= encode_config (step c)" using r_step estep assms by simp subsection \The universal function\label{s:the_universal}\ text \The next function computes the configuration after arbitrarily many steps.\ definition "r_leap \ Pr 2 (Cn 2 r_prod_encode [Cn 2 r_singleton_encode [Cn 2 r_prod_encode [Id 2 0, Cn 2 r_prod_encode [Id 2 1, r_constn 1 0]]], r_constn 1 0]) (Cn 4 r_step [Id 4 1])" lemma r_leap_prim [simp]: "prim_recfn 3 r_leap" unfolding r_leap_def using r_step_prim by simp lemma r_leap_total: "eval r_leap [t, i, x] \" using prim_recfn_total[OF r_leap_prim] by simp lemma r_leap: assumes "i = encode f" and "recfn (e_length x) f" shows "eval r_leap [t, i, x] \= encode_config (iterate t step ([(f, list_decode x, [])], None))" proof (induction t) case 0 then show ?case unfolding r_leap_def using r_step_prim assms encode_config encode_frame by simp next case (Suc t) let ?c = "([(f, list_decode x, [])], None)" let ?tc = "iterate t step ?c" have "valid (fst ?c)" using valid_def assms by simp then have valid: "valid (fst ?tc)" using iterate_step_valid by simp have "eval r_leap [Suc t, i, x] = eval (Cn 4 r_step [Id 4 1]) [t, the (eval r_leap [t, i, x]), i, x]" - unfolding r_leap_def using eval_Pr_prim_Suc r_step_prim assms by simp + by (smt One_nat_def Suc_eq_plus1 eq_numeral_Suc eval_Pr_converg_Suc list.size(3) list.size(4) nat_1_add_1 pred_numeral_simps(3) r_leap_def r_leap_prim r_leap_total) then have "eval r_leap [Suc t, i, x] = eval (Cn 4 r_step [Id 4 1]) [t, encode_config ?tc, i, x]" using Suc by simp then have "eval r_leap [Suc t, i, x] = eval r_step [encode_config ?tc]" using r_step_prim by simp then have "eval r_leap [Suc t, i, x] \= encode_config (step ?tc)" by (simp add: r_step_equiv_step valid) then show ?case by simp qed lemma step_leaves_empty_stack_empty: assumes "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)" shows "iterate (t + t') step ([(f, list_decode x, [])], None) = ([], Some v)" using assms by (induction t') simp_all text \The next function is essentially a convenience wrapper around @{term r_leap}. It returns zero if the configuration returned by @{term r_leap} is non-final, and @{term "Suc v"} if the configuration is final with return value $v$.\ definition "r_result \ Cn 3 r_ifz [Cn 3 r_pdec1 [r_leap], Cn 3 r_pdec2 [r_leap], r_constn 2 0]" lemma r_result_prim [simp]: "prim_recfn 3 r_result" unfolding r_result_def using r_leap_prim by simp lemma r_result_total: "total r_result" using r_result_prim by blast lemma r_result_empty_stack_None: assumes "i = encode f" and "recfn (e_length x) f" and "iterate t step ([(f, list_decode x, [])], None) = ([], None)" shows "eval r_result [t, i, x] \= 0" unfolding r_result_def using assms r_leap e2stack_0_iff_Nil e2stack_def e2stack_stack r_leap_total r_leap_prim e2rv_def e2rv_rv by simp lemma r_result_empty_stack_Some: assumes "i = encode f" and "recfn (e_length x) f" and "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)" shows "eval r_result [t, i, x] \= Suc v" unfolding r_result_def using assms r_leap e2stack_0_iff_Nil e2stack_def e2stack_stack r_leap_total r_leap_prim e2rv_def e2rv_rv by simp lemma r_result_empty_stack_stays: assumes "i = encode f" and "recfn (e_length x) f" and "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)" shows "eval r_result [t + t', i, x] \= Suc v" using assms step_leaves_empty_stack_empty r_result_empty_stack_Some by simp lemma r_result_nonempty_stack: assumes "i = encode f" and "recfn (e_length x) f" and "fst (iterate t step ([(f, list_decode x, [])], None)) \ []" shows "eval r_result [t, i, x] \= 0" proof - obtain ss rv where "iterate t step ([(f, list_decode x, [])], None) = (ss, rv)" by fastforce moreover from this assms(3) have "ss \ []" by simp ultimately have "eval r_leap [t, i, x] \= encode_config (ss, rv)" using assms r_leap by simp then have "eval (Cn 3 r_pdec1 [r_leap]) [t, i, x] \\ 0" using `ss \ []` r_leap_prim encode_config r_leap_total list_encode_0 by (auto, blast) then show ?thesis unfolding r_result_def using r_leap_prim by auto qed lemma r_result_Suc: assumes "i = encode f" and "recfn (e_length x) f" and "eval r_result [t, i, x] \= Suc v" shows "iterate t step ([(f, list_decode x, [])], None) = ([], Some v)" (is "?cfg = _") proof (cases "fst ?cfg") case Nil then show ?thesis using assms r_result_empty_stack_None r_result_empty_stack_Some by (metis Zero_not_Suc nat.inject option.collapse option.inject prod.exhaust_sel) next case Cons then show ?thesis using assms r_result_nonempty_stack by simp qed lemma r_result_converg: assumes "i = encode f" and "recfn (e_length x) f" and "eval f (list_decode x) \= v" shows "\t. (\t'\t. eval r_result [t', i, x] \= Suc v) \ (\t'= 0)" proof - let ?xs = "list_decode x" let ?stack = "[(f, ?xs, [])]" have "wellf f" using assms(2) by simp moreover have "length ?xs = arity f" using assms(2) by simp ultimately have "correct (?stack, None)" using step_correct valid_def by simp with assms(3) have "reachable (?stack, None) ([], Some v)" by simp then obtain t where "iterate t step (?stack, None) = ([], Some v)" "\t' []" using reachable_iterate_step_empty_stack by blast then have t: "eval r_result [t, i, x] \= Suc v" "\t'= 0" using r_result_empty_stack_Some r_result_nonempty_stack assms(1,2) by simp_all then have "eval r_result [t + t', i, x] \= Suc v" for t' using r_result_empty_stack_stays assms r_result_Suc by simp then have "\t'\t. eval r_result [t', i, x] \= Suc v" using le_Suc_ex by blast with t(2) show ?thesis by auto qed lemma r_result_diverg: assumes "i = encode f" and "recfn (e_length x) f" and "eval f (list_decode x) \" shows "eval r_result [t, i, x] \= 0" proof - let ?xs = "list_decode x" let ?stack = "[(f, ?xs, [])]" have "recfn (length ?xs) f" using assms(2) by auto then have "correct (?stack, None)" using step_correct valid_def by simp with assms(3) have "nonterminating (?stack, None)" by simp then show ?thesis using r_result_nonempty_stack assms(1,2) by simp qed text \Now we can define the universal partial recursive function. This function executes @{term r_result} for increasing time bounds, waits for it to reach a final configuration, and then extracts its result value. If no final configuration is reached, the universal function diverges.\ definition "r_univ \ Cn 2 r_dec [Cn 2 r_result [Mn 2 (Cn 3 r_not [r_result]), Id 2 0, Id 2 1]]" lemma r_univ_recfn [simp]: "recfn 2 r_univ" unfolding r_univ_def by simp theorem r_univ: assumes "i = encode f" and "recfn (e_length x) f" shows "eval r_univ [i, x] = eval f (list_decode x)" proof - let ?cond = "Cn 3 r_not [r_result]" let ?while = "Mn 2 ?cond" let ?res = "Cn 2 r_result [?while, Id 2 0, Id 2 1]" let ?xs = "list_decode x" have *: "eval ?cond [t, i, x] \= (if eval r_result [t, i, x] \= 0 then 1 else 0)" for t proof - have "eval ?cond [t, i, x] = eval r_not [the (eval r_result [t, i, x])]" using r_result_total by simp moreover have "eval r_result [t, i, x] \" by (simp add: r_result_total) ultimately show ?thesis by auto qed show ?thesis proof (cases "eval f ?xs \") case True then show ?thesis unfolding r_univ_def using * r_result_diverg[OF assms] eval_Mn_diverg by simp next case False then obtain v where v: "eval f ?xs \= v" by auto then obtain t where t: "\t'\t. eval r_result [t', i, x] \= Suc v" "\t'= 0" using r_result_converg[OF assms] by blast then have "\t'\t. eval ?cond [t', i, x] \= 0" "\t'= 1" using * by simp_all then have "eval ?while [i, x] \= t" using eval_Mn_convergI[of 2 ?cond "[i, x]" t] by simp then have "eval ?res [i, x] = eval r_result [t, i, x]" by simp then have "eval ?res [i, x] \= Suc v" using t(1) by simp then show ?thesis unfolding r_univ_def using v by simp qed qed theorem r_univ': assumes "recfn (e_length x) f" shows "eval r_univ [encode f, x] = eval f (list_decode x)" using r_univ assms by simp text \Universal functions for every arity can be built from @{term "r_univ"}.\ definition r_universal :: "nat \ recf" where "r_universal n \ Cn (Suc n) r_univ [Id (Suc n) 0, r_shift (r_list_encode (n - 1))]" lemma r_universal_recfn [simp]: "n > 0 \ recfn (Suc n) (r_universal n)" unfolding r_universal_def by simp lemma r_universal: assumes "recfn n f" and "length xs = n" shows "eval (r_universal n) (encode f # xs) = eval f xs" unfolding r_universal_def using wellf_arity_nonzero assms r_list_encode r_univ' by fastforce text \We will mostly be concerned with computing unary functions. Hence we introduce separate functions for this case.\ definition "r_result1 \ Cn 3 r_result [Id 3 0, Id 3 1, Cn 3 r_singleton_encode [Id 3 2]]" lemma r_result1_prim [simp]: "prim_recfn 3 r_result1" unfolding r_result1_def by simp lemma r_result1_total: "total r_result1" using Mn_free_imp_total by simp lemma r_result1 [simp]: "eval r_result1 [t, i, x] = eval r_result [t, i, singleton_encode x]" unfolding r_result1_def by simp text \The following function will be our standard Gödel numbering of all unary partial recursive functions.\ definition "r_phi \ r_universal 1" lemma r_phi_recfn [simp]: "recfn 2 r_phi" unfolding r_phi_def by simp theorem r_phi: assumes "i = encode f" and "recfn 1 f" shows "eval r_phi [i, x] = eval f [x]" - unfolding r_phi_def using r_universal assms by simp + unfolding r_phi_def using r_universal assms by force corollary r_phi': assumes "recfn 1 f" shows "eval r_phi [encode f, x] = eval f [x]" using assms r_phi by simp lemma r_phi'': "eval r_phi [i, x] = eval r_univ [i, singleton_encode x]" unfolding r_universal_def r_phi_def using r_list_encode by simp section \Applications of the universal function\ text \In this section we shall see some ways @{term r_univ} and @{term r_result} can be used.\ subsection \Lazy conditional evaluation\ text \With the help of @{term r_univ} we can now define a \hypertarget{p:r_lifz}{lazy variant} of @{term r_ifz}, in which only one branch is evaluated.\ definition r_lazyifzero :: "nat \ nat \ nat \ recf" where "r_lazyifzero n j\<^sub>1 j\<^sub>2 \ Cn (Suc (Suc n)) r_univ [Cn (Suc (Suc n)) r_ifz [Id (Suc (Suc n)) 0, r_constn (Suc n) j\<^sub>1, r_constn (Suc n) j\<^sub>2], r_shift (r_list_encode n)]" lemma r_lazyifzero_recfn: "recfn (Suc (Suc n)) (r_lazyifzero n j\<^sub>1 j\<^sub>2)" using r_lazyifzero_def by simp lemma r_lazyifzero: assumes "length xs = Suc n" and "j\<^sub>1 = encode f\<^sub>1" and "j\<^sub>2 = encode f\<^sub>2" and "recfn (Suc n) f\<^sub>1" and "recfn (Suc n) f\<^sub>2" shows "eval (r_lazyifzero n j\<^sub>1 j\<^sub>2) (c # xs) = (if c = 0 then eval f\<^sub>1 xs else eval f\<^sub>2 xs)" proof - let ?a = "r_constn (Suc n) n" let ?b = "Cn (Suc (Suc n)) r_ifz [Id (Suc (Suc n)) 0, r_constn (Suc n) j\<^sub>1, r_constn (Suc n) j\<^sub>2]" let ?c = "r_shift (r_list_encode n)" have "eval ?a (c # xs) \= n" using assms(1) by simp moreover have "eval ?b (c # xs) \= (if c = 0 then j\<^sub>1 else j\<^sub>2)" using assms(1) by simp moreover have "eval ?c (c # xs) \= list_encode xs" using assms(1) r_list_encode r_shift by simp ultimately have "eval (r_lazyifzero n j\<^sub>1 j\<^sub>2) (c # xs) = eval r_univ [if c = 0 then j\<^sub>1 else j\<^sub>2, list_encode xs]" unfolding r_lazyifzero_def using r_lazyifzero_recfn assms(1) by simp then show ?thesis using assms r_univ by simp qed definition r_lifz :: "recf \ recf \ recf" where "r_lifz f g \ r_lazyifzero (arity f - 1) (encode f) (encode g)" lemma r_lifz_recfn [simp]: assumes "recfn n f" and "recfn n g" shows "recfn (Suc n) (r_lifz f g)" using assms r_lazyifzero_recfn r_lifz_def wellf_arity_nonzero by auto lemma r_lifz [simp]: assumes "length xs = n" and "recfn n f" and "recfn n g" shows "eval (r_lifz f g) (c # xs) = (if c = 0 then eval f xs else eval g xs)" using assms r_lazyifzero r_lifz_def wellf_arity_nonzero by (metis One_nat_def Suc_pred) subsection \Enumerating the domains of partial recursive functions\ text \In this section we define a binary function $\mathit{enumdom}$ such that for all $i$, the domain of $\varphi_i$ equals $\{\mathit{enumdom}(i, x) \mid \mathit{enumdom}(i, x)\!\downarrow\}$. In other words, the image of $\mathit{enumdom}_i$ is the domain of $\varphi_i$. First we need some more properties of @{term r_leap} and @{term r_result}.\ lemma r_leap_Suc: "eval r_leap [Suc t, i, x] = eval r_step [the (eval r_leap [t, i, x])]" proof - have "eval r_leap [Suc t, i, x] = eval (Cn 4 r_step [Id 4 1]) [t, the (eval r_leap [t, i, x]), i, x]" using r_leap_total eval_Pr_converg_Suc r_leap_def by (metis length_Cons list.size(3) numeral_2_eq_2 numeral_3_eq_3 r_leap_prim) then show ?thesis using r_step_prim by auto qed lemma r_leap_Suc_saturating: assumes "pdec1 (the (eval r_leap [t, i, x])) = 0" shows "eval r_leap [Suc t, i, x] = eval r_leap [t, i, x]" proof - let ?e = "eval r_leap [t, i, x]" have "eval r_step [the ?e] \= estep (the ?e)" using r_step by simp then have "eval r_step [the ?e] \= prod_encode (0, e2rv (the ?e))" using estep_def assms by (simp add: e2stack_def) then have "eval r_step [the ?e] \= prod_encode (pdec1 (the ?e), pdec2 (the ?e))" using assms by (simp add: e2rv_def) then have "eval r_step [the ?e] \= the ?e" by simp then show ?thesis using r_leap_total r_leap_Suc by simp qed lemma r_result_Suc_saturating: assumes "eval r_result [t, i, x] \= Suc v" shows "eval r_result [Suc t, i, x] \= Suc v" proof - let ?r = "\t. eval r_ifz [pdec1 (the (eval r_leap [t, i, x])), pdec2 (the (eval r_leap [t, i, x])), 0]" have "?r t \= Suc v" using assms unfolding r_result_def using r_leap_total r_leap_prim by simp then have "pdec1 (the (eval r_leap [t, i, x])) = 0" using option.sel by fastforce then have "eval r_leap [Suc t, i, x] = eval r_leap [t, i, x]" using r_leap_Suc_saturating by simp moreover have "eval r_result [t, i, x] = ?r t" unfolding r_result_def using r_leap_total r_leap_prim by simp moreover have "eval r_result [Suc t, i, x] = ?r (Suc t)" unfolding r_result_def using r_leap_total r_leap_prim by simp ultimately have "eval r_result [Suc t, i, x] = eval r_result [t, i, x]" by simp with assms show ?thesis by simp qed lemma r_result_saturating: assumes "eval r_result [t, i, x] \= Suc v" shows "eval r_result [t + d, i, x] \= Suc v" using r_result_Suc_saturating assms by (induction d) simp_all lemma r_result_converg': assumes "eval r_univ [i, x] \= v" shows "\t. (\t'\t. eval r_result [t', i, x] \= Suc v) \ (\t'= 0)" proof - let ?f = "Cn 3 r_not [r_result]" let ?m = "Mn 2 ?f" have "recfn 2 ?m" by simp have eval_m: "eval ?m [i, x] \" proof assume "eval ?m [i, x] \" then have "eval r_univ [i, x] \" unfolding r_univ_def by simp with assms show False by simp qed then obtain t where t: "eval ?m [i, x] \= t" by auto then have f_t: "eval ?f [t, i, x] \= 0" and f_less_t: "\y. y < t \ eval ?f [y, i, x] \\ 0" using eval_Mn_convergE[of 2 ?f "[i, x]" t] `recfn 2 ?m` by (metis (no_types, lifting) One_nat_def Suc_1 length_Cons list.size(3))+ have eval_Cn2: "eval (Cn 2 r_result [?m, Id 2 0, Id 2 1]) [i, x] \" proof assume "eval (Cn 2 r_result [?m, Id 2 0, Id 2 1]) [i, x] \" then have "eval r_univ [i, x] \" unfolding r_univ_def by simp with assms show False by simp qed have "eval r_result [t, i, x] \= Suc v" proof (rule ccontr) assume neq_Suc: "\ eval r_result [t, i, x] \= Suc v" show False proof (cases "eval r_result [t, i, x] = None") case True then show ?thesis using f_t by simp next case False then obtain w where w: "eval r_result [t, i, x] \= w" "w \ Suc v" using neq_Suc by auto moreover have "eval r_result [t, i, x] \\ 0" by (rule ccontr; use f_t in auto) ultimately have "w \ 0" by simp have "eval (Cn 2 r_result [?m, Id 2 0, Id 2 1]) [i, x] = eval r_result [the (eval ?m [i, x]), i, x]" using eval_m by simp with w t have "eval (Cn 2 r_result [?m, Id 2 0, Id 2 1]) [i, x] \= w" by simp moreover have "eval r_univ [i, x] = eval r_dec [the (eval (Cn 2 r_result [?m, Id 2 0, Id 2 1]) [i, x])]" unfolding r_univ_def using eval_Cn2 by simp ultimately have "eval r_univ [i, x] = eval r_dec [w]" by simp then have "eval r_univ [i, x] \= w - 1" by simp with assms `w \ 0` w show ?thesis by simp qed qed then have "\t'\t. eval r_result [t', i, x] \= Suc v" using r_result_saturating le_Suc_ex by blast moreover have "eval r_result [y, i, x] \= 0" if "y < t" for y proof (rule ccontr) assume neq0: "eval r_result [y, i, x] \ Some 0" then show False proof (cases "eval r_result [y, i, x] = None") case True then show ?thesis using f_less_t `y < t` by fastforce next case False then obtain v where "eval r_result [y, i, x] \= v" "v \ 0" using neq0 by auto then have "eval ?f [y, i, x] \= 0" by simp then show ?thesis using f_less_t `y < t` by simp qed qed ultimately show ?thesis by auto qed lemma r_result_diverg': assumes "eval r_univ [i, x] \" shows "eval r_result [t, i, x] \= 0" proof (rule ccontr) let ?f = "Cn 3 r_not [r_result]" let ?m = "Mn 2 ?f" assume "eval r_result [t, i, x] \ Some 0" with r_result_total have "eval r_result [t, i, x] \\ 0" by simp then have "eval ?f [t, i, x] \= 0" by auto moreover have "eval ?f [y, i, x] \" if "y < t" for y using r_result_total by simp ultimately have "\z. eval ?f (z # [i, x]) \= 0 \ (\y)" by blast then have "eval ?m [i, x] \" by simp then have "eval r_univ [i, x] \" unfolding r_univ_def using r_result_total by simp with assms show False by simp qed lemma r_result_bivalent': assumes "eval r_univ [i, x] \= v" shows "eval r_result [t, i, x] \= Suc v \ eval r_result [t, i, x] \= 0" using r_result_converg'[OF assms] not_less by blast lemma r_result_Some': assumes "eval r_result [t, i, x] \= Suc v" shows "eval r_univ [i, x] \= v" proof (rule ccontr) assume not_v: "\ eval r_univ [i, x] \= v" show False proof (cases "eval r_univ [i, x] \") case True then show ?thesis using assms r_result_diverg' by simp next case False then obtain w where w: "eval r_univ [i, x] \= w" "w \ v" using not_v by auto then have "eval r_result [t, i, x] \= Suc w \ eval r_result [t, i, x] \= 0" using r_result_bivalent' by simp then show ?thesis using assms not_v w by simp qed qed lemma r_result1_converg': assumes "eval r_phi [i, x] \= v" shows "\t. (\t'\t. eval r_result1 [t', i, x] \= Suc v) \ (\t'= 0)" using assms r_result1 r_result_converg' r_phi'' by simp lemma r_result1_diverg': assumes "eval r_phi [i, x] \" shows "eval r_result1 [t, i, x] \= 0" using assms r_result1 r_result_diverg' r_phi'' by simp lemma r_result1_Some': assumes "eval r_result1 [t, i, x] \= Suc v" shows "eval r_phi [i, x] \= v" using assms r_result1 r_result_Some' r_phi'' by simp text \The next function performs dovetailing in order to evaluate $\varphi_i$ for every argument for arbitrarily many steps. Given $i$ and $z$, the function decodes $z$ into a pair $(x, t$) and outputs zero (meaning ``true'') iff.\ the computation of $\varphi_i$ on input $x$ halts after at most $t$ steps. Fixing $i$ and varying $z$ will eventually compute $\varphi_i$ for every argument in the domain of $\varphi_i$ sufficiently long for it to converge.\ definition "r_dovetail \ Cn 2 r_not [Cn 2 r_result1 [Cn 2 r_pdec2 [Id 2 1], Id 2 0, Cn 2 r_pdec1 [Id 2 1]]]" lemma r_dovetail_prim: "prim_recfn 2 r_dovetail" by (simp add: r_dovetail_def) lemma r_dovetail: "eval r_dovetail [i, z] \= (if the (eval r_result1 [pdec2 z, i, pdec1 z]) > 0 then 0 else 1)" unfolding r_dovetail_def using r_result_total by simp text \The function $\mathit{enumdom}$ works as follows in order to enumerate exactly the domain of $\varphi_i$. Given $i$ and $y$ it searches for the minimum $z \geq y$ for which the dovetail function returns true. This $z$ is decoded into $(x, t)$ and the $x$ is output. In this way every value output by $\mathit{enumdom}$ is in the domain of $\varphi_i$ by construction of @{term r_dovetail}. Conversely an $x$ in the domain will be output for $y = (x, t)$ where $t$ is such that $\varphi_i$ halts on $x$ within $t$ steps.\ definition "r_dovedelay \ Cn 3 r_and [Cn 3 r_dovetail [Id 3 1, Id 3 0], Cn 3 r_ifle [Id 3 2, Id 3 0, r_constn 2 0, r_constn 2 1]]" lemma r_dovedelay_prim: "prim_recfn 3 r_dovedelay" unfolding r_dovedelay_def using r_dovetail_prim by simp lemma r_dovedelay: "eval r_dovedelay [z, i, y] \= (if the (eval r_result1 [pdec2 z, i, pdec1 z]) > 0 \ y \ z then 0 else 1)" by (simp add: r_dovedelay_def r_dovetail r_dovetail_prim) definition "r_enumdom \ Cn 2 r_pdec1 [Mn 2 r_dovedelay]" lemma r_enumdom_recfn [simp]: "recfn 2 r_enumdom" by (simp add: r_enumdom_def r_dovedelay_prim) lemma r_enumdom [simp]: "eval r_enumdom [i, y] = (if \z. eval r_dovedelay [z, i, y] \= 0 then Some (pdec1 (LEAST z. eval r_dovedelay [z, i, y] \= 0)) else None)" proof - let ?h = "Mn 2 r_dovedelay" have "total r_dovedelay" using r_dovedelay_prim by blast then have "eval ?h [i, y] = (if (\z. eval r_dovedelay [z, i, y] \= 0) then Some (LEAST z. eval r_dovedelay [z, i, y] \= 0) else None)" using r_dovedelay_prim r_enumdom_recfn eval_Mn_convergI by simp then show ?thesis unfolding r_enumdom_def using r_dovedelay_prim by simp qed text \If @{term i} is the code of the empty function, @{term r_enumdom} has an empty domain, too.\ lemma r_enumdom_empty_domain: assumes "\x. eval r_phi [i, x] \" shows "\y. eval r_enumdom [i, y] \" using assms r_result1_diverg' r_dovedelay by simp text \If @{term i} is the code of a function with non-empty domain, @{term r_enumdom} enumerates its domain.\ lemma r_enumdom_nonempty_domain: assumes "eval r_phi [i, x\<^sub>0] \" shows "\y. eval r_enumdom [i, y] \" and "\x. eval r_phi [i, x] \ \ (\y. eval r_enumdom [i, y] \= x)" proof - show "eval r_enumdom [i, y] \" for y proof - obtain t where t: "\t'\t. the (eval r_result1 [t', i, x\<^sub>0]) > 0" using assms r_result1_converg' by fastforce let ?z = "prod_encode (x\<^sub>0, max t y)" have "y \ ?z" using le_prod_encode_2 max.bounded_iff by blast moreover have "pdec2 ?z \ t" by simp ultimately have "the (eval r_result1 [pdec2 ?z, i, pdec1 ?z]) > 0" using t by simp with `y \ ?z` r_dovedelay have "eval r_dovedelay [?z, i, y] \= 0" by presburger then show "eval r_enumdom [i, y] \" using r_enumdom by auto qed show "eval r_phi [i, x] \ = (\y. eval r_enumdom [i, y] \= x)" for x proof show "\y. eval r_enumdom [i, y] \= x" if "eval r_phi [i, x] \" for x proof - from that obtain v where "eval r_phi [i, x] \= v" by auto then obtain t where t: "the (eval r_result1 [t, i, x]) > 0" using r_result1_converg' assms by (metis Zero_not_Suc dual_order.refl option.sel zero_less_iff_neq_zero) let ?y = "prod_encode (x, t)" have "eval r_dovedelay [?y, i, ?y] \= 0" using r_dovedelay t by simp moreover from this have "(LEAST z. eval r_dovedelay [z, i, ?y] \= 0) = ?y" using gr_implies_not_zero r_dovedelay by (intro Least_equality; fastforce) ultimately have "eval r_enumdom [i, ?y] \= x" using r_enumdom by auto then show ?thesis by blast qed show "eval r_phi [i, x] \" if "\y. eval r_enumdom [i, y] \= x" for x proof - from that obtain y where y: "eval r_enumdom [i, y] \= x" by auto then have "eval r_enumdom [i, y] \" by simp then have "\z. eval r_dovedelay [z, i, y] \= 0" and *: "eval r_enumdom [i, y] \= pdec1 (LEAST z. eval r_dovedelay [z, i, y] \= 0)" (is "_ \= pdec1 ?z") using r_enumdom by metis+ then have z: "eval r_dovedelay [?z, i, y] \= 0" by (meson wellorder_Least_lemma(1)) have "the (eval r_result1 [pdec2 ?z, i, pdec1 ?z]) > 0" proof (rule ccontr) assume "\ (the (eval r_result1 [pdec2 ?z, i, pdec1 ?z]) > 0)" then show False using r_dovedelay z by simp qed then have "eval r_phi [i, pdec1 ?z] \" using r_result1_diverg' assms by fastforce then show ?thesis using y * by auto qed qed qed text \For every $\varphi_i$ with non-empty domain there is a total recursive function that enumerates the domain of $\varphi_i$.\ lemma nonempty_domain_enumerable: assumes "eval r_phi [i, x\<^sub>0] \" shows "\g. recfn 1 g \ total g \ (\x. eval r_phi [i, x] \ \ (\y. eval g [y] \= x))" proof - define g where "g \ Cn 1 r_enumdom [r_const i, Id 1 0]" then have "recfn 1 g" by simp moreover from this have "total g" using totalI1[of g] g_def assms r_enumdom_nonempty_domain(1) by simp moreover have "eval r_phi [i, x] \ \ (\y. eval g [y] \= x)" for x unfolding g_def using r_enumdom_nonempty_domain(2)[OF assms] by simp ultimately show ?thesis by auto qed subsection \Concurrent evaluation of functions\ text \We define a function that simulates two @{typ recf}s ``concurrently'' for the same argument and returns the result of the one converging first. If both diverge, so does the simulation function.\ definition "r_both \ Cn 4 r_ifz [Cn 4 r_result1 [Id 4 0, Id 4 1, Id 4 3], Cn 4 r_ifz [Cn 4 r_result1 [Id 4 0, Id 4 2, Id 4 3], Cn 4 r_prod_encode [r_constn 3 2, r_constn 3 0], Cn 4 r_prod_encode [r_constn 3 1, Cn 4 r_dec [Cn 4 r_result1 [Id 4 0, Id 4 2, Id 4 3]]]], Cn 4 r_prod_encode [r_constn 3 0, Cn 4 r_dec [Cn 4 r_result1 [Id 4 0, Id 4 1, Id 4 3]]]]" lemma r_both_prim [simp]: "prim_recfn 4 r_both" unfolding r_both_def by simp lemma r_both: assumes "\x. eval r_phi [i, x] = eval f [x]" and "\x. eval r_phi [j, x] = eval g [x]" shows "eval f [x] \ \ eval g [x] \ \ eval r_both [t, i, j, x] \= prod_encode (2, 0)" and "\eval r_result1 [t, i, x] \= 0; eval r_result1 [t, j, x] \= 0\ \ eval r_both [t, i, j, x] \= prod_encode (2, 0)" and "eval r_result1 [t, i, x] \= Suc v \ eval r_both [t, i, j, x] \= prod_encode (0, the (eval f [x]))" and "\eval r_result1 [t, i, x] \= 0; eval r_result1 [t, j, x] \= Suc v\ \ eval r_both [t, i, j, x] \= prod_encode (1, the (eval g [x]))" proof - have r_result_total [simp]: "eval r_result [t, k, x] \" for t k x using r_result_total by simp { assume "eval f [x] \ \ eval g [x] \" then have "eval r_result1 [t, i, x] \= 0" and "eval r_result1 [t, j, x] \= 0" using assms r_result1_diverg' by auto then show "eval r_both [t, i, j, x] \= prod_encode (2, 0)" unfolding r_both_def by simp next assume "eval r_result1 [t, i, x] \= 0" and "eval r_result1 [t, j, x] \= 0" then show "eval r_both [t, i, j, x] \= prod_encode (2, 0)" unfolding r_both_def by simp next assume "eval r_result1 [t, i, x] \= Suc v" moreover from this have "eval r_result1 [t, i, x] \= Suc (the (eval f [x]))" using assms r_result1_Some' by fastforce ultimately show "eval r_both [t, i, j, x] \= prod_encode (0, the (eval f [x]))" unfolding r_both_def by auto next assume "eval r_result1 [t, i, x] \= 0" and "eval r_result1 [t, j, x] \= Suc v" moreover from this have "eval r_result1 [t, j, x] \= Suc (the (eval g [x]))" using assms r_result1_Some' by fastforce ultimately show "eval r_both [t, i, j, x] \= prod_encode (1, the (eval g [x]))" unfolding r_both_def by auto } qed definition "r_parallel \ Cn 3 r_both [Mn 3 (Cn 4 r_le [Cn 4 r_pdec1 [r_both], r_constn 3 1]), Id 3 0, Id 3 1, Id 3 2]" lemma r_parallel_recfn [simp]: "recfn 3 r_parallel" unfolding r_parallel_def by simp lemma r_parallel: assumes "\x. eval r_phi [i, x] = eval f [x]" and "\x. eval r_phi [j, x] = eval g [x]" shows "eval f [x] \ \ eval g [x] \ \ eval r_parallel [i, j, x] \" and "eval f [x] \ \ eval g [x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval f [x]))" and "eval g [x] \ \ eval f [x] \ \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval g [x]))" and "eval f [x] \ \ eval g [x] \ \ eval r_parallel [i, j, x] \= prod_encode (0, the (eval f [x])) \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval g [x]))" proof - let ?cond = "Cn 4 r_le [Cn 4 r_pdec1 [r_both], r_constn 3 1]" define m where "m = Mn 3 ?cond" then have m: "r_parallel = Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]" unfolding r_parallel_def by simp from m_def have "recfn 3 m" by simp { assume "eval f [x] \ \ eval g [x] \" then have "\t. eval r_both [t, i, j, x] \= prod_encode (2, 0)" using assms r_both by simp then have "eval ?cond [t, i, j, x] \= 1" for t by simp then have "eval m [i, j, x] \" unfolding m_def using eval_Mn_diverg by simp then have "eval (Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]) [i, j, x] \" using `recfn 3 m` by simp then show "eval r_parallel [i, j, x] \" using m by simp next assume "eval f [x] \ \ eval g [x] \" then obtain vf vg where v: "eval f [x] \= vf" "eval g [x] \= vg" by auto then obtain tf where tf: "\t\tf. eval r_result1 [t, i, x] \= Suc vf" "\t= 0" using r_result1_converg' assms by metis from v obtain tg where tg: "\t\tg. eval r_result1 [t, j, x] \= Suc vg" "\t= 0" using r_result1_converg' assms by metis show "eval r_parallel [i, j, x] \= prod_encode (0, the (eval f [x])) \ eval r_parallel [i, j, x] \= prod_encode (1, the (eval g [x]))" proof (cases "tf \ tg") case True with tg(2) have j0: "\t= 0" by simp have *: "eval r_both [tf, i, j, x] \= prod_encode (0, the (eval f [x]))" using r_both(3) assms tf(1) by simp have "eval m [i, j, x] \= tf" unfolding m_def proof (rule eval_Mn_convergI) show "recfn (length [i, j, x]) (Mn 3 ?cond)" by simp have "eval (Cn 4 r_pdec1 [r_both]) [tf, i, j, x] \= 0" using * by simp then show "eval ?cond [tf, i, j, x] \= 0" by simp have "eval r_both [t, i, j, x] \= prod_encode (2, 0)" if "t < tf" for t using tf(2) r_both(2) assms that j0 by simp then have "eval ?cond [t, i, j, x] \= 1" if "t < tf" for t using that by simp then show "\y. y < tf \ eval ?cond [y, i, j, x] \\ 0" by simp qed moreover have "eval r_parallel [i, j, x] = eval (Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]) [i, j, x]" using m by simp ultimately have "eval r_parallel [i, j, x] = eval r_both [tf, i, j, x]" using `recfn 3 m` by simp with * have "eval r_parallel [i, j, x] \= prod_encode (0, the (eval f [x]))" by simp then show ?thesis by simp next case False with tf(2) have i0: "\t\tg. eval r_result1 [t, i, x] \= 0" by simp then have *: "eval r_both [tg, i, j, x] \= prod_encode (1, the (eval g [x]))" using assms r_both(4) tg(1) by auto have "eval m [i, j, x] \= tg" unfolding m_def proof (rule eval_Mn_convergI) show "recfn (length [i, j, x]) (Mn 3 ?cond)" by simp have "eval (Cn 4 r_pdec1 [r_both]) [tg, i, j, x] \= 1" using * by simp then show "eval ?cond [tg, i, j, x] \= 0" by simp have "eval r_both [t, i, j, x] \= prod_encode (2, 0)" if "t < tg" for t using tg(2) r_both(2) assms that i0 by simp then have "eval ?cond [t, i, j, x] \= 1" if "t < tg" for t using that by simp then show "\y. y < tg \ eval ?cond [y, i, j, x] \\ 0" by simp qed moreover have "eval r_parallel [i, j, x] = eval (Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]) [i, j, x]" using m by simp ultimately have "eval r_parallel [i, j, x] = eval r_both [tg, i, j, x]" using `recfn 3 m` by simp with * have "eval r_parallel [i, j, x] \= prod_encode (1, the (eval g [x]))" by simp then show ?thesis by simp qed next assume eval_fg: "eval g [x] \ \ eval f [x] \" then have i0: "\t. eval r_result1 [t, i, x] \= 0" using r_result1_diverg' assms by auto from eval_fg obtain v where "eval g [x] \= v" by auto then obtain t\<^sub>0 where t0: "\t\t\<^sub>0. eval r_result1 [t, j, x] \= Suc v" "\t0. eval r_result1 [t, j, x] \= 0" using r_result1_converg' assms by metis then have *: "eval r_both [t\<^sub>0, i, j, x] \= prod_encode (1, the (eval g [x]))" using r_both(4) assms i0 by simp have "eval m [i, j, x] \= t\<^sub>0" unfolding m_def proof (rule eval_Mn_convergI) show "recfn (length [i, j, x]) (Mn 3 ?cond)" by simp have "eval (Cn 4 r_pdec1 [r_both]) [t\<^sub>0, i, j, x] \= 1" using * by simp then show "eval ?cond [t\<^sub>0, i, j, x] \= 0" by simp have "eval r_both [t, i, j, x] \= prod_encode (2, 0)" if "t < t\<^sub>0" for t using t0(2) r_both(2) assms that i0 by simp then have "eval ?cond [t, i, j, x] \= 1" if "t < t\<^sub>0" for t using that by simp then show "\y. y < t\<^sub>0 \ eval ?cond [y, i, j, x] \\ 0" by simp qed moreover have "eval r_parallel [i, j, x] = eval (Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]) [i, j, x]" using m by simp ultimately have "eval r_parallel [i, j, x] = eval r_both [t\<^sub>0, i, j, x]" using `recfn 3 m` by simp with * show "eval r_parallel [i, j, x] \= prod_encode (1, the (eval g [x]))" by simp next assume eval_fg: "eval f [x] \ \ eval g [x] \" then have j0: "\t. eval r_result1 [t, j, x] \= 0" using r_result1_diverg' assms by auto from eval_fg obtain v where "eval f [x] \= v" by auto then obtain t\<^sub>0 where t0: "\t\t\<^sub>0. eval r_result1 [t, i, x] \= Suc v" "\t0. eval r_result1 [t, i, x] \= 0" using r_result1_converg' assms by metis then have *: "eval r_both [t\<^sub>0, i, j, x] \= prod_encode (0, the (eval f [x]))" using r_both(3) assms by blast have "eval m [i, j, x] \= t\<^sub>0" unfolding m_def proof (rule eval_Mn_convergI) show "recfn (length [i, j, x]) (Mn 3 ?cond)" by simp have "eval (Cn 4 r_pdec1 [r_both]) [t\<^sub>0, i, j, x] \= 0" using * by simp then show "eval ?cond [t\<^sub>0, i, j, x] \= 0" by simp have "eval r_both [t, i, j, x] \= prod_encode (2, 0)" if "t < t\<^sub>0" for t using t0(2) r_both(2) assms that j0 by simp then have "eval ?cond [t, i, j, x] \= 1" if "t < t\<^sub>0" for t using that by simp then show "\y. y < t\<^sub>0 \ eval ?cond [y, i, j, x] \\ 0" by simp qed moreover have "eval r_parallel [i, j, x] = eval (Cn 3 r_both [m, Id 3 0, Id 3 1, Id 3 2]) [i, j, x]" using m by simp ultimately have "eval r_parallel [i, j, x] = eval r_both [t\<^sub>0, i, j, x]" using `recfn 3 m` by simp with * show "eval r_parallel [i, j, x] \= prod_encode (0, the (eval f [x]))" by simp } qed end \ No newline at end of file