diff --git a/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy b/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy
--- a/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy
+++ b/thys/Ordered_Resolution_Prover/Herbrand_Interpretation.thy
@@ -1,137 +1,143 @@
 (*  Title:       Herbrand Interpretation
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
 *)
 
 section \<open>Herbrand Intepretation\<close>
 
 theory Herbrand_Interpretation
   imports Clausal_Logic
 begin
 
 text \<open>
 The material formalized here corresponds roughly to Sections 2.2 (``Herbrand
 Interpretations'') of Bachmair and Ganzinger, excluding the formula and term
 syntax.
 
 A Herbrand interpretation is a set of ground atoms that are to be considered true.
 \<close>
 
 type_synonym 'a interp = "'a set"
 
 definition true_lit :: "'a interp \<Rightarrow> 'a literal \<Rightarrow> bool" (infix "\<Turnstile>l" 50) where
   "I \<Turnstile>l L \<longleftrightarrow> (if is_pos L then (\<lambda>P. P) else Not) (atm_of L \<in> I)"
 
 lemma true_lit_simps[simp]:
   "I \<Turnstile>l Pos A \<longleftrightarrow> A \<in> I"
   "I \<Turnstile>l Neg A \<longleftrightarrow> A \<notin> I"
   unfolding true_lit_def by auto
 
 lemma true_lit_iff[iff]: "I \<Turnstile>l L \<longleftrightarrow> (\<exists>A. L = Pos A \<and> A \<in> I \<or> L = Neg A \<and> A \<notin> I)"
   by (cases L) simp+
 
 definition true_cls :: "'a interp \<Rightarrow> 'a clause \<Rightarrow> bool" (infix "\<Turnstile>" 50) where
   "I \<Turnstile> C \<longleftrightarrow> (\<exists>L \<in># C. I \<Turnstile>l L)"
 
 lemma true_cls_empty[iff]: "\<not> I \<Turnstile> {#}"
   unfolding true_cls_def by simp
 
 lemma true_cls_singleton[iff]: "I \<Turnstile> {#L#} \<longleftrightarrow> I \<Turnstile>l L"
   unfolding true_cls_def by simp
 
 lemma true_cls_add_mset[iff]: "I \<Turnstile> add_mset C D \<longleftrightarrow> I \<Turnstile>l C \<or> I \<Turnstile> D"
   unfolding true_cls_def by auto
 
 lemma true_cls_union[iff]: "I \<Turnstile> C + D \<longleftrightarrow> I \<Turnstile> C \<or> I \<Turnstile> D"
   unfolding true_cls_def by auto
 
 lemma true_cls_mono: "set_mset C \<subseteq> set_mset D \<Longrightarrow> I \<Turnstile> C \<Longrightarrow> I \<Turnstile> D"
   unfolding true_cls_def subset_eq by metis
 
 lemma
   assumes "I \<subseteq> J"
   shows
     false_to_true_imp_ex_pos: "\<not> I \<Turnstile> C \<Longrightarrow> J \<Turnstile> C \<Longrightarrow> \<exists>A \<in> J. Pos A \<in># C" and
     true_to_false_imp_ex_neg: "I \<Turnstile> C \<Longrightarrow> \<not> J \<Turnstile> C \<Longrightarrow> \<exists>A \<in> J. Neg A \<in># C"
   using assms unfolding subset_iff true_cls_def by (metis literal.collapse true_lit_simps)+
 
 lemma true_cls_replicate_mset[iff]: "I \<Turnstile> replicate_mset n L \<longleftrightarrow> n \<noteq> 0 \<and> I \<Turnstile>l L"
   by (simp add: true_cls_def)
 
 lemma pos_literal_in_imp_true_cls[intro]: "Pos A \<in># C \<Longrightarrow> A \<in> I \<Longrightarrow> I \<Turnstile> C"
   using true_cls_def by blast
 
 lemma neg_literal_notin_imp_true_cls[intro]: "Neg A \<in># C \<Longrightarrow> A \<notin> I \<Longrightarrow> I \<Turnstile> C"
   using true_cls_def by blast
 
 lemma pos_neg_in_imp_true: "Pos A \<in># C \<Longrightarrow> Neg A \<in># C \<Longrightarrow> I \<Turnstile> C"
   using true_cls_def by blast
 
 definition true_clss :: "'a interp \<Rightarrow> 'a clause set \<Rightarrow> bool" (infix "\<Turnstile>s" 50) where
   "I \<Turnstile>s CC \<longleftrightarrow> (\<forall>C \<in> CC. I \<Turnstile> C)"
 
 lemma true_clss_empty[iff]: "I \<Turnstile>s {}"
   by (simp add: true_clss_def)
 
 lemma true_clss_singleton[iff]: "I \<Turnstile>s {C} \<longleftrightarrow> I \<Turnstile> C"
   unfolding true_clss_def by blast
 
 lemma true_clss_insert[iff]: "I \<Turnstile>s insert C DD \<longleftrightarrow> I \<Turnstile> C \<and> I \<Turnstile>s DD"
   unfolding true_clss_def by blast
 
 lemma true_clss_union[iff]: "I \<Turnstile>s CC \<union> DD \<longleftrightarrow> I \<Turnstile>s CC \<and> I \<Turnstile>s DD"
   unfolding true_clss_def by blast
 
+lemma true_clss_Union[iff]: "I \<Turnstile>s \<Union> CCC \<longleftrightarrow> (\<forall>CC \<in> CCC. I \<Turnstile>s CC)"
+  unfolding true_clss_def by simp
+
 lemma true_clss_mono: "DD \<subseteq> CC \<Longrightarrow> I \<Turnstile>s CC \<Longrightarrow> I \<Turnstile>s DD"
   by (simp add: subsetD true_clss_def)
 
 lemma true_clss_mono_strong: "(\<forall>D \<in> DD. \<exists>C \<in> CC. C \<subseteq># D) \<Longrightarrow> I \<Turnstile>s CC \<Longrightarrow> I \<Turnstile>s DD"
   unfolding true_clss_def true_cls_def true_lit_def by (meson mset_subset_eqD)
 
 lemma true_clss_subclause: "C \<subseteq># D \<Longrightarrow> I \<Turnstile>s {C} \<Longrightarrow> I \<Turnstile>s {D}"
   by (rule true_clss_mono_strong[of _ "{C}"]) auto
 
 abbreviation satisfiable :: "'a clause set \<Rightarrow> bool" where
   "satisfiable CC \<equiv> \<exists>I. I \<Turnstile>s CC"
 
 lemma satisfiable_antimono: "CC \<subseteq> DD \<Longrightarrow> satisfiable DD \<Longrightarrow> satisfiable CC"
   using true_clss_mono by blast
 
 lemma unsatisfiable_mono: "CC \<subseteq> DD \<Longrightarrow> \<not> satisfiable CC \<Longrightarrow> \<not> satisfiable DD"
   using satisfiable_antimono by blast
 
 definition true_cls_mset :: "'a interp \<Rightarrow> 'a clause multiset \<Rightarrow> bool" (infix "\<Turnstile>m" 50) where
   "I \<Turnstile>m CC \<longleftrightarrow> (\<forall>C \<in># CC. I \<Turnstile> C)"
 
 lemma true_cls_mset_empty[iff]: "I \<Turnstile>m {#}"
   unfolding true_cls_mset_def by auto
 
 lemma true_cls_mset_singleton[iff]: "I \<Turnstile>m {#C#} \<longleftrightarrow> I \<Turnstile> C"
   by (simp add: true_cls_mset_def)
 
 lemma true_cls_mset_union[iff]: "I \<Turnstile>m CC + DD \<longleftrightarrow> I \<Turnstile>m CC \<and> I \<Turnstile>m DD"
   unfolding true_cls_mset_def by auto
 
+lemma true_cls_mset_Union[iff]: "I \<Turnstile>m \<Union># CCC \<longleftrightarrow> (\<forall>CC \<in># CCC. I \<Turnstile>m CC)"
+  unfolding true_cls_mset_def by simp
+
 lemma true_cls_mset_add_mset[iff]: "I \<Turnstile>m add_mset C CC \<longleftrightarrow> I \<Turnstile> C \<and> I \<Turnstile>m CC"
   unfolding true_cls_mset_def by auto
 
 lemma true_cls_mset_image_mset[iff]: "I \<Turnstile>m image_mset f A \<longleftrightarrow> (\<forall>x \<in># A. I \<Turnstile> f x)"
   unfolding true_cls_mset_def by auto
 
 lemma true_cls_mset_mono: "set_mset DD \<subseteq> set_mset CC \<Longrightarrow> I \<Turnstile>m CC \<Longrightarrow> I \<Turnstile>m DD"
   unfolding true_cls_mset_def subset_iff by auto
 
 lemma true_cls_mset_mono_strong: "(\<forall>D \<in># DD. \<exists>C \<in># CC. C \<subseteq># D) \<Longrightarrow> I \<Turnstile>m CC \<Longrightarrow> I \<Turnstile>m DD"
   unfolding true_cls_mset_def true_cls_def true_lit_def by (meson mset_subset_eqD)
 
 lemma true_clss_set_mset[iff]: "I \<Turnstile>s set_mset CC \<longleftrightarrow> I \<Turnstile>m CC"
   unfolding true_clss_def true_cls_mset_def by auto
 
 lemma true_clss_mset_set[simp]: "finite CC \<Longrightarrow> I \<Turnstile>m mset_set CC \<longleftrightarrow> I \<Turnstile>s CC"
   unfolding true_clss_def true_cls_mset_def by auto
 
 lemma true_cls_mset_true_cls: "I \<Turnstile>m CC \<Longrightarrow> C \<in># CC \<Longrightarrow> I \<Turnstile> C"
   using true_cls_mset_def by auto
 
 end
diff --git a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
--- a/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
+++ b/thys/Ordered_Resolution_Prover/Lazy_List_Liminf.thy
@@ -1,161 +1,165 @@
 (*  Title:       Liminf of Lazy Lists
     Author:      Jasmin Blanchette <j.c.blanchette at vu.nl>, 2014, 2017
     Author:      Dmitriy Traytel <traytel at inf.ethz.ch>, 2014
     Maintainer:  Jasmin Blanchette <j.c.blanchette at vu.nl>
 *)
 
 section \<open>Liminf of Lazy Lists\<close>
 
 theory Lazy_List_Liminf
   imports Coinductive.Coinductive_List
 begin
 
 text \<open>
 Lazy lists, as defined in the \emph{Archive of Formal Proofs}, provide finite and infinite lists in
 one type, defined coinductively. The present theory introduces the concept of the union of all
 elements of a lazy list of sets and the limit of such a lazy list. The definitions are stated more
 generally in terms of lattices. The basis for this theory is Section 4.1 (``Theorem Proving
 Processes'') of Bachmair and Ganzinger's chapter.
 \<close>
 
 definition Sup_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Sup_llist Xs = (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
 
 lemma lnth_subset_Sup_llist: "enat i < llength xs \<Longrightarrow> lnth xs i \<subseteq> Sup_llist xs"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LNil[simp]: "Sup_llist LNil = {}"
   unfolding Sup_llist_def by auto
 
 lemma Sup_llist_LCons[simp]: "Sup_llist (LCons X Xs) = X \<union> Sup_llist Xs"
   unfolding Sup_llist_def
 proof (intro subset_antisym subsetI)
   fix x
   assume "x \<in> (\<Union>i \<in> {i. enat i < llength (LCons X Xs)}. lnth (LCons X Xs) i)"
   then obtain i where len: "enat i < llength (LCons X Xs)" and nth: "x \<in> lnth (LCons X Xs) i"
     by blast
   from nth have "x \<in> X \<or> i > 0 \<and> x \<in> lnth Xs (i - 1)"
     by (metis lnth_LCons' neq0_conv)
   then have "x \<in> X \<or> (\<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i)"
     by (metis len Suc_pred' eSuc_enat iless_Suc_eq less_irrefl llength_LCons not_less order_trans)
   then show "x \<in> X \<union> (\<Union>i \<in> {i. enat i < llength Xs}. lnth Xs i)"
     by blast
 qed ((auto)[], metis i0_lb lnth_0 zero_enat_def, metis Suc_ile_eq lnth_Suc_LCons)
 
 lemma lhd_subset_Sup_llist: "\<not> lnull Xs \<Longrightarrow> lhd Xs \<subseteq> Sup_llist Xs"
   by (cases Xs) simp_all
 
 definition Sup_upto_llist :: "'a set llist \<Rightarrow> nat \<Rightarrow> 'a set" where
   "Sup_upto_llist Xs j = (\<Union>i \<in> {i. enat i < llength Xs \<and> i \<le> j}. lnth Xs i)"
 
 lemma Sup_upto_llist_0[simp]: "Sup_upto_llist Xs 0 = (if 0 < llength Xs then lnth Xs 0 else {})"
   unfolding Sup_upto_llist_def image_def by (simp add: enat_0)
 
 lemma Sup_upto_llist_Suc[simp]:
   "Sup_upto_llist Xs (Suc j) =
    Sup_upto_llist Xs j \<union> (if enat (Suc j) < llength Xs then lnth Xs (Suc j) else {})"
   unfolding Sup_upto_llist_def image_def by (auto intro: le_SucI elim: le_SucE)
 
 lemma Sup_upto_llist_mono: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_upto_llist Xs k"
   unfolding Sup_upto_llist_def by auto
 
 lemma Sup_upto_llist_subset_Sup_llist: "j \<le> k \<Longrightarrow> Sup_upto_llist Xs j \<subseteq> Sup_llist Xs"
   unfolding Sup_llist_def Sup_upto_llist_def by auto
 
 lemma elem_Sup_llist_imp_Sup_upto_llist:
 	"x \<in> Sup_llist Xs \<Longrightarrow> \<exists>j < llength Xs. x \<in> Sup_upto_llist Xs j"
   unfolding Sup_llist_def Sup_upto_llist_def by blast
 
 lemma lnth_subset_Sup_upto_llist: "enat j < llength Xs \<Longrightarrow> lnth Xs j \<subseteq> Sup_upto_llist Xs j"
   unfolding Sup_upto_llist_def by auto
 
 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 k"
   using assms
 proof induct
   case (insert x X)
   then have x: "x \<in> Sup_llist Xs" and X: "X \<subseteq> Sup_llist Xs"
     by simp+
   from x obtain k where k: "x \<in> Sup_upto_llist Xs k"
     using elem_Sup_llist_imp_Sup_upto_llist by fast
   from X obtain k' where k': "X \<subseteq> Sup_upto_llist Xs k'"
     using insert.hyps(3) by fast
   have "insert x X \<subseteq> Sup_upto_llist Xs (max k k')"
     using k k'
     by (metis insert_absorb insert_subset Sup_upto_llist_mono max.cobounded2 max.commute
         order.trans)
   then show ?case
     by fast
 qed simp
 
 definition Liminf_llist :: "'a set llist \<Rightarrow> 'a set" where
   "Liminf_llist Xs =
    (\<Union>i \<in> {i. enat i < llength Xs}. \<Inter>j \<in> {j. i \<le> j \<and> enat j < llength Xs}. lnth Xs j)"
 
 lemma Liminf_llist_LNil[simp]: "Liminf_llist LNil = {}"
   unfolding Liminf_llist_def by simp
 
 lemma Liminf_llist_LCons:
   "Liminf_llist (LCons X Xs) = (if lnull Xs then X else Liminf_llist Xs)" (is "?lhs = ?rhs")
 proof (cases "lnull Xs")
   case nnull: False
   show ?thesis
   proof
     {
       fix x
       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)"
       then 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)"
         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))
       then have "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
         by (metis Suc_ile_eq Suc_n_not_le_n lift_Suc_mono_le lnth_Suc_LCons nat_le_linear)
     }
     then show "?lhs \<subseteq> ?rhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
 
     {
       fix x
       assume "\<exists>i. enat i < llength Xs \<and> (\<forall>j. i \<le> j \<and> enat j < llength Xs \<longrightarrow> x \<in> lnth Xs j)"
       then 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"
         by blast
 
       have "enat (Suc i) \<le> llength Xs"
         using i by (simp add: Suc_ile_eq)
       moreover have "\<forall>j. Suc i \<le> j \<and> enat j \<le> llength Xs \<longrightarrow> x \<in> lnth (LCons X Xs) j"
         using Suc_ile_eq Suc_le_D j by force
       ultimately 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)"
         by blast
     }
     then show "?rhs \<subseteq> ?lhs"
       by (simp add: Liminf_llist_def nnull) (rule subsetI, simp)
   qed
 qed (simp add: Liminf_llist_def enat_0_iff(1))
 
 lemma lfinite_Liminf_llist: "lfinite Xs \<Longrightarrow> Liminf_llist Xs = (if lnull Xs then {} else llast Xs)"
 proof (induction rule: lfinite_induct)
   case (LCons xs)
   then obtain y ys where
     xs: "xs = LCons y ys"
     by (meson not_lnull_conv)
   show ?case
     unfolding xs by (simp add: Liminf_llist_LCons LCons.IH[unfolded xs, simplified] llast_LCons)
 qed (simp add: Liminf_llist_def)
 
 lemma Liminf_llist_ltl: "\<not> lnull (ltl Xs) \<Longrightarrow> Liminf_llist Xs = Liminf_llist (ltl Xs)"
   by (metis Liminf_llist_LCons lhd_LCons_ltl lnull_ltlI)
 
 lemma Liminf_llist_subset_Sup_llist: "Liminf_llist Xs \<subseteq> Sup_llist Xs"
   unfolding Liminf_llist_def Sup_llist_def by fast
 
 lemma image_Liminf_llist_subset: "f ` Liminf_llist Ns \<subseteq> Liminf_llist (lmap ((`) f) Ns)"
   unfolding Liminf_llist_def by auto
 
+lemma Liminf_llist_imp_exists_index:
+  "x \<in> Liminf_llist Xs \<Longrightarrow> \<exists>i. enat i < llength Xs \<and> x \<in> lnth Xs i"
+  unfolding Liminf_llist_def by auto
+
 end