equal
deleted
inserted
replaced
27 thm trm_raw_assg_raw.inducts |
27 thm trm_raw_assg_raw.inducts |
28 thm fv_defs |
28 thm fv_defs |
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 |
|
33 (* cannot lift yet *) |
|
34 thm eq_iff |
32 thm eq_iff |
35 thm eq_iff_simps |
33 thm eq_iff_simps |
|
34 |
36 (* bn / eqvt lemmas for fv / fv_bn / bn *) |
35 (* bn / eqvt lemmas for fv / fv_bn / bn *) |
37 |
36 |
38 ML {* |
37 ML {* |
39 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
38 val thms_d = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms distinct} |
40 *} |
39 *} |
57 |
56 |
58 ML {* |
57 ML {* |
59 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
58 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms perm_laws} |
60 *} |
59 *} |
61 |
60 |
62 |
|
63 section {* NOT *} |
|
64 |
|
65 ML {* |
61 ML {* |
66 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
62 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
67 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
63 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
68 prod.cases]} |
64 prod.cases]} |
69 *} |
65 *} |
70 |
66 |
|
67 ML {* |
|
68 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
|
69 @{thms eq_iff_simps[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
70 prod.cases]} |
|
71 *} |
71 |
72 |
72 |
73 ML {* |
73 |
74 val thms_f = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms bn_defs} |
|
75 *} |
74 |
76 |
75 thm perm_defs |
77 thm perm_defs |
76 thm perm_simps |
78 thm perm_simps |
77 |
79 |
78 lemma supp_fv: |
80 lemma supp_fv: |