1 theory NoneExamples |
1 theory NoneExamples |
2 imports "../NewParser" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
|
5 text {* |
|
6 This example is not covered by our binding |
|
7 specification. |
|
8 *} |
|
9 |
5 atom_decl name |
10 atom_decl name |
6 |
|
7 |
11 |
8 text {* |
12 text {* |
9 "Weirdo" example from Peter Sewell's bestiary. |
13 "Weirdo" example from Peter Sewell's bestiary. |
10 |
14 |
11 This example is not covered by our binding |
15 p2 occurs in two bodies |
12 specification. |
|
13 |
|
14 *} |
16 *} |
15 |
17 |
|
18 (* |
16 nominal_datatype weird = |
19 nominal_datatype weird = |
17 Foo_var "name" |
20 Foo_var "name" |
18 | Foo_pair "weird" "weird" |
21 | Foo_pair "weird" "weird" |
19 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
22 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
20 bind x in p1 p2, |
23 bind x in p1 p2, |
21 bind y in p2 p3 |
24 bind y in p2 p3 |
|
25 *) |
22 |
26 |
23 (* e1 occurs in two bodies *) |
27 text {* |
|
28 this example binds bound names and therefore the |
|
29 fv-function is not respectful - the proof just fails. |
|
30 *} |
24 |
31 |
25 nominal_datatype exp = |
|
26 Var name |
|
27 | Pair exp exp |
|
28 | LetRec x::name p::pat e1::exp e2::exp bind x in e1 e2, bind "bp p" in e1 |
|
29 and pat = |
|
30 PVar name |
|
31 | PUnit |
|
32 | PPair pat pat |
|
33 binder |
|
34 bp :: "pat \<Rightarrow> atom list" |
|
35 where |
|
36 "bp (PVar x) = [atom x]" |
|
37 | "bp (PUnit) = []" |
|
38 | "bp (PPair p1 p2) = bp p1 @ bp p2" |
|
39 |
|
40 |
|
41 (* this example binds bound names and |
|
42 so is not respectful *) |
|
43 (* |
32 (* |
44 nominal_datatype trm = |
33 nominal_datatype trm = |
45 Vr "name" |
34 Var "name" |
46 | Lm x::"name" t::"trm" bind x in t |
35 | Lam x::"name" t::"trm" bind x in t |
47 | Lt left::"trm" right::"trm" bind "bv left" in right |
36 | Let left::"trm" right::"trm" bind (set) "bv left" in right |
48 binder |
37 binder |
49 bv |
38 bv |
50 where |
39 where |
51 "bv (Vr n) = {}" |
40 "bv (Var n) = {}" |
52 | "bv (Lm n t) = {atom n} \<union> bv t" |
41 | "bv (Lam n t) = {atom n} \<union> bv t" |
53 | "bv (Lt l r) = bv l \<union> bv r" |
42 | "bv (Let l r) = bv l \<union> bv r" |
54 *) |
43 *) |
55 |
44 |
56 (* this example uses "-" in the binding function; |
45 text {* |
57 at the moment this is unsupported *) |
46 this example uses "-" in the binding function; |
|
47 at the moment this is unsupported |
|
48 *} |
|
49 |
58 (* |
50 (* |
59 nominal_datatype trm' = |
51 nominal_datatype trm' = |
60 Vr' "name" |
52 Var "name" |
61 | Lm' l::"name" r::"trm'" bind l in r |
53 | Lam l::"name" r::"trm'" bind l in r |
62 | Lt' l::"trm'" r::"trm'" bind "bv' l" in r |
54 | Let l::"trm'" r::"trm'" bind (set) "bv' l" in r |
63 binder |
55 binder |
64 bv' |
56 bv' |
65 where |
57 where |
66 "bv' (Vr' n) = {atom n}" |
58 "bv' (Var n) = {atom n}" |
67 | "bv' (Lm' n t) = bv' t - {atom n}" |
59 | "bv' (Lam n t) = bv' t - {atom n}" |
68 | "bv' (Lt' l r) = bv' l \<union> bv' r" |
60 | "bv' (Let l r) = bv' l \<union> bv' r" |
69 *) |
61 *) |
70 |
62 |
71 (* this example again binds bound names *) |
63 text {* |
|
64 again this example binds bound names - so not respectful |
|
65 *} |
|
66 |
72 (* |
67 (* |
73 nominal_datatype trm'' = |
68 nominal_datatype trm = |
74 Va'' "name" |
69 Var "name" |
75 | Lm'' n::"name" l::"trm''" bind n in l |
70 | Lam n::"name" l::"trm" bind n in l |
76 and bla'' = |
71 and bla = |
77 Bla'' f::"trm''" s::"trm''" bind "bv'' f" in s |
72 Bla f::"trm" s::"trm" bind (set) "bv f" in s |
78 binder |
73 binder |
79 bv'' |
74 bv :: "trm \<Rightarrow> atom set" |
80 where |
75 where |
81 "bv'' (Vm'' x) = {}" |
76 "bv (Vam x) = {}" |
82 | "bv'' (Lm'' x b) = {atom x}" |
77 | "bv (Lam x b) = {atom x}" |
83 *) |
78 *) |
84 |
79 |
85 end |
80 end |
86 |
81 |
87 |
82 |