author | blanchet |
Sun, 02 Feb 2014 20:53:51 +0100 | |
changeset 55260 | ada3ae6458d4 |
parent 55258 | 8cc42c1f9bb5 |
child 55263 | 4d63fffcde8d |
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 |
54495 | 14 |
type one_line_params = Sledgehammer_Reconstructor.one_line_params |
49914 | 15 |
|
55222 | 16 |
val trace : bool Config.T |
17 |
||
49914 | 18 |
type isar_params = |
55257 | 19 |
bool * (string option * string option) * Time.time * real * bool |
20 |
* (term, string) atp_step list * thm |
|
49914 | 21 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
22 |
val proof_text : Proof.context -> bool -> bool option -> (unit -> isar_params) -> int -> |
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
23 |
one_line_params -> string |
49883 | 24 |
end; |
25 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
26 |
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
49883 | 27 |
struct |
28 |
||
29 |
open ATP_Util |
|
49914 | 30 |
open ATP_Problem |
49883 | 31 |
open ATP_Proof |
32 |
open ATP_Proof_Reconstruct |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
33 |
open Sledgehammer_Util |
52555 | 34 |
open Sledgehammer_Reconstructor |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
35 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
36 |
open Sledgehammer_Isar_Preplay |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
37 |
open Sledgehammer_Isar_Compress |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
38 |
open Sledgehammer_Isar_Try0 |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
39 |
open Sledgehammer_Isar_Minimize |
49914 | 40 |
|
41 |
structure String_Redirect = ATP_Proof_Redirect( |
|
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset
|
42 |
type key = atp_step_name |
49914 | 43 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
44 |
val string_of = fst) |
|
45 |
||
49883 | 46 |
open String_Redirect |
47 |
||
55222 | 48 |
val trace = Attrib.setup_config_bool @{binding sledgehammer_isar_trace} (K false) |
49 |
||
54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset
|
50 |
val e_skolemize_rules = ["skolemize", "shift_quantors"] |
54836 | 51 |
val spass_pirate_datatype_rule = "DT" |
54746 | 52 |
val vampire_skolemisation_rule = "skolemisation" |
53 |
(* TODO: Use "Z3_Proof.string_of_rule" once it is moved to Isabelle *) |
|
54753 | 54 |
val z3_skolemize_rule = "sk" |
55 |
val z3_th_lemma_rule = "th-lemma" |
|
54746 | 56 |
|
54772 | 57 |
val skolemize_rules = |
58 |
e_skolemize_rules @ [spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule] |
|
54746 | 59 |
|
54769
3d6ac2f68bf3
correcly recognize E skolemization steps that are wrapped in a 'shift_quantors' inference
blanchet
parents:
54768
diff
changeset
|
60 |
val is_skolemize_rule = member (op =) skolemize_rules |
54755 | 61 |
val is_arith_rule = String.isPrefix z3_th_lemma_rule |
54836 | 62 |
val is_datatype_rule = String.isPrefix spass_pirate_datatype_rule |
54755 | 63 |
|
54501 | 64 |
fun raw_label_of_num num = (num, 0) |
49914 | 65 |
|
54501 | 66 |
fun label_of_clause [(num, _)] = raw_label_of_num num |
67 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
|
50005 | 68 |
|
54505 | 69 |
fun add_fact_of_dependencies [(_, ss as _ :: _)] = apsnd (union (op =) ss) |
70 |
| add_fact_of_dependencies names = apfst (insert (op =) (label_of_clause names)) |
|
49914 | 71 |
|
54758 | 72 |
(* No "real" literals means only type information (tfree_tcs, clsrel, or clsarity). *) |
73 |
fun is_only_type_information t = t aconv @{prop True} |
|
74 |
||
75 |
(* Discard facts; consolidate adjacent lines that prove the same formula, since they differ only in |
|
54759 | 76 |
type information. *) |
54799 | 77 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
54770 | 78 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
79 |
definitions. *) |
|
54700 | 80 |
if role = Lemma orelse role = Conjecture orelse role = Negated_Conjecture orelse |
54755 | 81 |
role = Hypothesis orelse is_arith_rule rule then |
54746 | 82 |
line :: lines |
54505 | 83 |
else if role = Axiom then |
49914 | 84 |
(* Facts are not proof lines. *) |
54507 | 85 |
lines |> is_only_type_information t ? map (replace_dependencies_in_line (name, [])) |
49914 | 86 |
else |
87 |
map (replace_dependencies_in_line (name, [])) lines |
|
54755 | 88 |
| add_line_pass1 line lines = line :: lines |
49914 | 89 |
|
55191 | 90 |
fun add_lines_pass2 res [] = rev res |
91 |
| add_lines_pass2 res ((name, role, t, rule, deps) :: lines) = |
|
55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
92 |
let |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
93 |
val is_last_line = null lines |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
94 |
|
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
95 |
fun looks_interesting () = |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
96 |
not (is_only_type_information t) andalso null (Term.add_tvars t []) |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
97 |
andalso length deps >= 2 andalso not (can the_single lines) |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
98 |
|
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
99 |
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
|
100 |
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
|
101 |
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
|
102 |
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
|
103 |
if role <> Plain orelse is_skolemize_rule rule orelse is_arith_rule rule orelse |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
104 |
is_datatype_rule rule orelse is_last_line orelse looks_interesting () orelse |
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
105 |
is_before_skolemize_rule () then |
55191 | 106 |
add_lines_pass2 ((name, role, t, rule, deps) :: res) lines |
55184
6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset
|
107 |
else |
55191 | 108 |
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
|
109 |
end |
49914 | 110 |
|
111 |
type isar_params = |
|
55257 | 112 |
bool * (string option * string option) * Time.time * real * bool * (term, string) atp_step list |
113 |
* thm |
|
49914 | 114 |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
115 |
val arith_methods = |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
116 |
[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method, |
55257 | 117 |
Algebra_Method, Metis_Method (NONE, NONE), Meson_Method] |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
118 |
val datatype_methods = [Simp_Method, Simp_Size_Method] |
55257 | 119 |
val metislike_methods0 = |
120 |
[Metis_Method (NONE, NONE), Simp_Method, Auto_Method, Arith_Method, Blast_Method, |
|
121 |
Fastforce_Method, Force_Method, Algebra_Method, Meson_Method] |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
122 |
val rewrite_methods = |
55257 | 123 |
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method (NONE, NONE), |
124 |
Meson_Method] |
|
125 |
val skolem_methods = [Metis_Method (NONE, NONE), Blast_Method, Meson_Method] |
|
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
126 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
127 |
fun isar_proof_text ctxt debug isar_proofs isar_params |
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
128 |
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = |
49883 | 129 |
let |
130 |
fun isar_proof_of () = |
|
131 |
let |
|
55257 | 132 |
val SOME (verbose, alt_metis_args, preplay_timeout, compress_isar, try0_isar, atp_proof, |
133 |
goal) = try isar_params () |
|
134 |
||
135 |
val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
136 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
137 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
138 |
val (_, ctxt) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
139 |
params |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
140 |
|> map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
141 |
|> (fn fixes => ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes) |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
142 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
143 |
val do_preplay = preplay_timeout <> Time.zeroTime |
55183
17ec4a29ef71
renamed Sledgehammer options for symmetry between positive and negative versions
blanchet
parents:
55169
diff
changeset
|
144 |
val try0_isar = try0_isar andalso do_preplay |
55253 | 145 |
val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
146 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
147 |
val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
148 |
fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
149 |
|
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
150 |
fun get_role keep_role ((num, _), role, t, rule, _) = |
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
151 |
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
|
152 |
|
49883 | 153 |
val atp_proof = |
154 |
atp_proof |
|
54755 | 155 |
|> rpair [] |-> fold_rev add_line_pass1 |
55191 | 156 |
|> add_lines_pass2 [] |
54700 | 157 |
|
54535
59737a43e044
support Negated_Conjecture as a TPTP role as well (e.g. for SMT proofs)
blanchet
parents:
54507
diff
changeset
|
158 |
val conjs = |
54700 | 159 |
map_filter (fn (name, role, _, _, _) => |
160 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
|
161 |
atp_proof |
|
54751 | 162 |
val assms = map_filter (Option.map fst o get_role (curry (op =) Hypothesis)) atp_proof |
54700 | 163 |
val lems = |
164 |
map_filter (get_role (curry (op =) Lemma)) atp_proof |
|
54751 | 165 |
|> map (fn ((l, t), rule) => |
54753 | 166 |
let |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
167 |
val (skos, meths) = |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
168 |
if is_skolemize_rule rule then (skolems_of t, skolem_methods) |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
169 |
else if is_arith_rule rule then ([], arith_methods) |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
170 |
else ([], rewrite_methods) |
54753 | 171 |
in |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
172 |
Prove ([], skos, l, t, [], (([], []), meths)) |
54753 | 173 |
end) |
54700 | 174 |
|
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
175 |
val bot = atp_proof |> List.last |> #1 |
54700 | 176 |
|
51145 | 177 |
val refute_graph = |
51212
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
178 |
atp_proof |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
179 |
|> map (fn (name, _, _, _, from) => (from, name)) |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
180 |
|> make_refute_graph bot |
2bbcc9cc12b4
ensure all conjecture clauses are in the graph -- to prevent exceptions later
blanchet
parents:
51208
diff
changeset
|
181 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
54700 | 182 |
|
51145 | 183 |
val axioms = axioms_of_refute_graph refute_graph conjs |
54700 | 184 |
|
51145 | 185 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
51156 | 186 |
val is_clause_tainted = exists (member (op =) tainted) |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
187 |
val steps = |
49883 | 188 |
Symtab.empty |
51201 | 189 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
54758 | 190 |
Symtab.update_new (s, (rule, t |
191 |
|> (if is_clause_tainted [name] then |
|
54768
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
192 |
HOLogic.dest_Trueprop |
ee0881a54c72
fixed confusion between 'prop' and 'bool' introduced in 4960647932ec
blanchet
parents:
54767
diff
changeset
|
193 |
#> role <> Conjecture ? s_not |
54758 | 194 |
#> 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
|
195 |
#> HOLogic.mk_Trueprop |
54758 | 196 |
else |
197 |
I)))) |
|
198 |
atp_proof |
|
54700 | 199 |
|
54755 | 200 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
54700 | 201 |
|
54757
4960647932ec
use 'prop' rather than 'bool' systematically in Isar reconstruction code
blanchet
parents:
54756
diff
changeset
|
202 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> close_form |
50016 | 203 |
| prop_of_clause names = |
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
204 |
let |
54758 | 205 |
val lits = map (HOLogic.dest_Trueprop o snd) |
206 |
(map_filter (Symtab.lookup steps o fst) names) |
|
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset
|
207 |
in |
54754 | 208 |
(case List.partition (can HOLogic.dest_not) lits of |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
209 |
(negs as _ :: _, pos as _ :: _) => |
54507 | 210 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), Library.foldr1 s_disj pos) |
54754 | 211 |
| _ => fold (curry s_disj) lits @{term False}) |
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset
|
212 |
end |
50016 | 213 |
|> HOLogic.mk_Trueprop |> close_form |
54700 | 214 |
|
55169 | 215 |
fun maybe_show outer c = (outer andalso eq_set (op =) (c, conjs)) ? cons Show |
54700 | 216 |
|
217 |
fun isar_steps outer predecessor accum [] = |
|
218 |
accum |
|
219 |
|> (if tainted = [] then |
|
220 |
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [], |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
221 |
((the_list predecessor, []), metislike_methods))) |
54700 | 222 |
else |
223 |
I) |
|
224 |
|> rev |
|
54755 | 225 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
54700 | 226 |
let |
227 |
val l = label_of_clause c |
|
228 |
val t = prop_of_clause c |
|
54755 | 229 |
val rule = rule_of_clause_id id |
230 |
val skolem = is_skolemize_rule rule |
|
231 |
||
54700 | 232 |
fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by) |
233 |
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs |
|
54755 | 234 |
|
235 |
val deps = fold add_fact_of_dependencies gamma no_facts |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
236 |
val meths = |
55245 | 237 |
if skolem then skolem_methods |
238 |
else if is_arith_rule rule then arith_methods |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
239 |
else if is_datatype_rule rule then datatype_methods |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
240 |
else metislike_methods |
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
241 |
val by = (deps, meths) |
54700 | 242 |
in |
243 |
if is_clause_tainted c then |
|
54712 | 244 |
(case gamma of |
54700 | 245 |
[g] => |
54755 | 246 |
if skolem andalso is_clause_tainted g then |
54751 | 247 |
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in |
55245 | 248 |
isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs |
54700 | 249 |
end |
51148
2246a2e17f92
tuning -- refactoring in preparation for handling skolemization of conjecture
blanchet
parents:
51147
diff
changeset
|
250 |
else |
54700 | 251 |
do_rest l (prove [] by) |
54712 | 252 |
| _ => do_rest l (prove [] by)) |
54700 | 253 |
else |
54765 | 254 |
do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by) |
54700 | 255 |
end |
256 |
| isar_steps outer predecessor accum (Cases cases :: infs) = |
|
257 |
let |
|
55186
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
258 |
fun isar_case (c, subinfs) = |
fafdf2424c57
don't forget the last inference(s) after conjecture skolemization
blanchet
parents:
55184
diff
changeset
|
259 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
54700 | 260 |
val c = succedent_of_cases cases |
261 |
val l = label_of_clause c |
|
262 |
val t = prop_of_clause c |
|
263 |
val step = |
|
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
264 |
Prove (maybe_show outer c [], [], l, t, |
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
265 |
map isar_case (filter_out (null o snd) cases), |
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
266 |
((the_list predecessor, []), metislike_methods)) |
54700 | 267 |
in |
268 |
isar_steps outer (SOME l) (step :: accum) infs |
|
269 |
end |
|
270 |
and isar_proof outer fix assms lems infs = |
|
271 |
Proof (fix, assms, lems @ isar_steps outer NONE [] infs) |
|
272 |
||
55257 | 273 |
val string_of_isar_proof = string_of_isar_proof ctxt subgoal subgoal_count |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
274 |
|
55222 | 275 |
val trace = Config.get ctxt trace |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
276 |
|
55256 | 277 |
val canonical_isar_proof = |
51145 | 278 |
refute_graph |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
279 |
|> trace ? tap (tracing o prefix "Refute graph: " o string_of_refute_graph) |
51031
63d71b247323
more robustness in Isar proof reconstruction (cf. bug report by Ondrej)
blanchet
parents:
51026
diff
changeset
|
280 |
|> redirect_graph axioms tainted bot |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
281 |
|> trace ? tap (tracing o prefix "Direct proof: " o string_of_direct_proof) |
54754 | 282 |
|> isar_proof true params assms lems |
55213 | 283 |
|> postprocess_isar_proof_remove_unreferenced_steps I |
284 |
|> relabel_isar_proof_canonically |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
285 |
|
55256 | 286 |
val preplay_ctxt = ctxt |
287 |
|> enrich_context_with_local_facts canonical_isar_proof |
|
288 |
|> silence_reconstructors debug |
|
289 |
||
55260 | 290 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
291 |
||
292 |
fun reset_preplay_outcomes (step as Prove (_, _, l, _, _, (_, meths))) = |
|
293 |
set_preplay_outcomes_of_isar_step preplay_data l (map (fn meth => (meth, |
|
294 |
Lazy.lazy (fn () => preplay_isar_step preplay_ctxt preplay_timeout meth step))) |
|
295 |
meths) |
|
296 |
| reset_preplay_outcomes _ = () |
|
297 |
||
298 |
val _ = fold_isar_steps (K o reset_preplay_outcomes) |
|
299 |
(steps_of_isar_proof canonical_isar_proof) () |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
300 |
|
55223
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
301 |
fun str_of_preplay_outcome outcome = |
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
302 |
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
|
303 |
|
3c593bad6b31
generalized preplaying infrastructure to store various results for various methods
blanchet
parents:
55222
diff
changeset
|
304 |
fun str_of_meth l meth = |
55260 | 305 |
string_of_proof_method meth ^ " " ^ |
306 |
str_of_preplay_outcome (preplay_outcome_of_isar_step (!preplay_data) l meth) |
|
55244
12e1a5d8ee48
simplified data structure -- eliminated distinction between 'first-class' and 'second-class' proof methods
blanchet
parents:
55223
diff
changeset
|
307 |
fun comment_of l = map (str_of_meth l) #> commas |
55222 | 308 |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
309 |
fun trace_isar_proof label proof = |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
310 |
if trace then |
55222 | 311 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ string_of_isar_proof comment_of proof ^ |
312 |
"\n") |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
313 |
else |
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
314 |
() |
54754 | 315 |
|
54828 | 316 |
val (play_outcome, isar_proof) = |
55256 | 317 |
canonical_isar_proof |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
318 |
|> tap (trace_isar_proof "Original") |
55258 | 319 |
|> compress_isar_proof preplay_ctxt compress_isar preplay_data |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
320 |
|> tap (trace_isar_proof "Compressed") |
55258 | 321 |
|> try0_isar ? try0_isar_proof preplay_ctxt preplay_timeout preplay_data |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
322 |
|> tap (trace_isar_proof "Tried0") |
55213 | 323 |
|> postprocess_isar_proof_remove_unreferenced_steps |
55258 | 324 |
(try0_isar ? minimize_isar_step_dependencies preplay_ctxt preplay_data) |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
325 |
|> tap (trace_isar_proof "Minimized") |
55260 | 326 |
|> `(preplay_outcome_of_isar_proof (!preplay_data)) |
55220 | 327 |
||> chain_isar_proof |
328 |
||> kill_useless_labels_in_isar_proof |
|
329 |
||> relabel_isar_proof_finally |
|
49883 | 330 |
in |
55222 | 331 |
(case string_of_isar_proof (K (K "")) isar_proof of |
49883 | 332 |
"" => |
55213 | 333 |
if isar_proofs = SOME true then "\nNo structured proof available (proof too simple)." |
334 |
else "" |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
335 |
| isar_text => |
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
336 |
let |
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset
|
337 |
val msg = |
51203 | 338 |
(if verbose then |
55260 | 339 |
let val num_steps = add_isar_steps (steps_of_isar_proof isar_proof) 0 in |
55213 | 340 |
[string_of_int num_steps ^ " step" ^ plural_s num_steps] |
341 |
end |
|
51203 | 342 |
else |
343 |
[]) @ |
|
54828 | 344 |
(if do_preplay then [string_of_play_outcome play_outcome] else []) |
50277 | 345 |
in |
54507 | 346 |
"\n\nStructured proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
347 |
Active.sendback_markup [Markup.padding_command] isar_text |
|
54754 | 348 |
end) |
49883 | 349 |
end |
54760
a1ac3eaa0d11
generate proper succedent for cases with trivial branches
blanchet
parents:
54759
diff
changeset
|
350 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
351 |
val one_line_proof = one_line_proof_text 0 one_line_params |
49883 | 352 |
val isar_proof = |
353 |
if debug then |
|
354 |
isar_proof_of () |
|
54754 | 355 |
else |
356 |
(case try isar_proof_of () of |
|
357 |
SOME s => s |
|
358 |
| NONE => |
|
359 |
if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "") |
|
49883 | 360 |
in one_line_proof ^ isar_proof end |
361 |
||
54824 | 362 |
fun isar_proof_would_be_a_good_idea (reconstr, play) = |
363 |
(case play of |
|
364 |
Played _ => reconstr = SMT |
|
54823 | 365 |
| Play_Timed_Out _ => true |
54824 | 366 |
| Play_Failed => true |
367 |
| Not_Played => false) |
|
51187
c344cf148e8f
avoid using "smt" for minimization -- better use the prover itself, since then Sledgehammer gets to try metis again and gives the opportunity to output an Isar proof -- and show Isar proof as fallback for SMT proofs
blanchet
parents:
51179
diff
changeset
|
368 |
|
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
369 |
fun proof_text ctxt debug isar_proofs isar_params num_chained |
55256 | 370 |
(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
|
371 |
(if isar_proofs = SOME true orelse |
2654b3965c8d
made "isar_proofs" a 3-way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset
|
372 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
373 |
isar_proof_text ctxt debug isar_proofs isar_params |
49883 | 374 |
else |
53052
a0db255af8c5
sledgehammer sendback always uses Markup.padding_command: sensible default for most practical applications -- old-style in-line replacement is superseded by auto mode or panel;
wenzelm
parents:
53047
diff
changeset
|
375 |
one_line_proof_text num_chained) one_line_params |
49883 | 376 |
|
377 |
end; |