[STATEMENT]
lemma r_limr_recfn: "recfn 1 r_limr"
  and r_limr_total: "total r_limr"
  and r_limr:
    "\<phi> (the (eval r_limr [i])) \<in> \<R>"
    "learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 1 r_limr &&& Partial_Recursive.total r_limr &&& \<phi> (the (eval r_limr [i])) \<in> \<R> &&& (learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i]))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
let ?P = "\<lambda>g.
    g \<in> \<R> \<and>
    (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
let ?Q = "\<lambda>g.
    recfn 1 g \<and>
    total g \<and>
    (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and> 
       (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
have "\<exists>g. ?P g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
using lemma_R_for_Lim_effective
[PROOF STATE]
proof (prove)
using this:
\<exists>g\<in>\<R>. \<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))

goal (1 subgoal):
 1. \<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
obtain g where "?P g"
[PROOF STATE]
proof (prove)
using this:
\<exists>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (1 subgoal):
 1. (\<And>g. g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i))))) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
[PROOF STEP]
obtain g' where g': "recfn 1 g'" "total g'" "\<forall>i. eval g' [i] = g i"
[PROOF STATE]
proof (prove)
using this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))

goal (1 subgoal):
 1. (\<And>g'. \<lbrakk>recfn 1 g'; Partial_Recursive.total g'; \<forall>i. eval g' [i] = g i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
with \<open>?P g\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i
[PROOF STEP]
have "?Q g'"
[PROOF STATE]
proof (prove)
using this:
g \<in> \<R> \<and> (\<forall>i. \<phi> (the (g i)) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (g i)))))
recfn 1 g'
Partial_Recursive.total g'
\<forall>i. eval g' [i] = g i

goal (1 subgoal):
 1. recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))

goal (4 subgoals):
 1. recfn 1 r_limr
 2. Partial_Recursive.total r_limr
 3. \<phi> (the (eval r_limr [i])) \<in> \<R>
 4. learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))
[PROOF STEP]
with r_limr_def someI_ex[of ?Q]
[PROOF STATE]
proof (chain)
picking this:
r_limr \<equiv> SOME g. recfn 1 g \<and> Partial_Recursive.total g \<and> (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))
\<exists>x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i]))))) \<Longrightarrow> recfn 1 (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> Partial_Recursive.total (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> (\<forall>i. \<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])))))
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))
[PROOF STEP]
show
    "recfn 1 r_limr"
    "total r_limr"
    "\<phi> (the (eval r_limr [i])) \<in> \<R>"
    "learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))"
[PROOF STATE]
proof (prove)
using this:
r_limr \<equiv> SOME g. recfn 1 g \<and> Partial_Recursive.total g \<and> (\<forall>i. \<phi> (the (eval g [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g [i])))))
\<exists>x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i]))))) \<Longrightarrow> recfn 1 (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> Partial_Recursive.total (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) \<and> (\<forall>i. \<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval (SOME x. recfn 1 x \<and> Partial_Recursive.total x \<and> (\<forall>i. \<phi> (the (eval x [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval x [i])))))) [i])))))
recfn 1 g' \<and> Partial_Recursive.total g' \<and> (\<forall>i. \<phi> (the (eval g' [i])) \<in> \<R> \<and> (\<forall>U \<psi>. learn_lim \<psi> U (\<phi> i) \<longrightarrow> learn_lim \<psi> U (\<phi> (the (eval g' [i])))))

goal (1 subgoal):
 1. (recfn 1 r_limr &&& Partial_Recursive.total r_limr) &&& \<phi> (the (eval r_limr [i])) \<in> \<R> &&& (learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i]))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 r_limr
Partial_Recursive.total r_limr
\<phi> (the (eval r_limr [i])) \<in> \<R>
learn_lim \<psi> U (\<phi> i) \<Longrightarrow> learn_lim \<psi> U (\<phi> (the (eval r_limr [i])))

goal:
No subgoals!
[PROOF STEP]
qed