166 text {* Below is the construction site code used if things do now work *} |
166 text {* Below is the construction site code used if things do now work *} |
167 |
167 |
168 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
168 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
169 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
169 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
170 |
170 |
171 ML {* val (g, thm, othm) = |
171 ML {* val t_t = |
172 Toplevel.program (fn () => |
172 Toplevel.program (fn () => |
173 repabs_eq @{context} t_r consts rty qty |
173 repabs @{context} t_r consts rty qty |
174 quot rel_refl trans2 |
174 quot rel_refl trans2 |
175 rsp_thms |
175 rsp_thms |
176 ) |
176 ) |
177 *} |
177 *} |
178 ML {* |
|
179 val t_t2 = |
|
180 Toplevel.program (fn () => |
|
181 repabs_eq2 @{context} (g, thm, othm) |
|
182 ) |
|
183 *} |
|
184 |
|
185 |
178 |
186 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
179 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
180 |
187 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
181 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
188 |
182 |
189 ML {* |
183 ML {* |
190 fun simp_lam_prs lthy thm = |
184 fun simp_lam_prs lthy thm = |
191 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
185 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
192 handle _ => thm |
186 handle _ => thm |
193 *} |
187 *} |
194 ML {* t_t2 *} |
188 ML {* t_t *} |
195 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
189 ML {* val t_l = simp_lam_prs @{context} t_t *} |
196 |
190 |
197 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
191 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
198 |
192 |
199 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
193 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
200 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
194 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |