[STATEMENT]
lemma r_prefixes: "eval r_prefixes [i, n] \<down>= list_encode (prefixes i n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
let ?h = "Pr 1 r_singleton_encode r_prefixes_aux"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
have "eval ?h [n, i] \<down>= list_encode (prefixes i n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
proof (induction n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [0, i] \<down>= Partial_Recursive.list_encode (prefixes i 0)
 2. \<And>n. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n) \<Longrightarrow> eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [0, i] \<down>= Partial_Recursive.list_encode (prefixes i 0)
 2. \<And>n. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n) \<Longrightarrow> eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [0, i] \<down>= Partial_Recursive.list_encode (prefixes i 0)
[PROOF STEP]
using r_prefixes_def r_prefixes_aux_recfn r_singleton_encode
[PROOF STATE]
proof (prove)
using this:
r_prefixes \<equiv> r_swap (Pr 1 r_singleton_encode r_prefixes_aux)
recfn 3 r_prefixes_aux
eval r_singleton_encode [?x] \<down>= singleton_encode ?x

goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [0, i] \<down>= Partial_Recursive.list_encode (prefixes i 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [0, i] \<down>= Partial_Recursive.list_encode (prefixes i 0)

goal (1 subgoal):
 1. \<And>n. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n) \<Longrightarrow> eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n) \<Longrightarrow> eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)

goal (1 subgoal):
 1. \<And>n. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n) \<Longrightarrow> eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)

goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
using r_prefixes_aux_recfn r_prefixes_aux eval_r_s
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)
recfn 3 r_prefixes_aux
eval r_prefixes_aux [?j, ?v, ?i] \<down>= e_snoc ?v (if eval r_s [e_snoc ?v 0] = eval r_s [?v] then 1 else 0)
s = (\<lambda>x. eval r_s [x])

goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))
[PROOF STEP]
by auto metis+
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [Suc n, i] \<down>= Partial_Recursive.list_encode (prefixes i (Suc n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)

goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)

goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
have "eval ?h [n, i] = eval r_prefixes [i, n]" for i n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] = eval r_prefixes [i, n]
[PROOF STEP]
unfolding r_prefixes_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] = eval (r_swap (Pr 1 r_singleton_encode r_prefixes_aux)) [i, n]
[PROOF STEP]
by (simp add: r_prefixes_aux_recfn)
[PROOF STATE]
proof (state)
this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [?n, ?i] = eval r_prefixes [?i, ?n]

goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)
eval (Pr 1 r_singleton_encode r_prefixes_aux) [?n, ?i] = eval r_prefixes [?i, ?n]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eval (Pr 1 r_singleton_encode r_prefixes_aux) [n, i] \<down>= Partial_Recursive.list_encode (prefixes i n)
eval (Pr 1 r_singleton_encode r_prefixes_aux) [?n, ?i] = eval r_prefixes [?i, ?n]

goal (1 subgoal):
 1. eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_prefixes [i, n] \<down>= Partial_Recursive.list_encode (prefixes i n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prefixes_neq_nil: "length (prefixes i x) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length (prefixes i x)
[PROOF STEP]
by (induction x) auto


[STATEMENT]
lemma psi_in_R2: "\<psi> \<in> \<R>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> \<in> \<R>\<^sup>2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<psi> \<in> \<P>\<^sup>2
 2. total2 \<psi>
[PROOF STEP]
define r_psi where "r_psi \<equiv> Cn 2 r_last [r_prefixes]"
[PROOF STATE]
proof (state)
this:
r_psi \<equiv> Cn 2 r_last [r_prefixes]

goal (2 subgoals):
 1. \<psi> \<in> \<P>\<^sup>2
 2. total2 \<psi>
[PROOF STEP]
have "recfn 2 r_psi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 r_psi
[PROOF STEP]
unfolding r_psi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfn 2 (Cn 2 r_last [r_prefixes])
[PROOF STEP]
by (simp add: r_prefixes_recfn)
[PROOF STATE]
proof (state)
this:
recfn 2 r_psi

goal (2 subgoals):
 1. \<psi> \<in> \<P>\<^sup>2
 2. total2 \<psi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
recfn 2 r_psi
[PROOF STEP]
have "eval r_psi [i, n] \<down>= last (prefixes i n)" for n i
[PROOF STATE]
proof (prove)
using this:
recfn 2 r_psi

goal (1 subgoal):
 1. eval r_psi [i, n] \<down>= last (prefixes i n)
[PROOF STEP]
unfolding r_psi_def
[PROOF STATE]
proof (prove)
using this:
recfn 2 (Cn 2 r_last [r_prefixes])

goal (1 subgoal):
 1. eval (Cn 2 r_last [r_prefixes]) [i, n] \<down>= last (prefixes i n)
[PROOF STEP]
using r_prefixes r_prefixes_recfn prefixes_neq_nil
[PROOF STATE]
proof (prove)
using this:
recfn 2 (Cn 2 r_last [r_prefixes])
eval r_prefixes [?i, ?n] \<down>= Partial_Recursive.list_encode (prefixes ?i ?n)
recfn 2 r_prefixes
0 < length (prefixes ?i ?x)

goal (1 subgoal):
 1. eval (Cn 2 r_last [r_prefixes]) [i, n] \<down>= last (prefixes i n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval r_psi [?i, ?n] \<down>= last (prefixes ?i ?n)

goal (2 subgoals):
 1. \<psi> \<in> \<P>\<^sup>2
 2. total2 \<psi>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
eval r_psi [?i, ?n] \<down>= last (prefixes ?i ?n)
[PROOF STEP]
have "(\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?i, ?n] \<down>= last (prefixes ?i ?n)

goal (1 subgoal):
 1. (\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2
[PROOF STEP]
using \<open>recfn 2 r_psi\<close> P2I[of "r_psi"]
[PROOF STATE]
proof (prove)
using this:
eval r_psi [?i, ?n] \<down>= last (prefixes ?i ?n)
recfn 2 r_psi
\<lbrakk>recfn 2 r_psi; \<And>x y. eval r_psi [x, y] = ?f x y\<rbrakk> \<Longrightarrow> ?f \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. (\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2

goal (2 subgoals):
 1. \<psi> \<in> \<P>\<^sup>2
 2. total2 \<psi>
[PROOF STEP]
with psi_def
[PROOF STATE]
proof (chain)
picking this:
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
(\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2
[PROOF STEP]
show "\<psi> \<in> \<P>\<^sup>2"
[PROOF STATE]
proof (prove)
using this:
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
(\<lambda>i x. Some (last (prefixes i x))) \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. \<psi> \<in> \<P>\<^sup>2
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<psi> \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. total2 \<psi>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<psi> \<in> \<P>\<^sup>2

goal (1 subgoal):
 1. total2 \<psi>
[PROOF STEP]
show "total2 psi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total2 \<psi>
[PROOF STEP]
unfolding psi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. total2 (\<lambda>i x. Some (last (prefixes i x)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
total2 \<psi>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma psi_0_or_1:
  assumes "n > 0"
  shows "\<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
0 < n
[PROOF STEP]
obtain m where "n = Suc m"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using gr0_implies_Suc
[PROOF STATE]
proof (prove)
using this:
0 < n
0 < ?n \<Longrightarrow> \<exists>m. ?n = Suc m

goal (1 subgoal):
 1. (\<And>m. n = Suc m \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
n = Suc m

goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = Suc m
[PROOF STEP]
have "last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1"
[PROOF STATE]
proof (prove)
using this:
n = Suc m

goal (1 subgoal):
 1. last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1

goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1

goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
using \<open>n = Suc m\<close> psi_def
[PROOF STATE]
proof (prove)
using this:
last (prefixes i (Suc m)) = 0 \<or> last (prefixes i (Suc m)) = 1
n = Suc m
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))

goal (1 subgoal):
 1. \<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> i n \<down>= 0 \<or> \<psi> i n \<down>= 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma psi_init: "(\<psi> i) \<triangleright> x = list_encode (prefixes i x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> i \<triangleright> x = Partial_Recursive.list_encode (prefixes i x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<psi> i \<triangleright> x = Partial_Recursive.list_encode (prefixes i x)
[PROOF STEP]
have "prefix (\<psi> i) x = prefixes i x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (\<psi> i) x = prefixes i x
[PROOF STEP]
unfolding psi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prefix (\<lambda>x. Some (last (prefixes i x))) x = prefixes i x
[PROOF STEP]
by (induction x) (simp_all add: prefix_0 prefix_Suc)
[PROOF STATE]
proof (state)
this:
prefix (\<psi> i) x = prefixes i x

goal (1 subgoal):
 1. \<psi> i \<triangleright> x = Partial_Recursive.list_encode (prefixes i x)
[PROOF STEP]
with init_def
[PROOF STATE]
proof (chain)
picking this:
?f \<triangleright> ?n \<equiv> Partial_Recursive.list_encode (prefix ?f ?n)
prefix (\<psi> i) x = prefixes i x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?f \<triangleright> ?n \<equiv> Partial_Recursive.list_encode (prefix ?f ?n)
prefix (\<psi> i) x = prefixes i x

goal (1 subgoal):
 1. \<psi> i \<triangleright> x = Partial_Recursive.list_encode (prefixes i x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> i \<triangleright> x = Partial_Recursive.list_encode (prefixes i x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ex_psi_in_U: "\<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
obtain j where j: "j \<ge> 2" "\<psi> j = \<phi> j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>2 \<le> j; \<psi> j = \<phi> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using kleene_fixed_point[of \<psi>] psi_in_R2 R2_imp_P2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<psi> \<in> \
\<^sup>2; \<And>i. \<lbrakk>?k \<le> i; \<phi> i = \<psi> i\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<psi> \<in> \<R>\<^sup>2
?f \<in> \<R>\<^sup>2 \<Longrightarrow> ?f \<in> \
\<^sup>2

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>2 \<le> j; \<psi> j = \<phi> j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
2 \<le> j
\<psi> j = \<phi> j

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
2 \<le> j
\<psi> j = \<phi> j
[PROOF STEP]
have "\<psi> j \<in> \
"
[PROOF STATE]
proof (prove)
using this:
2 \<le> j
\<psi> j = \<phi> j

goal (1 subgoal):
 1. \<psi> j \<in> \

[PROOF STEP]
by (simp add: phi_in_P2)
[PROOF STATE]
proof (state)
this:
\<psi> j \<in> \

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
define p where "p = (\<lambda>x. \<psi> j (x + 1))"
[PROOF STATE]
proof (state)
this:
p = (\<lambda>x. \<psi> j (x + 1))

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
have "p \<in> \<R>\<^sub>0\<^sub>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
from p_def \<open>\<psi> j \<in> \
\<close> skip_P1
[PROOF STATE]
proof (chain)
picking this:
p = (\<lambda>x. \<psi> j (x + 1))
\<psi> j \<in> \

?f \<in> \
 \<Longrightarrow> (\<lambda>x. ?f (x + ?n)) \<in> \

[PROOF STEP]
have "p \<in> \
"
[PROOF STATE]
proof (prove)
using this:
p = (\<lambda>x. \<psi> j (x + 1))
\<psi> j \<in> \

?f \<in> \
 \<Longrightarrow> (\<lambda>x. ?f (x + ?n)) \<in> \

goal (1 subgoal):
 1. p \<in> \

[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
p \<in> \

goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
from psi_in_R2
[PROOF STATE]
proof (chain)
picking this:
\<psi> \<in> \<R>\<^sup>2
[PROOF STEP]
have "total1 (\<psi> j)"
[PROOF STATE]
proof (prove)
using this:
\<psi> \<in> \<R>\<^sup>2

goal (1 subgoal):
 1. total1 (\<psi> j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
total1 (\<psi> j)

goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
with p_def
[PROOF STATE]
proof (chain)
picking this:
p = (\<lambda>x. \<psi> j (x + 1))
total1 (\<psi> j)
[PROOF STEP]
have "total1 p"
[PROOF STATE]
proof (prove)
using this:
p = (\<lambda>x. \<psi> j (x + 1))
total1 (\<psi> j)

goal (1 subgoal):
 1. total1 p
[PROOF STEP]
by (simp add: total1_def)
[PROOF STATE]
proof (state)
this:
total1 p

goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
with psi_0_or_1
[PROOF STATE]
proof (chain)
picking this:
0 < ?n \<Longrightarrow> \<psi> ?i ?n \<down>= 0 \<or> \<psi> ?i ?n \<down>= 1
total1 p
[PROOF STEP]
have "p n \<down>= 0 \<or> p n \<down>= 1" for n
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> \<psi> ?i ?n \<down>= 0 \<or> \<psi> ?i ?n \<down>= 1
total1 p

goal (1 subgoal):
 1. p n \<down>= 0 \<or> p n \<down>= 1
[PROOF STEP]
using psi_def p_def
[PROOF STATE]
proof (prove)
using this:
0 < ?n \<Longrightarrow> \<psi> ?i ?n \<down>= 0 \<or> \<psi> ?i ?n \<down>= 1
total1 p
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
p = (\<lambda>x. \<psi> j (x + 1))

goal (1 subgoal):
 1. p n \<down>= 0 \<or> p n \<down>= 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p ?n \<down>= 0 \<or> p ?n \<down>= 1

goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p ?n \<down>= 0 \<or> p ?n \<down>= 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
p ?n \<down>= 0 \<or> p ?n \<down>= 1

goal (1 subgoal):
 1. p \<in> \<R>\<^sub>0\<^sub>1
[PROOF STEP]
by (simp add: RPred1_def P1_total_imp_R1 \<open>p \<in> \
\<close> \<open>total1 p\<close>)
[PROOF STATE]
proof (state)
this:
p \<in> \<R>\<^sub>0\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> \<R>\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<in> \<R>\<^sub>0\<^sub>1

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
have "\<psi> j = [j] \<odot> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> j = [j] \<odot> p
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
show "\<psi> j x = ([j] \<odot> p) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
proof (cases "x = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
 2. x \<noteq> 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = 0

goal (2 subgoals):
 1. x = 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
 2. x \<noteq> 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = 0

goal (1 subgoal):
 1. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
using psi_def psi_def prepend_at_less
[PROOF STATE]
proof (prove)
using this:
x = 0
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
?n < length ?vs \<Longrightarrow> (?vs \<odot> ?f) ?n \<down>= ?vs ! ?n

goal (1 subgoal):
 1. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> j x = ([j] \<odot> p) x

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> 0

goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0

goal (1 subgoal):
 1. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
using p_def
[PROOF STATE]
proof (prove)
using this:
x \<noteq> 0
p = (\<lambda>x. \<psi> j (x + 1))

goal (1 subgoal):
 1. \<psi> j x = ([j] \<odot> p) x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<psi> j x = ([j] \<odot> p) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<psi> j x = ([j] \<odot> p) x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<psi> j = [j] \<odot> p

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<in> \<R>\<^sub>0\<^sub>1
\<psi> j = [j] \<odot> p
[PROOF STEP]
have "\<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>"
[PROOF STATE]
proof (prove)
using this:
p \<in> \<R>\<^sub>0\<^sub>1
\<psi> j = [j] \<odot> p

goal (1 subgoal):
 1. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
using j U_LIMCONS_def
[PROOF STATE]
proof (prove)
using this:
p \<in> \<R>\<^sub>0\<^sub>1
\<psi> j = [j] \<odot> p
2 \<le> j
\<psi> j = \<phi> j
U\<^bsub>LIM-CONS\<^esub> \<equiv> {vs @ [j] \<odot> p |vs j p. 2 \<le> j \<and> p \<in> \<R>\<^sub>0\<^sub>1 \<and> \<phi> j = vs @ [j] \<odot> p}

goal (1 subgoal):
 1. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
by (metis (mono_tags, lifting) append_Nil mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
\<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>

goal (1 subgoal):
 1. \<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma U_LIMCONS_not_learn_cons: "\<not> learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
assume learn: "learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s"
[PROOF STATE]
proof (state)
this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
have "s (list_encode (vs @ [0])) \<noteq> s (list_encode (vs @ [1]))" for vs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
obtain f\<^sub>0 where f0: "f\<^sub>0 \<in> U\<^bsub>LIM-CONS\<^esub>" "prefix f\<^sub>0 (length vs) = vs @ [0]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f\<^sub>0. \<lbrakk>f\<^sub>0 \<in> U\<^bsub>LIM-CONS\<^esub>; prefix f\<^sub>0 (length vs) = vs @ [0]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using U_LIMCONS_prefix_complete[of "vs @ [0]"]
[PROOF STATE]
proof (prove)
using this:
0 < length (vs @ [0]) \<Longrightarrow> \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length (vs @ [0]) - 1) = vs @ [0]

goal (1 subgoal):
 1. (\<And>f\<^sub>0. \<lbrakk>f\<^sub>0 \<in> U\<^bsub>LIM-CONS\<^esub>; prefix f\<^sub>0 (length vs) = vs @ [0]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f\<^sub>0 \<in> U\<^bsub>LIM-CONS\<^esub>
prefix f\<^sub>0 (length vs) = vs @ [0]

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
obtain f\<^sub>1 where f1: "f\<^sub>1 \<in> U\<^bsub>LIM-CONS\<^esub>" "prefix f\<^sub>1 (length vs) = vs @ [1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>f\<^sub>1. \<lbrakk>f\<^sub>1 \<in> U\<^bsub>LIM-CONS\<^esub>; prefix f\<^sub>1 (length vs) = vs @ [1]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using U_LIMCONS_prefix_complete[of "vs @ [1]"]
[PROOF STATE]
proof (prove)
using this:
0 < length (vs @ [1]) \<Longrightarrow> \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length (vs @ [1]) - 1) = vs @ [1]

goal (1 subgoal):
 1. (\<And>f\<^sub>1. \<lbrakk>f\<^sub>1 \<in> U\<^bsub>LIM-CONS\<^esub>; prefix f\<^sub>1 (length vs) = vs @ [1]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f\<^sub>1 \<in> U\<^bsub>LIM-CONS\<^esub>
prefix f\<^sub>1 (length vs) = vs @ [1]

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
have "f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)
[PROOF STEP]
using f0 f1
[PROOF STATE]
proof (prove)
using this:
f\<^sub>0 \<in> U\<^bsub>LIM-CONS\<^esub>
prefix f\<^sub>0 (length vs) = vs @ [0]
f\<^sub>1 \<in> U\<^bsub>LIM-CONS\<^esub>
prefix f\<^sub>1 (length vs) = vs @ [1]

goal (1 subgoal):
 1. f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)
[PROOF STEP]
by (metis lessI nth_append_length prefix_nth zero_neq_one)
[PROOF STATE]
proof (state)
this:
f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
have "\<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)
[PROOF STEP]
using learn_consE(3)[of \<phi> U_LIMCONS s, OF learn, of f\<^sub>0 "length vs", OF f0(1)]
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<le>length vs. \<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) k = f\<^sub>0 k

goal (1 subgoal):
 1. \<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
have "\<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)
[PROOF STEP]
using learn_consE(3)[of \<phi> U_LIMCONS s, OF learn, of f\<^sub>1 "length vs", OF f1(1)]
[PROOF STATE]
proof (prove)
using this:
\<forall>k\<le>length vs. \<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) k = f\<^sub>1 k

goal (1 subgoal):
 1. \<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)
\<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)
\<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)
[PROOF STEP]
have "the (s (f\<^sub>0 \<triangleright> length vs)) \<noteq> the (s (f\<^sub>1 \<triangleright> length vs))"
[PROOF STATE]
proof (prove)
using this:
f\<^sub>0 (length vs) \<noteq> f\<^sub>1 (length vs)
\<phi> (the (s (f\<^sub>0 \<triangleright> length vs))) (length vs) = f\<^sub>0 (length vs)
\<phi> (the (s (f\<^sub>1 \<triangleright> length vs))) (length vs) = f\<^sub>1 (length vs)

goal (1 subgoal):
 1. the (s (f\<^sub>0 \<triangleright> length vs)) \<noteq> the (s (f\<^sub>1 \<triangleright> length vs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
the (s (f\<^sub>0 \<triangleright> length vs)) \<noteq> the (s (f\<^sub>1 \<triangleright> length vs))

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
the (s (f\<^sub>0 \<triangleright> length vs)) \<noteq> the (s (f\<^sub>1 \<triangleright> length vs))
[PROOF STEP]
have "s (f\<^sub>0 \<triangleright> length vs) \<noteq> s (f\<^sub>1 \<triangleright> length vs)"
[PROOF STATE]
proof (prove)
using this:
the (s (f\<^sub>0 \<triangleright> length vs)) \<noteq> the (s (f\<^sub>1 \<triangleright> length vs))

goal (1 subgoal):
 1. s (f\<^sub>0 \<triangleright> length vs) \<noteq> s (f\<^sub>1 \<triangleright> length vs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s (f\<^sub>0 \<triangleright> length vs) \<noteq> s (f\<^sub>1 \<triangleright> length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
with f0(2) f1(2)
[PROOF STATE]
proof (chain)
picking this:
prefix f\<^sub>0 (length vs) = vs @ [0]
prefix f\<^sub>1 (length vs) = vs @ [1]
s (f\<^sub>0 \<triangleright> length vs) \<noteq> s (f\<^sub>1 \<triangleright> length vs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prefix f\<^sub>0 (length vs) = vs @ [0]
prefix f\<^sub>1 (length vs) = vs @ [1]
s (f\<^sub>0 \<triangleright> length vs) \<noteq> s (f\<^sub>1 \<triangleright> length vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))
[PROOF STEP]
by (simp add: init_def)
[PROOF STATE]
proof (state)
this:
s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (vs @ [1]))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (?vs @ [1]))

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (?vs @ [1]))
[PROOF STEP]
have "s (list_encode (vs @ [0])) \<noteq> s (list_encode vs) \<or>
      s (list_encode (vs @ [1])) \<noteq> s (list_encode vs)"
      for vs
[PROOF STATE]
proof (prove)
using this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode (?vs @ [1]))

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (vs @ [0])) \<noteq> s (Partial_Recursive.list_encode vs) \<or> s (Partial_Recursive.list_encode (vs @ [1])) \<noteq> s (Partial_Recursive.list_encode vs)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode ?vs) \<or> s (Partial_Recursive.list_encode (?vs @ [1])) \<noteq> s (Partial_Recursive.list_encode ?vs)

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode ?vs) \<or> s (Partial_Recursive.list_encode (?vs @ [1])) \<noteq> s (Partial_Recursive.list_encode ?vs)
[PROOF STEP]
have "s (list_encode (prefixes i (Suc x))) \<noteq> s (list_encode (prefixes i x))" for i x
[PROOF STATE]
proof (prove)
using this:
s (Partial_Recursive.list_encode (?vs @ [0])) \<noteq> s (Partial_Recursive.list_encode ?vs) \<or> s (Partial_Recursive.list_encode (?vs @ [1])) \<noteq> s (Partial_Recursive.list_encode ?vs)

goal (1 subgoal):
 1. s (Partial_Recursive.list_encode (prefixes i (Suc x))) \<noteq> s (Partial_Recursive.list_encode (prefixes i x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s (Partial_Recursive.list_encode (prefixes ?i (Suc ?x))) \<noteq> s (Partial_Recursive.list_encode (prefixes ?i ?x))

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s (Partial_Recursive.list_encode (prefixes ?i (Suc ?x))) \<noteq> s (Partial_Recursive.list_encode (prefixes ?i ?x))
[PROOF STEP]
have "\<not> learn_lim \<phi> {\<psi> i} s" for i
[PROOF STATE]
proof (prove)
using this:
s (Partial_Recursive.list_encode (prefixes ?i (Suc ?x))) \<noteq> s (Partial_Recursive.list_encode (prefixes ?i ?x))

goal (1 subgoal):
 1. \<not> learn_lim \<phi> {\<psi> i} s
[PROOF STEP]
using psi_def psi_init always_hyp_change_not_Lim
[PROOF STATE]
proof (prove)
using this:
s (Partial_Recursive.list_encode (prefixes ?i (Suc ?x))) \<noteq> s (Partial_Recursive.list_encode (prefixes ?i ?x))
\<psi> ?i ?x \<equiv> Some (last (prefixes ?i ?x))
\<psi> ?i \<triangleright> ?x = Partial_Recursive.list_encode (prefixes ?i ?x)
(\<And>x. ?s (?f \<triangleright> Suc x) \<noteq> ?s (?f \<triangleright> x)) \<Longrightarrow> \<not> learn_lim ?\<psi> {?f} ?s

goal (1 subgoal):
 1. \<not> learn_lim \<phi> {\<psi> i} s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> learn_lim \<phi> {\<psi> ?i} s

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> learn_lim \<phi> {\<psi> ?i} s
[PROOF STEP]
have "\<not> learn_lim \<phi> U_LIMCONS s"
[PROOF STATE]
proof (prove)
using this:
\<not> learn_lim \<phi> {\<psi> ?i} s

goal (1 subgoal):
 1. \<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s
[PROOF STEP]
using ex_psi_in_U learn_lim_closed_subseteq
[PROOF STATE]
proof (prove)
using this:
\<not> learn_lim \<phi> {\<psi> ?i} s
\<exists>j. \<psi> j \<in> U\<^bsub>LIM-CONS\<^esub>
\<lbrakk>learn_lim ?\<psi> ?U ?s; ?V \<subseteq> ?U\<rbrakk> \<Longrightarrow> learn_lim ?\<psi> ?V ?s

goal (1 subgoal):
 1. \<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. False
[PROOF STEP]
using learn learn_cons_def
[PROOF STATE]
proof (prove)
using this:
\<not> learn_lim \<phi> U\<^bsub>LIM-CONS\<^esub> s
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s
learn_cons ?\<psi> ?U ?s \<equiv> learn_lim ?\<psi> ?U ?s \<and> (\<forall>f\<in>?U. \<forall>n k. k \<le> n \<longrightarrow> ?\<psi> (the (?s (f \<triangleright> n))) k = f k)

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma U_LIMCONS_not_in_CONS: "U\<^bsub>LIM-CONS\<^esub> \<notin> CONS"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<notin> CONS
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
assume "U\<^bsub>LIM-CONS\<^esub> \<in> CONS"
[PROOF STATE]
proof (state)
this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS
[PROOF STEP]
have "U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>"
[PROOF STATE]
proof (prove)
using this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>
[PROOF STEP]
by (simp add: CONS_wrt_phi_eq_CONS)
[PROOF STATE]
proof (state)
this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>
[PROOF STEP]
obtain almost_s where "learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s"
[PROOF STATE]
proof (prove)
using this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>

goal (1 subgoal):
 1. (\<And>almost_s. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using CONS_wrt_def
[PROOF STATE]
proof (prove)
using this:
U\<^bsub>LIM-CONS\<^esub> \<in> CONS_wrt \<phi>
CONS_wrt ?\<psi> \<equiv> {U. \<exists>s. learn_cons ?\<psi> U s}

goal (1 subgoal):
 1. (\<And>almost_s. learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s
[PROOF STEP]
obtain s where s: "total1 s" "learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s"
[PROOF STATE]
proof (prove)
using this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>total1 s; learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using U_LIMCONS_prefix_complete U_prefix_complete_imp_total_strategy
[PROOF STATE]
proof (prove)
using this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> almost_s
0 < length ?vs \<Longrightarrow> \<exists>f\<in>U\<^bsub>LIM-CONS\<^esub>. prefix f (length ?vs - 1) = ?vs
\<lbrakk>\<And>vs. 0 < length vs \<Longrightarrow> \<exists>f\<in>?U. prefix f (length vs - 1) = vs; learn_cons ?\<psi> ?U ?s\<rbrakk> \<Longrightarrow> \<exists>t. total1 t \<and> learn_cons ?\<psi> ?U t

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>total1 s; learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
total1 s
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
total1 s
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s
[PROOF STEP]
have "s \<in> \<R>"
[PROOF STATE]
proof (prove)
using this:
total1 s
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. s \<in> \<R>
[PROOF STEP]
using learn_consE(1) P1_total_imp_R1
[PROOF STATE]
proof (prove)
using this:
total1 s
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s
learn_cons ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>?f \<in> \<P>; total1 ?f\<rbrakk> \<Longrightarrow> ?f \<in> \<R>

goal (1 subgoal):
 1. s \<in> \<R>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s \<in> \<R>

goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
with cons_lim_def
[PROOF STATE]
proof (chain)
picking this:
cons_lim ?s \<equiv> ?s \<in> \<R>
s \<in> \<R>
[PROOF STEP]
interpret cons_lim s
[PROOF STATE]
proof (prove)
using this:
cons_lim ?s \<equiv> ?s \<in> \<R>
s \<in> \<R>

goal (1 subgoal):
 1. cons_lim s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U\<^bsub>LIM-CONS\<^esub> \<in> CONS \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using s(2) U_LIMCONS_not_learn_cons
[PROOF STATE]
proof (prove)
using this:
learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s
\<not> learn_cons \<phi> U\<^bsub>LIM-CONS\<^esub> s

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem CONS_subset_Lim: "CONS \<subset> LIM"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CONS \<subset> LIM
[PROOF STEP]
using U_LIMCONS_in_Lim U_LIMCONS_not_in_CONS CONS_subseteq_Lim
[PROOF STATE]
proof (prove)
using this:
U\<^bsub>LIM-CONS\<^esub> \<in> LIM
U\<^bsub>LIM-CONS\<^esub> \<notin> CONS
CONS \<subseteq> LIM

goal (1 subgoal):
 1. CONS \<subset> LIM
[PROOF STEP]
by auto


[STATEMENT]
lemma INF_partition_nat3:
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice"
  shows "(\<Sqinter>j. f i j) =
    (\<Sqinter>j\<in>{j. i = j}. f i j) \<sqinter>
    (\<Sqinter>j\<in>{j. i < j}. f i j) \<sqinter>
    (\<Sqinter>j\<in>{j. j < i}. f i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> range (f i) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sqinter> range (f i) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have univ_part: "UNIV = {j. i = j} \<union> {j. i < j} \<union> {j. j < i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {j::nat. i = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i}
variables:
i :: nat
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNIV = {j::nat. (i::nat) = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i}

goal (1 subgoal):
 1. \<Sqinter> range (f i) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have "(\<Sqinter>j \<in> {j. i = j} \<union> {j. i < j} \<union> {j. j < i}. f i j) =
          (\<Sqinter>j\<in>{j. i = j}. f i j) \<sqinter>
          (\<Sqinter>j\<in>{j. i < j}. f i j) \<sqinter>
          (\<Sqinter>j\<in>{j. j < i}. f i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f i ` ({j::nat. i = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i})) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (metis INF_union)
[PROOF STATE]
proof (state)
this:
\<Sqinter> ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) (i::nat) ` ({j::nat. i = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i})) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})

goal (1 subgoal):
 1. \<Sqinter> range (f i) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
with univ_part
[PROOF STATE]
proof (chain)
picking this:
UNIV = {j::nat. (i::nat) = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i}
\<Sqinter> ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) (i::nat) ` ({j::nat. i = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i})) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
UNIV = {j::nat. (i::nat) = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i}
\<Sqinter> ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) (i::nat) ` ({j::nat. i = j} \<union> {j::nat. i < j} \<union> {j::nat. j < i})) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})

goal (1 subgoal):
 1. \<Sqinter> range (f i) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) (i::nat)) = \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})

goal:
No subgoals!
variables:
i :: nat
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
qed


[STATEMENT]
lemma INF_INF_partition_nat3:
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice"
  shows "(\<Sqinter>i. \<Sqinter>j. f i j) =
    (\<Sqinter>i. \<Sqinter>j\<in>{j. i = j}. f i j) \<sqinter>
    (\<Sqinter>i. \<Sqinter>j\<in>{j. i < j}. f i j) \<sqinter>
    (\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have "(\<Sqinter>i. \<Sqinter>j. f i j) = (\<Sqinter>i. ((\<Sqinter>j\<in>{j. i = j}. f i j) \<sqinter>
                                  (\<Sqinter>j\<in>{j. i < j}. f i j) \<sqinter>
                                  (\<Sqinter>j\<in>{j. j < i}. f i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (simp add: INF_partition_nat3)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i}))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i}))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have "... = (\<Sqinter>i. \<Sqinter>j\<in>{j. i = j}. f i j) \<sqinter>
                   (\<Sqinter>i. \<Sqinter>j\<in>{j. i < j}. f i j) \<sqinter>
                   (\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f i j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (simp add: INF_inf_distrib)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter> ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i ` {j::nat. i = j}) \<sqinter> \<Sqinter> (f i ` {j::nat. i < j}) \<sqinter> \<Sqinter> (f i ` {j::nat. j < i})) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>i::nat. \<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>i::nat. \<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter> range (f i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter> range ((f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) i)) = (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i = j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. i < j})) \<sqinter> (\<Sqinter>i::nat. \<Sqinter> (f i ` {j::nat. j < i}))

goal:
No subgoals!
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
qed


[STATEMENT]
lemma INF_nat_shift: "(\<Sqinter>i\<in>{i. 0 < i}. f i) = (\<Sqinter>i. f (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f ` {i::nat. (0::nat) < i}) = (\<Sqinter>i::nat. f (Suc i))
variables:
f :: nat \<Rightarrow> 'a
type variables:
'a :: Inf
[PROOF STEP]
by (metis greaterThan_0 greaterThan_def range_composition)


[STATEMENT]
lemma INF_nat_minus:
  fixes f :: "nat \<Rightarrow> 'a::refinement_lattice"
  shows "(\<Sqinter>j\<in>{j. i < j}. f (j - i)) = (\<Sqinter>k\<in>{k. 0 < k}. f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>j::nat\<in>{j::nat. i < j}. f (j - i)) = \<Sqinter> (f ` {k::nat. (0::nat) < k})
variables:
i :: nat
f :: nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sqinter>j::nat\<in>{j::nat. i < j}. f (j - i)) \<sqsubseteq> \<Sqinter> (f ` {k::nat. (0::nat) < k})
 2. \<Sqinter> (f ` {k::nat. (0::nat) < k}) \<sqsubseteq> (\<Sqinter>j::nat\<in>{j::nat. i < j}. f (j - i))
variables:
i :: nat
f :: nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
apply (rule INF_mono, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m::nat. (0::nat) < m \<Longrightarrow> \<exists>j>i. f (j - i) \<sqsubseteq> f m
 2. \<Sqinter> (f ` {k::nat. (0::nat) < k}) \<sqsubseteq> (\<Sqinter>j::nat\<in>{j::nat. i < j}. f (j - i))
variables:
f :: nat \<Rightarrow> 'a
i :: nat
type variables:
'a :: refinement_lattice
[PROOF STEP]
apply (metis add.right_neutral add_diff_cancel_left' add_less_cancel_left order_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sqinter> (f ` {k::nat. (0::nat) < k}) \<sqsubseteq> (\<Sqinter>j::nat\<in>{j::nat. i < j}. f (j - i))
variables:
i :: nat
f :: nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
apply (rule INF_mono, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m::nat. i < m \<Longrightarrow> \<exists>k>0::nat. f k \<sqsubseteq> f (m - i)
variables:
f :: nat \<Rightarrow> 'a
i :: nat
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (meson order_refl zero_less_diff)


[STATEMENT]
lemma INF_INF_guarded_switch:
  fixes f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice"
  shows "(\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j)) = (\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) = (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
proof (rule antisym)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have "\<And>jj ii. jj < ii \<Longrightarrow> \<exists>i. \<exists>j<i. f j (i - j) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>(jj::nat) ii::nat. jj < ii \<Longrightarrow> \<exists>(i::nat) j::nat. j < i \<and> f j (i - j) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(i::nat) j::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(i::nat) j::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>jj ii. jj < ii \<Longrightarrow> \<exists>i. (\<Sqinter>j\<in>{j. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(i::nat) j::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>(jj::nat) ii::nat. jj < ii \<Longrightarrow> \<exists>i::nat. (\<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (meson INF_lower mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>i::nat. (\<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>i::nat. (\<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>jj ii. jj < ii \<Longrightarrow> (\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>i::nat. (\<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>(jj::nat) ii::nat. jj < ii \<Longrightarrow> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (meson UNIV_I INF_lower dual_order.trans)
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>jj. (\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>ii\<in>{ii. jj < ii}. f jj (ii - jj))"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>jj::nat. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat\<in>{ii::nat. jj < ii}. f jj (ii - jj))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (metis (mono_tags, lifting) INF_greatest mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat\<in>{ii::nat. ?jj < ii}. f (?jj::nat) (ii - ?jj))

goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat\<in>{ii::nat. ?jj < ii}. f (?jj::nat) (ii - ?jj))
[PROOF STEP]
have "(\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>jj. \<Sqinter>ii\<in>{ii. jj < ii}. f jj (ii - jj))"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat\<in>{ii::nat. ?jj < ii}. f (?jj::nat) (ii - ?jj))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat. \<Sqinter>ii::nat\<in>{ii::nat. jj < ii}. f jj (ii - jj))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (simp add: INF_greatest)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat. \<Sqinter>ii::nat\<in>{ii::nat. jj < ii}. f jj (ii - jj))

goal (2 subgoals):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
 2. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat. \<Sqinter>ii::nat\<in>{ii::nat. jj < ii}. f jj (ii - jj))
[PROOF STEP]
show "(\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j))"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat. \<Sqinter>ii::nat\<in>{ii::nat. jj < ii}. f jj (ii - jj))

goal (1 subgoal):
 1. (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j))

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
have "\<And>ii jj. jj < ii \<Longrightarrow> \<exists>j. \<exists>i>j. f j (i - j) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>(ii::nat) jj::nat. jj < ii \<Longrightarrow> \<exists>(j::nat) i::nat. j < i \<and> f j (i - j) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(j::nat) i::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(j::nat) i::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>ii jj. jj < ii \<Longrightarrow> \<exists>j. (\<Sqinter>i\<in>{i. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>(j::nat) i::nat. j < i \<and> (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>(ii::nat) jj::nat. jj < ii \<Longrightarrow> \<exists>j::nat. (\<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (meson INF_lower mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>j::nat. (\<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>j::nat. (\<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>ii jj. jj < ii \<Longrightarrow> (\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> \<exists>j::nat. (\<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>(ii::nat) jj::nat. jj < ii \<Longrightarrow> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> f jj (ii - jj)
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (meson UNIV_I INF_lower dual_order.trans)
[PROOF STATE]
proof (state)
this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)
[PROOF STEP]
have "\<And>ii. (\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>jj\<in>{jj. jj < ii}. f jj (ii - jj))"
[PROOF STATE]
proof (prove)
using this:
(?jj::nat) < (?ii::nat) \<Longrightarrow> (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> f ?jj (?ii - ?jj)

goal (1 subgoal):
 1. \<And>ii::nat. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat\<in>{jj::nat. jj < ii}. f jj (ii - jj))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (metis (mono_tags, lifting) INF_greatest mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat\<in>{jj::nat. jj < ?ii}. f jj ((?ii::nat) - jj))

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat\<in>{jj::nat. jj < ?ii}. f jj ((?ii::nat) - jj))
[PROOF STEP]
have "(\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>ii. \<Sqinter>jj\<in>{jj. jj < ii}. f jj (ii - jj))"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>jj::nat\<in>{jj::nat. jj < ?ii}. f jj ((?ii::nat) - jj))

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat. \<Sqinter>jj::nat\<in>{jj::nat. jj < ii}. f jj (ii - jj))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by (simp add: INF_greatest)
[PROOF STATE]
proof (state)
this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat. \<Sqinter>jj::nat\<in>{jj::nat. jj < ii}. f jj (ii - jj))

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat. \<Sqinter>jj::nat\<in>{jj::nat. jj < ii}. f jj (ii - jj))
[PROOF STEP]
show "(\<Sqinter>j. \<Sqinter>i\<in>{i. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i. \<Sqinter>j\<in>{j. j < i}. f j (i - j))"
[PROOF STATE]
proof (prove)
using this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>ii::nat. \<Sqinter>jj::nat\<in>{jj::nat. jj < ii}. f jj (ii - jj))

goal (1 subgoal):
 1. (\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. f j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sqinter>j::nat. \<Sqinter>i::nat\<in>{i::nat. j < i}. (f::nat \<Rightarrow> nat \<Rightarrow> 'a::refinement_lattice) j (i - j)) \<sqsubseteq> (\<Sqinter>i::nat. \<Sqinter>j::nat\<in>{j::nat. j < i}. f j (i - j))

goal:
No subgoals!
variables:
f :: nat \<Rightarrow> nat \<Rightarrow> 'a
type variables:
'a :: refinement_lattice
[PROOF STEP]
qed


[STATEMENT]
lemma "True \<or> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<or> False
[PROOF STEP]
find_proof Hammer1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<or> False
[PROOF STEP]
oops


[STATEMENT]
lemma "True \<or> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<or> False
[PROOF STEP]
find_proof Hammer2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<or> False
[PROOF STEP]
oops


[STATEMENT]
lemma "True \<and> True \<or> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<and> True \<or> False
[PROOF STEP]
find_proof UserSimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<and> True \<or> False
[PROOF STEP]
oops


[STATEMENT]
lemma "QQ = PP"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. QQ = PP
[PROOF STEP]
find_proof IfMatchRuleExt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. QQ = PP
[PROOF STEP]
oops


[STATEMENT]
lemma "my_foo"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. my_foo
[PROOF STEP]
find_proof UserSimp2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. my_foo
[PROOF STEP]
oops


[STATEMENT]
lemma "\<And>xs .((case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. (case xs of [] \<Rightarrow> [] | y # ys \<Rightarrow> xs) = xs
[PROOF STEP]
find_proof CaseTac
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. (case xs of [] \<Rightarrow> [] | y # ys \<Rightarrow> xs) = xs
[PROOF STEP]
oops


[STATEMENT]
lemma "True" and "True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True &&& True
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. True
 2. True
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
find_proof MultiFF
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True
[PROOF STEP]
oops


[STATEMENT]
lemma "True" and "True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True &&& True
[PROOF STEP]
find_proof Auto2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True &&& True
[PROOF STEP]
oops


[STATEMENT]
lemma "foo 8 90"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foo (8::'a) (90::'a)
[PROOF STEP]
find_proof Hammer1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foo (8::'a) (90::'a)
[PROOF STEP]
try_hard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foo (8::'a) (90::'a)
[PROOF STEP]
oops


[STATEMENT]
lemma assumes D shows "B \<longrightarrow> B \<or> C" and "D" and "D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<longrightarrow> B \<or> C &&& D &&& D
[PROOF STEP]
try_hard
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<longrightarrow> B \<or> C &&& D &&& D
[PROOF STEP]
oops


[STATEMENT]
lemma shows "True" and "False" and "True" and "True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True &&& False) &&& True &&& True
[PROOF STEP]
find_proof Simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (True &&& False) &&& True &&& True
[PROOF STEP]
oops


[STATEMENT]
lemma state_safety:"safe_state (x::bool) (y::bool) = True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. safe_state x y = True
[PROOF STEP]
apply normalization
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cnjct2:
shows 1:"ps_safe p s"
 and  2:"valid_trans p s s' x"
 and  3:"ps_safe p s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps_safe p s &&& valid_trans p s s' x &&& ps_safe p s'
[PROOF STEP]
find_proof Hammer_Or_Defer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps_safe p s &&& valid_trans p s s' x &&& ps_safe p s'
[PROOF STEP]
(* very slow *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps_safe p s &&& valid_trans p s s' x &&& ps_safe p s'
[PROOF STEP]
oops


[STATEMENT]
lemma "True \<and> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<and> True
[PROOF STEP]
find_proof testCut
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<and> True
[PROOF STEP]
oops


[STATEMENT]
lemma trace_ft_append: "trace_between s (tr1@tr2) s'
  \<longleftrightarrow> (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh tr2 s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_between s (tr1 @ tr2) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh tr2 s')
[PROOF STEP]
apply (induction tr2 arbitrary: s' rule: rev_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s'. trace_between s (tr1 @ []) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh [] s')
 2. \<And>x xs s'. (\<And>s'. trace_between s (tr1 @ xs) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh xs s')) \<Longrightarrow> trace_between s (tr1 @ xs ## x) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh (xs ## x) s')
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs s'. (\<And>s'. trace_between s (tr1 @ xs) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh xs s')) \<Longrightarrow> trace_between s (tr1 @ xs ## x) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh (xs ## x) s')
[PROOF STEP]
apply (subst append_assoc[symmetric], subst trace_ft_snoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xs s'. (\<And>s'. trace_between s (tr1 @ xs) s' = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh xs s')) \<Longrightarrow> (\<exists>sh a ou. x = Trans sh a ou s' \<and> trace_between s (tr1 @ xs) sh \<and> step sh a = (ou, s')) = (\<exists>sh. trace_between s tr1 sh \<and> trace_between sh (xs ## x) s')
[PROOF STEP]
apply (auto simp: trace_ft_snoc)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma trace_ft_Cons: "trace_between s (trn#tr) s'
  \<longleftrightarrow> (\<exists>sh ou a. trn = Trans s a ou sh \<and> step s a = (ou,sh) \<and> trace_between sh tr s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_between s (trn # tr) s' = (\<exists>sh ou a. trn = Trans s a ou sh \<and> step s a = (ou, sh) \<and> trace_between sh tr s')
[PROOF STEP]
apply (subst trace_ft_append[where ?tr1.0 = "[trn]", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>sh. trace_between s [trn] sh \<and> trace_between sh tr s') = (\<exists>sh ou a. trn = Trans s a ou sh \<and> step s a = (ou, sh) \<and> trace_between sh tr s')
[PROOF STEP]
apply (subst trace_ft_snoc[where tr = "[]", simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>sh. (\<exists>a ou. trn = Trans s a ou sh \<and> step s a = (ou, sh)) \<and> trace_between sh tr s') = (\<exists>sh ou a. trn = Trans s a ou sh \<and> step s a = (ou, sh) \<and> trace_between sh tr s')
[PROOF STEP]
by auto


[STATEMENT]
lemma trace_to_ft: "trace_to tr s \<longleftrightarrow> trace_between istate tr s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. trace_to tr s = trace_between istate tr s
[PROOF STEP]
proof (rule,goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. trace_to tr s \<Longrightarrow> trace_between istate tr s
 2. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
trace_to tr s

goal (2 subgoals):
 1. trace_to tr s \<Longrightarrow> trace_between istate tr s
 2. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
trace_to tr s

goal (1 subgoal):
 1. trace_between istate tr s
[PROOF STEP]
by induction (auto intro: trace_between.intros)
[PROOF STATE]
proof (state)
this:
trace_between istate tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
trace_between istate tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trace_between istate tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
trace_between istate tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
fix s'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
assume "trace_between s' tr s"
[PROOF STATE]
proof (state)
this:
trace_between s' tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
hence "s' = istate \<longrightarrow> trace_to tr s"
[PROOF STATE]
proof (prove)
using this:
trace_between s' tr s

goal (1 subgoal):
 1. s' = istate \<longrightarrow> trace_to tr s
[PROOF STEP]
by induction (auto intro: trace_to.intros)
[PROOF STATE]
proof (state)
this:
s' = istate \<longrightarrow> trace_to tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
trace_between ?s'2 tr s \<Longrightarrow> ?s'2 = istate \<longrightarrow> trace_to tr s

goal (1 subgoal):
 1. trace_between istate tr s \<Longrightarrow> trace_to tr s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trace_between istate tr s
trace_between ?s'2 tr s \<Longrightarrow> ?s'2 = istate \<longrightarrow> trace_to tr s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
trace_between istate tr s
trace_between ?s'2 tr s \<Longrightarrow> ?s'2 = istate \<longrightarrow> trace_to tr s

goal (1 subgoal):
 1. trace_to tr s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
trace_to tr s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trace_to_reach: assumes "trace_to tr s" shows "reach s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
trace_to tr s

goal (1 subgoal):
 1. reach s
[PROOF STEP]
apply induction
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. reach istate
 2. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; reach s; step s a = (ou, s')\<rbrakk> \<Longrightarrow> reach s'
[PROOF STEP]
apply (rule reach.intros)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>trace_to tr s; reach s; step s a = (ou, s')\<rbrakk> \<Longrightarrow> reach s'
[PROOF STEP]
by (metis reach_step snd_conv)


[STATEMENT]
lemma reach_to_trace: assumes "reach s" obtains tr where "trace_to tr s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>tr. trace_to tr s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
reach s

goal (1 subgoal):
 1. (\<And>tr. trace_to tr s \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (induction rule: reach_step_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<And>tr. trace_to tr istate \<Longrightarrow> thesis) \<Longrightarrow> thesis
 2. \<And>s a. \<lbrakk>reach s; (\<And>tr. trace_to tr s \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>tr. trace_to tr (snd (step s a)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (auto intro: trace_to.intros) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s a. \<lbrakk>reach s; (\<And>tr. trace_to tr s \<Longrightarrow> thesis) \<Longrightarrow> thesis; \<And>tr. trace_to tr (snd (step s a)) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis surjective_pairing trace_to.step)


[STATEMENT]
lemma reach_trace_to_conv: "reach s \<longleftrightarrow> (\<exists>tr. trace_to tr s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reach s = (\<exists>tr. trace_to tr s)
[PROOF STEP]
by (blast intro: trace_to_reach elim: reach_to_trace)


[STATEMENT]
lemma trace_to_induct[case_names empty step, induct set]:
  "\<lbrakk>trace_to x1 x2; P [] istate;
  \<And>tr s a ou s'.
    \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk>
    \<Longrightarrow> P (tr ## Trans s a ou s') s'\<rbrakk>
  \<Longrightarrow> P x1 x2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_to x1 x2; P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'\<rbrakk> \<Longrightarrow> P x1 x2
[PROOF STEP]
apply (erule trace_to.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'\<rbrakk> \<Longrightarrow> P [] istate
 2. \<And>tr s a ou s'. \<lbrakk>P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'; trace_to tr s; P tr s; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'; trace_to tr s; P tr s; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'
[PROOF STEP]
apply (frule trace_to_reach)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'; trace_to tr s; P tr s; step s a = (ou, s'); reach s\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'
[PROOF STEP]
using reach_PairI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>reach ?s; step ?s ?a = (?ou, ?s')\<rbrakk> \<Longrightarrow> reach ?s'

goal (1 subgoal):
 1. \<And>tr s a ou s'. \<lbrakk>P [] istate; \<And>tr s a ou s'. \<lbrakk>trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'; trace_to tr s; P tr s; step s a = (ou, s'); reach s\<rbrakk> \<Longrightarrow> P (tr ## Trans s a ou s') s'
[PROOF STEP]
by blast