author  blanchet 
Mon, 26 Apr 2010 21:20:43 +0200  
changeset 36402  1b20805974c7 
parent 36396  417cdfb2746a 
child 36404  cb3dc64f13d7 
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 

35865  36 
open Sledgehammer_FOL_Clause 
37 
open Sledgehammer_Fact_Preprocessor 

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

38 

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

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

40 

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

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

43 

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

44 
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

45 

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

46 
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

47 
 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

48 
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

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

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

51 

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

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

53 

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

54 
(* Syntax trees, either term list or formulae *) 
36392  55 
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

56 

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

58 

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

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

61 

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

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

64 

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

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

67 

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

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

69 
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

70 
 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

71 
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

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

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

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

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

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

79 
 $$ "$"  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

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

81 
 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

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

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

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

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

86 

36392  87 
fun negate_stree t = SBranch ("c_Not", [t]) 
88 
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

89 

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

91 
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

92 
 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

93 
 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

94 
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

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

96 
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

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

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

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

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

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

102 

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

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

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

105 

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

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

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

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

109 

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

112 
val parse_tstp_annotations = 

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

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

114 
 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

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

116 

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

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

118 
The <name> could be an identifier, but we assume integers. *) 
36392  119 
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

120 
fun parse_tstp_line pool = 
36392  121 
(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

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

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

125 

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

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

127 

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

130 
val parse_dot_name = parse_integer  $$ "."  parse_integer 

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

131 

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

134 
 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

135 

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

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

138 
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

139 
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

140 

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

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

142 
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

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

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

146 

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

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

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

149 
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

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

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

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

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

155 

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

156 
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

157 

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

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

159 

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

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

161 

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

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

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

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

167 

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

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

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

171 

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

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

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

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

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

176 

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

177 
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

178 
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

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

180 

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

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

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

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

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

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

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

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

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

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

192 
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

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

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

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

198 
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

199 
 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

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

201 

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

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

203 
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

204 
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

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

206 

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

207 
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

208 

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

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

210 
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

211 

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

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

213 
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

214 

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

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

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

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

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

222 
 SBranch (a, ts) => 

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

224 
SOME "equal" => 
35865  225 
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

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

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

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

231 
constant.*) 

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

232 
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

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

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

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

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

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

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

241 
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

242 
 NONE => make_var (a,T) (* Variable from the ATP, say "X1" *) 
23519  243 
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

244 

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

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

248 
constraint_of_stree (not pol) t 

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

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

35865  252 
(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

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

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

255 

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

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

257 

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

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

259 

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

260 
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

261 
 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

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

263 

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

264 
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

265 
 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

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

267 

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

268 
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

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

270 
 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

271 
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

272 
 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

273 
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

274 
 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

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

276 
 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

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

278 
 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

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

280 
 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

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

282 
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

283 
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

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

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

286 

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

287 
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

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

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

290 
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

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

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

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

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

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

296 

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

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

298 
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

299 
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

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

301 
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

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

303 

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

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

305 
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

306 
 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

307 
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

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

309 
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

310 

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

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

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

313 
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts) 
33035  314 
 tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi)) 
315 
 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

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

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

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

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

320 
 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

321 
 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

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

323 

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

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

325 
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

326 
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

327 
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

328 
dt > repair_sorts vt > TypeInfer.constrain HOLogic.boolT 
be73a2b2443b
support readable names even when Isar proof reconstruction is enabled  useful for debugging
blanchet
parents:
36392
diff
changeset

329 
> Syntax.check_term 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

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

331 

29268  332 
fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t; 
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 = 
36291
b4c2043cc96c
added Isar proof reconstruction support for SPASS  which means all provers can now yield Isar proofs;
blanchet
parents:
36288
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 

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

408 
fun add_desired_line ctxt (num, t, []) (j, lines) = 
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 *) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

410 
 add_desired_line ctxt (num, t, deps) (j, lines) = 
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 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

413 
exists_subterm bad_free t orelse length deps < 2 then 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

414 
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

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

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

417 

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

418 
(* ### *) 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

419 
(*Replace numeric proof lines by strings, either from thm_names or sequential line numbers*) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

420 
fun stringify_deps thm_names deps_map [] = [] 
36395  421 
 stringify_deps thm_names deps_map ((num, t, deps) :: lines) = 
422 
if is_axiom_clause_number thm_names num then 

423 
(Vector.sub (thm_names, num  1), t, []) :: 

424 
stringify_deps thm_names deps_map lines 

425 
else 

426 
let 

36396  427 
val label = Int.toString (length deps_map) 
428 
fun string_for_num num = 

429 
if is_axiom_clause_number thm_names num then 

430 
SOME (Vector.sub (thm_names, num  1)) 

431 
else 

432 
AList.lookup (op =) deps_map num 

36395  433 
in 
36396  434 
(label, t, map_filter string_for_num (distinct (op=) deps)) :: 
435 
stringify_deps thm_names ((num, label) :: deps_map) lines 

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

437 

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

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

439 

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

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

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

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

445 
fun extract_clause_numbers_in_atp_proof atp_proof = 
35865  446 
let 
36395  447 
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

448 
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

449 
 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

450 
Int.fromString num 
36395  451 
 extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num 
452 
 extract_num _ = NONE 

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

453 
in atp_proof > split_lines > map_filter (extract_num o tokens_of) end 
33310  454 

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

457 
val chained_hint = "sledgehammer_chained" 

35865  458 

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

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

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

461 
 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

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

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

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

465 
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

466 
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

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

468 
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

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

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

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

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

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

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

476 

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

477 
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

478 
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

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

480 
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

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

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

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

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

485 
val n = Logic.count_prems (prop_of goal) 
36395  486 
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

487 

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

488 
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

489 

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

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

491 

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

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

493 
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

494 

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

495 
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

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

497 

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

498 
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

499 

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

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

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

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

503 
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

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

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

506 
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

507 

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

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

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

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

511 

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

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

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

514 
case Int.fromString s of 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

515 
SOME n => apfst (cons (raw_prefix, n)) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

516 
 NONE => apsnd (cons s) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

518 

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

519 
val add_fact_from_dep = apfst o cons o pair raw_prefix 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

520 

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

521 
fun step_for_tuple _ (label, t, []) = Assume ((raw_prefix, label), t) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

522 
 step_for_tuple j (label, t, deps) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

523 
Have (if j = 1 then [Show] else [], (raw_prefix, label), t, 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

525 

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

526 
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

527 
 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

528 
 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

529 
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

530 
 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

531 
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

532 
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

533 
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

534 
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

535 
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

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

537 
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

538 
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

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

540 
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

541 
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

542 

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

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

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

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

546 
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

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

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

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

550 
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

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

552 
val tuples = fold_rev (add_desired_line ctxt) tuples (0, []) > snd 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

554 
(if null frees then [] else [Fix frees]) @ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

556 
end 
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 
val indent_size = 2 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

560 

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

561 
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

562 

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

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

564 
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

565 
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

566 
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

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

568 
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

569 

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

570 
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

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

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

573 
 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

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

575 
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

576 

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

577 
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

578 
 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

579 
 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

580 
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

581 

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

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

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

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

585 
 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

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

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

588 
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

589 
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

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

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

592 
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

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

594 
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

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

596 
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

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

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

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

600 
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

601 

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

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

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

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

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

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

607 

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

608 
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

609 

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

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

612 
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

613 
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

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

615 
 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

616 
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

617 
 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

618 
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

619 
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

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

621 
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

622 
 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

623 
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

624 
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

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

626 
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

627 
 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

628 
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

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

630 
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

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

632 
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

633 
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

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

635 
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

636 
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

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

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

639 
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

640 
 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

641 
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

642 
 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

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

644 
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

645 
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

646 
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

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

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

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

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

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

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

653 
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

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

655 
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

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

657 
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

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

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

660 
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

661 
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

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

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

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

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

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

667 
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

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

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

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

671 
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

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

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

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

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

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

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

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

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

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

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

682 
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

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

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

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

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

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

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

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

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

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

692 
 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

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

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

695 
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

696 

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

697 
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

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

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

700 
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

701 
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

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

703 
 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

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

705 
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

706 
 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

707 
 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

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

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

710 
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

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

712 
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

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

714 
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

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

716 

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

717 
(* FIXME: implement *) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

719 

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

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

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

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

723 
 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

724 
 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

725 
 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

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

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

728 
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

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

730 
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

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

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

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

734 
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

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

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

737 

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

738 
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

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

740 
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

741 
fun do_label l = if member (op =) used_ls l then l else no_label 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

743 
 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

744 
 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

745 
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

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

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

748 
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

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

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

751 

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

752 
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

753 

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

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

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

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

757 
 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

758 
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

759 
 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

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

761 
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

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

763 
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

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

765 
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

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

767 
 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

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

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

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

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

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

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

774 
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

775 
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

776 
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

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

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

779 
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

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

781 
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

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

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

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

785 
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

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

787 
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

788 

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

789 
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

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

791 
fun do_indent ind = replicate_string (ind * indent_size) " " 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

792 
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

793 
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

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

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

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

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

798 
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

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

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

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

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

803 
o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

805 
(Syntax.string_of_term ctxt) 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

807 
 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

808 
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

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

810 
 do_by_facts _ ss = "by (metis " ^ space_implode " " ss ^ ")" 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

812 
do_indent (ind + 1) ^ do_using ls ^ do_by_facts ls ss 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

813 
and do_step ind (Fix ts) = 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

815 
 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

816 
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

817 
 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

818 
do_indent ind ^ do_have qs ^ " " ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

820 
 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

821 
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

822 
(map (do_block ind) proofs) ^ 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

823 
do_indent ind ^ do_have qs ^ " " ^ 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

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

825 
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

826 
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

827 
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

828 
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

829 
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

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

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

832 
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

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

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

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

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

837 
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

838 
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

839 

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

840 
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

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

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

843 
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

844 
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

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

846 
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

847 
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

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

849 
case proof_from_atp_proof pool ctxt atp_proof thm_names frees 
1b20805974c7
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
blanchet
parents:
36396
diff
changeset

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

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

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

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

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

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

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

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

858 
 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

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

860 
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

861 
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

862 
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

863 
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

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

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

866 

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

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

868 
if isar_proof then isar_proof_text else K metis_proof_text 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

869 

31038  870 
end; 