imports Main
begin

lemma finite_ImageI:
assumes "finite A"
assumes "a. aA  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 {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

primrec assert_option ::  where
"assert_option True  Some " | "assert_option False  None"

lemma assert_option_eqs[simp]:
"assert_option Φ = Some x  Φ"

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=], simp)
apply (case_tac x, auto) []
apply (drule spec[where x=], 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