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