equal
deleted
inserted
replaced
1 theory SingleLet |
1 theory SingleLet |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* val _ = recursive := false *} |
7 ML {* val _ = cheat_alpha_eqvt := true *} |
8 |
8 |
9 nominal_datatype trm = |
9 nominal_datatype trm = |
10 Var "name" |
10 Var "name" |
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
13 | Let a::"assg" t::"trm" bind "bn a" in t |
13 | Let a::"assg" t::"trm" bind_set "bn a" in t |
14 and assg = |
14 and assg = |
15 As "name" "trm" |
15 As "name" "trm" |
16 binder |
16 binder |
17 bn::"assg \<Rightarrow> atom set" |
17 bn::"assg \<Rightarrow> atom set" |
18 where |
18 where |
19 "bn (As x t) = {atom x}" |
19 "bn (As x t) = {atom x}" |
20 |
20 |
21 print_theorems |
|
22 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
21 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
23 |
|
24 thm trm_assg.fv |
22 thm trm_assg.fv |
25 thm trm_assg.supp |
23 thm trm_assg.supp |
26 thm trm_assg.eq_iff[simplified alphas_abs[symmetric]] |
24 thm trm_assg.eq_iff |
27 thm trm_assg.bn |
25 thm trm_assg.bn |
28 thm trm_assg.perm |
26 thm trm_assg.perm |
29 thm trm_assg.induct |
27 thm trm_assg.induct |
30 thm trm_assg.inducts |
28 thm trm_assg.inducts |
31 thm trm_assg.distinct |
29 thm trm_assg.distinct |
32 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
30 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
33 thm trm_assg.fv[simplified trm_assg.supp] |
31 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
|
32 |
|
33 setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *} |
|
34 declare permute_trm_raw_permute_assg_raw.simps[eqvt] |
|
35 declare alpha_gen_eqvt[eqvt] |
|
36 equivariance alpha_trm_raw |
|
37 |
34 |
38 |
35 end |
39 end |
36 |
40 |
37 |
41 |
38 |
42 |