1 theory Lambda |
1 theory Lambda |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 declare [[STEPS = 20]] |
6 declare [[STEPS = 21]] |
7 |
7 |
8 class s1 |
8 class s1 |
9 class s2 |
9 class s2 |
10 |
10 |
11 nominal_datatype lambda: |
11 nominal_datatype lambda: |
12 ('a, 'b) lam = |
12 ('a, 'b) lam = |
13 Var "name" |
13 Var "name" |
14 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" |
14 | App "('a::s1, 'b::s2) lam" "('a, 'b) lam" |
15 | Lam x::"name" l::"('a, 'b) lam" bind x in l |
15 | Lam x::"name" l::"('a, 'b) lam" bind x in l |
16 |
16 |
17 term Var_raw |
|
18 term Var |
|
19 term App_raw |
|
20 term App |
|
21 thm Var_def App_def Lam_def |
|
22 term abs_lam |
|
23 |
|
24 thm distinct |
17 thm distinct |
25 thm lam_raw.inducts |
18 thm induct |
26 thm lam_raw.exhaust |
19 thm exhaust |
27 thm fv_defs |
20 thm fv_defs |
28 thm bn_defs |
21 thm bn_defs |
29 thm perm_simps |
22 thm perm_simps |
30 thm perm_laws |
|
31 thm lam_raw.size |
|
32 thm eq_iff |
23 thm eq_iff |
33 thm eq_iff_simps |
24 thm fv_bn_eqvt |
34 thm fv_eqvt |
|
35 thm bn_eqvt |
|
36 thm size_eqvt |
25 thm size_eqvt |
37 |
26 |
38 ML {* |
|
39 val qtys = [@{typ "('a::{s1, fs}, 'b::{s2,fs}) lam"}] |
|
40 *} |
|
41 |
|
42 ML {* |
|
43 val thm_a = timeit (fn () => map (lift_thm @{context} qtys []) @{thms distinct}) |
|
44 *} |
|
45 |
|
46 ML {* |
|
47 val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.induct} |
|
48 *} |
|
49 |
|
50 ML {* |
|
51 val thms_i = map (lift_thm @{context} qtys []) @{thms lam_raw.exhaust} |
|
52 *} |
|
53 |
|
54 ML {* |
|
55 val thms_f = map (lift_thm @{context} qtys []) @{thms fv_defs} |
|
56 *} |
|
57 |
|
58 ML {* |
|
59 val thms_p = map (lift_thm @{context} qtys []) @{thms perm_simps} |
|
60 *} |
|
61 |
|
62 ML {* |
|
63 val thms_f = map (lift_thm @{context} qtys []) @{thms perm_laws} |
|
64 *} |
|
65 |
|
66 ML {* |
|
67 val simps = @{thms alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
68 prod.cases} |
|
69 *} |
|
70 |
|
71 ML {* |
|
72 val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff} |
|
73 *} |
|
74 |
|
75 ML {* |
|
76 val thms_e = map (lift_thm @{context} qtys simps) @{thms eq_iff_simps} |
|
77 *} |
|
78 |
|
79 |
|
80 ML {* |
|
81 val thms_f = map (lift_thm @{context} qtys []) @{thms bn_defs} |
|
82 *} |
|
83 |
|
84 ML {* |
|
85 val thms_f = map (lift_thm @{context} qtys []) @{thms bn_eqvt} |
|
86 *} |
|
87 |
|
88 ML {* |
|
89 val thms_f = map (lift_thm @{context} qtys []) @{thms fv_eqvt} |
|
90 *} |
|
91 |
|
92 ML {* |
|
93 val thms_f = map (lift_thm @{context} qtys []) @{thms size_eqvt} |
|
94 *} |
|
95 |
|
96 |
|
97 |
|
98 thm eq_iff |
|
99 |
27 |
100 thm lam.fv |
28 thm lam.fv |
101 thm lam.supp |
29 thm lam.supp |
102 lemmas supp_fn' = lam.fv[simplified lam.supp] |
30 lemmas supp_fn' = lam.fv[simplified lam.supp] |
103 |
31 |