equal
deleted
inserted
replaced
1 theory NoneExamples |
1 theory NoneExamples |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 text {* |
5 text {* |
6 This example is not covered by our binding |
6 These examples are not covered by our binding |
7 specification. |
7 specification. |
8 *} |
8 *} |
9 |
9 |
10 atom_decl name |
10 atom_decl name |
11 |
11 |
23 bind x in p1 p2, |
23 bind x in p1 p2, |
24 bind y in p2 p3 |
24 bind y in p2 p3 |
25 *) |
25 *) |
26 |
26 |
27 text {* |
27 text {* |
28 this example binds bound names and therefore the |
28 This example binds bound names and therefore the |
29 fv-function is not respectful - the proof just fails. |
29 fv-function is not respectful - the proof just fails. |
30 *} |
30 *} |
31 |
31 |
32 (* |
32 (* |
33 nominal_datatype trm = |
33 nominal_datatype trm = |
41 | "bv (Lam n t) = {atom n} \<union> bv t" |
41 | "bv (Lam n t) = {atom n} \<union> bv t" |
42 | "bv (Let l r) = bv l \<union> bv r" |
42 | "bv (Let l r) = bv l \<union> bv r" |
43 *) |
43 *) |
44 |
44 |
45 text {* |
45 text {* |
46 this example uses "-" in the binding function; |
46 This example uses "-" in the binding function; |
47 at the moment this is unsupported |
47 at the moment this is unsupported |
48 *} |
48 *} |
49 |
49 |
50 (* |
50 (* |
51 nominal_datatype trm' = |
51 nominal_datatype trm' = |
59 | "bv' (Lam n t) = bv' t - {atom n}" |
59 | "bv' (Lam n t) = bv' t - {atom n}" |
60 | "bv' (Let l r) = bv' l \<union> bv' r" |
60 | "bv' (Let l r) = bv' l \<union> bv' r" |
61 *) |
61 *) |
62 |
62 |
63 text {* |
63 text {* |
64 again this example binds bound names - so not respectful |
64 Again this example binds bound names - so is not respectful |
65 *} |
65 *} |
66 |
66 |
67 (* |
67 (* |
68 nominal_datatype trm = |
68 nominal_datatype trm = |
69 Var "name" |
69 Var "name" |
71 and bla = |
71 and bla = |
72 Bla f::"trm" s::"trm" bind (set) "bv f" in s |
72 Bla f::"trm" s::"trm" bind (set) "bv f" in s |
73 binder |
73 binder |
74 bv :: "trm \<Rightarrow> atom set" |
74 bv :: "trm \<Rightarrow> atom set" |
75 where |
75 where |
76 "bv (Vam x) = {}" |
76 "bv (Var x) = {}" |
77 | "bv (Lam x b) = {atom x}" |
77 | "bv (Lam x b) = {atom x}" |
78 *) |
78 *) |
|
79 |
|
80 text {* |
|
81 This example has mal-formed deep recursive binders. |
|
82 |
|
83 - Bla1: recursive deep binder used twice |
|
84 - Bla2: deep binder used recursively and non-recursively |
|
85 - Bla3: x used in recursive deep binder and somewhere else |
|
86 *} |
|
87 |
|
88 (* |
|
89 nominal_datatype trm = |
|
90 Var "name" |
|
91 and bla = |
|
92 App "trm" "trm" |
|
93 | Bla1 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1 f, bind "bv f" in s2 f |
|
94 | Bla2 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1, bind "bv f" in s2 f |
|
95 | Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" bind "bv f" x in s1 f, bind y x in s2 |
|
96 binder |
|
97 bv :: "trm \<Rightarrow> atom list" |
|
98 where |
|
99 "bv (Var a) = [atom a]" |
|
100 *) |
|
101 |
79 |
102 |
80 end |
103 end |
81 |
104 |
82 |
105 |
83 |
106 |