author  blanchet 
Tue, 27 Jul 2010 12:01:02 +0200  
changeset 38007  f0a4aa17f23f 
parent 37998  f1b7fb87f523 
child 38014  81c23d286f0c 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML 
33310  2 
Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory 
36392  3 
Author: Jasmin Blanchette, TU Muenchen 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

4 

33310  5 
Transfer of proofs from external provers. 
6 
*) 

7 

35826  8 
signature SLEDGEHAMMER_PROOF_RECONSTRUCT = 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

9 
sig 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

10 
type minimize_command = string list > string 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

11 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

12 
val metis_line: bool > int > int > string list > string 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

13 
val metis_proof_text: 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

14 
bool * minimize_command * string * string vector * thm * int 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

15 
> string * string list 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

16 
val isar_proof_text: 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

17 
string Symtab.table * bool * int * Proof.context * int list 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

18 
> bool * minimize_command * string * string vector * thm * int 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

19 
> string * string list 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

20 
val proof_text: 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

21 
bool > string Symtab.table * bool * int * Proof.context * int list 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

22 
> bool * minimize_command * string * string vector * thm * int 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

23 
> string * string list 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

24 
end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

25 

35826  26 
structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

27 
struct 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

28 

37578
9367cb36b1c4
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
blanchet
parents:
37577
diff
changeset

29 
open Metis_Clauses 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

30 
open Sledgehammer_Util 
37616
c8d2d84d6011
always perform relevance filtering on original formulas
blanchet
parents:
37578
diff
changeset

31 
open Sledgehammer_Fact_Filter 
37624  32 
open Sledgehammer_TPTP_Format 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

33 

36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

34 
type minimize_command = string list > string 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

35 

37991  36 
fun mk_anot phi = AConn (ANot, [phi]) 
37 
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) 

38 

37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

39 
val index_in_shape : int > int list > int = find_index o curry (op =) 
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

40 
fun is_axiom_clause_number thm_names num = 
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

41 
num > 0 andalso num <= Vector.length thm_names andalso 
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

42 
Vector.sub (thm_names, num  1) <> "" 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

43 
fun is_conjecture_clause_number conjecture_shape num = 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

44 
index_in_shape num conjecture_shape >= 0 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

45 

37991  46 
fun negate_term (Const (@{const_name All}, T) $ Abs (s, T', t')) = 
47 
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term t') 

48 
 negate_term (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = 

49 
Const (@{const_name All}, T) $ Abs (s, T', negate_term t') 

50 
 negate_term (@{const "op >"} $ t1 $ t2) = 

51 
@{const "op &"} $ t1 $ negate_term t2 

52 
 negate_term (@{const "op &"} $ t1 $ t2) = 

53 
@{const "op "} $ negate_term t1 $ negate_term t2 

54 
 negate_term (@{const "op "} $ t1 $ t2) = 

55 
@{const "op &"} $ negate_term t1 $ negate_term t2 

56 
 negate_term (@{const Not} $ t) = t 

57 
 negate_term t = @{const Not} $ t 

58 

36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

59 
datatype ('a, 'b, 'c, 'd, 'e) raw_step = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

60 
Definition of 'a * 'b * 'c  
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

61 
Inference of 'a * 'd * 'e list 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

62 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

63 
(**** PARSING OF TSTP FORMAT ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

64 

37991  65 
datatype int_or_string = Str of string  Int of int 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

66 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

67 
(*Strings enclosed in single quotes, e.g. filenames*) 
37991  68 
val scan_quoted = $$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

69 

37991  70 
val scan_dollar_name = 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

71 
Scan.repeat ($$ "$")  Symbol.scan_id >> (fn (ss, s) => implode ss ^ s) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

72 

36369
d2cd0d04b8e6
handle ATP proof delimiters in a cleaner, more extensible fashion
blanchet
parents:
36293
diff
changeset

73 
(* needed for SPASS's output format *) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

74 
fun repair_name _ "$true" = "c_True" 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

75 
 repair_name _ "$false" = "c_False" 
38007  76 
 repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

77 
 repair_name _ "equal" = "c_equal" (* probably not needed *) 
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37643
diff
changeset

78 
 repair_name pool s = Symtab.lookup pool s > the_default s 
36392  79 
(* Generalized firstorder terms, which include file names, numbers, etc. *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

80 
(* The "x" argument is not strictly necessary, but without it Poly/ML loops 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

81 
forever at compile time. *) 
37991  82 
fun parse_generalized_term x = 
83 
(scan_quoted >> (fn s => ATerm (Str s, [])) 

84 
 scan_dollar_name 

85 
 Scan.optional ($$ "("  parse_generalized_terms  $$ ")") [] 

86 
>> (fn (s, gs) => ATerm (Str s, gs)) 

87 
 scan_integer >> (fn k => ATerm (Int k, [])) 

88 
 $$ "("  parse_generalized_term  $$ ")" 

89 
 $$ "["  Scan.optional parse_generalized_terms []  $$ "]" 

90 
>> curry ATerm (Str "list")) x 

91 
and parse_generalized_terms x = 

92 
(parse_generalized_term ::: Scan.repeat ($$ ","  parse_generalized_term)) x 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

93 
fun parse_term pool x = 
37991  94 
((scan_dollar_name >> repair_name pool) 
95 
 Scan.optional ($$ "("  parse_terms pool  $$ ")") [] >> ATerm) x 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

96 
and parse_terms pool x = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

97 
(parse_term pool ::: Scan.repeat ($$ ","  parse_term pool)) x 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

98 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

99 
fun parse_predicate_term pool = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

100 
parse_term pool  Scan.option (Scan.option ($$ "!")  $$ "=" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

101 
 parse_term pool) 
37991  102 
>> (fn (u, NONE) => APred u 
103 
 (u1, SOME (NONE, u2)) => APred (ATerm ("c_equal", [u1, u2])) 

104 
 (u1, SOME (SOME _, u2)) => 

105 
mk_anot (APred (ATerm ("c_equal", [u1, u2])))) 

106 

107 
fun fo_term_head (ATerm (s, _)) = s 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

108 

37991  109 
(* TPTP formulas are fully parenthesized, so we don't need to worry about 
110 
operator precedence. *) 

111 
fun parse_formula pool x = 

112 
(($$ "("  parse_formula pool  $$ ")" 

113 
 ($$ "!" >> K AForall  $$ "?" >> K AExists) 

114 
 $$ "["  parse_terms pool  $$ "]"  $$ ":" 

115 
 parse_formula pool 

116 
>> (fn ((q, ts), phi) => AQuant (q, map fo_term_head ts, phi)) 

117 
 $$ "~"  parse_formula pool >> mk_anot 

118 
 parse_predicate_term pool) 

119 
 Scan.option ((Scan.this_string "=>" >> K AImplies 

120 
 Scan.this_string "<=>" >> K AIff 

121 
 Scan.this_string "<~>" >> K ANotIff 

122 
 Scan.this_string "<=" >> K AIf 

123 
 $$ "" >> K AOr  $$ "&" >> K AAnd) 

124 
 parse_formula pool) 

125 
>> (fn (phi1, NONE) => phi1 

126 
 (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x 

127 

128 
fun ints_of_generalized_term (ATerm (label, gs)) = 

129 
fold ints_of_generalized_term gs #> (case label of Int k => cons k  _ => I) 

36392  130 
val parse_tstp_annotations = 
37991  131 
Scan.optional ($$ ","  parse_generalized_term 
132 
 Scan.option ($$ ","  parse_generalized_terms) 

133 
>> (fn g => ints_of_generalized_term g [])) [] 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

134 

37991  135 
(* Syntax: (fofcnf)\(<num>, <formula_role>, <cnf_formula> <annotations>\). 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

136 
The <num> could be an identifier, but we assume integers. *) 
37991  137 
fun parse_tstp_line pool = 
138 
((Scan.this_string "fof"  Scan.this_string "cnf")  $$ "(") 

139 
 scan_integer  $$ ","  Symbol.scan_id  $$ "," 

140 
 parse_formula pool  parse_tstp_annotations  $$ ")"  $$ "." 

141 
>> (fn (((num, role), phi), deps) => 

142 
case role of 

143 
"definition" => 

144 
(case phi of 

38007  145 
AConn (AIff, [phi1 as APred _, phi2]) => 
146 
Definition (num, phi1, phi2) 

147 
 APred (ATerm ("$$e", _)) => 

148 
Inference (num, phi, deps) (* Vampire's equality proxy axiom *) 

37991  149 
 _ => raise Fail "malformed definition") 
150 
 _ => Inference (num, phi, deps)) 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

151 

b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

152 
(**** PARSING OF SPASS OUTPUT ****) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

153 

36392  154 
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role 
155 
is not clear anyway. *) 

37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

156 
val parse_dot_name = scan_integer  $$ "."  scan_integer 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

157 

36392  158 
val parse_spass_annotations = 
159 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

160 
 Scan.option ($$ ","))) [] 

36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

161 

36574  162 
(* It is not clear why some literals are followed by sequences of stars and/or 
163 
pluses. We ignore them. *) 

164 
fun parse_decorated_predicate_term pool = 

36562
c6c2661bf08e
the SPASS output syntax is more general than I thought  such a pity that there's no documentation
blanchet
parents:
36560
diff
changeset

165 
parse_predicate_term pool  Scan.repeat ($$ "*"  $$ "+"  $$ " ") 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

166 

37991  167 
fun mk_horn ([], []) = APred (ATerm ("c_False", [])) 
168 
 mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits 

169 
 mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits) 

170 
 mk_horn (neg_lits, pos_lits) = 

171 
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, 

172 
foldr1 (mk_aconn AOr) pos_lits) 

173 

36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

174 
fun parse_horn_clause pool = 
36574  175 
Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ "" 
176 
 Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ ">" 

177 
 Scan.repeat (parse_decorated_predicate_term pool) 

37991  178 
>> (mk_horn o apfst (op @)) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

179 

36558
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

180 
(* Syntax: <num>[0:<inference><annotations>] 
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

181 
<cnf_formulas>  <cnf_formulas> > <cnf_formulas>. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

182 
fun parse_spass_line pool = 
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

183 
scan_integer  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 
36558
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

184 
 parse_spass_annotations  $$ "]"  parse_horn_clause pool  $$ "." 
37991  185 
>> (fn ((num, deps), u) => Inference (num, u, deps)) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

186 

36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

187 
fun parse_line pool = parse_tstp_line pool  parse_spass_line pool 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

188 
fun parse_lines pool = Scan.repeat1 (parse_line pool) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

189 
fun parse_proof pool = 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

190 
fst o Scan.finite Symbol.stopper 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

191 
(Scan.error (!! (fn _ => raise Fail "unrecognized ATP output") 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

192 
(parse_lines pool))) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

193 
o explode o strip_spaces 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

194 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

195 
(**** INTERPRETATION OF TSTP SYNTAX TREES ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

196 

37991  197 
exception FO_TERM of string fo_term list 
37994
b04307085a09
make TPTP generator accept full firstorder formulas
blanchet
parents:
37991
diff
changeset

198 
exception FORMULA of (string, string fo_term) formula list 
37991  199 
exception SAME of unit 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

200 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

201 
(* Type variables are given the basic sort "HOL.type". Some will later be 
37991  202 
constrained by information from type literals, or by type inference. *) 
203 
fun type_from_fo_term tfrees (u as ATerm (a, us)) = 

204 
let val Ts = map (type_from_fo_term tfrees) us in 

205 
case strip_prefix_and_undo_ascii type_const_prefix a of 

206 
SOME b => Type (invert_const b, Ts) 

207 
 NONE => 

208 
if not (null us) then 

209 
raise FO_TERM [u] (* only "tconst"s have type arguments *) 

210 
else case strip_prefix_and_undo_ascii tfree_prefix a of 

211 
SOME b => 

212 
let val s = "'" ^ b in 

213 
TFree (s, AList.lookup (op =) tfrees s > the_default HOLogic.typeS) 

214 
end 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

215 
 NONE => 
37991  216 
case strip_prefix_and_undo_ascii tvar_prefix a of 
217 
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

218 
 NONE => 
37991  219 
(* Variable from the ATP, say "X1" *) 
220 
Type_Infer.param 0 (a, HOLogic.typeS) 

221 
end 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

222 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

223 
fun fix_atp_variable_name s = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

224 
let 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

225 
fun subscript_name s n = s ^ nat_subscript n 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

226 
val s = String.map Char.toLower s 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

227 
in 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

228 
case space_explode "_" s of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

229 
[_] => (case take_suffix Char.isDigit (String.explode s) of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

230 
(cs1 as _ :: _, cs2 as _ :: _) => 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

231 
subscript_name (String.implode cs1) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

232 
(the (Int.fromString (String.implode cs2))) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

233 
 (_, _) => s) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

234 
 [s1, s2] => (case Int.fromString s2 of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

235 
SOME n => subscript_name s1 n 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

236 
 NONE => s) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

237 
 _ => s 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

238 
end 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

239 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

240 
(* Firstorder translation. No types are known for variables. "HOLogic.typeT" 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

241 
should allow them to be inferred.*) 
37991  242 
fun term_from_fo_term thy full_types tfrees opt_T = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

243 
let 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

244 
fun aux opt_T extra_us u = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

245 
case u of 
37991  246 
ATerm ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 
247 
 ATerm ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 

248 
 ATerm (a, us) => 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

249 
if a = type_wrapper_name then 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

250 
case us of 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

251 
[typ_u, term_u] => 
37991  252 
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u 
253 
 _ => raise FO_TERM us 

254 
else case strip_prefix_and_undo_ascii const_prefix a of 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

255 
SOME "equal" => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

256 
list_comb (Const (@{const_name "op ="}, HOLogic.typeT), 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

257 
map (aux NONE []) us) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

258 
 SOME b => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

259 
let 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

260 
val c = invert_const b 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

261 
val num_type_args = num_type_args thy c 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

262 
val (type_us, term_us) = 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

263 
chop (if full_types then 0 else num_type_args) us 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

264 
(* Extra args from "hAPP" come after any arguments given directly to 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

265 
the constant. *) 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

266 
val term_ts = map (aux NONE []) term_us 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

267 
val extra_ts = map (aux NONE []) extra_us 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

268 
val t = 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

269 
Const (c, if full_types then 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

270 
case opt_T of 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

271 
SOME T => map fastype_of term_ts > T 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

272 
 NONE => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

273 
if num_type_args = 0 then 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

274 
Sign.const_instance thy (c, []) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

275 
else 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

276 
raise Fail ("no type information for " ^ quote c) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

277 
else 
37998  278 
Sign.const_instance thy (c, 
279 
map (type_from_fo_term tfrees) type_us)) 

37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

280 
in list_comb (t, term_ts @ extra_ts) end 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

281 
 NONE => (* a free or schematic variable *) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

282 
let 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

283 
val ts = map (aux NONE []) (us @ extra_us) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

284 
val T = map fastype_of ts > HOLogic.typeT 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

285 
val t = 
37991  286 
case strip_prefix_and_undo_ascii fixed_var_prefix a of 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

287 
SOME b => Free (b, T) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

288 
 NONE => 
37991  289 
case strip_prefix_and_undo_ascii schematic_var_prefix a of 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

290 
SOME b => Var ((b, 0), T) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

291 
 NONE => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

292 
(* Variable from the ATP, say "X1" *) 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

293 
Var ((fix_atp_variable_name a, 0), T) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

294 
in list_comb (t, ts) end 
37991  295 
in aux opt_T [] end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

296 

36392  297 
(* Type class literal applied to a type. Returns triple of polarity, class, 
298 
type. *) 

37991  299 
fun type_constraint_from_formula pos tfrees (AConn (ANot, [u])) = 
300 
type_constraint_from_formula (not pos) tfrees u 

301 
 type_constraint_from_formula pos tfrees (phi as APred (ATerm (a, us))) = 

302 
(case (strip_prefix_and_undo_ascii class_prefix a, 

303 
map (type_from_fo_term tfrees) us) of 

304 
(SOME b, [T]) => (pos, b, T) 

305 
 _ => raise FORMULA [phi]) 

306 
 type_constraint_from_formula _ _ phi = raise FORMULA [phi] 

21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

307 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

308 
(** Accumulate type constraints in a clause: negative type literals **) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

309 

36485  310 
fun add_var (key, z) = Vartab.map_default (key, []) (cons z) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

311 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

312 
fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

313 
 add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

314 
 add_type_constraint _ = I 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

315 

36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

316 
fun is_positive_literal (@{const Not} $ _) = false 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

317 
 is_positive_literal _ = true 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

318 

36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

319 
val combinator_table = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

320 
[(@{const_name COMBI}, @{thm COMBI_def_raw}), 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

321 
(@{const_name COMBK}, @{thm COMBK_def_raw}), 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

322 
(@{const_name COMBB}, @{thm COMBB_def_raw}), 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

323 
(@{const_name COMBC}, @{thm COMBC_def_raw}), 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

324 
(@{const_name COMBS}, @{thm COMBS_def_raw})] 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

325 

8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

326 
fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

327 
 uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

328 
 uncombine_term (t as Const (x as (s, _))) = 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

329 
(case AList.lookup (op =) combinator_table s of 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

330 
SOME thm => thm > prop_of > specialize_type @{theory} x > Logic.dest_equals > snd 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

331 
 NONE => t) 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

332 
 uncombine_term t = t 
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

333 

37991  334 
fun disjuncts (AConn (AOr, phis)) = maps disjuncts phis 
335 
 disjuncts phi = [phi] 

336 

337 
(* Update schematic type variables with detected sort constraints. It's not 

338 
totally clear when this code is necessary. *) 

339 
fun repair_tvar_sorts (tvar_tab, t) = 

36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

340 
let 
37991  341 
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) 
342 
 do_type (TVar (xi, s)) = 

343 
TVar (xi, the_default s (Vartab.lookup tvar_tab xi)) 

344 
 do_type (TFree z) = TFree z 

345 
fun do_term (Const (a, T)) = Const (a, do_type T) 

346 
 do_term (Free (a, T)) = Free (a, do_type T) 

347 
 do_term (Var (xi, T)) = Var (xi, do_type T) 

348 
 do_term (t as Bound _) = t 

349 
 do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term t) 

350 
 do_term (t1 $ t2) = do_term t1 $ do_term t2 

351 
in t > not (Vartab.is_empty tvar_tab) ? do_term end 

352 

353 
fun s_disj (t1, @{const False}) = t1 

354 
 s_disj p = HOLogic.mk_disj p 

355 

356 
fun quantify_over_free quant_s free_s body_t = 

357 
case Term.add_frees body_t [] > filter (curry (op =) free_s o fst) of 

358 
[] => body_t 

359 
 frees as (_, free_T) :: _ => 

360 
Abs (free_s, free_T, fold (curry abstract_over) (map Free frees) body_t) 

361 

362 
(* Interpret a list of syntax trees as a clause, given by "real" literals and 

363 
sort constraints. Accumulates sort constraints in "tvar_tab", with "real" 

364 
literals in "lits". *) 

365 
fun prop_from_formula thy full_types tfrees = 

366 
let 

367 
val do_sort_constraint = 

368 
add_type_constraint o type_constraint_from_formula true tfrees 

369 
fun do_real_literal phi = 

370 
case phi of 

371 
AQuant (_, [], phi) => do_real_literal phi 

372 
 AQuant (q, x :: xs, phi') => 

373 
let 

374 
val body = do_real_literal (AQuant (q, xs, phi')) 

375 
val quant_s = case q of 

376 
AForall => @{const_name All} 

377 
 AExists => @{const_name Ex} 

378 
in quantify_over_free quant_s x body end 

379 
 AConn (ANot, [phi']) => HOLogic.mk_not (do_real_literal phi') 

380 
 AConn (c, [phi1, phi2]) => 

381 
(phi1, phi2) 

382 
> pairself do_real_literal 

383 
> (case c of 

384 
AAnd => HOLogic.mk_conj 

385 
 AOr => HOLogic.mk_disj 

386 
 AImplies => HOLogic.mk_imp 

387 
 AIff => (fn (t1, t2) => HOLogic.eq_const HOLogic.boolT $ t1 $ t2)) 

388 
 APred tm => 

389 
term_from_fo_term thy full_types tfrees (SOME @{typ bool}) tm 

390 
 _ => raise FORMULA [phi] 

391 
fun do_literals (tvar_tab, t) [] = (tvar_tab, t) 

392 
 do_literals (tvar_tab, t) (u :: us) = 

393 
(do_literals (tvar_tab > do_sort_constraint u, t) us 

394 
handle FO_TERM _ => raise SAME () 

395 
 FORMULA _ => raise SAME ()) 

396 
handle SAME () => 

397 
do_literals (tvar_tab, s_disj (do_real_literal u, t)) us 

398 
in 

399 
repair_tvar_sorts o do_literals (Vartab.empty, HOLogic.false_const) 

400 
o disjuncts 

401 
end 

402 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

403 
fun check_formula ctxt = 
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36968
diff
changeset

404 
Type_Infer.constrain @{typ bool} 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

405 
#> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic ctxt) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

406 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

407 

72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

408 
(**** Translation of TSTP files to Isar Proofs ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

409 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

410 
fun unvarify_term (Var ((s, 0), T)) = Free (s, T) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

411 
 unvarify_term t = raise TERM ("unvarify_term: nonVar", [t]) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

412 

37991  413 
fun decode_line full_types tfrees (Definition (num, phi1, phi2)) ctxt = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

414 
let 
37991  415 
val thy = ProofContext.theory_of ctxt 
416 
val t1 = prop_from_formula thy full_types tfrees phi1 

36551  417 
val vars = snd (strip_comb t1) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

418 
val frees = map unvarify_term vars 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

419 
val unvarify_args = subst_atomic (vars ~~ frees) 
37991  420 
val t2 = prop_from_formula thy full_types tfrees phi2 
36551  421 
val (t1, t2) = 
422 
HOLogic.eq_const HOLogic.typeT $ t1 $ t2 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

423 
> unvarify_args > uncombine_term > check_formula ctxt 
36555
8ff45c2076da
expand combinators in Isar proofs constructed by Sledgehammer;
blanchet
parents:
36551
diff
changeset

424 
> HOLogic.dest_eq 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

425 
in 
36551  426 
(Definition (num, t1, t2), 
427 
fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt) 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

428 
end 
37991  429 
 decode_line full_types tfrees (Inference (num, u, deps)) ctxt = 
36551  430 
let 
37991  431 
val thy = ProofContext.theory_of ctxt 
432 
val t = u > prop_from_formula thy full_types tfrees 

37998  433 
> uncombine_term > check_formula ctxt 
36551  434 
in 
435 
(Inference (num, t, deps), 

436 
fold Variable.declare_term (OldTerm.term_frees t) ctxt) 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

437 
end 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

438 
fun decode_lines ctxt full_types tfrees lines = 
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

439 
fst (fold_map (decode_line full_types tfrees) lines ctxt) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

440 

37323  441 
fun aint_actual_inference _ (Definition _) = true 
442 
 aint_actual_inference t (Inference (_, t', _)) = not (t aconv t') 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

443 

c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

444 
(* No "real" literals means only type information (tfree_tcs, clsrel, or 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

445 
clsarity). *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

446 
val is_only_type_information = curry (op aconv) HOLogic.true_const 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

447 

c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

448 
fun replace_one_dep (old, new) dep = if dep = old then new else [dep] 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

449 
fun replace_deps_in_line _ (line as Definition _) = line 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

450 
 replace_deps_in_line p (Inference (num, t, deps)) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

451 
Inference (num, t, fold (union (op =) o replace_one_dep p) deps []) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

452 

22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

453 
(*Discard axioms; consolidate adjacent lines that prove the same clause, since they differ 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

454 
only in type information.*) 
36551  455 
fun add_line _ _ (line as Definition _) lines = line :: lines 
456 
 add_line conjecture_shape thm_names (Inference (num, t, [])) lines = 

36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

457 
(* No dependencies: axiom, conjecture clause, or internal axioms or 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

458 
definitions (Vampire). *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

459 
if is_axiom_clause_number thm_names num then 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

460 
(* Axioms are not proof lines. *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

461 
if is_only_type_information t then 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

462 
map (replace_deps_in_line (num, [])) lines 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

463 
(* Is there a repetition? If so, replace later line by earlier one. *) 
37323  464 
else case take_prefix (aint_actual_inference t) lines of 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

465 
(_, []) => lines (*no repetition of proof line*) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

466 
 (pre, Inference (num', _, _) :: post) => 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

467 
pre @ map (replace_deps_in_line (num', [num])) post 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

468 
else if is_conjecture_clause_number conjecture_shape num then 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

469 
Inference (num, t, []) :: lines 
36551  470 
else 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

471 
map (replace_deps_in_line (num, [])) lines 
36551  472 
 add_line _ _ (Inference (num, t, deps)) lines = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

473 
(* Type information will be deleted later; skip repetition test. *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

474 
if is_only_type_information t then 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

475 
Inference (num, t, deps) :: lines 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

476 
(* Is there a repetition? If so, replace later line by earlier one. *) 
37323  477 
else case take_prefix (aint_actual_inference t) lines of 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

478 
(* FIXME: Doesn't this code risk conflating proofs involving different 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

479 
types?? *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

480 
(_, []) => Inference (num, t, deps) :: lines 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

481 
 (pre, Inference (num', t', _) :: post) => 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

482 
Inference (num, t', deps) :: 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

483 
pre @ map (replace_deps_in_line (num', [num])) post 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

484 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

485 
(* Recursively delete empty lines (type information) from the proof. *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

486 
fun add_nontrivial_line (Inference (num, t, [])) lines = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

487 
if is_only_type_information t then delete_dep num lines 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

488 
else Inference (num, t, []) :: lines 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

489 
 add_nontrivial_line line lines = line :: lines 
36395  490 
and delete_dep num lines = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

491 
fold_rev add_nontrivial_line (map (replace_deps_in_line (num, [])) lines) [] 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

492 

37323  493 
(* ATPs sometimes reuse free variable names in the strangest ways. Removing 
494 
offending lines often does the trick. *) 

36560
45c1870f234f
fixed definition of "bad frees" so that it actually works
blanchet
parents:
36559
diff
changeset

495 
fun is_bad_free frees (Free x) = not (member (op =) frees x) 
45c1870f234f
fixed definition of "bad frees" so that it actually works
blanchet
parents:
36559
diff
changeset

496 
 is_bad_free _ _ = false 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

497 

36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

498 
(* Vampire is keen on producing these. *) 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

499 
fun is_trivial_formula (@{const Not} $ (Const (@{const_name "op ="}, _) 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

500 
$ t1 $ t2)) = (t1 aconv t2) 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

501 
 is_trivial_formula _ = false 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

502 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

503 
fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = 
37323  504 
(j, line :: map (replace_deps_in_line (num, [])) lines) 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

505 
 add_desired_line isar_shrink_factor conjecture_shape thm_names frees 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

506 
(Inference (num, t, deps)) (j, lines) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

507 
(j + 1, 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

508 
if is_axiom_clause_number thm_names num orelse 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

509 
is_conjecture_clause_number conjecture_shape num orelse 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

510 
(not (is_only_type_information t) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

511 
null (Term.add_tvars t []) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

512 
not (exists_subterm (is_bad_free frees) t) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

513 
not (is_trivial_formula t) andalso 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

514 
(null lines orelse (* last line must be kept *) 
36924  515 
(length deps >= 2 andalso j mod isar_shrink_factor = 0))) then 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

516 
Inference (num, t, deps) :: lines (* keep line *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

517 
else 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

518 
map (replace_deps_in_line (num, deps)) lines) (* drop line *) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

519 

36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

520 
(** EXTRACTING LEMMAS **) 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

521 

37991  522 
(* A list consisting of the first number in each line is returned. For TSTP, 
523 
interesting lines have the form "fof(108, axiom, ...)", where the number 

524 
(108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where 

525 
the first number (108) is extracted. *) 

37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37926
diff
changeset

526 
fun extract_formula_numbers_in_atp_proof atp_proof = 
35865  527 
let 
37962
d7dbe01f48d7
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
blanchet
parents:
37961
diff
changeset

528 
val tokens_of = String.tokens (not o Char.isAlphaNum) 
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37926
diff
changeset

529 
fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num 
36395  530 
 extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num 
531 
 extract_num _ = NONE 

36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

532 
in atp_proof > split_lines > map_filter (extract_num o tokens_of) end 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

533 

34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

534 
val indent_size = 2 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

535 
val no_label = ("", ~1) 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

536 

34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

537 
val raw_prefix = "X" 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

538 
val assum_prefix = "A" 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

539 
val fact_prefix = "F" 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

540 

34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

541 
fun string_for_label (s, num) = s ^ string_of_int num 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

542 

34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

543 
fun metis_using [] = "" 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

544 
 metis_using ls = 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

545 
"using " ^ space_implode " " (map string_for_label ls) ^ " " 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

546 
fun metis_apply _ 1 = "by " 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

547 
 metis_apply 1 _ = "apply " 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

548 
 metis_apply i _ = "prefer " ^ string_of_int i ^ " apply " 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

549 
fun metis_name full_types = if full_types then "metisFT" else "metis" 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

550 
fun metis_call full_types [] = metis_name full_types 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

551 
 metis_call full_types ss = 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

552 
"(" ^ metis_name full_types ^ " " ^ space_implode " " ss ^ ")" 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

553 
fun metis_command full_types i n (ls, ss) = 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

554 
metis_using ls ^ metis_apply i n ^ metis_call full_types ss 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

555 
fun metis_line full_types i n ss = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

556 
"Try this command: " ^ 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

557 
Markup.markup Markup.sendback (metis_command full_types i n ([], ss)) ^ ".\n" 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

558 
fun minimize_line _ [] = "" 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

559 
 minimize_line minimize_command facts = 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

560 
case minimize_command facts of 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

561 
"" => "" 
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

562 
 command => 
36065  563 
"To minimize the number of lemmas, try this command: " ^ 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

564 
Markup.markup Markup.sendback command ^ ".\n" 
31840
beeaa1ed1f47
check if conjectures have been used in proof
immler@in.tum.de
parents:
31479
diff
changeset

565 

37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

566 
val unprefix_chained = perhaps (try (unprefix chained_prefix)) 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

567 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

568 
fun metis_proof_text (full_types, minimize_command, atp_proof, thm_names, goal, 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

569 
i) = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

570 
let 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

571 
val raw_lemmas = 
37961
6a48c85a211a
first step in using "fof" rather than "cnf" in TPTP problems
blanchet
parents:
37926
diff
changeset

572 
atp_proof > extract_formula_numbers_in_atp_proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

573 
> filter (is_axiom_clause_number thm_names) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

574 
> map (fn i => Vector.sub (thm_names, i  1)) 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

575 
val (chained_lemmas, other_lemmas) = 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

576 
raw_lemmas > List.partition (String.isPrefix chained_prefix) 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

577 
>> map (unprefix chained_prefix) 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

578 
> pairself (sort_distinct string_ord) 
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

579 
val lemmas = other_lemmas @ chained_lemmas 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

580 
val n = Logic.count_prems (prop_of goal) 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

581 
in 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

582 
(metis_line full_types i n other_lemmas ^ 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

583 
minimize_line minimize_command lemmas, lemmas) 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

584 
end 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
30874
diff
changeset

585 

36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

586 
(** Isar proof construction and manipulation **) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

587 

c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

588 
fun merge_fact_sets (ls1, ss1) (ls2, ss2) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

589 
(union (op =) ls1 ls2, union (op =) ss1 ss2) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

590 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

591 
type label = string * int 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

592 
type facts = label list * string list 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

593 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

594 
datatype qualifier = Show  Then  Moreover  Ultimately 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

595 

36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

596 
datatype step = 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

597 
Fix of (string * typ) list  
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

598 
Let of term * term  
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

599 
Assume of label * term  
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

600 
Have of qualifier list * label * term * byline 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

601 
and byline = 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

602 
ByMetis of facts  
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

603 
CaseSplit of step list list * facts 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

604 

36574  605 
fun smart_case_split [] facts = ByMetis facts 
606 
 smart_case_split proofs facts = CaseSplit (proofs, facts) 

607 

36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

608 
fun add_fact_from_dep thm_names num = 
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

609 
if is_axiom_clause_number thm_names num then 
36480
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

610 
apsnd (insert (op =) (Vector.sub (thm_names, num  1))) 
36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

611 
else 
36480
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

612 
apfst (insert (op =) (raw_prefix, num)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

613 

37998  614 
fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

615 
fun forall_vars t = fold_rev forall_of (map Var (Term.add_vars t [])) t 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

616 

37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

617 
fun step_for_line _ _ (Definition (_, t1, t2)) = Let (t1, t2) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

618 
 step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

619 
 step_for_line thm_names j (Inference (num, t, deps)) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

620 
Have (if j = 1 then [Show] else [], (raw_prefix, num), 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

621 
forall_vars t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

622 
ByMetis (fold (add_fact_from_dep thm_names) deps ([], []))) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

623 

36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

624 
fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

625 
atp_proof conjecture_shape thm_names params frees = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

626 
let 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

627 
val lines = 
37991  628 
atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: pick it up) *) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

629 
> parse_proof pool 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

630 
> decode_lines ctxt full_types tfrees 
36551  631 
> rpair [] > fold_rev (add_line conjecture_shape thm_names) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

632 
> rpair [] > fold_rev add_nontrivial_line 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

633 
> rpair (0, []) > fold_rev (add_desired_line isar_shrink_factor 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

634 
conjecture_shape thm_names frees) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

635 
> snd 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

636 
in 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

637 
(if null params then [] else [Fix params]) @ 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

638 
map2 (step_for_line thm_names) (length lines downto 1) lines 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

639 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

640 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

641 
(* When redirecting proofs, we keep information about the labels seen so far in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

642 
the "backpatches" data structure. The first component indicates which facts 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

643 
should be associated with forthcoming proof steps. The second component is a 
37322
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

644 
pair ("assum_ls", "drop_ls"), where "assum_ls" are the labels that should 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

645 
become assumptions and "drop_ls" are the labels that should be dropped in a 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

646 
case split. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

647 
type backpatches = (label * facts) list * (label list * label list) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

648 

36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

649 
fun used_labels_of_step (Have (_, _, _, by)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

650 
(case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

651 
ByMetis (ls, _) => ls 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

652 
 CaseSplit (proofs, (ls, _)) => 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

653 
fold (union (op =) o used_labels_of) proofs ls) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

654 
 used_labels_of_step _ = [] 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

655 
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

656 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

657 
fun new_labels_of_step (Fix _) = [] 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

658 
 new_labels_of_step (Let _) = [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

659 
 new_labels_of_step (Assume (l, _)) = [l] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

660 
 new_labels_of_step (Have (_, l, _, _)) = [l] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

661 
val new_labels_of = maps new_labels_of_step 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

662 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

663 
val join_proofs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

664 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

665 
fun aux _ [] = NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

666 
 aux proof_tail (proofs as (proof1 :: _)) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

667 
if exists null proofs then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

668 
NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

669 
else if forall (curry (op =) (hd proof1) o hd) (tl proofs) then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

670 
aux (hd proof1 :: proof_tail) (map tl proofs) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

671 
else case hd proof1 of 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

672 
Have ([], l, t, _) => (* FIXME: should we really ignore the "by"? *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

673 
if forall (fn Have ([], l', t', _) :: _ => (l, t) = (l', t') 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

674 
 _ => false) (tl proofs) andalso 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

675 
not (exists (member (op =) (maps new_labels_of proofs)) 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

676 
(used_labels_of proof_tail)) then 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

677 
SOME (l, t, map rev proofs, proof_tail) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

678 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

679 
NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

680 
 _ => NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

681 
in aux [] o map rev end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

682 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

683 
fun case_split_qualifiers proofs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

684 
case length proofs of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

685 
0 => [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

686 
 1 => [Then] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

687 
 _ => [Ultimately] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

688 

37991  689 
fun redirect_proof conjecture_shape hyp_ts concl_t proof = 
33310  690 
let 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

691 
(* The first pass outputs those steps that are independent of the negated 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

692 
conjecture. The second pass flips the proof by contradiction to obtain a 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

693 
direct proof, introducing case splits when an inference depends on 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

694 
several facts that depend on the negated conjecture. *) 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

695 
fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape) 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

696 
val concl_l = (raw_prefix, List.last conjecture_shape) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

697 
fun first_pass ([], contra) = ([], contra) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

698 
 first_pass ((step as Fix _) :: proof, contra) = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

699 
first_pass (proof, contra) >> cons step 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

700 
 first_pass ((step as Let _) :: proof, contra) = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

701 
first_pass (proof, contra) >> cons step 
37498
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

702 
 first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

703 
if l = concl_l then 
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

704 
first_pass (proof, contra > l = concl_l ? cons step) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

705 
else 
36551  706 
first_pass (proof, contra) >> cons (Assume (l, find_hyp num)) 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

707 
 first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

708 
let val step = Have (qs, l, t, ByMetis (ls, ss)) in 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

709 
if exists (member (op =) (fst contra)) ls then 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

710 
first_pass (proof, contra >> cons l > cons step) 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

711 
else 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

712 
first_pass (proof, contra) >> cons step 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

713 
end 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

714 
 first_pass _ = raise Fail "malformed proof" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

715 
val (proof_top, (contra_ls, contra_proof)) = 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

716 
first_pass (proof, ([concl_l], [])) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

717 
val backpatch_label = the_default ([], []) oo AList.lookup (op =) o fst 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

718 
fun backpatch_labels patches ls = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

719 
fold merge_fact_sets (map (backpatch_label patches) ls) ([], []) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

720 
fun second_pass end_qs ([], assums, patches) = 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

721 
([Have (end_qs, no_label, concl_t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

722 
ByMetis (backpatch_labels patches (map snd assums)))], patches) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

723 
 second_pass end_qs (Assume (l, t) :: proof, assums, patches) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

724 
second_pass end_qs (proof, (t, l) :: assums, patches) 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

725 
 second_pass end_qs (Have (qs, l, t, ByMetis (ls, ss)) :: proof, assums, 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

726 
patches) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

727 
if member (op =) (snd (snd patches)) l andalso 
37322
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

728 
not (member (op =) (fst (snd patches)) l) andalso 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

729 
not (AList.defined (op =) (fst patches) l) then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

730 
second_pass end_qs (proof, assums, patches > apsnd (append ls)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

731 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

732 
(case List.partition (member (op =) contra_ls) ls of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

733 
([contra_l], co_ls) => 
37322
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

734 
if member (op =) qs Show then 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

735 
second_pass end_qs (proof, assums, 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

736 
patches >> cons (contra_l, (co_ls, ss))) 
0347b1a16682
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
blanchet
parents:
37319
diff
changeset

737 
else 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

738 
second_pass end_qs 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

739 
(proof, assums, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

740 
patches >> cons (contra_l, (l :: co_ls, ss))) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

741 
>> cons (if member (op =) (fst (snd patches)) l then 
37991  742 
Assume (l, negate_term t) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

743 
else 
37991  744 
Have (qs, l, negate_term t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

745 
ByMetis (backpatch_label patches l))) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

746 
 (contra_ls as _ :: _, co_ls) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

747 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

748 
val proofs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

749 
map_filter 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

750 
(fn l => 
37996
11c076ea92e9
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
blanchet
parents:
37995
diff
changeset

751 
if l = concl_l then 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

752 
NONE 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

753 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

754 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

755 
val drop_ls = filter (curry (op <>) l) contra_ls 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

756 
in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

757 
second_pass [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

758 
(proof, assums, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

759 
patches > apfst (insert (op =) l) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

760 
> apsnd (union (op =) drop_ls)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

761 
> fst > SOME 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

762 
end) contra_ls 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

763 
val (assumes, facts) = 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

764 
if member (op =) (fst (snd patches)) l then 
37991  765 
([Assume (l, negate_term t)], (l :: co_ls, ss)) 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

766 
else 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

767 
([], (co_ls, ss)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

768 
in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

769 
(case join_proofs proofs of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

770 
SOME (l, t, proofs, proof_tail) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

771 
Have (case_split_qualifiers proofs @ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

772 
(if null proof_tail then end_qs else []), l, t, 
36574  773 
smart_case_split proofs facts) :: proof_tail 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

774 
 NONE => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

775 
[Have (case_split_qualifiers proofs @ end_qs, no_label, 
36574  776 
concl_t, smart_case_split proofs facts)], 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

777 
patches) 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

778 
>> append assumes 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

779 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

780 
 _ => raise Fail "malformed proof") 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

781 
 second_pass _ _ = raise Fail "malformed proof" 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

782 
val proof_bottom = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

783 
second_pass [Show] (contra_proof, [], ([], ([], []))) > fst 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

784 
in proof_top @ proof_bottom end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

785 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

786 
val kill_duplicate_assumptions_in_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

787 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

788 
fun relabel_facts subst = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

789 
apfst (map (fn l => AList.lookup (op =) subst l > the_default l)) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

790 
fun do_step (step as Assume (l, t)) (proof, subst, assums) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

791 
(case AList.lookup (op aconv) assums t of 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

792 
SOME l' => (proof, (l, l') :: subst, assums) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

793 
 NONE => (step :: proof, subst, (t, l) :: assums)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

794 
 do_step (Have (qs, l, t, by)) (proof, subst, assums) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

795 
(Have (qs, l, t, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

796 
case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

797 
ByMetis facts => ByMetis (relabel_facts subst facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

798 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

799 
CaseSplit (map do_proof proofs, relabel_facts subst facts)) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

800 
proof, subst, assums) 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

801 
 do_step step (proof, subst, assums) = (step :: proof, subst, assums) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

802 
and do_proof proof = fold do_step proof ([], [], []) > #1 > rev 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

803 
in do_proof end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

804 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

805 
val then_chain_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

806 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

807 
fun aux _ [] = [] 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

808 
 aux _ ((step as Assume (l, _)) :: proof) = step :: aux l proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

809 
 aux l' (Have (qs, l, t, by) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

810 
(case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

811 
ByMetis (ls, ss) => 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

812 
Have (if member (op =) ls l' then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

813 
(Then :: qs, l, t, 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

814 
ByMetis (filter_out (curry (op =) l') ls, ss)) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

815 
else 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

816 
(qs, l, t, ByMetis (ls, ss))) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

817 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

818 
Have (qs, l, t, CaseSplit (map (aux no_label) proofs, facts))) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

819 
aux l proof 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

820 
 aux _ (step :: proof) = step :: aux no_label proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

821 
in aux no_label end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

822 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

823 
fun kill_useless_labels_in_proof proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

824 
let 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

825 
val used_ls = used_labels_of proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

826 
fun do_label l = if member (op =) used_ls l then l else no_label 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

827 
fun do_step (Assume (l, t)) = Assume (do_label l, t) 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

828 
 do_step (Have (qs, l, t, by)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

829 
Have (qs, do_label l, t, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

830 
case by of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

831 
CaseSplit (proofs, facts) => 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

832 
CaseSplit (map (map do_step) proofs, facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

833 
 _ => by) 
36556
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

834 
 do_step step = step 
81dc2c20f052
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
blanchet
parents:
36555
diff
changeset

835 
in map do_step proof end 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

836 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

837 
fun prefix_for_depth n = replicate_string (n + 1) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

838 

1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

839 
val relabel_proof = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

840 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

841 
fun aux _ _ _ [] = [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

842 
 aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

843 
if l = no_label then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

844 
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

845 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

846 
let val l' = (prefix_for_depth depth assum_prefix, next_assum) in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

847 
Assume (l', t) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

848 
aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

849 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

850 
 aux subst depth (next_assum, next_fact) (Have (qs, l, t, by) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

851 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

852 
val (l', subst, next_fact) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

853 
if l = no_label then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

854 
(l, subst, next_fact) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

855 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

856 
let 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

857 
val l' = (prefix_for_depth depth fact_prefix, next_fact) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

858 
in (l', (l, l') :: subst, next_fact + 1) end 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

859 
val relabel_facts = 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

860 
apfst (map (fn l => 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

861 
case AList.lookup (op =) subst l of 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

862 
SOME l' => l' 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

863 
 NONE => raise Fail ("unknown label " ^ 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

864 
quote (string_for_label l)))) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

865 
val by = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

866 
case by of 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

867 
ByMetis facts => ByMetis (relabel_facts facts) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

868 
 CaseSplit (proofs, facts) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

869 
CaseSplit (map (aux subst (depth + 1) (1, 1)) proofs, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

870 
relabel_facts facts) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

871 
in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

872 
Have (qs, l', t, by) :: 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

873 
aux subst depth (next_assum, next_fact) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

874 
end 
36491
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

875 
 aux subst depth nextp (step :: proof) = 
6769f8eacaac
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
blanchet
parents:
36488
diff
changeset

876 
step :: aux subst depth nextp proof 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

877 
in aux [] 0 (1, 1) end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

878 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

879 
fun string_for_proof ctxt full_types i n = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

880 
let 
37319
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

881 
fun fix_print_mode f x = 
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

882 
setmp_CRITICAL show_no_free_types true 
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

883 
(setmp_CRITICAL show_types true 
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

884 
(Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
42268dc7d6c4
show types in Isar proofs, but not for free variables;
blanchet
parents:
37172
diff
changeset

885 
(print_mode_value ())) f)) x 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

886 
fun do_indent ind = replicate_string (ind * indent_size) " " 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

887 
fun do_free (s, T) = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

888 
maybe_quote s ^ " :: " ^ 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

889 
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

890 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": " 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

891 
fun do_have qs = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

892 
(if member (op =) qs Moreover then "moreover " else "") ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

893 
(if member (op =) qs Ultimately then "ultimately " else "") ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

894 
(if member (op =) qs Then then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

895 
if member (op =) qs Show then "thus" else "hence" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

896 
else 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

897 
if member (op =) qs Show then "show" else "have") 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

898 
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) 
36570
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

899 
fun do_facts (ls, ss) = 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

900 
let 
9bebcb40599f
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
blanchet
parents:
36567
diff
changeset

901 
val ls = ls > sort_distinct (prod_ord string_ord int_ord) 
37171
fc1e20373e6a
make sure chained facts appear in Isar proofs generated by Sledgehammer  otherwise the proof won't work
blanchet
parents:
36968
diff
changeset

902 
val ss = ss > map unprefix_chained > sort_distinct string_ord 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

903 
in metis_command full_types 1 1 (ls, ss) end 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

904 
and do_step ind (Fix xs) = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

905 
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

906 
 do_step ind (Let (t1, t2)) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

907 
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

908 
 do_step ind (Assume (l, t)) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

909 
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

910 
 do_step ind (Have (qs, l, t, ByMetis facts)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

911 
do_indent ind ^ do_have qs ^ " " ^ 
36479  912 
do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

913 
 do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

914 
space_implode (do_indent ind ^ "moreover\n") 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

915 
(map (do_block ind) proofs) ^ 
36479  916 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^ 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

917 
do_facts facts ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

918 
and do_steps prefix suffix ind steps = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

919 
let val s = implode (map (do_step ind) steps) in 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

920 
replicate_string (ind * indent_size  size prefix) " " ^ prefix ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

921 
String.extract (s, ind * indent_size, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

922 
SOME (size s  ind * indent_size  1)) ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

923 
suffix ^ "\n" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

924 
end 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

925 
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof 
36564
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

926 
(* Onestep proofs are pointless; better use the Metis oneliner 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

927 
directly. *) 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

928 
and do_proof [Have (_, _, _, ByMetis _)] = "" 
96f767f546e7
be more discriminate: some oneline Isar proofs are silly
blanchet
parents:
36563
diff
changeset

929 
 do_proof proof = 
36480
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

930 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

931 
do_indent 0 ^ "proof \n" ^ 
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

932 
do_steps "" "" 1 proof ^ 
1e01a7162435
polish Isar proofs: don't mention facts twice, and don't show oneliner "structured" proofs
blanchet
parents:
36479
diff
changeset

933 
do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" 
36488
32c92af68ec9
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
blanchet
parents:
36486
diff
changeset

934 
in do_proof end 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

935 

37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

936 
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

937 
(other_params as (full_types, _, atp_proof, thm_names, goal, 
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

938 
i)) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

939 
let 
37995
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset

940 
(* ### FIXME: avoid duplication with ATP_Systems  and move strip_subgoal 
06f02b15ef8a
generate full firstorder formulas (FOF) in Sledgehammer
blanchet
parents:
37994
diff
changeset

941 
to ATP_Systems *) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

942 
val (params, hyp_ts, concl_t) = strip_subgoal goal i 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

943 
val frees = fold Term.add_frees (concl_t :: hyp_ts) [] 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

944 
val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) [] 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

945 
val n = Logic.count_prems (prop_of goal) 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

946 
val (one_line_proof, lemma_names) = metis_proof_text other_params 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

947 
fun isar_proof_for () = 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

948 
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
36924  949 
atp_proof conjecture_shape thm_names params 
950 
frees 

37991  951 
> redirect_proof conjecture_shape hyp_ts concl_t 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

952 
> kill_duplicate_assumptions_in_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

953 
> then_chain_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

954 
> kill_useless_labels_in_proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

955 
> relabel_proof 
37479
f6b1ee5b420b
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
blanchet
parents:
37410
diff
changeset

956 
> string_for_proof ctxt full_types i n of 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

957 
"" => "" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

958 
 proof => "\nStructured proof:\n" ^ Markup.markup Markup.sendback proof 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

959 
val isar_proof = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

960 
if debug then 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

961 
isar_proof_for () 
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

962 
else 
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

963 
try isar_proof_for () 
36287
96f45c5ffb36
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
blanchet
parents:
36285
diff
changeset

964 
> the_default "Warning: The Isar proof construction failed.\n" 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

965 
in (one_line_proof ^ isar_proof, lemma_names) end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

966 

36557  967 
fun proof_text isar_proof isar_params other_params = 
968 
(if isar_proof then isar_proof_text isar_params else metis_proof_text) 

969 
other_params 

36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

970 

31038  971 
end; 