diff -r 57944c1ef728 -r ed44eaaea63e Quot/QuotOption.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/QuotOption.thy	Thu Dec 10 14:35:06 2009 +0100
@@ -0,0 +1,82 @@
+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
\ No newline at end of file