# HG changeset patch
# User cek@localhost.localdomain
# Date 1250772269 -7200
# Node ID 672e14609e6ef5619ebc262fc85effa4236e18c7
# Parent  e0b4bca46c6a1cbe657e3c5288a206bb130acecf
UNION - Append theorem

diff -r e0b4bca46c6a -r 672e14609e6e QuotMain.thy
--- 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
+
diff -r e0b4bca46c6a -r 672e14609e6e Quotients.thy
--- a/Quotients.thy	Thu Aug 20 10:31:44 2009 +0200
+++ b/Quotients.thy	Thu Aug 20 14:44:29 2009 +0200
@@ -138,7 +138,7 @@
 lemma QUOTIENT_PROD:
   assumes a: "QUOTIENT E1 Abs1 Rep1"
   and     b: "QUOTIENT E2 Abs2 Rep2"
-  shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)"
+  shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
 using a b unfolding QUOTIENT_def
 oops