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(auto)
  apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
  apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
  apply(case_tac [!] r)
  apply(case_tac [!] s)
  apply(simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q] )
  using q
  unfolding Quotient_def
  apply(blast)+
  done
  
lemma option_equivp[quot_equiv]:
  assumes a: "equivp R"
  shows "equivp (option_rel R)"
  apply(rule equivpI)
  unfolding reflp_def symp_def transp_def
  apply(auto)
  apply(case_tac [!] x)
  apply(simp_all add: equivp_reflp[OF a])
  apply(case_tac [!] y)
  apply(simp_all add: equivp_symp[OF a])
  apply(case_tac [!] z)
  apply(simp_all)
  apply(clarify)
  apply(rule equivp_transp[OF a])
  apply(assumption)+
  done

lemma option_None_rsp[quot_respect]:
  assumes q: "Quotient R Abs Rep"
  shows "option_rel R None None"
  by simp

lemma option_Some_rsp[quot_respect]:
  assumes q: "Quotient R Abs Rep"
  shows "(R ===> option_rel R) Some Some"
  by simp

lemma option_None_prs[quot_preserve]:
  assumes q: "Quotient R Abs Rep"
  shows "option_map Abs None = None"
  by simp

lemma option_Some_prs[quot_respect]:
  assumes q: "Quotient R Abs Rep"
  shows "(Rep ---> option_map Abs) Some = Some"
  apply(simp add: expand_fun_eq)
  apply(simp add: Quotient_abs_rep[OF q])
  done

lemma option_map_id[id_simps]: 
  shows "option_map id \<equiv> id"
  apply (rule eq_reflection)
  apply (auto simp add: expand_fun_eq)
  apply (case_tac x)
  apply (auto)
  done

lemma option_rel_eq[id_simps]: 
  shows "option_rel op = \<equiv> op ="
  apply(rule eq_reflection)
  apply(auto simp add: expand_fun_eq)
  apply(case_tac x)
  apply(case_tac [!] xa)
  apply(auto)
  done

end