Theory Worklist_Common

theory Worklist_Common
  imports Worklist_Locales
begin

lemma list_ex_foldli:
  "list_ex P xs = foldli xs Not (λ x y. P x ∨ y) False"
  apply (induction xs)
  subgoal
    by simp
  subgoal for x xs
    by (induction xs) auto
  done

lemma (in Search_Space_finite) finitely_branching:
  assumes "reachable a"
  shows "finite ({a'. E a a' ∧ ¬ empty a'})"
proof -
  have "{a'. E a a' ∧ ¬ empty a'} ⊆ {a'. reachable a' ∧ ¬ empty a'}"
    using assms(1) by (auto intro: reachable_step)
  then show ?thesis using finite_reachable
    by (rule finite_subset)
qed

definition (in Search_Space_Key_Defs)
  "map_set_rel =
    {(m, s).
      ⋃(ran m) = s ∧ (∀ k. ∀ x. m k = Some x ⟶ (∀ v ∈ x. key v = k)) ∧
      finite (dom m) ∧ (∀ k S. m k = Some S ⟶ finite S)
    }"

end (* Theory *)