Theory SM.SOS_Misc_Add

theory SOS_Misc_Add
imports Main "HOL-Library.Monad_Syntax"
begin

lemma finite_ImageI:
  assumes "finite A"  
  assumes "a. aA  finite (R``{a})"
  shows "finite (R``A)"
proof -
  note [[simproc add: finite_Collect]]
  have "R``A = {R``{a} | a. a:A}"
    by auto
  also have "finite ({R``{a} | a. a:A})"
    apply (rule finite_Union)
    apply (simp add: assms)
    apply (clarsimp simp: assms)
    done
  finally show ?thesis .
qed

  (* Set monad utilities *)

  lemma do_set_push_Image:
    "g f m. g`(do {xm; f x}) = do {xm; g`f x}"
    "g f m. g`(do {let x = m; f x}) = (do {let x=m; g`f x})"
    by fastforce+
    
  lemma case_option_distrib: "f (case x of Some v  fs v | None  fn) 
    = (case x of Some v  f (fs v) | None  f fn)" 
    by (auto split: option.split)

  lemma case_sum_distrib: "f (case x of Inl x  fl x | Inr x  fr x) = 
    (case x of Inl x  f (fl x) | Inr x  f (fr x))"
    by (auto split: sum.split)

  lemma do_set_eq_bind:
    assumes "m'=m"
    assumes "x. xm  f x = g x"
    shows "do {xm; f x} = do {xm'; g x}"  
    using assms by auto

  lemma finite_bindI[intro]:
    assumes "finite m"
    assumes "x. xm  finite (f x)"
    shows "finite (do { xm; f x })"
  proof -
    have S: "do { xm; f x } = (f`m)"
      by auto
  
    show ?thesis  
      apply (subst S)
      using assms
      by blast
  qed        
  

(* Option monad utilities *)

  primrec assert_option :: "bool  unit option" where
    "assert_option True = Some ()" | "assert_option False = None"

  lemma assert_option_eqs[simp]:
    "assert_option Φ = Some x  Φ"  
    "assert_option Φ = None  ¬Φ"  
    by (cases Φ) auto


  (* TODO: Move *)
  lemma disj_eq_nota_conv[simp]:
    "(a  b  ¬a)  (a=False  b=True)" 
    "(b  a  ¬a)  (a=False  b=True)" 
    "(¬a  b  a)  (a=True  b=True)" 
    "(b  ¬a  a)  (a=True  b=True)" 
    by auto

  lemma all_disjx_conv[simp]:
    "(x. x  P x)  P False"  
    "(x. x  P (¬x))  P True"
    apply safe
    apply (drule spec[where x=False], simp)
    apply (case_tac x, auto) []
    apply (drule spec[where x=False], simp)
    apply (case_tac x, auto) []
    done

  lemma neq_Some_bool_cases[consumes 1, case_names None Some]:
    assumes "aSome x"  
    obtains "a=None" | "a = Some (¬x)"
    using assms by auto



  primrec find_min_idx :: "('a  bool)  'a list  nat" where
    "find_min_idx P [] = None"
  | "find_min_idx P (x#xs) = (
      if P x then Some 0 else
      map_option Suc (find_min_idx P xs)
    )"
  
  lemma find_min_idx_None_conv: 
    "find_min_idx P l = None  (aset l. ¬P a)"
    apply (induction l)
    apply auto
    done

  lemma find_min_idx_SomeD:
    "find_min_idx P l = Some i  P (l!i)  i < length l"
    by (induction l arbitrary: i) (auto split: if_split_asm)

  lemma find_min_idx_SomeD_complete: 
    "find_min_idx P l = Some i  (P (l!i)  i < length l  (j<i. ¬P (l!j)))"
    apply (induction l arbitrary: i) 
    apply (auto split: if_split_asm)
    apply (case_tac j)
    apply auto
    done

end