equal
deleted
inserted
replaced
9 ML {* val _ = cheat_alpha_eqvt := true *} |
9 ML {* val _ = cheat_alpha_eqvt := true *} |
10 ML {* val _ = cheat_equivp := true *} |
10 ML {* val _ = cheat_equivp := true *} |
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
11 ML {* val _ = cheat_alpha_bn_rsp := true *} |
12 |
12 |
13 nominal_datatype exp = |
13 nominal_datatype exp = |
14 VarP "name" |
14 Var "name" |
15 | AppP "exp" "exp" |
15 | App "exp" "exp" |
16 | LamP x::"name" e::"exp" bind_set x in e |
16 | Lam x::"name" e::"exp" bind_set x in e |
17 | LetP x::"name" p::"pat3" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 |
17 | Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 |
18 and pat3 = |
18 and pat = |
19 PVar "name" |
19 PVar "name" |
20 | PUnit |
20 | PUnit |
21 | PPair "pat3" "pat3" |
21 | PPair "pat" "pat" |
22 binder |
22 binder |
23 bp :: "pat3 \<Rightarrow> atom set" |
23 bp :: "pat \<Rightarrow> atom set" |
24 where |
24 where |
25 "bp (PVar x) = {atom x}" |
25 "bp (PVar x) = {atom x}" |
26 | "bp (PUnit) = {}" |
26 | "bp (PUnit) = {}" |
27 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
27 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
28 |
28 |
29 thm exp_pat3.fv |
29 thm exp_pat.fv |
30 thm exp_pat3.eq_iff |
30 thm exp_pat.eq_iff |
31 thm exp_pat3.bn |
31 thm exp_pat.bn |
32 thm exp_pat3.perm |
32 thm exp_pat.perm |
33 thm exp_pat3.induct |
33 thm exp_pat.induct |
34 thm exp_pat3.distinct |
34 thm exp_pat.distinct |
35 thm exp_pat3.fv |
35 thm exp_pat.fv |
36 thm exp_pat3.supp(1-2) |
36 thm exp_pat.supp(1-2) |
|
37 |
|
38 declare permute_exp_raw_permute_pat_raw.simps[eqvt] |
|
39 declare alpha_gen_eqvt[eqvt] |
|
40 |
|
41 equivariance alpha_exp_raw |
|
42 |
37 |
43 |
38 end |
44 end |
39 |
45 |
40 |
46 |
41 |
47 |