author  blanchet 
Mon, 15 Sep 2014 12:30:06 +0200  
changeset 58341  6c8b30b9f583 
parent 58142  d6a2e3567f95 
child 58342  9a82544fd29f 
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 
55287  14 
type one_line_params = Sledgehammer_Proof_Methods.one_line_params 
49914  15 

55222  16 
val trace : bool Config.T 
17 

49914  18 
type isar_params = 
57783  19 
bool * (string option * string option) * Time.time * real option * bool * bool 
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset

20 
* (term, string) atp_step list * thm 
49914  21 

55296  22 
val proof_text : Proof.context > bool > bool option > bool option > (unit > isar_params) > 
23 
int > 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 
55287  34 
open Sledgehammer_Proof_Methods 
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 

57785  49 
val e_definition_rule = "definition" 
57654
f89c0749533d
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
blanchet
parents:
57288
diff
changeset

50 
val e_skolemize_rule = "skolemize" 
57759  51 
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" 
57709  52 
val satallax_skolemize_rule = "tab_ex" 
54836  53 
val spass_pirate_datatype_rule = "DT" 
54746  54 
val vampire_skolemisation_rule = "skolemisation" 
57761  55 
val veriT_la_generic_rule = "la_generic" 
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

56 
val veriT_simp_arith_rule = "simp_arith" 
57761  57 
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" 
58 
val veriT_tmp_skolemize_rule = "tmp_skolemize" 

58142  59 
val waldmeister_skolemize_rule = ATP_Waldmeister.waldmeister_skolemize_rule 
58061  60 
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize 
61 
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") 

57702
dfc834e39c1f
Skolemization support for leoII and Zipperposition.
fleury
parents:
57699
diff
changeset

62 
val zipperposition_cnf_rule = "cnf" 
54746  63 

54772  64 
val skolemize_rules = 
57785  65 
[e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, 
66 
spass_skolemize_rule, vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, 

58142  67 
veriT_tmp_skolemize_rule, waldmeister_skolemize_rule, z3_skolemize_rule, zipperposition_cnf_rule] 
54746  68 

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

69 
val is_skolemize_rule = member (op =) skolemize_rules 
57761  70 
fun is_arith_rule rule = 
57762  71 
String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse 
57761  72 
rule = veriT_la_generic_rule 
54836  73 
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule 
54755  74 

54501  75 
fun raw_label_of_num num = (num, 0) 
49914  76 

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

50005  79 

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

49914  82 

54799  83 
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = 
54770  84 
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or 
85 
definitions. *) 

57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

86 
if role = Conjecture orelse role = Negated_Conjecture then 
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

87 
line :: lines 
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

88 
else if t aconv @{prop True} then 
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

89 
map (replace_dependencies_in_line (name, [])) lines 
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset

90 
else if role = Lemma orelse role = Hypothesis orelse is_arith_rule rule then 
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

91 
line :: lines 
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

92 
else if role = Axiom then 
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset

93 
lines (* axioms (facts) need no proof lines *) 
57768
a63f14f1214c
finetuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset

94 
else 
a63f14f1214c
finetuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset

95 
map (replace_dependencies_in_line (name, [])) lines 
54755  96 
 add_line_pass1 line lines = line :: lines 
49914  97 

57771  98 
fun add_lines_pass2 res [] = rev res 
99 
 add_lines_pass2 res ((line as (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

100 
let 
57791  101 
fun normalize role = 
102 
role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) 

103 

57771  104 
val norm_t = normalize role t 
105 
val is_duplicate = 

106 
exists (fn (prev_name, prev_role, prev_t, _, _) => 

107 
member (op =) deps prev_name andalso 

108 
Term.aconv_untyped (normalize prev_role prev_t, norm_t)) 

109 
res 

57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

110 

57787  111 
fun looks_boring () = t aconv @{prop False} orelse length deps < 2 
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

112 

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

113 
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

114 
is_skolemize_rule rule' andalso member (op =) deps' name 
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

115 

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

116 
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

117 
in 
57771  118 
if is_duplicate orelse 
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

119 
(role = Plain andalso not (is_skolemize_rule rule) andalso 
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

120 
not (is_arith_rule rule) andalso not (is_datatype_rule rule) andalso 
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

121 
not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then 
57771  122 
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

123 
else 
57771  124 
add_lines_pass2 (line :: 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

125 
end 
49914  126 

127 
type isar_params = 

57783  128 
bool * (string option * string option) * Time.time * real option * bool * bool 
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset

129 
* (term, string) atp_step list * thm 
49914  130 

56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56130
diff
changeset

131 
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58083
diff
changeset

132 
val basic_simp_based_methods = [Auto_Method, Simp_Method, Fastforce_Method, Force_Method] 
55323
253a029335a2
split 'linarith' and 'presburger' (to avoid annoying warnings + to speed up reconstruction when 'presburger' is needed)
blanchet
parents:
55311
diff
changeset

133 
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] 
55311  134 

57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

135 
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods 
55311  136 
val datatype_methods = [Simp_Method, Simp_Size_Method] 
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

137 
val systematic_methods = 
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

138 
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ 
57699  139 
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] 
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

140 
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods 
58092
4ae52c60603a
renamed 'skolem' to 'moura' (to suggest Z3style skolemization); reintroduced 'fastforce' to the mix of tested proof methods
blanchet
parents:
58083
diff
changeset

141 
fun skolem_methods_of z3 = basic_systematic_methods > z3 ? cons Moura_Method 
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset

142 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

143 
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params 
57739  144 
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = 
49883  145 
let 
56097  146 
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () 
147 

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

148 
fun generate_proof_text () = 
49883  149 
let 
57791  150 
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = 
57245  151 
isar_params () 
55257  152 

57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

153 
val systematic_methods' = insert (op =) (Metis_Method alt_metis_args) systematic_methods 
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

154 

55311  155 
fun massage_methods (meths as meth :: _) = 
57245  156 
if not try0 then [meth] 
58061  157 
else if smt_proofs = SOME true then SMT_Method :: meths 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

158 
else meths 
55273  159 

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

160 
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt 
55264  161 
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params 
162 
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

163 

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

164 
val do_preplay = preplay_timeout <> Time.zeroTime 
57783  165 
val compress = 
166 
(case compress of 

167 
NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 

168 
 SOME n => n) 

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

169 

57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

170 
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem 
58341  171 
fun skolems_of ctxt t = Term.add_frees t [] > filter_out (is_fixed ctxt o fst) > rev 
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset

172 

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

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

174 
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

175 

49883  176 
val atp_proof = 
57791  177 
fold_rev add_line_pass1 atp_proof0 [] 
57771  178 
> add_lines_pass2 [] 
54700  179 

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

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

183 
atp_proof 

54751  184 
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof 
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

185 

ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

186 
fun add_lemma ((l, t), rule) ctxt = 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

187 
let 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

188 
val (skos, meths) = 
58077  189 
(if is_skolemize_rule rule then 
190 
(skolems_of ctxt t, skolem_methods_of (rule = z3_skolemize_rule)) 

191 
else if is_arith_rule rule then 

192 
([], arith_methods) 

193 
else 

194 
([], rewrite_methods)) 

57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

195 
> massage_methods 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

196 
in 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

197 
(Prove ([], skos, l, t, [], ([], []), meths, ""), 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

198 
ctxt > not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

199 
end 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

200 

ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

201 
val (lems, _) = 
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

202 
fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt 
54700  203 

57791  204 
val bot = #1 (List.last atp_proof) 
54700  205 

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

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

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

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

210 
> fold (Atom_Graph.default_node o rpair ()) conjs 
54700  211 

51145  212 
val axioms = axioms_of_refute_graph refute_graph conjs 
54700  213 

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

216 
val steps = 
49883  217 
Symtab.empty 
51201  218 
> fold (fn (name as (s, _), role, t, rule, _) => 
54758  219 
Symtab.update_new (s, (rule, t 
220 
> (if is_clause_tainted [name] then 

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

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

222 
#> role <> Conjecture ? s_not 
54758  223 
#> 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

224 
#> HOLogic.mk_Trueprop 
54758  225 
else 
226 
I)))) 

227 
atp_proof 

54700  228 

54755  229 
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst 
54700  230 

57768
a63f14f1214c
finetuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset

231 
val finish_off = close_form #> rename_bound_vars 
57765  232 

57767
5bc204ca27ce
centralized boolean simplification so that e.g. LEOII benefits from it
blanchet
parents:
57765
diff
changeset

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

235 
let 
57765  236 
val lits = 
237 
map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) 

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

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

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

243 
end 
57767
5bc204ca27ce
centralized boolean simplification so that e.g. LEOII benefits from it
blanchet
parents:
57765
diff
changeset

244 
> HOLogic.mk_Trueprop > finish_off 
54700  245 

58083  246 
fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] 
54700  247 

248 
fun isar_steps outer predecessor accum [] = 

249 
accum 

250 
> (if tainted = [] then 

58083  251 
(* e.g., trivial, empty proof by Z3 *) 
54700  252 
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], 
57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset

253 
sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) 
54700  254 
else 
255 
I) 

256 
> rev 

54755  257 
 isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = 
54700  258 
let 
259 
val l = label_of_clause c 

260 
val t = prop_of_clause c 

54755  261 
val rule = rule_of_clause_id id 
262 
val skolem = is_skolemize_rule rule 

263 

57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset

264 
val deps = ([], []) 
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset

265 
> fold add_fact_of_dependencies gamma 
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset

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

267 
val meths = 
58077  268 
(if skolem then skolem_methods_of (rule = z3_skolemize_rule) 
55273  269 
else if is_arith_rule rule then arith_methods 
270 
else if is_datatype_rule rule then datatype_methods 

57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset

271 
else systematic_methods') 
55311  272 
> massage_methods 
55280  273 

58083  274 
fun prove sub facts = Prove (maybe_show outer c, [], l, t, sub, facts, meths, "") 
55280  275 
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs 
54700  276 
in 
277 
if is_clause_tainted c then 

54712  278 
(case gamma of 
54700  279 
[g] => 
54755  280 
if skolem andalso is_clause_tainted g then 
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

281 
(case skolems_of ctxt (prop_of_clause g) of 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

282 
[] => steps_of_rest (prove [] deps) 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

283 
 skos => 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

284 
let val subproof = Proof (skos, [], rev accum) in 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

285 
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

286 
end) 
51148
2246a2e17f92
tuning  refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset

287 
else 
55280  288 
steps_of_rest (prove [] deps) 
289 
 _ => steps_of_rest (prove [] deps)) 

54700  290 
else 
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset

291 
steps_of_rest 
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

292 
(if skolem then 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

293 
(case skolems_of ctxt t of 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

294 
[] => prove [] deps 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

295 
 skos => Prove ([], skos, l, t, [], deps, meths, "")) 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

296 
else 
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEOII)
blanchet
parents:
57744
diff
changeset

297 
prove [] deps) 
54700  298 
end 
299 
 isar_steps outer predecessor accum (Cases cases :: infs) = 

300 
let 

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

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

302 
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs 
54700  303 
val c = succedent_of_cases cases 
304 
val l = label_of_clause c 

305 
val t = prop_of_clause c 

306 
val step = 

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

308 
map isar_case (filter_out (null o snd) cases), 
57776
1111a9a328fe
rationalized sorting of facts  so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset

309 
sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") 
54700  310 
in 
311 
isar_steps outer (SOME l) (step :: accum) infs 

312 
end 

313 
and isar_proof outer fix assms lems infs = 

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

315 

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

317 

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

320 
> 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

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

322 
> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) 
54754  323 
> isar_proof true params assms lems 
58083  324 
> postprocess_isar_proof_remove_show_stuttering 
55213  325 
> postprocess_isar_proof_remove_unreferenced_steps I 
326 
> relabel_isar_proof_canonically 

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

327 

55286  328 
val ctxt = ctxt > enrich_context_with_local_facts canonical_isar_proof 
55256  329 

55260  330 
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty 
331 

55264  332 
val _ = fold_isar_steps (fn meth => 
57054  333 
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) 
55260  334 
(steps_of_isar_proof canonical_isar_proof) () 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

335 

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

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

337 
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

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

339 
string_of_proof_method ctxt [] meth ^ " " ^ 
55266  340 
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

341 
fun comment_of l = map (str_of_meth l) #> commas 
55222  342 

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

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

344 
if trace then 
55299  345 
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ 
56097  346 
string_of_isar_proof ctxt subgoal subgoal_count 
347 
(comment_isar_proof comment_of proof) ^ "\n") 

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

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

349 
() 
54754  350 

55299  351 
fun comment_of l (meth :: _) = 
352 
(case (verbose, 

353 
Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of 

354 
(false, Played _) => "" 

355 
 (_, outcome) => string_of_play_outcome outcome) 

356 

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

359 
> tap (trace_isar_proof "Original") 
57245  360 
> compress_isar_proof ctxt compress preplay_timeout preplay_data 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

361 
> tap (trace_isar_proof "Compressed") 
55213  362 
> postprocess_isar_proof_remove_unreferenced_steps 
55266  363 
(keep_fastest_method_of_isar_step (!preplay_data) 
57054  364 
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data) 
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset

365 
> tap (trace_isar_proof "Minimized") 
55260  366 
> `(preplay_outcome_of_isar_proof (!preplay_data)) 
55325  367 
> (comment_isar_proof comment_of 
368 
#> chain_isar_proof 

369 
#> kill_useless_labels_in_isar_proof 

57792  370 
#> relabel_isar_proof_nicely 
371 
#> rationalize_obtains_in_isar_proofs ctxt) 

49883  372 
in 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

373 
(case add_isar_steps (steps_of_isar_proof isar_proof) 0 of 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

374 
1 => 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

375 
one_line_proof_text ctxt 0 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

376 
(if play_outcome_ord (play_outcome, one_line_play) = LESS then 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

377 
(case isar_proof of 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

378 
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

379 
let val used_facts' = filter (member (op =) gfs o fst) used_facts in 
57739  380 
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

381 
end) 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

382 
else 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

383 
one_line_params) ^ 
57780  384 
(if isar_proofs = SOME true then "\n(No Isar proof available.)" 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

385 
else "") 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

386 
 num_steps => 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

387 
let 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

388 
val msg = 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

389 
(if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

390 
(if do_preplay then [string_of_play_outcome play_outcome] else []) 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

391 
in 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

392 
one_line_proof_text ctxt 0 one_line_params ^ 
57780  393 
"\n\nIsar proof" ^ (commas msg > not (null msg) ? enclose " (" ")") ^ ":\n" ^ 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

394 
Active.sendback_markup [Markup.padding_command] 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

395 
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof) 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

396 
end) 
49883  397 
end 
57056  398 
in 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

399 
if debug then 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

400 
generate_proof_text () 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

401 
else 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

402 
(case try generate_proof_text () of 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

403 
SOME s => s 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

404 
 NONE => 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

405 
one_line_proof_text ctxt 0 one_line_params ^ 
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

406 
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")) 
57056  407 
end 
49883  408 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

409 
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = 
54824  410 
(case play of 
58061  411 
Played _ => meth = SMT_Method andalso smt_proofs <> SOME true 
56093  412 
 Play_Timed_Out time => Time.> (time, Time.zeroTime) 
413 
 Play_Failed => true) 

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

414 

55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

415 
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained 
57739  416 
(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

417 
(if isar_proofs = SOME true orelse 
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

418 
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then 
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset

419 
isar_proof_text ctxt debug isar_proofs smt_proofs isar_params 
49883  420 
else 
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset

421 
one_line_proof_text ctxt num_chained) one_line_params 
49883  422 

423 
end; 