author  blanchet 
Fri, 19 Mar 2010 16:04:15 +0100  
changeset 35868  491a97039ce1 
parent 35865  2f8fb5242799 
child 35869  cac366550624 
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 
25492
4cc7976948ac
Chained theorems are no longer mentioned in metis calls and (if used) they prevent the
paulson
parents:
25414
diff
changeset

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

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

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

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

14 
val strip_prefix: string > string > string option 
33243  15 
val setup: theory > theory 
35865  16 
val is_proof_well_formed: string > bool 
17 
val metis_lemma_list: bool > string > 

33243  18 
string * string vector * (int * int) * Proof.context * thm * int > string * string list 
35865  19 
val structured_isar_proof: string > 
33243  20 
string * string vector * (int * int) * Proof.context * thm * int > string * string list 
24425
ca97c6f3d9cd
Returning both a "oneline" proof and a structured proof
paulson
parents:
24387
diff
changeset

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

22 

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

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

25 

35865  26 
open Sledgehammer_FOL_Clause 
27 
open Sledgehammer_Fact_Preprocessor 

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

28 

35865  29 
val trace_proof_path = Path.basic "atp_trace"; 
30 

31 
fun trace_proof_msg f = 

32 
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

33 

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

34 
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

35 

25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25492
diff
changeset

36 
(*For generating structured proofs: keep every nth proof line*) 
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
25999
diff
changeset

37 
val (modulus, modulus_setup) = Attrib.config_int "sledgehammer_modulus" 1; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

38 

25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25492
diff
changeset

39 
(*Indicates whether to include sort information in generated proofs*) 
26333
68e5eee47a45
Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
paulson
parents:
25999
diff
changeset

40 
val (recon_sorts, recon_sorts_setup) = Attrib.config_bool "sledgehammer_sorts" true; 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

41 

28477
9339d4dcec8b
version of sledgehammer using threads instead of processes, misc cleanup;
wenzelm
parents:
27865
diff
changeset

42 
val setup = modulus_setup #> recon_sorts_setup; 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

43 

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

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

45 

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

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

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

48 

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

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

50 

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

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

53 

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

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

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

56 

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

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

58 
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

59 
val truefalse = $$"$"  Symbol.scan_id >> (atom o tf); 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

60 

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

61 
(*Integer constants, typically proof line numbers*) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

62 
fun is_digit s = Char.isDigit (String.sub(s,0)); 
33035  63 
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

64 

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

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

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

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

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

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

71 

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

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

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

74 

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

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

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

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

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

79 

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

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

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

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

83 

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

85 

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

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

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

88 

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

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

90 

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

92 
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

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

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

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

96 

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 
(**** INTERPRETATION OF TSTP SYNTAX TREES ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

99 

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

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

101 

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

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

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

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

107 

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

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

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

111 

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

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

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

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

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

116 

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

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

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

119 

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

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

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

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

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

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

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

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

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

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

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

131 
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

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

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

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

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

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

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

140 

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

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

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

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

145 

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

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

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

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

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

150 

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

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

152 
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

153 

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

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

155 
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

156 

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

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

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

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

161 
Int _ => raise STREE t 
22428  162 
 Br ("hBOOL",[t]) => term_of_stree [] thy t (*ignore hBOOL*) 
163 
 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

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

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

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

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

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

173 
constant.*) 

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

174 
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

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

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

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

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

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

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

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

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

186 

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

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

188 
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

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

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

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

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

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

195 

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

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

197 

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

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

199 

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

200 
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

201 
 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

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

203 

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

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

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

206 

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

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

208 
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

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

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

211 
[] => 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

212 
 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

213 

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

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

216 
 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

217 
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

218 
handle STREE _ => 
22428  219 
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

220 

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

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

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

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

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

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

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

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

230 
 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

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

232 
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

233 

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

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

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

240 

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

242 

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

243 
fun ints_of_stree_aux (Int n, ns) = n::ns 
30190  244 
 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

245 

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

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

247 

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

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

249 
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

250 
val cl = clause_of_strees ctxt vt0 ts 
29268  251 
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

252 

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

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

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

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

256 
 _ => error ("TSTP line not terminated by \".\": " ^ implode chs); 
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 

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

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

260 

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

261 
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

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

263 

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

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

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

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

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

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

269 
 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

270 

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 
(**** Translation of TSTP files to Isar Proofs ****) 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

273 

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

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

275 
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

276 
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

277 

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

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

285 

286 
val strip_alls = strip_alls_aux 0; 

287 

288 
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

289 

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

292 
match_literal t1 t2 (match_literal u1 u2 env) 

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

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

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

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

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

309 

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

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

312 
fun matches_aux _ [] [] = true 

313 
 matches_aux env (lit::lits) ts = 

314 
let fun match1 us [] = false 

315 
 match1 us (t::ts) = 

316 
let val env' = match_literal lit t env 

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

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

31038  321 
in match1 [] ts end; 
23519  322 

323 
(*Is this length test useful?*) 

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

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

327 

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

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

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

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

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

335 

32994  336 
fun have_or_show "show " _ = "show \"" 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

337 
 have_or_show have lname = have ^ lname ^ ": \"" 
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

338 

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

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

340 
ATP may have their literals reordered.*) 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

341 
fun isar_lines ctxt ctms = 
28572  342 
let val string_of = PrintMode.setmp [] (fn term => Syntax.string_of_term ctxt term) 
35865  343 
val _ = trace_proof_msg (K "\n\nisar_lines: start\n") 
32994  344 
fun doline _ (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*) 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

345 
(case permuted_clause t ctms of 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

346 
SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n" 
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

347 
 NONE => "assume? " ^ lname ^ ": \"" ^ string_of t ^ "\"\n") (*no match!!*) 
22470
0d52e5157124
No label on "show"; tries to remove dependencies more cleanly
paulson
parents:
22428
diff
changeset

348 
 doline have (lname, t, deps) = 
23519  349 
have_or_show have lname ^ string_of (gen_all_vars (HOLogic.mk_Trueprop t)) ^ 
22372  350 
"\"\n by (metis " ^ space_implode " " deps ^ ")\n" 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

351 
fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)] 
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

352 
 dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines 
32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32955
diff
changeset

353 
in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end; 
21978
72c21698a055
Contains old Tools/ATP/AtpCommunication.ML, plus proof reconstruction
paulson
parents:
diff
changeset

354 

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

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

356 

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

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

359 

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

360 
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

361 

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

362 
fun replace_deps (old:int, new) (lno, t, deps) = 
33042  363 
(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

364 

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

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

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

367 
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

368 
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

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

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

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

372 
(_,[]) => lines (*no repetition of proof line*) 
32994  373 
 (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

374 
pre @ map (replace_deps (lno', [lno])) post) 
32994  375 
 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

376 
(lno, t, []) :: lines 
32994  377 
 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

378 
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

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

380 
else (*FIXME: Doesn't this code risk conflating proofs involving different types??*) 
22044
6c0702a96076
More compact proof reconstruction: lines having fewer than !min_deps dependences are folded
paulson
parents:
22012
diff
changeset

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

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

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

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

386 

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

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

388 
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

389 
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

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

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

392 
 add_nonnull_prfline ((lno, t, deps), lines) = (lno, t, deps) :: lines 
30190  393 
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

394 

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

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

397 

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

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

399 
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

400 
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

401 
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

402 
phase may delete some dependencies, hence this phase comes later.*) 
25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25492
diff
changeset

403 
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

404 
(nlines, (lno, t, []) :: lines) (*conjecture clauses must be kept*) 
25710
4cdf7de81e1b
Replaced refs by config params; finer critical section in mets method
paulson
parents:
25492
diff
changeset

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

408 
(not (null lines) andalso (*final line can't be deleted for these reasons*) 
31038  409 
(length deps < 2 orelse nlines mod (Config.get ctxt modulus) <> 0)) 
22491
535fbed859da
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
paulson
parents:
22470
diff
changeset

410 
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

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

412 

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

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

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

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

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

417 
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

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

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

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

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

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

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

425 

24547
64c20ee76bc1
Vampire structured proofs. Better parsing; some bug fixes.
paulson
parents:
24493
diff
changeset

426 
val proofstart = "proof (neg_clausify)\n"; 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

427 

80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

428 
fun isar_header [] = proofstart 
21999
0cf192e489e2
improvements to proof reconstruction. Some files loaded in a different order
paulson
parents:
21979
diff
changeset

429 
 isar_header ts = proofstart ^ "fix " ^ space_implode " " ts ^ "\n"; 
21979
80e10f181c46
Improvements to proof reconstruction. Now "fixes" is inserted
paulson
parents:
21978
diff
changeset

430 

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

431 
fun isar_proof_from_tstp_file cnfs ctxt th sgno thm_names = 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

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

433 
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

434 
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

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

436 
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

437 
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

438 
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

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

440 
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

441 
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

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

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

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

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

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

447 
val (ccls, fixes) = neg_conjecture_clauses ctxt th sgno 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

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

449 
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

450 
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

451 
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

452 
(fn () => "\nccl: " ^ string_of_thm ctxt th)) ccls 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

453 
val isar_lines = isar_lines ctxt (map prop_of ccls) 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

454 
(stringify_deps thm_names [] lines) 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

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

456 
in isar_header (map #1 fixes) ^ implode isar_lines ^ "qed\n" end 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

457 
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

458 

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

459 

33310  460 
(*=== EXTRACTING PROOFTEXT === *) 
31866  461 

35865  462 
val begin_proof_strs = ["# SZS output start CNFRefutation.", 
33310  463 
"=========== Refutation ==========", 
31866  464 
"Here is a proof"]; 
33310  465 

35865  466 
val end_proof_strs = ["# SZS output end CNFRefutation", 
33310  467 
"======= End of refutation =======", 
31866  468 
"Formulae used in the proof"]; 
33310  469 

470 
fun get_proof_extract proof = 

471 
let 

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

35865  474 
(find_first (fn s => String.isSubstring s proof) begin_proof_strs, 
475 
find_first (fn s => String.isSubstring s proof) end_proof_strs) 

33310  476 
in 
477 
if is_none begin_string orelse is_none end_string 

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

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

480 
> first_field (the end_string) > the > fst 

481 
end; 

31866  482 

35865  483 
(* ==== CHECK IF PROOF WAS SUCCESSFUL === *) 
31866  484 

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

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

31866  488 

33310  489 
(* === EXTRACTING LEMMAS === *) 
490 
(* lines have the form "cnf(108, axiom, ...", 

491 
the number (108) has to be extracted)*) 

35865  492 
fun get_step_nums false extract = 
493 
let 

494 
val toks = String.tokens (not o Char.isAlphaNum) 

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

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

497 
Int.fromString ntok 

498 
 inputno _ = NONE 

499 
val lines = split_lines extract 

500 
in map_filter (inputno o toks) lines end 

33310  501 
(*String contains multiple lines. We want those of the form 
502 
"253[0:Inp] et cetera..." 

503 
A list consisting of the first number in each line is returned. *) 

504 
 get_step_nums true proofextract = 

505 
let val toks = String.tokens (not o Char.isAlphaNum) 

506 
fun inputno (ntok::"0"::"Inp"::_) = Int.fromString ntok 

507 
 inputno _ = NONE 

508 
val lines = split_lines proofextract 

509 
in map_filter (inputno o toks) lines end 

510 

511 
(*extracting lemmas from tstpoutput between the lines from above*) 

512 
fun extract_lemmas get_step_nums (proof, thm_names, conj_count, _, _, _) = 

513 
let 

35865  514 
(* get the names of axioms from their numbers*) 
515 
fun get_axiom_names thm_names step_nums = 

516 
let 

517 
val last_axiom = Vector.length thm_names 

518 
fun is_axiom n = n <= last_axiom 

519 
fun is_conj n = n >= fst conj_count andalso 

520 
n < fst conj_count + snd conj_count 

521 
fun getname i = Vector.sub(thm_names, i1) 

522 
in 

523 
(sort_distinct string_ord (filter (fn x => x <> "??.unknown") 

524 
(map getname (filter is_axiom step_nums))), 

525 
exists is_conj step_nums) 

526 
end 

527 
in get_axiom_names thm_names (get_step_nums (get_proof_extract proof)) end; 

31410  528 

33310  529 
(*Used to label theorems chained into the sledgehammer call*) 
530 
val chained_hint = "CHAINED"; 

35865  531 
val kill_chained = filter_out (curry (op =) chained_hint) 
532 

33310  533 
(* metiscommand *) 
534 
fun metis_line [] = "apply metis" 

535 
 metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")" 

31038  536 

33310  537 
(* atp_minimize [atp=<prover>] <lemmas> *) 
538 
fun minimize_line _ [] = "" 

539 
 minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^ 

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

540 
Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^ 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

541 
space_implode " " (kill_chained lemmas)) 
31840
beeaa1ed1f47
check if conjectures have been used in proof
immler@in.tum.de
parents:
31479
diff
changeset

542 

35865  543 
fun metis_lemma_list dfg name result = 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

544 
let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

545 
(Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^ 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

546 
minimize_line name lemmas ^ 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

547 
(if used_conj then 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

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

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

550 
"\nWarning: The goal is provable because the context is inconsistent."), 
35865  551 
kill_chained lemmas) 
33310  552 
end; 
31037
ac8669134e7a
added Philipp Meyer's implementation of AtpMinimal
immler@in.tum.de
parents:
30874
diff
changeset

553 

35865  554 
fun structured_isar_proof name (result as (proof, thm_names, conj_count, ctxt, 
555 
goal, subgoalno)) = 

33310  556 
let 
35865  557 
(* Could use "split_lines", but it can return blank lines *) 
558 
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

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

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

563 
val (one_line_proof, lemma_names) = metis_lemma_list false name result 

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

564 
val tokens = String.tokens (fn c => c = #" ") one_line_proof 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

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

566 
if member (op =) tokens chained_hint then "" 
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

567 
else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names 
33310  568 
in 
35868
491a97039ce1
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
blanchet
parents:
35865
diff
changeset

569 
(one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof, 
35865  570 
lemma_names) 
571 
end 

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

572 

31038  573 
end; 