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+
−