author  haftmann 
Thu, 08 Jul 2010 16:19:24 +0200  
changeset 37744  3daaf23b9ab4 
parent 37643  f576af716aa6 
child 37926  e6ff246c0cdb 
permissions  rwrr 
35826  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML 
33310  2 
Author: Lawrence C Paulson and Claire Quigley, Cambridge University Computer Laboratory 
36392  3 
Author: Jasmin Blanchette, TU Muenchen 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

4 

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

7 

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

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

10 
type minimize_command = string list > string 
37624  11 
type name_pool = Sledgehammer_TPTP_Format.name_pool 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

12 

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

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

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

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

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

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

18 
name_pool option * bool * int * Proof.context * int list list 
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

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

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

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

22 
bool > name_pool option * bool * int * Proof.context * int list list 
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

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

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

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

26 

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

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

29 

37574
b8c1f4c46983
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
blanchet
parents:
37572
diff
changeset

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

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

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

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

35 

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

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

37 

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

38 
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" 
36392  39 
fun is_head_digit s = Char.isDigit (String.sub (s, 0)) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

40 

36607
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36606
diff
changeset

41 
val index_in_shape : int > int list list > int = 
e5f7235f39c5
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
krauss
parents:
36606
diff
changeset

42 
find_index o exists o curry (op =) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

43 
fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names 
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

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

45 
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

46 

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

47 
fun ugly_name NONE s = s 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

48 
 ugly_name (SOME the_pool) s = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

49 
case Symtab.lookup (snd the_pool) s of 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

50 
SOME s' => s' 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

51 
 NONE => s 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

52 

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

53 
fun smart_lambda v t = 
36551  54 
Abs (case v of 
55 
Const (s, _) => 

56 
List.last (space_explode skolem_infix (Long_Name.base_name s)) 

57 
 Var ((s, _), _) => s 

58 
 Free (s, _) => s 

59 
 _ => "", fastype_of v, abstract_over (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

60 
fun forall_of v t = HOLogic.all_const (fastype_of v) $ smart_lambda v 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

61 

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

62 
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

63 
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

64 
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

65 

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

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

67 

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

68 
fun strip_spaces_in_list [] = "" 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

69 
 strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

70 
 strip_spaces_in_list [c1, c2] = 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

71 
strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

72 
 strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

73 
if Char.isSpace c1 then 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

74 
strip_spaces_in_list (c2 :: c3 :: cs) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

75 
else if Char.isSpace c2 then 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

76 
if Char.isSpace c3 then 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

77 
strip_spaces_in_list (c1 :: c3 :: cs) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

79 
str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

80 
strip_spaces_in_list (c3 :: cs) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

82 
str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

83 
val strip_spaces = strip_spaces_in_list o String.explode 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

84 

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

85 
(* Syntax trees, either term list or formulae *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

86 
datatype node = IntLeaf of int  StrNode of string * node list 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

87 

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

88 
fun str_leaf s = StrNode (s, []) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

89 

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

90 
fun scons (x, y) = StrNode ("cons", [x, y]) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

91 
val slist_of = List.foldl scons (str_leaf "nil") 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

92 

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

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

95 

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

96 
(*Integer constants, typically proof line numbers*) 
36392  97 
val parse_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

98 

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

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

100 
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

101 

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

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

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

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

106 
 repair_name _ "equal" = "c_equal" (* probably not needed *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

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

110 
forever at compile time. *) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

111 
fun parse_term pool x = 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

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

114 
 (parse_dollar_name >> repair_name pool) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

115 
 Scan.optional ($$ "("  parse_terms pool  $$ ")") [] >> StrNode 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

116 
 $$ "("  parse_term pool  $$ ")" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

117 
 $$ "["  Scan.optional (parse_terms pool) []  $$ "]" >> slist_of) x 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

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

120 

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

121 
fun negate_node u = StrNode ("c_Not", [u]) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

122 
fun equate_nodes u1 u2 = StrNode ("c_equal", [u1, u2]) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

123 

36392  124 
(* Apply equal or notequal to a term. *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

125 
fun repair_predicate_term (u, NONE) = u 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

126 
 repair_predicate_term (u1, SOME (NONE, u2)) = equate_nodes u1 u2 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

127 
 repair_predicate_term (u1, SOME (SOME _, u2)) = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

128 
negate_node (equate_nodes u1 u2) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

130 
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

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

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

133 
fun parse_literal pool x = 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

134 
($$ "~"  parse_literal pool >> negate_node  parse_predicate_term pool) x 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

136 
parse_literal pool ::: Scan.repeat ($$ ""  parse_literal pool) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

138 
$$ "("  parse_literals pool  $$ ")"  parse_literals pool 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

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

141 
::: Scan.repeat ($$ ""  parse_parenthesized_literals pool) 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

143 

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

144 
fun ints_of_node (IntLeaf n) = cons n 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

145 
 ints_of_node (StrNode (_, us)) = fold ints_of_node us 
36392  146 
val parse_tstp_annotations = 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

147 
Scan.optional ($$ ","  parse_term NONE 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

148 
 Scan.option ($$ ","  parse_terms NONE) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

149 
>> (fn source => ints_of_node source [])) [] 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

150 

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

151 
fun parse_definition pool = 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

152 
$$ "("  parse_literal NONE  Scan.this_string "<=>" 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

154 

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

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

156 
The <num> could be an identifier, but we assume integers. *) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

157 
fun finish_tstp_definition_line (num, (u, us)) = Definition (num, u, us) 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

158 
fun finish_tstp_inference_line ((num, us), deps) = Inference (num, us, deps) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

160 
((Scan.this_string "fof"  $$ "(")  parse_integer  $$ "," 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

161 
 Scan.this_string "definition"  $$ ","  parse_definition pool 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

162 
 parse_tstp_annotations  $$ ")"  $$ "." 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

164 
 ((Scan.this_string "cnf"  $$ "(")  parse_integer  $$ "," 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

165 
 Symbol.scan_id  $$ ","  parse_clause pool 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

166 
 parse_tstp_annotations  $$ ")"  $$ "." 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

168 

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

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

170 

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

173 
val parse_dot_name = parse_integer  $$ "."  parse_integer 

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

174 

36392  175 
val parse_spass_annotations = 
176 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

177 
 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

178 

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

181 
fun parse_decorated_predicate_term pool = 

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

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

183 

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

184 
fun parse_horn_clause pool = 
36574  185 
Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ "" 
186 
 Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ ">" 

187 
 Scan.repeat (parse_decorated_predicate_term pool) 

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

188 
>> (fn (([], []), []) => [str_leaf "c_False"] 
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

189 
 ((clauses1, clauses2), clauses3) => 
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

190 
map negate_node (clauses1 @ clauses2) @ clauses3) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

191 

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

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

193 
<cnf_formulas>  <cnf_formulas> > <cnf_formulas>. *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

194 
fun finish_spass_line ((num, deps), us) = Inference (num, us, deps) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

195 
fun parse_spass_line pool = 
36392  196 
parse_integer  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 
36558
36eff5a50bab
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
blanchet
parents:
36557
diff
changeset

197 
 parse_spass_annotations  $$ "]"  parse_horn_clause pool  $$ "." 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

199 

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

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

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

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

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

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

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

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

207 

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

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

209 

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

210 
exception NODE of node list 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

211 

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

212 
(* Type variables are given the basic sort "HOL.type". Some will later be 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

213 
constrained by information from type literals, or by type inference. *) 
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

214 
fun type_from_node _ (u as IntLeaf _) = raise NODE [u] 
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

215 
 type_from_node tfrees (u as StrNode (a, us)) = 
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

216 
let val Ts = map (type_from_node tfrees) us in 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

217 
case strip_prefix type_const_prefix a of 
37572
a899f9506f39
more intramodule dependency cleanup + merge "const" and "type_const" tables, since this is safe
blanchet
parents:
37498
diff
changeset

218 
SOME b => Type (invert_const b, Ts) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

220 
if not (null us) then 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

221 
raise NODE [u] (* only "tconst"s have type arguments *) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

222 
else case strip_prefix tfree_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

223 
SOME b => 
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

224 
let val s = "'" ^ b in 
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

225 
TFree (s, AList.lookup (op =) tfrees s > the_default HOLogic.typeS) 
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

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

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

228 
case strip_prefix tvar_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

229 
SOME b => TVar (("'" ^ b, 0), HOLogic.typeS) 
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

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

231 
(* Variable from the ATP, say "X1" *) 
37145
01aa36932739
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
wenzelm
parents:
36968
diff
changeset

232 
Type_Infer.param 0 (a, HOLogic.typeS) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

234 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

251 

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

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

253 
should allow them to be inferred.*) 
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

254 
fun term_from_node thy full_types tfrees = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

256 
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

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

258 
IntLeaf _ => raise NODE [u] 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

259 
 StrNode ("hBOOL", [u1]) => aux (SOME @{typ bool}) [] u1 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

260 
 StrNode ("hAPP", [u1, u2]) => aux opt_T (u2 :: extra_us) u1 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

261 
 StrNode ("c_Not", [u1]) => @{const Not} $ aux (SOME @{typ bool}) [] u1 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

262 
 StrNode (a, us) => 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

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

265 
[typ_u, term_u] => 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

266 
aux (SOME (type_from_node tfrees typ_u)) extra_us term_u 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

267 
 _ => raise NODE us 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

268 
else case strip_prefix const_prefix a of 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

270 
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

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

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

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

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

275 
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

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

277 
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

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

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

280 
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

281 
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

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

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

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

285 
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

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

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

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

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

290 
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

291 
else 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset

292 
if String.isPrefix skolem_theory_name c then 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

293 
map fastype_of term_ts > HOLogic.typeT 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

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

295 
Sign.const_instance thy (c, 
37643
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

296 
map (type_from_node tfrees) type_us)) 
f576af716aa6
rewrote the TPTP problem generation code more or less from scratch;
blanchet
parents:
37624
diff
changeset

297 
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

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

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

300 
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

301 
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

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

303 
case strip_prefix fixed_var_prefix a of 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

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

306 
case strip_prefix 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

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

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

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

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

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

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

313 

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

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

316 
fun type_constraint_from_node pos tfrees (StrNode ("c_Not", [u])) = 
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

317 
type_constraint_from_node (not pos) tfrees u 
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

318 
 type_constraint_from_node pos tfrees u = case u of 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

319 
IntLeaf _ => raise NODE [u] 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

320 
 StrNode (a, us) => 
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

321 
(case (strip_prefix class_prefix a, 
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

322 
map (type_from_node tfrees) us) of 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

324 
 _ => raise NODE [u]) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

325 

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

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

327 

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

329 

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

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

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

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

333 

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

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

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

336 

36485  337 
fun negate_term thy (Const (@{const_name All}, T) $ Abs (s, T', t')) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

338 
Const (@{const_name Ex}, T) $ Abs (s, T', negate_term thy t') 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

339 
 negate_term thy (Const (@{const_name Ex}, T) $ Abs (s, T', t')) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

340 
Const (@{const_name All}, T) $ Abs (s, T', negate_term thy t') 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

341 
 negate_term thy (@{const "op >"} $ t1 $ t2) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

342 
@{const "op &"} $ t1 $ negate_term thy t2 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

343 
 negate_term thy (@{const "op &"} $ t1 $ t2) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

344 
@{const "op "} $ negate_term thy t1 $ negate_term thy t2 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

345 
 negate_term thy (@{const "op "} $ t1 $ t2) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

346 
@{const "op &"} $ negate_term thy t1 $ negate_term thy t2 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

347 
 negate_term _ (@{const Not} $ t) = t 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

348 
 negate_term _ t = @{const Not} $ t 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

349 

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

350 
fun clause_for_literals _ [] = HOLogic.false_const 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

353 
case List.partition is_positive_literal lits of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

355 
@{const "op >"} 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

356 
$ foldr1 HOLogic.mk_conj (map (negate_term thy) neg_lits) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

357 
$ foldr1 HOLogic.mk_disj pos_lits 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

358 
 _ => foldr1 HOLogic.mk_disj lits 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

359 

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

360 
(* Final treatment of the list of "real" literals from a clause. 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

361 
No "real" literals means only type information. *) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

362 
fun finish_clause _ [] = HOLogic.true_const 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

364 
lits > filter_out (curry (op =) HOLogic.false_const) > rev 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

366 

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

367 
(*Accumulate sort constraints in vt, with "real" literals in lits.*) 
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

368 
fun lits_of_nodes thy full_types tfrees = 
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

369 
let 
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

370 
fun aux (vt, lits) [] = (vt, finish_clause thy lits) 
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

371 
 aux (vt, lits) (u :: us) = 
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

372 
aux (add_type_constraint 
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

373 
(type_constraint_from_node true tfrees u) vt, lits) us 
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

374 
handle NODE _ => 
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

375 
aux (vt, term_from_node thy full_types tfrees (SOME @{typ bool}) 
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

376 
[] u :: lits) us 
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

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

378 

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

379 
(* Update TVars with detected sort constraints. It's not totally clear when 
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

380 
this code is necessary. *) 
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

381 
fun repair_tvar_sorts vt = 
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

382 
let 
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

383 
fun do_type (Type (a, Ts)) = Type (a, map do_type Ts) 
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

384 
 do_type (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) 
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

385 
 do_type (TFree z) = TFree z 
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

386 
fun do_term (Const (a, T)) = Const (a, do_type 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

387 
 do_term (Free (a, T)) = Free (a, do_type 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

388 
 do_term (Var (xi, T)) = Var (xi, do_type 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

389 
 do_term (t as Bound _) = 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

390 
 do_term (Abs (a, T, t)) = Abs (a, do_type T, do_term 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

391 
 do_term (t1 $ t2) = do_term t1 $ do_term t2 
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

392 
in not (Vartab.is_empty vt) ? do_term end 
36551  393 

394 
fun unskolemize_term t = 

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

395 
Term.add_consts t [] 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

396 
> filter (is_skolem_const_name o fst) > map Const 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

397 
> rpair t > fold forall_of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

398 

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

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

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

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

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

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

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

405 

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

406 
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

407 
 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

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

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

410 
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

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

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

413 

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

414 
(* Interpret a list of syntax trees as a clause, given by "real" literals and 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

415 
sort constraints. "vt" holds the initial sort constraints, from the 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

416 
conjecture clauses. *) 
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

417 
fun clause_of_nodes ctxt full_types tfrees us = 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

419 
val thy = ProofContext.theory_of ctxt 
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

420 
val (vt, t) = lits_of_nodes thy full_types tfrees (Vartab.empty, []) us 
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

421 
in repair_tvar_sorts vt t end 
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

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

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

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

425 

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

426 

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

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

428 

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

429 
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

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

431 

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

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

433 
let 
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

434 
val t1 = clause_of_nodes ctxt full_types tfrees [u] 
36551  435 
val vars = snd (strip_comb t1) 
36486
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

437 
val unvarify_args = subst_atomic (vars ~~ frees) 
36967
3c804030474b
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
blanchet
parents:
36924
diff
changeset

438 
val t2 = clause_of_nodes ctxt full_types tfrees us 
36551  439 
val (t1, t2) = 
440 
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

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

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

443 
in 
36551  444 
(Definition (num, t1, t2), 
445 
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

446 
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

447 
 decode_line full_types tfrees (Inference (num, us, deps)) ctxt = 
36551  448 
let 
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

449 
val t = us > clause_of_nodes ctxt full_types tfrees 
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 
> unskolemize_term > uncombine_term > check_formula ctxt 
36551  451 
in 
452 
(Inference (num, t, deps), 

453 
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

454 
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

455 
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

456 
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

457 

37323  458 
fun aint_actual_inference _ (Definition _) = true 
459 
 aint_actual_inference t (Inference (_, t', _)) = not (t aconv t') 

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

460 

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

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

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

463 
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

464 

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

465 
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

466 
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

467 
 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

468 
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

469 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

486 
Inference (num, t, []) :: lines 
36551  487 
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

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

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

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

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

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

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

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

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

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

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

500 
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

501 

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

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

503 
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

504 
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

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

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

508 
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

509 

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

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

512 
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

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

514 

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

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

516 
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

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

518 
 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

519 

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

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

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

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

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

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

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

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

528 
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

529 
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

530 
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

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

533 
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

534 
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

535 
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

536 

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

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

538 

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

539 
(* A list consisting of the first number in each line is returned. 
36395  540 
TSTP: Interesting lines have the form "cnf(108, axiom, ...)", where the 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

541 
number (108) is extracted. 
36395  542 
SPASS: Lines have the form "108[0:Inp] ...", where the first number (108) is 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

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

544 
fun extract_clause_numbers_in_atp_proof atp_proof = 
35865  545 
let 
36395  546 
val tokens_of = String.tokens (not o is_ident_char) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

547 
fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num 
36395  548 
 extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num 
549 
 extract_num _ = NONE 

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

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

551 

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

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

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

554 

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

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

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

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

558 

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

559 
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

560 

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

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

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

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

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

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

566 
 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

567 
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

568 
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

569 
 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

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

571 
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

572 
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

573 
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

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

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

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

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

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

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

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

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

583 

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

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

585 

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

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

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

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

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

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

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

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

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

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

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

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

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

598 
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

599 
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

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

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

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

603 

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

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

605 

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

606 
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

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

608 

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

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

610 
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

611 

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

612 
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

613 

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

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

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

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

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

618 
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

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

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

621 
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

622 

36574  623 
fun smart_case_split [] facts = ByMetis facts 
624 
 smart_case_split proofs facts = CaseSplit (proofs, facts) 

625 

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

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

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

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

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

630 
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

631 

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

632 
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

633 

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

634 
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

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

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

637 
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

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

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

640 

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

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

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

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

644 
val lines = 
36574  645 
atp_proof ^ "$" (* the $ sign acts as a sentinel *) 
36548
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

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

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

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

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

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

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

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

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

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

657 

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

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

659 
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

660 
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

661 
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

662 
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

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

664 
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

665 

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

666 
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

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

668 
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

669 
 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

670 
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

671 
 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

672 
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

673 

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

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

675 
 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

676 
 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

677 
 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

678 
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

679 

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

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

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

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

683 
 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

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

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

686 
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

687 
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

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

689 
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

690 
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

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

692 
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

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

694 
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

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

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

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

698 
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

699 

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

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

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

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

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

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

705 

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

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

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

709 
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

710 
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

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

712 
fun find_hyp num = nth hyp_ts (index_in_shape num conjecture_shape) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

713 
val concl_ls = map (pair raw_prefix) (List.last conjecture_shape) 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

714 
val canonicalize_labels = 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

715 
map (fn l => if member (op =) concl_ls l then hd concl_ls else l) 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

716 
#> distinct (op =) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

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

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

723 
if member (op =) concl_ls l then 
37324
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

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

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

727 
 first_pass (Have (qs, l, t, ByMetis (ls, ss)) :: proof, contra) = 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

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

729 
val ls = canonicalize_labels ls 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

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

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

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

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

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

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

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

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

738 
val (proof_top, (contra_ls, contra_proof)) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

740 
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

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

742 
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

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

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

745 
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

746 
 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

747 
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

748 
 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

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

750 
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

751 
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

752 
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

753 
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

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

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

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

757 
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

758 
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

759 
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

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

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

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

763 
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

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

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

766 
else 
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

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

768 
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

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

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

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

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

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

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

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

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

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

778 
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

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

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

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

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

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

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

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

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

787 
if member (op =) (fst (snd patches)) l then 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

788 
([Assume (l, negate_term thy t)], (l :: co_ls, ss)) 
d77250dd2416
fix bugs in Sledgehammer's Isar proof "redirection" code
blanchet
parents:
37323
diff
changeset

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

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

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

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

793 
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

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

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

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

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

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

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

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

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

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

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

806 
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

807 
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

808 

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

809 
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

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

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

812 
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

813 
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

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

815 
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

816 
 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

817 
 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

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

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

820 
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

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

822 
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

823 
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

824 
 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

825 
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

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

827 

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

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

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

830 
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

831 
 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

832 
 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

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

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

835 
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

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

837 
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

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

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

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

841 
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

842 
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

843 
 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

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

845 

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

846 
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

847 
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

848 
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

849 
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

850 
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

851 
 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

852 
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

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

854 
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

855 
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

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

857 
 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

858 
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

859 

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

860 
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

861 

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

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

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

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

865 
 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

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

867 
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

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

869 
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

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

871 
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

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

873 
 aux subst depth (next_assum, next_fact) (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

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

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

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

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

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

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

880 
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

881 
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

882 
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

883 
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

884 
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

885 
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

886 
 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

887 
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

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

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

890 
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

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

892 
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

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

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

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

896 
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

897 
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

898 
 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

899 
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

900 
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

901 

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

902 
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

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

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

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

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

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

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

909 
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

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

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

912 
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

913 
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

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

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

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

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

918 
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

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

920 
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

921 
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

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

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

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

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

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

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

928 
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

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

930 
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

931 
 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

932 
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

933 
 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

934 
do_indent ind ^ do_have qs ^ " " ^ 
36479  935 
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

936 
 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

937 
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

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

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

941 
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

942 
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

943 
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

944 
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

945 
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

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

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

948 
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

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

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

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

952 
 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

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

954 
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

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

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

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

958 

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

959 
fun strip_subgoal goal i = 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

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

961 
val (t, frees) = Logic.goal_params (prop_of goal) i 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

962 
val hyp_ts = t > Logic.strip_assums_hyp > map (curry subst_bounds frees) 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

963 
val concl_t = t > Logic.strip_assums_concl > curry subst_bounds frees 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

964 
in (rev (map dest_Free frees), hyp_ts, concl_t) end 
b426cbdb5a23
removed Sledgehammer's support for the DFG syntax;
blanchet
parents:
37479
diff
changeset

965 

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

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

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

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

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

970 
val thy = ProofContext.theory_of ctxt 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

971 
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

972 
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

973 
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

974 
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

975 
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

976 
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

977 
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
36924  978 
atp_proof conjecture_shape thm_names params 
979 
frees 

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

980 
> redirect_proof thy 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

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

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

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

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

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

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

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

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

989 
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

990 
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

991 
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

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

993 
> the_default "Warning: The Isar proof construction failed.\n" 
36283
25e69e93954d
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short oneliner proof  but in "debug" mode we do want to know what the exception is
blanchet
parents:
36281
diff
changeset

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

995 

36557  996 
fun proof_text isar_proof isar_params other_params = 
997 
(if isar_proof then isar_proof_text isar_params else metis_proof_text) 

998 
other_params 

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

999 

31038  1000 
end; 