author  blanchet 
Mon, 03 Feb 2014 10:14:18 +0100  
changeset 55273  e887c0743614 
parent 55267  e68fd012bbf3 
child 55274  b84867d6550b 
permissions  rwrr 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML 
49883  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Author: Steffen Juilf Smolka, TU Muenchen 

4 

49914  5 
Isar proof reconstruction from ATP proofs. 
49883  6 
*) 
7 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

8 
signature SLEDGEHAMMER_ISAR = 
49883  9 
sig 
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3specific code)
blanchet
parents:
54770
diff
changeset

10 
type atp_step_name = ATP_Proof.atp_step_name 
54495  11 
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step 
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset

12 
type 'a atp_proof = 'a ATP_Proof.atp_proof 
49914  13 
type stature = ATP_Problem_Generate.stature 
54495  14 
type one_line_params = Sledgehammer_Reconstructor.one_line_params 
49914  15 

55222  16 
val trace : bool Config.T 
17 

49914  18 
type isar_params = 
55267  19 
bool * (string option * string option) * Time.time * real * bool * bool 
55257  20 
* (term, string) atp_step list * thm 
49914  21 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

22 
val proof_text : Proof.context > bool > bool option > (unit > isar_params) > int > 
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset

23 
one_line_params > string 
49883  24 
end; 
25 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

26 
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = 
49883  27 
struct 
28 

29 
open ATP_Util 

49914  30 
open ATP_Problem 
49883  31 
open ATP_Proof 
32 
open ATP_Proof_Reconstruct 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

33 
open Sledgehammer_Util 
52555  34 
open Sledgehammer_Reconstructor 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

35 
open Sledgehammer_Isar_Proof 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

36 
open Sledgehammer_Isar_Preplay 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

37 
open Sledgehammer_Isar_Compress 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

38 
open Sledgehammer_Isar_Minimize 
49914  39 

40 
structure String_Redirect = ATP_Proof_Redirect( 

53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset

41 
type key = atp_step_name 
49914  42 
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') 
43 
val string_of = fst) 

44 

49883  45 
open String_Redirect 
46 

55222  47 
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false) 
48 

54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset

49 
val e_skolemize_rules = ["skolemize", "shift_quantors"] 
54836  50 
val spass_pirate_datatype_rule = "DT" 
54746  51 
val vampire_skolemisation_rule = "skolemisation" 
52 
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) 

54753  53 
val z3_skolemize_rule = "sk" 
54 
val z3_th_lemma_rule = "thlemma" 

54746  55 

54772  56 
val skolemize_rules = 
57 
e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] 

54746  58 

54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset

59 
val is_skolemize_rule = member (op =) skolemize_rules 
54755  60 
val is_arith_rule = String.isPrefix z3_th_lemma_rule 
54836  61 
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule 
54755  62 

54501  63 
fun raw_label_of_num num = (num, 0) 
49914  64 

54501  65 
fun label_of_clause [(num, _)] = raw_label_of_num num 
66 
 label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) 

50005  67 

54505  68 
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) 
69 
 add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) 

49914  70 

54758  71 
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) 
72 
fun is_only_type_information t = t aconv @{prop True} 

73 

74 
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in 

54759  75 
type information. *) 
54799  76 
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = 
54770  77 
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or 
78 
definitions. *) 

54700  79 
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse 
54755  80 
role = Hypothesis orelse is_arith_rule rule then 
54746  81 
line :: lines 
54505  82 
else if role = Axiom then 
49914  83 
(* Facts are not proof lines. *) 
54507  84 
lines > is_only_type_information t ? map (replace_dependencies_in_line (name, [])) 
49914  85 
else 
86 
map (replace_dependencies_in_line (name, [])) lines 

54755  87 
 add_line_pass1 line lines = line :: lines 
49914  88 

55191  89 
fun add_lines_pass2 res [] = rev res 
90 
 add_lines_pass2 res ((name, role, t, rule, deps) :: lines) = 

55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

91 
let 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

92 
val is_last_line = null lines 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

93 

6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

94 
fun looks_interesting () = 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

95 
not (is_only_type_information t) andalso null (Term.add_tvars t []) 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

96 
andalso length deps >= 2 andalso not (can the_single lines) 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

97 

6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

98 
fun is_skolemizing_line (_, _, _, rule', deps') = 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

99 
is_skolemize_rule rule' andalso member (op =) deps' name 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

100 
fun is_before_skolemize_rule () = exists is_skolemizing_line lines 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

101 
in 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

102 
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

103 
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse 
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

104 
is_before_skolemize_rule () then 
55191  105 
add_lines_pass2 ((name, role, t, rule, deps) :: res) lines 
55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

106 
else 
55191  107 
add_lines_pass2 res (map (replace_dependencies_in_line (name, deps)) lines) 
55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

108 
end 
49914  109 

110 
type isar_params = 

55267  111 
bool * (string option * string option) * Time.time * real * bool * bool 
112 
* (term, string) atp_step list * thm 

49914  113 

55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

114 
val arith_methods = 
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

115 
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, 
55257  116 
Algebra_Method, Metis_Method (NONE, NONE), Meson_Method] 
55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

117 
val datatype_methods = [Simp_Method, Simp_Size_Method] 
55257  118 
val metislike_methods0 = 
119 
[Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method, 

120 
Fastforce_Method, Force_Method, Algebra_Method, Meson_Method] 

55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

121 
val rewrite_methods = 
55257  122 
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE), 
123 
Meson_Method] 

124 
val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method] 

54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset

125 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

126 
fun isar_proof_text ctxt debug isar_proofs isar_params 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

127 
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = 
49883  128 
let 
129 
fun isar_proof_of () = 

130 
let 

55267  131 
val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, minimize, 
132 
atp_proof, goal) = try isar_params () 

55257  133 

134 
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

135 

55273  136 
val massage_meths = not try0_isar ? single o hd 
137 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

138 
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt 
55264  139 
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params 
140 
val ctxt = ctxt > Variable.set_body false > Proof_Context.add_fixes fixes > snd 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

141 

948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

142 
val do_preplay = preplay_timeout <> Time.zeroTime 
55253  143 
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar 
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

144 

948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

145 
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem 
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

146 
fun skolems_of t = Term.add_frees t [] > filter_out (is_fixed o fst) > rev 
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

147 

948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

148 
fun get_role keep_role ((num, _), role, t, rule, _) = 
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

149 
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE 
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

150 

49883  151 
val atp_proof = 
152 
atp_proof 

54755  153 
> rpair [] > fold_rev add_line_pass1 
55191  154 
> add_lines_pass2 [] 
54700  155 

54535
59737a43e044
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents:
54507
diff
changeset

156 
val conjs = 
54700  157 
map_filter (fn (name, role, _, _, _) => 
158 
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) 

159 
atp_proof 

54751  160 
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof 
54700  161 
val lems = 
162 
map_filter (get_role (curry (op =) Lemma)) atp_proof 

54751  163 
> map (fn ((l, t), rule) => 
54753  164 
let 
55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

165 
val (skos, meths) = 
55273  166 
(if is_skolemize_rule rule then (skolems_of t, skolem_methods) 
167 
else if is_arith_rule rule then ([], arith_methods) 

168 
else ([], rewrite_methods)) 

169 
> massage_meths 

54753  170 
in 
55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

171 
Prove ([], skos, l, t, [], (([], []), meths)) 
54753  172 
end) 
54700  173 

51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph  to prevent exceptions later
blanchet
parents:
51208
diff
changeset

174 
val bot = atp_proof > List.last > #1 
54700  175 

51145  176 
val refute_graph = 
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph  to prevent exceptions later
blanchet
parents:
51208
diff
changeset

177 
atp_proof 
2bbcc9cc12b4
ensure all conjecture clauses are in the graph  to prevent exceptions later
blanchet
parents:
51208
diff
changeset

178 
> map (fn (name, _, _, _, from) => (from, name)) 
2bbcc9cc12b4
ensure all conjecture clauses are in the graph  to prevent exceptions later
blanchet
parents:
51208
diff
changeset

179 
> make_refute_graph bot 
2bbcc9cc12b4
ensure all conjecture clauses are in the graph  to prevent exceptions later
blanchet
parents:
51208
diff
changeset

180 
> fold (Atom_Graph.default_node o rpair ()) conjs 
54700  181 

51145  182 
val axioms = axioms_of_refute_graph refute_graph conjs 
54700  183 

51145  184 
val tainted = tainted_atoms_of_refute_graph refute_graph conjs 
51156  185 
val is_clause_tainted = exists (member (op =) tainted) 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

186 
val steps = 
49883  187 
Symtab.empty 
51201  188 
> fold (fn (name as (s, _), role, t, rule, _) => 
54758  189 
Symtab.update_new (s, (rule, t 
190 
> (if is_clause_tainted [name] then 

54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset

191 
HOLogic.dest_Trueprop 
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset

192 
#> role <> Conjecture ? s_not 
54758  193 
#> fold exists_of (map Var (Term.add_vars t [])) 
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset

194 
#> HOLogic.mk_Trueprop 
54758  195 
else 
196 
I)))) 

197 
atp_proof 

54700  198 

54755  199 
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst 
54700  200 

54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54756
diff
changeset

201 
fun prop_of_clause [(num, _)] = Symtab.lookup steps num > the > snd > close_form 
50016  202 
 prop_of_clause names = 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

203 
let 
54758  204 
val lits = map (HOLogic.dest_Trueprop o snd) 
205 
(map_filter (Symtab.lookup steps o fst) names) 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

206 
in 
54754  207 
(case List.partition (can HOLogic.dest_not) lits of 
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

208 
(negs as _ :: _, pos as _ :: _) => 
54507  209 
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) 
54754  210 
 _ => fold (curry s_disj) lits @{term False}) 
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

211 
end 
50016  212 
> HOLogic.mk_Trueprop > close_form 
54700  213 

55169  214 
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show 
54700  215 

216 
fun isar_steps outer predecessor accum [] = 

217 
accum 

218 
> (if tainted = [] then 

219 
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], 

55273  220 
((the_list predecessor, []), massage_meths metislike_methods))) 
54700  221 
else 
222 
I) 

223 
> rev 

54755  224 
 isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = 
54700  225 
let 
226 
val l = label_of_clause c 

227 
val t = prop_of_clause c 

54755  228 
val rule = rule_of_clause_id id 
229 
val skolem = is_skolemize_rule rule 

230 

54700  231 
fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by) 
232 
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs 

54755  233 

234 
val deps = fold add_fact_of_dependencies gamma no_facts 

55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

235 
val meths = 
55273  236 
(if skolem then skolem_methods 
237 
else if is_arith_rule rule then arith_methods 

238 
else if is_datatype_rule rule then datatype_methods 

239 
else metislike_methods) 

240 
> massage_meths 

55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

241 
val by = (deps, meths) 
54700  242 
in 
243 
if is_clause_tainted c then 

54712  244 
(case gamma of 
54700  245 
[g] => 
54755  246 
if skolem andalso is_clause_tainted g then 
54751  247 
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in 
55245  248 
isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs 
54700  249 
end 
51148
2246a2e17f92
tuning  refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset

250 
else 
54700  251 
do_rest l (prove [] by) 
54712  252 
 _ => do_rest l (prove [] by)) 
54700  253 
else 
54765  254 
do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) 
54700  255 
end 
256 
 isar_steps outer predecessor accum (Cases cases :: infs) = 

257 
let 

55186
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset

258 
fun isar_case (c, subinfs) = 
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset

259 
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs 
54700  260 
val c = succedent_of_cases cases 
261 
val l = label_of_clause c 

262 
val t = prop_of_clause c 

263 
val step = 

54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset

264 
Prove (maybe_show outer c [], [], l, t, 
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset

265 
map isar_case (filter_out (null o snd) cases), 
55273  266 
((the_list predecessor, []), massage_meths metislike_methods)) 
54700  267 
in 
268 
isar_steps outer (SOME l) (step :: accum) infs 

269 
end 

270 
and isar_proof outer fix assms lems infs = 

271 
Proof (fix, assms, lems @ isar_steps outer NONE [] infs) 

272 

55257  273 
val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

274 

55222  275 
val trace = Config.get ctxt trace 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

276 

55256  277 
val canonical_isar_proof = 
51145  278 
refute_graph 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

279 
> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph) 
51031
63d71b247323
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents:
51026
diff
changeset

280 
> redirect_graph axioms tainted bot 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

281 
> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) 
54754  282 
> isar_proof true params assms lems 
55213  283 
> postprocess_isar_proof_remove_unreferenced_steps I 
284 
> relabel_isar_proof_canonically 

55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

285 

55264  286 
val ctxt = ctxt 
55256  287 
> enrich_context_with_local_facts canonical_isar_proof 
288 
> silence_reconstructors debug 

289 

55260  290 
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty 
291 

55264  292 
val _ = fold_isar_steps (fn meth => 
293 
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) 

55260  294 
(steps_of_isar_proof canonical_isar_proof) () 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

295 

55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

296 
fun str_of_preplay_outcome outcome = 
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

297 
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" 
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

298 

3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset

299 
fun str_of_meth l meth = 
55260  300 
string_of_proof_method meth ^ " " ^ 
55266  301 
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) 
55244
12e1a5d8ee48
simplified data structure  eliminated distinction between 'firstclass' and 'secondclass' proof methods
blanchet
parents:
55223
diff
changeset

302 
fun comment_of l = map (str_of_meth l) #> commas 
55222  303 

55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

304 
fun trace_isar_proof label proof = 
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

305 
if trace then 
55222  306 
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^ 
307 
"\n") 

55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

308 
else 
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

309 
() 
54754  310 

54828  311 
val (play_outcome, isar_proof) = 
55256  312 
canonical_isar_proof 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

313 
> tap (trace_isar_proof "Original") 
55264  314 
> compress_isar_proof ctxt compress_isar preplay_data 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

315 
> tap (trace_isar_proof "Compressed") 
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

316 
> tap (trace_isar_proof "Tried0") 
55213  317 
> postprocess_isar_proof_remove_unreferenced_steps 
55266  318 
(keep_fastest_method_of_isar_step (!preplay_data) 
55267  319 
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data) 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

320 
> tap (trace_isar_proof "Minimized") 
55260  321 
> `(preplay_outcome_of_isar_proof (!preplay_data)) 
55220  322 
> chain_isar_proof 
323 
> kill_useless_labels_in_isar_proof 

324 
> relabel_isar_proof_finally 

49883  325 
in 
55222  326 
(case string_of_isar_proof (K (K "")) isar_proof of 
49883  327 
"" => 
55213  328 
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." 
329 
else "" 

55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

330 
 isar_text => 
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

331 
let 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

332 
val msg = 
51203  333 
(if verbose then 
55260  334 
let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in 
55213  335 
[string_of_int num_steps ^ " step" ^ plural_s num_steps] 
336 
end 

51203  337 
else 
338 
[]) @ 

54828  339 
(if do_preplay then [string_of_play_outcome play_outcome] else []) 
50277  340 
in 
54507  341 
"\n\nStructured proof" ^ (commas msg > not (null msg) ? enclose " (" ")") ^ ":\n" ^ 
342 
Active.sendback_markup [Markup.padding_command] isar_text 

54754  343 
end) 
49883  344 
end 
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset

345 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

346 
val one_line_proof = one_line_proof_text 0 one_line_params 
49883  347 
val isar_proof = 
348 
if debug then 

349 
isar_proof_of () 

54754  350 
else 
351 
(case try isar_proof_of () of 

352 
SOME s => s 

353 
 NONE => 

354 
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") 

49883  355 
in one_line_proof ^ isar_proof end 
356 

54824  357 
fun isar_proof_would_be_a_good_idea (reconstr, play) = 
358 
(case play of 

359 
Played _ => reconstr = SMT 

54823  360 
 Play_Timed_Out _ => true 
54824  361 
 Play_Failed => true 
362 
 Not_Played => false) 

51187
c344cf148e8f
avoid using "smt" for minimization  better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof  and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset

363 

55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

364 
fun proof_text ctxt debug isar_proofs isar_params num_chained 
55256  365 
(one_line_params as (preplay, _, _, _, _, _)) = 
51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset

366 
(if isar_proofs = SOME true orelse 
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset

367 
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then 
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

368 
isar_proof_text ctxt debug isar_proofs isar_params 
49883  369 
else 
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications  oldstyle inline replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset

370 
one_line_proof_text num_chained) one_line_params 
49883  371 

372 
end; 