author  blanchet 
Wed, 21 Apr 2010 17:06:26 +0200  
changeset 36283  25e69e93954d 
parent 36281  dbbf4d5d584d 
child 36285  d868b34d604c 
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 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

3 

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

6 

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

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

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

10 

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

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

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

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

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

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

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

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

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

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

22 
val isar_proof_text: 
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

23 
bool > int > bool > Proof.context > minimize_command > string 
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

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

25 
val proof_text: 
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

26 
bool > bool > int > bool > Proof.context > minimize_command > string 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

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

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

29 

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

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

32 

35865  33 
open Sledgehammer_FOL_Clause 
34 
open Sledgehammer_Fact_Preprocessor 

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

35 

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

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

37 

35865  38 
val trace_proof_path = Path.basic "atp_trace"; 
39 

40 
fun trace_proof_msg f = 

41 
if !trace then File.append (File.tmp_path trace_proof_path) (f ()) else (); 

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

42 

32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
31866
diff
changeset

43 
fun string_of_thm ctxt = PrintMode.setmp [] (Display.string_of_thm ctxt); 
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
25999
diff
changeset

44 

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

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

46 

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

47 
(*Syntax trees, either termlist or formulae*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

48 
datatype stree = Int of int  Br of string * stree list; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

49 

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

50 
fun atom x = Br(x,[]); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

51 

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

52 
fun scons (x,y) = Br("cons", [x,y]); 
30190  53 
val listof = List.foldl scons (atom "nil"); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

54 

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

55 
(*Strings enclosed in single quotes, e.g. filenames*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

56 
val quoted = $$"'"  Scan.repeat (~$$"'")  $$"'" >> implode; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

57 

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

58 
(*Intended for $true and $false*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

59 
fun tf s = "c_" ^ str (Char.toUpper (String.sub(s,0))) ^ String.extract(s,1,NONE); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

60 
val truefalse = $$"$"  Symbol.scan_id >> (atom o tf); 
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 
(*Integer constants, typically proof line numbers*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

63 
fun is_digit s = Char.isDigit (String.sub(s,0)); 
33035  64 
val integer = Scan.many1 is_digit >> (the o Int.fromString o implode); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

65 

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

66 
(*Generalized FO terms, which include filenames, numbers, etc.*) 
25999  67 
fun termlist x = (term ::: Scan.repeat ($$","  term)) x 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

68 
and term x = (quoted >> atom  integer>>Int  truefalse  
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

69 
Symbol.scan_id  Scan.optional ($$"("  termlist  $$")") [] >> Br  
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

70 
$$"("  term  $$")"  
24547
64c20ee76bc1
Vampire structured proofs. Better parsing; some bug fixes.
paulson
parents:
24493
diff
changeset

71 
$$"["  Scan.optional termlist []  $$"]" >> listof) x; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

72 

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

73 
fun negate t = Br("c_Not", [t]); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

74 
fun equate (t1,t2) = Br("c_equal", [t1,t2]); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

75 

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

76 
(*Apply equal or notequal to a term*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

77 
fun syn_equal (t, NONE) = t 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

78 
 syn_equal (t1, SOME (NONE, t2)) = equate (t1,t2) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

79 
 syn_equal (t1, SOME (SOME _, t2)) = negate (equate (t1,t2)); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

80 

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

81 
(*Literals can involve negation, = and !=.*) 
24547
64c20ee76bc1
Vampire structured proofs. Better parsing; some bug fixes.
paulson
parents:
24493
diff
changeset

82 
fun literal x = ($$"~"  literal >> negate  
64c20ee76bc1
Vampire structured proofs. Better parsing; some bug fixes.
paulson
parents:
24493
diff
changeset

83 
(term  Scan.option (Scan.option ($$"!")  $$"="  term) >> syn_equal)) x; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

84 

25999  85 
val literals = literal ::: Scan.repeat ($$""  literal); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

86 

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

87 
(*Clause: a list of literals separated by the disjunction sign*) 
24547
64c20ee76bc1
Vampire structured proofs. Better parsing; some bug fixes.
paulson
parents:
24493
diff
changeset

88 
val clause = $$"("  literals  $$")"  Scan.single literal; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

89 

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

90 
val annotations = $$","  term  Scan.option ($$","  termlist); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

91 

25718  92 
(*<cnf_annotated> ::= cnf(<name>,<formula_role>,<cnf_formula><annotations>). 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

93 
The <name> could be an identifier, but we assume integers.*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

94 
val tstp_line = (Scan.this_string "cnf"  $$"(")  
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

95 
integer  $$","  Symbol.scan_id  $$","  
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

96 
clause  Scan.option annotations  $$ ")"; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

97 

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

98 

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

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

100 

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

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

102 

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

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

104 
fun strip_prefix s1 s = 
31038  105 
if String.isPrefix s1 s 
35865  106 
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

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

108 

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

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

110 
val type_const_trans_table_inv = 
35865  111 
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

112 

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

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

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

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

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

117 

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

118 
fun make_tvar b = TVar(("'" ^ b, 0), HOLogic.typeS); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

120 

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

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

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

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

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

125 
Int _ => raise STREE t 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

126 
 Br (a,ts) => 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

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

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

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

132 
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

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

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

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

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

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

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

141 

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

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

143 
val const_trans_table_inv = 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

144 
Symtab.update ("fequal", "op =") 
35865  145 
(Symtab.make (map swap (Symtab.dest const_trans_table))); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

146 

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

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

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

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

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

151 

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

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

153 
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

154 

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

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

156 
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

157 

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

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

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

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

162 
Int _ => raise STREE t 
22428  163 
 Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*) 
164 
 Br ("hAPP",[t,u]) => term_of_stree (u::args) thy t 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

165 
 Br (a,ts) => 
35865  166 
case strip_prefix const_prefix a of 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

167 
SOME "equal" => 
35865  168 
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

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

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

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

174 
constant.*) 

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

175 
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

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

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

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

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

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

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

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

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

187 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

188 
(*Type class literal applied to a type. Returns triple of polarity, class, type.*) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

189 
fun constraint_of_stree pol (Br("c_Not",[t])) = constraint_of_stree (not pol) t 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

190 
 constraint_of_stree pol t = case t of 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

191 
Int _ => raise STREE t 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

192 
 Br (a,ts) => 
35865  193 
(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

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

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

196 

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

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

198 

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

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

200 

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

201 
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

202 
 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

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

204 

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

205 
(*False literals (which E includes in its proofs) are deleted*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

206 
val nofalses = filter (not o equal HOLogic.false_const); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

207 

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

208 
(*Final treatment of the list of "real" literals from a clause.*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

209 
fun finish [] = HOLogic.true_const (*No "real" literals means only type information*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

211 
case nofalses lits of 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

212 
[] => HOLogic.false_const (*The empty clause, since we started with real literals*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

213 
 xs => foldr1 HOLogic.mk_disj (rev xs); 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

214 

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

215 
(*Accumulate sort constraints in vt, with "real" literals in lits.*) 
32994  216 
fun lits_of_strees _ (vt, lits) [] = (vt, finish lits) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

217 
 lits_of_strees ctxt (vt, lits) (t::ts) = 
22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

218 
lits_of_strees ctxt (add_constraint (constraint_of_stree true t, vt), lits) ts 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

219 
handle STREE _ => 
22428  220 
lits_of_strees ctxt (vt, term_of_stree [] (ProofContext.theory_of ctxt) t :: lits) ts; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

221 

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

222 
(*Update TVars/TFrees with detected sort constraints.*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

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

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

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

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

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

231 
 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

232 
 tmsubst (t $ u) = tmsubst t $ tmsubst u; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

233 
in fn t => if Vartab.is_empty vt then t else tmsubst t end; 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

234 

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

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

236 
vt0 holds the initial sort constraints, from the conjecture clauses.*) 
23519  237 
fun clause_of_strees ctxt vt0 ts = 
22728  238 
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts in 
24680  239 
singleton (Syntax.check_terms ctxt) (TypeInfer.constrain HOLogic.boolT (fix_sorts vt dt)) 
22728  240 
end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

241 

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

243 

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

244 
fun ints_of_stree_aux (Int n, ns) = n::ns 
30190  245 
 ints_of_stree_aux (Br(_,ts), ns) = List.foldl ints_of_stree_aux ns ts; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

246 

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

247 
fun ints_of_stree t = ints_of_stree_aux (t, []); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

248 

25086
729f9aad1f50
Improving the propagation of type constraints for Frees
paulson
parents:
24958
diff
changeset

249 
fun decode_tstp vt0 (name, role, ts, annots) ctxt = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

250 
let val deps = case annots of NONE => []  SOME (source,_) => ints_of_stree source 
25086
729f9aad1f50
Improving the propagation of type constraints for Frees
paulson
parents:
24958
diff
changeset

251 
val cl = clause_of_strees ctxt vt0 ts 
29268  252 
in ((name, role, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt) end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

253 

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

254 
fun dest_tstp ((((name, role), ts), annots), chs) = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

256 
"."::_ => (name, role, ts, annots) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

257 
 _ => error ("TSTP line not terminated by \".\": " ^ implode chs); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

258 

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

259 

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

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

261 

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

262 
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

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

264 

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

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

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

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

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

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

270 
 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

271 

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

272 

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

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

274 

22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

275 
fun decode_tstp_list ctxt tuples = 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

276 
let val vt0 = tfree_constraints_of_clauses Vartab.empty (map #3 tuples) 
25086
729f9aad1f50
Improving the propagation of type constraints for Frees
paulson
parents:
24958
diff
changeset

277 
in #1 (fold_map (decode_tstp vt0) tuples ctxt) end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

278 

23519  279 
(** Finding a matching assumption. The literals may be permuted, and variable names 
31038  280 
may disagree. We have to try all combinations of literals (quadratic!) and 
23519  281 
match up the variable names consistently. **) 
282 

35865  283 
fun strip_alls_aux n (Const(@{const_name all}, _)$Abs(a,T,t)) = 
23519  284 
strip_alls_aux (n+1) (subst_bound (Var ((a,n), T), t)) 
285 
 strip_alls_aux _ t = t; 

286 

287 
val strip_alls = strip_alls_aux 0; 

288 

289 
exception MATCH_LITERAL; 

22012
adf68479ae1b
Proof.context now sent to watcher and used in type inference step of proof reconstruction
paulson
parents:
21999
diff
changeset

290 

23519  291 
(*Ignore types: they are not to be trusted...*) 
292 
fun match_literal (t1$u1) (t2$u2) env = 

293 
match_literal t1 t2 (match_literal u1 u2 env) 

31038  294 
 match_literal (Abs (_,_,t1)) (Abs (_,_,t2)) env = 
23519  295 
match_literal t1 t2 env 
31038  296 
 match_literal (Bound i1) (Bound i2) env = 
23519  297 
if i1=i2 then env else raise MATCH_LITERAL 
31038  298 
 match_literal (Const(a1,_)) (Const(a2,_)) env = 
23519  299 
if a1=a2 then env else raise MATCH_LITERAL 
31038  300 
 match_literal (Free(a1,_)) (Free(a2,_)) env = 
23519  301 
if a1=a2 then env else raise MATCH_LITERAL 
302 
 match_literal (Var(ix1,_)) (Var(ix2,_)) env = insert (op =) (ix1,ix2) env 

32994  303 
 match_literal _ _ _ = raise MATCH_LITERAL; 
23519  304 

305 
(*Checking that all variable associations are unique. The list env contains no 

306 
repetitions, but does it contain say (x,y) and (y,y)? *) 

31038  307 
fun good env = 
23519  308 
let val (xs,ys) = ListPair.unzip env 
309 
in not (has_duplicates (op=) xs orelse has_duplicates (op=) ys) end; 

310 

311 
(*Match one list of literals against another, ignoring types and the order of 

312 
literals. Sorting is unreliable because we don't have types or variable names.*) 

313 
fun matches_aux _ [] [] = true 

314 
 matches_aux env (lit::lits) ts = 

315 
let fun match1 us [] = false 

316 
 match1 us (t::ts) = 

317 
let val env' = match_literal lit t env 

31038  318 
in (good env' andalso matches_aux env' lits (us@ts)) orelse 
319 
match1 (t::us) ts 

23519  320 
end 
321 
handle MATCH_LITERAL => match1 (t::us) ts 

31038  322 
in match1 [] ts end; 
23519  323 

324 
(*Is this length test useful?*) 

31038  325 
fun matches (lits1,lits2) = 
326 
length lits1 = length lits2 andalso 

23519  327 
matches_aux [] (map Envir.eta_contract lits1) (map Envir.eta_contract lits2); 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

328 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

329 
fun permuted_clause t = 
24958  330 
let val lits = HOLogic.disjuncts t 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

331 
fun perm [] = NONE 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

332 
 perm (ctm::ctms) = 
24958  333 
if matches (lits, HOLogic.disjuncts (HOLogic.dest_Trueprop (strip_alls ctm))) 
23519  334 
then SOME ctm else perm ctms 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

335 
in perm end; 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

336 

0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

337 
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

338 
ATP may have their literals reordered.*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

339 
fun isar_proof_body ctxt sorts ctms = 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

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

341 
val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n") 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

342 
val string_of_term = 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

343 
PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN) 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

344 
(print_mode_value ())) 
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

345 
(Syntax.string_of_term ctxt) 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

346 
fun have_or_show "show" _ = " show \"" 
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

347 
 have_or_show have lname = " " ^ have ^ " " ^ lname ^ ": \"" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

348 
fun do_line _ (lname, t, []) = 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

349 
(* No deps: it's a conjecture clause, with no proof. *) 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

350 
(case permuted_clause t ctms of 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

351 
SOME u => " assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

352 
 NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body", 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

353 
[t])) 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

354 
 do_line have (lname, t, deps) = 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

355 
have_or_show have lname ^ 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

356 
string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^ 
35966
f8c738abaed8
honor the newly introduced Sledgehammer parameters and fixed the parsing;
blanchet
parents:
35963
diff
changeset

357 
"\"\n by (metis " ^ space_implode " " deps ^ ")\n" 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

358 
fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)] 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

359 
 do_lines ((lname, t, deps) :: lines) = 
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

360 
do_line "have" (lname, t, deps) :: do_lines lines 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

361 
in setmp_CRITICAL show_sorts sorts do_lines end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

362 

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

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

364 

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

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

367 

22731
abfdccaed085
trying to make singlestep proofs work better, especially if they contain
paulson
parents:
22728
diff
changeset

368 
fun replace_dep (old:int, new) dep = if dep=old then new else [dep]; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

369 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

370 
fun replace_deps (old:int, new) (lno, t, deps) = 
33042  371 
(lno, t, List.foldl (uncurry (union (op =))) [] (map (replace_dep (old, new)) deps)); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

372 

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

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

374 
only in type information.*) 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

375 
fun add_prfline ((lno, "axiom", t, []), lines) = (*axioms are not proof lines*) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

376 
if eq_types t (*must be clsrel/clsarity: type information, so delete refs to it*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

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

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

379 
(case take_prefix (unequal t) lines of 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

380 
(_,[]) => lines (*no repetition of proof line*) 
32994  381 
 (pre, (lno', _, _) :: post) => (*repetition: replace later line by earlier one*) 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

382 
pre @ map (replace_deps (lno', [lno])) post) 
32994  383 
 add_prfline ((lno, _, t, []), lines) = (*no deps: conjecture clause*) 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

384 
(lno, t, []) :: lines 
32994  385 
 add_prfline ((lno, _, t, deps), lines) = 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

386 
if eq_types t then (lno, t, deps) :: lines 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

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

388 
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

389 
case take_prefix (unequal t) lines of 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

390 
(_,[]) => (lno, t, deps) :: lines (*no repetition of proof line*) 
32994  391 
 (pre, (lno', t', _) :: post) => 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

392 
(lno, t', deps) :: (*repetition: replace later line by earlier one*) 
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

393 
(pre @ map (replace_deps (lno', [lno])) post); 
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

394 

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

395 
(*Recursively delete empty lines (type information) from the proof.*) 
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

396 
fun add_nonnull_prfline ((lno, t, []), lines) = (*no dependencies, so a conjecture clause*) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

397 
if eq_types t (*must be type information, tfree_tcs, clsrel, clsarity: delete refs to it*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

398 
then delete_dep lno lines 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

399 
else (lno, t, []) :: lines 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

400 
 add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines 
30190  401 
and delete_dep lno lines = List.foldr add_nonnull_prfline [] (map (replace_deps (lno, [])) lines); 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

402 

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

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

405 

23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

406 
(*TVars are forbidden in goals. Also, we don't want lines with <2 dependencies. 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

407 
To further compress proofs, setting modulus:=n deletes every nth line, and nlines 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

408 
counts the number of proof lines processed so far. 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

409 
Deleted lines are replaced by their own dependencies. Note that the "add_nonnull_prfline" 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

410 
phase may delete some dependencies, hence this phase comes later.*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

411 
fun add_wanted_prfline ctxt _ ((lno, t, []), (nlines, lines)) = 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

412 
(nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

413 
 add_wanted_prfline ctxt modulus ((lno, t, deps), (nlines, lines)) = 
29272  414 
if eq_types t orelse not (null (Term.add_tvars t [])) orelse 
29268  415 
exists_subterm bad_free t orelse 
24937
340523598914
contextbased treatment of generalization; also handling TFrees in axiom clauses
paulson
parents:
24920
diff
changeset

416 
(not (null lines) andalso (*final line can't be deleted for these reasons*) 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

417 
(length deps < 2 orelse nlines mod modulus <> 0)) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

418 
then (nlines+1, map (replace_deps (lno, deps)) lines) (*Delete line*) 
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

419 
else (nlines+1, (lno, t, deps) :: lines); 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

420 

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

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

422 
fun stringify_deps thm_names deps_map [] = [] 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

423 
 stringify_deps thm_names deps_map ((lno, t, deps) :: lines) = 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

424 
if lno <= Vector.length thm_names (*axiom*) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

425 
then (Vector.sub(thm_names,lno1), t, []) :: stringify_deps thm_names deps_map lines 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

426 
else let val lname = Int.toString (length deps_map) 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
23083
diff
changeset

427 
fun fix lno = if lno <= Vector.length thm_names 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

428 
then SOME(Vector.sub(thm_names,lno1)) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

429 
else AList.lookup op= deps_map lno; 
32952  430 
in (lname, t, map_filter fix (distinct (op=) deps)) :: 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

431 
stringify_deps thm_names ((lno,lname)::deps_map) lines 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

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

433 

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

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

435 
(if i = 1 then "" else "prefer " ^ string_of_int i ^ "\n") ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

436 
"proof (neg_clausify)\n"; 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

438 
 isar_fixes ts = " fix " ^ space_implode " " ts ^ "\n"; 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

440 
 isar_proof_end _ = "next" 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

441 

36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

442 
fun isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names = 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

443 
let 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

444 
val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: start\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

445 
val tuples = map (dest_tstp o tstp_line o explode) cnfs 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

446 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

447 
Int.toString (length tuples) ^ " tuples extracted\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

448 
val ctxt = ProofContext.set_mode ProofContext.mode_schematic ctxt 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

449 
val raw_lines = List.foldr add_prfline [] (decode_tstp_list ctxt tuples) 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

450 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

451 
Int.toString (length raw_lines) ^ " raw_lines extracted\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

452 
val nonnull_lines = List.foldr add_nonnull_prfline [] raw_lines 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

453 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

454 
Int.toString (length nonnull_lines) ^ " nonnull_lines extracted\n") 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

455 
val (_, lines) = List.foldr (add_wanted_prfline ctxt modulus) (0,[]) nonnull_lines 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

456 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

457 
Int.toString (length lines) ^ " lines extracted\n") 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

458 
val (ccls, fixes) = neg_conjecture_clauses ctxt goal i 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

459 
val _ = trace_proof_msg (fn () => 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

460 
Int.toString (length ccls) ^ " conjecture clauses\n") 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

461 
val ccls = map forall_intr_vars ccls 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

462 
val _ = app (fn th => trace_proof_msg 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

463 
(fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

464 
val body = isar_proof_body ctxt sorts (map prop_of ccls) 
35869
cac366550624
start work on direct proof reconstruction for Sledgehammer
blanchet
parents:
35868
diff
changeset

465 
(stringify_deps thm_names [] lines) 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

466 
val n = Logic.count_prems (prop_of goal) 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

467 
val _ = trace_proof_msg (K "\nisar_proof_from_tstp_file: finishing\n") 
36063
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

469 
isar_proof_start i ^ isar_fixes (map #1 fixes) ^ implode body ^ 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

470 
isar_proof_end n ^ "\n" 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

471 
end 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

472 
handle STREE _ => error "Could not extract proof (ATP output malformed?)"; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

473 

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

474 

33310  475 
(*=== EXTRACTING PROOFTEXT === *) 
31866  476 

35865  477 
val begin_proof_strs = ["# SZS output start CNFRefutation.", 
33310  478 
"=========== Refutation ==========", 
31866  479 
"Here is a proof"]; 
33310  480 

35865  481 
val end_proof_strs = ["# SZS output end CNFRefutation", 
33310  482 
"======= End of refutation =======", 
31866  483 
"Formulae used in the proof"]; 
33310  484 

485 
fun get_proof_extract proof = 

486 
let 

31866  487 
(*splits to_split by the first possible of a list of splitters*) 
488 
val (begin_string, end_string) = 

35865  489 
(find_first (fn s => String.isSubstring s proof) begin_proof_strs, 
490 
find_first (fn s => String.isSubstring s proof) end_proof_strs) 

33310  491 
in 
492 
if is_none begin_string orelse is_none end_string 

493 
then error "Could not extract proof (no substring indicating a proof)" 

494 
else proof > first_field (the begin_string) > the > snd 

495 
> first_field (the end_string) > the > fst 

496 
end; 

31866  497 

35865  498 
(* ==== CHECK IF PROOF WAS SUCCESSFUL === *) 
31866  499 

35865  500 
fun is_proof_well_formed proof = 
501 
exists (fn s => String.isSubstring s proof) begin_proof_strs andalso 

502 
exists (fn s => String.isSubstring s proof) end_proof_strs 

31866  503 

33310  504 
(* === EXTRACTING LEMMAS === *) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

505 
(* A list consisting of the first number in each line is returned. 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

506 
TPTP: Interesting lines have the form "cnf(108, axiom, ...)", where the 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

507 
number (108) is extracted. 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

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

509 
extracted. *) 
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

510 
fun get_step_nums proof_extract = 
35865  511 
let 
512 
val toks = String.tokens (not o Char.isAlphaNum) 

513 
fun inputno ("cnf" :: ntok :: "axiom" :: _) = Int.fromString ntok 

514 
 inputno ("cnf" :: ntok :: "negated" :: "conjecture" :: _) = 

515 
Int.fromString ntok 

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

516 
 inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok (* DFG *) 
35865  517 
 inputno _ = NONE 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

518 
val lines = split_lines proof_extract 
35865  519 
in map_filter (inputno o toks) lines end 
33310  520 

521 
(*Used to label theorems chained into the sledgehammer call*) 

522 
val chained_hint = "CHAINED"; 

35865  523 
val kill_chained = filter_out (curry (op =) chained_hint) 
524 

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

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

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

527 
 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

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

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

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

531 
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

532 
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

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

534 
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

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

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

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

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

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

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

542 

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

543 
fun metis_proof_text minimize_command 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

544 
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

545 
val lemmas = 
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

546 
proof > get_proof_extract 
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

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

548 
> filter (fn i => i <= Vector.length thm_names) 
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

549 
> map (fn i => Vector.sub (thm_names, i  1)) 
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

550 
> filter (fn x => x <> "??.unknown") 
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

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

552 
val n = Logic.count_prems (prop_of goal) 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

553 
val xs = kill_chained lemmas 
cdc6855a6387
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
blanchet
parents:
36001
diff
changeset

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

555 
(metis_line i n xs ^ minimize_line minimize_command xs, kill_chained lemmas) 
36223
217ca1273786
make Sledgehammer's minimizer also minimize Isar proofs
blanchet
parents:
36140
diff
changeset

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

557 

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

558 
fun isar_proof_text debug modulus sorts ctxt minimize_command proof thm_names 
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

559 
goal i = 
33310  560 
let 
36064
48aec67c284f
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
blanchet
parents:
36063
diff
changeset

561 
(* We could use "split_lines", but it can return blank lines. *) 
35865  562 
val lines = String.tokens (equal #"\n"); 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

563 
val kill_spaces = 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

564 
String.translate (fn c => if Char.isSpace c then "" else str c) 
35865  565 
val extract = get_proof_extract proof 
566 
val cnfs = filter (String.isPrefix "cnf(") (map kill_spaces (lines extract)) 

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

567 
val (one_line_proof, lemma_names) = 
36281
dbbf4d5d584d
pass relevant options from "sledgehammer" to "sledgehammer minimize";
blanchet
parents:
36231
diff
changeset

568 
metis_proof_text minimize_command proof thm_names goal i 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

569 
val tokens = String.tokens (fn c => c = #" ") one_line_proof 
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

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

571 
case isar_proof_from_tstp_file cnfs modulus sorts ctxt goal i thm_names of 
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

572 
"" => "" 
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

573 
 isar_proof => Markup.markup Markup.sendback isar_proof 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

574 
val isar_proof = 
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

575 
if member (op =) tokens chained_hint then 
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

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

577 
else if debug then 
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

578 
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

579 
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

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

581 
> the_default "Error: The Isar proof reconstruction failed." 
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

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

583 

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

584 
fun proof_text isar_proof debug modulus sorts ctxt = 
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

585 
if isar_proof then isar_proof_text debug modulus sorts ctxt 
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

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

587 

31038  588 
end; 