251 fun mk_simp_implies Q = foldr (fn (R, S) => |
251 fun mk_simp_implies Q = foldr (fn (R, S) => |
252 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
252 Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps |
253 val aT = TFree ("'a", HOLogic.typeS); |
253 val aT = TFree ("'a", HOLogic.typeS); |
254 val x = Free ("x", aT); |
254 val x = Free ("x", aT); |
255 val y = Free ("y", aT) |
255 val y = Free ("y", aT) |
256 in OldGoals.prove_goalw_cterm [simp_implies_def] |
256 in standard (Goal.prove (Thm.theory_of_thm st) [] |
257 (cterm_of sign (Logic.mk_implies |
257 [mk_simp_implies (Logic.mk_equals (x, y))] |
258 (mk_simp_implies (Logic.mk_equals (x, y)), |
258 (mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))) |
259 mk_simp_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, y)))))) |
259 (fn prems => EVERY |
260 (fn hyps => [REPEAT (ares_tac (meta_eq_to_obj_eq :: hyps) 1)]) |
260 [rewrite_goals_tac [simp_implies_def], |
|
261 REPEAT (ares_tac (meta_eq_to_obj_eq :: map (rewrite_rule [simp_implies_def]) prems) 1)])) |
261 end |
262 end |
262 end; |
263 end; |
263 |
264 |
264 (*Congruence rules for = (instead of ==)*) |
265 (*Congruence rules for = (instead of ==)*) |
265 fun mk_meta_cong rl = zero_var_indexes |
266 fun mk_meta_cong rl = zero_var_indexes |
266 (let val rl' = Seq.hd (TRYALL (fn i => fn st => |
267 (let val rl' = Seq.hd (TRYALL (fn i => fn st => |
267 rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
268 rtac (lift_meta_eq_to_obj_eq i st) i st) rl) |
268 in mk_meta_eq rl' handle THM _ => |
269 in mk_meta_eq rl' handle THM _ => |