equal
deleted
inserted
replaced
18 (* |
18 (* |
19 nominal_datatype weird = |
19 nominal_datatype weird = |
20 Foo_var "name" |
20 Foo_var "name" |
21 | Foo_pair "weird" "weird" |
21 | Foo_pair "weird" "weird" |
22 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
22 | Foo x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
23 bind x in p1 p2, |
23 binds x in p1 p2, |
24 bind y in p2 p3 |
24 binds 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 = |
34 Var "name" |
34 Var "name" |
35 | Lam x::"name" t::"trm" bind x in t |
35 | Lam x::"name" t::"trm" binds x in t |
36 | Let left::"trm" right::"trm" bind (set) "bv left" in right |
36 | Let left::"trm" right::"trm" binds (set) "bv left" in right |
37 binder |
37 binder |
38 bv |
38 bv |
39 where |
39 where |
40 "bv (Var n) = {}" |
40 "bv (Var n) = {}" |
41 | "bv (Lam n t) = {atom n} \<union> bv t" |
41 | "bv (Lam n t) = {atom n} \<union> bv t" |
48 *} |
48 *} |
49 |
49 |
50 (* |
50 (* |
51 nominal_datatype trm' = |
51 nominal_datatype trm' = |
52 Var "name" |
52 Var "name" |
53 | Lam l::"name" r::"trm'" bind l in r |
53 | Lam l::"name" r::"trm'" binds l in r |
54 | Let l::"trm'" r::"trm'" bind (set) "bv' l" in r |
54 | Let l::"trm'" r::"trm'" binds (set) "bv' l" in r |
55 binder |
55 binder |
56 bv' |
56 bv' |
57 where |
57 where |
58 "bv' (Var n) = {atom n}" |
58 "bv' (Var n) = {atom n}" |
59 | "bv' (Lam n t) = bv' t - {atom n}" |
59 | "bv' (Lam n t) = bv' t - {atom n}" |
65 *} |
65 *} |
66 |
66 |
67 (* |
67 (* |
68 nominal_datatype trm = |
68 nominal_datatype trm = |
69 Var "name" |
69 Var "name" |
70 | Lam n::"name" l::"trm" bind n in l |
70 | Lam n::"name" l::"trm" binds n in l |
71 and bla = |
71 and bla = |
72 Bla f::"trm" s::"trm" bind (set) "bv f" in s |
72 Bla f::"trm" s::"trm" binds (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 (Var x) = {}" |
76 "bv (Var x) = {}" |
77 | "bv (Lam x b) = {atom x}" |
77 | "bv (Lam x b) = {atom x}" |
88 (* |
88 (* |
89 nominal_datatype trm = |
89 nominal_datatype trm = |
90 Var "name" |
90 Var "name" |
91 and bla = |
91 and bla = |
92 App "trm" "trm" |
92 App "trm" "trm" |
93 | Bla1 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1 f, bind "bv f" in s2 f |
93 | Bla1 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1 f, binds "bv f" in s2 f |
94 | Bla2 f::"trm" s1::"trm" s2::"trm" bind "bv f" in s1, bind "bv f" in s2 f |
94 | Bla2 f::"trm" s1::"trm" s2::"trm" binds "bv f" in s1, binds "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 |
95 | Bla3 f::"trm" s1::"trm" s2::"trm" x::"name" y::"name" binds "bv f" x in s1 f, binds y x in s2 |
96 binder |
96 binder |
97 bv :: "trm \<Rightarrow> atom list" |
97 bv :: "trm \<Rightarrow> atom list" |
98 where |
98 where |
99 "bv (Var a) = [atom a]" |
99 "bv (Var a) = [atom a]" |
100 *) |
100 *) |