Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
UNION - Append theorem
authorcek@localhost.localdomain
Thu, 20 Aug 2009 14:44:29 +0200
changeset 3 672e14609e6e
parent 2 e0b4bca46c6a
child 4 0eb89a350f43
UNION - Append theorem
QuotMain.thy file | annotate | diff | comparison | revisions
Quotients.thy file | annotate | diff | comparison | revisions 
--- 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
+
--- 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
nominal2