# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268990632 -3600
# Node ID 78d0adf8a086b18ca23a10445706c47f4a3baece
# Parent  6853ce3051184097bfb3b695c86420d9e8869340
TySch strong induction looks ok.

diff -r 6853ce305118 -r 78d0adf8a086 Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Mar 19 09:31:38 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 10:23:52 2010 +0100
@@ -62,18 +62,25 @@
   assumes a1: "\<And>name b. P b (Var name)"
   and     a2: "\<And>t1 t2 b. \<lbrakk>\<And>c. P c t1; \<And>c. P c t2\<rbrakk> \<Longrightarrow> P b (Fun t1 t2)"
   and     a3: "\<And>fset t b. \<lbrakk>\<And>c. P c t; fset_to_set (fmap atom fset) \<sharp>* b\<rbrakk> \<Longrightarrow> P' b (All fset t)"
-  shows "P a t \<and> P' d ts "
+  shows "P (a :: 'a :: pt) t \<and> P' d ts "
 proof -
-  have " (\<forall>p. P a (p \<bullet> t)) \<and> (\<forall>p. P' d (p \<bullet> ts))"
+  have " (\<forall>p a. P a (p \<bullet> t)) \<and> (\<forall>p d. P' d (p \<bullet> ts))"
     apply (rule t_tyS.induct)
     apply (simp add: a1)
-    apply (simp_all)
-    apply (rule allI)
+    apply (simp)
+    apply (rule allI)+
     apply (rule a2)
-    defer defer
+    apply simp
+    apply simp
+    apply (rule allI)
     apply (rule allI)
+    apply(subgoal_tac "\<exists>new::name fset. fset_to_set (fmap atom new) \<sharp>* (d, All (p \<bullet> fset) (p \<bullet> t))
+                                      \<and> fcard new = fcard fset")
+    apply clarify
+    (*apply(rule_tac t="p \<bullet> All fset t" and 
+                   s="(((p \<bullet> fset) \<leftrightarrow> new) + p) \<bullet> All fset t" in subst)
     apply (rule a3)
-    apply simp_all
+    apply simp_all*)
     sorry
   then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
   then show ?thesis by simp