--- a/Quotients.thy	Fri Dec 04 17:50:02 2009 +0100
+++ b/Quotients.thy	Fri Dec 04 17:57:03 2009 +0100
@@ -2,16 +2,15 @@
 imports Main
 begin
 
-definition
-  "NONEMPTY E \<equiv> \<exists>x. E x x"
+(* Other quotients that have not been proved yet *)
 
-fun 
-  OPTION_REL 
+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"
+  "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
@@ -19,10 +18,10 @@
   "option_map f None = None"
 | "option_map f (Some x) = Some (f x)"
 
-fun 
-  PROD_REL
+fun
+  prod_rel
 where
-  "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
+  "prod_rel R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)"
 
 fun
   prod_map
@@ -30,12 +29,12 @@
   "prod_map f1 f2 (a,b) = (f1 a, f2 b)"
 
 fun
-  SUM_REL
+  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"
+  "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
@@ -43,25 +42,39 @@
   "sum_map f1 f2 (Inl a) = Inl (f1 a)"
 | "sum_map f1 f2 (Inr a) = Inr (f2 a)"
 
-definition
-  "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> 
-                        (\<forall>a. R (Rep a) (Rep a)) \<and> 
-                        (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))"
+
+
+
+
+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 QUOTIENT_PROD:
-  assumes a: "QUOTIENT E1 Abs1 Rep1"
-  and     b: "QUOTIENT E2 Abs2 Rep2"
-  shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
-using a b unfolding QUOTIENT_def
-oops
+lemma "noption_map id = id"
+sorry
 
-lemma QUOTIENT_ABS_REP_LIST:
-  assumes a: "QUOTIENT_ABS_REP Abs Rep"
-  shows "QUOTIENT_ABS_REP (map Abs) (map Rep)"
-using a
-unfolding QUOTIENT_ABS_REP_def
-apply(rule_tac allI)
-apply(induct_tac a rule: list.induct)
-apply(auto)
-done
-
+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