equal
deleted
inserted
replaced
1 theory ExPS6 |
1 theory ExPS6 |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 (* example 6 from Peter Sewell's bestiary *) |
5 (* example 6 from Peter Sewell's bestiary *) |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 (* The binding structure is too complicated, so equivalence the |
9 (* Is this binding structure supported - I think not |
10 way we define it is not true *) |
10 because e1 occurs twice as body *) |
11 |
11 |
12 ML {* val _ = recursive := false *} |
12 nominal_datatype exp = |
13 nominal_datatype exp6 = |
13 Var name |
14 EVar name |
14 | Pair exp exp |
15 | EPair exp6 exp6 |
15 | LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1 |
16 | ELetRec x::name p::pat6 e1::exp6 e2::exp6 bind x in e1, bind x in e2, bind "bp6 p" in e1 |
16 and pat = |
17 and pat6 = |
17 PVar name |
18 PVar' name |
18 | PUnit |
19 | PUnit' |
19 | PPair pat pat |
20 | PPair' pat6 pat6 |
|
21 binder |
20 binder |
22 bp6 :: "pat6 \<Rightarrow> atom set" |
21 bp :: "pat \<Rightarrow> atom list" |
23 where |
22 where |
24 "bp6 (PVar' x) = {atom x}" |
23 "bp (PVar x) = [atom x]" |
25 | "bp6 (PUnit') = {}" |
24 | "bp (PUnit) = []" |
26 | "bp6 (PPair' p1 p2) = bp6 p1 \<union> bp6 p2" |
25 | "bp (PPair p1 p2) = bp p1 @ bp p2" |
27 |
26 |
28 thm exp6_pat6.fv |
27 thm exp_pat.fv |
29 thm exp6_pat6.eq_iff |
28 thm exp_pat.eq_iff |
30 thm exp6_pat6.bn |
29 thm exp_pat.bn |
31 thm exp6_pat6.perm |
30 thm exp_pat.perm |
32 thm exp6_pat6.induct |
31 thm exp_pat.induct |
33 thm exp6_pat6.distinct |
32 thm exp_pat.distinct |
34 thm exp6_pat6.supp |
33 thm exp_pat.supp |
|
34 |
|
35 declare permute_exp_raw_permute_pat_raw.simps[eqvt] |
|
36 declare alpha_gen_eqvt[eqvt] |
|
37 |
|
38 equivariance alpha_exp_raw |
|
39 |
35 |
40 |
36 end |
41 end |
37 |
42 |
38 |
43 |
39 |
44 |