# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1250854618 -7200
# Node ID 0eb89a350f434d0641baec49249c7104f4a2835d
# Parent  672e14609e6ef5619ebc262fc85effa4236e18c7
tuned

diff -r 672e14609e6e -r 0eb89a350f43 QuotMain.thy
--- a/QuotMain.thy	Thu Aug 20 14:44:29 2009 +0200
+++ b/QuotMain.thy	Fri Aug 21 13:36:58 2009 +0200
@@ -60,8 +60,18 @@
 unfolding ABS_def
 by (simp only: equiv[simplified EQUIV_def] lem7)
 
+
 lemma REP_ABS_rsp:
-  shows "R f g \<Longrightarrow> R f (REP (ABS g))"
+  shows "R f (REP (ABS g)) = R f g"
+  and   "R (REP (ABS g)) f = R g f"
+apply(subst thm11)
+apply(simp add: thm10 thm11)
+apply(subst thm11)
+apply(simp add: thm10 thm11)
+done
+
+lemma REP_ABS_rsp:
+  shows "R g g \<Longrightarrow> (REP (ABS g) = g"
 apply(subst thm11)
 apply(simp add: thm10 thm11)
 done
@@ -557,8 +567,8 @@
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
 apply(rule mem_respects)
-apply(unfold REP_fset_def ABS_fset_def)
-apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+        simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 apply(rule list_eq.intros)
 done
 
@@ -584,20 +594,16 @@
 done
 
 lemma helper:
-  assumes a : "list_eq l1 r1"
-  shows "list_eq (l1 @ l) (r1 @ l)"
+  assumes a : "list_eq l1 l2"  
+  shows "list_eq (l1 @ s) (l2 @ s)"
   using a
   apply(induct)
-  apply(simp add:list_eq.intros)
-  apply(simp add:list_eq_sym)
-  apply(simp add:list_eq.intros(3))
-  apply(simp add:list_eq.intros(4))
-  apply(simp add:list_eq.intros(5))
-  apply(rule_tac list_eq.intros(6))
-  apply(assumption)
-  apply(assumption)
+  apply(auto intro: list_eq.intros)
+  apply(simp add: list_eq_sym)
 done
 
+thm list_eq.intros
+
 lemma yyy :
   shows "
     (
@@ -610,25 +616,28 @@
   unfolding UNION_def EMPTY_def INSERT_def
   apply(rule_tac f="(op &)" in arg_cong2)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply (unfold REP_fset_def ABS_fset_def)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])
+  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,
+                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
   apply(simp)
   apply(rule_tac f="(op =)" in arg_cong2)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])
+  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
+                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
+                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
-  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset,symmetric])
-  apply(fold REP_fset_def ABS_fset_def)
+  apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
+                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule list_eq.intros(5))
   apply(rule list_eq.intros(3))
-  apply (unfold REP_fset_def ABS_fset_def)
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+                 simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
 done