1 theory ExNotRsp |
1 theory ExNotRsp |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 (* example 6 from Terms.thy *) |
7 (* this example binds bound names and |
8 |
8 so is not respectful *) |
9 nominal_datatype trm6 = |
9 (* |
10 Vr6 "name" |
10 nominal_datatype trm = |
11 | Lm6 x::"name" t::"trm6" bind x in t |
11 Vr "name" |
12 | Lt6 left::"trm6" right::"trm6" bind "bv6 left" in right |
12 | Lm x::"name" t::"trm" bind x in t |
|
13 | Lt left::"trm" right::"trm" bind "bv left" in right |
13 binder |
14 binder |
14 bv6 |
15 bv |
15 where |
16 where |
16 "bv6 (Vr6 n) = {}" |
17 "bv (Vr n) = {}" |
17 | "bv6 (Lm6 n t) = {atom n} \<union> bv6 t" |
18 | "bv (Lm n t) = {atom n} \<union> bv t" |
18 | "bv6 (Lt6 l r) = bv6 l \<union> bv6 r" |
19 | "bv (Lt l r) = bv l \<union> bv r" |
19 |
|
20 (* example 7 from Terms.thy *) |
|
21 nominal_datatype trm7 = |
|
22 Vr7 "name" |
|
23 | Lm7 l::"name" r::"trm7" bind l in r |
|
24 | Lt7 l::"trm7" r::"trm7" bind "bv7 l" in r |
|
25 binder |
|
26 bv7 |
|
27 where |
|
28 "bv7 (Vr7 n) = {atom n}" |
|
29 | "bv7 (Lm7 n t) = bv7 t - {atom n}" |
|
30 | "bv7 (Lt7 l r) = bv7 l \<union> bv7 r" |
|
31 *) |
20 *) |
32 |
21 |
33 (* example 9 from Terms.thy *) |
22 (* this example uses "-" in the binding function; |
34 nominal_datatype lam9 = |
23 at the moment this is unsupported *) |
35 Var9 "name" |
24 (* |
36 | Lam9 n::"name" l::"lam9" bind n in l |
25 nominal_datatype trm' = |
37 and bla9 = |
26 Vr' "name" |
38 Bla9 f::"lam9" s::"lam9" bind "bv9 f" in s |
27 | Lm' l::"name" r::"trm'" bind l in r |
|
28 | Lt' l::"trm'" r::"trm'" bind "bv' l" in r |
39 binder |
29 binder |
40 bv9 |
30 bv' |
41 where |
31 where |
42 "bv9 (Var9 x) = {}" |
32 "bv' (Vr' n) = {atom n}" |
43 | "bv9 (Lam9 x b) = {atom x}" |
33 | "bv' (Lm' n t) = bv' t - {atom n}" |
|
34 | "bv' (Lt' l r) = bv' l \<union> bv' r" |
|
35 *) |
|
36 |
|
37 (* this example again binds bound names *) |
|
38 (* |
|
39 nominal_datatype trm'' = |
|
40 Va'' "name" |
|
41 | Lm'' n::"name" l::"trm''" bind n in l |
|
42 and bla'' = |
|
43 Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s |
|
44 binder |
|
45 bv'' |
|
46 where |
|
47 "bv'' (Vm'' x) = {}" |
|
48 | "bv'' (Lm'' x b) = {atom x}" |
|
49 *) |
44 |
50 |
45 end |
51 end |
46 |
52 |
47 |
53 |
48 |
54 |