[STATEMENT]
lemma Sup_upto_llist_subset_Sup_llist: "Sup_upto_llist Xs j \<subseteq> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sup_upto_llist Xs j \<subseteq> Sup_llist Xs
[PROOF STEP]
unfolding Sup_llist_def Sup_upto_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> j}) \<subseteq> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by auto


[STATEMENT]
lemma elem_Sup_llist_imp_Sup_upto_llist:
  "x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j < llength Xs. x \<in> Sup_upto_llist Xs (enat j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j. enat j < llength Xs \<and> x \<in> Sup_upto_llist Xs (enat j)
[PROOF STEP]
unfolding Sup_llist_def Sup_upto_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<Union> (lnth Xs ` {i. enat i < llength Xs}) \<Longrightarrow> \<exists>j. enat j < llength Xs \<and> x \<in> \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> enat j})
[PROOF STEP]
by blast


[STATEMENT]
lemma lnth_subset_Sup_upto_llist: "j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs (enat j)
[PROOF STEP]
unfolding Sup_upto_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> \<Union> (lnth Xs ` {i. enat i < llength Xs \<and> enat i \<le> enat j})
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_Sup_llist_imp_Sup_upto_llist:
  assumes "finite X" and "X \<subseteq> Sup_llist Xs"
  shows "\<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite X
X \<subseteq> Sup_llist Xs

goal (1 subgoal):
 1. \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
proof induct
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
case (insert x X)
[PROOF STATE]
proof (state)
this:
finite X
x \<notin> X
X \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)
insert x X \<subseteq> Sup_llist Xs

goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
X \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)
insert x X \<subseteq> Sup_llist Xs
[PROOF STEP]
have x: "x \<in> Sup_llist Xs" and X: "X \<subseteq> Sup_llist Xs"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
X \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)
insert x X \<subseteq> Sup_llist Xs

goal (1 subgoal):
 1. x \<in> Sup_llist Xs &&& X \<subseteq> Sup_llist Xs
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<in> Sup_llist Xs
X \<subseteq> Sup_llist Xs

goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
from x
[PROOF STATE]
proof (chain)
picking this:
x \<in> Sup_llist Xs
[PROOF STEP]
obtain k where k: "x \<in> Sup_upto_llist Xs (enat k)"
[PROOF STATE]
proof (prove)
using this:
x \<in> Sup_llist Xs

goal (1 subgoal):
 1. (\<And>k. x \<in> Sup_upto_llist Xs (enat k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using elem_Sup_llist_imp_Sup_upto_llist
[PROOF STATE]
proof (prove)
using this:
x \<in> Sup_llist Xs
?x \<in> Sup_llist ?Xs \<Longrightarrow> \<exists>j. enat j < llength ?Xs \<and> ?x \<in> Sup_upto_llist ?Xs (enat j)

goal (1 subgoal):
 1. (\<And>k. x \<in> Sup_upto_llist Xs (enat k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> Sup_upto_llist Xs (enat k)

goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
from X
[PROOF STATE]
proof (chain)
picking this:
X \<subseteq> Sup_llist Xs
[PROOF STEP]
obtain k' where k': "X \<subseteq> Sup_upto_llist Xs (enat k')"
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Sup_llist Xs

goal (1 subgoal):
 1. (\<And>k'. X \<subseteq> Sup_upto_llist Xs (enat k') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert.hyps(3)
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> Sup_llist Xs
X \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. X \<subseteq> Sup_upto_llist Xs (enat k)

goal (1 subgoal):
 1. (\<And>k'. X \<subseteq> Sup_upto_llist Xs (enat k') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
X \<subseteq> Sup_upto_llist Xs (enat k')

goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
have "insert x X \<subseteq> Sup_upto_llist Xs (max k k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x X \<subseteq> Sup_upto_llist Xs (enat (max k k'))
[PROOF STEP]
using k k'
[PROOF STATE]
proof (prove)
using this:
x \<in> Sup_upto_llist Xs (enat k)
X \<subseteq> Sup_upto_llist Xs (enat k')

goal (1 subgoal):
 1. insert x X \<subseteq> Sup_upto_llist Xs (enat (max k k'))
[PROOF STEP]
by (metis (mono_tags) Sup_upto_llist_mono enat_ord_simps(1) insert_subset
      max.cobounded1 max.cobounded2 subset_iff)
[PROOF STATE]
proof (state)
this:
insert x X \<subseteq> Sup_upto_llist Xs (enat (max k k'))

goal (2 subgoals):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. F \<subseteq> Sup_upto_llist Xs (enat k); insert x F \<subseteq> Sup_llist Xs\<rbrakk> \<Longrightarrow> \<exists>k. insert x F \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert x X \<subseteq> Sup_upto_llist Xs (enat (max k k'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
insert x X \<subseteq> Sup_upto_llist Xs (enat (max k k'))

goal (1 subgoal):
 1. \<exists>k. insert x X \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>k. insert x X \<subseteq> Sup_upto_llist Xs (enat k)

goal (1 subgoal):
 1. {} \<subseteq> Sup_llist Xs \<Longrightarrow> \<exists>k. {} \<subseteq> Sup_upto_llist Xs (enat k)
[PROOF STEP]
qed simp


[STATEMENT]
lemma Liminf_llist_LNil[simp]: "Liminf_llist LNil = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist LNil = {}
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength LNil}. \<Inter> (lnth LNil ` {j. i \<le> j \<and> enat j < llength LNil})) = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma Liminf_llist_LCons:
  "Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
proof (cases "lnull Xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
 2. \<not> lnull Xs \<Longrightarrow> Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
case nnull: False
[PROOF STATE]
proof (state)
this:
\<not> lnull Xs

goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
 2. \<not> lnull Xs \<Longrightarrow> Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
assume "\<exists>i. enat i \<le> llength Xs
        \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)

goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)
[PROOF STEP]
have "\<exists>i. enat (Suc i) \<le> llength Xs
        \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)

goal (1 subgoal):
 1. \<exists>i. enat (Suc i) \<le> llength Xs \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)
[PROOF STEP]
by (cases "llength Xs",
            metis not_lnull_conv[THEN iffD1, OF nnull] Suc_le_D eSuc_enat eSuc_ile_mono
              llength_LCons not_less_eq_eq zero_enat_def zero_le,
            metis Suc_leD enat_ord_code(3))
[PROOF STATE]
proof (state)
this:
\<exists>i. enat (Suc i) \<le> llength Xs \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)

goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. enat (Suc i) \<le> llength Xs \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)
[PROOF STEP]
have "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. enat (Suc i) \<le> llength Xs \<and> (\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)

goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)
[PROOF STEP]
by (metis Suc_ile_eq Suc_n_not_le_n lift_Suc_mono_le lnth_Suc_LCons nat_le_linear)
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)

goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j) \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j)

goal (2 subgoals):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
 2. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j) \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j)
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j) \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j)

goal (1 subgoal):
 1. Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
[PROOF STATE]
proof (state)
this:
Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Liminf_llist (LCons X Xs) \<subseteq> (if lnull Xs then X else Liminf_llist Xs)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
assume "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)
[PROOF STEP]
obtain i where
        i: "enat i < llength Xs" and
        j: "\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength Xs; \<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enat i < llength Xs
\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
have "enat (Suc i) \<le> llength Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat (Suc i) \<le> llength Xs
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
enat i < llength Xs

goal (1 subgoal):
 1. enat (Suc i) \<le> llength Xs
[PROOF STEP]
by (simp add: Suc_ile_eq)
[PROOF STATE]
proof (state)
this:
enat (Suc i) \<le> llength Xs

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat (Suc i) \<le> llength Xs

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
have "\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j
[PROOF STEP]
using Suc_ile_eq Suc_le_D j
[PROOF STATE]
proof (prove)
using this:
(enat (Suc ?m) \<le> ?n) = (enat ?m < ?n)
Suc ?n \<le> ?m' \<Longrightarrow> \<exists>m. ?m' = Suc m
\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j

goal (1 subgoal):
 1. \<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat (Suc i) \<le> llength Xs
\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j
[PROOF STEP]
have "\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow>
        x \<in> lnth (LCons X Xs) j)"
[PROOF STATE]
proof (prove)
using this:
enat (Suc i) \<le> llength Xs
\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j

goal (1 subgoal):
 1. \<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j) \<Longrightarrow> \<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j) \<Longrightarrow> \<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j)
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
using this:
\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> ?x2 \<in> lnth Xs j) \<Longrightarrow> \<exists>i. enat i \<le> llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> ?x2 \<in> lnth (LCons X Xs) j)

goal (1 subgoal):
 1. (if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)
[PROOF STEP]
by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
[PROOF STATE]
proof (state)
this:
(if lnull Xs then X else Liminf_llist Xs) \<subseteq> Liminf_llist (LCons X Xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)

goal (1 subgoal):
 1. lnull Xs \<Longrightarrow> Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)
[PROOF STEP]
qed (simp add: Liminf_llist_def enat_0_iff(1))


[STATEMENT]
lemma lfinite_Liminf_llist: "lfinite Xs \<Longrightarrow> Liminf_llist Xs = (if lnull Xs then {} else llast Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite Xs \<Longrightarrow> Liminf_llist Xs = (if lnull Xs then {} else llast Xs)
[PROOF STEP]
proof (induction rule: lfinite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. lnull xs \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
 2. \<And>xs. \<lbrakk>lfinite xs; \<not> lnull xs; Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))\<rbrakk> \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
[PROOF STEP]
case (LCons xs)
[PROOF STATE]
proof (state)
this:
lfinite xs
\<not> lnull xs
Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))

goal (2 subgoals):
 1. \<And>xs. lnull xs \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
 2. \<And>xs. \<lbrakk>lfinite xs; \<not> lnull xs; Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))\<rbrakk> \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lfinite xs
\<not> lnull xs
Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))
[PROOF STEP]
obtain y ys where
    xs: "xs = LCons y ys"
[PROOF STATE]
proof (prove)
using this:
lfinite xs
\<not> lnull xs
Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))

goal (1 subgoal):
 1. (\<And>y ys. xs = LCons y ys \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson not_lnull_conv)
[PROOF STATE]
proof (state)
this:
xs = LCons y ys

goal (2 subgoals):
 1. \<And>xs. lnull xs \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
 2. \<And>xs. \<lbrakk>lfinite xs; \<not> lnull xs; Liminf_llist (ltl xs) = (if lnull (ltl xs) then {} else llast (ltl xs))\<rbrakk> \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist xs = (if lnull xs then {} else llast xs)
[PROOF STEP]
unfolding xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (LCons y ys) = (if lnull (LCons y ys) then {} else llast (LCons y ys))
[PROOF STEP]
by (simp add: Liminf_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
[PROOF STATE]
proof (state)
this:
Liminf_llist xs = (if lnull xs then {} else llast xs)

goal (1 subgoal):
 1. \<And>xs. lnull xs \<Longrightarrow> Liminf_llist xs = (if lnull xs then {} else llast xs)
[PROOF STEP]
qed (simp add: Liminf_llist_def)


[STATEMENT]
lemma Liminf_llist_ltl: "\<not> lnull (ltl Xs) \<Longrightarrow> Liminf_llist Xs = Liminf_llist (ltl Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> lnull (ltl Xs) \<Longrightarrow> Liminf_llist Xs = Liminf_llist (ltl Xs)
[PROOF STEP]
by (metis Liminf_llist_LCons lhd_LCons_ltl lnull_ltlI)


[STATEMENT]
lemma Liminf_llist_subset_Sup_llist: "Liminf_llist Xs \<subseteq> Sup_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist Xs \<subseteq> Sup_llist Xs
[PROOF STEP]
unfolding Liminf_llist_def Sup_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) \<subseteq> \<Union> (lnth Xs ` {i. enat i < llength Xs})
[PROOF STEP]
by fast


[STATEMENT]
lemma image_Liminf_llist_subset: "f ` Liminf_llist Ns \<subseteq> Liminf_llist (lmap ((`) f) Ns)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` Liminf_llist Ns \<subseteq> Liminf_llist (lmap ((`) f) Ns)
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (\<Union>i\<in>{i. enat i < llength Ns}. \<Inter> (lnth Ns ` {j. i \<le> j \<and> enat j < llength Ns})) \<subseteq> (\<Union>i\<in>{i. enat i < llength (lmap ((`) f) Ns)}. \<Inter> (lnth (lmap ((`) f) Ns) ` {j. i \<le> j \<and> enat j < llength (lmap ((`) f) Ns)}))
[PROOF STEP]
by auto


[STATEMENT]
lemma Liminf_llist_imp_exists_index:
  "x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i
[PROOF STEP]
by auto


[STATEMENT]
lemma not_Liminf_llist_imp_exists_index:
  "\<not> lnull Xs \<Longrightarrow> x \<notin> Liminf_llist Xs \<Longrightarrow> enat i < llength Xs \<Longrightarrow>
   (\<exists>j. i \<le> j \<and> enat j < llength Xs \<and> x \<notin> lnth Xs j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> lnull Xs; x \<notin> Liminf_llist Xs; enat i < llength Xs\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. enat j < llength Xs \<and> x \<notin> lnth Xs j
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> lnull Xs; x \<notin> (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})); enat i < llength Xs\<rbrakk> \<Longrightarrow> \<exists>j\<ge>i. enat j < llength Xs \<and> x \<notin> lnth Xs j
[PROOF STEP]
by auto


[STATEMENT]
lemma finite_subset_Liminf_llist_imp_exists_index:
  assumes
    nnil: "\<not> lnull Xs" and
    fin: "finite X" and
    in_lim: "X \<subseteq> Liminf_llist Xs"
  shows "\<exists>i. enat i < llength Xs \<and> X \<subseteq> (\<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
proof (cases "X = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. X = {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
 2. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
X = {}

goal (2 subgoals):
 1. X = {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
 2. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
X = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
X = {}

goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
using nnil
[PROOF STATE]
proof (prove)
using this:
X = {}
\<not> lnull Xs

goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
by (auto intro: exI[of _ 0] simp: zero_enat_def[symmetric])
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
case nemp: False
[PROOF STATE]
proof (state)
this:
X \<noteq> {}

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have in_lim':
      "\<forall>x \<in> X. \<exists>i. enat i < llength Xs \<and> x \<in> (\<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. \<exists>i. enat i < llength Xs \<and> x \<in> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
using in_lim[unfolded Liminf_llist_def] in_mono
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs}))
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B

goal (1 subgoal):
 1. \<forall>x\<in>X. \<exists>i. enat i < llength Xs \<and> x \<in> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. \<exists>i. enat i < llength Xs \<and> x \<in> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
obtain i_of where
      i_of_lt: "\<forall>x \<in> X. enat (i_of x) < llength Xs" and
      in_inter: "\<forall>x \<in> X. x \<in> (\<Inter>j \<in> {j. i_of x \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i_of. \<lbrakk>\<forall>x\<in>X. enat (i_of x) < llength Xs; \<forall>x\<in>X. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bchoice[OF in_lim']
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x\<in>X. enat (f x) < llength Xs \<and> x \<in> \<Inter> (lnth Xs ` {j. f x \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. (\<And>i_of. \<lbrakk>\<forall>x\<in>X. enat (i_of x) < llength Xs; \<forall>x\<in>X. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. enat (i_of x) < llength Xs
\<forall>x\<in>X. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
define i_max where
      "i_max = Max (i_of ` X)"
[PROOF STATE]
proof (state)
this:
i_max = Max (i_of ` X)

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have "i_max \<in> i_of ` X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_max \<in> i_of ` X
[PROOF STEP]
by (simp add: fin i_max_def nemp)
[PROOF STATE]
proof (state)
this:
i_max \<in> i_of ` X

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i_max \<in> i_of ` X
[PROOF STEP]
obtain x_max where
      x_max_in: "x_max \<in> X" and
      i_max_is: "i_max = i_of x_max"
[PROOF STATE]
proof (prove)
using this:
i_max \<in> i_of ` X

goal (1 subgoal):
 1. (\<And>x_max. \<lbrakk>x_max \<in> X; i_max = i_of x_max\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding i_max_def
[PROOF STATE]
proof (prove)
using this:
Max (i_of ` X) \<in> i_of ` X

goal (1 subgoal):
 1. (\<And>x_max. \<lbrakk>x_max \<in> X; Max (i_of ` X) = i_of x_max\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x_max \<in> X
i_max = i_of x_max

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have le_i_max: "\<forall>x \<in> X. i_of x \<le> i_max"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. i_of x \<le> i_max
[PROOF STEP]
unfolding i_max_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>X. i_of x \<le> Max (i_of ` X)
[PROOF STEP]
by (simp add: fin)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>X. i_of x \<le> i_max

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have "enat i_max < llength Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enat i_max < llength Xs
[PROOF STEP]
using i_of_lt x_max_in i_max_is
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. enat (i_of x) < llength Xs
x_max \<in> X
i_max = i_of x_max

goal (1 subgoal):
 1. enat i_max < llength Xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i_max < llength Xs

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enat i_max < llength Xs

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have "X \<subseteq> (\<Inter>j \<in> {j. i_max \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<subseteq> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
assume x_in: "x \<in> X"
[PROOF STATE]
proof (state)
this:
x \<in> X

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> X
[PROOF STEP]
have x_in_inter: "x \<in> (\<Inter>j \<in> {j. i_of x \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
using this:
x \<in> X

goal (1 subgoal):
 1. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
using in_inter
[PROOF STATE]
proof (prove)
using this:
x \<in> X
\<forall>x\<in>X. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
have "{j. i_max \<le> j \<and> enat j < llength Xs}
        \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {j. i_max \<le> j \<and> enat j < llength Xs} \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}
[PROOF STEP]
using x_in le_i_max
[PROOF STATE]
proof (prove)
using this:
x \<in> X
\<forall>x\<in>X. i_of x \<le> i_max

goal (1 subgoal):
 1. {j. i_max \<le> j \<and> enat j < llength Xs} \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{j. i_max \<le> j \<and> enat j < llength Xs} \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}

goal (1 subgoal):
 1. \<And>x. x \<in> X \<Longrightarrow> x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})
{j. i_max \<le> j \<and> enat j < llength Xs} \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}
[PROOF STEP]
show "x \<in> (\<Inter>j \<in> {j. i_max \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<Inter> (lnth Xs ` {j. i_of x \<le> j \<and> enat j < llength Xs})
{j. i_max \<le> j \<and> enat j < llength Xs} \<subseteq> {j. i_of x \<le> j \<and> enat j < llength Xs}

goal (1 subgoal):
 1. x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
X \<subseteq> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. X \<noteq> {} \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enat i_max < llength Xs
X \<subseteq> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat i_max < llength Xs
X \<subseteq> \<Inter> (lnth Xs ` {j. i_max \<le> j \<and> enat j < llength Xs})

goal (1 subgoal):
 1. \<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>i. enat i < llength Xs \<and> X \<subseteq> \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Liminf_llist_lmap_image:
  assumes f_inj: "inj_on f (Sup_llist (lmap g xs))"
  shows "Liminf_llist (lmap (\<lambda>x. f ` g x) xs) = f ` Liminf_llist (lmap g xs)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (lmap (\<lambda>x. f ` g x) xs) = f ` Liminf_llist (lmap g xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<subseteq> f ` Liminf_llist (lmap g xs)
 2. f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
show "?lhs \<subseteq> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<subseteq> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
assume "x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)"
[PROOF STATE]
proof (state)
this:
x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)

goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
obtain i where
      i_lt: "enat i < llength xs" and
      x_in_fgj: "\<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)"
[PROOF STATE]
proof (prove)
using this:
x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength xs; \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
x \<in> (\<Union>i\<in>{i. enat i < llength (lmap (\<lambda>x. f ` g x) xs)}. \<Inter> (lnth (lmap (\<lambda>x. f ` g x) xs) ` {j. i \<le> j \<and> enat j < llength (lmap (\<lambda>x. f ` g x) xs)}))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength xs; \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enat i < llength xs
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)

goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
have ex_in_gi: "\<exists>y. y \<in> g (lnth xs i) \<and> x = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. y \<in> g (lnth xs i) \<and> x = f y
[PROOF STEP]
using f_inj i_lt x_in_fgj
[PROOF STATE]
proof (prove)
using this:
inj_on f (Sup_llist (lmap g xs))
enat i < llength xs
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)

goal (1 subgoal):
 1. \<exists>y. y \<in> g (lnth xs i) \<and> x = f y
[PROOF STEP]
unfolding inj_on_def Sup_llist_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>\<Union> (lnth (lmap g xs) ` {i. enat i < llength (lmap g xs)}). \<forall>y\<in>\<Union> (lnth (lmap g xs) ` {i. enat i < llength (lmap g xs)}). f x = f y \<longrightarrow> x = y
enat i < llength xs
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)

goal (1 subgoal):
 1. \<exists>y. y \<in> g (lnth xs i) \<and> x = f y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>y. y \<in> g (lnth xs i) \<and> x = f y

goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
have "\<exists>y. \<forall>j. i \<le> j \<longrightarrow> enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y
[PROOF STEP]
apply (rule exI[of _ "SOME y. y \<in> g (lnth xs i) \<and> x = f y"])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> (SOME y. y \<in> g (lnth xs i) \<and> x = f y) \<in> g (lnth xs j) \<and> x = f (SOME y. y \<in> g (lnth xs i) \<and> x = f y)
[PROOF STEP]
using someI_ex[OF ex_in_gi] x_in_fgj f_inj i_lt x_in_fgj
[PROOF STATE]
proof (prove)
using this:
(SOME xa. xa \<in> g (lnth xs i) \<and> x = f xa) \<in> g (lnth xs i) \<and> x = f (SOME xa. xa \<in> g (lnth xs i) \<and> x = f xa)
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)
inj_on f (Sup_llist (lmap g xs))
enat i < llength xs
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)

goal (1 subgoal):
 1. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> (SOME y. y \<in> g (lnth xs i) \<and> x = f y) \<in> g (lnth xs j) \<and> x = f (SOME y. y \<in> g (lnth xs i) \<and> x = f y)
[PROOF STEP]
unfolding inj_on_def Sup_llist_def
[PROOF STATE]
proof (prove)
using this:
(SOME xa. xa \<in> g (lnth xs i) \<and> x = f xa) \<in> g (lnth xs i) \<and> x = f (SOME xa. xa \<in> g (lnth xs i) \<and> x = f xa)
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)
\<forall>x\<in>\<Union> (lnth (lmap g xs) ` {i. enat i < llength (lmap g xs)}). \<forall>y\<in>\<Union> (lnth (lmap g xs) ` {i. enat i < llength (lmap g xs)}). f x = f y \<longrightarrow> x = y
enat i < llength xs
\<forall>j\<ge>i. enat j < llength xs \<longrightarrow> x \<in> f ` g (lnth xs j)

goal (1 subgoal):
 1. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> (SOME y. y \<in> g (lnth xs i) \<and> x = f y) \<in> g (lnth xs j) \<and> x = f (SOME y. y \<in> g (lnth xs i) \<and> x = f y)
[PROOF STEP]
by simp (metis (no_types, lifting) imageE)
[PROOF STATE]
proof (state)
this:
\<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y

goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<Longrightarrow> x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y
[PROOF STEP]
show "x \<in> f ` Liminf_llist (lmap g xs)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y

goal (1 subgoal):
 1. x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
using i_lt
[PROOF STATE]
proof (prove)
using this:
\<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y
enat i < llength xs

goal (1 subgoal):
 1. x \<in> f ` Liminf_llist (lmap g xs)
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
\<exists>y. \<forall>j\<ge>i. enat j < llength xs \<longrightarrow> y \<in> g (lnth xs j) \<and> x = f y
enat i < llength xs

goal (1 subgoal):
 1. x \<in> f ` (\<Union>i\<in>{i. enat i < llength (lmap g xs)}. \<Inter> (lnth (lmap g xs) ` {j. i \<le> j \<and> enat j < llength (lmap g xs)}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> f ` Liminf_llist (lmap g xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Liminf_llist (lmap (\<lambda>x. f ` g x) xs) \<subseteq> f ` Liminf_llist (lmap g xs)

goal (1 subgoal):
 1. f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
show "?rhs \<subseteq> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
using image_Liminf_llist_subset[of f "lmap g xs", unfolded llist.map_comp]
[PROOF STATE]
proof (prove)
using this:
f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap ((`) f \<circ> g) xs)

goal (1 subgoal):
 1. f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f ` Liminf_llist (lmap g xs) \<subseteq> Liminf_llist (lmap (\<lambda>x. f ` g x) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Liminf_llist_lmap_union:
  assumes "\<forall>x \<in> lset xs. \<forall>Y \<in> lset xs. g x \<inter> h Y = {}"
  shows "Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) =
    Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) = Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) \<Longrightarrow> x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
 2. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) \<Longrightarrow> x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
 2. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
assume x_in: "x \<in> ?lhs"
[PROOF STATE]
proof (state)
this:
x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)

goal (2 subgoals):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) \<Longrightarrow> x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
 2. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
obtain i where
    i_lt: "enat i < llength xs" and
    j: "\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)"
[PROOF STATE]
proof (prove)
using this:
x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength xs; \<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x_in[unfolded Liminf_llist_def, simplified]
[PROOF STATE]
proof (prove)
using this:
x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
\<exists>xa. enat xa < llength xs \<and> (\<forall>xb. xa \<le> xb \<and> enat xb < llength xs \<longrightarrow> x \<in> g (lnth xs xb) \<or> x \<in> h (lnth xs xb))

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>enat i < llength xs; \<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enat i < llength xs
\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)

goal (2 subgoals):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) \<Longrightarrow> x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
 2. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat i < llength xs
\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)
[PROOF STEP]
have "(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j)))
     \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))"
[PROOF STATE]
proof (prove)
using this:
enat i < llength xs
\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)

goal (1 subgoal):
 1. (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))
[PROOF STEP]
using assms[unfolded disjoint_iff_not_equal]
[PROOF STATE]
proof (prove)
using this:
enat i < llength xs
\<forall>j. i \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j) \<or> x \<in> h (lnth xs j)
\<forall>x\<in>lset xs. \<forall>Y\<in>lset xs. \<forall>x\<in>g x. \<forall>y\<in>h Y. x \<noteq> y

goal (1 subgoal):
 1. (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))
[PROOF STEP]
by (metis in_lset_conv_lnth)
[PROOF STATE]
proof (state)
this:
(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))

goal (2 subgoals):
 1. \<And>x. x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs) \<Longrightarrow> x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
 2. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))
[PROOF STEP]
show "x \<in> ?rhs"
[PROOF STATE]
proof (prove)
using this:
(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))

goal (1 subgoal):
 1. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
(\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> g (lnth xs j))) \<or> (\<exists>i'. enat i' < llength xs \<and> (\<forall>j. i' \<le> j \<and> enat j < llength xs \<longrightarrow> x \<in> h (lnth xs j)))

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{i. enat i < llength (lmap g xs)}. \<Inter> (lnth (lmap g xs) ` {j. i \<le> j \<and> enat j < llength (lmap g xs)})) \<union> (\<Union>i\<in>{i. enat i < llength (lmap h xs)}. \<Inter> (lnth (lmap h xs) ` {j. i \<le> j \<and> enat j < llength (lmap h xs)}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs)

goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
show "x \<in> ?rhs \<Longrightarrow> x \<in> ?lhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>lset xs. \<forall>Y\<in>lset xs. g x \<inter> h Y = {}

goal (1 subgoal):
 1. x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>lset xs. \<forall>Y\<in>lset xs. g x \<inter> h Y = {}

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{i. enat i < llength (lmap g xs)}. \<Inter> (lnth (lmap g xs) ` {j. i \<le> j \<and> enat j < llength (lmap g xs)})) \<union> (\<Union>i\<in>{i. enat i < llength (lmap h xs)}. \<Inter> (lnth (lmap h xs) ` {j. i \<le> j \<and> enat j < llength (lmap h xs)})) \<Longrightarrow> x \<in> (\<Union>i\<in>{i. enat i < llength (lmap (\<lambda>x. g x \<union> h x) xs)}. \<Inter> (lnth (lmap (\<lambda>x. g x \<union> h x) xs) ` {j. i \<le> j \<and> enat j < llength (lmap (\<lambda>x. g x \<union> h x) xs)}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> Liminf_llist (lmap g xs) \<union> Liminf_llist (lmap h xs) \<Longrightarrow> x \<in> Liminf_llist (lmap (\<lambda>x. g x \<union> h x) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Liminf_set_filter_commute:
  "Liminf_llist (lmap (\<lambda>X. {x \<in> X. p x}) Xs) = {x \<in> Liminf_llist Xs. p x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_llist (lmap (\<lambda>X. {x \<in> X. p x}) Xs) = {x \<in> Liminf_llist Xs. p x}
[PROOF STEP]
unfolding Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength (lmap (\<lambda>X. {x \<in> X. p x}) Xs)}. \<Inter> (lnth (lmap (\<lambda>X. {x \<in> X. p x}) Xs) ` {j. i \<le> j \<and> enat j < llength (lmap (\<lambda>X. {x \<in> X. p x}) Xs)})) = {x \<in> \<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs}). p x}
[PROOF STEP]
by force


[STATEMENT]
lemma Liminf_upto_llist_eq_Liminf_llist_ltake:
  "Liminf_upto_llist Xs j = Liminf_llist (ltake (eSuc j) Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs j = Liminf_llist (ltake (eSuc j) Xs)
[PROOF STEP]
unfolding Liminf_upto_llist_def Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> j}. \<Inter> (lnth Xs ` {ja. i \<le> ja \<and> enat ja < llength Xs \<and> enat ja \<le> j})) = (\<Union>i\<in>{i. enat i < llength (ltake (eSuc j) Xs)}. \<Inter> (lnth (ltake (eSuc j) Xs) ` {ja. i \<le> ja \<and> enat ja < llength (ltake (eSuc j) Xs)}))
[PROOF STEP]
by (smt Collect_cong Sup.SUP_cong iless_Suc_eq lnth_ltake less_llength_ltake mem_Collect_eq)


[STATEMENT]
lemma Liminf_upto_llist_enat[simp]:
  "Liminf_upto_llist Xs (enat k) =
   (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
proof (cases "enat k < llength Xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
 2. \<not> enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
enat k < llength Xs

goal (2 subgoals):
 1. enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
 2. \<not> enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
enat k < llength Xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
enat k < llength Xs

goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
unfolding Liminf_upto_llist_def
[PROOF STATE]
proof (prove)
using this:
enat k < llength Xs

goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat k}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> enat k})) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)

goal (1 subgoal):
 1. \<not> enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
case k_ge: False
[PROOF STATE]
proof (state)
this:
\<not> enat k < llength Xs

goal (1 subgoal):
 1. \<not> enat k < llength Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
proof (cases "lnull Xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
 2. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
case nil: True
[PROOF STATE]
proof (state)
this:
lnull Xs

goal (2 subgoals):
 1. lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
 2. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lnull Xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lnull Xs

goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
unfolding Liminf_upto_llist_def
[PROOF STATE]
proof (prove)
using this:
lnull Xs

goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat k}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> enat k})) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
case nnil: False
[PROOF STATE]
proof (state)
this:
\<not> lnull Xs

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> lnull Xs
[PROOF STEP]
obtain j where
    j: "eSuc (enat j) = llength Xs"
[PROOF STATE]
proof (prove)
using this:
\<not> lnull Xs

goal (1 subgoal):
 1. (\<And>j. eSuc (enat j) = llength Xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using k_ge
[PROOF STATE]
proof (prove)
using this:
\<not> lnull Xs
\<not> enat k < llength Xs

goal (1 subgoal):
 1. (\<And>j. eSuc (enat j) = llength Xs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis eSuc_enat_iff enat_ile le_less_linear lhd_LCons_ltl llength_LCons)
[PROOF STATE]
proof (state)
this:
eSuc (enat j) = llength Xs

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
have fin: "lfinite Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lfinite Xs
[PROOF STEP]
using k_ge not_lfinite_llength
[PROOF STATE]
proof (prove)
using this:
\<not> enat k < llength Xs
\<not> lfinite ?xs \<Longrightarrow> llength ?xs = \<infinity>

goal (1 subgoal):
 1. lfinite Xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
lfinite Xs

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
have le_k: "enat i < llength Xs \<and> i \<le> k \<longleftrightarrow> enat i < llength Xs" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (enat i < llength Xs \<and> i \<le> k) = (enat i < llength Xs)
[PROOF STEP]
using k_ge linear order_le_less_subst2
[PROOF STATE]
proof (prove)
using this:
\<not> enat k < llength Xs
?x \<le> ?y \<or> ?y \<le> ?x
\<lbrakk>?a \<le> ?b; ?f ?b < ?c; \<And>x y. x \<le> y \<Longrightarrow> ?f x \<le> ?f y\<rbrakk> \<Longrightarrow> ?f ?a < ?c

goal (1 subgoal):
 1. (enat i < llength Xs \<and> i \<le> k) = (enat i < llength Xs)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(enat ?i < llength Xs \<and> ?i \<le> k) = (enat ?i < llength Xs)

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
have "Liminf_upto_llist Xs (enat k) = llast Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = llast Xs
[PROOF STEP]
using j nnil lfinite_Liminf_llist[OF fin] nnil
[PROOF STATE]
proof (prove)
using this:
eSuc (enat j) = llength Xs
\<not> lnull Xs
Liminf_llist Xs = (if lnull Xs then {} else llast Xs)
\<not> lnull Xs

goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = llast Xs
[PROOF STEP]
unfolding Liminf_upto_llist_def Liminf_llist_def
[PROOF STATE]
proof (prove)
using this:
eSuc (enat j) = llength Xs
\<not> lnull Xs
(\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) = (if lnull Xs then {} else llast Xs)
\<not> lnull Xs

goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat k}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> enat k})) = llast Xs
[PROOF STEP]
using llast_conv_lnth[OF j[symmetric]]
[PROOF STATE]
proof (prove)
using this:
eSuc (enat j) = llength Xs
\<not> lnull Xs
(\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) = (if lnull Xs then {} else llast Xs)
\<not> lnull Xs
llast Xs = lnth Xs j

goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat k}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> enat k})) = llast Xs
[PROOF STEP]
by (simp add: le_k)
[PROOF STATE]
proof (state)
this:
Liminf_upto_llist Xs (enat k) = llast Xs

goal (1 subgoal):
 1. \<not> lnull Xs \<Longrightarrow> Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Liminf_upto_llist Xs (enat k) = llast Xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Liminf_upto_llist Xs (enat k) = llast Xs

goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
using k_ge nnil
[PROOF STATE]
proof (prove)
using this:
Liminf_upto_llist Xs (enat k) = llast Xs
\<not> enat k < llength Xs
\<not> lnull Xs

goal (1 subgoal):
 1. Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Liminf_upto_llist Xs (enat k) = (if enat k < llength Xs then lnth Xs k else if lnull Xs then {} else llast Xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Liminf_upto_llist_infinity[simp]: "Liminf_upto_llist Xs \<infinity> = Liminf_llist Xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs \<infinity> = Liminf_llist Xs
[PROOF STEP]
unfolding Liminf_upto_llist_def Liminf_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> \<infinity>}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs \<and> enat j \<le> \<infinity>})) = (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs}))
[PROOF STEP]
by simp


[STATEMENT]
lemma Liminf_upto_llist_0[simp]:
  "Liminf_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs 0 = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
unfolding Liminf_upto_llist_def image_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> {y. \<exists>x\<in>{i. enat i < llength Xs \<and> enat i \<le> 0}. y = \<Inter> {y. \<exists>x\<in>{j. x \<le> j \<and> enat j < llength Xs \<and> enat j \<le> 0}. y = lnth Xs x}} = (if lnull Xs then {} else lhd Xs)
[PROOF STEP]
by (simp add: enat_0[symmetric]) (simp add: enat_0 lnth_0_conv_lhd)


[STATEMENT]
lemma Liminf_upto_llist_eSuc[simp]:
  "Liminf_upto_llist Xs (eSuc j) =
   (case j of
      enat k \<Rightarrow> Liminf_upto_llist Xs (enat (Suc k))
    | \<infinity> \<Rightarrow> Liminf_llist Xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Liminf_upto_llist Xs (eSuc j) = (case j of enat k \<Rightarrow> Liminf_upto_llist Xs (enat (Suc k)) | \<infinity> \<Rightarrow> Liminf_llist Xs)
[PROOF STEP]
by (auto simp: eSuc_enat split: enat.split)


[STATEMENT]
lemma elem_Liminf_llist_imp_Liminf_upto_llist:
  "x \<in> Liminf_llist Xs \<Longrightarrow>
   \<exists>i < llength Xs. \<forall>j. i \<le> j \<and> j < llength Xs \<longrightarrow> x \<in> Liminf_upto_llist Xs (enat j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i<llength Xs. \<forall>j. i \<le> enat j \<and> enat j < llength Xs \<longrightarrow> x \<in> Liminf_upto_llist Xs (enat j)
[PROOF STEP]
unfolding Liminf_llist_def Liminf_upto_llist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) \<Longrightarrow> \<exists>i<llength Xs. \<forall>j. i \<le> enat j \<and> enat j < llength Xs \<longrightarrow> x \<in> (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat j}. \<Inter> (lnth Xs ` {ja. i \<le> ja \<and> enat ja < llength Xs \<and> enat ja \<le> enat j}))
[PROOF STEP]
using enat_ord_simps(1)
[PROOF STATE]
proof (prove)
using this:
(enat ?m \<le> enat ?n) = (?m \<le> ?n)

goal (1 subgoal):
 1. x \<in> (\<Union>i\<in>{i. enat i < llength Xs}. \<Inter> (lnth Xs ` {j. i \<le> j \<and> enat j < llength Xs})) \<Longrightarrow> \<exists>i<llength Xs. \<forall>j. i \<le> enat j \<and> enat j < llength Xs \<longrightarrow> x \<in> (\<Union>i\<in>{i. enat i < llength Xs \<and> enat i \<le> enat j}. \<Inter> (lnth Xs ` {ja. i \<le> ja \<and> enat ja < llength Xs \<and> enat ja \<le> enat j}))
[PROOF STEP]
by force


[STATEMENT]
lemma wf_jvmprog_is_wf_typ: "wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)
[PROOF STEP]
using Rep_wf_jvmprog [of P]
[PROOF STATE]
proof (prove)
using this:
Rep_wf_jvmprog P \<in> wf_jvmprog

goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)
[PROOF STEP]
by (auto simp: wf_jvmprog_def split_beta)


[STATEMENT]
lemma wf_jvmprog_is_wf: "wf_jvm_prog (PROG P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_jvm_prog (PROG P)
[PROOF STEP]
using wf_jvmprog_is_wf_typ
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>TYPING ?P\<^esub> (PROG ?P)

goal (1 subgoal):
 1. wf_jvm_prog (PROG P)
[PROOF STEP]
unfolding wf_jvm_prog_def
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>TYPING ?P\<^esub> (PROG ?P)

goal (1 subgoal):
 1. \<exists>\<Phi>. wf_jvm_prog\<^bsub>\<Phi>\<^esub> (PROG P)
[PROOF STEP]
by blast


[STATEMENT]
lemma ex_new_class_name: "\<exists>C. \<not> is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
have "\<not> finite (UNIV :: cname set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
by (rule infinite_UNIV_listI)
[PROOF STATE]
proof (state)
this:
infinite UNIV

goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
hence "\<exists>C. C \<notin> set (map fst P)"
[PROOF STATE]
proof (prove)
using this:
infinite UNIV

goal (1 subgoal):
 1. \<exists>C. C \<notin> set (map fst P)
[PROOF STEP]
by -(rule ex_new_if_finite, auto)
[PROOF STATE]
proof (state)
this:
\<exists>C. C \<notin> set (map fst P)

goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. C \<notin> set (map fst P)
[PROOF STEP]
obtain C where "C \<notin> set (map fst P)"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. C \<notin> set (map fst P)

goal (1 subgoal):
 1. (\<And>C. C \<notin> set (map fst P) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
C \<notin> set (map fst P)

goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
have "\<not> is_class P C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_class P C
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_class P C \<Longrightarrow> False
[PROOF STEP]
assume "is_class P C"
[PROOF STATE]
proof (state)
this:
is_class P C

goal (1 subgoal):
 1. is_class P C \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_class P C
[PROOF STEP]
obtain D fs ms where "class P C = \<lfloor>(D, fs, ms)\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
is_class P C

goal (1 subgoal):
 1. (\<And>D fs ms. class P C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. is_class P C \<Longrightarrow> False
[PROOF STEP]
with \<open>C \<notin> set (map fst P)\<close>
[PROOF STATE]
proof (chain)
picking this:
C \<notin> set (map fst P)
class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
C \<notin> set (map fst P)
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. False
[PROOF STEP]
by (auto dest: map_of_SomeD intro!: image_eqI simp: class_def)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> is_class P C

goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> is_class P C

goal (1 subgoal):
 1. \<exists>C. \<not> is_class P C
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>C. \<not> is_class P C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ClassMain_unique_in_P:
  assumes "is_class (PROG P) C"
  shows "ClassMain P \<noteq> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ClassMain P \<noteq> C
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ClassMain P \<noteq> C
[PROOF STEP]
from ex_new_class_name [of "PROG P"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. \<not> is_class (PROG P) C
[PROOF STEP]
obtain D where "\<not> is_class (PROG P) D"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. \<not> is_class (PROG P) C

goal (1 subgoal):
 1. (\<And>D. \<not> is_class (PROG P) D \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_class (PROG P) D

goal (1 subgoal):
 1. ClassMain P \<noteq> C
[PROOF STEP]
with \<open>is_class (PROG P) C\<close>
[PROOF STATE]
proof (chain)
picking this:
is_class (PROG P) C
\<not> is_class (PROG P) D
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_class (PROG P) C
\<not> is_class (PROG P) D

goal (1 subgoal):
 1. ClassMain P \<noteq> C
[PROOF STEP]
unfolding ClassMain_def
[PROOF STATE]
proof (prove)
using this:
is_class (PROG P) C
\<not> is_class (PROG P) D

goal (1 subgoal):
 1. (SOME Name. \<not> is_class (PROG P) Name) \<noteq> C
[PROOF STEP]
by -(rule someI2, fastforce+)
[PROOF STATE]
proof (state)
this:
ClassMain P \<noteq> C

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_of_fstD: "\<lbrakk> map_of xs a = \<lfloor>b\<rfloor>; \<forall>x \<in> set xs. fst x \<noteq> a \<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_of xs a = \<lfloor>b\<rfloor>; \<forall>x\<in>set xs. fst x \<noteq> a\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma map_of_fstE: "\<lbrakk> map_of xs a = \<lfloor>b\<rfloor>; \<exists>x \<in> set xs. fst x = a \<Longrightarrow> thesis \<rbrakk> \<Longrightarrow> thesis"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map_of xs a = \<lfloor>b\<rfloor>; \<exists>x\<in>set xs. fst x = a \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (induct xs) (auto split: if_split_asm)


[STATEMENT]
lemma ex_unique_method_name:
  "\<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
from wf_jvmprog_is_wf [of P]
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog (PROG P)
[PROOF STEP]
have "distinct_fst (PROG P)"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog (PROG P)

goal (1 subgoal):
 1. Auxiliary.distinct_fst (PROG P)
[PROOF STEP]
by (simp add: wf_jvm_prog_def wf_jvm_prog_phi_def wf_prog_def)
[PROOF STATE]
proof (state)
this:
Auxiliary.distinct_fst (PROG P)

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
hence "{C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = fst ` set (PROG P)"
[PROOF STATE]
proof (prove)
using this:
Auxiliary.distinct_fst (PROG P)

goal (1 subgoal):
 1. {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = fst ` set (PROG P)
[PROOF STEP]
by (fastforce elim: map_of_fstE simp: class_def intro: map_of_SomeI)
[PROOF STATE]
proof (state)
this:
{C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = fst ` set (PROG P)

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
hence "finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
{C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = fst ` set (PROG P)

goal (1 subgoal):
 1. finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
have "{ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
    = snd ` snd ` the ` (\<lambda>C. class (PROG P) C) ` {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = snd ` snd ` the ` class (PROG P) ` {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
[PROOF STEP]
by (fastforce intro: rev_image_eqI map_of_SomeI simp: class_def)
[PROOF STATE]
proof (state)
this:
{ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = snd ` snd ` the ` class (PROG P) ` {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
{ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = snd ` snd ` the ` class (PROG P) ` {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
[PROOF STEP]
have "finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
finite {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
{ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>} = snd ` snd ` the ` class (PROG P) ` {C. \<exists>D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
have "\<not> finite (UNIV :: mname set)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite UNIV
[PROOF STEP]
by (rule infinite_UNIV_listI)
[PROOF STATE]
proof (state)
this:
infinite UNIV

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
infinite UNIV
[PROOF STEP]
have "\<exists>Name. Name \<notin> fst ` (\<Union>ms \<in> {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}. set ms)"
[PROOF STATE]
proof (prove)
using this:
finite {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>}
infinite UNIV

goal (1 subgoal):
 1. \<exists>Name. Name \<notin> fst ` \<Union> (set ` {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>})
[PROOF STEP]
by -(rule ex_new_if_finite, auto)
[PROOF STATE]
proof (state)
this:
\<exists>Name. Name \<notin> fst ` \<Union> (set ` {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>})

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>Name. Name \<notin> fst ` \<Union> (set ` {ms. \<exists>C D fs. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor>})

goal (1 subgoal):
 1. \<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma MethodMain_unique_in_P:
  assumes "PROG P \<turnstile> D sees M:Ts\<rightarrow>T = mb in C"
  shows "MethodMain P \<noteq> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MethodMain P \<noteq> M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. MethodMain P \<noteq> M
[PROOF STEP]
from ex_unique_method_name [of P]
[PROOF STATE]
proof (chain)
picking this:
\<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)
[PROOF STEP]
obtain M'
    where "\<And>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> (\<forall>m \<in> set ms. M' \<noteq> fst m)"
[PROOF STATE]
proof (prove)
using this:
\<exists>Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)

goal (1 subgoal):
 1. (\<And>M'. (\<And>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<Longrightarrow> \<forall>m\<in>set ms. M' \<noteq> fst m) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
class (PROG P) ?C = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<forall>m\<in>set ?ms. M' \<noteq> fst m

goal (1 subgoal):
 1. MethodMain P \<noteq> M
[PROOF STEP]
with \<open>PROG P \<turnstile> D sees M:Ts\<rightarrow>T = mb in C\<close>
[PROOF STATE]
proof (chain)
picking this:
PROG P \<turnstile> D sees M: Ts\<rightarrow>T = mb in C
class (PROG P) ?C = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<forall>m\<in>set ?ms. M' \<noteq> fst m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
PROG P \<turnstile> D sees M: Ts\<rightarrow>T = mb in C
class (PROG P) ?C = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<forall>m\<in>set ?ms. M' \<noteq> fst m

goal (1 subgoal):
 1. MethodMain P \<noteq> M
[PROOF STEP]
unfolding MethodMain_def
[PROOF STATE]
proof (prove)
using this:
PROG P \<turnstile> D sees M: Ts\<rightarrow>T = mb in C
class (PROG P) ?C = \<lfloor>(?D, ?fs, ?ms)\<rfloor> \<Longrightarrow> \<forall>m\<in>set ?ms. M' \<noteq> fst m

goal (1 subgoal):
 1. (SOME Name. \<forall>C D fs ms. class (PROG P) C = \<lfloor>(D, fs, ms)\<rfloor> \<longrightarrow> (\<forall>m\<in>set ms. Name \<noteq> fst m)) \<noteq> M
[PROOF STEP]
by -(rule someI2_ex, fastforce, fastforce dest!: visible_method_exists elim: map_of_fstE)
[PROOF STATE]
proof (state)
this:
MethodMain P \<noteq> M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ClassMain_is_no_class [dest!]: "is_class (PROG P) (ClassMain P) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_class (PROG P) (ClassMain P) \<Longrightarrow> False
[PROOF STEP]
proof (erule rev_notE)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> False \<Longrightarrow> \<not> is_class (PROG P) (ClassMain P)
[PROOF STEP]
from ex_new_class_name [of "PROG P"]
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. \<not> is_class (PROG P) C
[PROOF STEP]
obtain C where "\<not> is_class (PROG P) C"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. \<not> is_class (PROG P) C

goal (1 subgoal):
 1. (\<And>C. \<not> is_class (PROG P) C \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_class (PROG P) C

goal (1 subgoal):
 1. \<not> False \<Longrightarrow> \<not> is_class (PROG P) (ClassMain P)
[PROOF STEP]
thus "\<not> is_class (PROG P) (ClassMain P)"
[PROOF STATE]
proof (prove)
using this:
\<not> is_class (PROG P) C

goal (1 subgoal):
 1. \<not> is_class (PROG P) (ClassMain P)
[PROOF STEP]
unfolding ClassMain_def
[PROOF STATE]
proof (prove)
using this:
\<not> is_class (PROG P) C

goal (1 subgoal):
 1. \<not> is_class (PROG P) (SOME Name. \<not> is_class (PROG P) Name)
[PROOF STEP]
by (rule someI)
[PROOF STATE]
proof (state)
this:
\<not> is_class (PROG P) (ClassMain P)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma MethodMain_not_seen [dest!]: "PROG P \<turnstile> C sees (MethodMain P):Ts\<rightarrow>T = mb in D \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROG P \<turnstile> C sees MethodMain P: Ts\<rightarrow>T = mb in D \<Longrightarrow> False
[PROOF STEP]
by (fastforce dest: MethodMain_unique_in_P)


[STATEMENT]
lemma no_Call_from_ClassMain [dest!]: "PROG P \<turnstile> ClassMain P sees M:Ts\<rightarrow>T = mb in C \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROG P \<turnstile> ClassMain P sees M: Ts\<rightarrow>T = mb in C \<Longrightarrow> False
[PROOF STEP]
by (fastforce dest: sees_method_is_class)


[STATEMENT]
lemma no_Call_in_ClassMain [dest!]: "PROG P \<turnstile> C sees M:Ts\<rightarrow>T = mb in ClassMain P \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in ClassMain P \<Longrightarrow> False
[PROOF STEP]
by (fastforce dest: sees_method_idemp)


[STATEMENT]
lemma JVMCFG_edge_det: "\<lbrakk> P \<turnstile> n -(et)\<rightarrow> n'; P \<turnstile> n -(et')\<rightarrow> n' \<rbrakk> \<Longrightarrow> et = et'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk> P \<turnstile> n -et\<rightarrow> n';  P \<turnstile> n -et'\<rightarrow> n'\<rbrakk> \<Longrightarrow> et = et'
[PROOF STEP]
by (erule JVMCFG.cases) (erule JVMCFG.cases, (fastforce dest: sees_method_fun)+)+


[STATEMENT]
lemma sourcenode_reachable: "P \<turnstile> n -(ek)\<rightarrow> n' \<Longrightarrow> P \<turnstile> \<Rightarrow>n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P \<turnstile> n -ek\<rightarrow> n' \<Longrightarrow>  P \<turnstile> \<Rightarrow>n
[PROOF STEP]
by (erule JVMCFG.cases, auto)


[STATEMENT]
lemma targetnode_reachable:
  assumes edge: "P \<turnstile> n -(ek)\<rightarrow> n'"
  shows "P \<turnstile> \<Rightarrow>n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1.  P \<turnstile> \<Rightarrow>n'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1.  P \<turnstile> \<Rightarrow>n'
[PROOF STEP]
from edge
[PROOF STATE]
proof (chain)
picking this:
 P \<turnstile> n -ek\<rightarrow> n'
[PROOF STEP]
have "P \<turnstile> \<Rightarrow>n"
[PROOF STATE]
proof (prove)
using this:
 P \<turnstile> n -ek\<rightarrow> n'

goal (1 subgoal):
 1.  P \<turnstile> \<Rightarrow>n
[PROOF STEP]
by -(drule sourcenode_reachable)
[PROOF STATE]
proof (state)
this:
 P \<turnstile> \<Rightarrow>n

goal (1 subgoal):
 1.  P \<turnstile> \<Rightarrow>n'
[PROOF STEP]
with edge
[PROOF STATE]
proof (chain)
picking this:
 P \<turnstile> n -ek\<rightarrow> n'
 P \<turnstile> \<Rightarrow>n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
 P \<turnstile> n -ek\<rightarrow> n'
 P \<turnstile> \<Rightarrow>n

goal (1 subgoal):
 1.  P \<turnstile> \<Rightarrow>n'
[PROOF STEP]
by -(rule JVMCFG_reachable.intros)
[PROOF STATE]
proof (state)
this:
 P \<turnstile> \<Rightarrow>n'

goal:
No subgoals!
[PROOF STEP]
qed