author  wenzelm 
Wed, 29 May 2013 18:25:11 +0200  
changeset 52223  5bb6ae8acb87 
parent 49845  9b19c0e81166 
child 54883  dd04a8b654fc 
permissions  rwrr 
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; 
42495
1af81b70cf09
clarified Variable.focus vs. Variable.focus_cterm  eliminated clone;
wenzelm
parents:
42360
diff
changeset

36 
val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1; 
32281
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 
42360  70 
val cert = Thm.cterm_of (Proof_Context.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); 
52223
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
49845
diff
changeset

128 
in 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
49845
diff
changeset

129 
Thm.bicompose {flatten = true, match = false, incremented = false} 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
49845
diff
changeset

130 
(false, result, Thm.nprems_of st1) i st0 
5bb6ae8acb87
tuned signature  more explicit flags for lowlevel Thm.bicompose;
wenzelm
parents:
49845
diff
changeset

131 
end; 
32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

132 

2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

133 

2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

134 
(* tacticals *) 
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

135 

32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset

136 
fun GEN_FOCUS flags tac ctxt i st = 
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset

137 
if Thm.nprems_of st < i then Seq.empty 
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset

138 
else 
32329  139 
let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st; 
140 
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

141 

32281
750101435f60
focus: more precise treatment of schematic variables, only the "visible" part of the text is fixed;
wenzelm
parents:
32213
diff
changeset

142 
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

143 
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

144 
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

145 

49845  146 
fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt; 
20210
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset

147 

8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset

148 
end; 
8fe4ae4360eb
Tactical operations depending on local subgoal structure.
wenzelm
parents:
diff
changeset

149 

32200
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

150 
val SUBPROOF = Subgoal.SUBPROOF; 
2bd8ab91a426
advanced retrofit, which allows new subgoals and variables;
wenzelm
parents:
31794
diff
changeset

151 