equal
deleted
inserted
replaced
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Vr "name" |
12 Vr "name" |
13 | Ap "trm" "trm" |
13 | Ap "trm" "trm" |
14 | Lm x::"name" t::"trm" bind x in t |
14 | Lm x::"name" t::"trm" bind x in t |
15 | Lt a::"lts" t::"trm" bind "bn a" in t |
15 | Lt a::"lts" t::"trm" bind "bn a" in t |
|
16 (*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*) |
16 and lts = |
17 and lts = |
17 Lnil |
18 Lnil |
18 | Lcons "name" "trm" "lts" |
19 | Lcons "name" "trm" "lts" |
19 binder |
20 binder |
20 bn |
21 bn |
21 where |
22 where |
22 "bn Lnil = []" |
23 "bn Lnil = []" |
23 | "bn (Lcons x t l) = (atom x) # (bn l)" |
24 | "bn (Lcons x t l) = (atom x) # (bn l)" |
24 |
25 |
|
26 |
|
27 thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros |
|
28 |
25 thm trm_lts.fv |
29 thm trm_lts.fv |
26 thm trm_lts.eq_iff |
30 thm trm_lts.eq_iff |
27 thm trm_lts.bn |
31 thm trm_lts.bn |
28 thm trm_lts.perm |
32 thm trm_lts.perm |
29 thm trm_lts.induct[no_vars] |
33 thm trm_lts.induct[no_vars] |
30 thm trm_lts.inducts[no_vars] |
34 thm trm_lts.inducts[no_vars] |
31 thm trm_lts.distinct |
35 thm trm_lts.distinct |
|
36 (*thm trm_lts.supp*) |
32 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
37 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
33 |
38 |
34 primrec |
39 primrec |
35 permute_bn_raw |
40 permute_bn_raw |
36 where |
41 where |