--- a/QuotMain.thy	Thu Aug 20 10:31:44 2009 +0200
+++ b/QuotMain.thy	Thu Aug 20 14:44:29 2009 +0200
@@ -583,3 +583,63 @@
 apply(rule list_eq_sym)
 done
 
+lemma helper:
+  assumes a : "list_eq l1 r1"
+  shows "list_eq (l1 @ l) (r1 @ l)"
+  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)
+done
+
+lemma yyy :
+  shows "
+    (
+     (UNION EMPTY s = s) &
+     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
+    ) = (
+     ((ABS_fset ([] @ REP_fset s)) = s) &
+     ((ABS_fset ((e # (REP_fset s1)) @ REP_fset s2)) = ABS_fset (e # (REP_fset s1 @ REP_fset s2)))
+    )"
+  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(rule helper)
+  apply(rule list_eq.intros(3))
+  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+  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(rule helper)
+  apply(rule list_eq.intros(3))
+  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+  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(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 list_eq_sym)
+done
+
+lemma
+  shows "
+    (
+     (UNION EMPTY s = s) &
+     ((UNION (INSERT e s1) s2) = (INSERT e (UNION s1 s2)))
+    )"
+  apply(simp add:yyy)
+  apply (unfold REP_fset_def ABS_fset_def)
+  apply (rule QUOT_TYPE.thm10[OF QUOT_TYPE_fset])
+done
+