Theory Misc_Aux

theory Misc_Aux
imports "Certification_Monads.Error_Monad"
begin

section ‹Auxiliary definitions and lemmas›

subsection ‹Dropping first elements in lists and taking tails of lists›

definition drop_tail where
  "drop_tail n  xs = rev (drop n (rev xs))"

definition take_tail where
  "take_tail n xs = rev (take n (rev xs))"

lemma drop_tail_except_first:
  assumes "k = length fs"
  shows"drop_tail k (f#fs) = [f]"
  using assms by (simp add: drop_tail_def)

lemma take_tail_except_first:
  assumes "k = length fs"
  shows "take_tail k (f#fs) = fs"
  using assms by (simp add: take_tail_def)

lemma take_tail_Cons:
  assumes "k ≤ length xs"
  shows "take_tail k (x#xs) = take_tail k xs"
  using assms unfolding take_tail_def by simp

section ‹Sum bind split rules›

lemma sum_bind_split: "P (m ⤜ f) = ((∀v. m = Inl v ⟶ P (Inl v)) ∧ (∀v. m = Inr v ⟶ P (f v)))"
  by (cases m) (auto)

lemma sum_bind_split_asm: "P (m ⤜ f) = (¬ ((∃v. m = Inl v ∧ ¬ P (Inl v)) ∨ (∃x. m = Inr x ∧ ¬ P (f x))))"
  by (cases m) (auto)

lemmas sum_bind_splits = sum_bind_split sum_bind_split_asm

section ‹mapM›

fun mapM_sum :: "('a ⇒ 'e + 'b) ⇒ 'a list ⇒ 'e + 'b list" where
  "mapM_sum _ [] = Inr []"
| "mapM_sum f (x#xs) = do {
      y ← f x;
      ys ← mapM_sum f xs;
      Inr (y # ys)
    }"

lemma mapM_sum:
  assumes "isOK (mapM_sum f xs)" "x ∈ set xs"
  shows "isOK (f x)"
  using assms by (induction xs) auto

lemma sequence_isOK:
  assumes "isOK (sequence xs)" "x ∈ set xs"
  shows "isOK x"
  using assms by (induction xs) auto

end