author | blanchet |
Wed, 03 Nov 2010 22:33:23 +0100 | |
changeset 40342 | 3154f63e2bda |
parent 34075 | 451b0c8a15cf |
child 42360 | da8817d01e7c |
permissions | -rw-r--r-- |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/subgoal.ML |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
3 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
4 |
Tactical operations with explicit subgoal focus, based on canonical |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
5 |
proof decomposition. The "visible" part of the text within the |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
6 |
context is fixed, the remaining goal may be schematic. |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
7 |
*) |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
8 |
|
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
9 |
signature SUBGOAL = |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
10 |
sig |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
11 |
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
12 |
asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list} |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
13 |
val focus_params: Proof.context -> int -> thm -> focus * thm |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
14 |
val focus_prems: Proof.context -> int -> thm -> focus * thm |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
15 |
val focus: Proof.context -> int -> thm -> focus * thm |
32210
a5e9d9f3e5e1
retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents:
32200
diff
changeset
|
16 |
val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list -> |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
17 |
int -> thm -> thm -> thm Seq.seq |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
18 |
val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
19 |
val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
20 |
val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
21 |
val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
22 |
end; |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
23 |
|
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
24 |
structure Subgoal: SUBGOAL = |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
25 |
struct |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
26 |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
27 |
(* focus *) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
28 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
29 |
type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list, |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
30 |
asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}; |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
31 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
32 |
fun gen_focus (do_prems, do_concl) ctxt i raw_st = |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
33 |
let |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
34 |
val st = Simplifier.norm_hhf_protect raw_st; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
35 |
val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
36 |
val ((params, goal), ctxt2) = Variable.focus (Thm.cprem_of st' i) ctxt1; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
37 |
|
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
38 |
val (asms, concl) = |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
39 |
if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal) |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
40 |
else ([], goal); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
41 |
val text = asms @ (if do_concl then [concl] else []); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
42 |
|
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
43 |
val ((_, schematic_terms), ctxt3) = |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
44 |
Variable.import_inst true (map Thm.term_of text) ctxt2 |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
45 |
|>> Thm.certify_inst (Thm.theory_of_thm raw_st); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
46 |
|
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
47 |
val schematics = (schematic_types, schematic_terms); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
48 |
val asms' = map (Thm.instantiate_cterm schematics) asms; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
49 |
val concl' = Thm.instantiate_cterm schematics concl; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
50 |
val (prems, context) = Assumption.add_assumes asms' ctxt3; |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
51 |
in |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
52 |
({context = context, params = params, prems = prems, |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
53 |
asms = asms', concl = concl', schematics = schematics}, Goal.init concl') |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
54 |
end; |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
55 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
56 |
val focus_params = gen_focus (false, false); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
57 |
val focus_prems = gen_focus (true, false); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
58 |
val focus = gen_focus (true, true); |
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
59 |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
60 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
61 |
(* lift and retrofit *) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
62 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
63 |
(* |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
64 |
B [?'b, ?y] |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
65 |
---------------- |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
66 |
B ['b, y params] |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
67 |
*) |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
68 |
fun lift_import idx params th ctxt = |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
69 |
let |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
70 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt); |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
71 |
val ((_, [th']), ctxt') = Variable.importT [th] ctxt; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
72 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
73 |
val Ts = map (#T o Thm.rep_cterm) params; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
74 |
val ts = map Thm.term_of params; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
75 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
76 |
val prop = Thm.full_prop_of th'; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
77 |
val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) []; |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
78 |
val vars = rev (Term.add_vars prop []); |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
79 |
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt'; |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
80 |
|
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
81 |
fun var_inst v y = |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
82 |
let |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
83 |
val ((x, i), T) = v; |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
84 |
val (U, args) = |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
85 |
if member (op =) concl_vars v then (T, []) |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
86 |
else (Ts ---> T, ts); |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
87 |
val u = Free (y, U); |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
88 |
in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end; |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
89 |
val (inst1, inst2) = split_list (map (pairself (pairself cert)) (map2 var_inst vars ys)); |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
90 |
|
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
91 |
val th'' = Thm.instantiate ([], inst1) th'; |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
92 |
in ((inst2, th''), ctxt'') end; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
93 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
94 |
(* |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
95 |
[x, A x] |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
96 |
: |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
97 |
B x ==> C |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
98 |
------------------ |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
99 |
[!!x. A x ==> B x] |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
100 |
: |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
101 |
C |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
102 |
*) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
103 |
fun lift_subgoals params asms th = |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
104 |
let |
32329 | 105 |
fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct)); |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
106 |
val unlift = |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
107 |
fold (Thm.elim_implies o Thm.assume) asms o |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
108 |
Drule.forall_elim_list (map #2 params) o Thm.assume; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
109 |
val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th)); |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
110 |
val th' = fold (Thm.elim_implies o unlift) subgoals th; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
111 |
in (subgoals, th') end; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
112 |
|
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
113 |
fun retrofit ctxt1 ctxt0 params asms i st1 st0 = |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
114 |
let |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
115 |
val idx = Thm.maxidx_of st0 + 1; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
116 |
val ps = map #2 params; |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
117 |
val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1; |
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
118 |
val (subgoals, st3) = lift_subgoals params asms st2; |
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
119 |
val result = st3 |
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
120 |
|> Goal.conclude |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
121 |
|> Drule.implies_intr_list asms |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
122 |
|> Drule.forall_intr_list ps |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
123 |
|> Drule.implies_intr_list subgoals |
32284
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
124 |
|> fold_rev (Thm.forall_intr o #1) subgoal_inst |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
125 |
|> fold (Thm.forall_elim o #2) subgoal_inst |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
126 |
|> Thm.adjust_maxidx_thm idx |
d8ee8a956f19
retrofit: more precise handling of locally introduced schematic variables (avoid zero_var_indexes);
wenzelm
parents:
32283
diff
changeset
|
127 |
|> singleton (Variable.export ctxt2 ctxt0); |
34075
451b0c8a15cf
Subgoal.FOCUS etc.: resulting goal state is normalized as usual for resolution;
wenzelm
parents:
32329
diff
changeset
|
128 |
in Thm.bicompose false (false, result, Thm.nprems_of st1) i st0 end; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
129 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
130 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
131 |
(* tacticals *) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
132 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
133 |
fun GEN_FOCUS flags tac ctxt i st = |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
134 |
if Thm.nprems_of st < i then Seq.empty |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
135 |
else |
32329 | 136 |
let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st; |
137 |
in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end; |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
138 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
139 |
val FOCUS_PARAMS = GEN_FOCUS (false, false); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
140 |
val FOCUS_PREMS = GEN_FOCUS (true, false); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
141 |
val FOCUS = GEN_FOCUS (true, true); |
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
142 |
|
32329 | 143 |
fun SUBPROOF tac ctxt = FOCUS (Seq.map (tap (Goal.check_finished ctxt)) oo tac) ctxt; |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
144 |
|
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
145 |
end; |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
146 |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
147 |
val SUBPROOF = Subgoal.SUBPROOF; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
148 |