27 val prove: Proof.context -> string list -> term list -> term -> |
27 val prove: Proof.context -> string list -> term list -> term -> |
28 ({prems: thm list, context: Proof.context} -> tactic) -> thm |
28 ({prems: thm list, context: Proof.context} -> tactic) -> thm |
29 val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
29 val prove_global: theory -> string list -> term list -> term -> (thm list -> tactic) -> thm |
30 val extract: int -> int -> thm -> thm Seq.seq |
30 val extract: int -> int -> thm -> thm Seq.seq |
31 val retrofit: int -> int -> thm -> thm -> thm Seq.seq |
31 val retrofit: int -> int -> thm -> thm -> thm Seq.seq |
|
32 val precise_conjunction_tac: int -> int -> tactic |
32 val conjunction_tac: int -> tactic |
33 val conjunction_tac: int -> tactic |
33 val precise_conjunction_tac: int -> int -> tactic |
|
34 val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic |
34 val asm_rewrite_goal_tac: bool * bool * bool -> (simpset -> tactic) -> simpset -> int -> tactic |
35 val rewrite_goal_tac: thm list -> int -> tactic |
35 val rewrite_goal_tac: thm list -> int -> tactic |
36 val norm_hhf_tac: int -> tactic |
36 val norm_hhf_tac: int -> tactic |
37 val compose_hhf: thm -> int -> thm -> thm Seq.seq |
37 val compose_hhf: thm -> int -> thm -> thm Seq.seq |
38 val compose_hhf_tac: thm -> int -> tactic |
38 val compose_hhf_tac: thm -> int -> tactic |
178 else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; |
178 else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; |
179 |
179 |
180 |
180 |
181 (* multiple goals *) |
181 (* multiple goals *) |
182 |
182 |
183 val conj_tac = SUBGOAL (fn (goal, i) => |
183 local |
184 if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i |
184 |
185 else no_tac); |
185 fun conj_intrs n = |
186 |
186 let |
187 val conjunction_tac = TRY o REPEAT_ALL_NEW conj_tac; |
187 val cert = Thm.cterm_of ProtoPure.thy; |
|
188 val names = Name.invents Name.context "A" n; |
|
189 val As = map (fn name => cert (Free (name, propT))) names; |
|
190 in |
|
191 Thm.generalize ([], names) 0 |
|
192 (Drule.implies_intr_list As (Conjunction.intr_list (map Thm.assume As))) |
|
193 end; |
|
194 |
|
195 fun count_conjs A = |
|
196 (case try Logic.dest_conjunction A of |
|
197 NONE => 1 |
|
198 | SOME (_, B) => count_conjs B + 1); |
|
199 |
|
200 in |
188 |
201 |
189 val precise_conjunction_tac = |
202 val precise_conjunction_tac = |
190 let |
203 let |
191 fun tac 0 i = eq_assume_tac i |
204 fun tac 0 i = eq_assume_tac i |
192 | tac 1 i = SUBGOAL (K all_tac) i |
205 | tac 1 i = SUBGOAL (K all_tac) i |
193 | tac n i = conj_tac i THEN TRY (fn st => tac (n - 1) (i + 1) st); |
206 | tac 2 i = rtac Conjunction.conjunctionI i |
|
207 | tac n i = rtac (conj_intrs n) i; |
194 in TRY oo tac end; |
208 in TRY oo tac end; |
|
209 |
|
210 val conjunction_tac = TRY o REPEAT_ALL_NEW (SUBGOAL (fn (goal, i) => |
|
211 let val n = count_conjs goal |
|
212 in if n < 2 then no_tac else precise_conjunction_tac n i end)); |
|
213 |
|
214 fun PRECISE_CONJUNCTS n tac = |
|
215 SELECT_GOAL (precise_conjunction_tac n 1 |
|
216 THEN tac |
|
217 THEN PRIMITIVE (Conjunction.uncurry ~1)); |
195 |
218 |
196 fun CONJUNCTS tac = |
219 fun CONJUNCTS tac = |
197 SELECT_GOAL (conjunction_tac 1 |
220 SELECT_GOAL (conjunction_tac 1 |
198 THEN tac |
221 THEN tac |
199 THEN PRIMITIVE (Conjunction.uncurry ~1)); |
222 THEN PRIMITIVE (Conjunction.uncurry ~1)); |
200 |
223 |
201 fun PRECISE_CONJUNCTS n tac = |
224 end; |
202 SELECT_GOAL (precise_conjunction_tac n 1 |
|
203 THEN tac |
|
204 THEN PRIMITIVE (Conjunction.uncurry ~1)); |
|
205 |
225 |
206 |
226 |
207 (* rewriting *) |
227 (* rewriting *) |
208 |
228 |
209 (*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) |
229 (*Rewrite subgoal i only. SELECT_GOAL avoids inefficiencies in goals_conv.*) |