author | blanchet |
Mon, 04 Aug 2014 13:16:18 +0200 | |
changeset 57780 | e1a3d025552d |
parent 57776 | 1111a9a328fe |
child 57783 | 2bf99b3f62e1 |
permissions | -rw-r--r-- |
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 Z3-specific 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 = |
55296 | 19 |
bool * (string option * string option) * Time.time * real * 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 Isar-proof 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 |
||
57654
f89c0749533d
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
blanchet
parents:
57288
diff
changeset
|
49 |
val e_skolemize_rule = "skolemize" |
57759 | 50 |
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
57709 | 51 |
val satallax_skolemize_rule = "tab_ex" |
54836 | 52 |
val spass_pirate_datatype_rule = "DT" |
54746 | 53 |
val vampire_skolemisation_rule = "skolemisation" |
57761 | 54 |
val veriT_la_generic_rule = "la_generic" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
55 |
val veriT_simp_arith_rule = "simp_arith" |
57761 | 56 |
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
57 |
val veriT_tmp_skolemize_rule = "tmp_skolemize" |
|
58 |
val z3_skolemize_rule = Z3_New_Proof.string_of_rule Z3_New_Proof.Skolemize |
|
57762 | 59 |
val z3_th_lemma_rule_prefix = Z3_New_Proof.string_of_rule (Z3_New_Proof.Th_Lemma "") |
57702
dfc834e39c1f
Skolemization support for leo-II and Zipperposition.
fleury
parents:
57699
diff
changeset
|
60 |
val zipperposition_cnf_rule = "cnf" |
54746 | 61 |
|
54772 | 62 |
val skolemize_rules = |
57759 | 63 |
[e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, spass_skolemize_rule, |
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
64 |
vampire_skolemisation_rule, veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule, z3_skolemize_rule, |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
65 |
zipperposition_cnf_rule] |
54746 | 66 |
|
54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset
|
67 |
val is_skolemize_rule = member (op =) skolemize_rules |
57761 | 68 |
fun is_arith_rule rule = |
57762 | 69 |
String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse |
57761 | 70 |
rule = veriT_la_generic_rule |
54836 | 71 |
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule |
54755 | 72 |
|
54501 | 73 |
fun raw_label_of_num num = (num, 0) |
49914 | 74 |
|
54501 | 75 |
fun label_of_clause [(num, _)] = raw_label_of_num num |
76 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
|
50005 | 77 |
|
54505 | 78 |
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) |
79 |
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) |
|
49914 | 80 |
|
54799 | 81 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
54770 | 82 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
83 |
definitions. *) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
84 |
if role = Conjecture orelse role = Negated_Conjecture then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
85 |
line :: lines |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
86 |
else if t aconv @{prop True} then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
87 |
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
|
88 |
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
|
89 |
line :: lines |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
90 |
else if role = Axiom then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
91 |
lines (* axioms (facts) need no proof lines *) |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
92 |
else |
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
93 |
map (replace_dependencies_in_line (name, [])) lines |
54755 | 94 |
| add_line_pass1 line lines = line :: lines |
49914 | 95 |
|
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset
|
96 |
fun normalize role = |
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset
|
97 |
role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) |
57771 | 98 |
|
99 |
fun add_lines_pass2 res [] = rev res |
|
100 |
| 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
|
101 |
let |
57771 | 102 |
val norm_t = normalize role t |
103 |
val is_duplicate = |
|
104 |
exists (fn (prev_name, prev_role, prev_t, _, _) => |
|
105 |
member (op =) deps prev_name andalso |
|
106 |
Term.aconv_untyped (normalize prev_role prev_t, norm_t)) |
|
107 |
res |
|
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
108 |
|
57657
6840b23da81d
refined filter for ATP steps to avoid 'have True' steps in E proofs
blanchet
parents:
57654
diff
changeset
|
109 |
fun looks_boring () = |
57771 | 110 |
t aconv @{prop True} orelse 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
|
111 |
|
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 |
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
|
113 |
is_skolemize_rule rule' andalso member (op =) deps' name |
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
114 |
|
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
|
115 |
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
|
116 |
in |
57771 | 117 |
if is_duplicate orelse |
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
118 |
(role = Plain andalso not (is_skolemize_rule rule) andalso |
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
119 |
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
|
120 |
not (null lines) andalso looks_boring () andalso not (is_before_skolemize_rule ())) then |
57771 | 121 |
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
|
122 |
else |
57771 | 123 |
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
|
124 |
end |
49914 | 125 |
|
126 |
type isar_params = |
|
55296 | 127 |
bool * (string option * string option) * Time.time * real * bool * bool |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
128 |
* (term, string) atp_step list * thm |
49914 | 129 |
|
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56130
diff
changeset
|
130 |
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] |
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
131 |
val basic_simp_based_methods = [Auto_Method, Simp_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
|
132 |
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] |
55311 | 133 |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
134 |
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods |
55311 | 135 |
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
|
136 |
val systematic_methods = |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
137 |
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
57699 | 138 |
[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
|
139 |
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
140 |
val skolem_methods = basic_systematic_methods @ [Auto_Choice_Method] |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
141 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
142 |
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
57739 | 143 |
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
49883 | 144 |
let |
56097 | 145 |
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |
146 |
||
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
147 |
fun generate_proof_text () = |
49883 | 148 |
let |
57245 | 149 |
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) = |
150 |
isar_params () |
|
55257 | 151 |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
152 |
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
|
153 |
|
55311 | 154 |
fun massage_methods (meths as meth :: _) = |
57245 | 155 |
if not try0 then [meth] |
56081 | 156 |
else if smt_proofs = SOME true then SMT2_Method :: meths |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
157 |
else meths |
55273 | 158 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
159 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
55264 | 160 |
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params |
161 |
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
|
162 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
163 |
val do_preplay = preplay_timeout <> Time.zeroTime |
57245 | 164 |
val compress = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
165 |
|
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
166 |
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
167 |
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
|
168 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
169 |
fun get_role keep_role ((num, _), role, t, rule, _) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
170 |
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
|
171 |
|
49883 | 172 |
val atp_proof = |
57769 | 173 |
fold_rev add_line_pass1 atp_proof [] |
57771 | 174 |
|> add_lines_pass2 [] |
54700 | 175 |
|
54535
59737a43e044
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents:
54507
diff
changeset
|
176 |
val conjs = |
54700 | 177 |
map_filter (fn (name, role, _, _, _) => |
178 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
179 |
atp_proof |
|
54751 | 180 |
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
|
181 |
|
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
182 |
fun add_lemma ((l, t), rule) ctxt = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
183 |
let |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
184 |
val (skos, meths) = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
185 |
(if is_skolemize_rule rule then (skolems_of ctxt t, skolem_methods) |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
186 |
else if is_arith_rule rule then ([], arith_methods) |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
187 |
else ([], rewrite_methods)) |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
188 |
||> massage_methods |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
189 |
in |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
190 |
(Prove ([], skos, l, t, [], ([], []), meths, ""), |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
191 |
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
|
192 |
end |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
193 |
|
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
194 |
val (lems, _) = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
195 |
fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt |
54700 | 196 |
|
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
197 |
val bot = atp_proof |> List.last |> #1 |
54700 | 198 |
|
51145 | 199 |
val refute_graph = |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
200 |
atp_proof |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
201 |
|> map (fn (name, _, _, _, from) => (from, name)) |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
202 |
|> make_refute_graph bot |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
203 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
54700 | 204 |
|
51145 | 205 |
val axioms = axioms_of_refute_graph refute_graph conjs |
54700 | 206 |
|
51145 | 207 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
51156 | 208 |
val is_clause_tainted = exists (member (op =) tainted) |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
209 |
val steps = |
49883 | 210 |
Symtab.empty |
51201 | 211 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
54758 | 212 |
Symtab.update_new (s, (rule, t |
213 |
|> (if is_clause_tainted [name] then |
|
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
214 |
HOLogic.dest_Trueprop |
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
215 |
#> role <> Conjecture ? s_not |
54758 | 216 |
#> 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
|
217 |
#> HOLogic.mk_Trueprop |
54758 | 218 |
else |
219 |
I)))) |
|
220 |
atp_proof |
|
54700 | 221 |
|
54755 | 222 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
54700 | 223 |
|
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
224 |
val finish_off = close_form #> rename_bound_vars |
57765 | 225 |
|
57767
5bc204ca27ce
centralized boolean simplification so that e.g. LEO-II benefits from it
blanchet
parents:
57765
diff
changeset
|
226 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off |
50016 | 227 |
| prop_of_clause names = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
228 |
let |
57765 | 229 |
val lits = |
230 |
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
|
231 |
in |
54754 | 232 |
(case List.partition (can HOLogic.dest_not) lits of |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
233 |
(negs as _ :: _, pos as _ :: _) => |
54507 | 234 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
54754 | 235 |
| _ => fold (curry s_disj) lits @{term False}) |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
236 |
end |
57767
5bc204ca27ce
centralized boolean simplification so that e.g. LEO-II benefits from it
blanchet
parents:
57765
diff
changeset
|
237 |
|> HOLogic.mk_Trueprop |> finish_off |
54700 | 238 |
|
55169 | 239 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show |
54700 | 240 |
|
241 |
fun isar_steps outer predecessor accum [] = |
|
242 |
accum |
|
243 |
|> (if tainted = [] then |
|
244 |
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
|
245 |
sort_facts (the_list predecessor, []), massage_methods systematic_methods', "")) |
54700 | 246 |
else |
247 |
I) |
|
248 |
|> rev |
|
54755 | 249 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
54700 | 250 |
let |
251 |
val l = label_of_clause c |
|
252 |
val t = prop_of_clause c |
|
54755 | 253 |
val rule = rule_of_clause_id id |
254 |
val skolem = is_skolemize_rule rule |
|
255 |
||
57776
1111a9a328fe
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
blanchet
parents:
57771
diff
changeset
|
256 |
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
|
257 |
|> 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
|
258 |
|> sort_facts |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
259 |
val meths = |
55273 | 260 |
(if skolem then skolem_methods |
261 |
else if is_arith_rule rule then arith_methods |
|
262 |
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
|
263 |
else systematic_methods') |
55311 | 264 |
|> massage_methods |
55280 | 265 |
|
55299 | 266 |
fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "") |
55280 | 267 |
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
54700 | 268 |
in |
269 |
if is_clause_tainted c then |
|
54712 | 270 |
(case gamma of |
54700 | 271 |
[g] => |
54755 | 272 |
if skolem andalso is_clause_tainted g then |
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
273 |
(case skolems_of ctxt (prop_of_clause g) of |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
274 |
[] => steps_of_rest (prove [] deps) |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
275 |
| skos => |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
276 |
let val subproof = Proof (skos, [], rev accum) in |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
277 |
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
278 |
end) |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
279 |
else |
55280 | 280 |
steps_of_rest (prove [] deps) |
281 |
| _ => steps_of_rest (prove [] deps)) |
|
54700 | 282 |
else |
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
283 |
steps_of_rest |
57758
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
284 |
(if skolem then |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
285 |
(case skolems_of ctxt t of |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
286 |
[] => prove [] deps |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
287 |
| skos => Prove ([], skos, l, t, [], deps, meths, "")) |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
288 |
else |
b2e6166bf487
beware of 'skolem' rules that do not skolemize (e.g. LEO-II)
blanchet
parents:
57744
diff
changeset
|
289 |
prove [] deps) |
54700 | 290 |
end |
291 |
| isar_steps outer predecessor accum (Cases cases :: infs) = |
|
292 |
let |
|
55186
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
293 |
fun isar_case (c, subinfs) = |
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
294 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
54700 | 295 |
val c = succedent_of_cases cases |
296 |
val l = label_of_clause c |
|
297 |
val t = prop_of_clause c |
|
298 |
val step = |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
299 |
Prove (maybe_show outer c [], [], l, t, |
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
300 |
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
|
301 |
sort_facts (the_list predecessor, []), massage_methods systematic_methods', "") |
54700 | 302 |
in |
303 |
isar_steps outer (SOME l) (step :: accum) infs |
|
304 |
end |
|
305 |
and isar_proof outer fix assms lems infs = |
|
306 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
|
307 |
||
55222 | 308 |
val trace = Config.get ctxt trace |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
309 |
|
55256 | 310 |
val canonical_isar_proof = |
51145 | 311 |
refute_graph |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
312 |
|> 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
|
313 |
|> redirect_graph axioms tainted bot |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
314 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
54754 | 315 |
|> isar_proof true params assms lems |
55213 | 316 |
|> postprocess_isar_proof_remove_unreferenced_steps I |
317 |
|> relabel_isar_proof_canonically |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
318 |
|
55286 | 319 |
val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
55256 | 320 |
|
55260 | 321 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
322 |
||
55264 | 323 |
val _ = fold_isar_steps (fn meth => |
57054 | 324 |
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) |
55260 | 325 |
(steps_of_isar_proof canonical_isar_proof) () |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
326 |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
327 |
fun str_of_preplay_outcome outcome = |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
328 |
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
|
329 |
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
|
330 |
string_of_proof_method ctxt [] meth ^ " " ^ |
55266 | 331 |
str_of_preplay_outcome (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
332 |
fun comment_of l = map (str_of_meth l) #> commas |
55222 | 333 |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
334 |
fun trace_isar_proof label proof = |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
335 |
if trace then |
55299 | 336 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ |
56097 | 337 |
string_of_isar_proof ctxt subgoal subgoal_count |
338 |
(comment_isar_proof comment_of proof) ^ "\n") |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
339 |
else |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
340 |
() |
54754 | 341 |
|
55299 | 342 |
fun comment_of l (meth :: _) = |
343 |
(case (verbose, |
|
344 |
Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of |
|
345 |
(false, Played _) => "" |
|
346 |
| (_, outcome) => string_of_play_outcome outcome) |
|
347 |
||
54828 | 348 |
val (play_outcome, isar_proof) = |
55256 | 349 |
canonical_isar_proof |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
350 |
|> tap (trace_isar_proof "Original") |
57245 | 351 |
|> compress_isar_proof ctxt compress preplay_timeout preplay_data |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
352 |
|> tap (trace_isar_proof "Compressed") |
55213 | 353 |
|> postprocess_isar_proof_remove_unreferenced_steps |
55266 | 354 |
(keep_fastest_method_of_isar_step (!preplay_data) |
57054 | 355 |
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
356 |
|> tap (trace_isar_proof "Minimized") |
57245 | 357 |
(* It's not clear whether this is worth the trouble (and if so, "compress" has an |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55327
diff
changeset
|
358 |
unnatural semantics): *) |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55327
diff
changeset
|
359 |
(* |
55327
3c7f3122ccdc
do a second phase of proof compression after minimization
blanchet
parents:
55325
diff
changeset
|
360 |
|> minimize |
57245 | 361 |
? (compress_isar_proof ctxt compress preplay_timeout preplay_data |
55327
3c7f3122ccdc
do a second phase of proof compression after minimization
blanchet
parents:
55325
diff
changeset
|
362 |
#> tap (trace_isar_proof "Compressed again")) |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55327
diff
changeset
|
363 |
*) |
55260 | 364 |
|> `(preplay_outcome_of_isar_proof (!preplay_data)) |
55325 | 365 |
||> (comment_isar_proof comment_of |
366 |
#> chain_isar_proof |
|
367 |
#> kill_useless_labels_in_isar_proof |
|
57765 | 368 |
#> relabel_isar_proof_nicely) |
49883 | 369 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
370 |
(case add_isar_steps (steps_of_isar_proof isar_proof) 0 of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
371 |
1 => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
372 |
one_line_proof_text ctxt 0 |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
373 |
(if play_outcome_ord (play_outcome, one_line_play) = LESS then |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
374 |
(case isar_proof of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
375 |
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
376 |
let val used_facts' = filter (member (op =) gfs o fst) used_facts in |
57739 | 377 |
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
378 |
end) |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
379 |
else |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
380 |
one_line_params) ^ |
57780 | 381 |
(if isar_proofs = SOME true then "\n(No Isar proof available.)" |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
382 |
else "") |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
383 |
| num_steps => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
384 |
let |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
385 |
val msg = |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
386 |
(if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] else []) @ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
387 |
(if do_preplay then [string_of_play_outcome play_outcome] else []) |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
388 |
in |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
389 |
one_line_proof_text ctxt 0 one_line_params ^ |
57780 | 390 |
"\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
391 |
Active.sendback_markup [Markup.padding_command] |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
392 |
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof) |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
393 |
end) |
49883 | 394 |
end |
57056 | 395 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
396 |
if debug then |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
397 |
generate_proof_text () |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
398 |
else |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
399 |
(case try generate_proof_text () of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
400 |
SOME s => s |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
401 |
| NONE => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
402 |
one_line_proof_text ctxt 0 one_line_params ^ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
403 |
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")) |
57056 | 404 |
end |
49883 | 405 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
406 |
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = |
54824 | 407 |
(case play of |
56081 | 408 |
Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true |
56093 | 409 |
| Play_Timed_Out time => Time.> (time, Time.zeroTime) |
410 |
| 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
|
411 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
412 |
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
57739 | 413 |
(one_line_params as ((_, preplay), _, _, _)) = |
51190
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
414 |
(if isar_proofs = SOME true orelse |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
415 |
(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
|
416 |
isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
49883 | 417 |
else |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
418 |
one_line_proof_text ctxt num_chained) one_line_params |
49883 | 419 |
|
420 |
end; |