author  blanchet 
Tue, 27 Apr 2010 16:12:51 +0200  
changeset 36479  fcbf412c560f 
parent 36478  1aba777a367f 
child 36480  1e01a7162435 
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 

25492
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25414
diff
changeset

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

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

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

17 
val make_tvar: string > typ 
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

18 
val strip_prefix: string > string > string option 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

20 
val metis_proof_text: 
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

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

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

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

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

25 
> minimize_command * string * string vector * thm * int 
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

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

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

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

29 
> minimize_command * string * string vector * thm * int 
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

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

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

32 

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

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

35 

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

36 
open Sledgehammer_Util 
35865  37 
open Sledgehammer_FOL_Clause 
38 
open Sledgehammer_Fact_Preprocessor 

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

39 

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

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

41 

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

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

44 

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

45 
fun is_axiom_clause_number thm_names num = num <= Vector.length thm_names 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

46 

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

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

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

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

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

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

52 

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

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

54 

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

55 
(* Syntax trees, either term list or formulae *) 
36392  56 
datatype stree = SInt of int  SBranch of string * stree list; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

57 

36392  58 
fun atom x = SBranch (x, []) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

59 

36392  60 
fun scons (x, y) = SBranch ("cons", [x, y]) 
61 
val slist_of = List.foldl scons (atom "nil") 

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

62 

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

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

65 

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

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

68 

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

69 
(* needed for SPASS's output format *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

70 
fun repair_bool_literal "true" = "c_True" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

71 
 repair_bool_literal "false" = "c_False" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

72 
fun repair_name pool "equal" = "c_equal" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

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

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

77 
fun parse_term pool x = 
36392  78 
(parse_quoted >> atom 
79 
 parse_integer >> SInt 

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

80 
 $$ "$"  Symbol.scan_id >> (atom o repair_bool_literal) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

81 
 (Symbol.scan_id >> repair_name pool) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

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

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

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

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

87 

36392  88 
fun negate_stree t = SBranch ("c_Not", [t]) 
89 
fun equate_strees t1 t2 = SBranch ("c_equal", [t1, t2]); 

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

90 

36392  91 
(* Apply equal or notequal to a term. *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

92 
fun repair_predicate_term (t, NONE) = t 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

93 
 repair_predicate_term (t1, SOME (NONE, t2)) = equate_strees t1 t2 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

94 
 repair_predicate_term (t1, SOME (SOME _, t2)) = 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

95 
negate_stree (equate_strees t1 t2) 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

97 
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

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

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

100 
(*Literals can involve negation, = and !=.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

102 
($$ "~"  parse_literal pool >> negate_stree  parse_predicate_term pool) x 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

103 

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

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

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

106 

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

107 
(* Clause: a list of literals separated by the disjunction sign. *) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

109 
$$ "("  parse_literals pool  $$ ")"  Scan.single (parse_literal pool) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

110 

36392  111 
fun ints_of_stree (SInt n) = cons n 
112 
 ints_of_stree (SBranch (_, ts)) = fold ints_of_stree ts 

113 
val parse_tstp_annotations = 

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

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

115 
 Scan.option ($$ ","  parse_terms NONE) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

116 
>> (fn source => ints_of_stree source [])) [] 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

117 

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

118 
(* <cnf_annotated> ::= cnf(<name>, <formula_role>, <cnf_formula> <annotations>). 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

119 
The <name> could be an identifier, but we assume integers. *) 
36392  120 
fun retuple_tstp_line ((name, ts), deps) = (name, ts, deps) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

121 
fun parse_tstp_line pool = 
36392  122 
(Scan.this_string "cnf"  $$ "(")  parse_integer  $$ "," 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

123 
 Symbol.scan_id  $$ ","  parse_clause pool  parse_tstp_annotations 
36392  124 
 $$ ")"  $$ "." 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

126 

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

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

128 

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

131 
val parse_dot_name = parse_integer  $$ "."  parse_integer 

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

132 

36392  133 
val parse_spass_annotations = 
134 
Scan.optional ($$ ":"  Scan.repeat (parse_dot_name 

135 
 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

136 

36392  137 
(* It is not clear why some literals are followed by sequences of stars. We 
138 
ignore them. *) 

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

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

140 
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

141 

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

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

143 
Scan.repeat (parse_starred_predicate_term pool)  $$ ""  $$ ">" 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

144 
 Scan.repeat (parse_starred_predicate_term pool) 
36392  145 
>> (fn ([], []) => [atom "c_False"] 
146 
 (clauses1, clauses2) => map negate_stree clauses1 @ clauses2) 

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

147 

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

148 
(* Syntax: <name>[0:<inference><annotations>]  
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

150 
fun retuple_spass_line ((name, deps), ts) = (name, ts, deps) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

151 
fun parse_spass_line pool = 
36392  152 
parse_integer  $$ "["  $$ "0"  $$ ":"  Symbol.scan_id 
153 
 parse_spass_annotations  $$ "]"  $$ ""  $$ "" 

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

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

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

156 

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

157 
fun parse_line pool = fst o (parse_tstp_line pool  parse_spass_line pool) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

158 

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

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

160 

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

161 
exception STREE of stree; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

162 

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

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

164 
fun strip_prefix s1 s = 
31038  165 
if String.isPrefix s1 s 
35865  166 
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

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

168 

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

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

170 
val type_const_trans_table_inv = 
35865  171 
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

172 

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

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

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

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

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

177 

36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

178 
fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS); 
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

179 
fun make_tparam s = TypeInfer.param 0 (s, HOLogic.typeS) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

180 
fun make_var (b,T) = Var((b,0),T); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

181 

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

182 
(*Type variables are given the basic sort, HOL.type. Some will later be constrained 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

183 
by information from type literals, or by type inference.*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

184 
fun type_of_stree t = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

185 
case t of 
36392  186 
SInt _ => raise STREE t 
187 
 SBranch (a,ts) => 

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

188 
let val Ts = map type_of_stree ts 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

189 
in 
35865  190 
case strip_prefix tconst_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

191 
SOME b => Type(invert_type_const b, Ts) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

193 
if not (null ts) then raise STREE t (*only tconsts have type arguments*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

194 
else 
35865  195 
case strip_prefix tfree_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

196 
SOME b => TFree("'" ^ b, HOLogic.typeS) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

197 
 NONE => 
35865  198 
case strip_prefix tvar_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

199 
SOME b => make_tvar b 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

200 
 NONE => make_tparam a (* Variable from the ATP, say "X1" *) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

202 

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

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

204 
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

205 
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

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

207 

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

208 
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

209 

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

210 
(*The number of type arguments of a constant, zero if it's monomorphic*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

211 
fun num_typargs thy s = length (Sign.const_typargs thy (s, Sign.the_const_type thy s)); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

212 

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

213 
(*Generates a constant, given its type arguments*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

214 
fun const_of thy (a,Ts) = Const(a, Sign.const_instance thy (a,Ts)); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

215 

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

216 
(*Firstorder translation. No types are known for variables. HOLogic.typeT should allow 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

217 
them to be inferred.*) 
22428  218 
fun term_of_stree args thy t = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

219 
case t of 
36392  220 
SInt _ => raise STREE t 
221 
 SBranch ("hBOOL", [t]) => term_of_stree [] thy t (*ignore hBOOL*) 

222 
 SBranch ("hAPP", [t, u]) => term_of_stree (u::args) thy t 

223 
 SBranch (a, ts) => 

35865  224 
case strip_prefix const_prefix a of 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

225 
SOME "equal" => 
35865  226 
list_comb(Const (@{const_name "op ="}, HOLogic.typeT), List.map (term_of_stree [] thy) ts) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

228 
let val c = invert_const b 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

229 
val nterms = length ts  num_typargs thy c 
22428  230 
val us = List.map (term_of_stree [] thy) (List.take(ts,nterms) @ args) 
231 
(*Extra args from hAPP come AFTER any arguments given directly to the 

232 
constant.*) 

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

233 
val Ts = List.map type_of_stree (List.drop(ts,nterms)) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

234 
in list_comb(const_of thy (c, Ts), us) end 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

235 
 NONE => (*a variable, not a constant*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

236 
let val T = HOLogic.typeT 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

237 
val opr = (*a Free variable is typically a Skolem function*) 
35865  238 
case strip_prefix fixed_var_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

239 
SOME b => Free(b,T) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

240 
 NONE => 
35865  241 
case strip_prefix schematic_var_prefix a of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

242 
SOME b => make_var (b,T) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

243 
 NONE => make_var (a,T) (* Variable from the ATP, say "X1" *) 
23519  244 
in list_comb (opr, List.map (term_of_stree [] thy) (ts@args)) end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

245 

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

248 
fun constraint_of_stree pol (SBranch ("c_Not", [t])) = 

249 
constraint_of_stree (not pol) t 

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

250 
 constraint_of_stree pol t = case t of 
36392  251 
SInt _ => raise STREE t 
252 
 SBranch (a, ts) => 

35865  253 
(case (strip_prefix class_prefix a, map type_of_stree ts) of 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

254 
(SOME b, [T]) => (pol, b, T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

255 
 _ => raise STREE t); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

256 

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

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

258 

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

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

260 

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

261 
fun add_constraint ((false, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

262 
 add_constraint ((false, cl, TVar(ix,_)), vt) = addix (ix,cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

263 
 add_constraint (_, vt) = vt; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

264 

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

265 
fun is_positive_literal (@{const Trueprop} $ t) = is_positive_literal t 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

266 
 is_positive_literal (@{const Not} $ _) = false 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

268 

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

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

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

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

272 
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

273 
 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

274 
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

275 
 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

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

277 
 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

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

279 
 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

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

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

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

283 
if fastype_of t = @{typ prop} then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

284 
HOLogic.mk_Trueprop (negate_term thy (Object_Logic.atomize_term thy t)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

287 

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

288 
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

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

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

291 
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

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

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

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

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

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

297 

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

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

299 
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

300 
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

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

302 
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

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

304 

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

305 
(*Accumulate sort constraints in vt, with "real" literals in lits.*) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

306 
fun lits_of_strees thy (vt, lits) [] = (vt, finish_clause thy lits) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

307 
 lits_of_strees thy (vt, lits) (t :: ts) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

308 
lits_of_strees thy (add_constraint (constraint_of_stree true t, vt), lits) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

310 
handle STREE _ => lits_of_strees thy (vt, term_of_stree [] thy t :: lits) ts 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

311 

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

312 
(*Update TVars/TFrees with detected sort constraints.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

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

314 
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) 
33035  315 
 tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) 
316 
 tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1))) 

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

317 
fun tmsubst (Const (a, T)) = Const (a, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

318 
 tmsubst (Free (a, T)) = Free (a, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

319 
 tmsubst (Var (xi, T)) = Var (xi, tysubst T) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

320 
 tmsubst (t as Bound _) = t 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

321 
 tmsubst (Abs (a, T, t)) = Abs (a, tysubst T, tmsubst t) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

322 
 tmsubst (t $ u) = tmsubst t $ tmsubst u; 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

323 
in not (Vartab.is_empty vt) ? tmsubst end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

324 

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

325 
(*Interpret a list of syntax trees as a clause, given by "real" literals and sort constraints. 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

326 
vt0 holds the initial sort constraints, from the conjecture clauses.*) 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

327 
fun clause_of_strees ctxt vt ts = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

328 
let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in 
36393
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

329 
dt > repair_sorts vt > TypeInfer.constrain HOLogic.boolT 
36477
71cc00ea5768
allow schematic variables in types in terms that are reconstructed by Sledgehammer
blanchet
parents:
36475
diff
changeset

330 
> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic 
71cc00ea5768
allow schematic variables in types in terms that are reconstructed by Sledgehammer
blanchet
parents:
36475
diff
changeset

331 
ctxt) 
36285
d868b34d604c
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
blanchet
parents:
36283
diff
changeset

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

333 

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

334 
fun decode_line vt0 (name, ts, deps) ctxt = 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

335 
let val cl = clause_of_strees ctxt vt0 ts in 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

336 
((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

338 

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

339 
(** Global sort constraints on TFrees (from tfree_tcs) are positive unit clauses. **) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

340 

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

341 
fun add_tfree_constraint ((true, cl, TFree(a,_)), vt) = addix ((a,~1),cl) vt 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

342 
 add_tfree_constraint (_, vt) = vt; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

343 

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

344 
fun tfree_constraints_of_clauses vt [] = vt 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

345 
 tfree_constraints_of_clauses vt ([lit]::tss) = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

346 
(tfree_constraints_of_clauses (add_tfree_constraint (constraint_of_stree true lit, vt)) tss 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

347 
handle STREE _ => (*not a positive type constraint: ignore*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

348 
tfree_constraints_of_clauses vt tss) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

349 
 tfree_constraints_of_clauses vt (_::tss) = tfree_constraints_of_clauses vt tss; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

350 

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

351 

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

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

353 

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

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

355 
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #2 tuples) in 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

356 
#1 (fold_map (decode_line vt0) tuples ctxt) 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

358 

35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

359 
fun unequal t (_, t', _) = not (t aconv t'); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

360 

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

361 
(*No "real" literals means only type information*) 
23519  362 
fun eq_types t = t aconv HOLogic.true_const; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

363 

36395  364 
fun replace_dep (old, new) dep = if dep = old then new else [dep] 
365 
fun replace_deps p (num, t, deps) = 

366 
(num, t, fold (union (op =) o replace_dep p) deps []) 

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

367 

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

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

369 
only in type information.*) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

370 
fun add_line thm_names (num, t, []) lines = 
36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

371 
(* No dependencies: axiom or conjecture clause? *) 
36395  372 
if is_axiom_clause_number thm_names num then 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

373 
(* Axioms are not proof lines *) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

375 
(* Must be clsrel/clsarity: type information, so delete refs to it *) 
36395  376 
map (replace_deps (num, [])) lines 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

378 
(case take_prefix (unequal t) lines of 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

379 
(_,[]) => lines (*no repetition of proof line*) 
36395  380 
 (pre, (num', _, _) :: post) => (*repetition: replace later line by earlier one*) 
381 
pre @ map (replace_deps (num', [num])) post) 

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

382 
else 
36395  383 
(num, t, []) :: lines 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

384 
 add_line _ (num, t, deps) lines = 
36395  385 
if eq_types t then (num, t, deps) :: lines 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

386 
(*Type information will be deleted later; skip repetition test.*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

387 
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

388 
case take_prefix (unequal t) lines of 
36395  389 
(_,[]) => (num, t, deps) :: lines (*no repetition of proof line*) 
390 
 (pre, (num', t', _) :: post) => 

391 
(num, t', deps) :: (*repetition: replace later line by earlier one*) 

392 
(pre @ map (replace_deps (num', [num])) post); 

22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

393 

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

394 
(*Recursively delete empty lines (type information) from the proof.*) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

395 
fun add_nonnull_line (num, t, []) lines = (*no dependencies, so a conjecture clause*) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

397 
(*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

400 
(num, t, []) :: lines 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

401 
 add_nonnull_line (num, t, deps) lines = (num, t, deps) :: lines 
36395  402 
and delete_dep num lines = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

403 
fold_rev add_nonnull_line (map (replace_deps (num, [])) lines) [] 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

404 

35865  405 
fun bad_free (Free (a,_)) = String.isPrefix skolem_prefix a 
22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

406 
 bad_free _ = false; 
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

407 

36474  408 
fun add_desired_line ctxt _ (num, t, []) (j, lines) = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

409 
(j, (num, t, []) :: lines) (* conjecture clauses must be kept *) 
36474  410 
 add_desired_line ctxt shrink_factor (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

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

412 
if eq_types t orelse not (null (Term.add_tvars t [])) orelse 
36474  413 
exists_subterm bad_free t orelse 
414 
(length deps < 2 orelse j mod shrink_factor <> 0) then 

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

415 
map (replace_deps (num, deps)) lines (* delete line *) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

417 
(num, t, deps) :: lines) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

418 

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

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

420 

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

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

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

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

426 
fun extract_clause_numbers_in_atp_proof atp_proof = 
35865  427 
let 
36395  428 
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

429 
fun extract_num ("cnf" :: num :: "axiom" :: _) = Int.fromString num 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

430 
 extract_num ("cnf" :: num :: "negated_conjecture" :: _) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

431 
Int.fromString num 
36395  432 
 extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num 
433 
 extract_num _ = NONE 

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

434 
in atp_proof > split_lines > map_filter (extract_num o tokens_of) end 
33310  435 

36395  436 
(* Used to label theorems chained into the Sledgehammer call (or rather 
437 
goal?) *) 

438 
val chained_hint = "sledgehammer_chained" 

35865  439 

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

440 
fun apply_command _ 1 = "by " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

441 
 apply_command 1 _ = "apply " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

442 
 apply_command i _ = "prefer " ^ string_of_int i ^ " apply " 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

443 
fun metis_command i n [] = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

444 
apply_command i n ^ "metis" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

445 
 metis_command i n xs = 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

446 
apply_command i n ^ "(metis " ^ space_implode " " xs ^ ")" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

448 
"Try this command: " ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

449 
Markup.markup Markup.sendback (metis_command i n xs) ^ ".\n" 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

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

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

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

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

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

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

457 

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

458 
fun metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) = 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

459 
let 
36231
bede2d49ba3b
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
blanchet
parents:
36225
diff
changeset

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

461 
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

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

463 
> map (fn i => Vector.sub (thm_names, i  1)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

464 
> filter_out (fn s => s = "??.unknown" orelse s = chained_hint) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

465 
> sort_distinct string_ord 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

466 
val n = Logic.count_prems (prop_of goal) 
36395  467 
in (metis_line i n lemmas ^ minimize_line minimize_command lemmas, lemmas) end 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
30874
diff
changeset

468 

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

469 
val is_valid_line = String.isPrefix "cnf(" orf String.isSubstring "" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

470 

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

471 
(** NEW PROOF RECONSTRUCTION CODE **) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

472 

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

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

474 
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

475 

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

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

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

478 

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

479 
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

480 

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

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

482 
Fix of (string * typ) list  
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

484 
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

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

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

487 
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

488 

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

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

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

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

492 

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

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

494 
if is_axiom_clause_number thm_names num then 
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

495 
apsnd (cons (Vector.sub (thm_names, num  1))) 
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

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

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

498 

36479  499 
fun generalize_all_vars t = fold_rev Logic.all (map Var (Term.add_vars t [])) t 
36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

500 
fun step_for_tuple _ _ (label, t, []) = Assume ((raw_prefix, label), t) 
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

501 
 step_for_tuple thm_names j (label, t, deps) = 
36479  502 
Have (if j = 1 then [Show] else [], (raw_prefix, label), 
503 
generalize_all_vars (HOLogic.mk_Trueprop t), 

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

504 
Facts (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

505 

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

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

507 
 strip_spaces_in_list [c1] = if Char.isSpace c1 then "" else str c1 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

508 
 strip_spaces_in_list [c1, c2] = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

509 
strip_spaces_in_list [c1] ^ strip_spaces_in_list [c2] 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

510 
 strip_spaces_in_list (c1 :: c2 :: c3 :: cs) = 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

511 
if Char.isSpace c1 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

512 
strip_spaces_in_list (c2 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

513 
else if Char.isSpace c2 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

514 
if Char.isSpace c3 then 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

515 
strip_spaces_in_list (c1 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

517 
str c1 ^ (if forall is_ident_char [c1, c3] then " " else "") ^ 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

518 
strip_spaces_in_list (c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

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

520 
str c1 ^ strip_spaces_in_list (c2 :: c3 :: cs) 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

521 
val strip_spaces = strip_spaces_in_list o String.explode 
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
diff
changeset

522 

36474  523 
fun proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names frees = 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

528 
> map (parse_line pool o explode) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

530 
val tuples = fold_rev (add_line thm_names) tuples [] 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

531 
val tuples = fold_rev add_nonnull_line tuples [] 
36474  532 
val tuples = fold_rev (add_desired_line ctxt shrink_factor) tuples (0, []) 
533 
> snd 

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

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

535 
(if null frees then [] else [Fix frees]) @ 
36475
05209b869a6b
new Isar proof construction code: stringfy axiom names correctly
blanchet
parents:
36474
diff
changeset

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

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

538 

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

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

540 
val no_label = ("", ~1) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

541 

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

542 
fun no_show qs = not (member (op =) qs Show) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

543 

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

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

545 
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

546 
should be associated with forthcoming proof steps. The second component is a 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

547 
pair ("keep_ls", "drop_ls"), where "keep_ls" are the labels to keep and 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

548 
"drop_ls" are those that should be dropped in a case split. *) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

549 
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

550 

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

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

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

553 
Facts (ls, _) => ls 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

554 
 CaseSplit (proofs, (ls, _)) => fold (union (op =) o using_of) proofs ls) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

557 

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

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

559 
 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

560 
 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

561 
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

562 

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

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

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

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

566 
 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

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

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

569 
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

570 
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

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

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

573 
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

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

575 
not (exists (member (op =) (maps new_labels_of proofs)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

577 
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

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

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

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

581 
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

582 

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

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

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

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

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

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

588 

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

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

590 

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

591 
fun direct_proof thy conjecture_shape hyp_ts concl_t proof = 
33310  592 
let 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

596 
 first_pass ((ps as Fix _) :: proof, contra) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

597 
first_pass (proof, contra) >> cons ps 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

598 
 first_pass ((ps as Assume (l, t)) :: proof, contra) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

599 
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

600 
first_pass (proof, contra > cons ps) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

602 
first_pass (proof, contra) >> cons (Assume (l, find_hyp l)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

603 
 first_pass ((ps as Have (qs, l, t, Facts (ls, ss))) :: proof, contra) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

604 
if exists (member (op =) (fst contra)) ls then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

605 
first_pass (proof, contra >> cons l > cons ps) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

607 
first_pass (proof, contra) >> cons ps 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

608 
 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

609 
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

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

611 
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

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

613 
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

614 
fun second_pass end_qs ([], assums, patches) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

615 
([Have (end_qs, no_label, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

616 
if length assums < length concl_ls then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

617 
clause_for_literals thy (map (negate_term thy o fst) assums) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

621 
 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

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

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

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

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

626 
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

627 
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

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

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

630 
([contra_l], co_ls) => 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

634 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

648 
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

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

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

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

652 
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

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

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

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

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

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

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

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

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

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

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

663 
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

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

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

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

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

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

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

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

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

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

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

674 
val (proof_bottom, _) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

676 
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

677 

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

678 
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

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

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

681 
apfst (map (fn l => AList.lookup (op =) subst l > the_default l)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

682 
fun do_step (ps as Fix _) (proof, subst, assums) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

685 
(case AList.lookup (op aconv) assums t of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

688 
 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

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

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

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

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

693 
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

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

695 
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

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

697 

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

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

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

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

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

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

703 
 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

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

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

706 
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

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

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

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

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

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

712 
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

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

714 
in aux no_label end 
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 
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

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

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

719 
fun do_label l = if member (op =) used_ls l then l else no_label 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

720 
fun kill (Fix xs) = Fix xs 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

723 
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

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

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

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

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

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

729 

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

730 
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

731 

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

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

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

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

735 
 aux subst depth nextp ((ps as Fix _) :: proof) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

737 
 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

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

739 
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

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

741 
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

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

743 
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

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

745 
 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

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

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

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

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

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

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

752 
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

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

754 
val relabel_facts = apfst (map (the o AList.lookup (op =) subst)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

759 
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

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

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

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

763 
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

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

765 
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

766 

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

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

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

769 
fun fix_print_mode f = 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

770 
PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

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

772 
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

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

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

775 
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

776 
fun do_raw_label (s, j) = s ^ string_of_int j 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

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

782 
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

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

784 
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

785 
val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

787 
 do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " " 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

788 
fun do_by_facts [] [] = "by blast" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

789 
 do_by_facts _ [] = "by metis" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

790 
 do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")" 
36478
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

791 
fun do_facts (ls, ss) = do_using ls ^ do_by_facts ls ss 
1aba777a367f
fix types of "fix" variables to help proof reconstruction and aid readability
blanchet
parents:
36477
diff
changeset

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

793 
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" 
36402
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

794 
 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

795 
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

797 
do_indent ind ^ do_have qs ^ " " ^ 
36479  798 
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

799 
 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

800 
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

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

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

804 
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

805 
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

806 
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

807 
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

808 
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

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

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

811 
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

813 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

816 
do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

818 

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

819 
fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

820 
(minimize_command, atp_proof, thm_names, goal, i) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

822 
val thy = ProofContext.theory_of ctxt 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

823 
val (frees, hyp_ts, concl_t) = strip_subgoal goal i 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

824 
val n = Logic.count_prems (prop_of goal) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

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

826 
metis_proof_text (minimize_command, atp_proof, thm_names, goal, i) 
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

827 
fun isar_proof_for () = 
36474  828 
case proof_from_atp_proof pool ctxt shrink_factor atp_proof thm_names 
829 
frees 

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

830 
> direct_proof thy conjecture_shape hyp_ts concl_t 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

835 
> string_for_proof ctxt sorts 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

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

837 
 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

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

839 
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

840 
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

841 
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

842 
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

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

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

845 

36422  846 
fun proof_text isar_proof isar_params = 
847 
if isar_proof then isar_proof_text isar_params else metis_proof_text 

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

848 

31038  849 
end; 