wenzelm@20210
|
1 |
(* Title: Pure/subgoal.ML
|
wenzelm@20210
|
2 |
Author: Makarius
|
wenzelm@20210
|
3 |
|
wenzelm@20210
|
4 |
Tactical operations depending on local subgoal structure.
|
wenzelm@20210
|
5 |
*)
|
wenzelm@20210
|
6 |
|
wenzelm@20210
|
7 |
signature BASIC_SUBGOAL =
|
wenzelm@20210
|
8 |
sig
|
wenzelm@20231
|
9 |
val SUBPROOF:
|
wenzelm@20219
|
10 |
({context: Proof.context, schematics: ctyp list * cterm list,
|
wenzelm@20219
|
11 |
params: cterm list, asms: cterm list, concl: cterm,
|
wenzelm@20231
|
12 |
prems: thm list} -> tactic) -> Proof.context -> int -> tactic
|
wenzelm@20210
|
13 |
end
|
wenzelm@20210
|
14 |
|
wenzelm@20210
|
15 |
signature SUBGOAL =
|
wenzelm@20210
|
16 |
sig
|
wenzelm@20210
|
17 |
include BASIC_SUBGOAL
|
wenzelm@20210
|
18 |
val focus: Proof.context -> int -> thm ->
|
wenzelm@20219
|
19 |
{context: Proof.context, schematics: ctyp list * cterm list,
|
wenzelm@20219
|
20 |
params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
|
wenzelm@20210
|
21 |
|
wenzelm@20210
|
22 |
end;
|
wenzelm@20210
|
23 |
|
wenzelm@20210
|
24 |
structure Subgoal: SUBGOAL =
|
wenzelm@20210
|
25 |
struct
|
wenzelm@20210
|
26 |
|
wenzelm@20210
|
27 |
(* canonical proof decomposition -- similar to fix/assume/show *)
|
wenzelm@20210
|
28 |
|
wenzelm@20210
|
29 |
fun focus ctxt i st =
|
wenzelm@20210
|
30 |
let
|
wenzelm@21605
|
31 |
val ((schematics, [st']), ctxt') =
|
wenzelm@31794
|
32 |
Variable.import true [Simplifier.norm_hhf_protect st] ctxt;
|
wenzelm@20301
|
33 |
val ((params, goal), ctxt'') = Variable.focus_subgoal i st' ctxt';
|
wenzelm@20210
|
34 |
val asms = Drule.strip_imp_prems goal;
|
wenzelm@20210
|
35 |
val concl = Drule.strip_imp_concl goal;
|
wenzelm@20231
|
36 |
val (prems, context) = Assumption.add_assumes asms ctxt'';
|
wenzelm@20210
|
37 |
in
|
wenzelm@20219
|
38 |
({context = context, schematics = schematics, params = params,
|
wenzelm@20219
|
39 |
asms = asms, concl = concl, prems = prems}, Goal.init concl)
|
wenzelm@20210
|
40 |
end;
|
wenzelm@20210
|
41 |
|
wenzelm@20231
|
42 |
fun SUBPROOF tac ctxt i st =
|
wenzelm@20210
|
43 |
if Thm.nprems_of st < i then Seq.empty
|
wenzelm@20210
|
44 |
else
|
wenzelm@20210
|
45 |
let
|
wenzelm@20219
|
46 |
val (args as {context, params, ...}, st') = focus ctxt i st;
|
wenzelm@20219
|
47 |
fun export_closed th =
|
wenzelm@20219
|
48 |
let
|
wenzelm@20219
|
49 |
val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
|
wenzelm@20579
|
50 |
val vs = map (Thm.dest_arg o Drule.strip_imp_concl o Thm.cprop_of) params';
|
wenzelm@20219
|
51 |
in Drule.forall_intr_list vs th' end;
|
wenzelm@20219
|
52 |
fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
|
wenzelm@20219
|
53 |
in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
|
wenzelm@20210
|
54 |
|
wenzelm@20210
|
55 |
end;
|
wenzelm@20210
|
56 |
|
wenzelm@20210
|
57 |
structure BasicSubgoal: BASIC_SUBGOAL = Subgoal;
|
wenzelm@20210
|
58 |
open BasicSubgoal;
|