diff -r 8cf5c3e58889 -r 8ed62410236e Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Fri Nov 05 15:21:10 2010 +0000
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Nov 06 06:18:41 2010 +0000
@@ -4,7 +4,8 @@
 
 section {*** Type Schemes ***}
 
-atom_decl name
+atom_decl name 
+
 
 (* defined as a single nominal datatype *)
 
@@ -50,6 +51,45 @@
 thm tys2.fresh
 
 
+lemma strong_exhaust:
+  fixes c::"'a::fs"
+  assumes "\<And>names ty. \<lbrakk>fset (map_fset atom names) \<sharp>* c; y = All2 names ty\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+apply(rule_tac y="y" in tys2.exhaust)
+apply(rename_tac names ty2)
+apply(subgoal_tac "\<exists>q. (q \<bullet> (fset (map_fset atom names))) \<sharp>* c \<and> supp (All2 names ty2) \<sharp>* q")
+apply(erule exE)
+apply(perm_simp)
+apply(erule conjE)
+apply(rule assms(1))
+apply(assumption)
+apply(clarify)
+apply(drule supp_perm_eq[symmetric])
+apply(simp)
+thm at_set_avoiding
+apply(rule at_set_avoiding2)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp add: finite_supp)
+apply(simp)
+apply(simp add: fresh_star_def)
+apply(simp add: tys2.fresh)
+done
+
+
+lemma strong_induct:
+  fixes c::"'a::fs"
+  assumes "\<And>names ty2 c. fset (map_fset atom names) \<sharp>* c \<Longrightarrow> P c (All2 names ty2)"
+  shows "P c tys"
+using assms
+apply(induction_schema)
+apply(rule_tac y="tys" in strong_exhaust)
+apply(blast)
+apply(relation "measure (\<lambda>(x,y). size y)")
+apply(simp_all add: tys2.size)
+done
+
+
 text {* *}
 
 (*