Theory SOS_Misc_Add

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

lemma finite_ImageI:
  assumes "finite A"  
  assumes "⋀a. a∈A ⟹ 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 {x←m; f x}) = do {x←m; 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. x∈m ⟹ f x = g x"
    shows "do {x←m; f x} = do {x←m'; g x}"  
    using assms by auto

  lemma finite_bindI[intro]:
    assumes "finite m"
    assumes "⋀x. x∈m ⟹ finite (f x)"
    shows "finite (do { x←m; f x })"
  proof -
    have S: "do { x←m; 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 "a≠Some 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 ⟷ (∀a∈set 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