author | wenzelm |
Thu, 30 Jul 2009 12:20:43 +0200 | |
changeset 32283 | 3bebc195c124 |
parent 32281 | 750101435f60 |
child 32284 | d8ee8a956f19 |
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 |
*) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
68 |
fun lift_import params th ctxt = |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
69 |
let |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
70 |
val ((_, [th']), ctxt') = Variable.importT [th] ctxt; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
71 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
72 |
val Ts = map (#T o Thm.rep_cterm) params; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
73 |
val ts = map Thm.term_of params; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
74 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
75 |
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
|
76 |
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
|
77 |
val vars = rev (Term.add_vars prop []); |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
78 |
val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt'; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
79 |
fun var_inst (v as (_, T)) y = |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
80 |
if member (op =) concl_vars v then (v, Free (y, T)) |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
81 |
else (v, list_comb (Free (y, Ts ---> T), ts)); |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
82 |
val th'' = Thm.certify_instantiate ([], map2 var_inst vars ys) th'; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
83 |
in (th'', ctxt'') end; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
84 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
85 |
(* |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
86 |
[x, A x] |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
87 |
: |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
88 |
B x ==> C |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
89 |
------------------ |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
90 |
[!!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
|
91 |
: |
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
92 |
C |
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 |
fun lift_subgoals params asms th = |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
95 |
let |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
96 |
val lift = fold_rev Thm.all_name params o curry Drule.list_implies asms; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
97 |
val unlift = |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
98 |
fold (Thm.elim_implies o Thm.assume) asms o |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
99 |
Drule.forall_elim_list (map #2 params) o Thm.assume; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
100 |
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
|
101 |
val th' = fold (Thm.elim_implies o unlift) subgoals th; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
102 |
in (subgoals, th') end; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
103 |
|
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
104 |
fun retrofit ctxt1 ctxt0 params asms i st1 st0 = |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
105 |
let |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
106 |
val ps = map #2 params; |
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
107 |
val (st2, ctxt2) = lift_import ps st1 ctxt1; |
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
108 |
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
|
109 |
val result = st3 |
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
110 |
|> Goal.conclude |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
111 |
|> Drule.implies_intr_list asms |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
112 |
|> Drule.forall_intr_list ps |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
113 |
|> Drule.implies_intr_list subgoals |
32210
a5e9d9f3e5e1
retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents:
32200
diff
changeset
|
114 |
|> singleton (Variable.export ctxt2 ctxt0) |
a5e9d9f3e5e1
retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents:
32200
diff
changeset
|
115 |
|> Drule.zero_var_indexes |
32213
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
116 |
|> Drule.incr_indexes st0; |
f1b166317ae2
added focus_params/FOCUS_PARAMS, which focus on the parameter prefix only;
wenzelm
parents:
32210
diff
changeset
|
117 |
in Thm.compose_no_flatten false (result, Thm.nprems_of st1) i st0 end; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
118 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
119 |
|
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
120 |
(* tacticals *) |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
121 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
122 |
fun GEN_FOCUS flags tac ctxt i st = |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
123 |
if Thm.nprems_of st < i then Seq.empty |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
124 |
else |
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
125 |
let val (args as {context, params, asms, ...}, st') = gen_focus flags ctxt i st; |
32210
a5e9d9f3e5e1
retrofit: actually handle schematic variables -- need to export into original context;
wenzelm
parents:
32200
diff
changeset
|
126 |
in Seq.lifts (retrofit context ctxt params asms i) (tac args st') st end; |
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
127 |
|
32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset
|
128 |
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
|
129 |
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
|
130 |
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
|
131 |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
132 |
fun SUBPROOF tac = FOCUS (FILTER Thm.no_prems o tac); |
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
133 |
|
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
134 |
end; |
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset
|
135 |
|
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
136 |
val SUBPROOF = Subgoal.SUBPROOF; |
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset
|
137 |