```theory SOS_Misc_Add
begin

lemma finite_ImageI:
assumes "finite A"
assumes "⋀a. a∈A ⟹ finite (R``{a})"
shows "finite (R``A)"
proof -
have "R``A = ⋃{R``{a} | a. a:A}"
by auto
also have "finite (⋃{R``{a} | a. a:A})"
apply (rule finite_Union)
apply (clarsimp simp: assms)
done
finally show ?thesis .
qed

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

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

```