equal
deleted
inserted
replaced
154 |
154 |
155 |
155 |
156 |
156 |
157 text {* Below is the construction site code used if things do now work *} |
157 text {* Below is the construction site code used if things do now work *} |
158 |
158 |
159 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
159 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
160 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
160 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
161 |
161 |
162 ML {* val t_t = |
162 ML {* val t_t = |
163 Toplevel.program (fn () => |
163 Toplevel.program (fn () => |
164 repabs @{context} t_r consts rty qty |
164 repabs @{context} t_r consts rty qty |
168 *} |
168 *} |
169 |
169 |
170 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
170 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
171 |
171 |
172 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
172 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
173 |
|
174 ML {* |
|
175 fun simp_lam_prs lthy thm = |
|
176 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
|
177 handle _ => thm |
|
178 *} |
|
179 ML {* t_t *} |
173 ML {* t_t *} |
180 ML {* val t_l = simp_lam_prs @{context} t_t *} |
174 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
181 |
175 |
182 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
176 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
183 |
177 |
184 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
178 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
185 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
179 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
186 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
180 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
187 ML {* ObjectLogic.rulify t_r *} |
181 ML {* ObjectLogic.rulify t_r *} |
188 |
182 |
189 |
183 |
190 |
184 |