--- a/Quot/QuotOption.thy	Mon Jan 25 19:14:46 2010 +0100
+++ b/Quot/QuotOption.thy	Mon Jan 25 19:52:53 2010 +0100
@@ -22,80 +22,72 @@
 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])
+  apply(unfold Quotient_def)
+  apply(auto)
+  apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
+  apply(case_tac a, simp_all add: Quotient_abs_rep[OF q] Quotient_rel_rep[OF q])
+  apply(case_tac [!] r)
+  apply(case_tac [!] s)
+  apply(simp_all add: Quotient_abs_rep[OF q] 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
-
+  apply(blast)+
+  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(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  apply(case_tac [!] x)
+  apply(simp_all add: equivp_reflp[OF a])
+  apply(case_tac [!] y)
+  apply(simp_all add: equivp_symp[OF a])
+  apply(case_tac [!] z)
   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(clarify)
   apply(rule equivp_transp[OF a])
   apply(assumption)+
-  apply(simp only: option_rel_some[OF a])
   done
 
-lemma option_map_id[id_simps]: "option_map id \<equiv> id"
+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_respect]:
+  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 \<equiv> id"
   apply (rule eq_reflection)
-  apply (rule ext)
+  apply (auto simp add: expand_fun_eq)
   apply (case_tac x)
   apply (auto)
   done
 
-lemma option_rel_eq[id_simps]: "option_rel op = \<equiv> op ="
-  apply (rule eq_reflection)
-  apply (rule ext)+
-  apply (case_tac x)
-  apply auto
-  apply (case_tac xa)
-  apply auto
-  apply (case_tac xa)
-  apply auto
+lemma option_rel_eq[id_simps]: 
+  shows "option_rel op = \<equiv> op ="
+  apply(rule eq_reflection)
+  apply(auto simp add: expand_fun_eq)
+  apply(case_tac x)
+  apply(case_tac [!] xa)
+  apply(auto)
   done
 
 end