diff --git a/thys/Inductive_Inference/LIM_BC.thy b/thys/Inductive_Inference/LIM_BC.thy --- a/thys/Inductive_Inference/LIM_BC.thy +++ b/thys/Inductive_Inference/LIM_BC.thy @@ -1,1329 +1,1330 @@ section \LIM is a proper subset of BC\label{s:lim_bc}\ theory LIM_BC imports Lemma_R begin text \The proper inclusion of LIM in BC has been proved by Barzdin~\cite{b-ttlsf-74} (see also Case and Smith~\cite{cs-cicmii-83}). The proof constructs a class $V \in \mathrm{BC} - \mathrm{LIM}$ by diagonalization against all LIM strategies. Exploiting Lemma~R for LIM, we can assume that all such strategies are total functions. From the effective version of this lemma we derive a numbering @{term "\ \ \\<^sup>2"} such that for all $U \in \mathrm{LIM}$ there is an $i$ with $U\in \mathrm{LIM}_\varphi(\sigma_i)$. The idea behind $V$ is for every $i$ to construct a class $V_i$ of cardinality one or two such that $V_i \notin \mathrm{LIM}_\varphi(\sigma_i)$. It then follows that the union $V := \bigcup_i V_i$ cannot be learned by any $\sigma_i$ and thus $V \notin \mathrm{LIM}$. At the same time, the construction ensures that the functions in $V$ are ``predictable enough'' to be learnable in the BC sense. At the core is a process that maintains a state $(b, k)$ of a list $b$ of numbers and an index $k < |b|$ into this list. We imagine $b$ to be the prefix of the function being constructed, except for position $k$ where we imagine $b$ to have a ``gap''; that is, $b_k$ is not defined yet. Technically, we will always have $b_k = 0$, so $b$ also represents the prefix after the ``gap is filled'' with 0, whereas $b_{k:=1}$ represents the prefix where the gap is filled with 1. For every $i \in \mathbb{N}$, the process starts in state $(i0, 1)$ and computes the next state from a given state $(b,k)$ as follows: \begin{enumerate} \item if $ \sigma_i(b_{ subsection \Enumerating enough total strategies\ text \For the construction of $\sigma$ we need the function @{term r_limr} from the effective version of Lemma~R for LIM.\ definition "r_sigma \ Cn 2 r_phi [Cn 2 r_limr [Id 2 0], Id 2 1]" lemma r_sigma_recfn: "recfn 2 r_sigma" unfolding r_sigma_def using r_limr_recfn by simp lemma r_sigma: "eval r_sigma [i, x] = \ (the (eval r_limr [i])) x" unfolding r_sigma_def phi_def using r_sigma_recfn r_limr_total r_limr_recfn by simp lemma r_sigma_total: "total r_sigma" using r_sigma r_limr r_sigma_recfn totalI2[of r_sigma] by simp abbreviation sigma :: partial2 ("\") where "\ i x \ eval r_sigma [i, x]" lemma sigma: "\ i = \ (the (eval r_limr [i]))" using r_sigma by simp text \The numbering @{term \} does indeed enumerate enough total strategies for every LIM learning problem.\ lemma learn_lim_sigma: assumes "learn_lim \ U (\ i)" shows "learn_lim \ U (\ i)" using assms sigma r_limr by simp subsection \The diagonalization process\ text \The following function represents the process described above. It computes the next state from a given state $(b, k)$.\ definition "r_next \ Cn 1 r_ifeq [Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], r_pdec1], Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_take [r_pdec2, r_pdec1]], Cn 1 r_ifeq [Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_update [r_pdec1, r_pdec2, r_const 1]], Cn 1 r_sigma [Cn 1 r_hd [r_pdec1], Cn 1 r_take [r_pdec2, r_pdec1]], Cn 1 r_prod_encode [Cn 1 r_snoc [r_pdec1, Z], r_pdec2], Cn 1 r_prod_encode [Cn 1 r_snoc [Cn 1 r_update [r_pdec1, r_pdec2, r_const 1], Z], Cn 1 r_length [r_pdec1]]], Cn 1 r_prod_encode [Cn 1 r_snoc [r_pdec1, Z], Cn 1 r_length [r_pdec1]]]" lemma r_next_recfn: "recfn 1 r_next" unfolding r_next_def using r_sigma_recfn by simp text \The three conditions distinguished in @{term r_next} correspond to Steps 1, 2, and 3 of the process: hypothesis change when the gap is filled with 0; hypothesis change when the gap is filled with 1; or no hypothesis change either way.\ abbreviation "change_on_0 b k \ \ (e_hd b) b \ \ (e_hd b) (e_take k b)" abbreviation "change_on_1 b k \ \ (e_hd b) b = \ (e_hd b) (e_take k b) \ \ (e_hd b) (e_update b k 1) \ \ (e_hd b) (e_take k b)" abbreviation "change_on_neither b k \ \ (e_hd b) b = \ (e_hd b) (e_take k b) \ \ (e_hd b) (e_update b k 1) = \ (e_hd b) (e_take k b)" lemma change_conditions: obtains (on_0) "change_on_0 b k" | (on_1) "change_on_1 b k" | (neither) "change_on_neither b k" by auto lemma r_next: assumes "arg = prod_encode (b, k)" shows "change_on_0 b k \ eval r_next [arg] \= prod_encode (e_snoc b 0, e_length b)" and "change_on_1 b k \ eval r_next [arg] \= prod_encode (e_snoc (e_update b k 1) 0, e_length b)" and "change_on_neither b k \ eval r_next [arg] \= prod_encode (e_snoc b 0, k)" proof - let ?bhd = "Cn 1 r_hd [r_pdec1]" let ?bup = "Cn 1 r_update [r_pdec1, r_pdec2, r_const 1]" let ?bk = "Cn 1 r_take [r_pdec2, r_pdec1]" let ?bap = "Cn 1 r_snoc [r_pdec1, Z]" let ?len = "Cn 1 r_length [r_pdec1]" let ?thenthen = "Cn 1 r_prod_encode [?bap, r_pdec2]" let ?thenelse = "Cn 1 r_prod_encode [Cn 1 r_snoc [?bup, Z], ?len]" let ?else = "Cn 1 r_prod_encode [?bap, ?len]" have bhd: "eval ?bhd [arg] \= e_hd b" using assms by simp have bup: "eval ?bup [arg] \= e_update b k 1" using assms by simp have bk: "eval ?bk [arg] \= e_take k b" using assms by simp have bap: "eval ?bap [arg] \= e_snoc b 0" using assms by simp have len: "eval ?len [arg] \= e_length b" using assms by simp have else_: "eval ?else [arg] \= prod_encode (e_snoc b 0, e_length b)" using bap len by simp have thenthen: "eval ?thenthen [arg] \= prod_encode (e_snoc b 0, k)" using bap assms by simp have thenelse: "eval ?thenelse [arg] \= prod_encode (e_snoc (e_update b k 1) 0, e_length b)" using bup len by simp have then_: "eval (Cn 1 r_ifeq [Cn 1 r_sigma [?bhd, ?bup], Cn 1 r_sigma [?bhd, ?bk], ?thenthen, ?thenelse]) [arg] \= (if the (\ (e_hd b) (e_update b k 1)) = the (\ (e_hd b) (e_take k b)) then prod_encode (e_snoc b 0, k) else prod_encode (e_snoc (e_update b k 1) 0, e_length b))" (is "eval ?then [arg] \= ?then_eval") using bhd bup bk thenthen thenelse r_sigma r_sigma_recfn r_limr R1_imp_total1 by simp have *: "eval r_next [arg] \= (if the (\ (e_hd b) b) = the (\ (e_hd b) (e_take k b)) then ?then_eval else prod_encode (e_snoc b 0, e_length b))" unfolding r_next_def using bhd bk then_ else_ r_sigma r_sigma_recfn r_limr R1_imp_total1 assms by simp have r_sigma_neq: "eval r_sigma [x\<^sub>1, y\<^sub>1] \ eval r_sigma [x\<^sub>2, y\<^sub>2] \ the (eval r_sigma [x\<^sub>1, y\<^sub>1]) \ the (eval r_sigma [x\<^sub>2, y\<^sub>2])" for x\<^sub>1 y\<^sub>1 x\<^sub>2 y\<^sub>2 using r_sigma r_limr totalE[OF r_sigma_total r_sigma_recfn] r_sigma_recfn r_sigma_total by (metis One_nat_def Suc_1 length_Cons list.size(3) option.expand) { assume "change_on_0 b k" then show "eval r_next [arg] \= prod_encode (e_snoc b 0, e_length b)" using * r_sigma_neq by simp next assume "change_on_1 b k" then show "eval r_next [arg] \= prod_encode (e_snoc (e_update b k 1) 0, e_length b)" using * r_sigma_neq by simp next assume "change_on_neither b k" then show "eval r_next [arg] \= prod_encode (e_snoc b 0, k)" using * r_sigma_neq by simp } qed lemma r_next_total: "total r_next" proof (rule totalI1) show "recfn 1 r_next" using r_next_recfn by simp show "eval r_next [x] \" for x proof - obtain b k where "x = prod_encode (b, k)" using prod_encode_pdec'[of x] by metis then show ?thesis using r_next by fast qed qed text \The next function computes the state of the process after any number of iterations.\ definition "r_state \ Pr 1 (Cn 1 r_prod_encode [Cn 1 r_snoc [Cn 1 r_singleton_encode [Id 1 0], Z], r_const 1]) (Cn 3 r_next [Id 3 1])" lemma r_state_recfn: "recfn 2 r_state" unfolding r_state_def using r_next_recfn by simp lemma r_state_at_0: "eval r_state [0, i] \= prod_encode (list_encode [i, 0], 1)" proof - let ?f = "Cn 1 r_prod_encode [Cn 1 r_snoc [Cn 1 r_singleton_encode [Id 1 0], Z], r_const 1]" have "eval r_state [0, i] = eval ?f [i]" unfolding r_state_def using r_next_recfn by simp also have "... \= prod_encode (list_encode [i, 0], 1)" by (simp add: list_decode_singleton) finally show ?thesis . qed lemma r_state_total: "total r_state" unfolding r_state_def using r_next_recfn totalE[OF r_next_total r_next_recfn] totalI3[of "Cn 3 r_next [Id 3 1]"] by (intro Pr_total) auto text \We call the components of a state $(b, k)$ the \emph{block} $b$ and the \emph{gap} $k$.\ definition block :: "nat \ nat \ nat" where "block i t \ pdec1 (the (eval r_state [t, i]))" definition gap :: "nat \ nat \ nat" where "gap i t \ pdec2 (the (eval r_state [t, i]))" lemma state_at_0: "block i 0 = list_encode [i, 0]" "gap i 0 = 1" unfolding block_def gap_def r_state_at_0 by simp_all text \Some lemmas describing the behavior of blocks and gaps in one iteration of the process:\ lemma state_Suc: assumes "b = block i t" and "k = gap i t" shows "block i (Suc t) = pdec1 (the (eval r_next [prod_encode (b, k)]))" and "gap i (Suc t) = pdec2 (the (eval r_next [prod_encode (b, k)]))" proof - have "eval r_state [Suc t, i] = eval (Cn 3 r_next [Id 3 1]) [t, the (eval r_state [t, i]), i]" using r_state_recfn r_next_recfn totalE[OF r_state_total r_state_recfn, of "[t, i]"] by (simp add: r_state_def) also have "... = eval r_next [the (eval r_state [t, i])]" using r_next_recfn by simp also have "... = eval r_next [prod_encode (b, k)]" using assms block_def gap_def by simp finally have "eval r_state [Suc t, i] = eval r_next [prod_encode (b, k)]" . then show "block i (Suc t) = pdec1 (the (eval r_next [prod_encode (b, k)]))" "gap i (Suc t) = pdec2 (the (eval r_next [prod_encode (b, k)]))" by (simp add: block_def, simp add: gap_def) qed lemma gap_Suc: assumes "b = block i t" and "k = gap i t" shows "change_on_0 b k \ gap i (Suc t) = e_length b" and "change_on_1 b k \ gap i (Suc t) = e_length b" and "change_on_neither b k\ gap i (Suc t) = k" using assms r_next state_Suc by simp_all lemma block_Suc: assumes "b = block i t" and "k = gap i t" shows "change_on_0 b k \ block i (Suc t) = e_snoc b 0" and "change_on_1 b k \ block i (Suc t) = e_snoc (e_update b k 1) 0" and "change_on_neither b k\ block i (Suc t) = e_snoc b 0" using assms r_next state_Suc by simp_all text \Non-gap positions in the block remain unchanged after an iteration.\ lemma block_stable: assumes "j < e_length (block i t)" and "j \ gap i t" shows "e_nth (block i t) j = e_nth (block i (Suc t)) j" proof - from change_conditions[of "block i t" "gap i t"] show ?thesis using assms block_Suc gap_Suc by (cases, (simp_all add: nth_append)) qed text \Next are some properties of @{term block} and @{term gap}.\ lemma gap_in_block: "gap i t < e_length (block i t)" proof (induction t) case 0 then show ?case by (simp add: state_at_0) next case (Suc t) with change_conditions[of "block i t" "gap i t"] show ?case proof (cases) case on_0 then show ?thesis by (simp add: block_Suc(1) gap_Suc(1)) next case on_1 then show ?thesis by (simp add: block_Suc(2) gap_Suc(2)) next case neither then show ?thesis using Suc.IH block_Suc(3) gap_Suc(3) by force qed qed lemma length_block: "e_length (block i t) = Suc (Suc t)" proof (induction t) case 0 then show ?case by (simp add: state_at_0) next case (Suc t) with change_conditions[of "block i t" "gap i t"] show ?case by (cases, simp_all add: block_Suc gap_Suc) qed lemma gap_gr0: "gap i t > 0" proof (induction t) case 0 then show ?case by (simp add: state_at_0) next case (Suc t) with change_conditions[of "block i t" "gap i t"] show ?case using length_block by (cases, simp_all add: block_Suc gap_Suc) qed lemma hd_block: "e_hd (block i t) = i" proof (induction t) case 0 then show ?case by (simp add: state_at_0) next case (Suc t) from change_conditions[of "block i t" "gap i t"] show ?case proof (cases) case on_0 then show ?thesis using Suc block_Suc(1) length_block by (metis e_hd_snoc gap_Suc(1) gap_gr0) next case on_1 let ?b = "block i t" and ?k = "gap i t" have "?k > 0" using gap_gr0 Suc by simp then have "e_nth (e_update ?b ?k 1) 0 = e_nth ?b 0" by simp then have *: "e_hd (e_update ?b ?k 1) = e_hd ?b" using e_hd_nth0 gap_Suc(2)[of _ i t] gap_gr0 on_1 by (metis e_length_update) from on_1 have "block i (Suc t) = e_snoc (e_update ?b ?k 1) 0" by (simp add: block_Suc(2)) then show ?thesis using e_hd_0 e_hd_snoc Suc length_block \?k > 0\ * by (metis e_length_update gap_Suc(2) gap_gr0 on_1) next case neither - then show ?thesis using Suc block_Suc(3) length_block by simp + then show ?thesis + by (metis Suc block_stable e_hd_nth0 gap_gr0 length_block not_gr0 zero_less_Suc) qed qed text \Formally, a block always ends in zero, even if it ends in a gap.\ lemma last_block: "e_nth (block i t) (gap i t) = 0" proof (induction t) case 0 then show ?case by (simp add: state_at_0) next case (Suc t) from change_conditions[of "block i t" "gap i t"] show ?case proof cases case on_0 then show ?thesis using Suc by (simp add: block_Suc(1) gap_Suc(1)) next case on_1 then show ?thesis using Suc by (simp add: block_Suc(2) gap_Suc(2) nth_append) next case neither then have "block i (Suc t) = e_snoc (block i t) 0" "gap i (Suc t) = gap i t" by (simp_all add: gap_Suc(3) block_Suc(3)) then show ?thesis using Suc gap_in_block by (simp add: nth_append) qed qed lemma gap_le_Suc: "gap i t \ gap i (Suc t)" using change_conditions[of "block i t" "gap i t"] gap_Suc gap_in_block less_imp_le[of "gap i t" "e_length (block i t)"] by (cases) simp_all lemma gap_monotone: assumes "t\<^sub>1 \ t\<^sub>2" shows "gap i t\<^sub>1 \ gap i t\<^sub>2" proof - have "gap i t\<^sub>1 \ gap i (t\<^sub>1 + j)" for j proof (induction j) case 0 then show ?case by simp next case (Suc j) then show ?case using gap_le_Suc dual_order.trans by fastforce qed then show ?thesis using assms le_Suc_ex by blast qed text \We need some lemmas relating the shape of the next state to the hypothesis change conditions in Steps 1, 2, and 3.\ lemma state_change_on_neither: assumes "gap i (Suc t) = gap i t" shows "change_on_neither (block i t) (gap i t)" and "block i (Suc t) = e_snoc (block i t) 0" proof - let ?b = "block i t" and ?k = "gap i t" have "?k < e_length ?b" using gap_in_block by simp from change_conditions[of ?b ?k] show "change_on_neither (block i t) (gap i t)" proof (cases) case on_0 then show ?thesis using \?k < e_length ?b\ assms gap_Suc(1) by auto next case on_1 then show ?thesis using assms gap_Suc(2) by auto next case neither then show ?thesis by simp qed then show "block i (Suc t) = e_snoc (block i t) 0" using block_Suc(3) by simp qed lemma state_change_on_either: assumes "gap i (Suc t) \ gap i t" shows "\ change_on_neither (block i t) (gap i t)" and "gap i (Suc t) = e_length (block i t)" proof - let ?b = "block i t" and ?k = "gap i t" show "\ change_on_neither (block i t) (gap i t)" proof assume "change_on_neither (block i t) (gap i t)" then have "gap i (Suc t) = ?k" by (simp add: gap_Suc(3)) with assms show False by simp qed then show "gap i (Suc t) = e_length (block i t)" using gap_Suc(1) gap_Suc(2) by blast qed text \Next up is the definition of $\tau$. In every iteration the process determines $\tau_i(x)$ for some $x$ either by appending 0 to the current block $b$, or by filling the current gap $k$. In the former case, the value is determined for $x = |b|$, in the latter for $x = k$.\ text \For $i$ and $x$ the function @{term r_dettime} computes in which iteration the process for $i$ determines the value $\tau_i(x)$. This is the first iteration in which the block is long enough to contain position $x$ and in which $x$ is not the gap. If $\tau_i(x)$ is never determined, because Case~2 is reached with $k = x$, then @{term r_dettime} diverges.\ abbreviation determined :: "nat \ nat \ bool" where "determined i x \ \t. x < e_length (block i t) \ x \ gap i t" lemma determined_0: "determined i 0" using gap_gr0[of i 0] gap_in_block[of i 0] by force definition "r_dettime \ Mn 2 (Cn 3 r_and [Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]], Cn 3 r_neq [Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]]])" lemma r_dettime_recfn: "recfn 2 r_dettime" unfolding r_dettime_def using r_state_recfn by simp abbreviation dettime :: partial2 where "dettime i x \ eval r_dettime [i, x]" lemma r_dettime: shows "determined i x \ dettime i x \= (LEAST t. x < e_length (block i t) \ x \ gap i t)" and "\ determined i x \ dettime i x \" proof - define f where "f = (Cn 3 r_and [Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]], Cn 3 r_neq [Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]]])" then have "r_dettime = Mn 2 f" unfolding f_def r_dettime_def by simp have "recfn 3 f" unfolding f_def using r_state_recfn by simp then have "total f" unfolding f_def using Cn_total r_state_total Mn_free_imp_total by simp have f: "eval f [t, i, x] \= (if x < e_length (block i t) \ x \ gap i t then 0 else 1)" for t proof - let ?b = "Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]" let ?k = "Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]" have "eval ?b [t, i, x] \= pdec1 (the (eval r_state [t, i]))" using r_state_recfn r_state_total by simp then have b: "eval ?b [t, i, x] \= block i t" using block_def by simp have "eval ?k [t, i, x] \= pdec2 (the (eval r_state [t, i]))" using r_state_recfn r_state_total by simp then have k: "eval ?k [t, i, x] \= gap i t" using gap_def by simp have "eval (Cn 3 r_neq [Id 3 2, Cn 3 r_pdec2 [Cn 3 r_state [Id 3 0, Id 3 1]]]) [t, i, x] \= (if x \ gap i t then 0 else 1)" using b k r_state_recfn r_state_total by simp moreover have "eval (Cn 3 r_less [Id 3 2, Cn 3 r_length [Cn 3 r_pdec1 [Cn 3 r_state [Id 3 0, Id 3 1]]]]) [t, i, x] \= (if x < e_length (block i t) then 0 else 1)" using b k r_state_recfn r_state_total by simp ultimately show ?thesis unfolding f_def using b k r_state_recfn r_state_total by simp qed { assume "determined i x" with f have "\t. eval f [t, i, x] \= 0" by simp then have "dettime i x \= (LEAST t. eval f [t, i, x] \= 0)" using \total f\ \r_dettime = Mn 2 f\ r_dettime_recfn \recfn 3 f\ eval_Mn_total[of 2 f "[i, x]"] by simp then show "dettime i x \= (LEAST t. x < e_length (block i t) \ x \ gap i t)" using f by simp next assume "\ determined i x" with f have "\ (\t. eval f [t, i, x] \= 0)" by simp then have "dettime i x \" using \total f\ \r_dettime = Mn 2 f\ r_dettime_recfn \recfn 3 f\ eval_Mn_total[of 2 f "[i, x]"] by simp with f show "dettime i x \" by simp } qed lemma r_dettimeI: assumes "x < e_length (block i t) \ x \ gap i t" and "\T. x < e_length (block i T) \ x \ gap i T \ t \ T" shows "dettime i x \= t" proof - let ?P = "\T. x < e_length (block i T) \ x \ gap i T" have "determined i x" using assms(1) by auto moreover have "Least ?P = t" using assms Least_equality[of ?P t] by simp ultimately show ?thesis using r_dettime by simp qed lemma r_dettime_0: "dettime i 0 \= 0" using r_dettimeI[of _ i 0] determined_0 gap_gr0[of i 0] gap_in_block[of i 0] by fastforce text \Computing the value of $\tau_i(x)$ works by running the process @{term r_state} for @{term "dettime i x"} iterations and taking the value at index $x$ of the resulting block.\ definition "r_tau \ Cn 2 r_nth [Cn 2 r_pdec1 [Cn 2 r_state [r_dettime, Id 2 0]], Id 2 1]" lemma r_tau_recfn: "recfn 2 r_tau" unfolding r_tau_def using r_dettime_recfn r_state_recfn by simp abbreviation tau :: partial2 ("\") where "\ i x \ eval r_tau [i, x]" lemma tau_in_P2: "\ \ \

\<^sup>2" using r_tau_recfn by auto lemma tau_diverg: assumes "\ determined i x" shows "\ i x \" unfolding r_tau_def using assms r_dettime r_dettime_recfn r_state_recfn by simp lemma tau_converg: assumes "determined i x" shows "\ i x \= e_nth (block i (the (dettime i x))) x" proof - from assms obtain t where t: "dettime i x \= t" using r_dettime(1) by blast then have "eval (Cn 2 r_state [r_dettime, Id 2 0]) [i, x] = eval r_state [t, i]" using r_state_recfn r_dettime_recfn by simp moreover have "eval r_state [t, i] \" using r_state_total r_state_recfn by simp ultimately have "eval (Cn 2 r_pdec1 [Cn 2 r_state [r_dettime, Id 2 0]]) [i, x] = eval r_pdec1 [the (eval r_state [t, i])]" using r_state_recfn r_dettime_recfn by simp then show ?thesis unfolding r_tau_def using r_state_recfn r_dettime_recfn t block_def by simp qed lemma tau_converg': assumes "dettime i x \= t" shows "\ i x \= e_nth (block i t) x" using assms tau_converg[of x i] r_dettime(2)[of x i] by fastforce lemma tau_at_0: "\ i 0 \= i" proof - have "\ i 0 \= e_nth (block i 0) 0" using tau_converg'[OF r_dettime_0] by simp then show ?thesis using block_def by (simp add: r_state_at_0) qed lemma state_unchanged: assumes "gap i t - 1 \ y" and "y \ t" shows "gap i t = gap i y" proof - have "gap i t = gap i (gap i t - 1)" proof (induction t) case 0 then show ?case by (simp add: gap_def r_state_at_0) next case (Suc t) show ?case proof (cases "gap i (Suc t) = t + 2") case True then show ?thesis by simp next case False then show ?thesis using Suc state_change_on_either(2) length_block by force qed qed moreover have "gap i (gap i t - 1) \ gap i y" using assms(1) gap_monotone by simp moreover have "gap i y \ gap i t" using assms(2) gap_monotone by simp ultimately show ?thesis by simp qed text \The values of the non-gap indices $x$ of every block created in the diagonalization process equal $\tau_i(x)$.\ lemma tau_eq_state: assumes "j < e_length (block i t)" and "j \ gap i t" shows "\ i j \= e_nth (block i t) j" using assms proof (induction t) case 0 then have "j = 0" using gap_gr0[of i 0] gap_in_block[of i 0] length_block[of i 0] by simp then have "\ (e_hd (block i t)) j \= e_nth (block i (the (dettime i 0))) 0" using determined_0 tau_converg hd_block by simp then have "\ (e_hd (block i t)) j \= e_nth (block i 0) 0" using r_dettime_0 by simp then show ?case using \j = 0\ r_dettime_0 tau_converg' by simp next case (Suc t) let ?b = "block i t" let ?bb = "block i (Suc t)" let ?k = "gap i t" let ?kk = "gap i (Suc t)" show ?case proof (cases "?kk = ?k") case kk_eq_k: True then have bb_b0: "?bb = e_snoc ?b 0" using state_change_on_neither by simp show "\ i j \= e_nth ?bb j" proof (cases "j < e_length ?b") case True then have "e_nth ?bb j = e_nth ?b j" using bb_b0 by (simp add: nth_append) moreover have "j \ ?k" using Suc kk_eq_k by simp ultimately show ?thesis using Suc True by simp next case False then have j: "j = e_length ?b" using Suc.prems(1) length_block by auto then have "e_nth ?bb j = 0" using bb_b0 by simp have "dettime i j \= Suc t" proof (rule r_dettimeI) show "j < e_length ?bb \ j \ ?kk" using Suc.prems(1,2) by linarith show "\T. j < e_length (block i T) \ j \ gap i T \ Suc t \ T" using length_block j by simp qed with tau_converg' show ?thesis by simp qed next case False then have kk_lenb: "?kk = e_length ?b" using state_change_on_either by simp then show ?thesis proof (cases "j = ?k") case j_eq_k: True have "dettime i j \= Suc t" proof (rule r_dettimeI) show "j < e_length ?bb \ j \ ?kk" using Suc.prems(1,2) by simp show "Suc t \ T" if "j < e_length (block i T) \ j \ gap i T" for T proof (rule ccontr) assume "\ (Suc t \ T)" then have "T < Suc t" by simp then show False proof (cases "T < ?k - 1") case True then have "e_length (block i T) = T + 2" using length_block by simp then have "e_length (block i T) < ?k + 1" using True by simp then have "e_length (block i T) \ ?k" by simp then have "e_length (block i T) \ j" using j_eq_k by simp then show False using that by simp next case False then have "?k - 1 \ T" and "T \ t" using \T < Suc t\ by simp_all with state_unchanged have "gap i t = gap i T" by blast then show False using j_eq_k that by simp qed qed qed then show ?thesis using tau_converg' by simp next case False then have "j < e_length ?b" using kk_lenb Suc.prems(1,2) length_block by auto then show ?thesis using Suc False block_stable by fastforce qed qed qed lemma tau_eq_state': assumes "j < t + 2" and " j \ gap i t" shows "\ i j \= e_nth (block i t) j" using assms tau_eq_state length_block by simp text \We now consider the two cases described in the proof sketch. In Case~2 there is a gap that never gets filled, or equivalently there is a rightmost gap.\ abbreviation "case_two i \ (\t. \T. gap i T \ gap i t)" abbreviation "case_one i \ \ case_two i" text \Another characterization of Case~2 is that from some iteration on only @{term change_on_neither} holds.\ lemma case_two_iff_forever_neither: "case_two i \ (\t. \T\t. change_on_neither (block i T) (gap i T))" proof assume "\t. \T\t. change_on_neither (block i T) (gap i T)" then obtain t where t: "\T\t. change_on_neither (block i T) (gap i T)" by auto have "(gap i T) \ (gap i t)" for T proof (cases "T \ t") case True then show ?thesis using gap_monotone by simp next case False then show ?thesis proof (induction T) case 0 then show ?case by simp next case (Suc T) with t have "change_on_neither ((block i T)) ((gap i T))" by simp then show ?case using Suc.IH state_change_on_either(1)[of i T] gap_monotone[of T t i] by metis qed qed then show "\t. \T. gap i T \ gap i t" by auto next assume "\t. \T. gap i T \ gap i t" then obtain t where t: "\T. gap i T \ gap i t" by auto have "change_on_neither (block i T) (gap i T)" if "T\t" for T proof - have T: "(gap i T) \ (gap i t)" using gap_monotone that by simp show ?thesis proof (rule ccontr) assume "\ change_on_neither (block i T) (gap i T)" then have "change_on_0 (block i T) (gap i T) \ change_on_1 (block i T) (gap i T)" by simp then have "gap i (Suc T) > gap i T" using gap_le_Suc[of i] state_change_on_either(2)[of i] state_change_on_neither(1)[of i] dual_order.strict_iff_order by blast with T have "gap i (Suc T) > gap i t" by simp with t show False using not_le by auto qed qed then show "\t. \T\t. change_on_neither (block i T) (gap i T)" by auto qed text \In Case~1, $\tau_i$ is total.\ lemma case_one_tau_total: assumes "case_one i" shows "\ i x \" proof (cases "x = gap i x") case True from assms have "\t. \T. gap i T > gap i t" using le_less_linear gap_def[of i x] by blast then obtain T where T: "gap i T > gap i x" by auto then have "T > x" using gap_monotone leD le_less_linear by blast then have "x < T + 2" by simp moreover from T True have "x \ gap i T" by simp ultimately show ?thesis using tau_eq_state' by simp next case False moreover have "x < x + 2" by simp ultimately show ?thesis using tau_eq_state' by blast qed text \In Case~2, $\tau_i$ is undefined only at the gap that never gets filled.\ lemma case_two_tau_not_quite_total: assumes "\T. gap i T \ gap i t" shows "\ i (gap i t) \" and "x \ gap i t \ \ i x \" proof - let ?k = "gap i t" have "\ determined i ?k" proof assume "determined i ?k" then obtain T where T: "?k < e_length (block i T) \ ?k \ gap i T" by auto with assms have snd_le: "gap i T < ?k" by (simp add: dual_order.strict_iff_order) then have "T < t" using gap_monotone by (metis leD le_less_linear) from T length_block have "?k < T + 2" by simp moreover have "?k \ T + 1" using T state_change_on_either(2) \T < t\ state_unchanged by (metis Suc_eq_plus1 Suc_leI add_diff_cancel_right' le_add1 nat_neq_iff) ultimately have "?k \ T" by simp then have "gap i T = gap i ?k" using state_unchanged[of i T "?k"] \?k < T + 2\ snd_le by simp then show False by (metis diff_le_self state_unchanged leD nat_le_linear gap_monotone snd_le) qed with tau_diverg show "\ i ?k \" by simp assume "x \ ?k" show "\ i x \" proof (cases "x < t + 2") case True with \x \ ?k\ tau_eq_state' show ?thesis by simp next case False then have "gap i x = ?k" using assms by (simp add: dual_order.antisym gap_monotone) with \x \ ?k\ have "x \ gap i x" by simp then show ?thesis using tau_eq_state'[of x x] by simp qed qed lemma case_two_tau_almost_total: assumes "\t. \T. gap i T \ gap i t" (is "\t. ?P t") shows "\ i (gap i (Least ?P)) \" and "x \ gap i (Least ?P) \ \ i x \" proof - from assms have "?P (Least ?P)" using LeastI_ex[of ?P] by simp then show "\ i (gap i (Least ?P)) \" and "x \ gap i (Least ?P) \ \ i x \" using case_two_tau_not_quite_total by simp_all qed text \Some more properties of $\tau$.\ lemma init_tau_gap: "(\ i) \ (gap i t - 1) = e_take (gap i t) (block i t)" proof (intro initI') show 1: "e_length (e_take (gap i t) (block i t)) = Suc (gap i t - 1)" proof - have "gap i t > 0" using gap_gr0 by simp moreover have "gap i t < e_length (block i t)" using gap_in_block by simp ultimately have "e_length (e_take (gap i t) (block i t)) = gap i t" by simp then show ?thesis using gap_gr0 by simp qed show "\ i x \= e_nth (e_take (gap i t) (block i t)) x" if "x < Suc (gap i t - 1)" for x proof - have x_le: "x < gap i t" using that gap_gr0 by simp then have "x < e_length (block i t)" using gap_in_block less_trans by blast then have *: "\ i x \= e_nth (block i t) x" using x_le tau_eq_state by auto have "x < e_length (e_take (gap i t) (block i t))" using x_le 1 by simp then have "e_nth (block i t) x = e_nth (e_take (gap i t) (block i t)) x" using x_le by simp then show ?thesis using * by simp qed qed lemma change_on_0_init_tau: assumes "change_on_0 (block i t) (gap i t)" shows "(\ i) \ (t + 1) = block i t" proof (intro initI') let ?b = "block i t" and ?k = "gap i t" show "e_length (block i t) = Suc (t + 1)" using length_block by simp show "(\ i) x \= e_nth (block i t) x" if "x < Suc (t + 1)" for x proof (cases "x = ?k") case True have "gap i (Suc t) = e_length ?b" and b: "block i (Suc t) = e_snoc ?b 0" using gap_Suc(1) block_Suc(1) assms by simp_all then have "x < e_length (block i (Suc t))" "x \ gap i (Suc t)" using that length_block by simp_all then have "\ i x \= e_nth (block i (Suc t)) x" using tau_eq_state by simp then show ?thesis using that assms b by (simp add: nth_append) next case False then show ?thesis using that assms tau_eq_state' by simp qed qed lemma change_on_0_hyp_change: assumes "change_on_0 (block i t) (gap i t)" shows "\ i ((\ i) \ (t + 1)) \ \ i ((\ i) \ (gap i t - 1))" using assms hd_block init_tau_gap change_on_0_init_tau by simp lemma change_on_1_init_tau: assumes "change_on_1 (block i t) (gap i t)" shows "(\ i) \ (t + 1) = e_update (block i t) (gap i t) 1" proof (intro initI') let ?b = "block i t" and ?k = "gap i t" show "e_length (e_update ?b ?k 1) = Suc (t + 1)" using length_block by simp show "(\ i) x \= e_nth (e_update ?b ?k 1) x" if "x < Suc (t + 1)" for x proof (cases "x = ?k") case True have "gap i (Suc t) = e_length ?b" and b: "block i (Suc t) = e_snoc (e_update ?b ?k 1) 0" using gap_Suc(2) block_Suc(2) assms by simp_all then have "x < e_length (block i (Suc t))" "x \ gap i (Suc t)" using that length_block by simp_all then have "\ i x \= e_nth (block i (Suc t)) x" using tau_eq_state by simp then show ?thesis using that assms b nth_append by (simp add: nth_append) next case False then show ?thesis using that assms tau_eq_state' by simp qed qed lemma change_on_1_hyp_change: assumes "change_on_1 (block i t) (gap i t)" shows "\ i ((\ i) \ (t + 1)) \ \ i ((\ i) \ (gap i t - 1))" using assms hd_block init_tau_gap change_on_1_init_tau by simp lemma change_on_either_hyp_change: assumes "\ change_on_neither (block i t) (gap i t)" shows "\ i ((\ i) \ (t + 1)) \ \ i ((\ i) \ (gap i t - 1))" using assms change_on_0_hyp_change change_on_1_hyp_change by auto lemma filled_gap_0_init_tau: assumes "f\<^sub>0 = (\ i)((gap i t):=Some 0)" shows "f\<^sub>0 \ (t + 1) = block i t" proof (intro initI') show len: "e_length (block i t) = Suc (t + 1)" using assms length_block by auto show "f\<^sub>0 x \= e_nth (block i t) x" if "x < Suc (t + 1)" for x proof (cases "x = gap i t") case True then show ?thesis using assms last_block by auto next case False then show ?thesis using assms len tau_eq_state that by auto qed qed lemma filled_gap_1_init_tau: assumes "f\<^sub>1 = (\ i)((gap i t):=Some 1)" shows "f\<^sub>1 \ (t + 1) = e_update (block i t) (gap i t) 1" proof (intro initI') show len: "e_length (e_update (block i t) (gap i t) 1) = Suc (t + 1)" using e_length_update length_block by simp show "f\<^sub>1 x \= e_nth (e_update (block i t) (gap i t) 1) x" if "x < Suc (t + 1)" for x proof (cases "x = gap i t") case True moreover have "gap i t < e_length (block i t)" using gap_in_block by simp ultimately show ?thesis using assms by simp next case False then show ?thesis using assms len tau_eq_state that by auto qed qed subsection \The separating class\ text \Next we define the sets $V_i$ from the introductory proof sketch (page~\pageref{s:lim_bc}).\ definition V_bclim :: "nat \ partial1 set" where "V_bclim i \ if case_two i then let k = gap i (LEAST t. \T. gap i T \ gap i t) in {(\ i)(k:=Some 0), (\ i)(k:=Some 1)} else {\ i}" lemma V_subseteq_R1: "V_bclim i \ \" proof (cases "case_two i") case True define k where "k = gap i (LEAST t. \T. gap i T \ gap i t)" have "\ i \ \

" using tau_in_P2 P2_proj_P1 by auto then have "(\ i)(k:=Some 0) \ \

" and "(\ i)(k:=Some 1) \ \

" using P1_update_P1 by simp_all moreover have "total1 ((\ i)(k:=Some v))" for v using case_two_tau_almost_total(2)[OF True] k_def total1_def by simp ultimately have "(\ i)(k:=Some 0) \ \" and "(\ i)(k:=Some 1) \ \" using P1_total_imp_R1 by simp_all moreover have "V_bclim i = {(\ i)(k:=Some 0), (\ i)(k:=Some 1)}" using True V_bclim_def k_def by (simp add: Let_def) ultimately show ?thesis by simp next case False have "V_bclim i = {\ i}" unfolding V_bclim_def by (simp add: False) moreover have "\ i \ \" using total1I case_one_tau_total[OF False] tau_in_P2 P2_proj_P1[of \] P1_total_imp_R1 by simp ultimately show ?thesis by simp qed lemma case_one_imp_gap_unbounded: assumes "case_one i" shows "\t. gap i t - 1 > n" proof (induction n) case 0 then show ?case using assms gap_gr0[of i] state_at_0(2)[of i] by (metis diff_is_0_eq gr_zeroI) next case (Suc n) then obtain t where t: "gap i t - 1 > n" by auto moreover from assms have "\t. \T. gap i T > gap i t" using leI by blast ultimately obtain T where "gap i T > gap i t" by auto then have "gap i T - 1 > gap i t - 1" using gap_gr0[of i] by (simp add: Suc_le_eq diff_less_mono) with t have "gap i T - 1 > Suc n" by simp then show ?case by auto qed lemma case_one_imp_not_learn_lim_V: assumes "case_one i" shows "\ learn_lim \ (V_bclim i) (\ i)" proof - have V_bclim: "V_bclim i = {\ i}" using assms V_bclim_def by (auto simp add: Let_def) have "\m\<^sub>1>n. \m\<^sub>2>n. (\ i) ((\ i) \ m\<^sub>1) \ (\ i) ((\ i) \ m\<^sub>2)" for n proof - obtain t where t: "gap i t - 1 > n" using case_one_imp_gap_unbounded[OF assms] by auto moreover have "\t. \T\t. \ change_on_neither (block i T) (gap i T)" using assms case_two_iff_forever_neither by blast ultimately obtain T where T: "T \ t" "\ change_on_neither (block i T) (gap i T)" by auto then have "(\ i) ((\ i) \ (T + 1)) \ (\ i) ((\ i) \ (gap i T - 1))" using change_on_either_hyp_change by simp moreover have "gap i T - 1 > n" using t T(1) gap_monotone by (simp add: diff_le_mono less_le_trans) moreover have "T + 1 > n" proof - have "gap i T - 1 \ T" using gap_in_block length_block by (simp add: le_diff_conv less_Suc_eq_le) then show ?thesis using \gap i T - 1 > n\ by simp qed ultimately show ?thesis by auto qed with infinite_hyp_changes_not_Lim V_bclim show ?thesis by simp qed lemma case_two_imp_not_learn_lim_V: assumes "case_two i" shows "\ learn_lim \ (V_bclim i) (\ i)" proof - let ?P = "\t. \T. (gap i T) \ (gap i t)" let ?t = "LEAST t. ?P t" let ?k = "gap i ?t" let ?b = "e_take ?k (block i ?t)" have t: "\T. gap i T \ gap i ?t" using assms LeastI_ex[of ?P] by simp then have neither: "\T\?t. change_on_neither (block i T) (gap i T)" using gap_le_Suc gap_monotone state_change_on_neither(1) by (metis (no_types, lifting) antisym) have gap_T: "\T\?t. gap i T = ?k" using t gap_monotone antisym_conv by blast define f\<^sub>0 where "f\<^sub>0 = (\ i)(?k:=Some 0)" define f\<^sub>1 where "f\<^sub>1 = (\ i)(?k:=Some 1)" show ?thesis proof (rule same_hyp_for_two_not_Lim) show "f\<^sub>0 \ V_bclim i" and "f\<^sub>1 \ V_bclim i" using assms V_bclim_def f\<^sub>0_def f\<^sub>1_def by (simp_all add: Let_def) show "f\<^sub>0 \ f\<^sub>1" using f\<^sub>0_def f\<^sub>1_def by (meson map_upd_eqD1 zero_neq_one) show "\n\Suc ?t. \ i (f\<^sub>0 \ n) = \ i ?b" proof - have "\ i (block i T) = \ i (e_take ?k (block i T))" if "T \ ?t" for T using that gap_T neither hd_block by metis then have "\ i (block i T) = \ i ?b" if "T \ ?t" for T by (metis (no_types, lifting) init_tau_gap gap_T that) then have "\ i (f\<^sub>0 \ (T + 1)) = \ i ?b" if "T \ ?t" for T using filled_gap_0_init_tau[of f\<^sub>0 i T] f\<^sub>0_def gap_T that by (metis (no_types, lifting)) then have "\ i (f\<^sub>0 \ T) = \ i ?b" if "T \ Suc ?t" for T using that by (metis (no_types, lifting) Suc_eq_plus1 Suc_le_D Suc_le_mono) then show ?thesis by simp qed show "\n\Suc ?t. \ i (f\<^sub>1 \ n) = \ i ?b" proof - have "\ i (e_update (block i T) ?k 1) = \ i (e_take ?k (block i T))" if "T \ ?t" for T using neither by (metis (no_types, lifting) hd_block gap_T that) then have "\ i (e_update (block i T) ?k 1) = \ i ?b" if "T \ ?t" for T using that init_tau_gap[of i] gap_T by (metis (no_types, lifting)) then have "\ i (f\<^sub>1 \ (T + 1)) = \ i ?b" if "T \ ?t" for T using filled_gap_1_init_tau[of f\<^sub>1 i T] f\<^sub>1_def gap_T that by (metis (no_types, lifting)) then have "\ i (f\<^sub>1 \ T) = \ i ?b" if "T \ Suc ?t" for T using that by (metis (no_types, lifting) Suc_eq_plus1 Suc_le_D Suc_le_mono) then show ?thesis by simp qed qed qed corollary not_learn_lim_V: "\ learn_lim \ (V_bclim i) (\ i)" using case_one_imp_not_learn_lim_V case_two_imp_not_learn_lim_V by (cases "case_two i") simp_all text \Next we define the separating class.\ definition V_BCLIM :: "partial1 set" ("V\<^bsub>BC-LIM\<^esub>") where "V\<^bsub>BC-LIM\<^esub> \ \i. V_bclim i" lemma V_BCLIM_R1: "V\<^bsub>BC-LIM\<^esub> \ \" using V_BCLIM_def V_subseteq_R1 by auto lemma V_BCLIM_not_in_Lim: "V\<^bsub>BC-LIM\<^esub> \ LIM" proof assume "V\<^bsub>BC-LIM\<^esub> \ LIM" then obtain s where s: "learn_lim \ V\<^bsub>BC-LIM\<^esub> s" using learn_lim_wrt_goedel[OF goedel_numbering_phi] Lim_def by blast moreover obtain i where "\ i = s" using s learn_limE(1) phi_universal by blast ultimately have "learn_lim \ V\<^bsub>BC-LIM\<^esub> (\x. eval r_sigma [i, x])" using learn_lim_sigma by simp moreover have "V_bclim i \ V\<^bsub>BC-LIM\<^esub>" using V_BCLIM_def by auto ultimately have "learn_lim \ (V_bclim i) (\x. eval r_sigma [i, x])" using learn_lim_closed_subseteq by simp then show False using not_learn_lim_V by simp qed subsection \The separating class is in BC\ text \In order to show @{term "V\<^bsub>BC-LIM\<^esub> \ BC"} we define a hypothesis space that for every function $\tau_i$ and every list $b$ of numbers contains a copy of $\tau_i$ with the first $|b|$ values replaced by $b$.\ definition psitau :: partial2 ("\\<^sup>\") where "\\<^sup>\ b x \ (if x < e_length b then Some (e_nth b x) else \ (e_hd b) x)" lemma psitau_in_P2: "\\<^sup>\ \ \

\<^sup>2" proof - define r where "r \ Cn 2 (r_lifz r_nth (Cn 2 r_tau [Cn 2 r_hd [Id 2 0], Id 2 1])) [Cn 2 r_less [Id 2 1, Cn 2 r_length [Id 2 0]], Id 2 0, Id 2 1]" then have "recfn 2 r" using r_tau_recfn by simp moreover have "eval r [b, x] = \\<^sup>\ b x" for b x proof - let ?f = "Cn 2 r_tau [Cn 2 r_hd [Id 2 0], Id 2 1]" have "recfn 2 r_nth" "recfn 2 ?f" using r_tau_recfn by simp_all then have "eval (r_lifz r_nth ?f) [c, b, x] = (if c = 0 then eval r_nth [b, x] else eval ?f [b, x])" for c by simp moreover have "eval r_nth [b, x] \= e_nth b x" by simp moreover have "eval ?f [b, x] = \ (e_hd b) x" using r_tau_recfn by simp ultimately have "eval (r_lifz r_nth ?f) [c, b, x] = (if c = 0 then Some (e_nth b x) else \ (e_hd b) x)" for c by simp moreover have "eval (Cn 2 r_less [Id 2 1, Cn 2 r_length [Id 2 0]]) [b, x] \= (if x < e_length b then 0 else 1)" by simp ultimately show ?thesis unfolding r_def psitau_def using r_tau_recfn by simp qed ultimately show ?thesis by auto qed lemma psitau_init: "\\<^sup>\ (f \ n) x = (if x < Suc n then Some (the (f x)) else \ (the (f 0)) x)" proof - let ?e = "f \ n" have "e_length ?e = Suc n" by simp moreover have "x < Suc n \ e_nth ?e x = the (f x)" by simp moreover have "e_hd ?e = the (f 0)" using hd_init by simp ultimately show ?thesis using psitau_def by simp qed text \The class @{term V_BCLIM} can be learned BC-style in the hypothesis space @{term psitau} by the identity function.\ lemma learn_bc_V_BCLIM: "learn_bc \\<^sup>\ V\<^bsub>BC-LIM\<^esub> Some" proof (rule learn_bcI) show "environment \\<^sup>\ V\<^bsub>BC-LIM\<^esub> Some" using identity_in_R1 V_BCLIM_R1 psitau_in_P2 by auto show "\n\<^sub>0. \n\n\<^sub>0. \\<^sup>\ (the (Some (f \ n))) = f" if "f \ V\<^bsub>BC-LIM\<^esub>" for f proof - from that V_BCLIM_def obtain i where i: "f \ V_bclim i" by auto show ?thesis proof (cases "case_two i") case True let ?P = "\t. \T. (gap i T) \ (gap i t)" let ?lmin = "LEAST t. ?P t" define k where "k \ gap i ?lmin" have V_bclim: "V_bclim i = {(\ i)(k:=Some 0), (\ i)(k:=Some 1)}" using True V_bclim_def k_def by (simp add: Let_def) moreover have "0 < k" using gap_gr0[of i] k_def by simp ultimately have "f 0 \= i" using tau_at_0[of i] i by auto have "\\<^sup>\ (f \ n) = f" if "n \ k" for n proof fix x show "\\<^sup>\ (f \ n) x = f x" proof (cases "x \ n") case True then show ?thesis using R1_imp_total1 V_subseteq_R1 i psitau_init by fastforce next case False then have "\\<^sup>\ (f \ n) x = \ (the (f 0)) x" using psitau_init by simp then have "\\<^sup>\ (f \ n) x = \ i x" using \f 0 \= i\ by simp moreover have "f x = \ i x" using False V_bclim i that by auto ultimately show ?thesis by simp qed qed then show ?thesis by auto next case False then have "V_bclim i = {\ i}" using V_bclim_def by (auto simp add: Let_def) then have f: "f = \ i" using i by simp have "\\<^sup>\ (f \ n) = f" for n proof fix x show "\\<^sup>\ (f \ n) x = f x" proof (cases "x \ n") case True then show ?thesis using R1_imp_total1 V_BCLIM_R1 psitau_init that by auto next case False then show ?thesis by (simp add: f psitau_init tau_at_0) qed qed then show ?thesis by simp qed qed qed text \Finally, the main result of this section:\ theorem Lim_subset_BC: "LIM \ BC" using learn_bc_V_BCLIM BC_def Lim_subseteq_BC V_BCLIM_not_in_Lim by auto end diff --git a/thys/Inductive_Inference/Partial_Recursive.thy b/thys/Inductive_Inference/Partial_Recursive.thy --- a/thys/Inductive_Inference/Partial_Recursive.thy +++ b/thys/Inductive_Inference/Partial_Recursive.thy @@ -1,1914 +1,1914 @@ chapter \Partial recursive functions\ theory Partial_Recursive imports Main "HOL-Library.Nat_Bijection" begin text \This chapter lays the foundation for Chapter~\ref{c:iirf}. Essentially it develops recursion theory up to the point of certain fixed-point theorems. This in turn requires standard results such as the existence of a universal function and the $s$-$m$-$n$ theorem. Besides these, the chapter contains some results, mostly regarding decidability and the Kleene normal form, that are not strictly needed later. They are included as relatively low-hanging fruits to round off the chapter. The formalization of partial recursive functions is very much inspired by the Universal Turing Machine AFP entry by Xu et~al.~\cite{Universal_Turing_Machine-AFP}. It models partial recursive functions as algorithms whose semantics is given by an evaluation function. This works well for most of this chapter. For the next chapter, however, it is beneficial to regard partial recursive functions as ``proper'' partial functions. To that end, Section~\ref{s:alternative} introduces more conventional and convenient notation for the common special cases of unary and binary partial recursive functions. Especially for the nontrivial proofs I consulted the classical textbook by Rogers~\cite{Rogers87}, which also partially explains my preferring the traditional term ``recursive'' to the more modern ``computable''.\ section \Basic definitions\ subsection \Partial recursive functions\ text \To represent partial recursive functions we start from the same datatype as Xu et~al.~\cite{Universal_Turing_Machine-AFP}, more specifically from Urban's version of the formalization. In fact the datatype @{text recf} and the function @{text arity} below have been copied verbatim from it.\ datatype recf = Z | S | Id nat nat | Cn nat recf "recf list" | Pr nat recf recf | Mn nat recf fun arity :: "recf \ nat" where "arity Z = 1" | "arity S = 1" | "arity (Id m n) = m" | "arity (Cn n f gs) = n" | "arity (Pr n f g) = Suc n" | "arity (Mn n f) = n" text \Already we deviate from Xu et~al.\ in that we define a well-formedness predicate for partial recursive functions. Well-formedness essentially means arity constraints are respected when combining @{typ recf}s.\ fun wellf :: "recf \ bool" where "wellf Z = True" | "wellf S = True" | "wellf (Id m n) = (n < m)" | "wellf (Cn n f gs) = (n > 0 \ (\g \ set gs. arity g = n \ wellf g) \ arity f = length gs \ wellf f)" | "wellf (Pr n f g) = (arity g = Suc (Suc n) \ arity f = n \ wellf f \ wellf g)" | "wellf (Mn n f) = (n > 0 \ arity f = Suc n \ wellf f)" lemma wellf_arity_nonzero: "wellf f \ arity f > 0" by (induction f rule: arity.induct) simp_all lemma wellf_Pr_arity_greater_1: "wellf (Pr n f g) \ arity (Pr n f g) > 1" using wellf_arity_nonzero by auto text \For the most part of this chapter this is the meaning of ``$f$ is an $n$-ary partial recursive function'':\ abbreviation recfn :: "nat \ recf \ bool" where "recfn n f \ wellf f \ arity f = n" text \Some abbreviations for working with @{typ "nat option"}:\ abbreviation divergent :: "nat option \ bool" ("_ \" [50] 50) where "x \ \ x = None" abbreviation convergent :: "nat option \ bool" ("_ \" [50] 50) where "x \ \ x \ None" abbreviation convergent_eq :: "nat option \ nat \ bool" (infix "\=" 50) where "x \= y \ x = Some y" abbreviation convergent_neq :: "nat option \ nat \ bool" (infix "\\" 50) where "x \\ y \ x \ \ x \ Some y" text \In prose the terms ``halt'', ``terminate'', ``converge'', and ``defined'' will be used interchangeably; likewise for ``not halt'', ``diverge'', and ``undefined''. In names of lemmas, the abbreviations @{text converg} and @{text diverg} will be used consistently.\ text \Our second major deviation from Xu et~al.~\cite{Universal_Turing_Machine-AFP} is that we model the semantics of a @{typ recf} by combining the value and the termination of a function into one evaluation function with codomain @{typ "nat option"}, rather than separating both aspects into an evaluation function with codomain @{typ nat} and a termination predicate. The value of a well-formed partial recursive function applied to a correctly-sized list of arguments:\ fun eval_wellf :: "recf \ nat list \ nat option" where "eval_wellf Z xs \= 0" | "eval_wellf S xs \= Suc (xs ! 0)" | "eval_wellf (Id m n) xs \= xs ! n" | "eval_wellf (Cn n f gs) xs = (if \g \ set gs. eval_wellf g xs \ then eval_wellf f (map (\g. the (eval_wellf g xs)) gs) else None)" | "eval_wellf (Pr n f g) [] = undefined" | "eval_wellf (Pr n f g) (0 # xs) = eval_wellf f xs" | "eval_wellf (Pr n f g) (Suc x # xs) = Option.bind (eval_wellf (Pr n f g) (x # xs)) (\v. eval_wellf g (x # v # xs))" | "eval_wellf (Mn n f) xs = (let E = \z. eval_wellf f (z # xs) in if \z. E z \= 0 \ (\y) then Some (LEAST z. E z \= 0 \ (\y)) else None)" text \We define a function value only if the @{typ recf} is well-formed and its arity matches the number of arguments.\ definition eval :: "recf \ nat list \ nat option" where "recfn (length xs) f \ eval f xs \ eval_wellf f xs" lemma eval_Z [simp]: "eval Z [x] \= 0" by (simp add: eval_def) lemma eval_Z' [simp]: "length xs = 1 \ eval Z xs \= 0" by (simp add: eval_def) lemma eval_S [simp]: "eval S [x] \= Suc x" by (simp add: eval_def) lemma eval_S' [simp]: "length xs = 1 \ eval S xs \= Suc (hd xs)" using eval_def hd_conv_nth[of xs] by fastforce lemma eval_Id [simp]: assumes "n < m" and "m = length xs" shows "eval (Id m n) xs \= xs ! n" using assms by (simp add: eval_def) lemma eval_Cn [simp]: assumes "recfn (length xs) (Cn n f gs)" shows "eval (Cn n f gs) xs = (if \g\set gs. eval g xs \ then eval f (map (\g. the (eval g xs)) gs) else None)" proof - have "eval (Cn n f gs) xs = eval_wellf (Cn n f gs) xs" using assms eval_def by blast moreover have "\g. g \ set gs \ eval_wellf g xs = eval g xs" using assms eval_def by simp ultimately have "eval (Cn n f gs) xs = (if \g\set gs. eval g xs \ then eval_wellf f (map (\g. the (eval g xs)) gs) else None)" using map_eq_conv[of "\g. the (eval_wellf g xs)" gs "\g. the (eval g xs)"] by (auto, metis) moreover have "\ys. length ys = length gs \ eval f ys = eval_wellf f ys" using assms eval_def by simp ultimately show ?thesis by auto qed lemma eval_Pr_0 [simp]: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" shows "eval (Pr n f g) (0 # xs) = eval f xs" using assms by (simp add: eval_def) lemma eval_Pr_diverg_Suc [simp]: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" and "eval (Pr n f g) (x # xs) \" shows "eval (Pr n f g) (Suc x # xs) \" using assms by (simp add: eval_def) lemma eval_Pr_converg_Suc [simp]: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" and "eval (Pr n f g) (x # xs) \" shows "eval (Pr n f g) (Suc x # xs) = eval g (x # the (eval (Pr n f g) (x # xs)) # xs)" using assms eval_def by auto lemma eval_Pr_diverg_add: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" and "eval (Pr n f g) (x # xs) \" shows "eval (Pr n f g) ((x + y) # xs) \" using assms by (induction y) auto lemma eval_Pr_converg_le: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" and "eval (Pr n f g) (x # xs) \" and "y \ x" shows "eval (Pr n f g) (y # xs) \" using assms eval_Pr_diverg_add le_Suc_ex by metis lemma eval_Pr_Suc_converg: assumes "recfn (Suc n) (Pr n f g)" and "n = length xs" and "eval (Pr n f g) (Suc x # xs) \" shows "eval g (x # (the (eval (Pr n f g) (x # xs))) # xs) \" and "eval (Pr n f g) (Suc x # xs) = eval g (x # the (eval (Pr n f g) (x # xs)) # xs)" using eval_Pr_converg_Suc[of n f g xs x, OF assms(1,2)] eval_Pr_converg_le[of n f g xs "Suc x" x, OF assms] assms(3) by simp_all lemma eval_Mn [simp]: assumes "recfn (length xs) (Mn n f)" shows "eval (Mn n f) xs = (if (\z. eval f (z # xs) \= 0 \ (\y)) then Some (LEAST z. eval f (z # xs) \= 0 \ (\y)) else None)" using assms eval_def by auto text \For $\mu$-recursion, the condition @{term "(\y)"} inside @{text LEAST} in the definition of @{term eval_wellf} is redundant.\ lemma eval_wellf_Mn: "eval_wellf (Mn n f) xs = (if (\z. eval_wellf f (z # xs) \= 0 \ (\y)) then Some (LEAST z. eval_wellf f (z # xs) \= 0) else None)" proof - let ?P = "\z. eval_wellf f (z # xs) \= 0 \ (\y)" { assume "\z. ?P z" moreover define z where "z = Least ?P" ultimately have "?P z" using LeastI[of ?P] by blast have "(LEAST z. eval_wellf f (z # xs) \= 0) = z" proof (rule Least_equality) show "eval_wellf f (z # xs) \= 0" using \?P z\ by simp show "z \ y" if "eval_wellf f (y # xs) \= 0" for y proof (rule ccontr) assume "\ z \ y" then have "y < z" by simp moreover from this have "?P y" using that \?P z\ by simp ultimately show False using that not_less_Least z_def by blast qed qed } then show ?thesis by simp qed lemma eval_Mn': assumes "recfn (length xs) (Mn n f)" shows "eval (Mn n f) xs = (if (\z. eval f (z # xs) \= 0 \ (\y)) then Some (LEAST z. eval f (z # xs) \= 0) else None)" using assms eval_def eval_wellf_Mn by auto text \Proving that $\mu$-recursion converges is easier if one does not have to deal with @{text LEAST} directly.\ lemma eval_Mn_convergI: assumes "recfn (length xs) (Mn n f)" and "eval f (z # xs) \= 0" and "\y. y < z \ eval f (y # xs) \\ 0" shows "eval (Mn n f) xs \= z" proof - let ?P = "\z. eval f (z # xs) \= 0 \ (\y)" have "z = Least ?P" using Least_equality[of ?P z] assms(2,3) not_le_imp_less by blast moreover have "?P z" using assms(2,3) by simp ultimately show "eval (Mn n f) xs \= z" using eval_Mn[OF assms(1)] by meson qed text \Similarly, reasoning from a $\mu$-recursive function is simplified somewhat by the next lemma.\ lemma eval_Mn_convergE: assumes "recfn (length xs) (Mn n f)" and "eval (Mn n f) xs \= z" shows "z = (LEAST z. eval f (z # xs) \= 0 \ (\y))" and "eval f (z # xs) \= 0" and "\y. y < z \ eval f (y # xs) \\ 0" proof - let ?P = "\z. eval f (z # xs) \= 0 \ (\y)" show "z = Least ?P" using assms eval_Mn[OF assms(1)] by (metis (no_types, lifting) option.inject option.simps(3)) moreover have "\z. ?P z" using assms eval_Mn[OF assms(1)] by (metis option.distinct(1)) ultimately have "?P z" using LeastI[of ?P] by blast then have "eval f (z # xs) \= 0 \ (\y)" by simp then show "eval f (z # xs) \= 0" by simp show "\y. y < z \ eval f (y # xs) \\ 0" using not_less_Least[of _ ?P] \z = Least ?P\ \?P z\ less_trans by blast qed lemma eval_Mn_diverg: assumes "recfn (length xs) (Mn n f)" shows "\ (\z. eval f (z # xs) \= 0 \ (\y)) \ eval (Mn n f) xs \" using assms eval_Mn[OF assms(1)] by simp subsection \Extensional equality\ definition exteq :: "recf \ recf \ bool" (infix "\" 55) where "f \ g \ arity f = arity g \ (\xs. length xs = arity f \ eval f xs = eval g xs)" lemma exteq_refl: "f \ f" using exteq_def by simp lemma exteq_sym: "f \ g \ g \ f" using exteq_def by simp lemma exteq_trans: "f \ g \ g \ h \ f \ h" using exteq_def by simp lemma exteqI: assumes "arity f = arity g" and "\xs. length xs = arity f \ eval f xs = eval g xs" shows "f \ g" using assms exteq_def by simp lemma exteqI1: assumes "arity f = 1" and "arity g = 1" and "\x. eval f [x] = eval g [x]" shows "f \ g" using assms exteqI by (metis One_nat_def Suc_length_conv length_0_conv) text \For every partial recursive function @{term f} there are infinitely many extensionally equal ones, for example, those that wrap @{term f} arbitrarily often in the identity function.\ fun wrap_Id :: "recf \ nat \ recf" where "wrap_Id f 0 = f" | "wrap_Id f (Suc n) = Cn (arity f) (Id 1 0) [wrap_Id f n]" lemma recfn_wrap_Id: "recfn a f \ recfn a (wrap_Id f n)" using wellf_arity_nonzero by (induction n) auto lemma exteq_wrap_Id: "recfn a f \ f \ wrap_Id f n" proof (induction n) case 0 then show ?case by (simp add: exteq_refl) next case (Suc n) have "wrap_Id f n \ wrap_Id f (Suc n) " proof (rule exteqI) show "arity (wrap_Id f n) = arity (wrap_Id f (Suc n))" using Suc by (simp add: recfn_wrap_Id) show "eval (wrap_Id f n) xs = eval (wrap_Id f (Suc n)) xs" if "length xs = arity (wrap_Id f n)" for xs proof - have "recfn (length xs) (Cn (arity f) (Id 1 0) [wrap_Id f n])" using that Suc recfn_wrap_Id by (metis wrap_Id.simps(2)) then show "eval (wrap_Id f n) xs = eval (wrap_Id f (Suc n)) xs" by auto qed qed then show ?case using Suc exteq_trans by fast qed fun depth :: "recf \ nat" where "depth Z = 0" | "depth S = 0" | "depth (Id m n) = 0" | "depth (Cn n f gs) = Suc (max (depth f) (Max (set (map depth gs))))" | "depth (Pr n f g) = Suc (max (depth f) (depth g))" | "depth (Mn n f) = Suc (depth f)" lemma depth_wrap_Id: "recfn a f \ depth (wrap_Id f n) = depth f + n" by (induction n) simp_all lemma wrap_Id_injective: assumes "recfn a f" and "wrap_Id f n\<^sub>1 = wrap_Id f n\<^sub>2" shows "n\<^sub>1 = n\<^sub>2" using assms by (metis add_left_cancel depth_wrap_Id) lemma exteq_infinite: assumes "recfn a f" shows "infinite {g. recfn a g \ g \ f}" (is "infinite ?R") proof - have "inj (wrap_Id f)" using wrap_Id_injective \recfn a f\ by (meson inj_onI) then have "infinite (range (wrap_Id f))" using finite_imageD by blast moreover have "range (wrap_Id f) \ ?R" using assms exteq_sym exteq_wrap_Id recfn_wrap_Id by blast ultimately show ?thesis by (simp add: infinite_super) qed subsection \Primitive recursive and total functions\ fun Mn_free :: "recf \ bool" where "Mn_free Z = True" | "Mn_free S = True" | "Mn_free (Id m n) = True" | "Mn_free (Cn n f gs) = ((\g \ set gs. Mn_free g) \ Mn_free f)" | "Mn_free (Pr n f g) = (Mn_free f \ Mn_free g)" | "Mn_free (Mn n f) = False" text \This is our notion of $n$-ary primitive recursive function:\ abbreviation prim_recfn :: "nat \ recf \ bool" where "prim_recfn n f \ recfn n f \ Mn_free f" definition total :: "recf \ bool" where "total f \ \xs. length xs = arity f \ eval f xs \" lemma totalI [intro]: assumes "\xs. length xs = arity f \ eval f xs \" shows "total f" using assms total_def by simp lemma totalE [simp]: assumes "total f" and "recfn n f" and "length xs = n" shows "eval f xs \" using assms total_def by simp lemma totalI1 : assumes "recfn 1 f" and "\x. eval f [x] \" shows "total f" using assms totalI[of f] by (metis One_nat_def length_0_conv length_Suc_conv) lemma totalI2: assumes "recfn 2 f" and "\x y. eval f [x, y] \" shows "total f" using assms totalI[of f] by (smt length_0_conv length_Suc_conv numeral_2_eq_2) lemma totalI3: assumes "recfn 3 f" and "\x y z. eval f [x, y, z] \" shows "total f" using assms totalI[of f] by (smt length_0_conv length_Suc_conv numeral_3_eq_3) lemma totalI4: assumes "recfn 4 f" and "\w x y z. eval f [w, x, y, z] \" shows "total f" proof (rule totalI[of f]) fix xs :: "nat list" assume "length xs = arity f" then have "length xs = Suc (Suc (Suc (Suc 0)))" using assms(1) by simp then obtain w x y z where "xs = [w, x, y, z]" by (smt Suc_length_conv length_0_conv) then show "eval f xs \" using assms(2) by simp qed lemma Mn_free_imp_total [intro]: assumes "wellf f" and "Mn_free f" shows "total f" using assms proof (induction f rule: Mn_free.induct) case (5 n f g) have "eval (Pr n f g) (x # xs) \" if "length (x # xs) = arity (Pr n f g)" for x xs using 5 that by (induction x) auto then show ?case by (metis arity.simps(5) length_Suc_conv totalI) qed (auto simp add: total_def eval_def) lemma prim_recfn_total: "prim_recfn n f \ total f" using Mn_free_imp_total by simp lemma eval_Pr_prim_Suc: assumes "h = Pr n f g" and "prim_recfn (Suc n) h" and "length xs = n" shows "eval h (Suc x # xs) = eval g (x # the (eval h (x # xs)) # xs)" using assms eval_Pr_converg_Suc prim_recfn_total by simp lemma Cn_total: assumes "\g\set gs. total g" and "total f" and "recfn n (Cn n f gs)" shows "total (Cn n f gs)" using assms by (simp add: totalI) lemma Pr_total: assumes "total f" and "total g" and "recfn (Suc n) (Pr n f g)" shows "total (Pr n f g)" proof - have "eval (Pr n f g) (x # xs) \" if "length xs = n" for x xs using that assms by (induction x) auto then show ?thesis using assms(3) totalI by (metis Suc_length_conv arity.simps(5)) qed lemma eval_Mn_total: assumes "recfn (length xs) (Mn n f)" and "total f" shows "eval (Mn n f) xs = (if (\z. eval f (z # xs) \= 0) then Some (LEAST z. eval f (z # xs) \= 0) else None)" using assms by auto section \Simple functions\ text \This section, too, bears some similarity to Urban's formalization in Xu et~al.~\cite{Universal_Turing_Machine-AFP}, but is more minimalistic in scope. As a general naming rule, instances of @{typ recf} and functions returning such instances get names starting with @{text r_}. Typically, for an @{text r_xyz} there will be a lemma @{text r_xyz_recfn} or @{text r_xyz_prim} establishing its (primitive) recursiveness, arity, and well-formedness. Moreover there will be a lemma @{text r_xyz} describing its semantics, for which we will sometimes introduce an Isabelle function @{text xyz}.\ subsection \Manipulating parameters\ text \Appending dummy parameters:\ definition r_dummy :: "nat \ recf \ recf" where "r_dummy n f \ Cn (arity f + n) f (map (\i. Id (arity f + n) i) [0.. prim_recfn (a + n) (r_dummy n f)" using wellf_arity_nonzero by (auto simp add: r_dummy_def) lemma r_dummy_recfn [simp]: "recfn a f \ recfn (a + n) (r_dummy n f)" using wellf_arity_nonzero by (auto simp add: r_dummy_def) lemma r_dummy [simp]: "r_dummy n f = Cn (arity f + n) f (map (\i. Id (arity f + n) i) [0..= xs ! i" if "i < arity f" for i using that assms by (simp add: nth_append) ultimately have "map (\g. the (eval_wellf g (xs @ ys))) ?gs = xs" by (metis (no_types, lifting) assms(1) length_map nth_equalityI nth_map option.sel) moreover have "\g \ set ?gs. eval_wellf g (xs @ ys) \" using * by simp moreover have "recfn (length (xs @ ys)) ?r" using assms r_dummy_recfn by fastforce ultimately show ?thesis by (auto simp add: assms eval_def) qed text \Shrinking a binary function to a unary one is useful when we want to define a unary function via the @{term Pr} operation, which can only construct @{typ recf}s of arity two or higher.\ definition r_shrink :: "recf \ recf" where "r_shrink f \ Cn 1 f [Id 1 0, Id 1 0]" lemma r_shrink_prim [simp]: "prim_recfn 2 f \ prim_recfn 1 (r_shrink f)" by (simp add: r_shrink_def) lemma r_shrink_recfn [simp]: "recfn 2 f \ recfn 1 (r_shrink f)" by (simp add: r_shrink_def) lemma r_shrink [simp]: "recfn 2 f \ eval (r_shrink f) [x] = eval f [x, x]" by (simp add: r_shrink_def) definition r_swap :: "recf \ recf" where "r_swap f \ Cn 2 f [Id 2 1, Id 2 0]" lemma r_swap_recfn [simp]: "recfn 2 f \ recfn 2 (r_swap f)" by (simp add: r_swap_def) lemma r_swap_prim [simp]: "prim_recfn 2 f \ prim_recfn 2 (r_swap f)" by (simp add: r_swap_def) lemma r_swap [simp]: "recfn 2 f \ eval (r_swap f) [x, y] = eval f [y, x]" by (simp add: r_swap_def) text \Prepending one dummy parameter:\ definition r_shift :: "recf \ recf" where "r_shift f \ Cn (Suc (arity f)) f (map (\i. Id (Suc (arity f)) (Suc i)) [0.. prim_recfn (Suc a) (r_shift f)" by (simp add: r_shift_def) lemma r_shift_recfn [simp]: "recfn a f \ recfn (Suc a) (r_shift f)" by (simp add: r_shift_def) lemma r_shift [simp]: assumes "recfn (length xs) f" shows "eval (r_shift f) (x # xs) = eval f xs" proof - let ?r = "r_shift f" let ?gs = "map (\i. Id (Suc (arity f)) (Suc i)) [0..= xs ! i" if "i < arity f" for i using assms nth_append that by simp ultimately have "map (\g. the (eval g (x # xs))) ?gs = xs" by (metis (no_types, lifting) assms length_map nth_equalityI nth_map option.sel) moreover have "\g \ set ?gs. eval g (x # xs) \ None" using * by simp ultimately show ?thesis using r_shift_def assms by simp qed subsection \Arithmetic and logic\ text \The unary constants:\ fun r_const :: "nat \ recf" where "r_const 0 = Z" | "r_const (Suc c) = Cn 1 S [r_const c]" lemma r_const_prim [simp]: "prim_recfn 1 (r_const c)" by (induction c) (simp_all) lemma r_const [simp]: "eval (r_const c) [x] \= c" by (induction c) simp_all text \Constants of higher arities:\ definition "r_constn n c \ if n = 0 then r_const c else r_dummy n (r_const c)" lemma r_constn_prim [simp]: "prim_recfn (Suc n) (r_constn n c)" unfolding r_constn_def by simp lemma r_constn [simp]: "length xs = Suc n \ eval (r_constn n c) xs \= c" unfolding r_constn_def by simp (metis length_0_conv length_Suc_conv r_const) text \We introduce addition, subtraction, and multiplication, but interestingly enough we can make do without division.\ definition "r_add \ Pr 1 (Id 1 0) (Cn 3 S [Id 3 1])" lemma r_add_prim [simp]: "prim_recfn 2 r_add" by (simp add: r_add_def) lemma r_add [simp]: "eval r_add [a, b] \= a + b" unfolding r_add_def by (induction a) simp_all definition "r_mul \ Pr 1 Z (Cn 3 r_add [Id 3 1, Id 3 2])" lemma r_mul_prim [simp]: "prim_recfn 2 r_mul" unfolding r_mul_def by simp lemma r_mul [simp]: "eval r_mul [a, b] \= a * b" unfolding r_mul_def by (induction a) simp_all definition "r_dec \ Cn 1 (Pr 1 Z (Id 3 0)) [Id 1 0, Id 1 0]" lemma r_dec_prim [simp]: "prim_recfn 1 r_dec" by (simp add: r_dec_def) lemma r_dec [simp]: "eval r_dec [a] \= a - 1" proof - have "eval (Pr 1 Z (Id 3 0)) [x, y] \= x - 1" for x y by (induction x) simp_all then show ?thesis by (simp add: r_dec_def) qed definition "r_sub \ r_swap (Pr 1 (Id 1 0) (Cn 3 r_dec [Id 3 1]))" lemma r_sub_prim [simp]: "prim_recfn 2 r_sub" unfolding r_sub_def by simp lemma r_sub [simp]: "eval r_sub [a, b] \= a - b" proof - have "eval (Pr 1 (Id 1 0) (Cn 3 r_dec [Id 3 1])) [x, y] \= y - x" for x y by (induction x) simp_all then show ?thesis unfolding r_sub_def by simp qed definition "r_sign \ r_shrink (Pr 1 Z (r_constn 2 1))" lemma r_sign_prim [simp]: "prim_recfn 1 r_sign" unfolding r_sign_def by simp lemma r_sign [simp]: "eval r_sign [x] \= (if x = 0 then 0 else 1)" proof - have "eval (Pr 1 Z (r_constn 2 1)) [x, y] \= (if x = 0 then 0 else 1)" for x y by (induction x) simp_all then show ?thesis unfolding r_sign_def by simp qed text \In the logical functions, true will be represented by zero, and false will be represented by non-zero as argument and by one as result.\ definition "r_not \ Cn 1 r_sub [r_const 1, r_sign]" lemma r_not_prim [simp]: "prim_recfn 1 r_not" unfolding r_not_def by simp lemma r_not [simp]: "eval r_not [x] \= (if x = 0 then 1 else 0)" unfolding r_not_def by simp definition "r_nand \ Cn 2 r_not [r_add]" lemma r_nand_prim [simp]: "prim_recfn 2 r_nand" unfolding r_nand_def by simp lemma r_nand [simp]: "eval r_nand [x, y] \= (if x = 0 \ y = 0 then 1 else 0)" unfolding r_nand_def by simp definition "r_and \ Cn 2 r_not [r_nand]" lemma r_and_prim [simp]: "prim_recfn 2 r_and" unfolding r_and_def by simp lemma r_and [simp]: "eval r_and [x, y] \= (if x = 0 \ y = 0 then 0 else 1)" unfolding r_and_def by simp definition "r_or \ Cn 2 r_sign [r_mul]" lemma r_or_prim [simp]: "prim_recfn 2 r_or" unfolding r_or_def by simp lemma r_or [simp]: "eval r_or [x, y] \= (if x = 0 \ y = 0 then 0 else 1)" unfolding r_or_def by simp subsection \Comparison and conditions\ definition "r_ifz \ let ifzero = (Cn 3 r_mul [r_dummy 2 r_not, Id 3 1]); ifnzero = (Cn 3 r_mul [r_dummy 2 r_sign, Id 3 2]) in Cn 3 r_add [ifzero, ifnzero]" lemma r_ifz_prim [simp]: "prim_recfn 3 r_ifz" unfolding r_ifz_def by simp lemma r_ifz [simp]: "eval r_ifz [cond, val0, val1] \= (if cond = 0 then val0 else val1)" unfolding r_ifz_def by (simp add: Let_def) definition "r_eq \ Cn 2 r_sign [Cn 2 r_add [r_sub, r_swap r_sub]]" lemma r_eq_prim [simp]: "prim_recfn 2 r_eq" unfolding r_eq_def by simp lemma r_eq [simp]: "eval r_eq [x, y] \= (if x = y then 0 else 1)" unfolding r_eq_def by simp definition "r_ifeq \ Cn 4 r_ifz [r_dummy 2 r_eq, Id 4 2, Id 4 3]" lemma r_ifeq_prim [simp]: "prim_recfn 4 r_ifeq" unfolding r_ifeq_def by simp lemma r_ifeq [simp]: "eval r_ifeq [a, b, v\<^sub>0, v\<^sub>1] \= (if a = b then v\<^sub>0 else v\<^sub>1)" unfolding r_ifeq_def using r_dummy_append[of r_eq "[a, b]" "[v\<^sub>0, v\<^sub>1]" 2] by simp definition "r_neq \ Cn 2 r_not [r_eq]" lemma r_neq_prim [simp]: "prim_recfn 2 r_neq" unfolding r_neq_def by simp lemma r_neq [simp]: "eval r_neq [x, y] \= (if x = y then 1 else 0)" unfolding r_neq_def by simp definition "r_ifle \ Cn 4 r_ifz [r_dummy 2 r_sub, Id 4 2, Id 4 3]" lemma r_ifle_prim [simp]: "prim_recfn 4 r_ifle" unfolding r_ifle_def by simp lemma r_ifle [simp]: "eval r_ifle [a, b, v\<^sub>0, v\<^sub>1] \= (if a \ b then v\<^sub>0 else v\<^sub>1)" unfolding r_ifle_def using r_dummy_append[of r_sub "[a, b]" "[v\<^sub>0, v\<^sub>1]" 2] by simp definition "r_ifless \ Cn 4 r_ifle [Id 4 1, Id 4 0, Id 4 3, Id 4 2]" lemma r_ifless_prim [simp]: "prim_recfn 4 r_ifless" unfolding r_ifless_def by simp lemma r_ifless [simp]: "eval r_ifless [a, b, v\<^sub>0, v\<^sub>1] \= (if a < b then v\<^sub>0 else v\<^sub>1)" unfolding r_ifless_def by simp definition "r_less \ Cn 2 r_ifle [Id 2 1, Id 2 0, r_constn 1 1, r_constn 1 0]" lemma r_less_prim [simp]: "prim_recfn 2 r_less" unfolding r_less_def by simp lemma r_less [simp]: "eval r_less [x, y] \= (if x < y then 0 else 1)" unfolding r_less_def by simp definition "r_le \ Cn 2 r_ifle [Id 2 0, Id 2 1, r_constn 1 0, r_constn 1 1]" lemma r_le_prim [simp]: "prim_recfn 2 r_le" unfolding r_le_def by simp lemma r_le [simp]: "eval r_le [x, y] \= (if x \ y then 0 else 1)" unfolding r_le_def by simp text \Arguments are evaluated eagerly. Therefore @{term "r_ifz"}, etc. cannot be combined with a diverging function to implement a conditionally diverging function in the naive way. The following function implements a special case needed in the next section. A \hyperlink{p:r_lifz}{general lazy version} of @{term "r_ifz"} will be introduced later with the help of a universal function.\ definition "r_ifeq_else_diverg \ Cn 3 r_add [Id 3 2, Mn 3 (Cn 4 r_add [Id 4 0, Cn 4 r_eq [Id 4 1, Id 4 2]])]" lemma r_ifeq_else_diverg_recfn [simp]: "recfn 3 r_ifeq_else_diverg" unfolding r_ifeq_else_diverg_def by simp lemma r_ifeq_else_diverg [simp]: "eval r_ifeq_else_diverg [a, b, v] = (if a = b then Some v else None)" unfolding r_ifeq_else_diverg_def by simp section \The halting problem\label{s:halting}\ text \Decidability will be treated more thoroughly in Section~\ref{s:decidable}. But the halting problem is prominent enough to deserve an early mention.\ definition decidable :: "nat set \ bool" where "decidable X \ \f. recfn 1 f \ (\x. eval f [x] \= (if x \ X then 1 else 0))" text \No matter how partial recursive functions are encoded as natural numbers, the set of all codes of functions halting on their own code is undecidable.\ theorem halting_problem_undecidable: fixes code :: "nat \ recf" assumes "\f. recfn 1 f \ \i. code i = f" shows "\ decidable {x. eval (code 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 with assms obtain i where i: "code i = g" 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 (code 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 section \Encoding tuples and lists\ text \This section is based on the Cantor encoding for pairs. Tuples are encoded by repeated application of the pairing function, lists by pairing their length with the code for a tuple. Thus tuples have a fixed length that must be known when decoding, whereas lists are dynamically sized and know their current length.\ subsection \Pairs and tuples\ subsubsection \The Cantor pairing function\ definition "r_triangle \ r_shrink (Pr 1 Z (r_dummy 1 (Cn 2 S [r_add])))" lemma r_triangle_prim: "prim_recfn 1 r_triangle" unfolding r_triangle_def by simp lemma r_triangle: "eval r_triangle [n] \= Sum {0..n}" proof - let ?r = "r_dummy 1 (Cn 2 S [r_add])" have "eval ?r [x, y, z] \= Suc (x + y)" for x y z using r_dummy_append[of "Cn 2 S [r_add]" "[x, y]" "[z]" 1] by simp then have "eval (Pr 1 Z ?r) [x, y] \= Sum {0..x}" for x y by (induction x) simp_all then show ?thesis unfolding r_triangle_def by simp qed lemma r_triangle_eq_triangle [simp]: "eval r_triangle [n] \= triangle n" using r_triangle gauss_sum_nat triangle_def by simp definition "r_prod_encode \ Cn 2 r_add [Cn 2 r_triangle [r_add], Id 2 0]" lemma r_prod_encode_prim [simp]: "prim_recfn 2 r_prod_encode" unfolding r_prod_encode_def using r_triangle_prim by simp lemma r_prod_encode [simp]: "eval r_prod_encode [m, n] \= prod_encode (m, n)" unfolding r_prod_encode_def prod_encode_def using r_triangle_prim by simp text \These abbreviations are just two more things borrowed from Xu~et~al.~\cite{Universal_Turing_Machine-AFP}.\ abbreviation "pdec1 z \ fst (prod_decode z)" abbreviation "pdec2 z \ snd (prod_decode z)" lemma pdec1_le: "pdec1 i \ i" by (metis le_prod_encode_1 prod.collapse prod_decode_inverse) lemma pdec2_le: "pdec2 i \ i" by (metis le_prod_encode_2 prod.collapse prod_decode_inverse) lemma pdec_less: "pdec2 i < Suc i" using pdec2_le by (simp add: le_imp_less_Suc) lemma pdec1_zero: "pdec1 0 = 0" using pdec1_le by auto definition "r_maxletr \ Pr 1 Z (Cn 3 r_ifle [r_dummy 2 (Cn 1 r_triangle [S]), Id 3 2, Cn 3 S [Id 3 0], Id 3 1])" lemma r_maxletr_prim: "prim_recfn 2 r_maxletr" unfolding r_maxletr_def using r_triangle_prim by simp lemma not_Suc_Greatest_not_Suc: assumes "\ P (Suc x)" and "\x. P x" shows "(GREATEST y. y \ x \ P y) = (GREATEST y. y \ Suc x \ P y)" using assms by (metis le_SucI le_Suc_eq) lemma r_maxletr: "eval r_maxletr [x\<^sub>0, x\<^sub>1] \= (GREATEST y. y \ x\<^sub>0 \ triangle y \ x\<^sub>1)" proof - let ?g = "Cn 3 r_ifle [r_dummy 2 (Cn 1 r_triangle [S]), Id 3 2, Cn 3 S [Id 3 0], Id 3 1]" have greatest: "(if triangle (Suc x\<^sub>0) \ x\<^sub>1 then Suc x\<^sub>0 else (GREATEST y. y \ x\<^sub>0 \ triangle y \ x\<^sub>1)) = (GREATEST y. y \ Suc x\<^sub>0 \ triangle y \ x\<^sub>1)" for x\<^sub>0 x\<^sub>1 proof (cases "triangle (Suc x\<^sub>0) \ x\<^sub>1") case True then show ?thesis using Greatest_equality[of "\y. y \ Suc x\<^sub>0 \ triangle y \ x\<^sub>1"] by fastforce next case False then show ?thesis using not_Suc_Greatest_not_Suc[of "\y. triangle y \ x\<^sub>1" x\<^sub>0] by fastforce qed show ?thesis unfolding r_maxletr_def using r_triangle_prim proof (induction x\<^sub>0) case 0 then show ?case using Greatest_equality[of "\y. y \ 0 \ triangle y \ x\<^sub>1" 0] by simp next case (Suc x\<^sub>0) then show ?case using greatest by simp qed qed definition "r_maxlt \ r_shrink r_maxletr" lemma r_maxlt_prim: "prim_recfn 1 r_maxlt" unfolding r_maxlt_def using r_maxletr_prim by simp lemma r_maxlt: "eval r_maxlt [e] \= (GREATEST y. triangle y \ e)" proof - have "y \ triangle y" for y by (induction y) auto then have "triangle y \ e \ y \ e" for y e using order_trans by blast then have "(GREATEST y. y \ e \ triangle y \ e) = (GREATEST y. triangle y \ e)" by metis moreover have "eval r_maxlt [e] \= (GREATEST y. y \ e \ triangle y \ e)" using r_maxletr r_shrink r_maxlt_def r_maxletr_prim by fastforce ultimately show ?thesis by simp qed definition "pdec1' e \ e - triangle (GREATEST y. triangle y \ e)" definition "pdec2' e \ (GREATEST y. triangle y \ e) - pdec1' e" lemma max_triangle_bound: "triangle z \ e \ z \ e" by (metis Suc_pred add_leD2 less_Suc_eq triangle_Suc zero_le zero_less_Suc) lemma triangle_greatest_le: "triangle (GREATEST y. triangle y \ e) \ e" using max_triangle_bound GreatestI_nat[of "\y. triangle y \ e" 0 e] by simp lemma prod_encode_pdec': "prod_encode (pdec1' e, pdec2' e) = e" proof - let ?P = "\y. triangle y \ e" let ?y = "GREATEST y. ?P y" have "pdec1' e \ ?y" proof (rule ccontr) assume "\ pdec1' e \ ?y" then have "e - triangle ?y > ?y" using pdec1'_def by simp then have "?P (Suc ?y)" by simp moreover have "\z. ?P z \ z \ e" using max_triangle_bound by simp ultimately have "Suc ?y \ ?y" using Greatest_le_nat[of ?P "Suc ?y" e] by blast then show False by simp qed then have "pdec1' e + pdec2' e = ?y" using pdec1'_def pdec2'_def by simp then have "prod_encode (pdec1' e, pdec2' e) = triangle ?y + pdec1' e" by (simp add: prod_encode_def) then show ?thesis using pdec1'_def triangle_greatest_le by simp qed lemma pdec': "pdec1' e = pdec1 e" "pdec2' e = pdec2 e" using prod_encode_pdec' prod_encode_inverse by (metis fst_conv, metis snd_conv) definition "r_pdec1 \ Cn 1 r_sub [Id 1 0, Cn 1 r_triangle [r_maxlt]]" lemma r_pdec1_prim [simp]: "prim_recfn 1 r_pdec1" unfolding r_pdec1_def using r_triangle_prim r_maxlt_prim by simp lemma r_pdec1 [simp]: "eval r_pdec1 [e] \= pdec1 e" unfolding r_pdec1_def using r_triangle_prim r_maxlt_prim pdec' pdec1'_def by (simp add: r_maxlt) definition "r_pdec2 \ Cn 1 r_sub [r_maxlt, r_pdec1]" lemma r_pdec2_prim [simp]: "prim_recfn 1 r_pdec2" unfolding r_pdec2_def using r_maxlt_prim by simp lemma r_pdec2 [simp]: "eval r_pdec2 [e] \= pdec2 e" unfolding r_pdec2_def using r_maxlt_prim r_maxlt pdec' pdec2'_def by simp abbreviation "pdec12 i \ pdec1 (pdec2 i)" abbreviation "pdec22 i \ pdec2 (pdec2 i)" abbreviation "pdec122 i \ pdec1 (pdec22 i)" abbreviation "pdec222 i \ pdec2 (pdec22 i)" definition "r_pdec12 \ Cn 1 r_pdec1 [r_pdec2]" lemma r_pdec12_prim [simp]: "prim_recfn 1 r_pdec12" unfolding r_pdec12_def by simp lemma r_pdec12 [simp]: "eval r_pdec12 [e] \= pdec12 e" unfolding r_pdec12_def by simp definition "r_pdec22 \ Cn 1 r_pdec2 [r_pdec2]" lemma r_pdec22_prim [simp]: "prim_recfn 1 r_pdec22" unfolding r_pdec22_def by simp lemma r_pdec22 [simp]: "eval r_pdec22 [e] \= pdec22 e" unfolding r_pdec22_def by simp definition "r_pdec122 \ Cn 1 r_pdec1 [r_pdec22]" lemma r_pdec122_prim [simp]: "prim_recfn 1 r_pdec122" unfolding r_pdec122_def by simp lemma r_pdec122 [simp]: "eval r_pdec122 [e] \= pdec122 e" unfolding r_pdec122_def by simp definition "r_pdec222 \ Cn 1 r_pdec2 [r_pdec22]" lemma r_pdec222_prim [simp]: "prim_recfn 1 r_pdec222" unfolding r_pdec222_def by simp lemma r_pdec222 [simp]: "eval r_pdec222 [e] \= pdec222 e" unfolding r_pdec222_def by simp subsubsection \The Cantor tuple function\ text \The empty tuple gets no code, whereas singletons are encoded by their only element and other tuples by recursively applying the pairing function. This yields, for every $n$, the function @{term "tuple_encode n"}, which is a bijection between the natural numbers and the lists of length $(n + 1)$.\ fun tuple_encode :: "nat \ nat list \ nat" where "tuple_encode n [] = undefined" | "tuple_encode 0 (x # xs) = x" | "tuple_encode (Suc n) (x # xs) = prod_encode (x, tuple_encode n xs)" lemma tuple_encode_prod_encode: "tuple_encode 1 [x, y] = prod_encode (x, y)" by simp fun tuple_decode where "tuple_decode 0 i = [i]" | "tuple_decode (Suc n) i = pdec1 i # tuple_decode n (pdec2 i)" lemma tuple_encode_decode [simp]: "tuple_encode (length xs - 1) (tuple_decode (length xs - 1) i) = i" proof (induction "length xs - 1" arbitrary: xs i) case 0 then show ?case by simp next case (Suc n) then have "length xs - 1 > 0" by simp with Suc have *: "tuple_encode n (tuple_decode n j) = j" for j by (metis diff_Suc_1 length_tl) from Suc have "tuple_decode (Suc n) i = pdec1 i # tuple_decode n (pdec2 i)" using tuple_decode.simps(2) by blast then have "tuple_encode (Suc n) (tuple_decode (Suc n) i) = tuple_encode (Suc n) (pdec1 i # tuple_decode n (pdec2 i))" using Suc by simp also have "... = prod_encode (pdec1 i, tuple_encode n (tuple_decode n (pdec2 i)))" by simp also have "... = prod_encode (pdec1 i, pdec2 i)" using Suc * by simp also have "... = i" by simp finally have "tuple_encode (Suc n) (tuple_decode (Suc n) i) = i" . then show ?case by (simp add: Suc.hyps(2)) qed lemma tuple_encode_decode' [simp]: "tuple_encode n (tuple_decode n i) = i" using tuple_encode_decode by (metis Ex_list_of_length diff_Suc_1 length_Cons) lemma tuple_decode_encode: assumes "length xs > 0" shows "tuple_decode (length xs - 1) (tuple_encode (length xs - 1) xs) = xs" using assms proof (induction "length xs - 1" arbitrary: xs) case 0 moreover from this have "length xs = 1" by linarith ultimately show ?case by (metis One_nat_def length_0_conv length_Suc_conv tuple_decode.simps(1) tuple_encode.simps(2)) next case (Suc n) let ?t = "tl xs" let ?i = "tuple_encode (Suc n) xs" have "length ?t > 0" and "length ?t - 1 = n" using Suc by simp_all then have "tuple_decode n (tuple_encode n ?t) = ?t" using Suc by blast moreover have "?i = prod_encode (hd xs, tuple_encode n ?t)" using Suc by (metis hd_Cons_tl length_greater_0_conv tuple_encode.simps(3)) moreover have "tuple_decode (Suc n) ?i = pdec1 ?i # tuple_decode n (pdec2 ?i)" using tuple_decode.simps(2) by blast ultimately have "tuple_decode (Suc n) ?i = xs" using Suc.prems by simp then show ?case by (simp add: Suc.hyps(2)) qed lemma tuple_decode_encode' [simp]: assumes "length xs = Suc n" shows "tuple_decode n (tuple_encode n xs) = xs" using assms tuple_decode_encode by (metis diff_Suc_1 zero_less_Suc) lemma tuple_decode_length [simp]: "length (tuple_decode n i) = Suc n" by (induction n arbitrary: i) simp_all lemma tuple_decode_nonzero: assumes "n > 0" shows "tuple_decode n i = pdec1 i # tuple_decode (n - 1) (pdec2 i)" using assms by (metis One_nat_def Suc_pred tuple_decode.simps(2)) text \The tuple encoding functions are primitive recursive.\ fun r_tuple_encode :: "nat \ recf" where "r_tuple_encode 0 = Id 1 0" | "r_tuple_encode (Suc n) = Cn (Suc (Suc n)) r_prod_encode [Id (Suc (Suc n)) 0, r_shift (r_tuple_encode n)]" lemma r_tuple_encode_prim [simp]: "prim_recfn (Suc n) (r_tuple_encode n)" by (induction n) simp_all lemma r_tuple_encode: assumes "length xs = Suc n" shows "eval (r_tuple_encode n) xs \= tuple_encode n xs" using assms proof (induction n arbitrary: xs) case 0 then show ?case by (metis One_nat_def eval_Id length_Suc_conv nth_Cons_0 r_tuple_encode.simps(1) tuple_encode.simps(2) zero_less_one) next case (Suc n) then obtain y ys where y_ys: "y # ys = xs" by (metis length_Suc_conv) with Suc have "eval (r_tuple_encode n) ys \= tuple_encode n ys" by auto with y_ys have "eval (r_shift (r_tuple_encode n)) xs \= tuple_encode n ys" using Suc.prems r_shift_prim r_tuple_encode_prim by auto moreover have "eval (Id (Suc (Suc n)) 0) xs \= y" using y_ys Suc.prems by auto ultimately have "eval (r_tuple_encode (Suc n)) xs \= prod_encode (y, tuple_encode n ys)" using Suc.prems by simp then show ?case using y_ys by auto qed subsubsection \Functions on encoded tuples\ text \The function for accessing the $n$-th element of a tuple returns $0$ for out-of-bounds access.\ definition e_tuple_nth :: "nat \ nat \ nat \ nat" where "e_tuple_nth a i n \ if n \ a then (tuple_decode a i) ! n else 0" lemma e_tuple_nth_le [simp]: "n \ a \ e_tuple_nth a i n = (tuple_decode a i) ! n" using e_tuple_nth_def by simp lemma e_tuple_nth_gr [simp]: "n > a \ e_tuple_nth a i n = 0" using e_tuple_nth_def by simp lemma tuple_decode_pdec2: "tuple_decode a (pdec2 es) = tl (tuple_decode (Suc a) es)" by simp fun iterate :: "nat \ ('a \ 'a) \ ('a \ 'a)" where "iterate 0 f = id" | "iterate (Suc n) f = f \ (iterate n f)" lemma iterate_additive: assumes "iterate t\<^sub>1 f x = y" and "iterate t\<^sub>2 f y = z" shows "iterate (t\<^sub>1 + t\<^sub>2) f x = z" using assms by (induction t\<^sub>2 arbitrary: z) auto lemma iterate_additive': "iterate (t\<^sub>1 + t\<^sub>2) f x = iterate t\<^sub>2 f (iterate t\<^sub>1 f x)" using iterate_additive by metis lemma e_tuple_nth_elementary: assumes "k \ a" shows "e_tuple_nth a i k = (if a = k then (iterate k pdec2 i) else (pdec1 (iterate k pdec2 i)))" proof - have *: "tuple_decode (a - k) (iterate k pdec2 i) = drop k (tuple_decode a i)" using assms by (induction k) (simp, simp add: Suc_diff_Suc tuple_decode_pdec2 drop_Suc tl_drop) show ?thesis proof (cases "a = k") case True then have "tuple_decode 0 (iterate k pdec2 i) = drop k (tuple_decode a i)" using assms * by simp moreover from this have "drop k (tuple_decode a i) = [tuple_decode a i ! k]" using assms True by (metis nth_via_drop tuple_decode.simps(1)) ultimately show ?thesis using True by simp next case False with assms have "a - k > 0" by simp with * have "tuple_decode (a - k) (iterate k pdec2 i) = drop k (tuple_decode a i)" by simp then have "pdec1 (iterate k pdec2 i) = hd (drop k (tuple_decode a i))" using tuple_decode_nonzero \a - k > 0\ by (metis list.sel(1)) with \a - k > 0\ have "pdec1 (iterate k pdec2 i) = (tuple_decode a i) ! k" by (simp add: hd_drop_conv_nth) with False assms show ?thesis by simp qed qed definition "r_nth_inbounds \ let r = Pr 1 (Id 1 0) (Cn 3 r_pdec2 [Id 3 1]) in Cn 3 r_ifeq [Id 3 0, Id 3 2, Cn 3 r [Id 3 2, Id 3 1], Cn 3 r_pdec1 [Cn 3 r [Id 3 2, Id 3 1]]]" lemma r_nth_inbounds_prim: "prim_recfn 3 r_nth_inbounds" unfolding r_nth_inbounds_def by (simp add: Let_def) lemma r_nth_inbounds: "k \ a \ eval r_nth_inbounds [a, i, k] \= e_tuple_nth a i k" "eval r_nth_inbounds [a, i, k] \" proof - let ?r = "Pr 1 (Id 1 0) (Cn 3 r_pdec2 [Id 3 1])" let ?h = "Cn 3 ?r [Id 3 2, Id 3 1]" have "eval ?r [k, i] \= iterate k pdec2 i" for k i using r_pdec2_prim by (induction k) (simp_all) then have "eval ?h [a, i, k] \= iterate k pdec2 i" using r_pdec2_prim by simp then have "eval r_nth_inbounds [a, i, k] \= (if a = k then iterate k pdec2 i else pdec1 (iterate k pdec2 i))" unfolding r_nth_inbounds_def by (simp add: Let_def) then show "k \ a \ eval r_nth_inbounds [a, i, k] \= e_tuple_nth a i k" and "eval r_nth_inbounds [a, i, k] \" using e_tuple_nth_elementary by simp_all qed definition "r_tuple_nth \ Cn 3 r_ifle [Id 3 2, Id 3 0, r_nth_inbounds, r_constn 2 0]" lemma r_tuple_nth_prim: "prim_recfn 3 r_tuple_nth" unfolding r_tuple_nth_def using r_nth_inbounds_prim by simp lemma r_tuple_nth [simp]: "eval r_tuple_nth [a, i, k] \= e_tuple_nth a i k" unfolding r_tuple_nth_def using r_nth_inbounds_prim r_nth_inbounds by simp subsection \Lists\ subsubsection \Encoding and decoding\ text \Lists are encoded by pairing the length of the list with the code for the tuple made up of the list's elements. Then all these codes are incremented in order to make room for the empty list (cf.~Rogers~\cite[p.~71]{Rogers87}).\ fun list_encode :: "nat list \ nat" where "list_encode [] = 0" | "list_encode (x # xs) = Suc (prod_encode (length xs, tuple_encode (length xs) (x # xs)))" -lemma list_encode_0 [simp]: "list_encode xs = 0 \ xs = []" - using list_encode.elims by blast +lemma list_encode_0 [simp]: "list_encode xs = 0 \ xs = []" + using list_encode.elims Partial_Recursive.list_encode.simps(1) by blast lemma list_encode_1: "list_encode [0] = 1" by (simp add: prod_encode_def) fun list_decode :: "nat \ nat list" where "list_decode 0 = []" | "list_decode (Suc n) = tuple_decode (pdec1 n) (pdec2 n)" lemma list_encode_decode [simp]: "list_encode (list_decode n) = n" proof (cases n) case 0 then show ?thesis by simp next case (Suc k) then have *: "list_decode n = tuple_decode (pdec1 k) (pdec2 k)" (is "_ = ?t") by simp then obtain x xs where xxs: "x # xs = ?t" by (metis tuple_decode.elims) then have "list_encode ?t = list_encode (x # xs)" by simp then have 1: "list_encode ?t = Suc (prod_encode (length xs, tuple_encode (length xs) (x # xs)))" by simp have 2: "length xs = length ?t - 1" using xxs by (metis length_tl list.sel(3)) then have 3: "length xs = pdec1 k" using * by simp then have "tuple_encode (length ?t - 1) ?t = pdec2 k" using 2 tuple_encode_decode by metis then have "list_encode ?t = Suc (prod_encode (pdec1 k, pdec2 k))" using 1 2 3 xxs by simp with * Suc show ?thesis by simp qed lemma list_decode_encode [simp]: "list_decode (list_encode xs) = xs" proof (cases xs) case Nil then show ?thesis by simp next case (Cons y ys) then have "list_encode xs = Suc (prod_encode (length ys, tuple_encode (length ys) xs))" (is "_ = Suc ?i") by simp then have "list_decode (Suc ?i) = tuple_decode (pdec1 ?i) (pdec2 ?i)" by simp moreover have "pdec1 ?i = length ys" by simp moreover have "pdec2 ?i = tuple_encode (length ys) xs" by simp ultimately have "list_decode (Suc ?i) = tuple_decode (length ys) (tuple_encode (length ys) xs)" by simp moreover have "length ys = length xs - 1" using Cons by simp ultimately have "list_decode (Suc ?i) = tuple_decode (length xs - 1) (tuple_encode (length xs - 1) xs)" by simp then show ?thesis using Cons by simp qed abbreviation singleton_encode :: "nat \ nat" where "singleton_encode x \ list_encode [x]" lemma list_decode_singleton: "list_decode (singleton_encode x) = [x]" by simp definition "r_singleton_encode \ Cn 1 S [Cn 1 r_prod_encode [Z, Id 1 0]]" lemma r_singleton_encode_prim [simp]: "prim_recfn 1 r_singleton_encode" unfolding r_singleton_encode_def by simp lemma r_singleton_encode [simp]: "eval r_singleton_encode [x] \= singleton_encode x" unfolding r_singleton_encode_def by simp definition r_list_encode :: "nat \ recf" where "r_list_encode n \ Cn (Suc n) S [Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]]" lemma r_list_encode_prim [simp]: "prim_recfn (Suc n) (r_list_encode n)" unfolding r_list_encode_def by simp lemma r_list_encode: assumes "length xs = Suc n" shows "eval (r_list_encode n) xs \= list_encode xs" proof - have "eval (r_tuple_encode n) xs \" by (simp add: assms r_tuple_encode) then have "eval (Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]) xs \" using assms by simp then have "eval (r_list_encode n) xs = eval S [the (eval (Cn (Suc n) r_prod_encode [r_constn n n, r_tuple_encode n]) xs)]" unfolding r_list_encode_def using assms r_tuple_encode by simp moreover from assms obtain y ys where "xs = y # ys" by (meson length_Suc_conv) ultimately show ?thesis unfolding r_list_encode_def using assms r_tuple_encode by simp qed subsubsection \Functions on encoded lists\ text \The functions in this section mimic those on type @{typ "nat list"}. Their names are prefixed by @{text e_} and the names of the corresponding @{typ recf}s by @{text r_}.\ abbreviation e_tl :: "nat \ nat" where "e_tl e \ list_encode (tl (list_decode e))" text \In order to turn @{term e_tl} into a partial recursive function we first represent it in a more elementary way.\ lemma e_tl_elementary: "e_tl e = (if e = 0 then 0 else if pdec1 (e - 1) = 0 then 0 else Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1))))" proof (cases e) case 0 then show ?thesis by simp next case Suc_d: (Suc d) then show ?thesis proof (cases "pdec1 d") case 0 then show ?thesis using Suc_d by simp next case (Suc a) have *: "list_decode e = tuple_decode (pdec1 d) (pdec2 d)" using Suc_d by simp with Suc obtain x xs where xxs: "list_decode e = x # xs" by simp then have **: "e_tl e = list_encode xs" by simp have "list_decode (Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1)))) = tuple_decode (pdec1 (e - 1) - 1) (pdec22 (e - 1))" (is "?lhs = _") by simp also have "... = tuple_decode a (pdec22 (e - 1))" using Suc Suc_d by simp also have "... = tl (tuple_decode (Suc a) (pdec2 (e - 1)))" using tuple_decode_pdec2 Suc by presburger also have "... = tl (tuple_decode (pdec1 (e - 1)) (pdec2 (e - 1)))" using Suc Suc_d by auto also have "... = tl (list_decode e)" using * Suc_d by simp also have "... = xs" using xxs by simp finally have "?lhs = xs" . then have "list_encode ?lhs = list_encode xs" by simp then have "Suc (prod_encode (pdec1 (e - 1) - 1, pdec22 (e - 1))) = list_encode xs" using list_encode_decode by metis then show ?thesis using ** Suc_d Suc by simp qed qed definition "r_tl \ let r = Cn 1 r_pdec1 [r_dec] in Cn 1 r_ifz [Id 1 0, Z, Cn 1 r_ifz [r, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r], Cn 1 r_pdec22 [r_dec]]]]]" lemma r_tl_prim [simp]: "prim_recfn 1 r_tl" unfolding r_tl_def by (simp add: Let_def) lemma r_tl [simp]: "eval r_tl [e] \= e_tl e" unfolding r_tl_def using e_tl_elementary by (simp add: Let_def) text \We define the head of the empty encoded list to be zero.\ definition e_hd :: "nat \ nat" where "e_hd e \ if e = 0 then 0 else hd (list_decode e)" lemma e_hd [simp]: assumes "list_decode e = x # xs" shows "e_hd e = x" using e_hd_def assms by auto lemma e_hd_0 [simp]: "e_hd 0 = 0" using e_hd_def by simp lemma e_hd_neq_0 [simp]: assumes "e \ 0" shows "e_hd e = hd (list_decode e)" using e_hd_def assms by simp definition "r_hd \ Cn 1 r_ifz [Cn 1 r_pdec1 [r_dec], Cn 1 r_pdec2 [r_dec], Cn 1 r_pdec12 [r_dec]]" lemma r_hd_prim [simp]: "prim_recfn 1 r_hd" unfolding r_hd_def by simp lemma r_hd [simp]: "eval r_hd [e] \= e_hd e" proof - have "e_hd e = (if pdec1 (e - 1) = 0 then pdec2 (e - 1) else pdec12 (e - 1))" proof (cases e) case 0 then show ?thesis using pdec1_zero pdec2_le by auto next case (Suc d) then show ?thesis by (cases "pdec1 d") (simp_all add: pdec1_zero) qed then show ?thesis unfolding r_hd_def by simp qed abbreviation e_length :: "nat \ nat" where "e_length e \ length (list_decode e)" lemma e_length_0: "e_length e = 0 \ e = 0" by (metis list_encode.simps(1) length_0_conv list_encode_decode) definition "r_length \ Cn 1 r_ifz [Id 1 0, Z, Cn 1 S [Cn 1 r_pdec1 [r_dec]]]" lemma r_length_prim [simp]: "prim_recfn 1 r_length" unfolding r_length_def by simp lemma r_length [simp]: "eval r_length [e] \= e_length e" unfolding r_length_def by (cases e) simp_all text \Accessing an encoded list out of bounds yields zero.\ definition e_nth :: "nat \ nat \ nat" where "e_nth e n \ if e = 0 then 0 else e_tuple_nth (pdec1 (e - 1)) (pdec2 (e - 1)) n" lemma e_nth [simp]: "e_nth e n = (if n < e_length e then (list_decode e) ! n else 0)" by (cases e) (simp_all add: e_nth_def e_tuple_nth_def) lemma e_hd_nth0: "e_hd e = e_nth e 0" by (simp add: e_hd_def e_length_0 hd_conv_nth) definition "r_nth \ Cn 2 r_ifz [Id 2 0, r_constn 1 0, Cn 2 r_tuple_nth [Cn 2 r_pdec1 [r_dummy 1 r_dec], Cn 2 r_pdec2 [r_dummy 1 r_dec], Id 2 1]]" lemma r_nth_prim [simp]: "prim_recfn 2 r_nth" unfolding r_nth_def using r_tuple_nth_prim by simp lemma r_nth [simp]: "eval r_nth [e, n] \= e_nth e n" unfolding r_nth_def e_nth_def using r_tuple_nth_prim by simp definition "r_rev_aux \ Pr 1 r_hd (Cn 3 r_prod_encode [Cn 3 r_nth [Id 3 2, Cn 3 S [Id 3 0]], Id 3 1])" lemma r_rev_aux_prim: "prim_recfn 2 r_rev_aux" unfolding r_rev_aux_def by simp lemma r_rev_aux: assumes "list_decode e = xs" and "length xs > 0" and "i < length xs" shows "eval r_rev_aux [i, e] \= tuple_encode i (rev (take (Suc i) xs))" using assms(3) proof (induction i) case 0 then show ?case unfolding r_rev_aux_def using assms e_hd_def r_hd by (auto simp add: take_Suc) next case (Suc i) let ?g = "Cn 3 r_prod_encode [Cn 3 r_nth [Id 3 2, Cn 3 S [Id 3 0]], Id 3 1]" from Suc have "eval r_rev_aux [Suc i, e] = eval ?g [i, the (eval r_rev_aux [i, e]), e]" unfolding r_rev_aux_def by simp also have "... \= prod_encode (xs ! (Suc i), tuple_encode i (rev (take (Suc i) xs)))" using Suc by (simp add: assms(1)) finally show ?case by (simp add: Suc.prems take_Suc_conv_app_nth) qed corollary r_rev_aux_full: assumes "list_decode e = xs" and "length xs > 0" shows "eval r_rev_aux [length xs - 1, e] \= tuple_encode (length xs - 1) (rev xs)" using r_rev_aux assms by simp lemma r_rev_aux_total: "eval r_rev_aux [i, e] \" using r_rev_aux_prim totalE by fastforce definition "r_rev \ Cn 1 r_ifz [Id 1 0, Z, Cn 1 S [Cn 1 r_prod_encode [Cn 1 r_dec [r_length], Cn 1 r_rev_aux [Cn 1 r_dec [r_length], Id 1 0]]]]" lemma r_rev_prim [simp]: "prim_recfn 1 r_rev" unfolding r_rev_def using r_rev_aux_prim by simp lemma r_rev [simp]: "eval r_rev [e] \= list_encode (rev (list_decode e))" proof - let ?d = "Cn 1 r_dec [r_length]" let ?a = "Cn 1 r_rev_aux [?d, Id 1 0]" let ?p = "Cn 1 r_prod_encode [?d, ?a]" let ?s = "Cn 1 S [?p]" have eval_a: "eval ?a [e] = eval r_rev_aux [e_length e - 1, e]" using r_rev_aux_prim by simp then have "eval ?s [e] \" using r_rev_aux_prim by (simp add: r_rev_aux_total) then have *: "eval r_rev [e] \= (if e = 0 then 0 else the (eval ?s [e]))" using r_rev_aux_prim by (simp add: r_rev_def) show ?thesis proof (cases "e = 0") case True then show ?thesis using * by simp next case False then obtain xs where xs: "xs = list_decode e" "length xs > 0" using e_length_0 by auto then have len: "length xs = e_length e" by simp with eval_a have "eval ?a [e] = eval r_rev_aux [length xs - 1, e]" by simp then have "eval ?a [e] \= tuple_encode (length xs - 1) (rev xs)" using xs r_rev_aux_full by simp then have "eval ?s [e] \= Suc (prod_encode (length xs - 1, tuple_encode (length xs - 1) (rev xs)))" using len r_rev_aux_prim by simp then have "eval ?s [e] \= Suc (prod_encode (length (rev xs) - 1, tuple_encode (length (rev xs) - 1) (rev xs)))" by simp moreover have "length (rev xs) > 0" using xs by simp ultimately have "eval ?s [e] \= list_encode (rev xs)" by (metis list_encode.elims diff_Suc_1 length_Cons length_greater_0_conv) then show ?thesis using xs * by simp qed qed abbreviation e_cons :: "nat \ nat \ nat" where "e_cons e es \ list_encode (e # list_decode es)" lemma e_cons_elementary: "e_cons e es = (if es = 0 then Suc (prod_encode (0, e)) else Suc (prod_encode (e_length es, prod_encode (e, pdec2 (es - 1)))))" proof (cases "es = 0") case True then show ?thesis by simp next case False then have "e_length es = Suc (pdec1 (es - 1))" by (metis list_decode.elims diff_Suc_1 tuple_decode_length) moreover have "es = e_tl (list_encode (e # list_decode es))" by (metis list.sel(3) list_decode_encode list_encode_decode) ultimately show ?thesis using False e_tl_elementary by (metis list_decode.simps(2) diff_Suc_1 list_encode_decode prod.sel(1) prod_encode_inverse snd_conv tuple_decode.simps(2)) qed definition "r_cons_else \ Cn 2 S [Cn 2 r_prod_encode [Cn 2 r_length [Id 2 1], Cn 2 r_prod_encode [Id 2 0, Cn 2 r_pdec2 [Cn 2 r_dec [Id 2 1]]]]]" lemma r_cons_else_prim: "prim_recfn 2 r_cons_else" unfolding r_cons_else_def by simp lemma r_cons_else: "eval r_cons_else [e, es] \= Suc (prod_encode (e_length es, prod_encode (e, pdec2 (es - 1))))" unfolding r_cons_else_def by simp definition "r_cons \ Cn 2 r_ifz [Id 2 1, Cn 2 S [Cn 2 r_prod_encode [r_constn 1 0, Id 2 0]], r_cons_else]" lemma r_cons_prim [simp]: "prim_recfn 2 r_cons" unfolding r_cons_def using r_cons_else_prim by simp lemma r_cons [simp]: "eval r_cons [e, es] \= e_cons e es" unfolding r_cons_def using r_cons_else_prim r_cons_else e_cons_elementary by simp abbreviation e_snoc :: "nat \ nat \ nat" where "e_snoc es e \ list_encode (list_decode es @ [e])" lemma e_nth_snoc_small [simp]: assumes "n < e_length b" shows "e_nth (e_snoc b z) n = e_nth b n" using assms by (simp add: nth_append) lemma e_hd_snoc [simp]: assumes "e_length b > 0" shows "e_hd (e_snoc b x) = e_hd b" proof - from assms have "b \ 0" using less_imp_neq by force then have hd: "e_hd b = hd (list_decode b)" by simp have "e_length (e_snoc b x) > 0" by simp then have "e_snoc b x \ 0" using not_gr_zero by fastforce then have "e_hd (e_snoc b x) = hd (list_decode (e_snoc b x))" by simp with assms hd show ?thesis by simp qed definition "r_snoc \ Cn 2 r_rev [Cn 2 r_cons [Id 2 1, Cn 2 r_rev [Id 2 0]]]" lemma r_snoc_prim [simp]: "prim_recfn 2 r_snoc" unfolding r_snoc_def by simp lemma r_snoc [simp]: "eval r_snoc [es, e] \= e_snoc es e" unfolding r_snoc_def by simp abbreviation e_butlast :: "nat \ nat" where "e_butlast e \ list_encode (butlast (list_decode e))" abbreviation e_take :: "nat \ nat \ nat" where "e_take n x \ list_encode (take n (list_decode x))" definition "r_take \ Cn 2 r_ifle [Id 2 0, Cn 2 r_length [Id 2 1], Pr 1 Z (Cn 3 r_snoc [Id 3 1, Cn 3 r_nth [Id 3 2, Id 3 0]]), Id 2 1]" lemma r_take_prim [simp]: "prim_recfn 2 r_take" unfolding r_take_def by simp_all lemma r_take: assumes "x = list_encode es" shows "eval r_take [n, x] \= list_encode (take n es)" proof - let ?g = "Cn 3 r_snoc [Id 3 1, Cn 3 r_nth [Id 3 2, Id 3 0]]" let ?h = "Pr 1 Z ?g" have "total ?h" using Mn_free_imp_total by simp have "m \ length es \ eval ?h [m, x] \= list_encode (take m es)" for m proof (induction m) case 0 then show ?case using assms r_take_def by (simp add: r_take_def) next case (Suc m) then have "m < length es" by simp then have "eval ?h [Suc m, x] = eval ?g [m, the (eval ?h [m, x]), x]" using Suc r_take_def by simp also have "... = eval ?g [m, list_encode (take m es), x]" using Suc by simp also have "... \= e_snoc (list_encode (take m es)) (es ! m)" by (simp add: \m < length es\ assms) also have "... \= list_encode ((take m es) @ [es ! m])" using list_decode_encode by simp also have "... \= list_encode (take (Suc m) es)" by (simp add: \m < length es\ take_Suc_conv_app_nth) finally show ?case . qed moreover have "eval (Id 2 1) [m, x] \= list_encode (take m es)" if "m > length es" for m using that assms by simp moreover have "eval r_take [m, x] \= (if m \ e_length x then the (eval ?h [m, x]) else the (eval (Id 2 1) [m, x]))" for m unfolding r_take_def using \total ?h\ by simp ultimately show ?thesis unfolding r_take_def by fastforce qed corollary r_take' [simp]: "eval r_take [n, x] \= e_take n x" by (simp add: r_take) definition "r_last \ Cn 1 r_hd [r_rev]" lemma r_last_prim [simp]: "prim_recfn 1 r_last" unfolding r_last_def by simp lemma r_last [simp]: assumes "e = list_encode xs" and "length xs > 0" shows "eval r_last [e] \= last xs" proof - from assms(2) have "length (rev xs) > 0" by simp then have "list_encode (rev xs) > 0" by (metis gr0I list.size(3) list_encode_0) moreover have "eval r_last [e] = eval r_hd [the (eval r_rev [e])]" unfolding r_last_def by simp ultimately show ?thesis using assms hd_rev by auto qed definition "r_update_aux \ let f = r_constn 2 0; g = Cn 5 r_snoc [Id 5 1, Cn 5 r_ifeq [Id 5 0, Id 5 3, Id 5 4, Cn 5 r_nth [Id 5 2, Id 5 0]]] in Pr 3 f g" lemma r_update_aux_recfn: "recfn 4 r_update_aux" unfolding r_update_aux_def by simp lemma r_update_aux: assumes "n \ e_length b" shows "eval r_update_aux [n, b, j, v] \= list_encode ((take n (list_decode b))[j:=v])" using assms proof (induction n) case 0 then show ?case unfolding r_update_aux_def by simp next case (Suc n) then have n: "n < e_length b" by simp let ?a = "Cn 5 r_nth [Id 5 2, Id 5 0]" let ?b = "Cn 5 r_ifeq [Id 5 0, Id 5 3, Id 5 4, ?a]" define g where "g \ Cn 5 r_snoc [Id 5 1, ?b]" then have g: "eval g [n, r, b, j, v] \= e_snoc r (if n = j then v else e_nth b n)" for r by simp have "Pr 3 (r_constn 2 0) g = r_update_aux" using r_update_aux_def g_def by simp then have "eval r_update_aux [Suc n, b, j, v] = eval g [n, the (eval r_update_aux [n, b, j, v]), b, j, v]" using r_update_aux_recfn Suc n eval_Pr_converg_Suc by (metis arity.simps(5) length_Cons list.size(3) nat_less_le numeral_3_eq_3 option.simps(3)) then have *: "eval r_update_aux [Suc n, b, j, v] \= e_snoc (list_encode ((take n (list_decode b))[j:=v])) (if n = j then v else e_nth b n)" using g Suc by simp consider (j_eq_n) "j = n" | (j_less_n) "j < n" | (j_gt_n) "j > n" by linarith then show ?case proof (cases) case j_eq_n moreover from this have "(take (Suc n) (list_decode b))[j:=v] = (take n (list_decode b))[j:=v] @ [v]" using n by (metis length_list_update nth_list_update_eq take_Suc_conv_app_nth take_update_swap) ultimately show ?thesis using * by simp next case j_less_n moreover from this have "(take (Suc n) (list_decode b))[j:=v] = (take n (list_decode b))[j:=v] @ [(list_decode b) ! n]" using n by (simp add: le_eq_less_or_eq list_update_append min_absorb2 take_Suc_conv_app_nth) ultimately show ?thesis using * by auto next case j_gt_n moreover from this have "(take (Suc n) (list_decode b))[j:=v] = (take n (list_decode b))[j:=v] @ [(list_decode b) ! n]" using n take_Suc_conv_app_nth by auto ultimately show ?thesis using * by auto qed qed abbreviation e_update :: "nat \ nat \ nat \ nat" where "e_update b j v \ list_encode ((list_decode b)[j:=v])" definition "r_update \ Cn 3 r_update_aux [Cn 3 r_length [Id 3 0], Id 3 0, Id 3 1, Id 3 2]" lemma r_update_recfn [simp]: "recfn 3 r_update" unfolding r_update_def using r_update_aux_recfn by simp lemma r_update [simp]: "eval r_update [b, j, v] \= e_update b j v" unfolding r_update_def using r_update_aux r_update_aux_recfn by simp lemma e_length_update [simp]: "e_length (e_update b k v) = e_length b" by simp definition e_append :: "nat \ nat \ nat" where "e_append xs ys \ list_encode (list_decode xs @ list_decode ys)" lemma e_length_append: "e_length (e_append xs ys) = e_length xs + e_length ys" using e_append_def by simp lemma e_nth_append_small: assumes "n < e_length xs" shows "e_nth (e_append xs ys) n = e_nth xs n" using e_append_def assms by (simp add: nth_append) lemma e_nth_append_big: assumes "n \ e_length xs" shows "e_nth (e_append xs ys) n = e_nth ys (n - e_length xs)" using e_append_def assms e_nth by (simp add: less_diff_conv2 nth_append) definition "r_append \ let f = Id 2 0; g = Cn 4 r_snoc [Id 4 1, Cn 4 r_nth [Id 4 3, 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_append_prim [simp]: "prim_recfn 2 r_append" unfolding r_append_def by simp lemma r_append [simp]: "eval r_append [a, b] \= e_append a b" proof - define g where "g = Cn 4 r_snoc [Id 4 1, Cn 4 r_nth [Id 4 3, Id 4 0]]" then have g: "eval g [j, r, a, b] \= e_snoc r (e_nth b j)" for j r by simp let ?h = "Pr 2 (Id 2 0) g" have "eval ?h [n, a, b] \= list_encode (list_decode a @ (take n (list_decode b)))" if "n \ e_length b" for n using that g g_def by (induction n) (simp_all add: take_Suc_conv_app_nth) then show ?thesis unfolding r_append_def g_def e_append_def by simp qed definition e_append_zeros :: "nat \ nat \ nat" where "e_append_zeros b z \ e_append b (list_encode (replicate z 0))" lemma e_append_zeros_length: "e_length (e_append_zeros b z) = e_length b + z" using e_append_def e_append_zeros_def by simp lemma e_nth_append_zeros: "e_nth (e_append_zeros b z) i = e_nth b i" using e_append_zeros_def e_nth_append_small e_nth_append_big by auto lemma e_nth_append_zeros_big: assumes "i \ e_length b" shows "e_nth (e_append_zeros b z) i = 0" unfolding e_append_zeros_def using e_nth_append_big[of b i "list_encode (replicate z 0)", OF assms(1)] by simp definition "r_append_zeros \ r_swap (Pr 1 (Id 1 0) (Cn 3 r_snoc [Id 3 1, r_constn 2 0]))" lemma r_append_zeros_prim [simp]: "prim_recfn 2 r_append_zeros" unfolding r_append_zeros_def by simp lemma r_append_zeros: "eval r_append_zeros [b, z] \= e_append_zeros b z" proof - let ?r = "Pr 1 (Id 1 0) (Cn 3 r_snoc [Id 3 1, r_constn 2 0])" have "eval ?r [z, b] \= e_append_zeros b z" using e_append_zeros_def e_append_def by (induction z) (simp_all add: replicate_append_same) then show ?thesis by (simp add: r_append_zeros_def) 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,2539 +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 (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 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 \k < length gs\ 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 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 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 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 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 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 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, opaque_lifting) 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 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 auto next case S 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 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]" 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) + using \ss \ []\ r_leap_prim encode_config r_leap_total list_encode_0 by auto 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 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