equal
deleted
inserted
replaced
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 21]] |
7 declare [[STEPS = 100]] |
8 |
8 |
9 nominal_datatype singlelet: trm = |
9 nominal_datatype single_let: 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 x in t |
13 | Let a::"assg" t::"trm" bind (set) "bn a" in t |
13 | Let a::"assg" t::"trm" bind (set) "bn a" in t |
14 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 |
14 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2 |
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
23 |
23 |
24 |
24 thm single_let.distinct |
25 thm distinct |
25 thm single_let.induct |
26 thm induct |
26 thm single_let.exhaust |
27 thm exhaust |
27 thm single_let.fv_defs |
28 thm fv_defs |
28 thm single_let.bn_defs |
29 thm bn_defs |
29 thm single_let.perm_simps |
30 thm perm_simps |
30 thm single_let.eq_iff |
31 thm eq_iff |
31 thm single_let.fv_bn_eqvt |
32 thm fv_bn_eqvt |
32 thm single_let.size_eqvt |
33 thm size_eqvt |
|
34 |
33 |
35 |
34 |
36 |
35 (* |
37 |
36 |
38 |
37 |
39 lemma supp_fv: |
38 lemma supp_fv: |
40 "supp t = fv_trm t" |
39 "supp t = fv_trm t" |
41 "supp b = fv_bn b" |
40 "supp b = fv_bn b" |
65 thm trm_assg.perm |
64 thm trm_assg.perm |
66 thm trm_assg.induct |
65 thm trm_assg.induct |
67 thm trm_assg.inducts |
66 thm trm_assg.inducts |
68 thm trm_assg.distinct |
67 thm trm_assg.distinct |
69 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
68 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
|
69 *) |
70 |
70 |
71 (* TEMPORARY |
71 |
72 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
|
73 *) |
|
74 |
72 |
75 end |
73 end |
76 |
74 |
77 |
75 |
78 |
76 |