equal
deleted
inserted
replaced
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 (* x is bound in both e1 and e2 |
7 (* x is bound in both e1 and e2; |
8 names in p are bound only in e1 *) |
8 bp-names in p are bound only in e1 |
|
9 *) |
|
10 |
|
11 declare [[STEPS = 100]] |
9 |
12 |
10 nominal_datatype exp = |
13 nominal_datatype exp = |
11 Var name |
14 Var name |
12 | Pair exp exp |
15 | Pair exp exp |
13 | LetRec x::name p::pat e1::exp e2::exp bind x in e2, bind x "bp p" in e1 |
16 | LetRec x::name p::pat e1::exp e2::exp bind x in e2, bind x "bp p" in e1 |
20 where |
23 where |
21 "bp (PVar x) = [atom x]" |
24 "bp (PVar x) = [atom x]" |
22 | "bp (PUnit) = []" |
25 | "bp (PUnit) = []" |
23 | "bp (PPair p1 p2) = bp p1 @ bp p2" |
26 | "bp (PPair p1 p2) = bp p1 @ bp p2" |
24 |
27 |
|
28 thm exp_pat.distinct |
|
29 thm exp_pat.induct |
|
30 thm exp_pat.inducts |
|
31 thm exp_pat.exhaust |
|
32 thm exp_pat.fv_defs |
|
33 thm exp_pat.bn_defs |
|
34 thm exp_pat.perm_simps |
|
35 thm exp_pat.eq_iff |
|
36 thm exp_pat.fv_bn_eqvt |
|
37 thm exp_pat.size_eqvt |
|
38 thm exp_pat.supports |
|
39 thm exp_pat.fsupp |
|
40 thm exp_pat.supp |
|
41 |
|
42 |
25 end |
43 end |