equal
deleted
inserted
replaced
1 theory SingleLet |
1 theory SingleLet |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
|
6 |
|
7 ML {* print_depth 50 *} |
|
8 declare [[STEPS = 19]] |
6 |
9 |
7 nominal_datatype trm = |
10 nominal_datatype trm = |
8 Var "name" |
11 Var "name" |
9 | App "trm" "trm" |
12 | App "trm" "trm" |
10 | Lam x::"name" t::"trm" bind_set x in t |
13 | Lam x::"name" t::"trm" bind_set x in t |
14 binder |
17 binder |
15 bn::"assg \<Rightarrow> atom set" |
18 bn::"assg \<Rightarrow> atom set" |
16 where |
19 where |
17 "bn (As x t) = {atom x}" |
20 "bn (As x t) = {atom x}" |
18 |
21 |
|
22 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] |
|
23 |
19 ML {* Inductive.the_inductive *} |
24 ML {* Inductive.the_inductive *} |
20 thm trm_assg.fv |
25 thm trm_assg.fv |
21 thm trm_assg.supp |
26 thm trm_assg.supp |
22 thm trm_assg.eq_iff |
27 thm trm_assg.eq_iff |
23 thm trm_assg.bn |
28 thm trm_assg.bn |
24 thm trm_assg.perm |
29 thm trm_assg.perm |
25 thm trm_assg.induct |
30 thm trm_assg.induct |
26 thm trm_assg.inducts |
31 thm trm_assg.inducts |
27 thm trm_assg.distinct |
32 thm trm_assg.distinct |
28 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
33 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
|
34 |
|
35 (* TEMPORARY |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
36 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
30 |
37 *) |
31 |
38 |
32 |
39 |
33 |
40 |
34 end |
41 end |
35 |
42 |