theory QuotOption

imports QuotMain

begin

fun

  option_rel

where

  "option_rel R None None = True"

| "option_rel R (Some x) None = False"

| "option_rel R None (Some x) = False"

| "option_rel R (Some x) (Some y) = R x y"

fun

  option_map

where

  "option_map f None = None"

| "option_map f (Some x) = Some (f x)"

declare [[map option = (option_map, option_rel)]]

lemma option_quotient[quot_thm]:

  assumes q: "Quotient R Abs Rep"

  shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)"

  apply (unfold Quotient_def)

  apply (rule conjI)

  apply (rule allI)

  apply (case_tac a)

  apply (simp_all add: Quotient_abs_rep[OF q])

  apply (rule conjI)

  apply (rule allI)

  apply (case_tac a)

  apply (simp_all add: Quotient_rel_rep[OF q])

  apply (rule allI)+

  apply (case_tac r)

  apply (case_tac s)

  apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q])

  apply (case_tac s)

  apply (simp_all add: Quotient_abs_rep[OF q] add: Quotient_rel_rep[OF q])

  using q

  unfolding Quotient_def

  apply metis

done

lemma option_rel_some:

  assumes e: "equivp R"

  and     a: "option_rel R (Some a) = option_rel R (Some aa)"

  shows      "R a aa"

using a apply(drule_tac x="Some aa" in fun_cong)

apply(simp add: equivp_reflp[OF e])

done

lemma option_equivp[quot_equiv]:

  assumes a: "equivp R"

  shows "equivp (option_rel R)"

  unfolding equivp_def

  apply(rule allI)+

  apply(case_tac x)

  apply(case_tac y)

  apply(simp_all)

  apply(unfold not_def)

  apply(rule impI)

  apply(drule_tac x="None" in fun_cong)

  apply simp

  apply(case_tac y)

  apply(simp_all)

  apply(unfold not_def)

  apply(rule impI)

  apply(drule_tac x="None" in fun_cong)

  apply simp

  apply(rule iffI)

  apply(rule ext)

  apply(case_tac xa)

  apply(auto)

  apply(rule equivp_transp[OF a])

  apply(rule equivp_symp[OF a])

  apply(assumption)+

  apply(rule equivp_transp[OF a])

  apply(assumption)+

  apply(simp only: option_rel_some[OF a])

  done

end