# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268990689 -3600
# Node ID 2789dd26171a31ccbaf66f5a15dc08f9168f847e
# Parent  0d845717f1812ddca75e72859cfe3449953b599d# Parent  c8c2f83fadb47f3092a0ffa5d2c501146380421d
merge

diff -r c8c2f83fadb4 -r 2789dd26171a Nominal/Parser.thy
--- a/Nominal/Parser.thy	Fri Mar 19 09:40:57 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 19 10:24:49 2010 +0100
@@ -2,8 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift"
 begin
 
-atom_decl name
-
 section{* Interface for nominal_datatype *}
 
 text {*
diff -r c8c2f83fadb4 -r 2789dd26171a Nominal/TySch.thy
--- a/Nominal/TySch.thy	Fri Mar 19 09:40:57 2010 +0100
+++ b/Nominal/TySch.thy	Fri Mar 19 10:24:49 2010 +0100
@@ -59,12 +59,32 @@
 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"
-  oops
-
+  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 :: 'a :: pt) t \<and> P' d ts "
+proof -
+  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)
+    apply (rule allI)+
+    apply (rule a2)
+    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*)
+    sorry
+  then have "P a (0 \<bullet> t) \<and> P' d (0 \<bullet> ts)" by blast
+  then show ?thesis by simp
+qed
 
 lemma
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"