author  obua 
Tue, 13 Sep 2005 17:05:59 +0200  
changeset 17335  7cff05c90a0e 
parent 17328  7bbfb79eda96 
child 17379  85109eec887b 
permissions  rwrr 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

1 
(* Title: HOL/Import/proof_kernel.ML 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

2 
ID: $Id$ 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

3 
Author: Sebastian Skalberg (TU Muenchen) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

4 
*) 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

5 

14516  6 
signature ProofKernel = 
7 
sig 

8 
type hol_type 

9 
type tag 

10 
type term 

11 
type thm 

12 
type ('a,'b) subst 

13 

14 
type proof_info 

15 
datatype proof = Proof of proof_info * proof_content 

16 
and proof_content 

17 
= PRefl of term 

18 
 PInstT of proof * (hol_type,hol_type) subst 

19 
 PSubst of proof list * term * proof 

20 
 PAbs of proof * term 

21 
 PDisch of proof * term 

22 
 PMp of proof * proof 

23 
 PHyp of term 

24 
 PAxm of string * term 

25 
 PDef of string * string * term 

26 
 PTmSpec of string * string list * proof 

27 
 PTyDef of string * string * proof 

28 
 PTyIntro of string * string * string * string * term * term * proof 

29 
 POracle of tag * term list * term 

30 
 PDisk 

31 
 PSpec of proof * term 

32 
 PInst of proof * (term,term) subst 

33 
 PGen of proof * term 

34 
 PGenAbs of proof * term option * term list 

35 
 PImpAS of proof * proof 

36 
 PSym of proof 

37 
 PTrans of proof * proof 

38 
 PComb of proof * proof 

39 
 PEqMp of proof * proof 

40 
 PEqImp of proof 

41 
 PExists of proof * term * term 

42 
 PChoose of term * proof * proof 

43 
 PConj of proof * proof 

44 
 PConjunct1 of proof 

45 
 PConjunct2 of proof 

46 
 PDisj1 of proof * term 

47 
 PDisj2 of proof * term 

48 
 PDisjCases of proof * proof * proof 

49 
 PNotI of proof 

50 
 PNotE of proof 

51 
 PContr of proof * term 

52 

53 
exception PK of string * string 

54 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

55 
val get_proof_dir: string > theory > string option 
14516  56 
val debug : bool ref 
57 
val disk_info_of : proof > (string * string) option 

58 
val set_disk_info_of : proof > string > string > unit 

59 
val mk_proof : proof_content > proof 

60 
val content_of : proof > proof_content 

61 
val import_proof : string > string > theory > (theory > term) option * (theory > proof) 

62 

63 
val rewrite_hol4_term: Term.term > theory > Thm.thm 

64 

65 
val type_of : term > hol_type 

66 

67 
val get_thm : string > string > theory > (theory * thm option) 

68 
val get_def : string > string > term > theory > (theory * thm option) 

69 
val get_axiom: string > string > theory > (theory * thm option) 

70 

71 
val store_thm : string > string > thm > theory > theory * thm 

72 

73 
val to_isa_thm : thm > (term * term) list * Thm.thm 

74 
val to_isa_term: term > Term.term 

75 

76 
val REFL : term > theory > theory * thm 

77 
val ASSUME : term > theory > theory * thm 

78 
val INST_TYPE : (hol_type,hol_type) subst > thm > theory > theory * thm 

79 
val INST : (term,term)subst > thm > theory > theory * thm 

80 
val EQ_MP : thm > thm > theory > theory * thm 

81 
val EQ_IMP_RULE : thm > theory > theory * thm 

82 
val SUBST : thm list > term > thm > theory > theory * thm 

83 
val DISJ_CASES : thm > thm > thm > theory > theory * thm 

84 
val DISJ1: thm > term > theory > theory * thm 

85 
val DISJ2: term > thm > theory > theory * thm 

86 
val IMP_ANTISYM: thm > thm > theory > theory * thm 

87 
val SYM : thm > theory > theory * thm 

88 
val MP : thm > thm > theory > theory * thm 

89 
val GEN : term > thm > theory > theory * thm 

90 
val CHOOSE : term > thm > thm > theory > theory * thm 

91 
val EXISTS : term > term > thm > theory > theory * thm 

92 
val ABS : term > thm > theory > theory * thm 

93 
val GEN_ABS : term option > term list > thm > theory > theory * thm 

94 
val TRANS : thm > thm > theory > theory * thm 

95 
val CCONTR : term > thm > theory > theory * thm 

96 
val CONJ : thm > thm > theory > theory * thm 

97 
val CONJUNCT1: thm > theory > theory * thm 

98 
val CONJUNCT2: thm > theory > theory * thm 

99 
val NOT_INTRO: thm > theory > theory * thm 

100 
val NOT_ELIM : thm > theory > theory * thm 

101 
val SPEC : term > thm > theory > theory * thm 

102 
val COMB : thm > thm > theory > theory * thm 

103 
val DISCH: term > thm > theory > theory * thm 

104 

105 
val type_introduction: string > string > string > string > string > term * term > thm > theory > theory * thm 

106 

107 
val new_definition : string > string > term > theory > theory * thm 

108 
val new_specification : string > string > string list > thm > theory > theory * thm 

109 
val new_type_definition : string > string > string > thm > theory > theory * thm 

110 
val new_axiom : string > term > theory > theory * thm 

111 

17322  112 
val prin : term > unit 
113 

14516  114 
end 
115 

116 
structure ProofKernel :> ProofKernel = 

117 
struct 

118 
type hol_type = Term.typ 

119 
type term = Term.term 

120 
datatype tag = Tag of string list 

121 
type ('a,'b) subst = ('a * 'b) list 

122 
datatype thm = HOLThm of (Term.term * Term.term) list * Thm.thm 

123 

17324  124 
fun hthm2thm (HOLThm (_, th)) = th 
125 

17328  126 

14516  127 
datatype proof_info 
128 
= Info of {disk_info: (string * string) option ref} 

129 

130 
datatype proof = Proof of proof_info * proof_content 

131 
and proof_content 

132 
= PRefl of term 

133 
 PInstT of proof * (hol_type,hol_type) subst 

134 
 PSubst of proof list * term * proof 

135 
 PAbs of proof * term 

136 
 PDisch of proof * term 

137 
 PMp of proof * proof 

138 
 PHyp of term 

139 
 PAxm of string * term 

140 
 PDef of string * string * term 

141 
 PTmSpec of string * string list * proof 

142 
 PTyDef of string * string * proof 

143 
 PTyIntro of string * string * string * string * term * term * proof 

144 
 POracle of tag * term list * term 

145 
 PDisk 

146 
 PSpec of proof * term 

147 
 PInst of proof * (term,term) subst 

148 
 PGen of proof * term 

149 
 PGenAbs of proof * term option * term list 

150 
 PImpAS of proof * proof 

151 
 PSym of proof 

152 
 PTrans of proof * proof 

153 
 PComb of proof * proof 

154 
 PEqMp of proof * proof 

155 
 PEqImp of proof 

156 
 PExists of proof * term * term 

157 
 PChoose of term * proof * proof 

158 
 PConj of proof * proof 

159 
 PConjunct1 of proof 

160 
 PConjunct2 of proof 

161 
 PDisj1 of proof * term 

162 
 PDisj2 of proof * term 

163 
 PDisjCases of proof * proof * proof 

164 
 PNotI of proof 

165 
 PNotE of proof 

166 
 PContr of proof * term 

167 

168 
exception PK of string * string 

169 
fun ERR f mesg = PK (f,mesg) 

170 

171 
fun print_exn e = 

172 
case e of 

173 
PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e) 

174 
 _ => Goals.print_exn e 

175 

176 
(* Compatibility. *) 

177 

14685  178 
fun mk_syn thy c = 
16427  179 
if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn 
14685  180 
else Syntax.literal c 
14516  181 

14673  182 
fun quotename c = 
14685  183 
if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c 
14516  184 

185 
fun smart_string_of_cterm ct = 

186 
let 

187 
val {sign,t,T,...} = rep_cterm ct 

188 
(* Hack to avoid parse errors with Trueprop *) 

189 
val ct = (cterm_of sign (HOLogic.dest_Trueprop t) 

190 
handle TERM _ => ct) 

191 
fun match cu = t aconv (term_of cu) 

192 
fun G 0 = I 

193 
 G 1 = Library.setmp show_types true 

194 
 G 2 = Library.setmp show_all_types true 

195 
 G _ = error ("ProofKernel.smart_string_of_cterm internal error: " ^ (G 2 string_of_cterm ct)) 

196 
fun F sh_br n = 

197 
let 

14980  198 
val str = Library.setmp show_brackets sh_br (G n string_of_cterm) ct 
14516  199 
val cu = transform_error (read_cterm sign) (str,T) 
200 
in 

201 
if match cu 

202 
then quote str 

203 
else F false (n+1) 

204 
end 

205 
handle ERROR_MESSAGE mesg => 

206 
if String.isPrefix "Ambiguous" mesg andalso 

207 
not sh_br 

208 
then F true n 

209 
else F false (n+1) 

210 
in 

15647  211 
transform_error (Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true (F false))) 0 
14516  212 
end 
213 
handle ERROR_MESSAGE mesg => 

214 
(writeln "Exception in smart_string_of_cterm!"; 

215 
writeln mesg; 

14980  216 
quote (string_of_cterm ct)) 
14516  217 

218 
val smart_string_of_thm = smart_string_of_cterm o cprop_of 

219 

220 
fun prth th = writeln ((Library.setmp print_mode [] string_of_thm) th) 

221 
fun prc ct = writeln ((Library.setmp print_mode [] string_of_cterm) ct) 

222 
val prin = Library.setmp print_mode [] prin 

223 
fun pth (HOLThm(ren,thm)) = 

224 
let 

17322  225 
(*val _ = writeln "Renaming:" 
226 
val _ = app (fn(v,w) => (prin v; writeln " >"; prin w)) ren*) 

14516  227 
val _ = prth thm 
228 
in 

229 
() 

230 
end 

231 

232 
fun disk_info_of (Proof(Info{disk_info,...},_)) = !disk_info 

15531  233 
fun mk_proof p = Proof(Info{disk_info = ref NONE},p) 
14516  234 
fun content_of (Proof(_,p)) = p 
235 

236 
fun set_disk_info_of (Proof(Info{disk_info,...},_)) thyname thmname = 

15531  237 
disk_info := SOME(thyname,thmname) 
14516  238 

239 
structure Lib = 

240 
struct 

241 
fun wrap b e s = String.concat[b,s,e] 

242 

243 
fun assoc x = 

244 
let 

245 
fun F [] = raise PK("Lib.assoc","Not found") 

246 
 F ((x',y)::rest) = if x = x' 

247 
then y 

248 
else F rest 

249 
in 

250 
F 

251 
end 

252 
fun i mem L = 

253 
let fun itr [] = false 

254 
 itr (a::rst) = i=a orelse itr rst 

255 
in itr L end; 

256 

257 
fun insert i L = if i mem L then L else i::L 

258 

259 
fun mk_set [] = [] 

260 
 mk_set (a::rst) = insert a (mk_set rst) 

261 

262 
fun [] union S = S 

263 
 S union [] = S 

264 
 (a::rst) union S2 = rst union (insert a S2) 

265 

266 
fun implode_subst [] = [] 

267 
 implode_subst (x::r::rest) = ((x,r)::(implode_subst rest)) 

268 
 implode_subst _ = raise ERR "implode_subst" "malformed substitution list" 

269 

270 
fun apboth f (x,y) = (f x,f y) 

271 
end 

272 
open Lib 

273 

274 
structure Tag = 

275 
struct 

276 
val empty_tag = Tag [] 

277 
fun read name = Tag [name] 

278 
fun merge (Tag tag1) (Tag tag2) = Tag (Lib.union(tag1,tag2)) 

279 
end 

280 

281 
(* Acutal code. *) 

282 

283 
fun get_segment thyname l = (Lib.assoc "s" l 

284 
handle PK _ => thyname) 

14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

285 
val get_name : (string * string) list > string = Lib.assoc "n" 
14516  286 

287 
local 

288 
open LazyScan 

289 
infix 7   

290 
infix 5 :  ^^ 

291 
infix 3 >> 

292 
infix 0  

293 
in 

294 
exception XML of string 

295 

296 
datatype xml = Elem of string * (string * string) list * xml list 

297 
datatype XMLtype = XMLty of xml  FullType of hol_type 

298 
datatype XMLterm = XMLtm of xml  FullTerm of term 

299 

300 
fun pair x y = (x,y) 

301 

302 
fun scan_id toks = 

303 
let 

304 
val (x,toks2) = one Char.isAlpha toks 

305 
val (xs,toks3) = any Char.isAlphaNum toks2 

306 
in 

307 
(String.implode (x::xs),toks3) 

308 
end 

309 

310 
fun scan_string str c = 

311 
let 

312 
fun F [] toks = (c,toks) 

313 
 F (c::cs) toks = 

314 
case LazySeq.getItem toks of 

15531  315 
SOME(c',toks') => 
14516  316 
if c = c' 
317 
then F cs toks' 

318 
else raise SyntaxError 

15531  319 
 NONE => raise SyntaxError 
14516  320 
in 
321 
F (String.explode str) 

322 
end 

323 

324 
local 

325 
val scan_entity = 

326 
(scan_string "amp;" #"&") 

327 
 scan_string "quot;" #"\"" 

328 
 scan_string "gt;" #">" 

329 
 scan_string "lt;" #"<" 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

330 
 scan_string "apos;" #"'" 
14516  331 
in 
332 
fun scan_nonquote toks = 

333 
case LazySeq.getItem toks of 

15531  334 
SOME (c,toks') => 
14516  335 
(case c of 
336 
#"\"" => raise SyntaxError 

337 
 #"&" => scan_entity toks' 

338 
 c => (c,toks')) 

15531  339 
 NONE => raise SyntaxError 
14516  340 
end 
341 

342 
val scan_string = $$ #"\""  repeat scan_nonquote  $$ #"\"" >> 

343 
String.implode 

344 

345 
val scan_attribute = scan_id  $$ #"="  scan_string 

346 

347 
val scan_start_of_tag = $$ #"<"  scan_id  

348 
repeat ($$ #" "  scan_attribute) 

349 

14518
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

350 
(* The evaluation delay introduced through the 'toks' argument is needed 
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

351 
for the sake of the SML/NJ (110.9.1) compiler. Either that or an explicit 
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

352 
type :( *) 
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

353 
fun scan_end_of_tag toks = ($$ #"/"  $$ #">"  succeed []) toks 
c3019a66180f
Added a number of explicit type casts and delayed evaluations (all seemingly
skalberg
parents:
14516
diff
changeset

354 

14516  355 
val scan_end_tag = $$ #"<"  $$ #"/"  scan_id  $$ #">" 
356 

357 
fun scan_children id = $$ #">"  repeat scan_tag  scan_end_tag >> 

358 
(fn (chldr,id') => if id = id' 

359 
then chldr 

360 
else raise XML "Tag mismatch") 

361 
and scan_tag toks = 

362 
let 

363 
val ((id,atts),toks2) = scan_start_of_tag toks 

364 
val (chldr,toks3) = (scan_children id  scan_end_of_tag) toks2 

365 
in 

366 
(Elem (id,atts,chldr),toks3) 

367 
end 

368 
end 

369 

370 
val type_of = Term.type_of 

371 

372 
val boolT = Type("bool",[]) 

373 
val propT = Type("prop",[]) 

374 

375 
fun mk_defeq name rhs thy = 

376 
let 

377 
val ty = type_of rhs 

378 
in 

379 
Logic.mk_equals (Const(Sign.intern_const (sign_of thy) name,ty),rhs) 

380 
end 

381 

382 
fun mk_teq name rhs thy = 

383 
let 

384 
val ty = type_of rhs 

385 
in 

386 
HOLogic.mk_eq (Const(Sign.intern_const (sign_of thy) name,ty),rhs) 

387 
end 

388 

389 
fun intern_const_name thyname const thy = 

390 
case get_hol4_const_mapping thyname const thy of 

15531  391 
SOME (_,cname,_) => cname 
392 
 NONE => (case get_hol4_const_renaming thyname const thy of 

393 
SOME cname => Sign.intern_const (sign_of thy) (thyname ^ "." ^ cname) 

394 
 NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const)) 

14516  395 

396 
fun intern_type_name thyname const thy = 

397 
case get_hol4_type_mapping thyname const thy of 

15531  398 
SOME (_,cname) => cname 
399 
 NONE => Sign.intern_const (sign_of thy) (thyname ^ "." ^ const) 

14516  400 

401 
fun mk_vartype name = TFree(name,["HOL.type"]) 

402 
fun mk_thy_type thy Thy Tyop Args = Type(intern_type_name Thy Tyop thy,Args) 

403 

404 
val mk_var = Free 

405 

406 
fun dom_rng (Type("fun",[dom,rng])) = (dom,rng) 

407 
 dom_rng _ = raise ERR "dom_rng" "Not a functional type" 

408 

16486  409 
fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) 
14516  410 

17322  411 
local 
412 
(* fun get_const sg thyname name = 

413 
(case term_of (read_cterm sg (name, TypeInfer.logicT)) of 

414 
c as Const _ => c) 

415 
handle _ => raise ERR "get_type" (name ^ ": No such constant")*) 

416 
fun get_const sg thyname name = 

417 
(case Sign.const_type sg name of 

418 
SOME ty => Const (name, ty) 

419 
 NONE => raise ERR "get_type" (name ^ ": No such constant")) 

14516  420 
in 
16486  421 
fun prim_mk_const thy Thy Nam = 
14516  422 
let 
16486  423 
val name = intern_const_name Thy Nam thy 
14516  424 
val cmaps = HOL4ConstMaps.get thy 
425 
in 

16486  426 
case StringPair.lookup(cmaps,(Thy,Nam)) of 
15531  427 
SOME(_,_,SOME ty) => Const(name,ty) 
17322  428 
 _ => get_const (sign_of thy) Thy name 
14516  429 
end 
430 
end 

431 

432 
fun mk_comb(f,a) = f $ a 

433 
fun mk_abs(x,a) = Term.lambda x a 

434 

435 
(* Needed for HOL Light *) 

436 
fun protect_tyvarname s = 

437 
let 

438 
fun no_quest s = 

439 
if Char.contains s #"?" 

440 
then String.translate (fn #"?" => "q_"  c => Char.toString c) s 

441 
else s 

442 
fun beg_prime s = 

443 
if String.isPrefix "'" s 

444 
then s 

445 
else "'" ^ s 

446 
in 

447 
s > no_quest > beg_prime 

448 
end 

449 
fun protect_varname s = 

450 
let 

451 
fun no_beg_underscore s = 

452 
if String.isPrefix "_" s 

453 
then "dummy" ^ s 

454 
else s 

455 
in 

456 
s > no_beg_underscore 

457 
end 

458 

17322  459 
val ty_num_prefix = "N_" 
460 

461 
fun startsWithDigit s = Char.isDigit (hd (String.explode s)) 

462 

463 
fun protect_tyname tyn = 

464 
let 

465 
val tyn' = 

466 
if String.isPrefix ty_num_prefix tyn then raise (ERR "conv_ty_name" ("type name '"^tyn^"' is reserved")) else 

467 
(if startsWithDigit tyn then ty_num_prefix^tyn else tyn) 

468 
in 

469 
tyn' 

470 
end 

471 

472 

473 

14516  474 
structure TypeNet = 
475 
struct 

17322  476 

14516  477 
fun get_type_from_index thy thyname types is = 
478 
case Int.fromString is of 

479 
SOME i => (case Array.sub(types,i) of 

480 
FullType ty => ty 

481 
 XMLty xty => 

482 
let 

483 
val ty = get_type_from_xml thy thyname types xty 

484 
val _ = Array.update(types,i,FullType ty) 

485 
in 

486 
ty 

487 
end) 

488 
 NONE => raise ERR "get_type_from_index" "Bad index" 

489 
and get_type_from_xml thy thyname types = 

490 
let 

491 
fun gtfx (Elem("tyi",[("i",iS)],[])) = 

492 
get_type_from_index thy thyname types iS 

493 
 gtfx (Elem("tyc",atts,[])) = 

494 
mk_thy_type thy 

495 
(get_segment thyname atts) 

17322  496 
(protect_tyname (get_name atts)) 
14516  497 
[] 
498 
 gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s) 

499 
 gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) = 

500 
mk_thy_type thy 

501 
(get_segment thyname atts) 

17322  502 
(protect_tyname (get_name atts)) 
14516  503 
(map gtfx tys) 
504 
 gtfx _ = raise ERR "get_type" "Bad type" 

505 
in 

506 
gtfx 

507 
end 

508 

509 
fun input_types thyname (Elem("tylist",[("i",i)],xtys)) = 

510 
let 

511 
val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[]))) 

512 
fun IT _ [] = () 

513 
 IT n (xty::xtys) = 

514 
(Array.update(types,n,XMLty xty); 

515 
IT (n+1) xtys) 

516 
val _ = IT 0 xtys 

517 
in 

518 
types 

519 
end 

520 
 input_types _ _ = raise ERR "input_types" "Bad type list" 

521 
end 

522 

523 
structure TermNet = 

524 
struct 

17322  525 

14516  526 
fun get_term_from_index thy thyname types terms is = 
527 
case Int.fromString is of 

528 
SOME i => (case Array.sub(terms,i) of 

529 
FullTerm tm => tm 

530 
 XMLtm xtm => 

531 
let 

532 
val tm = get_term_from_xml thy thyname types terms xtm 

533 
val _ = Array.update(terms,i,FullTerm tm) 

534 
in 

535 
tm 

536 
end) 

537 
 NONE => raise ERR "get_term_from_index" "Bad index" 

538 
and get_term_from_xml thy thyname types terms = 

539 
let 

15531  540 
fun get_type [] = NONE 
541 
 get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty) 

14516  542 
 get_type _ = raise ERR "get_term" "Bad type" 
543 

544 
fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) = 

545 
mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi) 

546 
 gtfx (Elem("tmc",atts,[])) = 

547 
let 

548 
val segment = get_segment thyname atts 

549 
val name = get_name atts 

550 
in 

551 
mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts)) 

552 
handle PK _ => prim_mk_const thy segment name 

553 
end 

554 
 gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) = 

555 
let 

556 
val f = get_term_from_index thy thyname types terms tmf 

557 
val a = get_term_from_index thy thyname types terms tma 

558 
in 

559 
mk_comb(f,a) 

560 
end 

561 
 gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 

562 
let 

563 
val x = get_term_from_index thy thyname types terms tmx 

564 
val a = get_term_from_index thy thyname types terms tma 

565 
in 

566 
mk_abs(x,a) 

567 
end 

568 
 gtfx (Elem("tmi",[("i",iS)],[])) = 

569 
get_term_from_index thy thyname types terms iS 

570 
 gtfx (Elem(tag,_,_)) = 

571 
raise ERR "get_term" ("Not a term: "^tag) 

572 
in 

573 
gtfx 

574 
end 

575 

576 
fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) = 

577 
let 

578 
val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[]))) 

579 

580 
fun IT _ [] = () 

581 
 IT n (xtm::xtms) = 

582 
(Array.update(terms,n,XMLtm xtm); 

583 
IT (n+1) xtms) 

584 
val _ = IT 0 xtms 

585 
in 

586 
terms 

587 
end 

588 
 input_terms _ _ _ = raise ERR "input_terms" "Bad term list" 

589 
end 

590 

591 
fun get_proof_dir (thyname:string) thy = 

592 
let 

593 
val import_segment = 

594 
case get_segment2 thyname thy of 

15531  595 
SOME seg => seg 
596 
 NONE => get_import_segment thy 

16427  597 
val path = space_explode ":" (getenv "HOL4_PROOFS") 
15531  598 
fun find [] = NONE 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

599 
 find (p::ps) = 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

600 
(let 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

601 
val dir = OS.Path.joinDirFile {dir = p,file=import_segment} 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

602 
in 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

603 
if OS.FileSys.isDir dir 
15531  604 
then SOME dir 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

605 
else find ps 
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

606 
end) handle OS.SysErr _ => find ps 
14516  607 
in 
15570  608 
Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) 
14516  609 
end 
610 

611 
fun proof_file_name thyname thmname thy = 

612 
let 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

613 
val path = case get_proof_dir thyname thy of 
15531  614 
SOME p => p 
615 
 NONE => error "Cannot find proof files" 

14516  616 
val _ = OS.FileSys.mkDir path handle OS.SysErr _ => () 
617 
in 

14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

618 
OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = thmname, ext = SOME "prf"}} 
14516  619 
end 
620 

621 
fun xml_to_proof thyname types terms prf thy = 

622 
let 

623 
val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types 

624 
val xml_to_term = TermNet.get_term_from_xml thy thyname types terms 

625 

626 
fun index_to_term is = 

627 
TermNet.get_term_from_index thy thyname types terms is 

628 

629 
fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is)) 

630 
 x2p (Elem("pinstt",[],p::lambda)) = 

631 
let 

632 
val p = x2p p 

633 
val lambda = implode_subst (map xml_to_hol_type lambda) 

634 
in 

635 
mk_proof (PInstT(p,lambda)) 

636 
end 

637 
 x2p (Elem("psubst",[("i",is)],prf::prfs)) = 

638 
let 

639 
val tm = index_to_term is 

640 
val prf = x2p prf 

641 
val prfs = map x2p prfs 

642 
in 

643 
mk_proof (PSubst(prfs,tm,prf)) 

644 
end 

645 
 x2p (Elem("pabs",[("i",is)],[prf])) = 

646 
let 

647 
val p = x2p prf 

648 
val t = index_to_term is 

649 
in 

650 
mk_proof (PAbs (p,t)) 

651 
end 

652 
 x2p (Elem("pdisch",[("i",is)],[prf])) = 

653 
let 

654 
val p = x2p prf 

655 
val t = index_to_term is 

656 
in 

657 
mk_proof (PDisch (p,t)) 

658 
end 

659 
 x2p (Elem("pmp",[],[prf1,prf2])) = 

660 
let 

661 
val p1 = x2p prf1 

662 
val p2 = x2p prf2 

663 
in 

664 
mk_proof (PMp(p1,p2)) 

665 
end 

666 
 x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is)) 

667 
 x2p (Elem("paxiom",[("n",n),("i",is)],[])) = 

668 
mk_proof (PAxm(n,index_to_term is)) 

669 
 x2p (Elem("pfact",atts,[])) = 

670 
let 

671 
val thyname = get_segment thyname atts 

672 
val thmname = get_name atts 

673 
val p = mk_proof PDisk 

674 
val _ = set_disk_info_of p thyname thmname 

675 
in 

676 
p 

677 
end 

678 
 x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) = 

679 
mk_proof (PDef(seg,name,index_to_term is)) 

680 
 x2p (Elem("ptmspec",[("s",seg)],p::names)) = 

681 
let 

682 
val names = map (fn Elem("name",[("n",name)],[]) => name 

683 
 _ => raise ERR "x2p" "Bad proof (ptmspec)") names 

684 
in 

685 
mk_proof (PTmSpec(seg,names,x2p p)) 

686 
end 

687 
 x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) = 

688 
let 

689 
val P = xml_to_term xP 

690 
val t = xml_to_term xt 

691 
in 

17322  692 
mk_proof (PTyIntro(seg,protect_tyname name,abs_name,rep_name,P,t,x2p p)) 
14516  693 
end 
694 
 x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) = 

17322  695 
mk_proof (PTyDef(seg,protect_tyname name,x2p p)) 
14516  696 
 x2p (xml as Elem("poracle",[],chldr)) = 
697 
let 

698 
val (oracles,terms) = Library.partition (fn (Elem("oracle",_,_)) => true  _ => false) chldr 

699 
val ors = map (fn (Elem("oracle",[("n",name)],[])) => name  xml => raise ERR "x2p" "bad oracle") oracles 

700 
val (c,asl) = case terms of 

701 
[] => raise ERR "x2p" "Bad oracle description" 

702 
 (hd::tl) => (hd,tl) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

703 
val tg = foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors 
14516  704 
in 
705 
mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c)) 

706 
end 

707 
 x2p (Elem("pspec",[("i",is)],[prf])) = 

708 
let 

709 
val p = x2p prf 

710 
val tm = index_to_term is 

711 
in 

712 
mk_proof (PSpec(p,tm)) 

713 
end 

714 
 x2p (Elem("pinst",[],p::theta)) = 

715 
let 

716 
val p = x2p p 

717 
val theta = implode_subst (map xml_to_term theta) 

718 
in 

719 
mk_proof (PInst(p,theta)) 

720 
end 

721 
 x2p (Elem("pgen",[("i",is)],[prf])) = 

722 
let 

723 
val p = x2p prf 

724 
val tm = index_to_term is 

725 
in 

726 
mk_proof (PGen(p,tm)) 

727 
end 

728 
 x2p (Elem("pgenabs",[],prf::tms)) = 

729 
let 

730 
val p = x2p prf 

731 
val tml = map xml_to_term tms 

732 
in 

15531  733 
mk_proof (PGenAbs(p,NONE,tml)) 
14516  734 
end 
735 
 x2p (Elem("pgenabs",[("i",is)],prf::tms)) = 

736 
let 

737 
val p = x2p prf 

738 
val tml = map xml_to_term tms 

739 
in 

15531  740 
mk_proof (PGenAbs(p,SOME (index_to_term is),tml)) 
14516  741 
end 
742 
 x2p (Elem("pimpas",[],[prf1,prf2])) = 

743 
let 

744 
val p1 = x2p prf1 

745 
val p2 = x2p prf2 

746 
in 

747 
mk_proof (PImpAS(p1,p2)) 

748 
end 

749 
 x2p (Elem("psym",[],[prf])) = 

750 
let 

751 
val p = x2p prf 

752 
in 

753 
mk_proof (PSym p) 

754 
end 

755 
 x2p (Elem("ptrans",[],[prf1,prf2])) = 

756 
let 

757 
val p1 = x2p prf1 

758 
val p2 = x2p prf2 

759 
in 

760 
mk_proof (PTrans(p1,p2)) 

761 
end 

762 
 x2p (Elem("pcomb",[],[prf1,prf2])) = 

763 
let 

764 
val p1 = x2p prf1 

765 
val p2 = x2p prf2 

766 
in 

767 
mk_proof (PComb(p1,p2)) 

768 
end 

769 
 x2p (Elem("peqmp",[],[prf1,prf2])) = 

770 
let 

771 
val p1 = x2p prf1 

772 
val p2 = x2p prf2 

773 
in 

774 
mk_proof (PEqMp(p1,p2)) 

775 
end 

776 
 x2p (Elem("peqimp",[],[prf])) = 

777 
let 

778 
val p = x2p prf 

779 
in 

780 
mk_proof (PEqImp p) 

781 
end 

782 
 x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) = 

783 
let 

784 
val p = x2p prf 

785 
val ex = index_to_term ise 

786 
val w = index_to_term isw 

787 
in 

788 
mk_proof (PExists(p,ex,w)) 

789 
end 

790 
 x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) = 

791 
let 

792 
val v = index_to_term is 

793 
val p1 = x2p prf1 

794 
val p2 = x2p prf2 

795 
in 

796 
mk_proof (PChoose(v,p1,p2)) 

797 
end 

798 
 x2p (Elem("pconj",[],[prf1,prf2])) = 

799 
let 

800 
val p1 = x2p prf1 

801 
val p2 = x2p prf2 

802 
in 

803 
mk_proof (PConj(p1,p2)) 

804 
end 

805 
 x2p (Elem("pconjunct1",[],[prf])) = 

806 
let 

807 
val p = x2p prf 

808 
in 

809 
mk_proof (PConjunct1 p) 

810 
end 

811 
 x2p (Elem("pconjunct2",[],[prf])) = 

812 
let 

813 
val p = x2p prf 

814 
in 

815 
mk_proof (PConjunct2 p) 

816 
end 

817 
 x2p (Elem("pdisj1",[("i",is)],[prf])) = 

818 
let 

819 
val p = x2p prf 

820 
val t = index_to_term is 

821 
in 

822 
mk_proof (PDisj1 (p,t)) 

823 
end 

824 
 x2p (Elem("pdisj2",[("i",is)],[prf])) = 

825 
let 

826 
val p = x2p prf 

827 
val t = index_to_term is 

828 
in 

829 
mk_proof (PDisj2 (p,t)) 

830 
end 

831 
 x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) = 

832 
let 

833 
val p1 = x2p prf1 

834 
val p2 = x2p prf2 

835 
val p3 = x2p prf3 

836 
in 

837 
mk_proof (PDisjCases(p1,p2,p3)) 

838 
end 

839 
 x2p (Elem("pnoti",[],[prf])) = 

840 
let 

841 
val p = x2p prf 

842 
in 

843 
mk_proof (PNotI p) 

844 
end 

845 
 x2p (Elem("pnote",[],[prf])) = 

846 
let 

847 
val p = x2p prf 

848 
in 

849 
mk_proof (PNotE p) 

850 
end 

851 
 x2p (Elem("pcontr",[("i",is)],[prf])) = 

852 
let 

853 
val p = x2p prf 

854 
val t = index_to_term is 

855 
in 

856 
mk_proof (PContr (p,t)) 

857 
end 

858 
 x2p xml = raise ERR "x2p" "Bad proof" 

859 
in 

860 
x2p prf 

861 
end 

862 

17322  863 
fun import_proof_concl thyname thmname thy = 
864 
let 

865 
val is = TextIO.openIn(proof_file_name thyname thmname thy) 

866 
val (proof_xml,_) = scan_tag (LazySeq.of_instream is) 

867 
val _ = TextIO.closeIn is 

868 
in 

869 
case proof_xml of 

870 
Elem("proof",[],xtypes::xterms::prf::rest) => 

871 
let 

872 
val types = TypeNet.input_types thyname xtypes 

873 
val terms = TermNet.input_terms thyname types xterms 

874 
fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm 

875 
in 

876 
case rest of 

877 
[] => NONE 

878 
 [xtm] => SOME (f xtm) 

879 
 _ => raise ERR "import_proof" "Bad argument list" 

880 
end 

881 
 _ => raise ERR "import_proof" "Bad proof" 

882 
end 

883 

14516  884 
fun import_proof thyname thmname thy = 
885 
let 

886 
val is = TextIO.openIn(proof_file_name thyname thmname thy) 

887 
val (proof_xml,_) = scan_tag (LazySeq.of_instream is) 

888 
val _ = TextIO.closeIn is 

17322  889 
in 
14516  890 
case proof_xml of 
891 
Elem("proof",[],xtypes::xterms::prf::rest) => 

892 
let 

893 
val types = TypeNet.input_types thyname xtypes 

894 
val terms = TermNet.input_terms thyname types xterms 

895 
in 

896 
(case rest of 

15531  897 
[] => NONE 
898 
 [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm) 

14516  899 
 _ => raise ERR "import_proof" "Bad argument list", 
900 
xml_to_proof thyname types terms prf) 

901 
end 

902 
 _ => raise ERR "import_proof" "Bad proof" 

903 
end 

904 

905 
fun uniq_compose m th i st = 

906 
let 

907 
val res = bicompose false (false,th,m) i st 

908 
in 

909 
case Seq.pull res of 

15531  910 
SOME (th,rest) => (case Seq.pull rest of 
911 
SOME _ => raise ERR "uniq_compose" "Not unique!" 

912 
 NONE => th) 

913 
 NONE => raise ERR "uniq_compose" "No result" 

14516  914 
end 
915 

916 
val reflexivity_thm = thm "refl" 

917 
val substitution_thm = thm "subst" 

918 
val mp_thm = thm "mp" 

919 
val imp_antisym_thm = thm "light_imp_as" 

920 
val disch_thm = thm "impI" 

921 
val ccontr_thm = thm "ccontr" 

922 

923 
val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq" 

924 

925 
val gen_thm = thm "HOLallI" 

926 
val choose_thm = thm "exE" 

927 
val exists_thm = thm "exI" 

928 
val conj_thm = thm "conjI" 

929 
val conjunct1_thm = thm "conjunct1" 

930 
val conjunct2_thm = thm "conjunct2" 

931 
val spec_thm = thm "spec" 

932 
val disj_cases_thm = thm "disjE" 

933 
val disj1_thm = thm "disjI1" 

934 
val disj2_thm = thm "disjI2" 

935 

936 
local 

937 
val th = thm "not_def" 

938 
val sg = sign_of_thm th 

939 
val pp = reflexive (cterm_of sg (Const("Trueprop",boolT>propT))) 

940 
in 

941 
val not_elim_thm = combination pp th 

942 
end 

943 

944 
val not_intro_thm = symmetric not_elim_thm 

945 
val abs_thm = thm "ext" 

946 
val trans_thm = thm "trans" 

947 
val symmetry_thm = thm "sym" 

948 
val transitivity_thm = thm "trans" 

949 
val eqmp_thm = thm "iffD1" 

950 
val eqimp_thm = thm "HOL4Setup.eq_imp" 

951 
val comb_thm = thm "cong" 

952 

953 
(* Betaeta normalizes a theorem (only the conclusion, not the * 

954 
hypotheses!) *) 

955 

956 
fun beta_eta_thm th = 

957 
let 

958 
val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th 

959 
val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1 

960 
in 

961 
th2 

962 
end 

963 

964 
fun implies_elim_all th = 

15570  965 
Library.foldl (fn (th,p) => implies_elim th (assume p)) (th,cprems_of th) 
14516  966 

967 
fun norm_hyps th = 

968 
th > beta_eta_thm 

969 
> implies_elim_all 

970 
> implies_intr_hyps 

971 

972 
fun mk_GEN v th sg = 

973 
let 

974 
val c = HOLogic.dest_Trueprop (concl_of th) 

975 
val cv = cterm_of sg v 

976 
val lc = Term.lambda v c 

977 
val clc = Thm.cterm_of sg lc 

978 
val cvty = ctyp_of_term cv 

979 
val th1 = implies_elim_all th 

980 
val th2 = beta_eta_thm (forall_intr cv th1) 

15531  981 
val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) 
14516  982 
val c = prop_of th3 
983 
val vname = fst(dest_Free v) 

984 
val (cold,cnew) = case c of 

985 
tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) => 

986 
(Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0)) 

987 
 tpc $ (Const("All",allT) $ rest) => (tpc,tpc) 

988 
 _ => raise ERR "mk_GEN" "Unknown conclusion" 

989 
val th4 = Thm.rename_boundvars cold cnew th3 

990 
val res = implies_intr_hyps th4 

991 
in 

992 
res 

993 
end 

994 

995 
(* rotate left k places, leaving the first j and last l premises alone 

996 
*) 

997 

998 
fun permute_prems j k 0 th = Thm.permute_prems j k th 

999 
 permute_prems j k l th = 

1000 
th > Thm.permute_prems 0 (~l) 

1001 
> Thm.permute_prems (j+l) k 

1002 
> Thm.permute_prems 0 l 

1003 

1004 
fun rearrange sg tm th = 

1005 
let 

1006 
val tm' = Pattern.beta_eta_contract tm 

1007 
fun find [] n = permute_prems 0 1 0 (implies_intr (Thm.cterm_of sg tm) th) 

1008 
 find (p::ps) n = if tm' aconv (Pattern.beta_eta_contract p) 

1009 
then permute_prems n 1 0 th 

1010 
else find ps (n+1) 

1011 
in 

1012 
find (prems_of th) 0 

1013 
end 

1014 

1015 
fun zip (x::xs) (y::ys) = (x,y)::(zip xs ys) 

1016 
 zip [] [] = [] 

1017 
 zip _ _ = raise ERR "zip" "arguments not of same length" 

1018 

1019 
fun mk_INST dom rng th = 

1020 
th > forall_intr_list dom 

1021 
> forall_elim_list rng 

1022 

1023 
val collect_vars = 

1024 
let 

1025 
fun F vars (Bound _) = vars 

1026 
 F vars (tm as Free _) = 

1027 
if tm mem vars 

1028 
then vars 

1029 
else (tm::vars) 

1030 
 F vars (Const _) = vars 

1031 
 F vars (tm1 $ tm2) = F (F vars tm1) tm2 

1032 
 F vars (Abs(_,_,body)) = F vars body 

1033 
 F vars (Var _) = raise ERR "collect_vars" "Schematic variable found" 

1034 
in 

1035 
F [] 

1036 
end 

1037 

1038 
(* Code for disambiguating variablenames (wrt. types) *) 

1039 

1040 
val disamb_info_empty = {vars=[],rens=[]} 

1041 

1042 
fun rens_of {vars,rens} = rens 

1043 

1044 
fun name_of_var (Free(vname,_)) = vname 

1045 
 name_of_var _ = raise ERR "name_of_var" "Not a variable" 

1046 

17322  1047 
fun disamb_term_from info tm = (info, tm) 
14516  1048 

1049 
fun swap (x,y) = (y,x) 

1050 

17322  1051 
fun has_ren (HOLThm _) = false 
14516  1052 

1053 
fun prinfo {vars,rens} = (writeln "Vars:"; 

1054 
app prin vars; 

1055 
writeln "Renaming:"; 

1056 
app (fn(x,y)=>(prin x; writeln " >"; prin y)) rens) 

1057 

17322  1058 
fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) 
14516  1059 

17322  1060 
fun disamb_terms_from info tms = (info, tms) 
14516  1061 

17324  1062 
fun disamb_thms_from info hthms = (info, map hthm2thm hthms) 
14516  1063 

1064 
fun disamb_term tm = disamb_term_from disamb_info_empty tm 

1065 
fun disamb_terms tms = disamb_terms_from disamb_info_empty tms 

1066 
fun disamb_thm thm = disamb_thm_from disamb_info_empty thm 

1067 
fun disamb_thms thms = disamb_thms_from disamb_info_empty thms 

1068 

17322  1069 
fun norm_hthm sg (hth as HOLThm _) = hth 
14516  1070 

1071 
(* End of disambiguating code *) 

1072 

1073 
val debug = ref false 

1074 

1075 
fun if_debug f x = if !debug then f x else () 

1076 
val message = if_debug writeln 

1077 

1078 
val conjE_helper = Thm.permute_prems 0 1 conjE 

1079 

1080 
fun get_hol4_thm thyname thmname thy = 

1081 
case get_hol4_theorem thyname thmname thy of 

15531  1082 
SOME hth => SOME (HOLThm hth) 
1083 
 NONE => 

14516  1084 
let 
1085 
val pending = HOL4Pending.get thy 

1086 
in 

1087 
case StringPair.lookup (pending,(thyname,thmname)) of 

15531  1088 
SOME hth => SOME (HOLThm hth) 
1089 
 NONE => NONE 

14516  1090 
end 
1091 

1092 
fun non_trivial_term_consts tm = 

15570  1093 
List.filter (fn c => not (c = "Trueprop" orelse 
14516  1094 
c = "All" orelse 
1095 
c = "op >" orelse 

1096 
c = "op &" orelse 

1097 
c = "op =")) (Term.term_consts tm) 

1098 

1099 
fun match_consts t (* th *) = 

1100 
let 

1101 
fun add_consts (Const (c, _), cs) = 

1102 
(case c of 

1103 
"op =" => "==" ins_string cs 

1104 
 "op >" => "==>" ins_string cs 

1105 
 "All" => cs 

1106 
 "all" => cs 

1107 
 "op &" => cs 

1108 
 "Trueprop" => cs 

1109 
 _ => c ins_string cs) 

1110 
 add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) 

1111 
 add_consts (Abs (_, _, t), cs) = add_consts (t, cs) 

1112 
 add_consts (_, cs) = cs 

1113 
val t_consts = add_consts(t,[]) 

1114 
in 

1115 
fn th => eq_set(t_consts,add_consts(prop_of th,[])) 

1116 
end 

1117 

1118 
fun split_name str = 

1119 
let 

1120 
val sub = Substring.all str 

1121 
val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) 

1122 
val (newstr,u) = apboth Substring.string (Substring.splitr (fn c => c = #"_") f) 

1123 
in 

1124 
if not (idx = "") andalso u = "_" 

15531  1125 
then SOME (newstr,valOf(Int.fromString idx)) 
1126 
else NONE 

14516  1127 
end 
15531  1128 
handle _ => NONE 
14516  1129 

1130 
fun rewrite_hol4_term t thy = 

1131 
let 

1132 
val sg = sign_of thy 

1133 

16427  1134 
val hol4rews1 = map (Thm.transfer sg) (HOL4Rewrites.get thy) 
14516  1135 
val hol4ss = empty_ss setmksimps single addsimps hol4rews1 
1136 
in 

16427  1137 
Thm.transfer sg (Simplifier.full_rewrite hol4ss (cterm_of sg t)) 
14516  1138 
end 
1139 

1140 
fun get_isabelle_thm thyname thmname hol4conc thy = 

1141 
let 

15647  1142 
val _ = message "get_isabelle_thm called..." 
14516  1143 
val sg = sign_of thy 
1144 

1145 
val (info,hol4conc') = disamb_term hol4conc 

1146 
val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) 

1147 
val isaconc = 

1148 
case concl_of i2h_conc of 

1149 
Const("==",_) $ lhs $ _ => lhs 

1150 
 _ => error "get_isabelle_thm" "Bad rewrite rule" 

1151 
val _ = (message "Original conclusion:"; 

1152 
if_debug prin hol4conc'; 

1153 
message "Modified conclusion:"; 

1154 
if_debug prin isaconc) 

1155 

1156 
fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th) 

1157 
in 

1158 
case get_hol4_mapping thyname thmname thy of 

15531  1159 
SOME (SOME thmname) => 
14516  1160 
let 
1161 
val _ = message ("Looking for " ^ thmname) 

16486  1162 
val th1 = (SOME (transform_error (PureThy.get_thm thy) (Name thmname)) 
14516  1163 
handle ERROR_MESSAGE _ => 
1164 
(case split_name thmname of 

16486  1165 
SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx1)) 
15531  1166 
handle _ => NONE) 
1167 
 NONE => NONE)) 

14516  1168 
in 
1169 
case th1 of 

15531  1170 
SOME th2 => 
14516  1171 
(case Shuffler.set_prop thy isaconc [(thmname,th2)] of 
15531  1172 
SOME (_,th) => (message "YES";(thy, SOME (mk_res th))) 
1173 
 NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping")) 

1174 
 NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping") 

14516  1175 
end 
15531  1176 
 SOME NONE => error ("Trying to access ignored theorem " ^ thmname) 
1177 
 NONE => 

14516  1178 
let 
1179 
val _ = (message "Looking for conclusion:"; 

1180 
if_debug prin isaconc) 

1181 
val cs = non_trivial_term_consts isaconc 

1182 
val _ = (message "Looking for consts:"; 

15647  1183 
message (commas cs)) 
14516  1184 
val pot_thms = Shuffler.find_potential thy isaconc 
1185 
val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") 

1186 
in 

1187 
case Shuffler.set_prop thy isaconc pot_thms of 

15531  1188 
SOME (isaname,th) => 
14516  1189 
let 
1190 
val hth as HOLThm args = mk_res th 

1191 
val thy' = thy > add_hol4_theorem thyname thmname args 

1192 
> add_hol4_mapping thyname thmname isaname 

1193 
in 

15531  1194 
(thy',SOME hth) 
14516  1195 
end 
15531  1196 
 NONE => (thy,NONE) 
14516  1197 
end 
1198 
end 

15647  1199 
handle e => (message "Exception in get_isabelle_thm"; if_debug print_exn e handle _ => (); (thy,NONE)) 
14516  1200 

17322  1201 
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy = 
1202 
let 

1203 
val (a, b) = get_isabelle_thm thyname thmname hol4conc thy 

1204 
fun warn () = 

1205 
let 

1206 
val sg = sign_of thy 

1207 
val (info,hol4conc') = disamb_term hol4conc 

1208 
val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) 

1209 
in 

1210 
case concl_of i2h_conc of 

1211 
Const("==",_) $ lhs $ _ => 

1212 
(warning ("Failed lookup of theorem '"^thmname^"':"); 

1213 
writeln "Original conclusion:"; 

1214 
prin hol4conc'; 

1215 
writeln "Modified conclusion:"; 

1216 
prin lhs) 

1217 
 _ => () 

1218 
end 

1219 
in 

1220 
case b of 

1221 
NONE => (warn () handle _ => (); (a,b)) 

1222 
 _ => (a, b) 

1223 
end 

1224 

14516  1225 
fun get_thm thyname thmname thy = 
1226 
case get_hol4_thm thyname thmname thy of 

15531  1227 
SOME hth => (thy,SOME hth) 
17322  1228 
 NONE => ((case import_proof_concl thyname thmname thy of 
1229 
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy 

15647  1230 
 NONE => (message "No conclusion"; (thy,NONE))) 
1231 
handle e as IO.Io _ => (message "IO exception"; (thy,NONE)) 

1232 
 e as PK _ => (message "PK exception"; (thy,NONE))) 

14516  1233 

1234 
fun rename_const thyname thy name = 

1235 
case get_hol4_const_renaming thyname name thy of 

15531  1236 
SOME cname => cname 
1237 
 NONE => name 

14516  1238 

1239 
fun get_def thyname constname rhs thy = 

1240 
let 

1241 
val constname = rename_const thyname thy constname 

1242 
val (thmname,thy') = get_defname thyname constname thy 

1243 
val _ = message ("Looking for definition " ^ thyname ^ "." ^ thmname) 

1244 
in 

17322  1245 
get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' 
14516  1246 
end 
1247 

1248 
fun get_axiom thyname axname thy = 

1249 
case get_thm thyname axname thy of 

15531  1250 
arg as (_,SOME _) => arg 
14516  1251 
 _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")") 
1252 

1253 
fun intern_store_thm gen_output thyname thmname hth thy = 

1254 
let 

1255 
val sg = sign_of thy 

1256 
val (hth' as HOLThm (args as (_,th))) = norm_hthm sg hth 

1257 
val _ = if has_ren hth' then warning ("Theorem " ^ thmname ^ " needs variabledisambiguating") 

1258 
else () 

1259 
val rew = rewrite_hol4_term (concl_of th) thy 

1260 
val th = equal_elim rew th 

1261 
val thy' = add_hol4_pending thyname thmname args thy 

1262 
val thy2 = if gen_output 

1263 
then add_dump ("lemma " ^ thmname ^ ": " ^ (smart_string_of_thm th) ^ "\n by (import " ^ thyname ^ " " ^ thmname ^ ")") thy' 

1264 
else thy' 

1265 
in 

1266 
(thy2,hth') 

1267 
end 

1268 

1269 
val store_thm = intern_store_thm true 

1270 

1271 
fun mk_REFL ctm = 

1272 
let 

1273 
val cty = Thm.ctyp_of_term ctm 

1274 
in 

15531  1275 
Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm 
14516  1276 
end 
1277 

1278 
fun REFL tm thy = 

1279 
let 

1280 
val _ = message "REFL:" 

1281 
val (info,tm') = disamb_term tm 

1282 
val sg = sign_of thy 

1283 
val ctm = Thm.cterm_of sg tm' 

1284 
val res = HOLThm(rens_of info,mk_REFL ctm) 

1285 
val _ = if_debug pth res 

1286 
in 

1287 
(thy,res) 

1288 
end 

1289 

1290 
fun ASSUME tm thy = 

1291 
let 

1292 
val _ = message "ASSUME:" 

1293 
val (info,tm') = disamb_term tm 

1294 
val sg = sign_of thy 

1295 
val ctm = Thm.cterm_of sg (HOLogic.mk_Trueprop tm') 

1296 
val th = Thm.trivial ctm 

1297 
val res = HOLThm(rens_of info,th) 

1298 
val _ = if_debug pth res 

1299 
in 

1300 
(thy,res) 

1301 
end 

1302 

1303 
fun INST_TYPE lambda (hth as HOLThm(rens,th)) thy = 

1304 
let 

1305 
val _ = message "INST_TYPE:" 

1306 
val _ = if_debug pth hth 

1307 
val sg = sign_of thy 

1308 
val tys_before = add_term_tfrees (prop_of th,[]) 

1309 
val th1 = varifyT th 

1310 
val tys_after = add_term_tvars (prop_of th1,[]) 

15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15647
diff
changeset

1311 
val tyinst = map (fn (bef, iS) => 
14516  1312 
(case try (Lib.assoc (TFree bef)) lambda of 
15794
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15647
diff
changeset

1313 
SOME ty => (ctyp_of sg (TVar iS), ctyp_of sg ty) 
5de27a5fc5ed
Adapted to new interface of instantiation and unification / matching functions.
berghofe
parents:
15647
diff
changeset

1314 
 NONE => (ctyp_of sg (TVar iS), ctyp_of sg (TFree bef)) 
14516  1315 
)) 
1316 
(zip tys_before tys_after) 

1317 
val res = Drule.instantiate (tyinst,[]) th1 

17328  1318 
val hth = HOLThm([],res) 
14516  1319 
val res = norm_hthm sg hth 
1320 
val _ = message "RESULT:" 

1321 
val _ = if_debug pth res 

1322 
in 

1323 
(thy,res) 

1324 
end 

1325 

1326 
fun INST sigma hth thy = 

1327 
let 

1328 
val _ = message "INST:" 

1329 
val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma 

1330 
val _ = if_debug pth hth 

1331 
val sg = sign_of thy 

17335
7cff05c90a0e
fixed INST: has same semantic now as INST_TYPE for repetitions
obua
parents:
17328
diff
changeset

1332 
val (sdom,srng) = ListPair.unzip (rev sigma) 
17328  1333 
val th = hthm2thm hth 
1334 
val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th 

1335 
val res = HOLThm([],th1) 

14516  1336 
val _ = message "RESULT:" 
1337 
val _ = if_debug pth res 

1338 
in 

1339 
(thy,res) 

1340 
end 

1341 

1342 
fun EQ_IMP_RULE (hth as HOLThm(rens,th)) thy = 

1343 
let 

1344 
val _ = message "EQ_IMP_RULE:" 

1345 
val _ = if_debug pth hth 

1346 
val res = HOLThm(rens,th RS eqimp_thm) 

1347 
val _ = message "RESULT:" 

1348 
val _ = if_debug pth res 

1349 
in 

1350 
(thy,res) 

1351 
end 

1352 

17322  1353 
fun mk_EQ_MP th1 th2 = [beta_eta_thm th1, beta_eta_thm th2] MRS eqmp_thm 
14516  1354 

1355 
fun EQ_MP hth1 hth2 thy = 

1356 
let 

1357 
val _ = message "EQ_MP:" 

1358 
val _ = if_debug pth hth1 

1359 
val _ = if_debug pth hth2 

1360 
val (info,[th1,th2]) = disamb_thms [hth1,hth2] 

1361 
val res = HOLThm(rens_of info,mk_EQ_MP th1 th2) 

1362 
val _ = message "RESULT:" 

1363 
val _ = if_debug pth res 

1364 
in 

1365 
(thy,res) 

1366 
end 

1367 

1368 
fun mk_COMB th1 th2 sg = 

1369 
let 

1370 
val (f,g) = case concl_of th1 of 

1371 
_ $ (Const("op =",_) $ f $ g) => (f,g) 

1372 
 _ => raise ERR "mk_COMB" "First theorem not an equality" 

1373 
val (x,y) = case concl_of th2 of 

1374 
_ $ (Const("op =",_) $ x $ y) => (x,y) 

1375 
 _ => raise ERR "mk_COMB" "Second theorem not an equality" 

1376 
val fty = type_of f 

1377 
val (fd,fr) = dom_rng fty 

1378 
val comb_thm' = Drule.instantiate' 

15531  1379 
[SOME (ctyp_of sg fd),SOME (ctyp_of sg fr)] 
1380 
[SOME (cterm_of sg f),SOME (cterm_of sg g), 

1381 
SOME (cterm_of sg x),SOME (cterm_of sg y)] comb_thm 

14516  1382 
in 
1383 
[th1,th2] MRS comb_thm' 

1384 
end 

1385 

1386 
fun SUBST rews ctxt hth thy = 

1387 
let 

1388 
val _ = message "SUBST:" 

1389 
val _ = if_debug (app pth) rews 

1390 
val _ = if_debug prin ctxt 

1391 
val _ = if_debug pth hth 

1392 
val (info,th) = disamb_thm hth 

1393 
val (info1,ctxt') = disamb_term_from info ctxt 

1394 
val (info2,rews') = disamb_thms_from info1 rews 

1395 

1396 
val sg = sign_of thy 

1397 
val cctxt = cterm_of sg ctxt' 

1398 
fun subst th [] = th 

1399 
 subst th (rew::rews) = subst (mk_COMB th rew sg) rews 

1400 
val res = HOLThm(rens_of info2,mk_EQ_MP (subst (mk_REFL cctxt) rews') th) 

1401 
val _ = message "RESULT:" 

1402 
val _ = if_debug pth res 

1403 
in 

1404 
(thy,res) 

1405 
end 

1406 

1407 
fun DISJ_CASES hth hth1 hth2 thy = 

1408 
let 

1409 
val _ = message "DISJ_CASES:" 

1410 
val _ = if_debug (app pth) [hth,hth1,hth2] 

1411 
val (info,th) = disamb_thm hth 

1412 
val (info1,th1) = disamb_thm_from info hth1 

1413 
val (info2,th2) = disamb_thm_from info1 hth2 

1414 
val sg = sign_of thy 

1415 
val th1 = norm_hyps th1 

1416 
val th2 = norm_hyps th2 

1417 
val (l,r) = case concl_of th of 

1418 
_ $ (Const("op ",_) $ l $ r) => (l,r) 

1419 
 _ => raise ERR "DISJ_CASES" "Conclusion not a disjunction" 

1420 
val th1' = rearrange sg (HOLogic.mk_Trueprop l) th1 

1421 
val th2' = rearrange sg (HOLogic.mk_Trueprop r) th2 

1422 
val res1 = th RS disj_cases_thm 

1423 
val res2 = uniq_compose ((nprems_of th1')1) th1' ((nprems_of th)+1) res1 

1424 
val res3 = uniq_compose ((nprems_of th2')1) th2' (nprems_of res2) res2 

1425 
val res = HOLThm(rens_of info2,res3) 

1426 
val _ = message "RESULT:" 

1427 
val _ = if_debug pth res 

1428 
in 

1429 
(thy,res) 

1430 
end 

1431 

1432 
fun DISJ1 hth tm thy = 

1433 
let 

1434 
val _ = message "DISJ1:" 

1435 
val _ = if_debug pth hth 

1436 
val _ = if_debug prin tm 

1437 
val (info,th) = disamb_thm hth 

1438 
val (info',tm') = disamb_term_from info tm 

1439 
val sg = sign_of thy 

1440 
val ct = Thm.cterm_of sg tm' 

15531  1441 
val disj1_thm' = Drule.instantiate' [] [NONE,SOME ct] disj1_thm 
14516  1442 
val res = HOLThm(rens_of info',th RS disj1_thm') 
1443 
val _ = message "RESULT:" 

1444 
val _ = if_debug pth res 

1445 
in 

1446 
(thy,res) 

1447 
end 

1448 

1449 
fun DISJ2 tm hth thy = 

1450 
let 

1451 
val _ = message "DISJ1:" 

1452 
val _ = if_debug prin tm 

1453 
val _ = if_debug pth hth 

1454 
val (info,th) = disamb_thm hth 

1455 
val (info',tm') = disamb_term_from info tm 

1456 
val sg = sign_of thy 

1457 
val ct = Thm.cterm_of sg tm' 

15531  1458 
val disj2_thm' = Drule.instantiate' [] [NONE,SOME ct] disj2_thm 
14516  1459 
val res = HOLThm(rens_of info',th RS disj2_thm') 
1460 
val _ = message "RESULT:" 

1461 
val _ = if_debug pth res 

1462 
in 

1463 