author | blanchet |
Wed, 06 Dec 2023 14:05:18 +0100 | |
changeset 79143 | 2eb3dcae9781 |
parent 78696 | ef89f1beee95 |
child 79730 | 4031aafc2dda |
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 = |
57783 | 19 |
bool * (string option * string option) * Time.time * real option * bool * bool |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
20 |
* (term, string) atp_step list * thm |
49914 | 21 |
|
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70931
diff
changeset
|
22 |
val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int -> |
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70931
diff
changeset
|
23 |
one_line_params -> string |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
75956
diff
changeset
|
24 |
val abduce_text : Proof.context -> term list -> string |
49883 | 25 |
end; |
26 |
||
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
27 |
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
49883 | 28 |
struct |
29 |
||
30 |
open ATP_Util |
|
49914 | 31 |
open ATP_Problem |
70931 | 32 |
open ATP_Problem_Generate |
49883 | 33 |
open ATP_Proof |
34 |
open ATP_Proof_Reconstruct |
|
49918
cf441f4a358b
renamed Isar-proof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset
|
35 |
open Sledgehammer_Util |
55287 | 36 |
open Sledgehammer_Proof_Methods |
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
37 |
open Sledgehammer_Isar_Proof |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
38 |
open Sledgehammer_Isar_Preplay |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
39 |
open Sledgehammer_Isar_Compress |
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset
|
40 |
open Sledgehammer_Isar_Minimize |
49914 | 41 |
|
42 |
structure String_Redirect = ATP_Proof_Redirect( |
|
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset
|
43 |
type key = atp_step_name |
49914 | 44 |
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') |
45 |
val string_of = fst) |
|
46 |
||
49883 | 47 |
open String_Redirect |
48 |
||
69593 | 49 |
val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false) |
55222 | 50 |
|
57785 | 51 |
val e_definition_rule = "definition" |
57654
f89c0749533d
'shift_quantors' is not an E skolemization rule (cf. 3ab503b04bdb)
blanchet
parents:
57288
diff
changeset
|
52 |
val e_skolemize_rule = "skolemize" |
57759 | 53 |
val leo2_extcnf_forall_neg_rule = "extcnf_forall_neg" |
57709 | 54 |
val satallax_skolemize_rule = "tab_ex" |
54746 | 55 |
val vampire_skolemisation_rule = "skolemisation" |
57761 | 56 |
val veriT_la_generic_rule = "la_generic" |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
57 |
val veriT_simp_arith_rule = "simp_arith" |
75956
1e2a9d2251b0
remove duplicate parsing for alethe; fix skolemization;
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
75873
diff
changeset
|
58 |
val veriT_skolemize_rules = Lethe_Proof.skolemization_steps |
58061 | 59 |
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize |
60 |
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") |
|
57702
dfc834e39c1f
Skolemization support for leo-II and Zipperposition.
fleury
parents:
57699
diff
changeset
|
61 |
val zipperposition_cnf_rule = "cnf" |
54746 | 62 |
|
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
63 |
val symbol_introduction_rules = |
57785 | 64 |
[e_definition_rule, e_skolemize_rule, leo2_extcnf_forall_neg_rule, satallax_skolemize_rule, |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72401
diff
changeset
|
65 |
spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
66 |
zipperposition_cnf_rule, zipperposition_define_rule] @ veriT_skolemize_rules |
54746 | 67 |
|
58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
68 |
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) |
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
69 |
val is_maybe_ext_rule = is_ext_rule orf String.isPrefix satallax_tab_rule_prefix |
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
70 |
|
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
71 |
val is_symbol_introduction_rule = member (op =) symbol_introduction_rules |
57761 | 72 |
fun is_arith_rule rule = |
57762 | 73 |
String.isPrefix z3_th_lemma_rule_prefix rule orelse rule = veriT_simp_arith_rule orelse |
57761 | 74 |
rule = veriT_la_generic_rule |
54755 | 75 |
|
54501 | 76 |
fun raw_label_of_num num = (num, 0) |
49914 | 77 |
|
54501 | 78 |
fun label_of_clause [(num, _)] = raw_label_of_num num |
79 |
| label_of_clause c = (space_implode "___" (map (fst o raw_label_of_num o fst) c), 0) |
|
50005 | 80 |
|
58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
81 |
fun add_global_fact ss = apsnd (union (op =) ss) |
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
82 |
|
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
83 |
fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss |
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
84 |
| add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) |
49914 | 85 |
|
54799 | 86 |
fun add_line_pass1 (line as (name, role, t, rule, [])) lines = |
54770 | 87 |
(* No dependencies: lemma (for Z3), fact, conjecture, or (for Vampire) internal facts or |
88 |
definitions. *) |
|
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
89 |
if role = Conjecture orelse role = Negated_Conjecture then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
90 |
line :: lines |
69593 | 91 |
else if t aconv \<^prop>\<open>True\<close> then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
92 |
map (replace_dependencies_in_line (name, [])) lines |
75123
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
93 |
else if role = Definition orelse role = Lemma orelse role = Hypothesis |
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
94 |
orelse is_arith_rule rule then |
57708
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
95 |
line :: lines |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
96 |
else if role = Axiom then |
4b52c1b319ce
veriT changes for lifted terms, and ite_elim rules.
fleury
parents:
57705
diff
changeset
|
97 |
lines (* axioms (facts) need no proof lines *) |
57768
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
98 |
else |
a63f14f1214c
fine-tuned Isar reconstruction, esp. boolean simplifications
blanchet
parents:
57767
diff
changeset
|
99 |
map (replace_dependencies_in_line (name, [])) lines |
54755 | 100 |
| add_line_pass1 line lines = line :: lines |
49914 | 101 |
|
57771 | 102 |
fun add_lines_pass2 res [] = rev res |
103 |
| 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
|
104 |
let |
57791 | 105 |
fun normalize role = |
106 |
role = Conjecture ? (HOLogic.dest_Trueprop #> s_not #> HOLogic.mk_Trueprop) |
|
107 |
||
57771 | 108 |
val norm_t = normalize role t |
109 |
val is_duplicate = |
|
110 |
exists (fn (prev_name, prev_role, prev_t, _, _) => |
|
58514
1fc93ea5136b
eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents:
58506
diff
changeset
|
111 |
(prev_role = Hypothesis andalso prev_t aconv t) orelse |
1fc93ea5136b
eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents:
58506
diff
changeset
|
112 |
(member (op =) deps prev_name andalso |
1fc93ea5136b
eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents:
58506
diff
changeset
|
113 |
Term.aconv_untyped (normalize prev_role prev_t, norm_t))) |
57771 | 114 |
res |
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
115 |
|
69593 | 116 |
fun looks_boring () = t aconv \<^prop>\<open>False\<close> 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
|
117 |
|
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
118 |
fun is_symbol_introduction_line (_, _, _, rule', deps') = |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
119 |
is_symbol_introduction_rule rule' andalso member (op =) deps' name |
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset
|
120 |
|
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
121 |
fun is_before_symbol_introduction_rule () = exists is_symbol_introduction_line 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 |
in |
57771 | 123 |
if is_duplicate orelse |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
124 |
(role = Plain andalso not (is_symbol_introduction_rule rule) andalso |
58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEO-II and Satallax
blanchet
parents:
58517
diff
changeset
|
125 |
not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
126 |
not (null lines) andalso looks_boring () andalso |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
127 |
not (is_before_symbol_introduction_rule ())) then |
57771 | 128 |
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
|
129 |
else |
57771 | 130 |
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
|
131 |
end |
49914 | 132 |
|
133 |
type isar_params = |
|
57783 | 134 |
bool * (string option * string option) * Time.time * real option * bool * bool |
55288
1a4358d14ce2
added 'smt' option to control generation of 'by smt' proofs
blanchet
parents:
55287
diff
changeset
|
135 |
* (term, string) atp_step list * thm |
49914 | 136 |
|
78695 | 137 |
val basic_systematic_methods = |
138 |
[Metis_Method (NONE, NONE), Meson_Method, Blast_Method, SATx_Method, Argo_Method] |
|
139 |
val basic_simp_based_methods = |
|
140 |
[Auto_Method, Simp_Method, Fastforce_Method, Force_Method] |
|
141 |
val basic_arith_methods = |
|
142 |
[Linarith_Method, Presburger_Method, Algebra_Method] |
|
55311 | 143 |
|
57744
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
144 |
val arith_methods = basic_arith_methods @ basic_simp_based_methods @ basic_systematic_methods |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
145 |
val systematic_methods = |
a68b8db8691d
added appropriate method for skolemization of Z3 steps to the mix
blanchet
parents:
57741
diff
changeset
|
146 |
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ |
57699 | 147 |
[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
|
148 |
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods |
58517 | 149 |
val skolem_methods = Moura_Method :: systematic_methods |
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset
|
150 |
|
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
59577
diff
changeset
|
151 |
fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params |
57739 | 152 |
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = |
49883 | 153 |
let |
58843 | 154 |
val _ = if debug then writeln "Constructing Isar proof..." else () |
56097 | 155 |
|
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
156 |
fun generate_proof_text () = |
49883 | 157 |
let |
57791 | 158 |
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = |
57245 | 159 |
isar_params () |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
160 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
161 |
if null atp_proof0 then |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
162 |
one_line_proof_text ctxt 0 one_line_params |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
163 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
164 |
let |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
165 |
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
|
166 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
167 |
fun massage_methods (meths as meth :: _) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
168 |
if not try0 then [meth] |
75868
e7b04452eef3
revived 'try0' and 'smart' Isar proofs in Sledgehammer
blanchet
parents:
75124
diff
changeset
|
169 |
else if smt_proofs then insert (op =) (SMT_Method SMT_Z3) meths |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
170 |
else meths |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
171 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
172 |
val (params, _, concl_t) = strip_subgoal goal subgoal ctxt |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
173 |
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
174 |
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
|
175 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
176 |
val do_preplay = preplay_timeout <> Time.zeroTime |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
177 |
val compress = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
178 |
(case compress of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
179 |
NONE => if isar_proofs = NONE andalso do_preplay then 1000.0 else 10.0 |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
180 |
| SOME n => n) |
55168
948e8b7ea82f
correctly handle exceptions arising from (experimental) Isar proof code
blanchet
parents:
54838
diff
changeset
|
181 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
182 |
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
183 |
fun introduced_symbols_of ctxt t = |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
184 |
Term.add_frees t [] |> filter_out (is_fixed ctxt o fst) |> rev |
54700 | 185 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
186 |
fun get_role keep_role ((num, _), role, t, rule, _) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
187 |
if keep_role role then SOME ((raw_label_of_num num, t), rule) else NONE |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
188 |
|
72355 | 189 |
val trace = Config.get ctxt trace |
190 |
||
191 |
val string_of_atp_steps = |
|
192 |
let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in |
|
193 |
enclose "[\n" "\n]" o cat_lines o map (enclose " " "," o to_string) |
|
194 |
end |
|
195 |
||
196 |
val atp_proof = atp_proof0 |
|
197 |
|> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps) |
|
75047
7d2a5d1f09af
guard against duplicate lines in Zipperposition proofs
blanchet
parents:
72798
diff
changeset
|
198 |
|> distinct (op =) (* Zipperposition generates duplicate lines *) |
7d2a5d1f09af
guard against duplicate lines in Zipperposition proofs
blanchet
parents:
72798
diff
changeset
|
199 |
|> (fn lines => fold_rev add_line_pass1 lines []) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
200 |
|> add_lines_pass2 [] |
72355 | 201 |
|> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
202 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
203 |
val conjs = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
204 |
map_filter (fn (name, role, _, _, _) => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
205 |
if member (op =) [Conjecture, Negated_Conjecture] role then SOME name else NONE) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
206 |
atp_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
207 |
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
|
208 |
|
72584 | 209 |
fun add_lemma ((label, goal), rule) ctxt = |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
210 |
let |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
211 |
val (obtains, proof_methods) = |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
212 |
(if is_symbol_introduction_rule rule then (introduced_symbols_of ctxt goal, skolem_methods) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
213 |
else if is_arith_rule rule then ([], arith_methods) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
214 |
else ([], rewrite_methods)) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
215 |
||> massage_methods |
72584 | 216 |
val prove = Prove { |
217 |
qualifiers = [], |
|
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
218 |
obtains = obtains, |
72584 | 219 |
label = label, |
220 |
goal = goal, |
|
221 |
subproofs = [], |
|
222 |
facts = ([], []), |
|
223 |
proof_methods = proof_methods, |
|
224 |
comment = ""} |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
225 |
in |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
226 |
(prove, ctxt |> not (null obtains) ? (Variable.add_fixes (map fst obtains) #> snd)) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
227 |
end |
57288
ffd928316c75
supports gradual skolemization (cf. Z3) by threading context through correctly
blanchet
parents:
57287
diff
changeset
|
228 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
229 |
val (lems, _) = |
75123
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
230 |
fold_map add_lemma (map_filter (get_role (member (op =) [Definition, Lemma])) |
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
231 |
atp_proof) ctxt |
54700 | 232 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
233 |
val bot = #1 (List.last atp_proof) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
234 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
235 |
val refute_graph = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
236 |
atp_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
237 |
|> map (fn (name, _, _, _, from) => (from, name)) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
238 |
|> make_refute_graph bot |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
239 |
|> fold (Atom_Graph.default_node o rpair ()) conjs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
240 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
241 |
val axioms = axioms_of_refute_graph refute_graph conjs |
54700 | 242 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
243 |
val tainted = tainted_atoms_of_refute_graph refute_graph conjs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
244 |
val is_clause_tainted = exists (member (op =) tainted) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
245 |
val steps = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
246 |
Symtab.empty |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
247 |
|> fold (fn (name as (s, _), role, t, rule, _) => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
248 |
Symtab.update_new (s, (rule, t |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
249 |
|> (if is_clause_tainted [name] then |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
250 |
HOLogic.dest_Trueprop |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
251 |
#> role <> Conjecture ? s_not |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
252 |
#> fold exists_of (map Var (Term.add_vars t [])) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
253 |
#> HOLogic.mk_Trueprop |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
254 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
255 |
I)))) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
256 |
atp_proof |
58516
1edba0152491
insert lemmas closer to where they are needed, both for esthetics and (primarily) for correctness in case the lemma refers to a skolem
blanchet
parents:
58514
diff
changeset
|
257 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
258 |
fun is_referenced_in_step _ (Let _) = false |
72584 | 259 |
| is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) = |
260 |
member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs |
|
72582 | 261 |
and is_referenced_in_proof l (Proof {steps, ...}) = |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
262 |
exists (is_referenced_in_step l) steps |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
263 |
|
78696
ef89f1beee95
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
blanchet
parents:
78695
diff
changeset
|
264 |
(* We try to introduce pure lemmas (not "obtains") close to where |
ef89f1beee95
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
blanchet
parents:
78695
diff
changeset
|
265 |
they are used. *) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
266 |
fun insert_lemma_in_step lem |
75057
79b4e711d6a2
robustly handle empty proof blocks in Isar proof output
blanchet
parents:
75051
diff
changeset
|
267 |
(step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs), |
79b4e711d6a2
robustly handle empty proof blocks in Isar proof output
blanchet
parents:
75051
diff
changeset
|
268 |
proof_methods, comment}) = |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
269 |
let val l' = the (label_of_isar_step lem) in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
270 |
if member (op =) ls l' then |
58517 | 271 |
[lem, step] |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
272 |
else |
72584 | 273 |
let val refs = map (is_referenced_in_proof l') subproofs in |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
274 |
if length (filter I refs) = 1 then |
72584 | 275 |
[Prove { |
276 |
qualifiers = qualifiers, |
|
277 |
obtains = obtains, |
|
278 |
label = label, |
|
279 |
goal = goal, |
|
280 |
subproofs = |
|
281 |
map2 (fn false => I | true => insert_lemma_in_proof lem) refs subproofs, |
|
282 |
facts = (ls, gs), |
|
283 |
proof_methods = proof_methods, |
|
284 |
comment = comment}] |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
285 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
286 |
[lem, step] |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
287 |
end |
58517 | 288 |
end |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
289 |
and insert_lemma_in_steps lem [] = [lem] |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
290 |
| insert_lemma_in_steps lem (step :: steps) = |
78696
ef89f1beee95
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
blanchet
parents:
78695
diff
changeset
|
291 |
if not (null (obtains_of_isar_step lem)) |
ef89f1beee95
parse applie lambdas correctly plus deal gracefully with lambda-lifting in Zipperposition
blanchet
parents:
78695
diff
changeset
|
292 |
orelse is_referenced_in_step (the (label_of_isar_step lem)) step then |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
293 |
insert_lemma_in_step lem step @ steps |
54700 | 294 |
else |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
295 |
step :: insert_lemma_in_steps lem steps |
72583 | 296 |
and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = |
72585 | 297 |
isar_proof_with_steps proof (insert_lemma_in_steps lem steps) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
298 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
299 |
val rule_of_clause_id = fst o the o Symtab.lookup steps o fst |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
300 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
301 |
val finish_off = close_form #> rename_bound_vars |
54755 | 302 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
303 |
fun prop_of_clause [(num, _)] = Symtab.lookup steps num |> the |> snd |> finish_off |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
304 |
| prop_of_clause names = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
305 |
let |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
306 |
val lits = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
307 |
map (HOLogic.dest_Trueprop o snd) (map_filter (Symtab.lookup steps o fst) names) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
308 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
309 |
(case List.partition (can HOLogic.dest_not) lits of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
310 |
(negs as _ :: _, pos as _ :: _) => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
311 |
s_imp (Library.foldr1 s_conj (map HOLogic.dest_not negs), |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
312 |
Library.foldr1 s_disj pos) |
69593 | 313 |
| _ => fold (curry s_disj) lits \<^term>\<open>False\<close>) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
314 |
end |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
315 |
|> HOLogic.mk_Trueprop |> finish_off |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
316 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
317 |
fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] |
55280 | 318 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
319 |
fun isar_steps outer predecessor accum [] = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
320 |
accum |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
321 |
|> (if tainted = [] then |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
322 |
(* e.g., trivial, empty proof by Z3 *) |
72584 | 323 |
cons (Prove { |
324 |
qualifiers = if outer then [Show] else [], |
|
325 |
obtains = [], |
|
326 |
label = no_label, |
|
327 |
goal = concl_t, |
|
328 |
subproofs = [], |
|
329 |
facts = sort_facts (the_list predecessor, []), |
|
330 |
proof_methods = massage_methods systematic_methods', |
|
331 |
comment = ""}) |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
332 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
333 |
I) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
334 |
|> rev |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
335 |
| isar_steps outer _ accum (Have (id, (gamma, c)) :: infs) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
336 |
let |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
337 |
val l = label_of_clause c |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
338 |
val t = prop_of_clause c |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
339 |
val rule = rule_of_clause_id id |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
340 |
val introduces_symbols = is_symbol_introduction_rule rule |
54700 | 341 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
342 |
val deps = ([], []) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
343 |
|> fold add_fact_of_dependency gamma |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
344 |
|> is_maybe_ext_rule rule ? add_global_fact [short_thm_name ctxt ext] |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
345 |
|> sort_facts |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
346 |
val meths = |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
347 |
(if introduces_symbols then skolem_methods |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
348 |
else if is_arith_rule rule then arith_methods |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
349 |
else systematic_methods') |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
350 |
|> massage_methods |
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
351 |
|
72584 | 352 |
fun prove subproofs facts = Prove { |
353 |
qualifiers = maybe_show outer c, |
|
354 |
obtains = [], |
|
355 |
label = l, |
|
356 |
goal = t, |
|
357 |
subproofs = subproofs, |
|
358 |
facts = facts, |
|
359 |
proof_methods = meths, |
|
360 |
comment = ""} |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
361 |
fun steps_of_rest step = isar_steps outer (SOME l) (step :: accum) infs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
362 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
363 |
if is_clause_tainted c then |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
364 |
(case gamma of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
365 |
[g] => |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
366 |
if introduces_symbols andalso is_clause_tainted g andalso not (null accum) then |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
367 |
let |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
368 |
val fixes = introduced_symbols_of ctxt (prop_of_clause g) |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
369 |
val subproof = Proof {fixes = fixes, assumptions = [], steps = rev accum} |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
370 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
371 |
isar_steps outer (SOME l) [prove [subproof] ([], [])] infs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
372 |
end |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
373 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
374 |
steps_of_rest (prove [] deps) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
375 |
| _ => steps_of_rest (prove [] deps)) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
376 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
377 |
steps_of_rest |
75124
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
378 |
(if introduces_symbols then |
f12539c8de0c
more handling of Zipperposition definitions in Isar proof construction
blanchet
parents:
75123
diff
changeset
|
379 |
(case introduced_symbols_of ctxt t of |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
380 |
[] => prove [] deps |
72584 | 381 |
| skos => Prove { |
382 |
qualifiers = [], |
|
383 |
obtains = skos, |
|
384 |
label = l, |
|
385 |
goal = t, |
|
386 |
subproofs = [], |
|
387 |
facts = deps, |
|
388 |
proof_methods = meths, |
|
389 |
comment = ""}) |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
390 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
391 |
prove [] deps) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
392 |
end |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
393 |
| isar_steps outer predecessor accum (Cases cases :: infs) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
394 |
let |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
395 |
fun isar_case (c, subinfs) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
396 |
isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
397 |
val c = succedent_of_cases cases |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
398 |
val l = label_of_clause c |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
399 |
val t = prop_of_clause c |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
400 |
val step = |
72584 | 401 |
Prove { |
402 |
qualifiers = maybe_show outer c, |
|
403 |
obtains = [], |
|
404 |
label = l, |
|
405 |
goal = t, |
|
406 |
subproofs = map isar_case (filter_out (null o snd) cases), |
|
407 |
facts = sort_facts (the_list predecessor, []), |
|
408 |
proof_methods = massage_methods systematic_methods', |
|
409 |
comment = ""} |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
410 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
411 |
isar_steps outer (SOME l) (step :: accum) infs |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
412 |
end |
72582 | 413 |
and isar_proof outer fixes assumptions lems infs = |
414 |
let val steps = fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs) in |
|
415 |
Proof {fixes = fixes, assumptions = assumptions, steps = steps} |
|
416 |
end |
|
55214
48a347b40629
better tracing + syntactically correct 'metis' calls
blanchet
parents:
55213
diff
changeset
|
417 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
418 |
val canonical_isar_proof = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
419 |
refute_graph |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
420 |
|> trace ? tap (tracing o prefix "Refute graph:\n" o string_of_refute_graph) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
421 |
|> redirect_graph axioms tainted bot |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
422 |
|> trace ? tap (tracing o prefix "Direct proof:\n" o string_of_direct_proof) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
423 |
|> isar_proof true params assms lems |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
424 |
|> postprocess_isar_proof_remove_show_stuttering |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
425 |
|> postprocess_isar_proof_remove_unreferenced_steps I |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
426 |
|> relabel_isar_proof_canonically |
54754 | 427 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
428 |
val ctxt = ctxt |> enrich_context_with_local_facts canonical_isar_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
429 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
430 |
val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
431 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
432 |
val _ = fold_isar_steps (fn meth => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
433 |
K (set_preplay_outcomes_of_isar_step ctxt preplay_timeout preplay_data meth [])) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
434 |
(steps_of_isar_proof canonical_isar_proof) () |
55299 | 435 |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
436 |
fun str_of_preplay_outcome outcome = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
437 |
if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?" |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
438 |
fun str_of_meth l meth = |
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
72355
diff
changeset
|
439 |
string_of_proof_method [] meth ^ " " ^ |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
440 |
str_of_preplay_outcome |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
441 |
(preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
442 |
fun comment_of l = map (str_of_meth l) #> commas |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
443 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
444 |
fun trace_isar_proof label proof = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
445 |
if trace then |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
446 |
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
447 |
string_of_isar_proof ctxt subgoal subgoal_count |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
448 |
(comment_isar_proof comment_of proof) ^ "\n") |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
449 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
450 |
() |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
451 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
452 |
fun comment_of l (meth :: _) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
453 |
(case (verbose, |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
454 |
Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth)) of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
455 |
(false, Played _) => "" |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
456 |
| (_, outcome) => string_of_play_outcome outcome) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
457 |
|
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
458 |
val (play_outcome, isar_proof) = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
459 |
canonical_isar_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
460 |
|> tap (trace_isar_proof "Original") |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
461 |
|> compress_isar_proof ctxt compress preplay_timeout preplay_data |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
462 |
|> tap (trace_isar_proof "Compressed") |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
463 |
|> postprocess_isar_proof_remove_unreferenced_steps |
75051
1a8f6cb5efd6
don't perform preplaying steps if preplaying is disabled
blanchet
parents:
75049
diff
changeset
|
464 |
(do_preplay ? keep_fastest_method_of_isar_step (!preplay_data) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
465 |
#> minimize ? minimize_isar_step_dependencies ctxt preplay_data) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
466 |
|> tap (trace_isar_proof "Minimized") |
75123
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
467 |
|> `(if do_preplay then preplay_outcome_of_isar_proof (!preplay_data) |
66eb6fdfc244
handle Zipperposition definitions in Isar proof construction
blanchet
parents:
75057
diff
changeset
|
468 |
else K (Play_Timed_Out Time.zeroTime)) |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
469 |
||> (comment_isar_proof comment_of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
470 |
#> chain_isar_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
471 |
#> kill_useless_labels_in_isar_proof |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
472 |
#> relabel_isar_proof_nicely |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
473 |
#> rationalize_obtains_in_isar_proofs ctxt) |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
474 |
in |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
475 |
(case (num_chained, add_isar_steps (steps_of_isar_proof isar_proof) 0) of |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
476 |
(0, 1) => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
477 |
one_line_proof_text ctxt 0 |
67560 | 478 |
(if is_less (play_outcome_ord (play_outcome, one_line_play)) then |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
479 |
(case isar_proof of |
79143 | 480 |
Proof {steps = [Prove {qualifiers = [Show], facts = (_, gfs), |
481 |
proof_methods = meth :: _, ...}], ...} => |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
482 |
let |
68668
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
483 |
val used_facts' = |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
484 |
map_filter (fn s => |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
485 |
if exists (fn (s', (sc, _)) => s' = s andalso sc = Chained) |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
486 |
used_facts then |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
487 |
NONE |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
488 |
else |
c9570658e8f1
don't lose facts that were introduced to deal with a theory or some preprocessing in the prover (e.g. the definition of 'abs' in an SMT proof)
blanchet
parents:
67560
diff
changeset
|
489 |
SOME (s, (Global, General))) gfs |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
490 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
491 |
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) |
79143 | 492 |
end |
493 |
| _ => one_line_params) |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
494 |
else |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
495 |
one_line_params) ^ |
75049 | 496 |
(if isar_proofs = SOME true then "\n(No Isar proof available)" else "") |
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
497 |
| (_, num_steps) => |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
498 |
let |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
499 |
val msg = |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
500 |
(if verbose then [string_of_int num_steps ^ " step" ^ plural_s num_steps] |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
501 |
else []) @ |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
502 |
(if do_preplay then [string_of_play_outcome play_outcome] else []) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
503 |
in |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
504 |
one_line_proof_text ctxt 0 one_line_params ^ |
75873 | 505 |
(if isar_proofs <> NONE orelse (case play_outcome of Played _ => true | _ => false) then |
506 |
"\n\nIsar proof" ^ (commas msg |> not (null msg) ? enclose " (" ")") ^ ":\n" ^ |
|
507 |
Active.sendback_markup_command |
|
508 |
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof) |
|
509 |
else |
|
510 |
"") |
|
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
511 |
end) |
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset
|
512 |
end |
49883 | 513 |
end |
57056 | 514 |
in |
57287
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
515 |
if debug then |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
516 |
generate_proof_text () |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
517 |
else |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
518 |
(case try generate_proof_text () of |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
519 |
SOME s => s |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
520 |
| NONE => |
68aa585269ac
given two one-liners, only show the best of the two
blanchet
parents:
57286
diff
changeset
|
521 |
one_line_proof_text ctxt 0 one_line_params ^ |
63692 | 522 |
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) |
57056 | 523 |
end |
49883 | 524 |
|
72355 | 525 |
fun isar_proof_would_be_a_good_idea (_, play) = |
54824 | 526 |
(case play of |
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70931
diff
changeset
|
527 |
Played _ => false |
62826 | 528 |
| Play_Timed_Out time => time > Time.zeroTime |
56093 | 529 |
| 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
|
530 |
|
55297
1dfcd49f5dcb
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
blanchet
parents:
55296
diff
changeset
|
531 |
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained |
57739 | 532 |
(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
|
533 |
(if isar_proofs = SOME true orelse |
71931
0c8a9c028304
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
blanchet
parents:
70931
diff
changeset
|
534 |
(isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then |
60612
79d71bfea310
removed chained facts from preplaying -- and careful about extra chained facts when removing 'proof -' and 'qed' from one-line Isar proofs
blanchet
parents:
59577
diff
changeset
|
535 |
isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params |
49883 | 536 |
else |
56985
82c83978fbd9
correctly add extra facts to lemmas (cf. conjecture and hypotheses) in Z3 Isar proofs
blanchet
parents:
56983
diff
changeset
|
537 |
one_line_proof_text ctxt num_chained) one_line_params |
49883 | 538 |
|
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
75956
diff
changeset
|
539 |
fun abduce_text ctxt tms = |
77425 | 540 |
"Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^ |
77418
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
75956
diff
changeset
|
541 |
cat_lines (map (Syntax.string_of_term ctxt) tms) |
a8458f0df4ee
implemented ad hoc abduction in Sledgehammer with E
blanchet
parents:
75956
diff
changeset
|
542 |
|
49883 | 543 |
end; |