equal
deleted
inserted
replaced
1 theory Test |
1 theory Test |
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 1 *} |
5 text {* example 1 *} |
|
6 |
|
7 (* ML {* set show_hyps *} *) |
6 |
8 |
7 nominal_datatype lam = |
9 nominal_datatype lam = |
8 VAR "name" |
10 VAR "name" |
9 | APP "lam" "lam" |
11 | APP "lam" "lam" |
10 | LET bp::"bp" t::"lam" bind "bi bp" in t |
12 | LET bp::"bp" t::"lam" bind "bi bp" in t |
75 |
77 |
76 nominal_datatype tyS = |
78 nominal_datatype tyS = |
77 All xs::"name list" ty::"t_raw" bind xs in ty |
79 All xs::"name list" ty::"t_raw" bind xs in ty |
78 *) |
80 *) |
79 |
81 |
|
82 |
|
83 (* alpha_eqvt fails... |
80 nominal_datatype t = |
84 nominal_datatype t = |
81 Var "name" |
85 Var "name" |
82 | Fun "t" "t" |
86 | Fun "t" "t" |
83 and tyS = |
87 and tyS = |
84 All xs::"name set" ty::"t" bind xs in ty |
88 All xs::"name set" ty::"t" bind xs in ty *) |
85 |
89 |
86 (* example 1 from Terms.thy *) |
90 (* example 1 from Terms.thy *) |
87 |
91 |
88 nominal_datatype trm1 = |
92 nominal_datatype trm1 = |
89 Vr1 "name" |
93 Vr1 "name" |
133 "bv3 ANil = {}" |
137 "bv3 ANil = {}" |
134 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
138 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
135 |
139 |
136 (* example 4 from Terms.thy *) |
140 (* example 4 from Terms.thy *) |
137 |
141 |
138 |
142 (* fv_eqvt does not work, we need to repaire defined permute functions... |
139 nominal_datatype trm4 = |
143 nominal_datatype trm4 = |
140 Vr4 "name" |
144 Vr4 "name" |
141 | Ap4 "trm4" "trm4 list" |
145 | Ap4 "trm4" "trm4 list" |
142 | Lm4 x::"name" t::"trm4" bind x in t |
146 | Lm4 x::"name" t::"trm4" bind x in t |
143 |
147 *) |
144 |
148 |
145 (* example 5 from Terms.thy *) |
149 (* example 5 from Terms.thy *) |
146 |
150 |
147 nominal_datatype trm5 = |
151 nominal_datatype trm5 = |
148 Vr5 "name" |
152 Vr5 "name" |