equal
deleted
inserted
replaced
97 (* transformations of premises in inductions *) |
97 (* transformations of premises in inductions *) |
98 val transform_prem1: Proof.context -> string list -> thm -> thm |
98 val transform_prem1: Proof.context -> string list -> thm -> thm |
99 val transform_prem2: Proof.context -> string list -> thm -> thm |
99 val transform_prem2: Proof.context -> string list -> thm -> thm |
100 |
100 |
101 (* transformation into the object logic *) |
101 (* transformation into the object logic *) |
102 val atomize: thm -> thm |
102 val atomize: Proof.context -> thm -> thm |
103 val atomize_rule: int -> thm -> thm |
103 val atomize_rule: Proof.context -> int -> thm -> thm |
104 val atomize_concl: 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: (int -> tactic) -> int -> tactic |
108 end |
108 end |
109 |
109 |
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) (etac 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 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars; |
495 fun atomize ctxt = Conv.fconv_rule (Object_Logic.atomize ctxt) o forall_intr_vars; |
496 fun atomize_rule i thm = |
496 fun atomize_rule ctxt i thm = |
497 Conv.fconv_rule (Conv.concl_conv i Object_Logic.atomize) thm |
497 Conv.fconv_rule (Conv.concl_conv i (Object_Logic.atomize ctxt)) thm |
498 fun atomize_concl thm = atomize_rule (length (prems_of thm)) thm |
498 fun atomize_concl ctxt thm = atomize_rule ctxt (length (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 tac i = |
503 let |
503 let |