# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271084719 -7200
# Node ID 69fff336dd189e1612179ba55ee8e59706e079d2
# Parent  2e849bc2163ae2a7ffe6519ac424ff2ea0b7275e
Porting lemmas from Quotient package FSet to new FSet.

diff -r 2e849bc2163a -r 69fff336dd18 Nominal/FSet.thy
--- a/Nominal/FSet.thy	Mon Apr 12 14:31:23 2010 +0200
+++ b/Nominal/FSet.thy	Mon Apr 12 17:05:19 2010 +0200
@@ -115,12 +115,39 @@
 is
   "fcard_raw"
 
+lemma fcard_raw_0:
+  fixes a :: "'a list"
+  shows "(fcard_raw a = 0) = (a \<approx> [])"
+  apply (induct a)
+  apply auto
+  apply (drule memb_absorb)
+  apply (auto simp add: nil_not_cons)
+  done
+
 lemma fcard_raw_gt_0:
   assumes a: "x \<in> set xs"
   shows "0 < fcard_raw xs"
   using a
   by (induct xs) (auto simp add: memb_def)
 
+lemma fcard_raw_not_memb:
+  fixes x :: "'a"
+  fixes xs :: "'a list"
+  shows "(~(memb x xs)) = (fcard_raw (x # xs) = Suc (fcard_raw xs))"
+  by auto
+
+lemma fcard_raw_suc:
+  fixes xs :: "'a list"
+  fixes n :: "nat"
+  assumes c: "fcard_raw xs = Suc n"
+  shows "\<exists>a ys. ~(memb a ys) \<and> xs \<approx> (a # ys)"
+  using c
+  apply(induct xs)
+  apply simp
+  apply (auto)
+  apply (metis memb_def)
+  done
+
 lemma fcard_raw_delete_one:
   "fcard_raw ([x \<leftarrow> xs. x \<noteq> y]) = (if memb y xs then fcard_raw xs - 1 else fcard_raw xs)"
   by (induct xs) (auto dest: fcard_raw_gt_0 simp add: memb_def)
@@ -149,6 +176,10 @@
 is
  "map"
 
+lemma map_append:
+  "(map f (a @ b)) \<approx> (map f a) @ (map f b)"
+  by simp
+
 text {* raw section *}
 
 lemma map_rsp_aux:
@@ -271,8 +302,14 @@
   "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
   by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
 
+quotient_definition
+  "fconcat :: ('a fset) fset \<Rightarrow> 'a fset"
+is
+  "concat"
 
-
+lemma list_equiv_rsp[quot_respect]:
+  shows "(op \<approx> ===> op \<approx> ===> op =) op \<approx> op \<approx>"
+  by auto
 
 section {* lifted part *}
 
@@ -336,9 +373,18 @@
   shows "fcard (finsert x S) = (if x |\<in>| S then fcard S else Suc (fcard S))"
   by (lifting fcard_raw_cons)
 
+lemma fcard_0: "(fcard a = 0) = (a = {||})"
+  by (lifting fcard_raw_0)
+
 lemma fcard_gt_0: "x \<in> fset_to_set xs \<Longrightarrow> 0 < fcard xs"
   by (lifting fcard_raw_gt_0)
 
+lemma fcard_not_memb: "(x |\<notin>| xs) = (fcard (finsert x xs) = Suc (fcard xs))"
+  by (lifting fcard_raw_not_memb)
+
+lemma fcard_suc: "fcard xs = Suc n \<Longrightarrow> \<exists>a ys. a |\<notin>| ys \<and> xs = finsert a ys"
+  by (lifting fcard_raw_suc)
+
 text {* funion *}
 
 lemma funion_simps[simp]:
@@ -419,6 +465,9 @@
   "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
   by (lifting inj_map_eq_iff)
 
+lemma fmap_funion: "fmap f (a |\<union>| b) = fmap f a |\<union>| fmap f b"
+  by (lifting map_append)
+
 ML {*
 fun dest_fsetT (Type ("FSet.fset", [T])) = T
   | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);