167 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
167 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
168 end |
168 end |
169 *} |
169 *} |
170 |
170 |
171 |
171 |
172 thm id_apply |
|
173 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
172 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
174 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
173 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
175 thm HOL.sym[OF lambda_prs_mn_b,simplified] |
|
176 |
174 |
177 ML {* |
175 ML {* |
178 fun simp_lam_prs lthy thm = |
176 fun simp_lam_prs lthy thm = |
179 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
177 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
180 handle _ => thm |
178 handle _ => thm |
181 *} |
179 *} |
182 ML {* t_t2 *} |
180 ML {* t_t2 *} |
183 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
181 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
184 |
182 |
185 ML {* |
183 ML {* |
186 fun simp_allex_prs lthy thm = |
184 fun simp_allex_prs lthy quot thm = |
187 let |
185 let |
188 val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]}; |
186 val rwf = @{thm FORALL_PRS} OF [quot]; |
189 val rwfs = @{thm "HOL.sym"} OF [rwf]; |
187 val rwfs = @{thm "HOL.sym"} OF [rwf]; |
190 val rwe = @{thm EXISTS_PRS[OF QUOTIENT_my_int]}; |
188 val rwe = @{thm EXISTS_PRS} OF [quot]; |
191 val rwes = @{thm "HOL.sym"} OF [rwe] |
189 val rwes = @{thm "HOL.sym"} OF [rwe] |
192 in |
190 in |
193 (simp_allex_prs lthy (eqsubst_thm lthy [rwfs, rwes] thm)) |
191 (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) |
194 end |
192 end |
195 handle _ => thm |
193 handle _ => thm |
196 *} |
194 *} |
197 |
195 |
198 ML {* val t_a = simp_allex_prs @{context} t_l *} |
196 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
199 |
197 |
200 ML {* val t_defs = @{thms PLUS_def} *} |
198 ML {* val t_defs = @{thms PLUS_def} *} |
201 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
199 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
202 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
200 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
203 ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *} |
201 ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *} |