107 apply(blast) |
107 apply(blast) |
108 done |
108 done |
109 |
109 |
110 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
110 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
111 |
111 |
|
112 ML {* val _ = recursive := true *} |
|
113 |
|
114 nominal_datatype lam' = |
|
115 VAR' "name" |
|
116 | APP' "lam'" "lam'" |
|
117 | LAM' x::"name" t::"lam'" bind x in t |
|
118 | LET' bp::"bp'" t::"lam'" bind "bi' bp" in t |
|
119 and bp' = |
|
120 BP' "name" "lam'" |
|
121 binder |
|
122 bi'::"bp' \<Rightarrow> atom set" |
|
123 where |
|
124 "bi' (BP' x t) = {atom x}" |
|
125 |
|
126 thm lam'_bp'_fv |
|
127 thm lam'_bp'_inject[no_vars] |
|
128 thm lam'_bp'_bn |
|
129 thm lam'_bp'_perm |
|
130 thm lam'_bp'_induct |
|
131 thm lam'_bp'_inducts |
|
132 thm lam'_bp'_distinct |
|
133 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *} |
|
134 |
|
135 lemma supp_fv: |
|
136 shows "supp t = fv_lam' t" |
|
137 and "supp bp = fv_bp' bp" |
|
138 apply(induct t and bp rule: lam'_bp'_inducts) |
|
139 apply(simp_all add: lam'_bp'_fv) |
|
140 (* VAR case *) |
|
141 apply(simp only: supp_def) |
|
142 apply(simp only: lam'_bp'_perm) |
|
143 apply(simp only: lam'_bp'_inject) |
|
144 apply(simp only: supp_def[symmetric]) |
|
145 apply(simp only: supp_at_base) |
|
146 (* APP case *) |
|
147 apply(simp only: supp_def) |
|
148 apply(simp only: lam'_bp'_perm) |
|
149 apply(simp only: lam'_bp'_inject) |
|
150 apply(simp only: de_Morgan_conj) |
|
151 apply(simp only: Collect_disj_eq) |
|
152 apply(simp only: infinite_Un) |
|
153 apply(simp only: Collect_disj_eq) |
|
154 (* LAM case *) |
|
155 apply(rule_tac t="supp (LAM' name lam'_raw)" and s="supp (Abs {atom name} lam'_raw)" in subst) |
|
156 apply(simp (no_asm) only: supp_def) |
|
157 apply(simp only: lam'_bp'_perm) |
|
158 apply(simp only: permute_ABS) |
|
159 apply(simp only: lam'_bp'_inject) |
|
160 apply(simp only: Abs_eq_iff) |
|
161 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
162 apply(simp only: alpha_gen) |
|
163 apply(simp only: supp_eqvt[symmetric]) |
|
164 apply(simp only: eqvts) |
|
165 apply(simp only: supp_Abs) |
|
166 (* LET case *) |
|
167 apply(rule_tac t="supp (LET' bp'_raw lam'_raw)" and |
|
168 s="supp (Abs (bi' bp'_raw) (bp'_raw, lam'_raw))" in subst) |
|
169 apply(simp (no_asm) only: supp_def) |
|
170 apply(simp only: lam'_bp'_perm) |
|
171 apply(simp only: permute_ABS) |
|
172 apply(simp only: lam'_bp'_inject) |
|
173 apply(simp only: eqvts) |
|
174 apply(simp only: Abs_eq_iff) |
|
175 apply(rule Collect_cong) |
|
176 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
177 apply(simp) |
|
178 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
179 apply(simp) |
|
180 apply(rule Collect_cong) |
|
181 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
182 apply(simp) |
|
183 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
184 apply(simp) |
|
185 apply(rule ext) |
|
186 apply(rule sym) |
|
187 apply(subgoal_tac "fv_bp' = supp") |
|
188 apply(subgoal_tac "fv_lam' = supp") |
|
189 apply(simp) |
|
190 apply(rule trans) |
|
191 apply(rule alpha_abs_Pair[symmetric]) |
|
192 apply(simp add: alpha_gen supp_Pair) |
|
193 oops |
|
194 |
|
195 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]] |
|
196 |
|
197 |
112 text {* example 2 *} |
198 text {* example 2 *} |
113 |
199 |
|
200 ML {* val _ = recursive := false *} |
114 nominal_datatype trm' = |
201 nominal_datatype trm' = |
115 Var "name" |
202 Var "name" |
116 | App "trm'" "trm'" |
203 | App "trm'" "trm'" |
117 | Lam x::"name" t::"trm'" bind x in t |
204 | Lam x::"name" t::"trm'" bind x in t |
118 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
205 | Let p::"pat'" "trm'" t::"trm'" bind "f p" in t |
132 thm trm'_pat'_bn |
219 thm trm'_pat'_bn |
133 thm trm'_pat'_perm |
220 thm trm'_pat'_perm |
134 thm trm'_pat'_induct |
221 thm trm'_pat'_induct |
135 thm trm'_pat'_distinct |
222 thm trm'_pat'_distinct |
136 |
223 |
137 (* compat should be |
224 lemma supp_fv_trm'_pat': |
138 compat (PN) pi (PN) == True |
225 shows "supp t = fv_trm' t" |
139 compat (PS x) pi (PS x') == pi o x = x' |
226 and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp" |
140 compat (PD p1 p2) pi (PD p1' p2') == compat p1 pi p1' & compat p2 pi p2' |
227 apply(induct t and bp rule: trm'_pat'_inducts) |
141 *) |
228 apply(simp_all add: trm'_pat'_fv) |
|
229 (* VAR case *) |
|
230 apply(simp only: supp_def) |
|
231 apply(simp only: trm'_pat'_perm) |
|
232 apply(simp only: trm'_pat'_inject) |
|
233 apply(simp only: supp_def[symmetric]) |
|
234 apply(simp only: supp_at_base) |
|
235 (* APP case *) |
|
236 apply(simp only: supp_def) |
|
237 apply(simp only: trm'_pat'_perm) |
|
238 apply(simp only: trm'_pat'_inject) |
|
239 apply(simp only: de_Morgan_conj) |
|
240 apply(simp only: Collect_disj_eq) |
|
241 apply(simp only: infinite_Un) |
|
242 apply(simp only: Collect_disj_eq) |
|
243 (* LAM case *) |
|
244 apply(rule_tac t="supp (Lam name trm'_raw)" and s="supp (Abs {atom name} trm'_raw)" in subst) |
|
245 apply(simp (no_asm) only: supp_def) |
|
246 apply(simp only: trm'_pat'_perm) |
|
247 apply(simp only: permute_ABS) |
|
248 apply(simp only: trm'_pat'_inject) |
|
249 apply(simp only: Abs_eq_iff) |
|
250 apply(simp only: insert_eqvt atom_eqvt empty_eqvt) |
|
251 apply(simp only: alpha_gen) |
|
252 apply(simp only: supp_eqvt[symmetric]) |
|
253 apply(simp only: eqvts) |
|
254 apply(simp only: supp_Abs) |
|
255 (* LET case *) |
|
256 apply(rule_tac t="supp (Let pat'_raw trm'_raw1 trm'_raw2)" |
|
257 and s="supp (Abs (f pat'_raw) trm'_raw2) \<union> supp trm'_raw1 \<union> fv_f pat'_raw" in subst) |
|
258 apply(simp (no_asm) only: supp_def) |
|
259 apply(simp only: trm'_pat'_perm) |
|
260 apply(simp only: permute_ABS) |
|
261 apply(simp only: trm'_pat'_inject) |
|
262 apply(simp only: eqvts) |
|
263 apply(simp only: Abs_eq_iff) |
|
264 apply(simp only: ex_simps) |
|
265 apply(simp only: de_Morgan_conj) |
|
266 apply(simp only: Collect_disj_eq) |
|
267 apply(simp only: infinite_Un) |
|
268 apply(simp only: Collect_disj_eq) |
|
269 apply(simp only: alpha_gen) |
|
270 apply(simp only: supp_eqvt[symmetric]) |
|
271 apply(simp only: eqvts) |
|
272 apply(blast) |
|
273 apply(simp add: supp_Abs) |
|
274 apply(blast) |
|
275 (* PN case *) |
|
276 apply(simp only: supp_def) |
|
277 apply(simp only: trm'_pat'_perm) |
|
278 apply(simp only: trm'_pat'_inject) |
|
279 apply(simp) |
|
280 (* PS case *) |
|
281 apply(simp only: supp_def) |
|
282 apply(simp only: trm'_pat'_perm) |
|
283 apply(simp only: trm'_pat'_inject) |
|
284 apply(simp only: supp_def[symmetric]) |
|
285 apply(simp only: supp_at_base) |
|
286 apply(simp) |
|
287 (* PD case *) |
|
288 apply(simp only: supp_def) |
|
289 apply(simp only: trm'_pat'_perm) |
|
290 apply(simp only: trm'_pat'_inject) |
|
291 apply(simp only: de_Morgan_conj) |
|
292 apply(simp only: Collect_disj_eq) |
|
293 apply(simp only: infinite_Un) |
|
294 apply(simp only: Collect_disj_eq) |
|
295 apply(simp only: supp_def[symmetric]) |
|
296 apply(simp add: supp_at_base) |
|
297 done |
|
298 |
|
299 thm trm'_pat'_fv[simplified supp_fv_trm'_pat'(1)[symmetric] supp_fv_trm'_pat'(2)[THEN conjunct1, symmetric]] |
142 |
300 |
143 nominal_datatype trm0 = |
301 nominal_datatype trm0 = |
144 Var0 "name" |
302 Var0 "name" |
145 | App0 "trm0" "trm0" |
303 | App0 "trm0" "trm0" |
146 | Lam0 x::"name" t::"trm0" bind x in t |
304 | Lam0 x::"name" t::"trm0" bind x in t |