102 val atomize: Proof.context -> thm -> thm |
102 val atomize: Proof.context -> thm -> thm |
103 val atomize_rule: Proof.context -> int -> thm -> thm |
103 val atomize_rule: Proof.context -> int -> thm -> thm |
104 val atomize_concl: Proof.context -> thm -> thm |
104 val atomize_concl: Proof.context -> thm -> thm |
105 |
105 |
106 (* applies a tactic to a formula composed of conjunctions *) |
106 (* applies a tactic to a formula composed of conjunctions *) |
107 val conj_tac: (int -> tactic) -> int -> tactic |
107 val conj_tac: Proof.context -> (int -> tactic) -> int -> tactic |
108 end |
108 end |
109 |
109 |
110 |
110 |
111 structure Nominal_Library: NOMINAL_LIBRARY = |
111 structure Nominal_Library: NOMINAL_LIBRARY = |
112 struct |
112 struct |
448 fun map_thm_tac ctxt tac thm = |
448 fun map_thm_tac ctxt tac thm = |
449 let |
449 let |
450 val monos = Inductive.get_monos ctxt |
450 val monos = Inductive.get_monos ctxt |
451 val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} |
451 val simpset = put_simpset HOL_basic_ss ctxt addsimps @{thms split_def} |
452 in |
452 in |
453 EVERY [cut_facts_tac [thm] 1, etac rev_mp 1, |
453 EVERY [cut_facts_tac [thm] 1, eresolve_tac ctxt [rev_mp] 1, |
454 REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), |
454 REPEAT_DETERM (FIRSTGOAL (simp_tac simpset THEN' resolve_tac ctxt monos)), |
455 REPEAT_DETERM (rtac impI 1 THEN (assume_tac ctxt 1 ORELSE tac))] |
455 REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))] |
456 end |
456 end |
457 |
457 |
458 fun map_thm ctxt f tac thm = |
458 fun map_thm ctxt f tac thm = |
459 let |
459 let |
460 val opt_goal_trm = map_term f (Thm.prop_of thm) |
460 val opt_goal_trm = map_term f (Thm.prop_of thm) |
483 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
483 Const (name, _) => if member (op =) names name then SOME f2 else NONE |
484 | _ => NONE) |
484 | _ => NONE) |
485 | split_conj2 _ _ = NONE; |
485 | split_conj2 _ _ = NONE; |
486 |
486 |
487 fun transform_prem1 ctxt names thm = |
487 fun transform_prem1 ctxt names thm = |
488 map_thm ctxt (split_conj1 names) (etac conjunct1 1) thm |
488 map_thm ctxt (split_conj1 names) (eresolve_tac ctxt [conjunct1] 1) thm |
489 |
489 |
490 fun transform_prem2 ctxt names thm = |
490 fun transform_prem2 ctxt names thm = |
491 map_thm ctxt (split_conj2 names) (etac conjunct2 1) thm |
491 map_thm ctxt (split_conj2 names) (eresolve_tac ctxt [conjunct2] 1) thm |
492 |
492 |
493 |
493 |
494 (* transforms a theorem into one of the object logic *) |
494 (* transforms a theorem into one of the object logic *) |
495 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; |
495 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; |
496 fun atomize_rule ctxt i thm = |
496 fun atomize_rule ctxt i thm = |
497 Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm |
497 Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm |
498 fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm |
498 fun atomize_concl ctxt thm = atomize_rule ctxt (length (Thm.prems_of thm)) thm |
499 |
499 |
500 |
500 |
501 (* applies a tactic to a formula composed of conjunctions *) |
501 (* applies a tactic to a formula composed of conjunctions *) |
502 fun conj_tac tac i = |
502 fun conj_tac ctxt tac i = |
503 let |
503 let |
504 fun select (trm, i) = |
504 fun select (trm, i) = |
505 case trm of |
505 case trm of |
506 @{term "Trueprop"} $ t' => select (t', i) |
506 @{term "Trueprop"} $ t' => select (t', i) |
507 | @{term "op &"} $ _ $ _ => EVERY' [rtac @{thm conjI}, RANGE [conj_tac tac, conj_tac tac]] i |
507 | @{term "op &"} $ _ $ _ => |
|
508 EVERY' [resolve_tac ctxt @{thms conjI}, RANGE [conj_tac ctxt tac, conj_tac ctxt tac]] i |
508 | _ => tac i |
509 | _ => tac i |
509 in |
510 in |
510 SUBGOAL select i |
511 SUBGOAL select i |
511 end |
512 end |
512 |
513 |