equal
deleted
inserted
replaced
20 term APP_raw |
20 term APP_raw |
21 term LET_raw |
21 term LET_raw |
22 term Test.BP_raw |
22 term Test.BP_raw |
23 thm bi_raw.simps |
23 thm bi_raw.simps |
24 thm permute_lam_raw_permute_bp_raw.simps |
24 thm permute_lam_raw_permute_bp_raw.simps |
25 thm alpha_lam_raw_alpha_bp_raw.intros |
25 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
26 thm fv_lam_raw_fv_bp_raw.simps |
26 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
27 thm eqvts |
27 thm eqvts |
28 |
28 |
29 print_theorems |
29 print_theorems |
30 |
30 |
31 text {* example 2 *} |
31 text {* example 2 *} |
133 "bv3 ANil = {}" |
133 "bv3 ANil = {}" |
134 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
134 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
135 |
135 |
136 (* example 4 from Terms.thy *) |
136 (* example 4 from Terms.thy *) |
137 |
137 |
138 |
|
139 nominal_datatype trm4 = |
138 nominal_datatype trm4 = |
140 Vr4 "name" |
139 Vr4 "name" |
141 | Ap4 "trm4" "trm4 list" |
140 | Ap4 "trm4" "trm4 list" |
142 | Lm4 x::"name" t::"trm4" bind x in t |
141 | Lm4 x::"name" t::"trm4" bind x in t |
143 |
142 |
|
143 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
|
144 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
144 |
145 |
145 (* example 5 from Terms.thy *) |
146 (* example 5 from Terms.thy *) |
146 |
147 |
147 nominal_datatype trm5 = |
148 nominal_datatype trm5 = |
148 Vr5 "name" |
149 Vr5 "name" |
219 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
220 | Cut n::"coname" t1::"phd" c::"coname" t2::"phd" bind n in t1, bind c in t2 |
220 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
221 | AndR c1::"coname" t1::"phd" c2::"coname" t2::"phd" "coname" bind c1 in t1, bind c2 in t2 |
221 | AndL1 n::"name" t::"phd" "name" bind n in t |
222 | AndL1 n::"name" t::"phd" "name" bind n in t |
222 | AndL2 n::"name" t::"phd" "name" bind n in t |
223 | AndL2 n::"name" t::"phd" "name" bind n in t |
223 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
224 | ImpL c::"coname" t1::"phd" n::"name" t2::"phd" "name" bind c in t1, bind n in t2 |
224 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in 1, bind c in t |
225 | ImpR c::"coname" n::"name" t::"phd" "coname" bind n in t, bind c in t |
|
226 |
|
227 (* PROBLEM?: why does it create for the Cut AndR ImpL cases |
|
228 two permutations, but only one is used *) |
|
229 thm alpha_phd_raw.intros[no_vars] |
|
230 thm fv_phd_raw.simps[no_vars] |
225 |
231 |
226 (* example form Leroy 96 about modules; OTT *) |
232 (* example form Leroy 96 about modules; OTT *) |
227 |
233 |
228 nominal_datatype mexp = |
234 nominal_datatype mexp = |
229 Acc "path" |
235 Acc "path" |
334 |
340 |
335 (*thm bv_raw.simps*) |
341 (*thm bv_raw.simps*) |
336 |
342 |
337 (* example 3 from Peter Sewell's bestiary *) |
343 (* example 3 from Peter Sewell's bestiary *) |
338 nominal_datatype exp = |
344 nominal_datatype exp = |
339 Var name |
345 Var "name" |
340 | App exp exp |
346 | App "exp" "exp" |
341 | Lam x::name e::exp bind x in e |
347 | Lam x::"name" e::"exp" bind x in e |
342 | Let x::name p::pat e1::exp e2::exp bind x in e2, bind "bp p" in e1 |
348 | Let x::"name" p::"pat" e1::"exp" e2::"exp" bind x in e2, bind "bp p" in e1 |
343 and pat = |
349 and pat = |
344 PVar name |
350 PVar "name" |
345 | PUnit |
351 | PUnit |
346 | PPair pat pat |
352 | PPair "pat" "pat" |
347 binder |
353 binder |
348 bp :: "pat \<Rightarrow> atom set" |
354 bp :: "pat \<Rightarrow> atom set" |
349 where |
355 where |
350 "bp (PVar x) = {atom x}" |
356 "bp (PVar x) = {atom x}" |
351 | "bp (PUnit) = {}" |
357 | "bp (PUnit) = {}" |