1 theory Lambda |
1 theory Lambda |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
|
5 |
|
6 lemma Abs_lst1_fcb2: |
|
7 fixes a b :: "'a :: at" |
|
8 and S T :: "'b :: fs" |
|
9 and c::"'c::fs" |
|
10 assumes e: "(Abs_lst [atom a] T) = (Abs_lst [atom b] S)" |
|
11 and fcb1: "atom a \<sharp> f a T c" |
|
12 and fcb2: "atom b \<sharp> f b S c" |
|
13 and fresh: "{atom a, atom b} \<sharp>* c" |
|
14 and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a T c) = f (p \<bullet> a) (p \<bullet> T) c" |
|
15 and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b S c) = f (p \<bullet> b) (p \<bullet> S) c" |
|
16 shows "f a T c = f b S c" |
|
17 proof - |
|
18 have fin1: "finite (supp (f a T c))" |
|
19 apply(rule_tac S="supp (a, T, c)" in supports_finite) |
|
20 apply(simp add: supports_def) |
|
21 apply(simp add: fresh_def[symmetric]) |
|
22 apply(clarify) |
|
23 apply(subst perm1) |
|
24 apply(simp add: supp_swap fresh_star_def) |
|
25 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
26 apply(simp add: finite_supp) |
|
27 done |
|
28 have fin2: "finite (supp (f b S c))" |
|
29 apply(rule_tac S="supp (b, S, c)" in supports_finite) |
|
30 apply(simp add: supports_def) |
|
31 apply(simp add: fresh_def[symmetric]) |
|
32 apply(clarify) |
|
33 apply(subst perm2) |
|
34 apply(simp add: supp_swap fresh_star_def) |
|
35 apply(simp add: swap_fresh_fresh fresh_Pair) |
|
36 apply(simp add: finite_supp) |
|
37 done |
|
38 obtain d::"'a::at" where fr: "atom d \<sharp> (a, b, S, T, c, f a T c, f b S c)" |
|
39 using obtain_fresh'[where x="(a, b, S, T, c, f a T c, f b S c)"] |
|
40 apply(auto simp add: finite_supp supp_Pair fin1 fin2) |
|
41 done |
|
42 have "(a \<leftrightarrow> d) \<bullet> (Abs_lst [atom a] T) = (b \<leftrightarrow> d) \<bullet> (Abs_lst [atom b] S)" |
|
43 apply(simp (no_asm_use) only: flip_def) |
|
44 apply(subst swap_fresh_fresh) |
|
45 apply(simp add: Abs_fresh_iff) |
|
46 using fr |
|
47 apply(simp add: Abs_fresh_iff) |
|
48 apply(subst swap_fresh_fresh) |
|
49 apply(simp add: Abs_fresh_iff) |
|
50 using fr |
|
51 apply(simp add: Abs_fresh_iff) |
|
52 apply(rule e) |
|
53 done |
|
54 then have "Abs_lst [atom d] ((a \<leftrightarrow> d) \<bullet> T) = Abs_lst [atom d] ((b \<leftrightarrow> d) \<bullet> S)" |
|
55 apply (simp add: swap_atom flip_def) |
|
56 done |
|
57 then have eq: "(a \<leftrightarrow> d) \<bullet> T = (b \<leftrightarrow> d) \<bullet> S" |
|
58 by (simp add: Abs1_eq_iff) |
|
59 have "f a T c = (a \<leftrightarrow> d) \<bullet> f a T c" |
|
60 unfolding flip_def |
|
61 apply(rule sym) |
|
62 apply(rule swap_fresh_fresh) |
|
63 using fcb1 |
|
64 apply(simp) |
|
65 using fr |
|
66 apply(simp add: fresh_Pair) |
|
67 done |
|
68 also have "... = f d ((a \<leftrightarrow> d) \<bullet> T) c" |
|
69 unfolding flip_def |
|
70 apply(subst perm1) |
|
71 using fresh fr |
|
72 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
73 apply(simp) |
|
74 done |
|
75 also have "... = f d ((b \<leftrightarrow> d) \<bullet> S) c" using eq by simp |
|
76 also have "... = (b \<leftrightarrow> d) \<bullet> f b S c" |
|
77 unfolding flip_def |
|
78 apply(subst perm2) |
|
79 using fresh fr |
|
80 apply(simp add: supp_swap fresh_star_def fresh_Pair) |
|
81 apply(simp) |
|
82 done |
|
83 also have "... = f b S c" |
|
84 apply(rule flip_fresh_fresh) |
|
85 using fcb2 |
|
86 apply(simp) |
|
87 using fr |
|
88 apply(simp add: fresh_Pair) |
|
89 done |
|
90 finally show ?thesis by simp |
|
91 qed |
5 |
92 |
6 |
93 |
7 atom_decl name |
94 atom_decl name |
8 |
95 |
9 nominal_datatype lam = |
96 nominal_datatype lam = |
42 unfolding frees_lst_graph_def |
129 unfolding frees_lst_graph_def |
43 apply (rule, perm_simp, rule) |
130 apply (rule, perm_simp, rule) |
44 apply(rule TrueI) |
131 apply(rule TrueI) |
45 apply(rule_tac y="x" in lam.exhaust) |
132 apply(rule_tac y="x" in lam.exhaust) |
46 apply(auto) |
133 apply(auto) |
47 apply (erule Abs_lst1_fcb) |
134 apply (erule_tac c="()" in Abs_lst1_fcb2) |
48 apply(simp add: supp_removeAll fresh_def) |
135 apply(simp add: supp_removeAll fresh_def) |
49 apply(drule supp_eqvt_at) |
136 apply(simp add: supp_removeAll fresh_def) |
50 apply(simp add: finite_supp) |
137 apply(simp add: fresh_star_def fresh_Unit) |
51 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
138 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
|
139 apply(simp add: eqvt_at_def removeAll_eqvt atom_eqvt) |
52 done |
140 done |
53 |
141 |
54 termination |
142 termination |
55 by lexicographic_order |
143 by lexicographic_order |
56 |
144 |
71 apply(erule frees_set_graph.induct) |
159 apply(erule frees_set_graph.induct) |
72 apply(auto)[9] |
160 apply(auto)[9] |
73 apply(rule_tac y="x" in lam.exhaust) |
161 apply(rule_tac y="x" in lam.exhaust) |
74 apply(auto)[3] |
162 apply(auto)[3] |
75 apply(simp) |
163 apply(simp) |
76 apply(erule Abs_lst1_fcb) |
164 apply(erule_tac c="()" in Abs_lst1_fcb2) |
77 apply(simp_all add: fresh_minus_atom_set) |
165 apply(simp add: fresh_minus_atom_set) |
78 apply(erule fresh_eqvt_at) |
166 apply(simp add: fresh_minus_atom_set) |
79 apply(simp_all add: finite_supp eqvt_at_def eqvts) |
167 apply(simp add: fresh_star_def fresh_Unit) |
|
168 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
|
169 apply(simp add: Diff_eqvt eqvt_at_def, perm_simp, rule refl) |
80 done |
170 done |
81 |
171 |
82 termination |
172 termination |
83 by lexicographic_order |
173 by lexicographic_order |
84 |
174 |
153 height :: "lam \<Rightarrow> int" |
243 height :: "lam \<Rightarrow> int" |
154 where |
244 where |
155 "height (Var x) = 1" |
245 "height (Var x) = 1" |
156 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
246 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
157 | "height (Lam [x].t) = height t + 1" |
247 | "height (Lam [x].t) = height t + 1" |
158 unfolding eqvt_def height_graph_def |
248 apply(simp add: eqvt_def height_graph_def) |
159 apply (rule, perm_simp, rule) |
249 apply (rule, perm_simp, rule) |
160 apply(rule TrueI) |
250 apply(rule TrueI) |
161 apply(rule_tac y="x" in lam.exhaust) |
251 apply(rule_tac y="x" in lam.exhaust) |
162 apply(auto simp add: lam.distinct lam.eq_iff) |
252 apply(auto) |
163 apply (erule Abs_lst1_fcb) |
253 apply (erule_tac c="()" in Abs_lst1_fcb2) |
164 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
254 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
165 done |
255 done |
166 |
256 |
167 termination |
257 termination |
168 by lexicographic_order |
258 by lexicographic_order |
169 |
259 |
170 thm height.simps |
260 thm height.simps |
178 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
268 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
179 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
269 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
180 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
270 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
181 unfolding eqvt_def subst_graph_def |
271 unfolding eqvt_def subst_graph_def |
182 apply (rule, perm_simp, rule) |
272 apply (rule, perm_simp, rule) |
183 apply(rule TrueI) |
273 apply(rule TrueI) |
184 apply(auto simp add: lam.distinct lam.eq_iff) |
274 apply(auto simp add: lam.distinct lam.eq_iff) |
185 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
275 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
186 apply(blast)+ |
276 apply(blast)+ |
187 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
277 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
188 apply (erule Abs_lst1_fcb) |
278 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
189 apply(simp_all add: Abs_fresh_iff) |
279 apply(simp_all add: Abs_fresh_iff) |
190 apply(drule_tac a="atom (xa)" in fresh_eqvt_at) |
280 apply(simp add: fresh_star_def fresh_Pair) |
191 apply(simp_all add: finite_supp fresh_Pair) |
281 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
192 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
282 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
193 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
|
194 apply(simp add: eqvt_at_def) |
|
195 apply(simp_all add: swap_fresh_fresh) |
|
196 done |
283 done |
197 |
284 |
198 termination |
285 termination |
199 by lexicographic_order |
286 by lexicographic_order |
200 |
287 |
363 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
450 | "trans (App t1 t2) xs = LNApp (trans t1 xs) (trans t2 xs)" |
364 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
451 | "atom x \<sharp> xs \<Longrightarrow> trans (Lam [x]. t) xs = LNLam (trans t (x # xs))" |
365 apply (simp add: eqvt_def trans_graph_def) |
452 apply (simp add: eqvt_def trans_graph_def) |
366 apply (rule, perm_simp, rule) |
453 apply (rule, perm_simp, rule) |
367 apply (erule trans_graph.induct) |
454 apply (erule trans_graph.induct) |
368 apply (auto simp add: ln.fresh) |
455 apply (auto simp add: ln.fresh)[3] |
369 apply (simp add: supp_lookup_fresh) |
456 apply (simp add: supp_lookup_fresh) |
370 apply (simp add: fresh_star_def ln.fresh) |
457 apply (simp add: fresh_star_def ln.fresh) |
371 apply (simp add: ln.fresh fresh_star_def) |
458 apply (simp add: ln.fresh fresh_star_def) |
|
459 apply(auto)[1] |
372 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
460 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
373 apply (auto simp add: fresh_star_def)[3] |
461 apply (auto simp add: fresh_star_def)[3] |
374 apply (erule Abs_lst1_fcb) |
462 apply(simp_all) |
375 apply (simp_all add: fresh_star_def) |
463 apply(erule conjE)+ |
376 apply (drule supp_eqvt_at) |
464 apply (erule Abs_lst1_fcb2) |
377 apply (rule finite_supp) |
465 apply (simp add: fresh_star_def) |
378 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
466 apply (simp add: fresh_star_def) |
379 apply (simp add: eqvt_at_def swap_fresh_fresh) |
467 apply (simp add: fresh_star_def) |
|
468 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
469 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
380 done |
470 done |
381 |
471 |
382 termination |
472 termination |
383 by lexicographic_order |
473 by lexicographic_order |
384 |
474 |
393 apply(simp add: eqvt_def cbvs_graph_def) |
483 apply(simp add: eqvt_def cbvs_graph_def) |
394 apply(rule, perm_simp, rule) |
484 apply(rule, perm_simp, rule) |
395 apply(simp_all) |
485 apply(simp_all) |
396 apply(case_tac x) |
486 apply(case_tac x) |
397 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
487 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
398 apply(auto simp add: fresh_star_def) |
488 apply(auto simp add: fresh_star_def)[3] |
399 apply(erule Abs_lst1_fcb) |
489 apply(erule conjE) |
400 apply(simp_all add: pure_fresh) |
490 apply(erule Abs_lst1_fcb2) |
401 apply (simp add: eqvt_at_def swap_fresh_fresh) |
491 apply(simp add: pure_fresh fresh_star_def) |
|
492 apply(simp add: pure_fresh fresh_star_def) |
|
493 apply(simp add: pure_fresh fresh_star_def) |
|
494 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
495 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
402 done |
496 done |
403 |
497 |
404 termination |
498 termination |
405 by lexicographic_order |
499 by lexicographic_order |
406 |
500 |
458 unfolding eqvt_def transdb_graph_def |
552 unfolding eqvt_def transdb_graph_def |
459 apply (rule, perm_simp, rule) |
553 apply (rule, perm_simp, rule) |
460 apply(rule TrueI) |
554 apply(rule TrueI) |
461 apply (case_tac x) |
555 apply (case_tac x) |
462 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
556 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
463 apply (auto simp add: fresh_star_def fresh_at_list) |
557 apply (auto simp add: fresh_star_def fresh_at_list)[3] |
464 apply (rule_tac f="dblam_in" in arg_cong) |
558 apply(simp_all) |
465 apply (erule Abs_lst1_fcb) |
559 apply(erule conjE) |
466 apply (simp_all add: pure_fresh) |
560 apply (erule_tac c="xsa" in Abs_lst1_fcb2) |
467 apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> xsa = xsa") |
561 apply (simp add: pure_fresh) |
468 apply (simp add: eqvt_at_def) |
562 apply (simp add: pure_fresh) |
469 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
563 apply(simp add: fresh_star_def fresh_at_list) |
|
564 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
|
565 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq db_in_eqvt) |
470 done |
566 done |
471 |
567 |
472 termination |
568 termination |
473 by lexicographic_order |
569 by lexicographic_order |
474 |
570 |
547 | "eval (Lam [x].t) = Lam [x].(eval t)" |
643 | "eval (Lam [x].t) = Lam [x].(eval t)" |
548 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)" |
644 | "eval (App t1 t2) = apply_subst (eval t1) (eval t2)" |
549 | "apply_subst (Var x) t2 = App (Var x) t2" |
645 | "apply_subst (Var x) t2 = App (Var x) t2" |
550 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2" |
646 | "apply_subst (App t0 t1) t2 = App (App t0 t1) t2" |
551 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])" |
647 | "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])" |
552 apply(simp add: eval_apply_subst_graph_def eqvt_def) |
648 apply(simp add: eval_apply_subst_graph_def eqvt_def) |
553 apply(rule, perm_simp, rule) |
649 apply(rule, perm_simp, rule) |
554 apply(rule TrueI) |
650 apply(rule TrueI) |
555 apply (case_tac x) |
651 apply (case_tac x) |
556 apply (case_tac a rule: lam.exhaust) |
652 apply (case_tac a rule: lam.exhaust) |
557 apply simp_all[3] |
653 apply simp_all[3] |
558 apply blast |
654 apply blast |
559 apply (case_tac b) |
655 apply (case_tac b) |
560 apply (rule_tac y="a" and c="ba" in lam.strong_exhaust) |
656 apply (rule_tac y="a" and c="ba" in lam.strong_exhaust) |
561 apply simp_all[3] |
657 apply simp_all[3] |
562 apply blast |
658 apply blast |
563 apply blast |
659 apply blast |
564 apply (simp add: Abs1_eq_iff fresh_star_def) |
660 apply (simp add: Abs1_eq_iff fresh_star_def) |
565 apply(simp_all) |
661 apply(simp_all) |
566 apply(erule Abs_lst1_fcb) |
662 apply(erule_tac c="()" in Abs_lst1_fcb2) |
567 apply (simp add: Abs_fresh_iff) |
663 apply (simp add: Abs_fresh_iff) |
568 apply (simp add: Abs_fresh_iff) |
664 apply (simp add: Abs_fresh_iff) |
569 apply (erule fresh_eqvt_at) |
665 apply(simp add: fresh_star_def fresh_Unit) |
570 apply (simp add: finite_supp) |
666 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
571 apply (simp add: fresh_Inl) |
667 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
572 apply (simp add: eqvt_at_def) |
668 apply(erule conjE) |
573 apply simp |
669 apply(erule_tac c="t2a" in Abs_lst1_fcb2) |
574 apply clarify |
670 apply (erule fresh_eqvt_at) |
575 apply(erule Abs_lst1_fcb) |
671 apply (simp add: finite_supp) |
576 apply (erule fresh_eqvt_at) |
672 apply (simp add: fresh_Inl var_fresh_subst) |
577 apply (simp add: finite_supp) |
673 apply (erule fresh_eqvt_at) |
578 apply (simp add: fresh_Inl var_fresh_subst) |
674 apply (simp add: finite_supp) |
579 apply (erule fresh_eqvt_at) |
675 apply (simp add: fresh_Inl var_fresh_subst) |
580 apply (simp add: finite_supp) |
676 apply(simp add: fresh_star_def fresh_Unit) |
581 apply (simp add: fresh_Inl) |
677 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
582 apply (simp add: fresh_def) |
678 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq subst_eqvt) |
583 using supp_subst apply blast |
|
584 apply (simp add: eqvt_at_def subst_eqvt) |
|
585 apply (subst (2) swap_fresh_fresh) |
|
586 apply assumption+ |
|
587 apply rule |
|
588 apply simp |
|
589 done |
679 done |
590 |
680 |
591 |
681 |
592 (* a small test |
682 (* a small test |
593 termination sorry |
683 termination sorry |