56 |
56 |
57 ML {* |
57 ML {* |
58 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} |
59 *} |
59 *} |
60 |
60 |
61 ML {* |
|
62 Local_Theory.exit_global; |
|
63 Class.instantiation; |
|
64 Class.prove_instantiation_exit_result; |
|
65 Named_Target.theory_init; |
|
66 op |-> |
|
67 *} |
|
68 |
|
69 done |
|
70 |> ... |
|
71 |-> (fn x => Class.prove_instantiation_exit_result phi tac x) |
|
72 |-> (fn y => ...) |
|
73 |
|
74 |
|
75 |
61 |
76 section {* NOT *} |
62 section {* NOT *} |
77 |
63 |
|
64 lemma [quot_respect]: |
|
65 "(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 |
|
84 |
|
85 thm eq_iff(5) |
|
86 thm eq_iff(5)[unfolded alphas permute_prod.simps] |
|
87 ML {* |
|
88 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) |
|
89 @{thms eq_iff(5)[unfolded alphas permute_prod.simps]} |
|
90 *} |
78 |
91 |
79 ML {* |
92 ML {* |
80 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]} |
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]} |
81 *} |
94 *} |
82 |
95 |
83 ML {* |
96 ML {* |
84 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
97 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolded alphas]} |
85 *} |
98 *} |
86 |
99 |
87 |
|
88 (* |
|
89 instance trm :: size .. |
|
90 instance assg :: size .. |
|
91 |
|
92 lemma "(size (Var x)) = 0" |
|
93 apply(descending) |
|
94 apply(rule trm_raw_assg_raw.size(9 - 16)) |
|
95 apply(simp) |
|
96 *) |
|
97 |
|
98 ML {* |
|
99 val thms_e = map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff[unfolding alphas]} |
|
100 *} |
|
101 |
100 |
102 |
101 |
103 thm perm_defs |
102 thm perm_defs |
104 thm perm_simps |
103 thm perm_simps |
105 |
104 |