author  blanchet 
Tue, 22 Jun 2010 14:28:22 +0200  
changeset 37498  b426cbdb5a23 
parent 37479  f6b1ee5b420b 
child 37572  a899f9506f39 
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 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

11 
type name_pool = Sledgehammer_FOL_Clause.name_pool 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

12 

24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

13 
val invert_const: string > string 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

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

15 
val num_type_args: theory > string > int 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

16 
val strip_prefix: string > string > string option 
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

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

18 
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

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

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

21 
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

22 
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 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

25 
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

26 
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

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

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

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

30 

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

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

33 

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

34 
open Sledgehammer_Util 
35865  35 
open Sledgehammer_FOL_Clause 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

36 
open Sledgehammer_HOL_Clause 
35865  37 
open Sledgehammer_Fact_Preprocessor 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

38 

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

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

40 

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

41 
fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" 
36392  42 
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

43 

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

44 
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

45 
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

46 
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

47 
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

48 
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

49 

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

50 
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

51 
 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

52 
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

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

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

55 

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

56 
fun smart_lambda v t = 
36551  57 
Abs (case v of 
58 
Const (s, _) => 

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

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

61 
 Free (s, _) => s 

62 
 _ => "", 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

63 
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

64 

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

66 
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

67 
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

68 

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

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

70 

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

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

72 
 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

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

74 
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

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

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

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

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

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

80 
strip_spaces_in_list (c1 :: 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 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ 
a8a6d7172c8c
try out Vampire 11 and parse its output correctly;
blanchet
parents:
36492
diff
changeset

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

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

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

86 
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

87 

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

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

89 
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

90 

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

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

92 

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

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

94 
val slist_of = List.foldl scons (str_leaf "nil") 
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 
(*Strings enclosed in single quotes, e.g. filenames*) 
36392  97 
val parse_quoted = $$ "'"  Scan.repeat (~$$ "'")  $$ "'" >> implode; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

98 

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

99 
(*Integer constants, typically proof line numbers*) 
36392  100 
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

101 

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

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

103 
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

104 

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

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

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

107 
 repair_name _ "$false" = "c_False" 
36559  108 
 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

109 
 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

110 
 repair_name pool s = ugly_name pool s 
36392  111 
(* 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

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

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

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

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

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

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

118 
 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

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

120 
 $$ "["  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

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

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

123 

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

124 
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

125 
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

126 

36392  127 
(* 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

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

129 
 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

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

131 
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

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

133 
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

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

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

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

137 
($$ "~"  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

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

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

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

141 
$$ "("  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

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

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

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

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

146 

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

147 
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

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

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

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

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

153 

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

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

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

156 
 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

157 

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

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

159 
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

160 
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

161 
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

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

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

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

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

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

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

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

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

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

171 

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

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

173 

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

176 
val parse_dot_name = parse_integer  $$ "."  parse_integer 

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

177 

36392  178 
val parse_spass_annotations = 
179 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

180 
 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

181 

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

184 
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

185 
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

186 

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

187 
fun parse_horn_clause pool = 
36574  188 
Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ "" 
189 
 Scan.repeat (parse_decorated_predicate_term pool)  $$ ""  $$ ">" 

190 
 Scan.repeat (parse_decorated_predicate_term pool) 

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

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

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

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

194 

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

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

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

197 
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

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

200 
 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

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

202 

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

203 
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

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

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

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

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

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

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

210 

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

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

212 

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

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

214 

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

215 
(*If string s has the prefix s1, return the result of deleting it.*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

216 
fun strip_prefix s1 s = 
31038  217 
if String.isPrefix s1 s 
35865  218 
then SOME (undo_ascii_of (String.extract (s, size s1, NONE))) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

220 

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

221 
(*Invert the table of translations between Isabelle and ATPs*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

222 
val type_const_trans_table_inv = 
35865  223 
Symtab.make (map swap (Symtab.dest type_const_trans_table)); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

224 

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

225 
fun invert_type_const c = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

226 
case Symtab.lookup type_const_trans_table_inv c of 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

227 
SOME c' => c' 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

228 
 NONE => c; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

229 

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

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

231 
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

232 
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

233 
 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

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

235 
case strip_prefix tconst_prefix a of 
c2d7e2dff59e
support Vampire definitions of constants as "let" constructs in Isar proofs
blanchet
parents:
36485
diff
changeset

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

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

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

239 
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

240 
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

241 
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

242 
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

243 
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

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

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

246 
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

247 
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

248 
 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

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

250 
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

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

252 

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

253 
(*Invert the table of translations between Isabelle and ATPs*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

255 
Symtab.update ("fequal", @{const_name "op ="}) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

256 
(Symtab.make (map swap (Symtab.dest const_trans_table))) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

257 

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

258 
fun invert_const c = c > Symtab.lookup const_trans_table_inv > the_default c 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

259 

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

260 
(* The number of type arguments of a constant, zero if it's monomorphic. For 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

261 
(instances of) Skolem pseudoconstants, this information is encoded in the 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

262 
constant name. *) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

263 
fun num_type_args thy s = 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset

264 
if String.isPrefix skolem_theory_name s then 
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset

265 
s > unprefix skolem_theory_name 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

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

267 
> space_explode "_" > List.last > Int.fromString > the 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

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

269 
(s, Sign.the_const_type thy s) > Sign.const_typargs thy > length 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

270 

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

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

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

273 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

287 

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

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

289 
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

290 
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

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

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

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

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

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

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

297 
 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

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

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

300 
case us 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

301 
[term_u, typ_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

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

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

304 
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

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

306 
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

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

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

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

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

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

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

313 
val num_term_args = length us  actual_num_type_args 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

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

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

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

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

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

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

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

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

323 
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

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

325 
(* Extra args from "hAPP" come after any arguments 
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

326 
given directly to the constant. *) 
37410
2bf7e6136047
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
blanchet
parents:
37399
diff
changeset

327 
if String.isPrefix skolem_theory_name c then 
37399
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

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

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

330 
Sign.const_instance thy (c, 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

331 
map (type_from_node tfrees) 
34f080a12063
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
blanchet
parents:
37324
diff
changeset

332 
(drop num_term_args us))) 
36909
7d5587f6d5f7
made Sledgehammer's fulltyped proof reconstruction work for the first time;
blanchet
parents:
36607
diff
changeset

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

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

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

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

337 
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

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

339 
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

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

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

342 
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

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

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

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

346 
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

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

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

349 

36392  350 
(* Type class literal applied to a type. Returns triple of polarity, class, 
351 
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

352 
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

353 
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

354 
 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

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

356 
 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

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

358 
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

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

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

361 

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

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

363 

36485  364 
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

365 

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

366 
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

367 
 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

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

369 

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

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

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

372 

36485  373 
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

374 
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

375 
 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

376 
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

377 
 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

378 
@{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

379 
 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

380 
@{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

381 
 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

382 
@{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

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

384 
 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

385 

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

386 
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

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

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

389 
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

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

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

392 
$ 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

393 
$ 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

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

395 

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

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

397 
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

398 
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

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

400 
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

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

402 

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

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

404 
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

405 
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

406 
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

407 
 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

408 
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

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

410 
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

411 
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

412 
[] 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

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

414 

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

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

416 
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

417 
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

418 
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

419 
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

420 
 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

421 
 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

422 
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

423 
 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

424 
 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

425 
 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

426 
 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

427 
 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

428 
in not (Vartab.is_empty vt) ? do_term end 
36551  429 

430 
fun unskolemize_term t = 

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

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

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

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

434 

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

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

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

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

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

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

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

441 

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

442 
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

443 
 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

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

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

446 
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

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

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

449 

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

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

451 
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

452 
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

453 
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

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

455 
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

456 
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

457 
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

458 
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

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

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

461 

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

462 

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

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

464 

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

465 
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

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

467 

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

468 
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

469 
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

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

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

473 
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

474 
val t2 = clause_of_nodes ctxt full_types tfrees us 
36551  475 
val (t1, t2) = 
476 
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

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

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

479 
in 
36551  480 
(Definition (num, t1, t2), 
481 
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

482 
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

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

485 
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

486 
> unskolemize_term > uncombine_term > check_formula ctxt 
36551  487 
in 
488 
(Inference (num, t, deps), 

489 
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

490 
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

491 
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

492 
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

493 

37323  494 
fun aint_actual_inference _ (Definition _) = true 
495 
 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

496 

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

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

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

499 
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

500 

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

501 
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

502 
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

503 
 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

504 
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

505 

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

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

507 
only in type information.*) 
36551  508 
fun add_line _ _ (line as Definition _) lines = line :: lines 
509 
 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

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

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

512 
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

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

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

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

516 
(* Is there a repetition? If so, replace later line by earlier one. *) 
37323  517 
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

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

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

520 
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

521 
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

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

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

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

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

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

529 
(* Is there a repetition? If so, replace later line by earlier one. *) 
37323  530 
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

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

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

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

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

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

536 
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

537 

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

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

539 
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

540 
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

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

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

544 
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

545 

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

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

548 
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

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

550 

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

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

552 
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

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

554 
 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

555 

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

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

558 
 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

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

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

561 
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

562 
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

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

564 
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

565 
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

566 
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

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

569 
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

570 
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

571 
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

572 

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

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

574 

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

575 
(* A list consisting of the first number in each line is returned. 
36395  576 
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

577 
number (108) is extracted. 
36395  578 
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

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

580 
fun extract_clause_numbers_in_atp_proof atp_proof = 
35865  581 
let 
36395  582 
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

583 
fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num 
36395  584 
 extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num 
585 
 extract_num _ = NONE 

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

586 
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

587 

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

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

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

590 

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

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

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

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

594 

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

595 
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

596 

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

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

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

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

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

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

602 
 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

603 
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

604 
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

605 
 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

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

607 
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

608 
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

609 
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

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

611 
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

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

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

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

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

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

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

619 

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

620 
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

621 

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

622 
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

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

624 
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

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

626 
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

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

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

629 
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

630 
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

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

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

633 
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

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

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

636 
(metis_line full_types i n other_lemmas ^ 
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

637 
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

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

639 

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

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

641 

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

642 
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

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

644 

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

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

646 
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

647 

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

648 
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

649 

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

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

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

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

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

654 
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

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

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

657 
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

658 

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

661 

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

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

663 
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

664 
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

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

666 
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

667 

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

668 
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

669 

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

670 
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

671 
 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

672 
 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

673 
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

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

675 
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

676 

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

677 
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

678 
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

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

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

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

683 
> decode_lines ctxt full_types tfrees 
36551  684 
> 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

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

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

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

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

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

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

691 
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

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

693 

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

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

695 
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

696 
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

697 
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

698 
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

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

700 
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

701 

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

702 
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

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

704 
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

705 
 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

706 
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

707 
 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

708 
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

709 

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

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

711 
 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

712 
 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

713 
 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

714 
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

715 

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

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

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

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

719 
 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

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

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

722 
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

723 
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

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

725 
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

726 
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

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

728 
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

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

730 
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

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

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

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

734 
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

735 

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

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

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

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

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

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

741 

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

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

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

745 
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

746 
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

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

748 
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

749 
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

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

751 
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

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

753 
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

754 
 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

755 
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

756 
 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

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

758 
 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

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

760 
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

761 
else 
36551  762 
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

763 
 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

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

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

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

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

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

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

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

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

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

773 
 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

774 
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

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

776 
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

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

778 
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

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

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

781 
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

782 
 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

783 
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

784 
 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

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

786 
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

787 
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

788 
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

789 
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

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

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

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

793 
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

794 
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

795 
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

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

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

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

799 
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

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

801 
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

802 
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

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

804 
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

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

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

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

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

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

810 
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

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

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

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

814 
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

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

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

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

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

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

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

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

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

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

824 
([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

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

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

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

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

829 
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

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

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

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

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

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

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

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

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

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

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

842 
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

843 
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

844 

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

845 
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

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

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

848 
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

849 
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

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

851 
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

852 
 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

853 
 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

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

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

856 
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

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

858 
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

859 
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

860 
 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

861 
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

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

863 

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

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

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

866 
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

867 
 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

868 
 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

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

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

871 
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

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

873 
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

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

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

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

877 
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

878 
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

879 
 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

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

881 

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

882 
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

883 
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

884 
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

885 
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

886 
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

887 
 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

888 
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

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

890 
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

891 
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

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

893 
 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

894 
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

895 

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

896 
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

897 

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

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

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

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

901 
 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

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

903 
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

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

905 
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

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

907 
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

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

909 
 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

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

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

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

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

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

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

916 
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

917 
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

918 
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

919 
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

920 
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

921 
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

922 
 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

923 
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

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

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

926 
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

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

928 
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

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

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

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

932 
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

933 
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

934 
 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

935 
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

936 
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

937 

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

938 
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

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

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

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

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

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

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

945 
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

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

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

948 
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

949 
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

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

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

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

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

954 
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

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

956 
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

957 
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

958 
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

959 
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

960 
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

961 
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

962 
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

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

964 
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

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

966 
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

967 
 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

968 
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

969 
 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

970 
do_indent ind ^ do_have qs ^ " " ^ 
36479  971 
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

972 
 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

973 
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

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

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

977 
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

978 
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

979 
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

980 
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

981 
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

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

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

984 
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

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

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

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

988 
 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

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

990 
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

991 
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

992 
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

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

994 

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

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

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

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

998 
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

999 
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

1000 
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

1001 

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

1002 
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

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

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

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

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

1007 
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

1008 
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

1009 
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

1010 
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

1011 
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

1012 
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

1013 
case proof_from_atp_proof pool ctxt full_types tfrees isar_shrink_factor 
36924  1014 
atp_proof conjecture_shape thm_names params 
1015 
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

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

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

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

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

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

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

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

1023 
 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

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

1025 
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

1026 
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

1027 
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

1028 
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

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

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

1031 

36557  1032 
fun proof_text isar_proof isar_params other_params = 
1033 
(if isar_proof then isar_proof_text isar_params else metis_proof_text) 

1034 
other_params 

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

1035 

31038  1036 
end; 