author  desharna 
Thu, 12 Nov 2020 11:00:34 +0100  
changeset 72585  18eb7ec2720f 
parent 72584  4ea19e5dc67e 
child 72798  e732c98b02e6 
permissions  rwrr 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_isar.ML 
49883  2 
Author: Jasmin Blanchette, TU Muenchen 
3 
Author: Steffen Juilf Smolka, TU Muenchen 

4 

49914  5 
Isar proof reconstruction from ATP proofs. 
49883  6 
*) 
7 

55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

8 
signature SLEDGEHAMMER_ISAR = 
49883  9 
sig 
54771
85879aa61334
move some Z3 specifics out (and into private repository with the rest of the Z3specific code)
blanchet
parents:
54770
diff
changeset

10 
type atp_step_name = ATP_Proof.atp_step_name 
54495  11 
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step 
53586
bd5fa6425993
prefixed types and some functions with "atp_" for disambiguation
blanchet
parents:
53052
diff
changeset

12 
type 'a atp_proof = 'a ATP_Proof.atp_proof 
49914  13 
type stature = ATP_Problem_Generate.stature 
55287  14 
type one_line_params = Sledgehammer_Proof_Methods.one_line_params 
49914  15 

55222  16 
val trace : bool Config.T 
17 

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

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

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 
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 
70931  31 
open ATP_Problem_Generate 
49883  32 
open ATP_Proof 
33 
open ATP_Proof_Reconstruct 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

34 
open Sledgehammer_Util 
55287  35 
open Sledgehammer_Proof_Methods 
55202
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

36 
open Sledgehammer_Isar_Proof 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

37 
open Sledgehammer_Isar_Preplay 
824c48a539c9
renamed many Sledgehammer ML files to clarify structure
blanchet
parents:
55194
diff
changeset

38 
open Sledgehammer_Isar_Compress 
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 

69593  48 
val trace = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_isar_trace\<close> (K false) 
55222  49 

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

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

56 
val veriT_simp_arith_rule = "simp_arith" 
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
72401
diff
changeset

57 
val veriT_skolemize_rules = Verit_Proof.skolemization_steps 
58061  58 
val z3_skolemize_rule = Z3_Proof.string_of_rule Z3_Proof.Skolemize 
59 
val z3_th_lemma_rule_prefix = Z3_Proof.string_of_rule (Z3_Proof.Th_Lemma "") 

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

60 
val zipperposition_cnf_rule = "cnf" 
54746  61 

54772  62 
val skolemize_rules = 
57785  63 
[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@mpiinf.mpg.de>
parents:
72401
diff
changeset

64 
spass_skolemize_rule, vampire_skolemisation_rule, z3_skolemize_rule, 
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpiinf.mpg.de>
parents:
72401
diff
changeset

65 
zipperposition_cnf_rule] @ veriT_skolemize_rules 
54746  66 

58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

67 
fun is_ext_rule rule = (rule = leo2_extcnf_equal_neg_rule) 
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

68 
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 LEOII and Satallax
blanchet
parents:
58517
diff
changeset

69 

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

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

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

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

50005  79 

58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

80 
fun add_global_fact ss = apsnd (union (op =) ss) 
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

81 

4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

82 
fun add_fact_of_dependency [(_, ss as _ :: _)] = add_global_fact ss 
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

83 
 add_fact_of_dependency names = apfst (insert (op =) (label_of_clause names)) 
49914  84 

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

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

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

89 
line :: lines 
69593  90 
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

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

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

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

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

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

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

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

57771  100 
fun add_lines_pass2 res [] = rev res 
101 
 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

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

105 

57771  106 
val norm_t = normalize role t 
107 
val is_duplicate = 

108 
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

109 
(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

110 
(member (op =) deps prev_name andalso 
1fc93ea5136b
eliminate duplicate hypotheses (which can arise due to (un)clausification)
blanchet
parents:
58506
diff
changeset

111 
Term.aconv_untyped (normalize prev_role prev_t, norm_t))) 
57771  112 
res 
57770
6c4ab6f0a6fc
normalize conjectures vs. negated conjectures when comparing terms
blanchet
parents:
57769
diff
changeset

113 

69593  114 
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

115 

6e2295db4cf8
keep formula right before skolemization, because the universal variables might be different (or differently ordered) as in the original axiom or negated conjecture from which it was skolemized
blanchet
parents:
55183
diff
changeset

116 
fun is_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

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

118 

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

119 
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

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

122 
(role = Plain andalso not (is_skolemize_rule rule) andalso 
58653
4b44c227c0e0
improved handling of extensionality in Isar proofs generated from LEOII and Satallax
blanchet
parents:
58517
diff
changeset

123 
not (is_ext_rule rule) andalso not (is_arith_rule rule) andalso 
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
72355
diff
changeset

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

126 
else 
57771  127 
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

128 
end 
49914  129 

130 
type isar_params = 

57783  131 
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

132 
* (term, string) atp_step list * thm 
49914  133 

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

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

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

136 
val basic_arith_methods = [Linarith_Method, Presburger_Method, Algebra_Method] 
55311  137 

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

138 
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

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

140 
basic_systematic_methods @ basic_arith_methods @ basic_simp_based_methods @ 
57699  141 
[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

142 
val rewrite_methods = basic_simp_based_methods @ basic_systematic_methods @ basic_arith_methods 
58517  143 
val skolem_methods = Moura_Method :: systematic_methods 
54766
6ac273f176cd
store alternative proof methods in Isar data structure
blanchet
parents:
54765
diff
changeset

144 

60612
79d71bfea310
removed chained facts from preplaying  and careful about extra chained facts when removing 'proof ' and 'qed' from oneline Isar proofs
blanchet
parents:
59577
diff
changeset

145 
fun isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params 
57739  146 
(one_line_params as ((used_facts, (_, one_line_play)), banner, subgoal, subgoal_count)) = 
49883  147 
let 
58843  148 
val _ = if debug then writeln "Constructing Isar proof..." else () 
56097  149 

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

150 
fun generate_proof_text () = 
49883  151 
let 
57791  152 
val (verbose, alt_metis_args, preplay_timeout, compress, try0, minimize, atp_proof0, goal) = 
57245  153 
isar_params () 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

154 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

155 
if null atp_proof0 then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

156 
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

157 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

158 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

159 
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

160 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

161 
fun massage_methods (meths as meth :: _) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

162 
if not try0 then [meth] 
72518
4be6ae020fc4
Added smt (verit) to Sledgehammer's proof preplay.
desharna
parents:
72513
diff
changeset

163 
else if smt_proofs then SMT_Method SMT_Default :: meths 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

165 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

166 
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

167 
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

168 
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

169 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

170 
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

171 
val compress = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

172 
(case compress of 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

173 
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

174 
 SOME n => n) 
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 
fun is_fixed ctxt = Variable.is_declared ctxt orf Name.is_skolem 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

177 
fun skolems_of ctxt t = Term.add_frees t [] > filter_out (is_fixed ctxt o fst) > rev 
54700  178 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

179 
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

180 
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

181 

72355  182 
val trace = Config.get ctxt trace 
183 

184 
val string_of_atp_steps = 

185 
let val to_string = ATP_Proof.string_of_atp_step (Syntax.string_of_term ctxt) I in 

186 
enclose "[\n" "\n]" o cat_lines o map (enclose " " "," o to_string) 

187 
end 

188 

189 
val atp_proof = atp_proof0 

190 
> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps) 

191 
> (fn x => fold_rev add_line_pass1 x []) 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

192 
> add_lines_pass2 [] 
72355  193 
> 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

194 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

195 
val conjs = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

196 
map_filter (fn (name, role, _, _, _) => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

197 
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

198 
atp_proof 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

199 
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

200 

72584  201 
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

202 
let 
72584  203 
val (skos, proof_methods) = 
204 
(if is_skolemize_rule rule then (skolems_of ctxt goal, skolem_methods) 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

205 
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

206 
else ([], rewrite_methods)) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

207 
> massage_methods 
72584  208 
val prove = Prove { 
209 
qualifiers = [], 

210 
obtains = skos, 

211 
label = label, 

212 
goal = goal, 

213 
subproofs = [], 

214 
facts = ([], []), 

215 
proof_methods = proof_methods, 

216 
comment = ""} 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

217 
in 
72584  218 
(prove, ctxt > not (null skos) ? (Variable.add_fixes (map fst skos) #> snd)) 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

220 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

221 
val (lems, _) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

222 
fold_map add_lemma (map_filter (get_role (curry (op =) Lemma)) atp_proof) ctxt 
54700  223 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

224 
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

225 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

226 
val refute_graph = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

227 
atp_proof 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

228 
> map (fn (name, _, _, _, from) => (from, name)) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

229 
> make_refute_graph bot 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

231 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

232 
val axioms = axioms_of_refute_graph refute_graph conjs 
54700  233 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

234 
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

235 
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

236 
val steps = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

237 
Symtab.empty 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

239 
Symtab.update_new (s, (rule, t 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

240 
> (if is_clause_tainted [name] then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

241 
HOLogic.dest_Trueprop 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

242 
#> role <> Conjecture ? s_not 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

243 
#> 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

244 
#> HOLogic.mk_Trueprop 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

245 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

246 
I)))) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

247 
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

248 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

249 
fun is_referenced_in_step _ (Let _) = false 
72584  250 
 is_referenced_in_step l (Prove {subproofs, facts = (ls, _), ...}) = 
251 
member (op =) ls l orelse exists (is_referenced_in_proof l) subproofs 

72582  252 
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

253 
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

254 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

255 
fun insert_lemma_in_step lem 
72584  256 
(step as Prove {qualifiers, obtains, label, goal, subproofs, facts = (ls, gs), 
257 
proof_methods, comment}) = 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

258 
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

259 
if member (op =) ls l' then 
58517  260 
[lem, step] 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

261 
else 
72584  262 
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

263 
if length (filter I refs) = 1 then 
72584  264 
[Prove { 
265 
qualifiers = qualifiers, 

266 
obtains = obtains, 

267 
label = label, 

268 
goal = goal, 

269 
subproofs = 

270 
map2 (fn false => I  true => insert_lemma_in_proof lem) refs subproofs, 

271 
facts = (ls, gs), 

272 
proof_methods = proof_methods, 

273 
comment = comment}] 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

274 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

275 
[lem, step] 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

276 
end 
58517  277 
end 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

278 
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

279 
 insert_lemma_in_steps lem (step :: steps) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

280 
if is_referenced_in_step (the (label_of_isar_step lem)) step then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

281 
insert_lemma_in_step lem step @ steps 
54700  282 
else 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

283 
step :: insert_lemma_in_steps lem steps 
72583  284 
and insert_lemma_in_proof lem (proof as Proof {steps, ...}) = 
72585  285 
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

286 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

287 
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

288 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

289 
val finish_off = close_form #> rename_bound_vars 
54755  290 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

291 
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

292 
 prop_of_clause names = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

293 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

294 
val lits = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

295 
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

296 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

297 
(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

298 
(negs as _ :: _, pos as _ :: _) => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

299 
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

300 
Library.foldr1 s_disj pos) 
69593  301 
 _ => 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

302 
end 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

303 
> HOLogic.mk_Trueprop > finish_off 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

304 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

305 
fun maybe_show outer c = if outer andalso eq_set (op =) (c, conjs) then [Show] else [] 
55280  306 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

307 
fun isar_steps outer predecessor accum [] = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

308 
accum 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

309 
> (if tainted = [] then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

310 
(* e.g., trivial, empty proof by Z3 *) 
72584  311 
cons (Prove { 
312 
qualifiers = if outer then [Show] else [], 

313 
obtains = [], 

314 
label = no_label, 

315 
goal = concl_t, 

316 
subproofs = [], 

317 
facts = sort_facts (the_list predecessor, []), 

318 
proof_methods = massage_methods systematic_methods', 

319 
comment = ""}) 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

320 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

321 
I) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

322 
> rev 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

323 
 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

324 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

325 
val l = label_of_clause c 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

326 
val t = prop_of_clause c 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

327 
val rule = rule_of_clause_id id 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

328 
val skolem = is_skolemize_rule rule 
54700  329 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

330 
val deps = ([], []) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

331 
> fold add_fact_of_dependency gamma 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

333 
> sort_facts 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

334 
val meths = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

335 
(if skolem then skolem_methods 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

336 
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

337 
else systematic_methods') 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

339 

72584  340 
fun prove subproofs facts = Prove { 
341 
qualifiers = maybe_show outer c, 

342 
obtains = [], 

343 
label = l, 

344 
goal = t, 

345 
subproofs = subproofs, 

346 
facts = facts, 

347 
proof_methods = meths, 

348 
comment = ""} 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

349 
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

350 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

351 
if is_clause_tainted c then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

352 
(case gamma of 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

353 
[g] => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

354 
if skolem andalso is_clause_tainted g then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

355 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

356 
val skos = skolems_of ctxt (prop_of_clause g) 
72582  357 
val subproof = Proof {fixes = skos, assumptions = [], steps = rev accum} 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

358 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

359 
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

360 
end 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

361 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

362 
steps_of_rest (prove [] deps) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

363 
 _ => steps_of_rest (prove [] deps)) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

364 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

365 
steps_of_rest 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

366 
(if skolem then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

367 
(case skolems_of ctxt t of 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

368 
[] => prove [] deps 
72584  369 
 skos => Prove { 
370 
qualifiers = [], 

371 
obtains = skos, 

372 
label = l, 

373 
goal = t, 

374 
subproofs = [], 

375 
facts = deps, 

376 
proof_methods = meths, 

377 
comment = ""}) 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

378 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

379 
prove [] deps) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

380 
end 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

381 
 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

382 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

383 
fun isar_case (c, subinfs) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

384 
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

385 
val c = succedent_of_cases cases 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

386 
val l = label_of_clause c 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

387 
val t = prop_of_clause c 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

388 
val step = 
72584  389 
Prove { 
390 
qualifiers = maybe_show outer c, 

391 
obtains = [], 

392 
label = l, 

393 
goal = t, 

394 
subproofs = map isar_case (filter_out (null o snd) cases), 

395 
facts = sort_facts (the_list predecessor, []), 

396 
proof_methods = massage_methods systematic_methods', 

397 
comment = ""} 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

398 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

399 
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

400 
end 
72582  401 
and isar_proof outer fixes assumptions lems infs = 
402 
let val steps = fold_rev insert_lemma_in_steps lems (isar_steps outer NONE [] infs) in 

403 
Proof {fixes = fixes, assumptions = assumptions, steps = steps} 

404 
end 

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

405 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

406 
val canonical_isar_proof = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

407 
refute_graph 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

409 
> redirect_graph axioms tainted bot 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

411 
> isar_proof true params assms lems 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

412 
> postprocess_isar_proof_remove_show_stuttering 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

414 
> relabel_isar_proof_canonically 
54754  415 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

416 
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

417 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

418 
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

419 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

420 
val _ = fold_isar_steps (fn meth => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

421 
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

422 
(steps_of_isar_proof canonical_isar_proof) () 
55299  423 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

424 
fun str_of_preplay_outcome outcome = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

425 
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

426 
fun str_of_meth l meth = 
72401
2783779b7dd3
removed obsolete unmaintained experimental prover Pirate
blanchet
parents:
72355
diff
changeset

427 
string_of_proof_method [] meth ^ " " ^ 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

428 
str_of_preplay_outcome 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

429 
(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

430 
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

431 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

432 
fun trace_isar_proof label proof = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

433 
if trace then 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

434 
tracing (timestamp () ^ "\n" ^ label ^ ":\n\n" ^ 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

435 
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

436 
(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

437 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

438 
() 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

439 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

440 
fun comment_of l (meth :: _) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

441 
(case (verbose, 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

442 
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

443 
(false, Played _) => "" 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

444 
 (_, outcome) => string_of_play_outcome outcome) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

445 

0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

446 
val (play_outcome, isar_proof) = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

447 
canonical_isar_proof 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

448 
> tap (trace_isar_proof "Original") 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

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

450 
> tap (trace_isar_proof "Compressed") 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

451 
> postprocess_isar_proof_remove_unreferenced_steps 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

452 
(keep_fastest_method_of_isar_step (!preplay_data) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

453 
#> 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

454 
> tap (trace_isar_proof "Minimized") 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

455 
> `(preplay_outcome_of_isar_proof (!preplay_data)) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

456 
> (comment_isar_proof comment_of 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

457 
#> chain_isar_proof 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

458 
#> kill_useless_labels_in_isar_proof 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

459 
#> relabel_isar_proof_nicely 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

460 
#> rationalize_obtains_in_isar_proofs ctxt) 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

461 
in 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

462 
(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

463 
(0, 1) => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

464 
one_line_proof_text ctxt 0 
67560  465 
(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

466 
(case isar_proof of 
72584  467 
Proof {steps = [Prove {facts = (_, gfs), proof_methods = meth :: _, ...}], 
468 
...} => 

62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

469 
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

470 
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

471 
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

472 
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

473 
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

474 
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

475 
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

476 
SOME (s, (Global, General))) gfs 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

477 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

478 
((used_facts', (meth, play_outcome)), banner, subgoal, subgoal_count) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

479 
end) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

480 
else 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

481 
one_line_params) ^ 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

482 
(if isar_proofs = SOME true then "\n(No Isar proof available.)" else "") 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

483 
 (_, num_steps) => 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

484 
let 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

485 
val msg = 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

486 
(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

487 
else []) @ 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

488 
(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

489 
in 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

490 
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

491 
"\n\nIsar proof" ^ (commas msg > not (null msg) ? enclose " (" ")") ^ ":\n" ^ 
63518  492 
Active.sendback_markup_command 
62220
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

493 
(string_of_isar_proof ctxt subgoal subgoal_count isar_proof) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

494 
end) 
0e17a97234bd
avoid error in Isar proof reconstruction if no ATP proof is available
blanchet
parents:
60612
diff
changeset

495 
end 
49883  496 
end 
57056  497 
in 
57287
68aa585269ac
given two oneliners, only show the best of the two
blanchet
parents:
57286
diff
changeset

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

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

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

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

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

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

504 
one_line_proof_text ctxt 0 one_line_params ^ 
63692  505 
(if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else "")) 
57056  506 
end 
49883  507 

72355  508 
fun isar_proof_would_be_a_good_idea (_, play) = 
54824  509 
(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

510 
Played _ => false 
62826  511 
 Play_Timed_Out time => time > Time.zeroTime 
56093  512 
 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

513 

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

514 
fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained 
57739  515 
(one_line_params as ((_, preplay), _, _, _)) = 
51190
2654b3965c8d
made "isar_proofs" a 3way option, to provide a way to totally disable isar_proofs if desired
blanchet
parents:
51187
diff
changeset

516 
(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

517 
(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 oneline Isar proofs
blanchet
parents:
59577
diff
changeset

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

520 
one_line_proof_text ctxt num_chained) one_line_params 
49883  521 

522 
end; 