equal
deleted
inserted
replaced
17 thm lam.perm_simps |
17 thm lam.perm_simps |
18 thm lam.eq_iff |
18 thm lam.eq_iff |
19 thm lam.fv_bn_eqvt |
19 thm lam.fv_bn_eqvt |
20 thm lam.size_eqvt |
20 thm lam.size_eqvt |
21 |
21 |
|
22 ML {* |
|
23 Outer_Syntax.local_theory_to_proof; |
|
24 Proof.theorem |
|
25 *} |
|
26 |
|
27 ML {* |
|
28 fun prove_strong_ind pred_name avoids ctxt = |
|
29 let |
|
30 val _ = () |
|
31 in |
|
32 Proof.theorem NONE (fn thss => fn ctxt => ctxt) [] ctxt |
|
33 end |
|
34 |
|
35 (* outer syntax *) |
|
36 local |
|
37 structure P = Parse; |
|
38 structure S = Scan |
|
39 |
|
40 in |
|
41 val _ = |
|
42 Outer_Syntax.local_theory_to_proof "nominal_inductive" |
|
43 "prove strong induction theorem for inductive predicate involving nominal datatypes" |
|
44 Keyword.thy_goal |
|
45 (Parse.xname -- |
|
46 (Scan.optional (Parse.$$$ "avoids" |-- Parse.enum1 "|" (Parse.name -- |
|
47 (Parse.$$$ ":" |-- Parse.and_list1 Parse.term))) []) >> (fn (pred_name, avoids) => |
|
48 prove_strong_ind pred_name avoids)) |
|
49 |
|
50 end |
|
51 *} |
|
52 |
22 |
53 |
23 section {* Typing *} |
54 section {* Typing *} |
24 |
55 |
25 nominal_datatype ty = |
56 nominal_datatype ty = |
26 TVar string |
57 TVar string |
27 | TFun ty ty ("_ \<rightarrow> _") |
58 | TFun ty ty ("_ \<rightarrow> _") |
28 |
59 |
29 |
|
30 (* |
|
31 declare ty.perm[eqvt] |
|
32 |
60 |
33 inductive |
61 inductive |
34 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
62 valid :: "(name \<times> ty) list \<Rightarrow> bool" |
35 where |
63 where |
36 "valid []" |
64 "valid []" |
51 thm eqvts |
79 thm eqvts |
52 thm eqvts_raw |
80 thm eqvts_raw |
53 |
81 |
54 thm typing.induct[of "\<Gamma>" "t" "T", no_vars] |
82 thm typing.induct[of "\<Gamma>" "t" "T", no_vars] |
55 |
83 |
|
84 (* |
56 lemma |
85 lemma |
57 fixes c::"'a::fs" |
86 fixes c::"'a::fs" |
58 assumes a: "\<Gamma> \<turnstile> t : T" |
87 assumes a: "\<Gamma> \<turnstile> t : T" |
59 and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
88 and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x, T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
60 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> |
89 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> |