diff -r 6088fea1c8b1 -r 8a1c8dc72b5c Quotients.thy
--- a/Quotients.thy	Mon Dec 07 14:00:36 2009 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,80 +0,0 @@
-theory Quotients
-imports Main
-begin
-
-(* Other quotients that have not been proved yet *)
-
-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)"
-
-fun
-  prod_rel
-where
-  "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
-
-fun
-  prod_map
-where
-  "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
-
-fun
-  sum_rel
-where
-  "sum_rel R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
-| "sum_rel R1 R2 (Inl a1) (Inr b2) = False"
-| "sum_rel R1 R2 (Inr a2) (Inl b1) = False"
-| "sum_rel R1 R2 (Inr a2) (Inr b2) = R2 a2 b2"
-
-fun
-  sum_map
-where
-  "sum_map f1 f2 (Inl a) = Inl (f1 a)"
-| "sum_map f1 f2 (Inr a) = Inr (f2 a)"
-
-
-
-
-
-fun
-  noption_map::"('a \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
-where
-  "noption_map f (nSome x) = nSome (f x)"
-| "noption_map f nNone = nNone"
-
-fun
-  noption_rel
-where
-  "noption_rel r (nSome x) (nSome y) = r x y"
-| "noption_rel r _ _ = False"
-
-declare [[map noption = (noption_map, noption_rel)]]
-
-lemma "noption_map id = id"
-sorry
-
-lemma noption_Quotient:
-  assumes q: "Quotient R Abs Rep"
-  shows "Quotient (noption_rel R) (noption_map Abs) (noption_map Rep)"
-  apply (unfold Quotient_def)
-  apply (auto)
-  using q
-  apply (unfold Quotient_def)
-  apply (case_tac "a :: 'b noption")
-  apply (simp)
-  apply (simp)
-  apply (case_tac "a :: 'b noption")
-  apply (simp only: option_map.simps)
-  apply (subst option_rel.simps)
-  (* Simp starts hanging so don't know how to continue *)
-  sorry