--- a/Nominal/TySch.thy	Thu Mar 18 23:20:46 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 00:35:58 2010 +0100
@@ -55,6 +55,49 @@
 lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
 by (lifting set_eqvt)
 
+thm list_induct2'[no_vars]
+
+lemma fset_induct2:
+    "Pa {||} {||} \<Longrightarrow>
+    (\<forall>x xs. Pa (finsert x xs) {||}) \<Longrightarrow>
+    (\<forall>y ys. Pa {||} (finsert y ys)) \<Longrightarrow>
+    (\<forall>x xs y ys. Pa xs ys \<longrightarrow> Pa (finsert x xs) (finsert y ys)) \<Longrightarrow>
+    Pa xsa ysa"
+by (lifting list_induct2')
+
+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 fset_cong:
+  "(fset_to_set x = fset_to_set y) = (x = y)"
+  by (lifting set_cong)
+
+lemma supp_fset_to_set:
+  "supp (fset_to_set x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts)
+  apply (simp add: fset_cong)
+  done
+
+lemma inj_map_eq_iff:
+  "inj f \<Longrightarrow> (map f l \<approx> map f m) = (l \<approx> m)"
+  by (simp add: Set.expand_set_eq[symmetric] inj_image_eq_iff)
+
+lemma inj_fmap_eq_iff:
+  "inj f \<Longrightarrow> (fmap f l = fmap f m) = (l = m)"
+  by (lifting inj_map_eq_iff)
+
+lemma atom_fmap_cong:
+  shows "(fmap atom x = fmap atom y) = (x = y)"
+  apply(rule inj_fmap_eq_iff)
+  apply(simp add: inj_on_def)
+  done
+
 lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
 apply (induct l)
 apply (simp_all)
@@ -64,6 +107,12 @@
 lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
 by (lifting map_eqvt)
 
+lemma supp_fmap_atom:
+  "supp (fmap atom x) = supp x"
+  apply (simp add: supp_def)
+  apply (simp add: eqvts eqvts_raw atom_fmap_cong)
+  done
+
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"