diff -r a0c7290a4e27 -r 27cdc0a3a763 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Apr 21 12:25:52 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Mon Apr 26 10:01:13 2010 +0200
@@ -126,44 +126,109 @@
   typing :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow> bool" ("_ \<turnstile> _ : _" [60,60,60] 60) 
 where
     t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x : T"
-  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2 \<or> \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
+  | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> \<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : T2"
   | t_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; (x, T1) # \<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam x t : T1 \<rightarrow> T2"
 
-inductive
-  typing' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<Turnstile> _ : _" [60,60,60] 60) 
-where
-    t'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Var x : T"
-  | t'_App[intro]: "\<lbrakk>\<Gamma> \<Turnstile> t1 : T1\<rightarrow>T2 \<and> \<Gamma> \<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> App t1 t2 : T2"
-  | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> \<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
-  typing2' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ 2\<Turnstile> _ : _" [60,60,60] 60) 
-where
-    t2'_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Var x : T"
-  | t2'_App[intro]: "\<lbrakk>\<Gamma> 2\<Turnstile> t1 : T1\<rightarrow>T2 \<or> \<Gamma> 2\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> App t1 t2 : T2"
-  | t2'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> 2\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<Turnstile> Lam x t : T1\<rightarrow>T2"
-
-inductive
-  typing'' :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ |\<Turnstile> _ : _" [60,60,60] 60)
-and  valid' :: "(name\<times>ty) list \<Rightarrow> bool"
-where
-    v1[intro]: "valid' []"
-  | v2[intro]: "\<lbrakk>valid' \<Gamma>;atom x\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid' ((x,T)#\<Gamma>)"
-  | t'_Var[intro]: "\<lbrakk>valid' \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Var x : T"
-  | t'_App[intro]: "\<lbrakk>\<Gamma> |\<Turnstile> t1 : T1\<rightarrow>T2; \<Gamma> |\<Turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> App t1 t2 : T2"
-  | t'_Lam[intro]: "\<lbrakk>atom x\<sharp>\<Gamma>;(x,T1)#\<Gamma> |\<Turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> |\<Turnstile> Lam x t : T1\<rightarrow>T2"
-
 equivariance valid
 equivariance typing
-equivariance typing'
-equivariance typing2' 
-equivariance typing''
 
 thm valid.eqvt
 thm typing.eqvt
 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)"  
@@ -189,27 +254,9 @@
 declare permute_lam_raw.simps[eqvt]
 declare alpha_gen_eqvt[eqvt]
 equivariance alpha_lam_raw'
+
 thm eqvts_raw
 
-
-
-(* HERE *)
-
-lemma
-  assumes a: "alpha_lam_raw' t1 t2"
-  shows "alpha_lam_raw' (p \<bullet> t1) (p \<bullet> t2)"
-using a
-apply(induct)
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a1} 1*})
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a2} 1*})
-(*
-apply(tactic {* Nominal_Eqvt.eqvt_rel_case_tac 
-  @{context} ["Lambda.alpha_lam_raw'"] @{term "p::perm"} @{thm a3} 1*})
-*)
-oops
-
 section {* size function *}
 
 lemma size_eqvt_raw:
@@ -367,6 +414,29 @@
 done
 *)
 
+
+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