61 |
62 |
62 section {* NOT *} |
63 section {* NOT *} |
63 |
64 |
64 lemma [quot_respect]: |
65 lemma [quot_respect]: |
65 "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" |
66 "(alpha_assg_raw ===> alpha_assg_raw ===> op =) alpha_bn_raw alpha_bn_raw" |
66 "(op = ===> (alpha_trm_raw ===> op =) ===> prod_rel op = alpha_trm_raw ===> op =) prod_fv prod_fv" |
|
67 "((prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =) ===> |
|
68 (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===> |
|
69 prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> |
|
70 prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =) |
|
71 prod_alpha prod_alpha" |
|
72 "(op = ===> |
|
73 (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===> |
|
74 prod_rel op = alpha_trm_raw ===> prod_rel op = alpha_trm_raw ===> op =) |
|
75 prod_alpha prod_alpha" |
|
76 "((prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> |
|
77 prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw ===> op =) ===> |
|
78 (alpha_trm_raw ===> alpha_trm_raw ===> op =) ===> |
|
79 prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===> |
|
80 prod_rel (prod_rel (prod_rel op = alpha_trm_raw) alpha_trm_raw) alpha_trm_raw ===> |
|
81 op =) |
|
82 prod_alpha prod_alpha" |
|
83 sorry |
67 sorry |
84 |
68 |
85 thm eq_iff(5) |
69 |
86 thm eq_iff(5)[unfolded alphas permute_prod.simps] |
|
87 ML {* |
70 ML {* |
88 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
71 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
89 @{thms eq_iff(5)[unfolded alphas permute_prod.simps]} |
72 @{thms eq_iff[unfolded alphas permute_prod.simps prod_fv.simps prod_alpha_def prod_rel.simps |
|
73 prod.cases]} |
90 *} |
74 *} |
91 |
75 |
92 ML {* |
|
93 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas prod_fv.simps prod_rel.simps prod_alpha_def]} |
|
94 *} |
|
95 |
76 |
96 ML {* |
|
97 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas]} |
|
98 *} |
|
99 |
77 |
100 |
78 |
101 |
79 |
102 thm perm_defs |
80 thm perm_defs |
103 thm perm_simps |
81 thm perm_simps |