# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1262959332 -3600
# Node ID 42b90994ac77e5040e2fdc2f6534c7de5b872e9d
# Parent  e1f1114ae8bd0740d36277d50555e27e3ac8bbfd
map and rel simps for all quotients; needed when changing the relations to aggregate ones.

diff -r e1f1114ae8bd -r 42b90994ac77 Quot/QuotOption.thy
--- 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
diff -r e1f1114ae8bd -r 42b90994ac77 Quot/QuotProd.thy
--- 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)]]
diff -r e1f1114ae8bd -r 42b90994ac77 Quot/QuotSum.thy
--- 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