--- a/Nominal/TySch.thy	Fri Mar 19 06:55:17 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 08:31:43 2010 +0100
@@ -10,109 +10,6 @@
 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)
-
-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)
-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)
-
-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"
@@ -125,42 +22,39 @@
 thm t_tyS.perm
 thm t_tyS.inducts
 thm t_tyS.distinct
+ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}
 
 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
+  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
+  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]
 
@@ -169,7 +63,7 @@
   \<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"
-
+  oops
 
 
 lemma