|
2436
|
1 |
theory Let
|
|
2454
|
2 |
imports "../Nominal2"
|
|
1600
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
atom_decl name
|
|
|
6 |
|
|
|
7 |
nominal_datatype trm =
|
|
2436
|
8 |
Var "name"
|
|
|
9 |
| App "trm" "trm"
|
2950
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
10 |
| Lam x::"name" t::"trm" binds x in t
|
0911cb7bf696
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
11 |
| Let as::"assn" t::"trm" binds "bn as" in t
|
|
2490
|
12 |
and assn =
|
|
|
13 |
ANil
|
|
|
14 |
| ACons "name" "trm" "assn"
|
|
1600
|
15 |
binder
|
|
|
16 |
bn
|
|
|
17 |
where
|
|
2490
|
18 |
"bn ANil = []"
|
|
|
19 |
| "bn (ACons x t as) = (atom x) # (bn as)"
|
|
|
20 |
|
|
2924
|
21 |
print_theorems
|
|
|
22 |
|
|
|
23 |
thm alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros
|
|
|
24 |
thm bn_raw.simps
|
|
|
25 |
thm permute_bn_raw.simps
|
|
|
26 |
thm trm_assn.perm_bn_alpha
|
|
|
27 |
thm trm_assn.permute_bn
|
|
|
28 |
|
|
2490
|
29 |
thm trm_assn.fv_defs
|
|
2924
|
30 |
thm trm_assn.eq_iff
|
|
2490
|
31 |
thm trm_assn.bn_defs
|
|
2922
|
32 |
thm trm_assn.bn_inducts
|
|
2490
|
33 |
thm trm_assn.perm_simps
|
|
2956
|
34 |
thm trm_assn.permute_bn
|
2492
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
35 |
thm trm_assn.induct
|
5ac9a74d22fd
post-processed eq_iff and supp threormes according to the fv-supp equality
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
36 |
thm trm_assn.inducts
|
|
2490
|
37 |
thm trm_assn.distinct
|
|
|
38 |
thm trm_assn.supp
|
|
2493
|
39 |
thm trm_assn.fresh
|
2617
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
40 |
thm trm_assn.exhaust
|
e44551d067e6
properly exported strong exhaust theorem; cleaned up some examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
thm trm_assn.strong_exhaust
|
2931
aaef9dec5e1d
side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
42 |
thm trm_assn.perm_bn_simps
|
|
2494
|
43 |
|
|
2670
|
44 |
|
2932
e8ab80062061
Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
45 |
end
|