--- 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