equal
deleted
inserted
replaced
5 begin |
5 begin |
6 |
6 |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
9 |
|
10 ML {* trace := true *} |
|
11 |
10 nominal_datatype lam = |
12 nominal_datatype lam = |
11 Var "name" |
13 Var "name" |
12 | App "lam" "lam" |
14 | App "lam" "lam" |
13 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
15 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
14 |
16 |
17 by perm_simp rule |
19 by perm_simp rule |
18 |
20 |
19 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)" |
21 lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)" |
20 proof - |
22 proof - |
21 have "alpha_lam_raw (rep_lam (abs_lam t)) t" |
23 have "alpha_lam_raw (rep_lam (abs_lam t)) t" |
22 using rep_abs_rsp_left Quotient_lam equivp_reflp lam_equivp by metis |
24 using rep_abs_rsp_left Quotient3_lam equivp_reflp lam_equivp by metis |
23 then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)" |
25 then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)" |
24 unfolding alpha_lam_raw_eqvt[symmetric] permute_pure . |
26 unfolding alpha_lam_raw_eqvt[symmetric] permute_pure . |
25 then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)" |
27 then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)" |
26 using Quotient_rel Quotient_lam by metis |
28 using Quotient3_rel Quotient3_lam by metis |
27 thus ?thesis using permute_lam_def id_apply map_fun_apply by metis |
29 thus ?thesis using permute_lam_def id_apply map_fun_apply by metis |
28 qed |
30 qed |
29 |
31 |
30 |
32 |
31 section {* Simple examples from Norrish 2004 *} |
33 section {* Simple examples from Norrish 2004 *} |