equal
deleted
inserted
replaced
|
1 |
1 theory ExPS7 |
2 theory ExPS7 |
2 imports "../NewParser" |
3 imports "../NewParser" |
3 begin |
4 begin |
4 |
5 |
5 (* example 7 from Peter Sewell's bestiary *) |
6 (* example 7 from Peter Sewell's bestiary *) |
6 |
7 |
7 atom_decl name |
8 atom_decl name |
8 |
9 |
9 nominal_datatype exp7 = |
10 nominal_datatype exp = |
10 EVar name |
11 Var name |
11 | EUnit |
12 | Unit |
12 | EPair exp7 exp7 |
13 | Pair exp exp |
13 | ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e |
14 | LetRec l::"lrbs" e::"exp" bind_set "bs l" in l e |
14 and lrb = |
15 and lrb = |
15 Assign name exp7 |
16 Assign name exp |
16 and lrbs = |
17 and lrbs = |
17 Single lrb |
18 Single lrb |
18 | More lrb lrbs |
19 | More lrb lrbs |
19 binder |
20 binder |
20 b7 :: "lrb \<Rightarrow> atom set" and |
21 b :: "lrb \<Rightarrow> atom set" and |
21 b7s :: "lrbs \<Rightarrow> atom set" |
22 bs :: "lrbs \<Rightarrow> atom set" |
22 where |
23 where |
23 "b7 (Assign x e) = {atom x}" |
24 "b (Assign x e) = {atom x}" |
24 | "b7s (Single a) = b7 a" |
25 | "bs (Single a) = b a" |
25 | "b7s (More a as) = (b7 a) \<union> (b7s as)" |
26 | "bs (More a as) = (b a) \<union> (bs as)" |
26 thm exp7_lrb_lrbs.eq_iff |
27 |
27 thm exp7_lrb_lrbs.supp |
28 thm exp_lrb_lrbs.eq_iff |
|
29 thm exp_lrb_lrbs.supp |
|
30 |
|
31 declare permute_exp_raw_permute_lrb_raw_permute_lrbs_raw.simps[eqvt] |
|
32 declare alpha_gen_eqvt[eqvt] |
|
33 |
|
34 equivariance alpha_exp_raw |
28 |
35 |
29 end |
36 end |
30 |
37 |
31 |
38 |
32 |
39 |