equal
deleted
inserted
replaced
4 |
4 |
5 (* example 3 from Peter Sewell's bestiary *) |
5 (* example 3 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = cheat_equivp := true *} |
|
10 ML {* val _ = cheat_alpha_bn_rsp := true *} |
|
11 |
|
12 nominal_datatype exp = |
9 nominal_datatype exp = |
13 Var "name" |
10 Var "name" |
14 | App "exp" "exp" |
11 | App "exp" "exp" |
15 | Lam x::"name" e::"exp" bind_set x in e |
12 | Lam x::"name" e::"exp" bind x in e |
16 | Let x::"name" p::"pat" e1::"exp" e2::"exp" bind_set x in e2, bind_set "bp p" in e1 |
13 | Let x::"name" p::"pat" e1::"exp" e2::"exp" bind (set) x in e2, bind (set) "bp p" in e1 |
17 and pat = |
14 and pat = |
18 PVar "name" |
15 PVar "name" |
19 | PUnit |
16 | PUnit |
20 | PPair "pat" "pat" |
17 | PPair "pat" "pat" |
21 binder |
18 binder |
23 where |
20 where |
24 "bp (PVar x) = {atom x}" |
21 "bp (PVar x) = {atom x}" |
25 | "bp (PUnit) = {}" |
22 | "bp (PUnit) = {}" |
26 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
23 | "bp (PPair p1 p2) = bp p1 \<union> bp p2" |
27 |
24 |
28 thm exp_pat.fv |
25 |
|
26 thm exp_pat.distinct |
|
27 thm exp_pat.induct |
|
28 thm exp_pat.exhaust |
|
29 thm exp_pat.fv_defs |
|
30 thm exp_pat.bn_defs |
|
31 thm exp_pat.perm_simps |
29 thm exp_pat.eq_iff |
32 thm exp_pat.eq_iff |
30 thm exp_pat.bn |
33 thm exp_pat.fv_bn_eqvt |
31 thm exp_pat.perm |
34 thm exp_pat.size_eqvt |
32 thm exp_pat.induct |
|
33 thm exp_pat.distinct |
|
34 thm exp_pat.fv |
|
35 thm exp_pat.supp(1-2) |
|
36 |
|
37 |
|
38 |
35 |
39 |
36 |
40 end |
37 end |
41 |
38 |
42 |
39 |