--- a/Nominal/Parser.thy	Thu Mar 18 22:06:28 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 23:20:46 2010 +0100
@@ -410,7 +410,7 @@
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = tracing "Finite Support";
-  val supports = map (prove_supports lthy20 q_perm) consts
+  val supports = map (prove_supports lthy20 q_perm) consts handle _ => []
   val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys) handle _ => []
   val thy3 = Local_Theory.exit_global lthy20;
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;

--- a/Nominal/TySch.thy	Thu Mar 18 22:06:28 2010 +0100
+++ b/Nominal/TySch.thy	Thu Mar 18 23:20:46 2010 +0100
@@ -1,5 +1,5 @@
 theory TySch
-imports "Parser" "../Attic/Prove"
+imports "Parser" "../Attic/Prove" "FSet"
 begin
 
 atom_decl name
@@ -10,21 +10,121 @@
 ML {* val _ = cheat_fv_eqvt := false *}
 ML {* val _ = cheat_alpha_eqvt := false *}
 
+lemma permute_rsp_fset[quot_respect]:
+  "(op = ===> op \<approx> ===> op \<approx>) permute permute"
+  apply (simp add: eqvts[symmetric])
+  apply clarify
+  apply (subst permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
+  apply (subst mem_eqvt[symmetric])
+  apply (erule_tac x="- x \<bullet> xb" in allE)
+  apply simp
+  done
+
+instantiation FSet.fset :: (pt) pt
+begin
+
+term "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+quotient_definition
+  "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+is
+  "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
+lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
+by (rule permute_zero)
+
+lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
+by (lifting permute_list_zero)
+
+lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
+by (rule permute_plus)
+
+lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
+by (lifting permute_list_plus)
+
+instance
+apply default
+apply (rule permute_fset_zero)
+apply (rule permute_fset_plus)
+done
+
+end
+
+lemma fset_to_set_eqvt[eqvt]: "pi \<bullet> (fset_to_set x) = fset_to_set (pi \<bullet> x)"
+by (lifting set_eqvt)
+
+lemma map_eqvt[eqvt]: "pi \<bullet> (map f l) = map (pi \<bullet> f) (pi \<bullet> l)"
+apply (induct l)
+apply (simp_all)
+apply (simp only: eqvt_apply)
+done
+
+lemma fmap_eqvt[eqvt]: "pi \<bullet> (fmap f l) = fmap (pi \<bullet> f) (pi \<bullet> l)"
+by (lifting map_eqvt)
+
 nominal_datatype t =
   Var "name"
 | Fun "t" "t"
 and tyS =
-  All xs::"name set" ty::"t" bind xs in ty
+  All xs::"name fset" ty::"t" bind xs in ty
 
 thm t_tyS.fv
 thm t_tyS.eq_iff
 thm t_tyS.bn
 thm t_tyS.perm
-thm t_tyS.induct
+thm t_tyS.inducts
 thm t_tyS.distinct
 
+lemma finite_fv_t_tyS:
+  shows "finite (fv_t t)" "finite (fv_tyS ts)"
+  by (induct rule: t_tyS.inducts) (simp_all)
+
+lemma infinite_Un:
+  shows "infinite (S \<union> T) \<longleftrightarrow> infinite S \<or> infinite T"
+  by simp
+
+lemma supp_fv_t_tyS:
+  shows "fv_t t = supp t" "fv_tyS ts = supp ts"
+apply(induct rule: t_tyS.inducts)
+apply(simp_all only: t_tyS.fv)
+prefer 3
+apply(rule_tac t="supp (All fset t)" and s="supp (Abs (fset_to_set (fmap atom fset)) t)" in subst)
+prefer 2
+apply(subst finite_supp_Abs)
+apply(drule sym)
+apply(simp add: finite_fv_t_tyS(1))
+apply(simp)
+apply(simp_all (no_asm) only: supp_def)
+apply(simp_all only: t_tyS.perm)
+apply(simp_all only: permute_ABS)
+apply(simp_all only: t_tyS.eq_iff Abs_eq_iff)
+apply(simp_all only: alpha_gen)
+apply(simp_all only: eqvts[symmetric])
+apply(simp_all only: eqvts eqvts_raw)
+apply(simp_all only: supp_at_base[symmetric,simplified supp_def])
+apply(simp_all only: infinite_Un[symmetric] Collect_disj_eq[symmetric])
+apply(simp_all only: de_Morgan_conj[symmetric])
+done
+
+instance t and tyS :: fs
+apply default
+apply (simp_all add: supp_fv_t_tyS[symmetric] finite_fv_t_tyS)
+done
+
+lemmas t_tyS_supp = t_tyS.fv[simplified supp_fv_t_tyS]
+
+lemma induct:
+"\<lbrakk>\<And>name b. P b (Var name);
+  \<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2);
+  \<And>fset t. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)
+ \<rbrakk> \<Longrightarrow> P a t"
+
+
+
 lemma
-  shows "All {a, b} (Fun (Var a) (Var b)) = All {b, a} (Fun (Var a) (Var b))"
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen)
@@ -33,7 +133,7 @@
   done
 
 lemma
-  shows "All {a, b} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var b) (Var a))"
+  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alpha_gen fresh_star_def eqvts)
@@ -41,7 +141,7 @@
   done
 
 lemma
-  shows "All {a, b, c} (Fun (Var a) (Var b)) = All {a, b} (Fun (Var a) (Var b))"
+  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: t_tyS.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alpha_gen fresh_star_def eqvts t_tyS.eq_iff)
@@ -49,7 +149,7 @@
 
 lemma
   assumes a: "a \<noteq> b"
-  shows "\<not>(All {a, b} (Fun (Var a) (Var b)) = All {c} (Fun (Var c) (Var c)))"
+  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
   using a
   apply(simp add: t_tyS.eq_iff)
   apply(clarify)