equal
deleted
inserted
replaced
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 17]] |
7 declare [[STEPS = 18]] |
8 |
8 |
9 nominal_datatype trm = |
9 nominal_datatype trm = |
10 Var "name" |
10 Var "name" |
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
23 |
23 |
24 (* can lift *) |
24 (* can lift *) |
25 thm distinct |
25 thm distinct |
26 thm trm_raw_assg_raw.inducts |
26 thm trm_raw_assg_raw.inducts |
27 thm fv_defs |
27 thm fv_defs |
28 |
28 thm perm_simps |
|
29 thm perm_laws |
|
30 thm trm_raw_assg_raw.size(9 - 16) |
29 |
31 |
30 (* cannot lift yet *) |
32 (* cannot lift yet *) |
31 thm eq_iff |
33 thm eq_iff |
32 thm eq_iff_simps |
34 thm eq_iff_simps |
33 thm perm_simps |
|
34 thm perm_laws |
|
35 thm trm_raw_assg_raw.size(9 - 16) |
|
36 |
|
37 (* rsp lemmas *) |
|
38 thm size_rsp |
|
39 thm funs_rsp |
|
40 thm constrs_rsp |
|
41 thm permute_rsp |
|
42 |
|
43 declare constrs_rsp[quot_respect] |
|
44 declare funs_rsp[quot_respect] |
|
45 declare size_rsp[quot_respect] |
|
46 declare permute_rsp[quot_respect] |
|
47 |
|
48 ML {* |
|
49 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
|
50 *} |
|
51 |
|
52 ML {* |
|
53 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
|
54 *} |
|
55 |
|
56 ML {* |
|
57 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
|
58 *} |
|
59 |
35 |
60 instantiation trm and assg :: size |
36 instantiation trm and assg :: size |
61 begin |
37 begin |
62 |
38 |
63 quotient_definition |
39 quotient_definition |
69 is "size :: assg_raw \<Rightarrow> nat" |
45 is "size :: assg_raw \<Rightarrow> nat" |
70 |
46 |
71 instance .. |
47 instance .. |
72 |
48 |
73 end |
49 end |
74 |
|
75 ML {* |
|
76 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
77 *} |
|
78 |
|
79 |
|
80 |
50 |
81 instantiation trm and assg :: pt |
51 instantiation trm and assg :: pt |
82 begin |
52 begin |
83 |
53 |
84 quotient_definition |
54 quotient_definition |
99 apply(default) |
69 apply(default) |
100 sorry |
70 sorry |
101 |
71 |
102 end |
72 end |
103 |
73 |
104 |
74 ML {* |
105 (* |
75 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
106 lemma [quot_respect]: |
76 *} |
107 "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" |
77 |
108 apply(simp) |
78 ML {* |
109 sorry |
79 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.inducts} |
110 *) |
80 *} |
|
81 |
|
82 ML {* |
|
83 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_defs} |
|
84 *} |
|
85 |
|
86 ML {* |
|
87 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
88 *} |
|
89 |
|
90 ML {* |
|
91 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps} |
|
92 *} |
|
93 |
|
94 ML {* |
|
95 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
|
96 *} |
|
97 |
|
98 |
|
99 |
|
100 |
|
101 |
|
102 section {* NOT *} |
|
103 |
111 |
104 |
112 ML {* |
105 ML {* |
113 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} |
106 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} |
114 *} |
107 *} |
115 |
108 |
131 ML {* |
124 ML {* |
132 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
125 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
133 *} |
126 *} |
134 |
127 |
135 section {* NOT *} |
128 section {* NOT *} |
136 |
|
137 |
|
138 ML {* |
|
139 val thms_i = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms trm_raw_assg_raw.size(9 - 16)} |
|
140 *} |
|
141 |
|
142 |
|
143 ML {* |
|
144 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
|
145 *} |
|
146 |
|
147 ML {* |
|
148 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
|
149 *} |
|
150 |
|
151 |
129 |
152 ML {* |
130 ML {* |
153 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
131 val thms_p = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_simps(1)} |
154 *} |
132 *} |
155 |
133 |