author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57739 | b6af899a78ac |
parent 57735 | 056a55b44ec7 |
child 57741 | a35d2d26d66e |
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" |
57702
dfc834e39c1f
Skolemization support for leo-II and Zipperposition.
fleury
parents:
57699
diff
changeset
|
50 |
val leo2_extcnf_combined_rule = "extcnf_combined" |
57709 | 51 |
val satallax_skolemize_rule = "tab_ex" |
54836 | 52 |
val spass_pirate_datatype_rule = "DT" |
54746 | 53 |
val vampire_skolemisation_rule = "skolemisation" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
54 |
val veriT_tmp_skolemize_rule = "tmp_skolemize" |
57715
cf8e4b1acd33
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
fleury
parents:
57714
diff
changeset
|
55 |
val veriT_tmp_ite_elim_rule = "tmp_ite_elim" |
cf8e4b1acd33
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
fleury
parents:
57714
diff
changeset
|
56 |
val veriT_skolemize_rules = [veriT_tmp_ite_elim_rule, veriT_tmp_skolemize_rule] |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
57 |
val veriT_simp_arith_rule = "simp_arith" |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
58 |
val veriT_la_generic_rule = "la_generic" |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
59 |
val veriT_arith_rules = [veriT_simp_arith_rule, veriT_la_generic_rule] |
54746 | 60 |
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
54753 | 61 |
val z3_skolemize_rule = "sk" |
62 |
val z3_th_lemma_rule = "th-lemma" |
|
57702
dfc834e39c1f
Skolemization support for leo-II and Zipperposition.
fleury
parents:
57699
diff
changeset
|
63 |
val zipperposition_cnf_rule = "cnf" |
54746 | 64 |
|
54772 | 65 |
val skolemize_rules = |
57713 | 66 |
[e_skolemize_rule, leo2_extcnf_combined_rule, satallax_skolemize_rule, spass_skolemize_rule, |
57715
cf8e4b1acd33
Skolemization for tmp_ite_elim rule in the SMT solver veriT.
fleury
parents:
57714
diff
changeset
|
67 |
vampire_skolemisation_rule, z3_skolemize_rule, zipperposition_cnf_rule] @ veriT_skolemize_rules |
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 |
57714
4856a7b8b9c3
Changing the role of rule "tmp_ite_elim" of the SMT solver veriT to Lemma.
fleury
parents:
57713
diff
changeset
|
70 |
val is_arith_rule = String.isPrefix z3_th_lemma_rule orf member (op =) veriT_arith_rules |
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 *) |
57056 | 92 |
else map (replace_dependencies_in_line (name, [])) lines |
54755 | 93 |
| add_line_pass1 line lines = line :: lines |
49914 | 94 |
|
56130
1ef77430713b
consolidate consecutive steps that prove the same formula
blanchet
parents:
56128
diff
changeset
|
95 |
fun add_lines_pass2 res _ [] = rev res |
1ef77430713b
consolidate consecutive steps that prove the same formula
blanchet
parents:
56128
diff
changeset
|
96 |
| add_lines_pass2 res prev_t ((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
|
97 |
let |
57657
6840b23da81d
refined filter for ATP steps to avoid 'have True' steps in E proofs
blanchet
parents:
57654
diff
changeset
|
98 |
fun looks_boring () = |
6840b23da81d
refined filter for ATP steps to avoid 'have True' steps in E proofs
blanchet
parents:
57654
diff
changeset
|
99 |
t aconv @{prop True} orelse t aconv @{prop False} orelse t aconv prev_t orelse |
6840b23da81d
refined filter for ATP steps to avoid 'have True' steps in E proofs
blanchet
parents:
57654
diff
changeset
|
100 |
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
|
101 |
|
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 |
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
|
103 |
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
|
104 |
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
|
105 |
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
|
106 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse |
57657
6840b23da81d
refined filter for ATP steps to avoid 'have True' steps in E proofs
blanchet
parents:
57654
diff
changeset
|
107 |
is_datatype_rule rule orelse null lines orelse not (looks_boring ()) orelse |
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 |
is_before_skolemize_rule () then |
56130
1ef77430713b
consolidate consecutive steps that prove the same formula
blanchet
parents:
56128
diff
changeset
|
109 |
add_lines_pass2 (line :: res) t 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
|
110 |
else |
56130
1ef77430713b
consolidate consecutive steps that prove the same formula
blanchet
parents:
56128
diff
changeset
|
111 |
add_lines_pass2 res t (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
|
112 |
end |
49914 | 113 |
|
114 |
type isar_params = |
|
55296 | 115 |
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
|
116 |
* (term, string) atp_step list * thm |
49914 | 117 |
|
56852
b38c5b9cf590
added 'satx' to Sledgehammer's portfolio (cf. 'isar_try0')
blanchet
parents:
56130
diff
changeset
|
118 |
val basic_systematic_methods = [Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method] |
56097 | 119 |
val 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
|
120 |
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] |
55311 | 121 |
|
122 |
val arith_methods = basic_arith_methods @ simp_based_methods @ basic_systematic_methods |
|
123 |
val datatype_methods = [Simp_Method, Simp_Size_Method] |
|
124 |
val systematic_methods0 = basic_systematic_methods @ basic_arith_methods @ simp_based_methods @ |
|
57699 | 125 |
[Metis_Method (SOME full_typesN, NONE), Metis_Method (SOME no_typesN, NONE)] |
55311 | 126 |
val rewrite_methods = simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
127 |
val skolem_methods = basic_systematic_methods |
|
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
128 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
129 |
fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
57739 | 130 |
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
49883 | 131 |
let |
56097 | 132 |
val _ = if debug then Output.urgent_message "Constructing Isar proof..." else () |
133 |
||
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
134 |
fun generate_proof_text () = |
49883 | 135 |
let |
57245 | 136 |
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof, goal) = |
137 |
isar_params () |
|
55257 | 138 |
|
55311 | 139 |
val systematic_methods = insert (op =) (Metis_Method alt_metis_args) systematic_methods0 |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
140 |
|
55311 | 141 |
fun massage_methods (meths as meth :: _) = |
57245 | 142 |
if not try0 then [meth] |
56081 | 143 |
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
|
144 |
else meths |
55273 | 145 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
146 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
55264 | 147 |
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params |
148 |
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
|
149 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
150 |
val do_preplay = preplay_timeout <> Time.zeroTime |
57245 | 151 |
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
|
152 |
|
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
153 |
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
|
154 |
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
|
155 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
156 |
fun get_role keep_role ((num, _), role, t, rule, _) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
157 |
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
|
158 |
|
49883 | 159 |
val atp_proof = |
160 |
atp_proof |
|
54755 | 161 |
|> rpair [] |-> fold_rev add_line_pass1 |
56130
1ef77430713b
consolidate consecutive steps that prove the same formula
blanchet
parents:
56128
diff
changeset
|
162 |
|> add_lines_pass2 [] Term.dummy |
54700 | 163 |
|
54535
59737a43e044
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents:
54507
diff
changeset
|
164 |
val conjs = |
54700 | 165 |
map_filter (fn (name, role, _, _, _) => |
166 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
167 |
atp_proof |
|
54751 | 168 |
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
|
169 |
|
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
170 |
fun add_lemma ((l, t), rule) ctxt = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
171 |
let |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
172 |
val (skos, meths) = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
173 |
(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
|
174 |
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
|
175 |
else ([], rewrite_methods)) |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
176 |
||> massage_methods |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
177 |
in |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
178 |
(Prove ([], skos, l, t, [], ([], []), meths, ""), |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
179 |
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
|
180 |
end |
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 |
val (lems, _) = |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
183 |
fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt |
54700 | 184 |
|
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
185 |
val bot = atp_proof |> List.last |> #1 |
54700 | 186 |
|
51145 | 187 |
val refute_graph = |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
188 |
atp_proof |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
189 |
|> map (fn (name, _, _, _, from) => (from, name)) |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
190 |
|> make_refute_graph bot |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
191 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
54700 | 192 |
|
51145 | 193 |
val axioms = axioms_of_refute_graph refute_graph conjs |
54700 | 194 |
|
51145 | 195 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
51156 | 196 |
val is_clause_tainted = exists (member (op =) tainted) |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
197 |
val steps = |
49883 | 198 |
Symtab.empty |
51201 | 199 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
54758 | 200 |
Symtab.update_new (s, (rule, t |
201 |
|> (if is_clause_tainted [name] then |
|
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
202 |
HOLogic.dest_Trueprop |
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
203 |
#> role <> Conjecture ? s_not |
54758 | 204 |
#> 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
|
205 |
#> HOLogic.mk_Trueprop |
54758 | 206 |
else |
207 |
I)))) |
|
208 |
atp_proof |
|
54700 | 209 |
|
54755 | 210 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
54700 | 211 |
|
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54756
diff
changeset
|
212 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form |
50016 | 213 |
| prop_of_clause names = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
214 |
let |
54758 | 215 |
val lits = map (HOLogic.dest_Trueprop o snd) |
216 |
(map_filter (Symtab.lookup steps o fst) names) |
|
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
217 |
in |
54754 | 218 |
(case List.partition (can HOLogic.dest_not) lits of |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
219 |
(negs as _ :: _, pos as _ :: _) => |
54507 | 220 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
54754 | 221 |
| _ => fold (curry s_disj) lits @{term False}) |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
222 |
end |
50016 | 223 |
|> HOLogic.mk_Trueprop |> close_form |
54700 | 224 |
|
55169 | 225 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show |
54700 | 226 |
|
227 |
fun isar_steps outer predecessor accum [] = |
|
228 |
accum |
|
229 |
|> (if tainted = [] then |
|
230 |
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
|
55311 | 231 |
(the_list predecessor, []), massage_methods systematic_methods, "")) |
54700 | 232 |
else |
233 |
I) |
|
234 |
|> rev |
|
54755 | 235 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
54700 | 236 |
let |
237 |
val l = label_of_clause c |
|
238 |
val t = prop_of_clause c |
|
54755 | 239 |
val rule = rule_of_clause_id id |
240 |
val skolem = is_skolemize_rule rule |
|
241 |
||
55279 | 242 |
val deps = fold add_fact_of_dependencies gamma ([], []) |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
243 |
val meths = |
55273 | 244 |
(if skolem then skolem_methods |
245 |
else if is_arith_rule rule then arith_methods |
|
246 |
else if is_datatype_rule rule then datatype_methods |
|
55311 | 247 |
else systematic_methods) |
248 |
|> massage_methods |
|
55280 | 249 |
|
55299 | 250 |
fun prove sub facts = Prove (maybe_show outer c [], [], l, t, sub, facts, meths, "") |
55280 | 251 |
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
54700 | 252 |
in |
253 |
if is_clause_tainted c then |
|
54712 | 254 |
(case gamma of |
54700 | 255 |
[g] => |
54755 | 256 |
if skolem andalso is_clause_tainted g then |
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
257 |
let val subproof = Proof (skolems_of ctxt (prop_of_clause g), [], rev accum) in |
55280 | 258 |
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs |
54700 | 259 |
end |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
260 |
else |
55280 | 261 |
steps_of_rest (prove [] deps) |
262 |
| _ => steps_of_rest (prove [] deps)) |
|
54700 | 263 |
else |
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
264 |
steps_of_rest |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
265 |
(if skolem then Prove ([], skolems_of ctxt t, l, t, [], deps, meths, "") |
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
266 |
else prove [] deps) |
54700 | 267 |
end |
268 |
| isar_steps outer predecessor accum (Cases cases :: infs) = |
|
269 |
let |
|
55186
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
270 |
fun isar_case (c, subinfs) = |
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
271 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
54700 | 272 |
val c = succedent_of_cases cases |
273 |
val l = label_of_clause c |
|
274 |
val t = prop_of_clause c |
|
275 |
val step = |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
276 |
Prove (maybe_show outer c [], [], l, t, |
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
277 |
map isar_case (filter_out (null o snd) cases), |
55311 | 278 |
(the_list predecessor, []), massage_methods systematic_methods, "") |
54700 | 279 |
in |
280 |
isar_steps outer (SOME l) (step :: accum) infs |
|
281 |
end |
|
282 |
and isar_proof outer fix assms lems infs = |
|
283 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
|
284 |
||
55222 | 285 |
val trace = Config.get ctxt trace |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
286 |
|
55256 | 287 |
val canonical_isar_proof = |
51145 | 288 |
refute_graph |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
289 |
|> 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
|
290 |
|> redirect_graph axioms tainted bot |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
291 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
54754 | 292 |
|> isar_proof true params assms lems |
55213 | 293 |
|> postprocess_isar_proof_remove_unreferenced_steps I |
294 |
|> relabel_isar_proof_canonically |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
295 |
|
55286 | 296 |
val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
55256 | 297 |
|
55260 | 298 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
299 |
||
55264 | 300 |
val _ = fold_isar_steps (fn meth => |
57054 | 301 |
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) |
55260 | 302 |
(steps_of_isar_proof canonical_isar_proof) () |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
303 |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
304 |
fun str_of_preplay_outcome outcome = |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
305 |
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
|
306 |
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
|
307 |
string_of_proof_method ctxt [] meth ^ " " ^ |
55266 | 308 |
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
|
309 |
fun comment_of l = map (str_of_meth l) #> commas |
55222 | 310 |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
311 |
fun trace_isar_proof label proof = |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
312 |
if trace then |
55299 | 313 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ |
56097 | 314 |
string_of_isar_proof ctxt subgoal subgoal_count |
315 |
(comment_isar_proof comment_of proof) ^ "\n") |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
316 |
else |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
317 |
() |
54754 | 318 |
|
55299 | 319 |
fun comment_of l (meth :: _) = |
320 |
(case (verbose, |
|
321 |
Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of |
|
322 |
(false, Played _) => "" |
|
323 |
| (_, outcome) => string_of_play_outcome outcome) |
|
324 |
||
54828 | 325 |
val (play_outcome, isar_proof) = |
55256 | 326 |
canonical_isar_proof |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
327 |
|> tap (trace_isar_proof "Original") |
57245 | 328 |
|> compress_isar_proof ctxt compress preplay_timeout preplay_data |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
329 |
|> tap (trace_isar_proof "Compressed") |
55213 | 330 |
|> postprocess_isar_proof_remove_unreferenced_steps |
55266 | 331 |
(keep_fastest_method_of_isar_step (!preplay_data) |
57054 | 332 |
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
333 |
|> tap (trace_isar_proof "Minimized") |
57245 | 334 |
(* 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
|
335 |
unnatural semantics): *) |
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55327
diff
changeset
|
336 |
(* |
55327
3c7f3122ccdc
do a second phase of proof compression after minimization
blanchet
parents:
55325
diff
changeset
|
337 |
|> minimize |
57245 | 338 |
? (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
|
339 |
#> tap (trace_isar_proof "Compressed again")) |
55329
3c2dbd2e221f
more generous Isar proof compression -- try to remove failing steps
blanchet
parents:
55327
diff
changeset
|
340 |
*) |
55260 | 341 |
|> `(preplay_outcome_of_isar_proof (!preplay_data)) |
55325 | 342 |
||> (comment_isar_proof comment_of |
343 |
#> chain_isar_proof |
|
344 |
#> kill_useless_labels_in_isar_proof |
|
345 |
#> relabel_isar_proof_nicely) |
|
49883 | 346 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
347 |
(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
|
348 |
1 => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
349 |
one_line_proof_text ctxt 0 |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
350 |
(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
|
351 |
(case isar_proof of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
352 |
Proof (_, _, [Prove (_, _, _, _, _, (_, gfs), meth :: _, _)]) => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
353 |
let val used_facts' = filter (member (op =) gfs o fst) used_facts in |
57739 | 354 |
((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
|
355 |
end) |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
356 |
else |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
357 |
one_line_params) ^ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
358 |
(if isar_proofs = SOME true then "\n(No structured proof available -- proof too simple.)" |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
359 |
else "") |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
360 |
| num_steps => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
361 |
let |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
362 |
val msg = |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
363 |
(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
|
364 |
(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
|
365 |
in |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
366 |
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
|
367 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
368 |
Active.sendback_markup [Markup.padding_command] |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
369 |
(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
|
370 |
end) |
49883 | 371 |
end |
57056 | 372 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
373 |
if debug then |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
374 |
generate_proof_text () |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
375 |
else |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
376 |
(case try generate_proof_text () of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
377 |
SOME s => s |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
378 |
| NONE => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
379 |
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
|
380 |
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed." else "")) |
57056 | 381 |
end |
49883 | 382 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
383 |
fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) = |
54824 | 384 |
(case play of |
56081 | 385 |
Played _ => meth = SMT2_Method andalso smt_proofs <> SOME true |
56093 | 386 |
| Play_Timed_Out time => Time.> (time, Time.zeroTime) |
387 |
| 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
|
388 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
389 |
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
57739 | 390 |
(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
|
391 |
(if isar_proofs = SOME true orelse |
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
392 |
(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
|
393 |
isar_proof_text ctxt debug isar_proofs smt_proofs isar_params |
49883 | 394 |
else |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
395 |
one_line_proof_text ctxt num_chained) one_line_params |
49883 | 396 |
|
397 |
end; |