diff -r db158e995bfc -r 9df6144e281b Quot/Quotient_Option.thy
--- a/Quot/Quotient_Option.thy	Thu Feb 25 07:48:57 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-(*  Title:      Quotient_Option.thy
-    Author:     Cezary Kaliszyk and Christian Urban
-*)
-theory Quotient_Option
-imports Quotient Quotient_Syntax
-begin
-
-section {* Quotient infrastructure for the option type. *}
-
-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"
-
-declare [[map option = (Option.map, option_rel)]]
-
-text {* should probably be in Option.thy *}
-lemma split_option_all:
-  shows "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>a. P (Some a))"
-  apply(auto)
-  apply(case_tac x)
-  apply(simp_all)
-  done
-
-lemma option_quotient[quot_thm]:
-  assumes q: "Quotient R Abs Rep"
-  shows "Quotient (option_rel R) (Option.map Abs) (Option.map Rep)"
-  unfolding Quotient_def
-  apply(simp add: split_option_all)
-  apply(simp 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(simp_all add: split_option_all)
-  apply(blast intro: equivp_reflp[OF a])
-  apply(blast intro: equivp_symp[OF a])
-  apply(blast intro: equivp_transp[OF a])
-  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_preserve]:
-  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 = id"
-  by (simp add: expand_fun_eq split_option_all)
-
-lemma option_rel_eq[id_simps]:
-  shows "option_rel (op =) = (op =)"
-  by (simp add: expand_fun_eq split_option_all)
-
-end