--- a/Nominal/FSet.thy	Fri Mar 19 00:36:08 2010 +0100
+++ b/Nominal/FSet.thy	Fri Mar 19 06:55:17 2010 +0100
@@ -66,7 +66,9 @@
 section {* Augmenting a set -- @{const finsert} *}
 
 lemma nil_not_cons:
-  shows "\<not>[] \<approx> x # xs"
+  shows
+  "\<not>[] \<approx> x # xs"
+  "\<not>x # xs \<approx> []"
   by auto
 
 lemma memb_cons_iff:
@@ -132,7 +134,7 @@
   apply(metis)
   apply(drule_tac x="[x \<leftarrow> b. x \<noteq> a1]" in meta_spec)
   apply(simp add: fcard_raw_delete_one)
-  apply(metis Suc_pred' fcard_raw_gt_0 fcard_raw_delete_one memb_def)
+  apply(metis Suc_pred'[OF fcard_raw_gt_0] fcard_raw_delete_one memb_def)
   done
 
 lemma fcard_raw_rsp[quot_respect]:
@@ -253,11 +255,23 @@
   "a @ b \<approx> b @ a"
   by auto
 
-
 lemma append_rsp[quot_respect]:
   shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @"
   by (auto)
 
+lemma set_cong: "(set x = set y) = (x \<approx> y)"
+  apply rule
+  apply simp_all
+  apply (induct x y rule: list_induct2')
+  apply simp_all
+  apply auto
+  done
+
+lemma inj_map_eq_iff:
+  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
+  by (simp add: expand_set_eq[symmetric] inj_image_eq_iff)
+
+
 
 
 section {* lifted part *}
@@ -277,7 +291,8 @@
   by (lifting memb_absorb)
 
 lemma fempty_not_finsert[simp]:
-  shows "{||} \<noteq> finsert x S"
+  "{||} \<noteq> finsert x S"
+  "finsert x S \<noteq> {||}"
   by (lifting nil_not_cons)
 
 lemma finsert_left_comm:
@@ -294,7 +309,7 @@
 
 text {* fset_to_set *}
 
-lemma fset_to_set_simps:
+lemma fset_to_set_simps[simp]:
   "fset_to_set {||} = {}"
   "fset_to_set (finsert (h :: 'b) t) = insert h (fset_to_set t)"
   by (lifting list2set_thm)
@@ -307,6 +322,10 @@
   "(\<forall>a. a \<notin> fset_to_set A) = (A = {||})"
   by (lifting none_mem_nil)
 
+lemma fset_cong:
+  "(fset_to_set x = fset_to_set y) = (x = y)"
+  by (lifting set_cong)
+
 text {* fcard *}
 
 lemma fcard_fempty [simp]:
@@ -345,15 +364,15 @@
   shows "\<lbrakk>S = {||} \<Longrightarrow> P; \<And>x S'. S = finsert x S' \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   by (lifting list.exhaust)
 
-lemma fset_induct[case_names fempty finsert]:
+lemma fset_induct_weak[case_names fempty finsert]:
   shows "\<lbrakk>P {||}; \<And>x S. P S \<Longrightarrow> P (finsert x S)\<rbrakk> \<Longrightarrow> P S"
   by (lifting list.induct)
 
-lemma fset_induct2[case_names fempty finsert, induct type: fset]:
+lemma fset_induct[case_names fempty finsert, induct type: fset]:
   assumes prem1: "P {||}" 
   and     prem2: "\<And>x S. \<lbrakk>x |\<notin>| S; P S\<rbrakk> \<Longrightarrow> P (finsert x S)"
   shows "P S"
-proof(induct S rule: fset_induct)
+proof(induct S rule: fset_induct_weak)
   case fempty
   show "P {||}" by (rule prem1)
 next
@@ -371,6 +390,38 @@
   qed
 qed
 
+lemma fset_induct2:
+  "P {||} {||} \<Longrightarrow>
+  (\<And>x xs. x |\<notin>| xs \<Longrightarrow> P (finsert x xs) {||}) \<Longrightarrow>
+  (\<And>y ys. y |\<notin>| ys \<Longrightarrow> P {||} (finsert y ys)) \<Longrightarrow>
+  (\<And>x xs y ys. \<lbrakk>P xs ys; x |\<notin>| xs; y |\<notin>| ys\<rbrakk> \<Longrightarrow> P (finsert x xs) (finsert y ys)) \<Longrightarrow>
+  P xsa ysa"
+  apply (induct xsa arbitrary: ysa)
+  apply (induct_tac x rule: fset_induct)
+  apply simp_all
+  apply (induct_tac xa rule: fset_induct)
+  apply simp_all
+  done
 
+(* fmap *)
+lemma fmap_simps[simp]:
+  "fmap (f :: 'a \<Rightarrow> 'b) {||} = {||}"
+  "fmap f (finsert x xs) = finsert (f x) (fmap f xs)"
+  by (lifting map.simps)
+
+lemma fmap_set_image:
+  "fset_to_set (fmap f fs) = f ` (fset_to_set fs)"
+  apply (induct fs)
+  apply (simp_all)
+done
+
+lemma inj_fmap_eq_iff:
+  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
+  by (lifting inj_map_eq_iff)
+
+ML {*
+fun dest_fsetT (Type ("FSet.fset", [T])) = T
+  | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []);
+*}
 
 end