equal
deleted
inserted
replaced
29 thm perm_simps |
29 thm perm_simps |
30 thm perm_laws |
30 thm perm_laws |
31 thm trm_raw_assg_raw.size(9 - 16) |
31 thm trm_raw_assg_raw.size(9 - 16) |
32 thm eq_iff |
32 thm eq_iff |
33 thm eq_iff_simps |
33 thm eq_iff_simps |
|
34 thm bn_defs |
|
35 thm fv_eqvt |
|
36 thm bn_eqvt |
|
37 thm size_eqvt |
34 |
38 |
35 (* bn / eqvt lemmas for fv / fv_bn / bn *) |
39 |
|
40 (* eqvt lemmas for fv / fv_bn / bn *) |
36 |
41 |
37 ML {* |
42 ML {* |
38 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
43 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
39 *} |
44 *} |
40 |
45 |
72 |
77 |
73 ML {* |
78 ML {* |
74 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs} |
79 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs} |
75 *} |
80 *} |
76 |
81 |
77 thm perm_defs |
82 ML {* |
78 thm perm_simps |
83 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_eqvt} |
|
84 *} |
|
85 |
|
86 ML {* |
|
87 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms fv_eqvt} |
|
88 *} |
|
89 |
|
90 ML {* |
|
91 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms size_eqvt} |
|
92 *} |
|
93 |
|
94 |
|
95 |
79 |
96 |
80 lemma supp_fv: |
97 lemma supp_fv: |
81 "supp t = fv_trm t" |
98 "supp t = fv_trm t" |
82 "supp b = fv_bn b" |
99 "supp b = fv_bn b" |
83 apply(induct t and b rule: i1) |
100 apply(induct t and b rule: i1) |