equal
deleted
inserted
replaced
69 apply(simp) |
69 apply(simp) |
70 *) |
70 *) |
71 |
71 |
72 text {* example 1 *} |
72 text {* example 1 *} |
73 |
73 |
|
74 (* ML {* set show_hyps *} *) |
|
75 |
74 nominal_datatype lam = |
76 nominal_datatype lam = |
75 VAR "name" |
77 VAR "name" |
76 | APP "lam" "lam" |
78 | APP "lam" "lam" |
77 | LET bp::"bp" t::"lam" bind "bi bp" in t |
79 | LET bp::"bp" t::"lam" bind "bi bp" in t |
78 and bp = |
80 and bp = |
145 |
147 |
146 nominal_datatype tyS = |
148 nominal_datatype tyS = |
147 All xs::"name list" ty::"t_raw" bind xs in ty |
149 All xs::"name list" ty::"t_raw" bind xs in ty |
148 *) |
150 *) |
149 |
151 |
|
152 |
|
153 (* alpha_eqvt fails... |
150 nominal_datatype t = |
154 nominal_datatype t = |
151 Var "name" |
155 Var "name" |
152 | Fun "t" "t" |
156 | Fun "t" "t" |
153 and tyS = |
157 and tyS = |
154 All xs::"name set" ty::"t" bind xs in ty |
158 All xs::"name set" ty::"t" bind xs in ty *) |
155 |
159 |
156 (* example 1 from Terms.thy *) |
160 (* example 1 from Terms.thy *) |
157 |
161 |
158 nominal_datatype trm1 = |
162 nominal_datatype trm1 = |
159 Vr1 "name" |
163 Vr1 "name" |
203 "bv3 ANil = {}" |
207 "bv3 ANil = {}" |
204 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
208 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
205 |
209 |
206 (* example 4 from Terms.thy *) |
210 (* example 4 from Terms.thy *) |
207 |
211 |
|
212 (* fv_eqvt does not work, we need to repaire defined permute functions... |
208 nominal_datatype trm4 = |
213 nominal_datatype trm4 = |
209 Vr4 "name" |
214 Vr4 "name" |
210 | Ap4 "trm4" "trm4 list" |
215 | Ap4 "trm4" "trm4 list" |
211 | Lm4 x::"name" t::"trm4" bind x in t |
216 | Lm4 x::"name" t::"trm4" bind x in t |
212 |
217 |