author  blanchet 
Tue, 24 Aug 2010 18:03:43 +0200  
changeset 38698  d19c3a7ce38b 
parent 38696  4c6b65d6a135 
child 38738  0ce517c1970f 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML 
38027  2 
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory 
3 
Author: Claire Quigley, Cambridge University Computer Laboratory 

36392  4 
Author: Jasmin Blanchette, TU Muenchen 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

5 

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

8 

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

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

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

12 

36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

13 
val metis_proof_text: 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

14 
bool * minimize_command * string * (string * bool) vector * thm * int 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

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

16 
val isar_proof_text: 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

17 
string Symtab.table * bool * int * Proof.context * int list list 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

18 
> bool * minimize_command * string * (string * bool) vector * thm * int 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

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

20 
val proof_text: 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

21 
bool > string Symtab.table * bool * int * Proof.context * int list list 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

22 
> bool * minimize_command * string * (string * bool) vector * thm * int 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

23 
> string * (string * bool) 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 

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

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

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

32 
open Sledgehammer_Fact_Filter 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

34 

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

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

36 

38014  37 
(* Simple simplifications to ensure that sort annotations don't leave a trail of 
38 
spurious "True"s. *) 

39 
fun s_not @{const False} = @{const True} 

40 
 s_not @{const True} = @{const False} 

41 
 s_not (@{const Not} $ t) = t 

42 
 s_not t = @{const Not} $ t 

43 
fun s_conj (@{const True}, t2) = t2 

44 
 s_conj (t1, @{const True}) = t1 

45 
 s_conj p = HOLogic.mk_conj p 

46 
fun s_disj (@{const False}, t2) = t2 

47 
 s_disj (t1, @{const False}) = t1 

48 
 s_disj p = HOLogic.mk_disj p 

49 
fun s_imp (@{const True}, t2) = t2 

50 
 s_imp (t1, @{const False}) = s_not t1 

51 
 s_imp p = HOLogic.mk_imp p 

52 
fun s_iff (@{const True}, t2) = t2 

53 
 s_iff (t1, @{const True}) = t1 

54 
 s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2 

55 

56 
fun mk_anot (AConn (ANot, [phi])) = phi 

57 
 mk_anot phi = AConn (ANot, [phi]) 

37991  58 
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2]) 
59 

38066  60 
fun index_in_shape x = find_index (exists (curry (op =) x)) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

61 
fun is_axiom_number axiom_names num = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

62 
num > 0 andalso num <= Vector.length axiom_names andalso 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

63 
fst (Vector.sub (axiom_names, num  1)) <> "" 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

64 
fun is_conjecture_number conjecture_shape num = 
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

65 
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

66 

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

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

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

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

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

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

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

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

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

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

78 
 negate_term t = @{const Not} $ t 

79 

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

80 
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

81 
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

82 
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

83 

38035  84 
fun raw_step_number (Definition (num, _, _)) = num 
85 
 raw_step_number (Inference (num, _, _)) = num 

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

86 

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

88 

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

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

91 

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

93 
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

94 

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

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

96 
 repair_name _ "$false" = "c_False" 
38007  97 
 repair_name _ "$$e" = "c_equal" (* seen in Vampire proofs *) 
38035  98 
 repair_name _ "equal" = "c_equal" (* needed by SPASS? *) 
99 
 repair_name pool s = 

100 
case Symtab.lookup pool s of 

101 
SOME s' => s' 

102 
 NONE => 

103 
if String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s then 

104 
"c_equal" (* seen in Vampire proofs *) 

105 
else 

106 
s 

36392  107 
(* Generalized firstorder terms, which include file names, numbers, etc. *) 
38035  108 
val parse_potential_integer = 
109 
(scan_dollar_name  scan_quoted) >> K NONE 

110 
 scan_integer >> SOME 

111 
fun parse_annotation x = 

112 
((parse_potential_integer ::: Scan.repeat ($$ " "  parse_potential_integer) 

38036  113 
>> map_filter I)  Scan.optional parse_annotation [] 
38035  114 
>> uncurry (union (op =)) 
115 
 $$ "("  parse_annotations  $$ ")" 

116 
 $$ "["  parse_annotations  $$ "]") x 

117 
and parse_annotations x = 

38036  118 
(Scan.optional (parse_annotation 
119 
::: Scan.repeat ($$ ","  parse_annotation)) [] 

38035  120 
>> (fn numss => fold (union (op =)) numss [])) x 
121 

122 
(* Vampire proof lines sometimes contain needless information such as "(0:3)", 

123 
which can be hard to disambiguate from function application in an LL(1) 

124 
parser. As a workaround, we extend the TPTP term syntax with such detritus 

125 
and ignore it. *) 

38066  126 
fun parse_vampire_detritus x = 
127 
(scan_integer  $$ ":"  scan_integer >> K []) x 

38035  128 

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

129 
fun parse_term pool x = 
37991  130 
((scan_dollar_name >> repair_name pool) 
38035  131 
 Scan.optional ($$ "("  (parse_vampire_detritus  parse_terms pool) 
132 
 $$ ")") [] 

133 
 Scan.optional ($$ "("  parse_vampire_detritus  $$ ")") [] 

134 
>> ATerm) x 

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

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

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

137 

38034  138 
fun parse_atom pool = 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

139 
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

140 
 parse_term pool) 
38035  141 
>> (fn (u1, NONE) => AAtom u1 
38034  142 
 (u1, SOME (NONE, u2)) => AAtom (ATerm ("c_equal", [u1, u2])) 
37991  143 
 (u1, SOME (SOME _, u2)) => 
38034  144 
mk_anot (AAtom (ATerm ("c_equal", [u1, u2])))) 
37991  145 

146 
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

147 

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

150 
fun parse_formula pool x = 

151 
(($$ "("  parse_formula pool  $$ ")" 

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

153 
 $$ "["  parse_terms pool  $$ "]"  $$ ":" 

154 
 parse_formula pool 

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

156 
 $$ "~"  parse_formula pool >> mk_anot 

38034  157 
 parse_atom pool) 
37991  158 
 Scan.option ((Scan.this_string "=>" >> K AImplies 
159 
 Scan.this_string "<=>" >> K AIff 

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

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

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

163 
 parse_formula pool) 

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

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

166 

38035  167 
val parse_tstp_extra_arguments = 
168 
Scan.optional ($$ ","  parse_annotation 

169 
 Scan.option ($$ ","  parse_annotations)) [] 

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

170 

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

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

175 
 scan_integer  $$ ","  Symbol.scan_id  $$ "," 

38035  176 
 parse_formula pool  parse_tstp_extra_arguments  $$ ")"  $$ "." 
37991  177 
>> (fn (((num, role), phi), deps) => 
178 
case role of 

179 
"definition" => 

180 
(case phi of 

38034  181 
AConn (AIff, [phi1 as AAtom _, phi2]) => 
38007  182 
Definition (num, phi1, phi2) 
38036  183 
 AAtom (ATerm ("c_equal", _)) => 
38007  184 
Inference (num, phi, deps) (* Vampire's equality proxy axiom *) 
37991  185 
 _ => raise Fail "malformed definition") 
186 
 _ => 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

187 

38035  188 
(**** PARSING OF VAMPIRE OUTPUT ****) 
189 

190 
(* Syntax: <num>. <formula> <annotation> *) 

191 
fun parse_vampire_line pool = 

192 
scan_integer  $$ "."  parse_formula pool  parse_annotation 

193 
>> (fn ((num, phi), deps) => Inference (num, phi, deps)) 

194 

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

195 
(**** 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

196 

36392  197 
(* SPASS returns clause references of the form "x.y". We ignore "y", whose role 
198 
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

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

200 

36392  201 
val parse_spass_annotations = 
202 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

203 
 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

204 

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

38034  207 
fun parse_decorated_atom pool = 
208 
parse_atom 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

209 

38034  210 
fun mk_horn ([], []) = AAtom (ATerm ("c_False", [])) 
37991  211 
 mk_horn ([], pos_lits) = foldr1 (mk_aconn AOr) pos_lits 
212 
 mk_horn (neg_lits, []) = mk_anot (foldr1 (mk_aconn AAnd) neg_lits) 

213 
 mk_horn (neg_lits, pos_lits) = 

214 
mk_aconn AImplies (foldr1 (mk_aconn AAnd) neg_lits, 

215 
foldr1 (mk_aconn AOr) pos_lits) 

216 

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

217 
fun parse_horn_clause pool = 
38034  218 
Scan.repeat (parse_decorated_atom pool)  $$ ""  $$ "" 
219 
 Scan.repeat (parse_decorated_atom pool)  $$ ""  $$ ">" 

220 
 Scan.repeat (parse_decorated_atom pool) 

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

222 

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

223 
(* Syntax: <num>[0:<inference><annotations>] 
38034  224 
<atoms>  <atoms> > <atoms>. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

225 
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

226 
scan_integer  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 
38035  227 
 parse_spass_annotations  $$ "]"  parse_horn_clause pool  $$ "." 
37991  228 
>> (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

229 

38035  230 
fun parse_line pool = 
231 
parse_tstp_line pool  parse_vampire_line pool  parse_spass_line pool 

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

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

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

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

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

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

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

238 

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

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

240 

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

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

244 

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

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

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

249 
case strip_prefix_and_undo_ascii type_const_prefix a of 

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

251 
 NONE => 

252 
if not (null us) then 

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

254 
else case strip_prefix_and_undo_ascii tfree_prefix a of 

255 
SOME b => 

256 
let val s = "'" ^ b in 

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

258 
end 

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

259 
 NONE => 
37991  260 
case strip_prefix_and_undo_ascii tvar_prefix a of 
261 
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

262 
 NONE => 
37991  263 
(* Variable from the ATP, say "X1" *) 
264 
Type_Infer.param 0 (a, HOLogic.typeS) 

265 
end 

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

266 

38014  267 
(* Type class literal applied to a type. Returns triple of polarity, class, 
268 
type. *) 

269 
fun type_constraint_from_term pos tfrees (u as ATerm (a, us)) = 

270 
case (strip_prefix_and_undo_ascii class_prefix a, 

271 
map (type_from_fo_term tfrees) us) of 

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

273 
 _ => raise FO_TERM [u] 

274 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

275 
(** Accumulate type constraints in a formula: negative type literals **) 
38014  276 
fun add_var (key, z) = Vartab.map_default (key, []) (cons z) 
277 
fun add_type_constraint (false, cl, TFree (a ,_)) = add_var ((a, ~1), cl) 

278 
 add_type_constraint (false, cl, TVar (ix, _)) = add_var (ix, cl) 

279 
 add_type_constraint _ = I 

280 

38490  281 
fun repair_atp_variable_name f s = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

283 
fun subscript_name s n = s ^ nat_subscript n 
38488  284 
val s = String.map f s 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

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

287 
[_] => (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

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

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

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

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

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

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

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

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

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

297 

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

298 
(* Firstorder translation. No types are known for variables. "HOLogic.typeT" 
38014  299 
should allow them to be inferred. *) 
300 
fun raw_term_from_pred thy full_types tfrees = 

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

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

302 
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

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

306 
 ATerm (a, us) => 

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

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

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

309 
[typ_u, term_u] => 
37991  310 
aux (SOME (type_from_fo_term tfrees typ_u)) extra_us term_u 
311 
 _ => raise FO_TERM us 

312 
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

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

314 
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

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

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

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

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

319 
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

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

321 
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

322 
(* 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

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

324 
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

325 
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

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

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

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

329 
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

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

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

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

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

334 
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

335 
else 
37998  336 
Sign.const_instance thy (c, 
337 
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

338 
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

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

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

341 
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

342 
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

343 
val t = 
37991  344 
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

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

346 
 NONE => 
37991  347 
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

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

349 
 NONE => 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset

350 
if is_tptp_variable a then 
38490  351 
Var ((repair_atp_variable_name Char.toLower a, 0), T) 
38017
3ad3e3ca2451
move Sledgehammerspecific code out of "Sledgehammer_TPTP_Format"
blanchet
parents:
38015
diff
changeset

352 
else 
38488  353 
(* Skolem constants? *) 
38490  354 
Var ((repair_atp_variable_name Char.toUpper a, 0), T) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

355 
in list_comb (t, ts) end 
38014  356 
in aux (SOME HOLogic.boolT) [] end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

357 

38014  358 
fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) = 
359 
if String.isPrefix class_prefix s then 

360 
add_type_constraint (type_constraint_from_term pos tfrees u) 

361 
#> pair @{const True} 

362 
else 

363 
pair (raw_term_from_pred thy full_types tfrees u) 

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

364 

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

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

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

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

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

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

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

371 

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

372 
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

373 
 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

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

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

376 
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

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

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

379 

37991  380 
(* Update schematic type variables with detected sort constraints. It's not 
381 
totally clear when this code is necessary. *) 

38014  382 
fun repair_tvar_sorts (t, tvar_tab) = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

383 
let 
37991  384 
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) 
385 
 do_type (TVar (xi, s)) = 

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

387 
 do_type (TFree z) = TFree z 

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

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

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

391 
 do_term (t as Bound _) = t 

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

393 
 do_term (t1 $ t2) = do_term t1 $ do_term t2 

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

395 

396 
fun quantify_over_free quant_s free_s body_t = 

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

398 
[] => body_t 

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

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

401 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

402 
(* Interpret an ATP formula as a HOL term, extracting sort constraints as they 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

403 
appear in the formula. *) 
38014  404 
fun prop_from_formula thy full_types tfrees phi = 
405 
let 

406 
fun do_formula pos phi = 

37991  407 
case phi of 
38014  408 
AQuant (_, [], phi) => do_formula pos phi 
37991  409 
 AQuant (q, x :: xs, phi') => 
38014  410 
do_formula pos (AQuant (q, xs, phi')) 
411 
#>> quantify_over_free (case q of 

412 
AForall => @{const_name All} 

38490  413 
 AExists => @{const_name Ex}) 
414 
(repair_atp_variable_name Char.toLower x) 

38014  415 
 AConn (ANot, [phi']) => do_formula (not pos) phi' #>> s_not 
37991  416 
 AConn (c, [phi1, phi2]) => 
38014  417 
do_formula (pos > c = AImplies ? not) phi1 
418 
##>> do_formula pos phi2 

419 
#>> (case c of 

420 
AAnd => s_conj 

421 
 AOr => s_disj 

422 
 AImplies => s_imp 

38038  423 
 AIf => s_imp o swap 
424 
 AIff => s_iff 

425 
 ANotIff => s_not o s_iff) 

38034  426 
 AAtom tm => term_from_pred thy full_types tfrees pos tm 
37991  427 
 _ => raise FORMULA [phi] 
38014  428 
in repair_tvar_sorts (do_formula true phi Vartab.empty) end 
37991  429 

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

430 
fun check_formula ctxt = 
38014  431 
Type_Infer.constrain HOLogic.boolT 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

433 

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

434 

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

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

436 

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

437 
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

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

439 

37991  440 
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

441 
let 
37991  442 
val thy = ProofContext.theory_of ctxt 
443 
val t1 = prop_from_formula thy full_types tfrees phi1 

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

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

446 
val unvarify_args = subst_atomic (vars ~~ frees) 
37991  447 
val t2 = prop_from_formula thy full_types tfrees phi2 
36551  448 
val (t1, t2) = 
449 
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

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

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

452 
in 
36551  453 
(Definition (num, t1, t2), 
454 
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

455 
end 
37991  456 
 decode_line full_types tfrees (Inference (num, u, deps)) ctxt = 
36551  457 
let 
37991  458 
val thy = ProofContext.theory_of ctxt 
459 
val t = u > prop_from_formula thy full_types tfrees 

37998  460 
> uncombine_term > check_formula ctxt 
36551  461 
in 
462 
(Inference (num, t, deps), 

463 
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

464 
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

465 
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

466 
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

467 

38035  468 
fun is_same_inference _ (Definition _) = false 
469 
 is_same_inference t (Inference (_, t', _)) = t aconv t' 

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

470 

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

471 
(* 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

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

473 
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

474 

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

475 
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

476 
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

477 
 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

478 
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

479 

38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

480 
(* Discard axioms; consolidate adjacent lines that prove the same formula, since 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

481 
they differ only in type information.*) 
36551  482 
fun add_line _ _ (line as Definition _) lines = line :: lines 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

483 
 add_line conjecture_shape axiom_names (Inference (num, t, [])) lines = 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

484 
(* No dependencies: axiom, conjecture, or (for Vampire) internal axioms or 
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

485 
definitions. *) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

486 
if is_axiom_number axiom_names num then 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

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

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

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

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

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

494 
pre @ map (replace_deps_in_line (num', [num])) post 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

495 
else if is_conjecture_number conjecture_shape num then 
38105
373351f5f834
don't choke on synonyms when parsing SPASS's Flotter output + renamings;
blanchet
parents:
38085
diff
changeset

496 
Inference (num, negate_term t, []) :: lines 
36551  497 
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

498 
map (replace_deps_in_line (num, [])) lines 
36551  499 
 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

500 
(* 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

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

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

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

505 
(* FIXME: Doesn't this code risk conflating proofs involving different 
38035  506 
types? *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

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

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

510 
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

511 

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

512 
(* 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

513 
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

514 
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

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

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

518 
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

519 

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

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

522 
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

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

524 

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

525 
(* 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

526 
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

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

528 
 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

529 

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

530 
fun add_desired_line _ _ _ _ (line as Definition (num, _, _)) (j, lines) = 
37323  531 
(j, line :: map (replace_deps_in_line (num, [])) lines) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

532 
 add_desired_line isar_shrink_factor conjecture_shape axiom_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

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

534 
(j + 1, 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

535 
if is_axiom_number axiom_names num orelse 
38085
cc44e887246c
avoid "clause" and "cnf" terminology where it no longer makes sense
blanchet
parents:
38066
diff
changeset

536 
is_conjecture_number conjecture_shape num orelse 
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

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

538 
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

539 
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

540 
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

541 
(null lines orelse (* last line must be kept *) 
36924  542 
(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

543 
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

544 
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

545 
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

546 

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

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

548 

38599  549 
(* Like "split_line", but ignores "\n" that follow a comma (as in SNARK's 
550 
output). *) 

551 
val split_proof_lines = 

552 
let 

553 
fun aux [] [] = [] 

554 
 aux line [] = [implode (rev line)] 

555 
 aux line ("," :: "\n" :: rest) = aux ("," :: line) rest 

556 
 aux line ("\n" :: rest) = aux line [] @ aux [] rest 

557 
 aux line (s :: rest) = aux (s :: line) rest 

558 
in aux [] o explode end 

559 

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

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

38033  563 
the first number (108) is extracted. For Vampire, we look for 
564 
"108. ... [input]". *) 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

565 
fun used_facts_in_atp_proof axiom_names atp_proof = 
35865  566 
let 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

567 
fun axiom_name_at_index num = 
38039
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

568 
let val j = Int.fromString num > the_default ~1 in 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

569 
if is_axiom_number axiom_names j then 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

570 
SOME (Vector.sub (axiom_names, j  1)) 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

571 
else 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

572 
NONE 
38039
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

573 
end 
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

574 
val tokens_of = 
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

575 
String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") 
38599  576 
fun do_line (tag :: num :: "axiom" :: (rest as _ :: _)) = 
577 
if tag = "cnf" orelse tag = "fof" then 

578 
(case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of 

579 
SOME name => 

38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

580 
if member (op =) rest "file" then 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

581 
SOME (name, is_true_for axiom_names name) 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

582 
else 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

583 
axiom_name_at_index num 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

584 
 NONE => axiom_name_at_index num) 
38599  585 
else 
586 
NONE 

38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

587 
 do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num 
38039
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

588 
 do_line (num :: rest) = 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

589 
(case List.last rest of "input" => axiom_name_at_index num  _ => NONE) 
38039
e2d546a07fa2
revive "e" and "remote_e"'s fact extraction so that it works with E 1.2 as well;
blanchet
parents:
38038
diff
changeset

590 
 do_line _ = NONE 
38599  591 
in atp_proof > split_proof_lines > map_filter (do_line o tokens_of) end 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

592 

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

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

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

595 

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

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

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

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

599 

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

600 
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

601 

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

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

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

604 
"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

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

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

607 
 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

608 
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

609 
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

610 
 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

611 
"(" ^ 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

612 
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

613 
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

614 
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

615 
"Try this command: " ^ 
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38490
diff
changeset

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

617 
fun minimize_line _ [] = "" 
38696
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38599
diff
changeset

618 
 minimize_line minimize_command ss = 
4c6b65d6a135
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
blanchet
parents:
38599
diff
changeset

619 
case minimize_command ss of 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

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

621 
 command => 
38597
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38490
diff
changeset

622 
"\nTo minimize the number of lemmas, try this: " ^ 
db482afec7f0
no spurious trailing "\n" at the end of Sledgehammer's output
blanchet
parents:
38490
diff
changeset

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

624 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

625 
fun used_facts axiom_names = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

626 
used_facts_in_atp_proof axiom_names 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

627 
#> List.partition snd 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

628 
#> pairself (sort_distinct (string_ord) o map fst) 
38015  629 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

630 
fun metis_proof_text (full_types, minimize_command, atp_proof, axiom_names, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

632 
let 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

633 
val (chained_lemmas, other_lemmas) = used_facts axiom_names atp_proof 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

634 
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

635 
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

636 
(metis_line full_types i n other_lemmas ^ 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

637 
minimize_line minimize_command (other_lemmas @ chained_lemmas), 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

638 
map (rpair false) other_lemmas @ map (rpair true) chained_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

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

640 

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

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

642 

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

643 
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

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

645 

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

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

647 
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

648 

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

649 
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

650 

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

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

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

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

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

655 
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

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

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

658 
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

659 

36574  660 
fun smart_case_split [] facts = ByMetis facts 
661 
 smart_case_split proofs facts = CaseSplit (proofs, facts) 

662 

38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

663 
fun add_fact_from_dep axiom_names num = 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

664 
if is_axiom_number axiom_names num then 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

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

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

667 
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

668 

37998  669 
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

670 
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

671 

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

672 
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

673 
 step_for_line _ _ (Inference (num, t, [])) = Assume ((raw_prefix, num), t) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

675 
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

676 
forall_vars t, 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

677 
ByMetis (fold (add_fact_from_dep axiom_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

678 

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

679 
fun proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

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

682 
val lines = 
38035  683 
atp_proof ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

684 
> parse_proof pool 
38035  685 
> sort (int_ord o pairself raw_step_number) 
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

686 
> decode_lines ctxt full_types tfrees 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

687 
> rpair [] > fold_rev (add_line conjecture_shape axiom_names) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

689 
> rpair (0, []) > fold_rev (add_desired_line isar_shrink_factor 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

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

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

693 
(if null params then [] else [Fix params]) @ 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

694 
map2 (step_for_line axiom_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

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

696 

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

697 
(* 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

698 
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

699 
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

700 
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

701 
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

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

703 
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

704 

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

705 
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

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

707 
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

708 
 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

709 
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

710 
 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

711 
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

712 

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

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

714 
 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

715 
 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

716 
 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

717 
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

718 

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

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

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

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

722 
 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

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

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

725 
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

726 
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

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

728 
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

729 
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

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

731 
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

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

733 
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

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

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

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

737 
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

738 

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

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

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

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

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

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

744 

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

747 
(* 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

748 
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

749 
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

750 
several facts that depend on the negated conjecture. *) 
38038  751 
fun find_hyp num = 
752 
nth hyp_ts (index_in_shape num conjecture_shape) 

753 
handle Subscript => 

754 
raise Fail ("Cannot find hypothesis " ^ Int.toString num) 

38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

755 
val concl_ls = map (pair raw_prefix) (List.last conjecture_shape) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

756 
val canonicalize_labels = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

757 
map (fn l => if member (op =) concl_ls l then hd concl_ls else l) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

758 
#> distinct (op =) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

759 
fun first_pass ([], contra) = ([], contra) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

760 
 first_pass ((step as Fix _) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

761 
first_pass (proof, contra) >> cons step 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

762 
 first_pass ((step as Let _) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

763 
first_pass (proof, contra) >> cons step 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

764 
 first_pass ((step as Assume (l as (_, num), _)) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

765 
if member (op =) concl_ls l then 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

766 
first_pass (proof, contra > l = hd concl_ls ? cons step) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

767 
else 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

768 
first_pass (proof, contra) >> cons (Assume (l, find_hyp num)) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

769 
 first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

770 
let 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

771 
val ls = canonicalize_labels ls 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

772 
val step = Have (qs, l, t, ByMetis (ls, ss)) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

773 
in 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

774 
if exists (member (op =) (fst contra)) ls then 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

775 
first_pass (proof, contra >> cons l > cons step) 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

776 
else 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

777 
first_pass (proof, contra) >> cons step 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

778 
end 
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

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

780 
val (proof_top, (contra_ls, contra_proof)) = 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

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

782 
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

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

784 
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

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

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

787 
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

788 
 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

789 
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

790 
 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

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

792 
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

793 
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

794 
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

795 
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

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

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

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

799 
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

800 
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

801 
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

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

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

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

805 
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

806 
>> cons (if member (op =) (fst (snd patches)) l then 
37991  807 
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

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

810 
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

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

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

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

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

815 
(fn l => 
38040
174568533593
fix bug in the SPASS Flotter hack, when a conjecture FOF is translated to several CNF clauses
blanchet
parents:
38039
diff
changeset

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

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

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

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

820 
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

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

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

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

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

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

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

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

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

829 
if member (op =) (fst (snd patches)) l then 
37991  830 
([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

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

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

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

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

835 
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

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

837 
(if null proof_tail then end_qs else []), l, t, 
36574  838 
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

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

840 
[Have (case_split_qualifiers proofs @ end_qs, no_label, 
36574  841 
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

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

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

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

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

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

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

848 
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

849 
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

850 

38490  851 
(* FIXME: Still needed? Probably not. *) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

852 
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

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

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

855 
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

856 
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

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

858 
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

859 
 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

860 
 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

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

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

863 
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

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

865 
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

866 
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

867 
 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

868 
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

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

870 

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

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

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

873 
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

874 
 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

875 
 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

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

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

878 
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

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

880 
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

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

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

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

884 
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

885 
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

886 
 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

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

888 

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

889 
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

890 
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

891 
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

892 
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

893 
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

894 
 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

895 
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

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

897 
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

898 
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

899 
 _ => 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

900 
 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

901 
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

902 

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

903 
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

904 

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

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

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

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

908 
 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

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

910 
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

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

912 
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

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

914 
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

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

916 
 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

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

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

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

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

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

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

923 
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

924 
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

925 
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

926 
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

927 
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

928 
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

929 
 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

930 
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

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

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

933 
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

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

935 
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

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

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

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

939 
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

940 
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

941 
 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

942 
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

943 
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

944 

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

945 
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

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

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

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

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

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

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

952 
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

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

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

955 
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

956 
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

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

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

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

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

961 
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

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

963 
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

964 
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

965 
fun do_facts (ls, ss) = 
38698
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

966 
metis_command full_types 1 1 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

967 
(ls > sort_distinct (prod_ord string_ord int_ord), 
d19c3a7ce38b
clean handling of whether a fact is chained or not;
blanchet
parents:
38696
diff
changeset

968 
ss > sort_distinct string_ord) 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

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

970 
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

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

972 
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

973 
 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

974 
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

975 
 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

976 
do_indent ind ^ do_have qs ^ " " ^ 
36479  977 
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

978 
 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

979 
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

980 
(map (do_block ind) proofs) ^ 
36479  981 
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

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

983 
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

984 
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

985 
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

986 
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

987 
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

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

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

990 
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

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

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

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

994 
 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

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

996 
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

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

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

1000 

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

1001 
fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape) 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

1002 
(other_params as (full_types, _, atp_proof, axiom_names, 
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

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

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

1005 
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

1006 
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

1007 
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

1008 
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

1009 
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

1010 
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

1011 
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
38282
319c59682c51
move Sledgehammer's HOL > FOL translation to separate file (sledgehammer_translate.ML)
blanchet
parents:
38105
diff
changeset

1012 
atp_proof conjecture_shape axiom_names params 
36924  1013 
frees 
37991  1014 
> 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

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

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

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

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

1019 
> string_for_proof ctxt full_types i n of 
38599  1020 
"" => "\nNo structured proof available." 
1021 
 proof => "\n\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

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

1023 
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

1024 
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

1025 
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

1026 
try isar_proof_for () 
38599  1027 
> the_default "\nWarning: The Isar proof construction failed." 
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

1028 
in (one_line_proof ^ isar_proof, lemma_names) end 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

1029 

36557  1030 
fun proof_text isar_proof isar_params other_params = 
1031 
(if isar_proof then isar_proof_text isar_params else metis_proof_text) 

1032 
other_params 

36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

1033 

31038  1034 
end; 