--- a/Quot/QuotOption.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotOption.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -80,4 +80,22 @@
   apply(simp only: option_rel_some[OF a])
   done
 
-end
\ No newline at end of file
+lemma option_map_id[id_simps]: "option_map id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  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
+  done
+
+end

--- a/Quot/QuotProd.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotProd.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -92,6 +92,12 @@
 lemma prod_fun_id[id_simps]: "prod_fun id id \<equiv> id"
   by (rule eq_reflection) (simp add: prod_fun_def)
 
+lemma prod_rel_eq[id_simps]: "prod_rel op = op = \<equiv> op ="
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply auto
+  done
+
 section {* general setup for products *}
 
 declare [[map * = (prod_fun, prod_rel)]]

--- a/Quot/QuotSum.thy	Fri Jan 08 14:43:30 2010 +0100
+++ b/Quot/QuotSum.thy	Fri Jan 08 15:02:12 2010 +0100
@@ -82,4 +82,22 @@
   apply(rule sum_fun_fun[OF q1 q2])
   done
 
-end
\ No newline at end of file
+lemma sum_map_id[id_simps]: "sum_map id id \<equiv> id"
+  apply (rule eq_reflection)
+  apply (rule ext)
+  apply (case_tac x)
+  apply (auto)
+  done
+
+lemma sum_rel_eq[id_simps]: "sum_rel op = 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
+  done
+
+end