--- a/Nominal/Ex/Lambda.thy	Sun Apr 25 09:26:36 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 26 08:08:20 2010 +0200
@@ -137,6 +137,98 @@
 thm eqvts
 thm eqvts_raw
 
+thm typing.induct[of "\<Gamma>" "t" "T", no_vars]
+
+lemma
+  fixes c::"'a::fs"
+  assumes a: "\<Gamma> \<turnstile> t : T" 
+  and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T"
+  and a2: "\<And>\<Gamma> t1 T1 T2 t2 c. \<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<And>d. P d \<Gamma> t1 T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1; \<And>d. P d \<Gamma> t2 T1\<rbrakk> 
+           \<Longrightarrow> P c \<Gamma> (App t1 t2) T2"
+  and a3: "\<And>x \<Gamma> T1 t T2 c. \<lbrakk>atom x \<sharp> c; atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2; \<And>d. P d ((x, T1) # \<Gamma>) t T2\<rbrakk> 
+           \<Longrightarrow> P c \<Gamma> (Lam x t) T1 \<rightarrow> T2"
+  shows "P c \<Gamma> t T"
+proof -
+  from a have "\<And>p c. P c (p \<bullet> \<Gamma>) (p \<bullet> t) (p \<bullet> T)"
+  proof (induct)
+    case (t_Var \<Gamma> x T p c)
+    then show ?case
+      apply -
+      apply(perm_strict_simp)
+      apply(rule a1)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      done
+  next
+    case (t_App \<Gamma> t1 T1 T2 t2 p c)
+    then show ?case
+      apply -
+      apply(perm_strict_simp)
+      apply(rule_tac ?T1.0="p \<bullet> T1" in a2)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      apply(assumption)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      apply(assumption)
+      done
+  next
+    case (t_Lam x \<Gamma> T1 t T2 p c)
+    then show ?case
+      apply -
+      apply(subgoal_tac "\<exists>q. (q \<bullet> {p \<bullet> atom x}) \<sharp>* c \<and> 
+        supp (p \<bullet> \<Gamma>, p \<bullet> Lam x t, p \<bullet> (T1 \<rightarrow> T2)) \<sharp>* q")
+      apply(erule exE)
+      apply(rule_tac t="p \<bullet> \<Gamma>" and  s="q \<bullet> p \<bullet> \<Gamma>" in subst)
+      apply(rule supp_perm_eq)
+      apply(simp add: supp_Pair fresh_star_union)
+      apply(rule_tac t="p \<bullet> Lam x t" and  s="q \<bullet> p \<bullet> Lam x t" in subst)
+      apply(rule supp_perm_eq)
+      apply(simp add: supp_Pair fresh_star_union)
+      apply(rule_tac t="p \<bullet> (T1 \<rightarrow> T2)" and  s="q \<bullet> p \<bullet> (T1 \<rightarrow> T2)" in subst)
+      apply(rule supp_perm_eq)
+      apply(simp add: supp_Pair fresh_star_union)
+      apply(simp add: eqvts)
+      apply(rule a3)
+      apply(simp add: fresh_star_def)
+      apply(rule_tac p="-q" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      apply(rule_tac p="-q" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+      apply(assumption)
+      apply(drule_tac x="d" in meta_spec)
+      apply(drule_tac x="q + p" in meta_spec)
+      apply(simp)
+      apply(rule at_set_avoiding2)
+      apply(simp add: finite_supp)
+      apply(simp add: finite_supp)
+      apply(simp add: finite_supp)
+      apply(rule_tac p="-p" in permute_boolE)
+      apply(perm_strict_simp add: permute_minus_cancel)
+	(* supplied by the user *)
+      apply(simp add: fresh_star_prod)
+      apply(simp add: fresh_star_def)
+
+
+      done
+(* HERE *)      
+
+
+
+
+
+
 
 inductive
   tt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"  
@@ -323,6 +415,26 @@
 *)
 
 
+ML {*
+
+fun prove_strong_ind (pred_name, avoids) ctxt = 
+  Proof.theorem NONE (K I) [] ctxt
+
+local structure P = OuterParse and K = OuterKeyword in
+
+val _ =
+  OuterSyntax.local_theory_to_proof "nominal_inductive"
+    "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
+      (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
+        (P.$$$ ":" |-- P.and_list1 P.term))) []) >>  prove_strong_ind)
+
+end;
+
+*}
+
+nominal_inductive typing
+
+
 
 end