equal
deleted
inserted
replaced
177 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
177 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
178 in |
178 in |
179 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
179 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
180 end |
180 end |
181 *} |
181 *} |
|
182 |
|
183 |
|
184 |
|
185 ML {* |
|
186 fun atomize_goal thy gl = |
|
187 let |
|
188 val vars = map Free (Term.add_frees gl []); |
|
189 fun lambda_all (var as Free(_, T)) trm = (Term.all T) $ lambda var trm; |
|
190 val gla = fold lambda_all vars (@{term "Trueprop"} $ gl) |
|
191 val glf = Type.legacy_freeze gla |
|
192 val glac = (snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glf)) |
|
193 in |
|
194 term_of glac |
|
195 end |
|
196 *} |
|
197 |
|
198 ML {* atomize_goal @{theory} @{term "PLUS a b = PLUS b a"} *} |
182 |
199 |
183 |
200 |
184 ML {* |
201 ML {* |
185 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
202 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
186 let |
203 let |
230 val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) |
247 val artrm = (prop_of (atomize_thm @{thm plus_sym_pre})) |
231 val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm |
248 val reg_artm = mk_REGULARIZE_goal @{context} artrm aqtrm |
232 *} |
249 *} |
233 |
250 |
234 ML {* |
251 ML {* |
235 lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "Trueprop (\<forall>a b. PLUS a b = PLUS b a)"} |
252 lift_thm_g_my_int @{context} @{thm plus_sym_pre} @{term "PLUS a b = PLUS b a"} |
236 *} |
253 *} |
237 |
254 |
238 |
255 |
239 prove {* reg_artm *} |
256 prove {* reg_artm *} |
240 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
257 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
399 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
416 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_a *} |
400 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
417 ML {* val defs_sym = flat (map (add_lower_defs @{context}) defs) *} |
401 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
418 ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_l *} |
402 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
419 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
403 ML {* ObjectLogic.rulify t_r *} |
420 ML {* ObjectLogic.rulify t_r *} |
|
421 ML {* @{term "Trueprop"} *} |
|
422 |