# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264448142 -3600
# Node ID 5455b19ef138aff8aeeec5c11188923663acd7d3
# Parent  0419b20ee83cdf4db4839da7bd450914956fc5aa
re-inserted lemma in QuotList

diff -r 0419b20ee83c -r 5455b19ef138 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Mon Jan 25 19:52:53 2010 +0100
+++ b/Quot/QuotList.thy	Mon Jan 25 20:35:42 2010 +0100
@@ -192,13 +192,9 @@
 apply(simp_all)
 done
 
-
-(* Rest are unused *)
-text {*
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
 by (induct x) (auto simp add: a)
-*}
 
 end
diff -r 0419b20ee83c -r 5455b19ef138 Quot/QuotSum.thy
--- a/Quot/QuotSum.thy	Mon Jan 25 19:52:53 2010 +0100
+++ b/Quot/QuotSum.thy	Mon Jan 25 20:35:42 2010 +0100
@@ -23,30 +23,22 @@
   assumes a: "equivp R1"
   assumes b: "equivp R2"
   shows "equivp (sum_rel R1 R2)"
-unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def
-apply(auto)
-apply(case_tac x)
-apply(auto simp add: equivp_reflp[OF a] equivp_reflp[OF b])
-apply(case_tac x)
-apply(case_tac y)
-prefer 3
-apply(case_tac y)
-apply(auto simp add: equivp_symp[OF a] equivp_symp[OF b])
-apply(case_tac x)
-apply(case_tac y)
-apply(case_tac z)
-prefer 3
-apply(case_tac z)
-prefer 5
-apply(case_tac y)
-apply(case_tac z)
-prefer 3
-apply(case_tac z)
-apply(auto)
-apply(metis equivp_transp[OF b])
-apply(metis equivp_transp[OF a])
-done
+  apply(rule equivpI)
+  unfolding reflp_def symp_def transp_def
+  apply(auto)
+  apply(case_tac [!] x)
+  apply(simp_all add: equivp_reflp[OF a] equivp_reflp[OF b])
+  apply(case_tac [!] y)
+  apply(simp_all add: equivp_symp[OF a] equivp_symp[OF b])
+  apply(case_tac [!] z)
+  apply(simp_all)
+  apply(rule equivp_transp[OF a])
+  apply(assumption)+
+  apply(rule equivp_transp[OF b])
+  apply(assumption)+
+  done
 
+(*
 lemma sum_fun_fun:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
@@ -62,34 +54,38 @@
   unfolding Quotient_def 
   apply metis+
   done
+*)
 
 lemma sum_quotient[quot_thm]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "Quotient (sum_rel R1 R2) (sum_map Abs1 Abs2) (sum_map Rep1 Rep2)"
   unfolding Quotient_def
-  apply(rule conjI)
-  apply(rule allI)
+  apply(auto)
+  apply(case_tac a)
+  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]
+                      Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
   apply(case_tac a)
-  apply(simp add: Quotient_abs_rep[OF q1])
-  apply(simp add: Quotient_abs_rep[OF q2])
-  apply(rule conjI)
-  apply(rule allI)
-  apply(case_tac a)
-  apply(simp add: Quotient_rel_rep[OF q1])
-  apply(simp add: Quotient_rel_rep[OF q2])
-  apply(rule allI)+
-  apply(rule sum_fun_fun[OF q1 q2])
+  apply(simp_all add: Quotient_abs_rep[OF q1] Quotient_rel_rep[OF q1]
+                      Quotient_abs_rep[OF q2] Quotient_rel_rep[OF q2])
+  apply(case_tac [!] r)
+  apply(case_tac [!] s)
+  apply(simp_all)
+  using q1 q2
+  unfolding Quotient_def
+  apply(blast)+
   done
 
-lemma sum_map_id[id_simps]: "sum_map id id \<equiv> id"
+lemma sum_map_id[id_simps]: 
+  shows "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 ="
+lemma sum_rel_eq[id_simps]: 
+  "sum_rel op = op = \<equiv> op ="
   apply (rule eq_reflection)
   apply (rule ext)+
   apply (case_tac x)