Theory Basic_Utils

text ‹Trivialities›
theory Basic_Utils
  imports TRS.Trs
begin

lemmas construct_exI' = Ex_list_of_length_P

lemma construct_exI'_double:
  assumes "∀i < n. ∃x y. P x y i"
  shows "∃xs ys. length xs = n ∧ length ys = n ∧ (∀i < n. P (xs ! i) (ys ! i) i)"
proof -
  from assms obtain f g where "P (f i) (g i) i" if "i < n" for i using assms by metis
  then show ?thesis by (intro exI[of _ "map _ [0..<n]"]) auto
qed

(* TODO: check whether this is still needed *)
lemma construct_exI:
  assumes "∀i < n. ∃xs. P (xs ! i) i"
  shows "∃xs. length xs = n ∧ (∀i < n. P (xs ! i) i)"
proof -
  guess xss using construct_exI'[OF assms] by (elim exE)
  then show ?thesis by (intro exI[of _ "map (λi. xss ! i ! i) [0..<n]"]) auto
qed

definition right_ground_trs :: "('f, 'v) trs ⇒ bool" where
  "right_ground_trs R ≡ ∀(l, r) ∈ R. ground r"

definition ground_trs :: "('f, 'v) trs ⇒ bool" where
  "ground_trs R ≡ ∀(l, r) ∈ R. ground l ∧ ground r"

lemma ground_imp_right_ground_trs [simp]:
  "ground_trs R ⟹ right_ground_trs R"
  unfolding ground_trs_def right_ground_trs_def by fast

definition set_to_list :: "'a set ⇒ 'a list"
  where "set_to_list s = (SOME l. set l = s)"

lemma set_set_to_list:
  "finite s ⟹ set (set_to_list s) = s"
  unfolding set_to_list_def by (metis (mono_tags) finite_list some_eq_ex)

end