author  blanchet 
Sun, 03 May 2015 22:15:29 +0200  
changeset 60252  2c468c062589 
parent 59058  a78612c67ec0 
child 60305  7d278b0617d3 
permissions  rwrr 
55287  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML 
52555  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Author: Steffen Juilf Smolka, TU Muenchen 

4 

5 
Reconstructors. 

6 
*) 

7 

55287  8 
signature SLEDGEHAMMER_PROOF_METHODS = 
52555  9 
sig 
10 
type stature = ATP_Problem_Generate.stature 

11 

55285  12 
datatype proof_method = 
13 
Metis_Method of string option * string option  

14 
Meson_Method  

58061  15 
SMT_Method  
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset

16 
SATx_Method  
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

17 
Blast_Method  
55285  18 
Simp_Method  
19 
Simp_Size_Method  

20 
Auto_Method  

58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

21 
Fastforce_Method  
55285  22 
Force_Method  
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

23 
Moura_Method  
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

24 
Linarith_Method  
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

25 
Presburger_Method  
55285  26 
Algebra_Method 
52555  27 

54824  28 
datatype play_outcome = 
29 
Played of Time.time  

30 
Play_Timed_Out of Time.time  

56093  31 
Play_Failed 
52555  32 

54824  33 
type one_line_params = 
57739  34 
((string * stature) list * (proof_method * play_outcome)) * string * int * int 
52555  35 

57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

36 
val is_proof_method_direct : proof_method > bool 
60252
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

37 
val proof_method_distinguishes_chained_and_direct : proof_method > bool 
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

38 
val string_of_proof_method : Proof.context > string list > proof_method > string 
57054  39 
val tac_of_proof_method : Proof.context > thm list * thm list > proof_method > int > tactic 
57720  40 
val thms_influence_proof_method : Proof.context > proof_method > thm list > bool 
55211  41 
val string_of_play_outcome : play_outcome > string 
55269  42 
val play_outcome_ord : play_outcome * play_outcome > order 
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

43 
val one_line_proof_text : Proof.context > int > one_line_params > string 
54495  44 
end; 
52555  45 

55287  46 
structure Sledgehammer_Proof_Methods : SLEDGEHAMMER_PROOF_METHODS = 
52555  47 
struct 
48 

54828  49 
open ATP_Util 
52555  50 
open ATP_Problem_Generate 
55211  51 
open ATP_Proof_Reconstruct 
52555  52 

55285  53 
datatype proof_method = 
54 
Metis_Method of string option * string option  

55 
Meson_Method  

58061  56 
SMT_Method  
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56093
diff
changeset

57 
SATx_Method  
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

58 
Blast_Method  
55285  59 
Simp_Method  
60 
Simp_Size_Method  

61 
Auto_Method  

58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

62 
Fastforce_Method  
55285  63 
Force_Method  
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

64 
Moura_Method  
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

65 
Linarith_Method  
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55315
diff
changeset

66 
Presburger_Method  
55285  67 
Algebra_Method 
52555  68 

54824  69 
datatype play_outcome = 
70 
Played of Time.time  

71 
Play_Timed_Out of Time.time  

56093  72 
Play_Failed 
52555  73 

57739  74 
type one_line_params = 
75 
((string * stature) list * (proof_method * play_outcome)) * string * int * int 

55211  76 

57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

77 
fun is_proof_method_direct (Metis_Method _) = true 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

78 
 is_proof_method_direct Meson_Method = true 
58061  79 
 is_proof_method_direct SMT_Method = true 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

80 
 is_proof_method_direct Simp_Method = true 
57465  81 
 is_proof_method_direct Simp_Size_Method = true 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

82 
 is_proof_method_direct _ = false 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

83 

60252
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

84 
fun proof_method_distinguishes_chained_and_direct Simp_Method = true 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

85 
 proof_method_distinguishes_chained_and_direct Simp_Size_Method = true 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

86 
 proof_method_distinguishes_chained_and_direct _ = false 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

87 

58499
094efe6ac459
don't affect other subgoals with 'auto' in oneliner proofs
blanchet
parents:
58092
diff
changeset

88 
fun is_proof_method_multi_goal Auto_Method = true 
094efe6ac459
don't affect other subgoals with 'auto' in oneliner proofs
blanchet
parents:
58092
diff
changeset

89 
 is_proof_method_multi_goal _ = false 
094efe6ac459
don't affect other subgoals with 'auto' in oneliner proofs
blanchet
parents:
58092
diff
changeset

90 

56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

91 
fun maybe_paren s = s > not (Symbol_Pos.is_identifier s) ? enclose "(" ")" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

92 

56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

93 
fun string_of_proof_method ctxt ss meth = 
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

94 
let 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

95 
val meth_s = 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

96 
(case meth of 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

97 
Metis_Method (NONE, NONE) => "metis" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

98 
 Metis_Method (type_enc_opt, lam_trans_opt) => 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

99 
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

100 
 Meson_Method => "meson" 
58061  101 
 SMT_Method => "smt" 
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

102 
 SATx_Method => "satx" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

103 
 Blast_Method => "blast" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

104 
 Simp_Method => if null ss then "simp" else "simp add:" 
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

105 
 Simp_Size_Method => "simp add: " ^ short_thm_name ctxt @{thm size_ne_size_imp_ne} 
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

106 
 Auto_Method => "auto" 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

107 
 Fastforce_Method => "fastforce" 
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

108 
 Force_Method => "force" 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

109 
 Moura_Method => "moura" 
56983
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

110 
 Linarith_Method => "linarith" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

111 
 Presburger_Method => "presburger" 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

112 
 Algebra_Method => "algebra") 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

113 
in 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

114 
maybe_paren (space_implode " " (meth_s :: ss)) 
132142089ea6
use 'simp add:' syntax in Sledgehammer rather than 'using'
blanchet
parents:
56965
diff
changeset

115 
end 
55285  116 

57054  117 
fun tac_of_proof_method ctxt (local_facts, global_facts) meth = 
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

118 
Method.insert_tac local_facts THEN' 
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

119 
(case meth of 
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

120 
Metis_Method (type_enc_opt, lam_trans_opt) => 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

121 
let val ctxt = Config.put Metis_Tactic.verbose false ctxt in 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

122 
Metis_Tactic.metis_tac [type_enc_opt > the_default (hd partial_type_encs)] 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

123 
(lam_trans_opt > the_default default_metis_lam_trans) ctxt global_facts 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

124 
end 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

125 
 Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts 
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

126 
 SMT_Method => SMT_Solver.smt_tac ctxt global_facts 
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

127 
 Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts) 
57465  128 
 Simp_Size_Method => 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

129 
Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts)) 
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

130 
 _ => 
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

131 
Method.insert_tac global_facts THEN' 
55285  132 
(case meth of 
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

133 
SATx_Method => SAT.satx_tac ctxt 
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

134 
 Blast_Method => blast_tac ctxt 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

135 
 Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt) 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

136 
 Fastforce_Method => Clasimp.fast_force_tac ctxt 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

137 
 Force_Method => Clasimp.force_tac ctxt 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

138 
 Moura_Method => moura_tac ctxt 
57290
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

139 
 Linarith_Method => 
bc06471cb7b7
move method silencing code closer to the methods it is trying to silence, to reduce bad sideeffects
blanchet
parents:
57287
diff
changeset

140 
let val ctxt = Config.put Lin_Arith.verbose false ctxt in Lin_Arith.tac ctxt end 
56965
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

141 
 Presburger_Method => Cooper.tac true [] [] ctxt 
222f46a4dbec
new approach to silence proof methods, to avoid weird theory/context mismatches
blanchet
parents:
56951
diff
changeset

142 
 Algebra_Method => Groebner.algebra_tac [] [] ctxt)) 
55211  143 

58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58075
diff
changeset

144 
val simp_based_methods = [Simp_Method, Simp_Size_Method, Auto_Method, Force_Method, Moura_Method] 
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset

145 

57720  146 
fun thms_influence_proof_method ctxt meth ths = 
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset

147 
not (member (op =) simp_based_methods meth) orelse 
58075
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

148 
(* unfortunate pointer comparison  but it's always safe to consider a theorem useful *) 
95bab16eac45
going back to bc06471cb7b7 for silencing  the bad side effects occurred only with 'smt', and the alternative silencing sometimes broke 'auto' etc.
blanchet
parents:
58074
diff
changeset

149 
not (pointer_eq (ctxt addsimps ths, ctxt)) 
57675
47336af5d2b2
faster minimization by not adding facts that are already in the simpset
blanchet
parents:
57674
diff
changeset

150 

54828  151 
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time) 
56093  152 
 string_of_play_outcome (Play_Timed_Out time) = 
153 
if time = Time.zeroTime then "" else string_of_ext_time (true, time) ^ ", timed out" 

54828  154 
 string_of_play_outcome Play_Failed = "failed" 
155 

55269  156 
fun play_outcome_ord (Played time1, Played time2) = 
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58499
diff
changeset

157 
int_ord (apply2 Time.toMilliseconds (time1, time2)) 
55269  158 
 play_outcome_ord (Played _, _) = LESS 
159 
 play_outcome_ord (_, Played _) = GREATER 

160 
 play_outcome_ord (Play_Timed_Out time1, Play_Timed_Out time2) = 

59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
58499
diff
changeset

161 
int_ord (apply2 Time.toMilliseconds (time1, time2)) 
55269  162 
 play_outcome_ord (Play_Timed_Out _, _) = LESS 
163 
 play_outcome_ord (_, Play_Timed_Out _) = GREATER 

164 
 play_outcome_ord (Play_Failed, Play_Failed) = EQUAL 

165 

55211  166 
fun apply_on_subgoal _ 1 = "by " 
167 
 apply_on_subgoal 1 _ = "apply " 

57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

168 
 apply_on_subgoal i n = "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n 
55211  169 

55285  170 
(* FIXME *) 
60252
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

171 
fun proof_method_command ctxt meth i n used_chaineds _(*num_chained*) extras = 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

172 
let 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

173 
val (indirect_ss, direct_ss) = 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

174 
if is_proof_method_direct meth then 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

175 
([], extras > proof_method_distinguishes_chained_and_direct meth ? append used_chaineds) 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

176 
else 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

177 
(extras, []) 
2c468c062589
improved oneline preplaying (don't rely on 'using x by simp' to mean 'by (simp add: x)' and beware of inaccessible '(local.)this')
blanchet
parents:
59058
diff
changeset

178 
in 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

179 
(if null indirect_ss then "" else "using " ^ space_implode " " indirect_ss ^ " ") ^ 
58499
094efe6ac459
don't affect other subgoals with 'auto' in oneliner proofs
blanchet
parents:
58092
diff
changeset

180 
apply_on_subgoal i n ^ string_of_proof_method ctxt direct_ss meth ^ 
094efe6ac459
don't affect other subgoals with 'auto' in oneliner proofs
blanchet
parents:
58092
diff
changeset

181 
(if is_proof_method_multi_goal meth andalso n <> 1 then "[1]" else "") 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57054
diff
changeset

182 
end 
55211  183 

56093  184 
fun try_command_line banner play command = 
185 
let val s = string_of_play_outcome play in 

186 
banner ^ ": " ^ Active.sendback_markup [Markup.padding_command] command ^ 

187 
(s > s <> "" ? enclose " (" ")") ^ "." 

188 
end 

52555  189 

56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

190 
fun one_line_proof_text ctxt num_chained 
57739  191 
((used_facts, (meth, play)), banner, subgoal, subgoal_count) = 
57777  192 
let val (chained, extra) = List.partition (fn (_, (sc, _)) => sc = Chained) used_facts in 
57735
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset

193 
map fst extra 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset

194 
> proof_method_command ctxt meth subgoal subgoal_count (map fst chained) num_chained 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset

195 
> (if play = Play_Failed then enclose "Oneline proof reconstruction failed: " "." 
056a55b44ec7
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
blanchet
parents:
57720
diff
changeset

196 
else try_command_line banner play) 
55211  197 
end 
52555  198 

54495  199 
end; 