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_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