56 using a |
57 using a |
57 by (nominal_induct t avoiding: x y s u rule: lam.strong_induct) |
58 by (nominal_induct t avoiding: x y s u rule: lam.strong_induct) |
58 (auto simp add: fresh_fact forget) |
59 (auto simp add: fresh_fact forget) |
59 |
60 |
60 inductive |
61 inductive |
|
62 beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _") |
|
63 where |
|
64 beta_beta: "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<rightarrow> t[x ::= s]" |
|
65 | beta_Lam: "t \<rightarrow> s \<Longrightarrow> Lam [x].t \<rightarrow> Lam [x].s" |
|
66 | beta_App1: "t \<rightarrow> s \<Longrightarrow> App t u \<rightarrow> App s u" |
|
67 | beta_App2: "t \<rightarrow> s \<Longrightarrow> App u t \<rightarrow> App u s" |
|
68 |
|
69 equivariance beta |
|
70 |
|
71 nominal_inductive beta |
|
72 avoids beta_beta: "x" |
|
73 | beta_Lam: "x" |
|
74 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
|
75 |
|
76 inductive |
61 equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _") |
77 equ :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx> _") |
62 where |
78 where |
63 equ_beta: "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<approx> t[x ::= s]" |
79 equ_beta: "atom x \<sharp> s \<Longrightarrow> App (Lam [x].t) s \<approx> t[x ::= s]" |
64 | equ_refl: "t \<approx> t" |
80 | equ_refl: "t \<approx> t" |
65 | equ_sym: "t \<approx> s \<Longrightarrow> s \<approx> t" |
81 | equ_sym: "t \<approx> s \<Longrightarrow> s \<approx> t" |
73 nominal_inductive equ |
89 nominal_inductive equ |
74 avoids equ_beta: "x" |
90 avoids equ_beta: "x" |
75 | equ_Lam: "x" |
91 | equ_Lam: "x" |
76 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
92 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
77 |
93 |
|
94 inductive |
|
95 equ2 :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<approx>2 _") |
|
96 where |
|
97 equ2_beta1: "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> App (Lam [x].t1) t2 \<approx>2 s1[x ::= s2]" |
|
98 | equ2_beta2: "\<lbrakk>atom x \<sharp> (t2, s2); s1 \<approx>2 t1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> s1[x ::= s2] \<approx>2 App (Lam [x].t1) t2" |
|
99 | equ2_Var: "Var x \<approx>2 Var x" |
|
100 | equ2_Lam: "t \<approx>2 s \<Longrightarrow> Lam [x].t \<approx>2 Lam [x].s" |
|
101 | equ2_App: "\<lbrakk>t1 \<approx>2 s1; t2 \<approx>2 s2\<rbrakk> \<Longrightarrow> App t1 t2 \<approx>2 App s1 s2" |
|
102 |
|
103 equivariance equ2 |
|
104 |
|
105 nominal_inductive equ2 |
|
106 avoids equ2_beta1: "x" |
|
107 | equ2_beta2: "x" |
|
108 | equ2_Lam: "x" |
|
109 by (simp_all add: fresh_star_def fresh_Pair lam.fresh fresh_fact) |
|
110 |
|
111 lemma equ2_refl: |
|
112 fixes t::"lam" |
|
113 shows "t \<approx>2 t" |
|
114 apply(induct t rule: lam.induct) |
|
115 apply(auto intro: equ2.intros) |
|
116 done |
|
117 |
|
118 lemma equ2_symm: |
|
119 fixes t s::"lam" |
|
120 assumes "t \<approx>2 s" |
|
121 shows "s \<approx>2 t" |
|
122 using assms |
|
123 apply(induct) |
|
124 apply(auto intro: equ2.intros) |
|
125 done |
|
126 |
|
127 lemma equ2_trans: |
|
128 fixes t1 t2 t3::"lam" |
|
129 assumes "t1 \<approx>2 t2" "t2 \<approx>2 t3" |
|
130 shows "t1 \<approx>2 t3" |
|
131 using assms |
|
132 apply(nominal_induct t1 t2 avoiding: t3 rule: equ2.strong_induct) |
|
133 defer |
|
134 defer |
|
135 apply(erule equ2.cases) |
|
136 apply(auto) |
|
137 apply(rule equ2_beta2) |
|
138 apply(simp) |
|
139 apply(simp) |
|
140 apply(simp) |
|
141 apply(rule equ2_refl) |
|
142 defer |
|
143 apply(rotate_tac 4) |
|
144 apply(erule equ2.cases) |
|
145 apply(auto) |
|
146 oops |
|
147 |
|
148 |
|
149 |
|
150 |
|
151 |
78 lemma [quot_respect]: |
152 lemma [quot_respect]: |
79 shows "(op = ===> equ) Var Var" |
153 shows "(op = ===> equ) Var Var" |
80 and "(equ ===> equ ===> equ) App App" |
154 and "(equ ===> equ ===> equ) App App" |
81 and "(op = ===> equ ===> equ) Beta.Lam Beta.Lam" |
155 and "(op = ===> equ ===> equ) Beta.Lam Beta.Lam" |
82 unfolding fun_rel_def |
156 unfolding fun_rel_def |
159 apply(rule equ_refl) |
233 apply(rule equ_refl) |
160 done |
234 done |
161 |
235 |
162 end |
236 end |
163 |
237 |
|
238 lemma qlam_perm[simp]: |
|
239 shows "p \<bullet> (QVar x) = QVar (p \<bullet> x)" |
|
240 and "p \<bullet> (QApp t s) = QApp (p \<bullet> t) (p \<bullet> s)" |
|
241 and "p \<bullet> (QLam [x].t) = QLam [p \<bullet> x].(p \<bullet> t)" |
|
242 apply(descending) |
|
243 apply(simp add: equ_refl) |
|
244 apply(descending) |
|
245 apply(simp add: equ_refl) |
|
246 apply(descending) |
|
247 apply(simp add: equ_refl) |
|
248 done |
|
249 |
|
250 lemma qlam_supports: |
|
251 shows "{atom x} supports (QVar x)" |
|
252 and "supp (t, s) supports (QApp t s)" |
|
253 and "supp (x, t) supports (QLam [x].t)" |
|
254 unfolding supports_def fresh_def[symmetric] |
|
255 by (auto simp add: swap_fresh_fresh) |
|
256 |
|
257 lemma qlam_fs: |
|
258 fixes t::"qlam" |
|
259 shows "finite (supp t)" |
|
260 apply(induct t rule: qlam_induct) |
|
261 apply(rule supports_finite) |
|
262 apply(rule qlam_supports) |
|
263 apply(simp) |
|
264 apply(rule supports_finite) |
|
265 apply(rule qlam_supports) |
|
266 apply(simp add: supp_Pair) |
|
267 apply(rule supports_finite) |
|
268 apply(rule qlam_supports) |
|
269 apply(simp add: supp_Pair finite_supp) |
|
270 done |
|
271 |
|
272 instantiation qlam :: fs |
|
273 begin |
|
274 |
|
275 instance |
|
276 apply(default) |
|
277 apply(rule qlam_fs) |
|
278 done |
|
279 |
|
280 end |
|
281 |
164 quotient_definition subst_qlam ("_[_ ::q= _]") |
282 quotient_definition subst_qlam ("_[_ ::q= _]") |
165 where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst |
283 where "subst_qlam::qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" is subst |
166 |
284 |
167 lemma |
285 lemma |
168 "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))" |
286 "(QVar x)[y ::q= s] = (if x = y then s else (QVar x))" |
169 apply(descending) |
287 apply(descending) |
170 apply(simp) |
288 apply(simp) |
176 apply(descending) |
294 apply(descending) |
177 apply(simp) |
295 apply(simp) |
178 apply(rule equ_refl) |
296 apply(rule equ_refl) |
179 done |
297 done |
180 |
298 |
181 lemma |
299 definition |
182 "(QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])" |
300 "Supp t = \<Inter>{supp s | s. s \<approx> t}" |
183 apply(descending) |
301 |
184 apply(subst subst.simps) |
302 lemma [quot_respect]: |
185 prefer 3 |
303 shows "(equ ===> op=) Supp Supp" |
186 apply(rule equ_refl) |
304 unfolding fun_rel_def |
|
305 unfolding Supp_def |
|
306 apply(rule allI)+ |
|
307 apply(rule impI) |
|
308 apply(rule_tac f="Inter" in arg_cong) |
|
309 apply(auto) |
|
310 apply (metis equ_trans) |
|
311 by (metis equivp_def qlam_equivp) |
|
312 |
|
313 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" |
|
314 is "Supp::lam \<Rightarrow> atom set" |
|
315 |
|
316 lemma Supp_supp: |
|
317 "Supp t \<subseteq> supp t" |
|
318 unfolding Supp_def |
|
319 apply(auto) |
|
320 apply(drule_tac x="supp t" in spec) |
|
321 apply(auto simp add: equ_refl) |
|
322 done |
|
323 |
|
324 lemma Supp_Lam: |
|
325 "atom a \<notin> Supp (Lam [a].t)" |
|
326 proof - |
|
327 have "atom a \<notin> supp (Lam [a].t)" by (simp add: lam.supp) |
|
328 then show ?thesis using Supp_supp |
|
329 by blast |
|
330 qed |
|
331 |
|
332 lemmas s = Supp_Lam[quot_lifted] |
|
333 |
|
334 definition |
|
335 ssupp :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ ssupp _") |
|
336 where |
|
337 "A ssupp x \<equiv> \<forall>p. (\<forall>a \<in> A. (p \<bullet> a) = a) \<longleftrightarrow> (p \<bullet> x) = x" |
|
338 |
|
339 lemma ssupp_supports: |
|
340 "A ssupp x \<Longrightarrow> A supports x" |
|
341 unfolding ssupp_def supports_def |
|
342 apply(rule allI)+ |
|
343 apply(drule_tac x="(a \<rightleftharpoons> b)" in spec) |
|
344 apply(auto) |
|
345 by (metis swap_atom_simps(3)) |
|
346 |
|
347 lemma ssupp_supp: |
|
348 assumes a: "finite A" |
|
349 and b: "A ssupp x" |
|
350 shows "supp x = A" |
|
351 proof - |
|
352 { assume 0: "A - supp x \<noteq> {}" |
|
353 then obtain a where 1: "a \<in> A - supp x" by auto |
|
354 obtain a' where *: "a' \<in> UNIV - A" and **: "sort_of a' = sort_of a" |
|
355 by (rule obtain_atom[OF a]) (auto) |
|
356 have "(a \<rightleftharpoons> a') \<bullet> a = a'" using 1 ** * by (auto) |
|
357 then have w0: "(a \<rightleftharpoons> a') \<bullet> x \<noteq> x" |
|
358 using b unfolding ssupp_def |
|
359 apply - |
|
360 apply(drule_tac x="(a \<rightleftharpoons> a')" in spec) |
|
361 apply(auto) |
|
362 using 1 * |
|
363 apply(auto) |
|
364 done |
|
365 have w1: "a \<sharp> x" unfolding fresh_def using 1 by auto |
|
366 have w2: "a' \<sharp> x" using * |
|
367 apply(rule_tac supports_fresh) |
|
368 apply(rule ssupp_supports) |
|
369 apply(rule b) |
|
370 apply(rule a) |
|
371 apply(auto) |
|
372 done |
|
373 have "False" using w0 w1 w2 by (simp add: swap_fresh_fresh) |
|
374 then have "supp x = A" by simp } |
|
375 moreover |
|
376 { assume "A - supp x = {}" |
|
377 moreover |
|
378 have "supp x \<subseteq> A" |
|
379 apply(rule supp_is_subset) |
|
380 apply(rule ssupp_supports) |
|
381 apply(rule b) |
|
382 apply(rule a) |
|
383 done |
|
384 ultimately have "supp x = A" |
|
385 by blast |
|
386 } |
|
387 ultimately show "supp x = A" by blast |
|
388 qed |
|
389 |
|
390 |
|
391 lemma |
|
392 "(supp x) ssupp x" |
|
393 unfolding ssupp_def |
|
394 apply(auto) |
|
395 apply(rule supp_perm_eq) |
|
396 apply(simp add: fresh_star_def) |
|
397 apply(auto) |
|
398 apply(simp add: fresh_perm) |
|
399 apply(simp add: fresh_perm[symmetric]) |
|
400 (*Tzevelekos 2008, section 2.1.2 property 2.5*) |
|
401 oops |
|
402 |
|
403 |
|
404 function |
|
405 qsubst :: "qlam \<Rightarrow> name \<Rightarrow> qlam \<Rightarrow> qlam" ("_ [_ ::qq= _]" [90, 90, 90] 90) |
|
406 where |
|
407 "(QVar x)[y ::qq= s] = (if x = y then s else (QVar x))" |
|
408 | "(QApp t1 t2)[y ::qq= s] = QApp (t1[y ::qq= s]) (t2[y ::qq= s])" |
|
409 | "\<lbrakk>atom x \<sharp> y; atom x \<sharp> s\<rbrakk> \<Longrightarrow> (QLam [x]. t)[y ::qq= s] = QLam [x].(t[y ::qq= s])" |
|
410 apply(simp_all add:) |
|
411 oops |
|
412 |
|
413 |
|
414 lemma |
|
415 assumes a: "Lam [x].t \<approx> s" |
|
416 shows "\<exists>x' t'. s = Lam [x']. t' \<and> t \<approx> t'" |
|
417 using a |
|
418 apply(induct s rule:lam.induct) |
|
419 apply(erule equ.cases) |
|
420 apply(auto) |
|
421 apply(erule equ.cases) |
|
422 apply(auto) |
|
423 |
|
424 |
|
425 |
|
426 lemma |
|
427 "atom x \<sharp> y \<Longrightarrow> atom x \<notin> supp_qlam s \<Longrightarrow> (QLam [x].t)[y ::q= s] = QLam [x].(t[y ::q= s])" |
|
428 apply(descending) |
187 oops |
429 oops |
188 |
430 |
189 |
431 |
190 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)" |
432 lemma [eqvt]: "(p \<bullet> abs_qlam t) = abs_qlam (p \<bullet> t)" |
191 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
433 apply (subst fun_cong[OF fun_cong[OF meta_eq_to_obj_eq[OF permute_qlam_def]], of p, simplified]) |
219 apply(rule supports_abs_qlam) |
461 apply(rule supports_abs_qlam) |
220 apply(simp add: QVar_def) |
462 apply(simp add: QVar_def) |
221 done |
463 done |
222 |
464 |
223 section {* Supp *} |
465 section {* Supp *} |
224 |
|
225 definition |
|
226 "Supp t = \<Inter>{supp s | s. s \<approx> t}" |
|
227 |
|
228 lemma [quot_respect]: |
|
229 shows "(equ ===> op=) Supp Supp" |
|
230 unfolding fun_rel_def |
|
231 unfolding Supp_def |
|
232 apply(rule allI)+ |
|
233 apply(rule impI) |
|
234 apply(rule_tac f="Inter" in arg_cong) |
|
235 apply(auto) |
|
236 apply (metis equ_trans) |
|
237 by (metis equivp_def qlam_equivp) |
|
238 |
|
239 quotient_definition "supp_qlam::qlam \<Rightarrow> atom set" |
|
240 is "Supp::lam \<Rightarrow> atom set" |
|
241 |
466 |
242 lemma s: |
467 lemma s: |
243 assumes "s \<approx> t" |
468 assumes "s \<approx> t" |
244 shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)" |
469 shows "a \<sharp> (abs_qlam s) \<longleftrightarrow> a \<sharp> (abs_qlam t)" |
245 using assms |
470 using assms |
324 |
548 |
325 lemma |
549 lemma |
326 "size (QLam [x].t) = Suc (size t)" |
550 "size (QLam [x].t) = Suc (size t)" |
327 apply(descending) |
551 apply(descending) |
328 apply(simp add: Size_def) |
552 apply(simp add: Size_def) |
329 apply(rule_tac n="Suc (size t)" and m="size t" in Least_Suc2) |
553 thm Least_Suc |
|
554 apply(rule trans) |
|
555 apply(rule_tac n="Suc (size t)" in Least_Suc) |
330 apply(simp add: Collect_def) |
556 apply(simp add: Collect_def) |
331 apply(rule_tac x="Lam [x].t" in exI) |
557 apply(rule_tac x="Lam [x].t" in exI) |
332 apply(auto intro: equ_refl)[1] |
558 apply(auto intro: equ_refl)[1] |
|
559 apply(simp add: Collect_def) |
|
560 apply(auto) |
|
561 defer |
333 apply(simp add: Collect_def) |
562 apply(simp add: Collect_def) |
334 apply(rule_tac x="t" in exI) |
563 apply(rule_tac x="t" in exI) |
335 apply(auto intro: equ_refl)[1] |
564 apply(auto intro: equ_refl)[1] |
336 apply(simp add: Collect_def) |
565 apply(simp add: Collect_def) |
337 defer |
566 defer |