author  wenzelm 
Sun, 15 Apr 2007 23:25:50 +0200  
changeset 22709  9ab51bac6287 
parent 22691  290454649b8c 
child 24630  351a308ab58d 
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$ 
17490  3 
Author: Sebastian Skalberg (TU Muenchen), Steven Obua 
14620
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 
17657  56 
val disambiguate_frees : Thm.thm > Thm.thm 
14516  57 
val debug : bool ref 
58 
val disk_info_of : proof > (string * string) option 

59 
val set_disk_info_of : proof > string > string > unit 

60 
val mk_proof : proof_content > proof 

61 
val content_of : proof > proof_content 

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

63 

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

65 

66 
val type_of : term > hol_type 

67 

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

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

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

71 

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

73 

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

75 
val to_isa_term: term > Term.term 

19064  76 
val to_hol_thm : Thm.thm > thm 
14516  77 

78 
val REFL : term > theory > theory * thm 

79 
val ASSUME : term > theory > theory * thm 

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

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

82 
val EQ_MP : thm > thm > theory > theory * thm 

83 
val EQ_IMP_RULE : thm > theory > theory * thm 

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

85 
val DISJ_CASES : thm > thm > thm > theory > theory * thm 

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

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

88 
val IMP_ANTISYM: thm > thm > theory > theory * thm 

89 
val SYM : thm > theory > theory * thm 

90 
val MP : thm > thm > theory > theory * thm 

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

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

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

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

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

96 
val TRANS : thm > thm > theory > theory * thm 

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

98 
val CONJ : thm > thm > theory > theory * thm 

99 
val CONJUNCT1: thm > theory > theory * thm 

100 
val CONJUNCT2: thm > theory > theory * thm 

101 
val NOT_INTRO: thm > theory > theory * thm 

102 
val NOT_ELIM : thm > theory > theory * thm 

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

104 
val COMB : thm > thm > theory > theory * thm 

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

106 

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

108 

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

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

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

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

113 

17322  114 
val prin : term > unit 
19067  115 
val protect_factname : string > string 
116 
val replay_protect_varname : string > string > unit 

19068  117 
val replay_add_dump : string > theory > theory 
14516  118 
end 
119 

120 
structure ProofKernel :> ProofKernel = 

121 
struct 

122 
type hol_type = Term.typ 

123 
type term = Term.term 

124 
datatype tag = Tag of string list 

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

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

127 

17324  128 
fun hthm2thm (HOLThm (_, th)) = th 
129 

19064  130 
fun to_hol_thm th = HOLThm ([], th) 
17328  131 

19068  132 
val replay_add_dump = add_dump 
133 
fun add_dump s thy = (ImportRecorder.add_dump s; replay_add_dump s thy) 

134 

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

137 

138 
datatype proof = Proof of proof_info * proof_content 

139 
and proof_content 

140 
= PRefl of term 

141 
 PInstT of proof * (hol_type,hol_type) subst 

142 
 PSubst of proof list * term * proof 

143 
 PAbs of proof * term 

144 
 PDisch of proof * term 

145 
 PMp of proof * proof 

146 
 PHyp of term 

147 
 PAxm of string * term 

148 
 PDef of string * string * term 

149 
 PTmSpec of string * string list * proof 

150 
 PTyDef of string * string * proof 

151 
 PTyIntro of string * string * string * string * term * term * proof 

152 
 POracle of tag * term list * term 

153 
 PDisk 

154 
 PSpec of proof * term 

155 
 PInst of proof * (term,term) subst 

156 
 PGen of proof * term 

157 
 PGenAbs of proof * term option * term list 

158 
 PImpAS of proof * proof 

159 
 PSym of proof 

160 
 PTrans of proof * proof 

161 
 PComb of proof * proof 

162 
 PEqMp of proof * proof 

163 
 PEqImp of proof 

164 
 PExists of proof * term * term 

165 
 PChoose of term * proof * proof 

166 
 PConj of proof * proof 

167 
 PConjunct1 of proof 

168 
 PConjunct2 of proof 

169 
 PDisj1 of proof * term 

170 
 PDisj2 of proof * term 

171 
 PDisjCases of proof * proof * proof 

172 
 PNotI of proof 

173 
 PNotE of proof 

174 
 PContr of proof * term 

175 

176 
exception PK of string * string 

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

178 

179 
fun print_exn e = 

180 
case e of 

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

17959  182 
 _ => OldGoals.print_exn e 
14516  183 

184 
(* Compatibility. *) 

185 

19264  186 
val string_of_mixfix = Pretty.string_of o Syntax.pretty_mixfix; 
187 

14685  188 
fun mk_syn thy c = 
16427  189 
if Syntax.is_identifier c andalso not (Syntax.is_keyword (Sign.syn_of thy) c) then NoSyn 
14685  190 
else Syntax.literal c 
14516  191 

14673  192 
fun quotename c = 
14685  193 
if Syntax.is_identifier c andalso not (OuterSyntax.is_keyword c) then c else quote c 
14516  194 

17652  195 
fun simple_smart_string_of_cterm ct = 
196 
let 

22596  197 
val {thy,t,T,...} = rep_cterm ct 
17652  198 
(* Hack to avoid parse errors with Trueprop *) 
22596  199 
val ct = (cterm_of thy (HOLogic.dest_Trueprop t) 
17652  200 
handle TERM _ => ct) 
201 
in 

202 
quote( 

203 
Library.setmp print_mode [] ( 

204 
Library.setmp show_brackets false ( 

205 
Library.setmp show_all_types true ( 

206 
Library.setmp Syntax.ambiguity_is_error false ( 

207 
Library.setmp show_sorts true string_of_cterm)))) 

208 
ct) 

209 
end 

210 

19064  211 
exception SMART_STRING 
212 

14516  213 
fun smart_string_of_cterm ct = 
214 
let 

22596  215 
val {thy,t,T,...} = rep_cterm ct 
14516  216 
(* Hack to avoid parse errors with Trueprop *) 
22596  217 
val ct = (cterm_of thy (HOLogic.dest_Trueprop t) 
14516  218 
handle TERM _ => ct) 
219 
fun match cu = t aconv (term_of cu) 

17652  220 
fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true) 
19064  221 
 G 1 = Library.setmp show_brackets true (G 0) 
222 
 G 2 = Library.setmp show_all_types true (G 0) 

223 
 G 3 = Library.setmp show_brackets true (G 2) 

224 
 G _ = raise SMART_STRING 

17652  225 
fun F n = 
14516  226 
let 
17652  227 
val str = Library.setmp show_brackets false (G n string_of_cterm) ct 
22675
acf10be7dcca
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
wenzelm
parents:
22596
diff
changeset

228 
val cu = Thm.read_cterm thy (str,T) 
14516  229 
in 
230 
if match cu 

231 
then quote str 

17652  232 
else F (n+1) 
14516  233 
end 
18678  234 
handle ERROR mesg => F (n+1) 
19064  235 
 SMART_STRING => raise ERROR ("smart_string failed for: "^(G 0 string_of_cterm ct)) 
14516  236 
in 
18678  237 
Library.setmp print_mode [] (Library.setmp Syntax.ambiguity_is_error true F) 0 
14516  238 
end 
18678  239 
handle ERROR mesg => simple_smart_string_of_cterm ct 
17652  240 

14516  241 
val smart_string_of_thm = smart_string_of_cterm o cprop_of 
242 

17917  243 
fun prth th = writeln (Library.setmp print_mode [] string_of_thm th) 
244 
fun prc ct = writeln (Library.setmp print_mode [] string_of_cterm ct) 

245 
fun prin t = writeln 

246 
(Library.setmp print_mode [] (fn () => Sign.string_of_term (the_context ()) t) ()); 

14516  247 
fun pth (HOLThm(ren,thm)) = 
248 
let 

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

14516  251 
val _ = prth thm 
252 
in 

253 
() 

254 
end 

255 

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

15531  257 
fun mk_proof p = Proof(Info{disk_info = ref NONE},p) 
14516  258 
fun content_of (Proof(_,p)) = p 
259 

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

15531  261 
disk_info := SOME(thyname,thmname) 
14516  262 

263 
structure Lib = 

264 
struct 

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

266 

267 
fun assoc x = 

268 
let 

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

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

271 
then y 

272 
else F rest 

273 
in 

274 
F 

275 
end 

276 
fun i mem L = 

277 
let fun itr [] = false 

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

279 
in itr L end; 

280 

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

282 

283 
fun mk_set [] = [] 

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

285 

286 
fun [] union S = S 

287 
 S union [] = S 

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

289 

290 
fun implode_subst [] = [] 

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

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

293 

294 
end 

295 
open Lib 

296 

297 
structure Tag = 

298 
struct 

299 
val empty_tag = Tag [] 

300 
fun read name = Tag [name] 

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

302 
end 

303 

304 
(* Acutal code. *) 

305 

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

307 
handle PK _ => thyname) 

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

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

310 
local 

311 
open LazyScan 

312 
infix 7   

313 
infix 5 :  ^^ 

314 
infix 3 >> 

315 
infix 0  

316 
in 

317 
exception XML of string 

318 

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

320 
datatype XMLtype = XMLty of xml  FullType of hol_type 

321 
datatype XMLterm = XMLtm of xml  FullTerm of term 

322 

323 
fun pair x y = (x,y) 

324 

325 
fun scan_id toks = 

326 
let 

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

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

329 
in 

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

331 
end 

332 

333 
fun scan_string str c = 

334 
let 

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

336 
 F (c::cs) toks = 

337 
case LazySeq.getItem toks of 

15531  338 
SOME(c',toks') => 
14516  339 
if c = c' 
340 
then F cs toks' 

341 
else raise SyntaxError 

15531  342 
 NONE => raise SyntaxError 
14516  343 
in 
344 
F (String.explode str) 

345 
end 

346 

347 
local 

348 
val scan_entity = 

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

350 
 scan_string "quot;" #"\"" 

351 
 scan_string "gt;" #">" 

352 
 scan_string "lt;" #"<" 

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

353 
 scan_string "apos;" #"'" 
14516  354 
in 
355 
fun scan_nonquote toks = 

356 
case LazySeq.getItem toks of 

15531  357 
SOME (c,toks') => 
14516  358 
(case c of 
359 
#"\"" => raise SyntaxError 

360 
 #"&" => scan_entity toks' 

361 
 c => (c,toks')) 

15531  362 
 NONE => raise SyntaxError 
14516  363 
end 
364 

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

366 
String.implode 

367 

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

369 

370 
val scan_start_of_tag = $$ #"<"  scan_id  

371 
repeat ($$ #" "  scan_attribute) 

372 

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

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

374 
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

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

376 
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

377 

14516  378 
val scan_end_tag = $$ #"<"  $$ #"/"  scan_id  $$ #">" 
379 

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

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

382 
then chldr 

383 
else raise XML "Tag mismatch") 

384 
and scan_tag toks = 

385 
let 

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

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

388 
in 

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

390 
end 

391 
end 

392 

393 
val type_of = Term.type_of 

394 

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

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

397 

398 
fun mk_defeq name rhs thy = 

399 
let 

400 
val ty = type_of rhs 

401 
in 

17894  402 
Logic.mk_equals (Const(Sign.intern_const thy name,ty),rhs) 
14516  403 
end 
404 

405 
fun mk_teq name rhs thy = 

406 
let 

407 
val ty = type_of rhs 

408 
in 

17894  409 
HOLogic.mk_eq (Const(Sign.intern_const thy name,ty),rhs) 
14516  410 
end 
411 

412 
fun intern_const_name thyname const thy = 

413 
case get_hol4_const_mapping thyname const thy of 

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

17894  416 
SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname) 
417 
 NONE => Sign.intern_const thy (thyname ^ "." ^ const)) 

14516  418 

419 
fun intern_type_name thyname const thy = 

420 
case get_hol4_type_mapping thyname const thy of 

15531  421 
SOME (_,cname) => cname 
17894  422 
 NONE => Sign.intern_const thy (thyname ^ "." ^ const) 
14516  423 

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

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

426 

427 
val mk_var = Free 

428 

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

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

431 

16486  432 
fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty) 
14516  433 

17322  434 
local 
17894  435 
fun get_const sg thyname name = 
436 
(case Sign.const_type sg name of 

437 
SOME ty => Const (name, ty) 

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

14516  439 
in 
16486  440 
fun prim_mk_const thy Thy Nam = 
14516  441 
let 
17894  442 
val name = intern_const_name Thy Nam thy 
443 
val cmaps = HOL4ConstMaps.get thy 

14516  444 
in 
17894  445 
case StringPair.lookup cmaps (Thy,Nam) of 
446 
SOME(_,_,SOME ty) => Const(name,ty) 

447 
 _ => get_const thy Thy name 

14516  448 
end 
449 
end 

450 

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

452 

453 
(* Needed for HOL Light *) 

454 
fun protect_tyvarname s = 

455 
let 

456 
fun no_quest s = 

457 
if Char.contains s #"?" 

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

459 
else s 

460 
fun beg_prime s = 

461 
if String.isPrefix "'" s 

462 
then s 

463 
else "'" ^ s 

464 
in 

465 
s > no_quest > beg_prime 

466 
end 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

467 

17444  468 
val protected_varnames = ref (Symtab.empty:string Symtab.table) 
469 
val invented_isavar = ref (IntInf.fromInt 0) 

470 

17490  471 
fun innocent_varname s = Syntax.is_identifier s andalso not (String.isPrefix "u_" s) 
472 

18678  473 
val check_name_thy = theory "Main" 
17592  474 

18678  475 
fun valid_boundvarname s = 
22709  476 
can (fn () => Thm.read_cterm check_name_thy ("SOME "^s^". True", dummyT)) (); 
18678  477 

478 
fun valid_varname s = 

22709  479 
can (fn () => Thm.read_cterm check_name_thy (s, dummyT)) (); 
17490  480 

14516  481 
fun protect_varname s = 
17490  482 
if innocent_varname s andalso valid_varname s then s else 
17444  483 
case Symtab.lookup (!protected_varnames) s of 
484 
SOME t => t 

485 
 NONE => 

486 
let 

487 
val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) 

17490  488 
val t = "u_"^(IntInf.toString (!invented_isavar)) 
19067  489 
val _ = ImportRecorder.protect_varname s t 
17444  490 
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) 
491 
in 

492 
t 

493 
end 

14516  494 

19067  495 
exception REPLAY_PROTECT_VARNAME of string*string*string 
496 

497 
fun replay_protect_varname s t = 

498 
case Symtab.lookup (!protected_varnames) s of 

499 
SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') 

500 
 NONE => 

501 
let 

502 
val _ = invented_isavar := IntInf.+ (!invented_isavar, IntInf.fromInt 1) 

503 
val t = "u_"^(IntInf.toString (!invented_isavar)) 

504 
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) 

505 
in 

506 
() 

507 
end 

508 

17490  509 
fun protect_boundvarname s = if innocent_varname s andalso valid_boundvarname s then s else "u" 
17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

510 

df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

511 
fun mk_lambda (v as Free (x, T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

512 
 mk_lambda (v as Var ((x, _), T)) t = Abs (protect_boundvarname x, T, abstract_over (v, t)) 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

513 
 mk_lambda v t = raise TERM ("lambda", [v, t]); 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

514 

df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

515 
fun replacestr x y s = 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

516 
let 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

517 
val xl = explode x 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

518 
val yl = explode y 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

519 
fun isprefix [] ys = true 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

520 
 isprefix (x::xs) (y::ys) = if x = y then isprefix xs ys else false 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

521 
 isprefix _ _ = false 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

522 
fun isp s = isprefix xl s 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

523 
fun chg s = yl@(List.drop (s, List.length xl)) 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

524 
fun r [] = [] 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

525 
 r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

526 
in 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

527 
implode(r (explode s)) 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

528 
end 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

529 

df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

530 
fun protect_factname s = replacestr "." "_dot_" s 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

531 
fun unprotect_factname s = replacestr "_dot_" "." s 
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

532 

17322  533 
val ty_num_prefix = "N_" 
534 

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

536 

537 
fun protect_tyname tyn = 

538 
let 

539 
val tyn' = 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

540 
if String.isPrefix ty_num_prefix tyn then raise (ERR "protect_ty_name" ("type name '"^tyn^"' is reserved")) else 
17322  541 
(if startsWithDigit tyn then ty_num_prefix^tyn else tyn) 
542 
in 

543 
tyn' 

544 
end 

545 

17444  546 
fun protect_constname tcn = tcn 
547 
(* if tcn = ".." then "dotdot" 

548 
else if tcn = "==" then "eqeq" 

549 
else tcn*) 

17322  550 

14516  551 
structure TypeNet = 
552 
struct 

17322  553 

14516  554 
fun get_type_from_index thy thyname types is = 
555 
case Int.fromString is of 

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

557 
FullType ty => ty 

558 
 XMLty xty => 

559 
let 

560 
val ty = get_type_from_xml thy thyname types xty 

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

562 
in 

563 
ty 

564 
end) 

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

566 
and get_type_from_xml thy thyname types = 

567 
let 

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

569 
get_type_from_index thy thyname types iS 

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

571 
mk_thy_type thy 

572 
(get_segment thyname atts) 

17322  573 
(protect_tyname (get_name atts)) 
14516  574 
[] 
575 
 gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s) 

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

577 
mk_thy_type thy 

578 
(get_segment thyname atts) 

17322  579 
(protect_tyname (get_name atts)) 
14516  580 
(map gtfx tys) 
581 
 gtfx _ = raise ERR "get_type" "Bad type" 

582 
in 

583 
gtfx 

584 
end 

585 

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

587 
let 

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

589 
fun IT _ [] = () 

590 
 IT n (xty::xtys) = 

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

592 
IT (n+1) xtys) 

593 
val _ = IT 0 xtys 

594 
in 

595 
types 

596 
end 

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

598 
end 

599 

600 
structure TermNet = 

601 
struct 

17322  602 

14516  603 
fun get_term_from_index thy thyname types terms is = 
604 
case Int.fromString is of 

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

606 
FullTerm tm => tm 

607 
 XMLtm xtm => 

608 
let 

609 
val tm = get_term_from_xml thy thyname types terms xtm 

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

611 
in 

612 
tm 

613 
end) 

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

615 
and get_term_from_xml thy thyname types terms = 

616 
let 

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

14516  619 
 get_type _ = raise ERR "get_term" "Bad type" 
620 

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

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

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

624 
let 

625 
val segment = get_segment thyname atts 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

626 
val name = protect_constname(get_name atts) 
14516  627 
in 
628 
mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts)) 

629 
handle PK _ => prim_mk_const thy segment name 

630 
end 

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

632 
let 

633 
val f = get_term_from_index thy thyname types terms tmf 

634 
val a = get_term_from_index thy thyname types terms tma 

635 
in 

636 
mk_comb(f,a) 

637 
end 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

638 
 gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
17490  639 
let 
640 
val x = get_term_from_index thy thyname types terms tmx 

641 
val a = get_term_from_index thy thyname types terms tma 

14516  642 
in 
17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

643 
mk_lambda x a 
14516  644 
end 
645 
 gtfx (Elem("tmi",[("i",iS)],[])) = 

646 
get_term_from_index thy thyname types terms iS 

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

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

649 
in 

650 
gtfx 

651 
end 

652 

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

654 
let 

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

656 

657 
fun IT _ [] = () 

658 
 IT n (xtm::xtms) = 

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

660 
IT (n+1) xtms) 

661 
val _ = IT 0 xtms 

662 
in 

663 
terms 

664 
end 

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

666 
end 

667 

668 
fun get_proof_dir (thyname:string) thy = 

669 
let 

670 
val import_segment = 

671 
case get_segment2 thyname thy of 

15531  672 
SOME seg => seg 
673 
 NONE => get_import_segment thy 

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

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

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

678 
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

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

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

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

683 
end) handle OS.SysErr _ => find ps 
14516  684 
in 
15570  685 
Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) 
14516  686 
end 
687 

688 
fun proof_file_name thyname thmname thy = 

689 
let 

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

690 
val path = case get_proof_dir thyname thy of 
15531  691 
SOME p => p 
692 
 NONE => error "Cannot find proof files" 

14516  693 
val _ = OS.FileSys.mkDir path handle OS.SysErr _ => () 
694 
in 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

695 
OS.Path.joinDirFile {dir = path, file = OS.Path.joinBaseExt {base = (unprotect_factname thmname), ext = SOME "prf"}} 
14516  696 
end 
697 

698 
fun xml_to_proof thyname types terms prf thy = 

699 
let 

700 
val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types 

701 
val xml_to_term = TermNet.get_term_from_xml thy thyname types terms 

702 

703 
fun index_to_term is = 

704 
TermNet.get_term_from_index thy thyname types terms is 

705 

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

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

708 
let 

709 
val p = x2p p 

710 
val lambda = implode_subst (map xml_to_hol_type lambda) 

711 
in 

712 
mk_proof (PInstT(p,lambda)) 

713 
end 

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

715 
let 

716 
val tm = index_to_term is 

717 
val prf = x2p prf 

718 
val prfs = map x2p prfs 

719 
in 

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

721 
end 

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

723 
let 

724 
val p = x2p prf 

725 
val t = index_to_term is 

726 
in 

727 
mk_proof (PAbs (p,t)) 

728 
end 

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

730 
let 

731 
val p = x2p prf 

732 
val t = index_to_term is 

733 
in 

734 
mk_proof (PDisch (p,t)) 

735 
end 

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

737 
let 

738 
val p1 = x2p prf1 

739 
val p2 = x2p prf2 

740 
in 

741 
mk_proof (PMp(p1,p2)) 

742 
end 

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

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

745 
mk_proof (PAxm(n,index_to_term is)) 

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

747 
let 

748 
val thyname = get_segment thyname atts 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

749 
val thmname = protect_factname (get_name atts) 
14516  750 
val p = mk_proof PDisk 
751 
val _ = set_disk_info_of p thyname thmname 

752 
in 

753 
p 

754 
end 

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

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

756 
mk_proof (PDef(seg,protect_constname name,index_to_term is)) 
14516  757 
 x2p (Elem("ptmspec",[("s",seg)],p::names)) = 
758 
let 

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

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

761 
in 

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

763 
end 

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

765 
let 

766 
val P = xml_to_term xP 

767 
val t = xml_to_term xt 

768 
in 

17440
df77edc4f5d0
fixed HOLlight/Isabelle syntax incompatability via more protect_xxx functions
obua
parents:
17412
diff
changeset

769 
mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p)) 
14516  770 
end 
771 
 x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) = 

17322  772 
mk_proof (PTyDef(seg,protect_tyname name,x2p p)) 
14516  773 
 x2p (xml as Elem("poracle",[],chldr)) = 
774 
let 

19686  775 
val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true  _ => false) chldr 
14516  776 
val ors = map (fn (Elem("oracle",[("n",name)],[])) => name  xml => raise ERR "x2p" "bad oracle") oracles 
777 
val (c,asl) = case terms of 

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

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

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

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

783 
end 

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

785 
let 

786 
val p = x2p prf 

787 
val tm = index_to_term is 

788 
in 

789 
mk_proof (PSpec(p,tm)) 

790 
end 

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

792 
let 

793 
val p = x2p p 

794 
val theta = implode_subst (map xml_to_term theta) 

795 
in 

796 
mk_proof (PInst(p,theta)) 

797 
end 

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

799 
let 

800 
val p = x2p prf 

801 
val tm = index_to_term is 

802 
in 

803 
mk_proof (PGen(p,tm)) 

804 
end 

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

806 
let 

807 
val p = x2p prf 

808 
val tml = map xml_to_term tms 

809 
in 

15531  810 
mk_proof (PGenAbs(p,NONE,tml)) 
14516  811 
end 
812 
 x2p (Elem("pgenabs",[("i",is)],prf::tms)) = 

813 
let 

814 
val p = x2p prf 

815 
val tml = map xml_to_term tms 

816 
in 

15531  817 
mk_proof (PGenAbs(p,SOME (index_to_term is),tml)) 
14516  818 
end 
819 
 x2p (Elem("pimpas",[],[prf1,prf2])) = 

820 
let 

821 
val p1 = x2p prf1 

822 
val p2 = x2p prf2 

823 
in 

824 
mk_proof (PImpAS(p1,p2)) 

825 
end 

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

827 
let 

828 
val p = x2p prf 

829 
in 

830 
mk_proof (PSym p) 

831 
end 

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

833 
let 

834 
val p1 = x2p prf1 

835 
val p2 = x2p prf2 

836 
in 

837 
mk_proof (PTrans(p1,p2)) 

838 
end 

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

840 
let 

841 
val p1 = x2p prf1 

842 
val p2 = x2p prf2 

843 
in 

844 
mk_proof (PComb(p1,p2)) 

845 
end 

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

847 
let 

848 
val p1 = x2p prf1 

849 
val p2 = x2p prf2 

850 
in 

851 
mk_proof (PEqMp(p1,p2)) 

852 
end 

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

854 
let 

855 
val p = x2p prf 

856 
in 

857 
mk_proof (PEqImp p) 

858 
end 

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

860 
let 

861 
val p = x2p prf 

862 
val ex = index_to_term ise 

863 
val w = index_to_term isw 

864 
in 

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

866 
end 

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

868 
let 

869 
val v = index_to_term is 

870 
val p1 = x2p prf1 

871 
val p2 = x2p prf2 

872 
in 

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

874 
end 

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

876 
let 

877 
val p1 = x2p prf1 

878 
val p2 = x2p prf2 

879 
in 

880 
mk_proof (PConj(p1,p2)) 

881 
end 

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

883 
let 

884 
val p = x2p prf 

885 
in 

886 
mk_proof (PConjunct1 p) 

887 
end 

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

889 
let 

890 
val p = x2p prf 

891 
in 

892 
mk_proof (PConjunct2 p) 

893 
end 

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

895 
let 

896 
val p = x2p prf 

897 
val t = index_to_term is 

898 
in 

899 
mk_proof (PDisj1 (p,t)) 

900 
end 

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

902 
let 

903 
val p = x2p prf 

904 
val t = index_to_term is 

905 
in 

906 
mk_proof (PDisj2 (p,t)) 

907 
end 

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

909 
let 

910 
val p1 = x2p prf1 

911 
val p2 = x2p prf2 

912 
val p3 = x2p prf3 

913 
in 

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

915 
end 

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

917 
let 

918 
val p = x2p prf 

919 
in 

920 
mk_proof (PNotI p) 

921 
end 

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

923 
let 

924 
val p = x2p prf 

925 
in 

926 
mk_proof (PNotE p) 

927 
end 

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

929 
let 

930 
val p = x2p prf 

931 
val t = index_to_term is 

932 
in 

933 
mk_proof (PContr (p,t)) 

934 
end 

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

936 
in 

937 
x2p prf 

938 
end 

939 

17322  940 
fun import_proof_concl thyname thmname thy = 
941 
let 

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

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

944 
val _ = TextIO.closeIn is 

945 
in 

946 
case proof_xml of 

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

948 
let 

949 
val types = TypeNet.input_types thyname xtypes 

950 
val terms = TermNet.input_terms thyname types xterms 

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

952 
in 

953 
case rest of 

954 
[] => NONE 

955 
 [xtm] => SOME (f xtm) 

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

957 
end 

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

959 
end 

960 

14516  961 
fun import_proof thyname thmname thy = 
962 
let 

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

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

965 
val _ = TextIO.closeIn is 

17322  966 
in 
14516  967 
case proof_xml of 
968 
Elem("proof",[],xtypes::xterms::prf::rest) => 

969 
let 

970 
val types = TypeNet.input_types thyname xtypes 

971 
val terms = TermNet.input_terms thyname types xterms 

972 
in 

973 
(case rest of 

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

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

978 
end 

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

980 
end 

981 

982 
fun uniq_compose m th i st = 

983 
let 

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

985 
in 

986 
case Seq.pull res of 

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

989 
 NONE => th) 

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

14516  991 
end 
992 

993 
val reflexivity_thm = thm "refl" 

994 
val substitution_thm = thm "subst" 

995 
val mp_thm = thm "mp" 

996 
val imp_antisym_thm = thm "light_imp_as" 

997 
val disch_thm = thm "impI" 

998 
val ccontr_thm = thm "ccontr" 

999 

1000 
val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq" 

1001 

1002 
val gen_thm = thm "HOLallI" 

1003 
val choose_thm = thm "exE" 

1004 
val exists_thm = thm "exI" 

1005 
val conj_thm = thm "conjI" 

1006 
val conjunct1_thm = thm "conjunct1" 

1007 
val conjunct2_thm = thm "conjunct2" 

1008 
val spec_thm = thm "spec" 

1009 
val disj_cases_thm = thm "disjE" 

1010 
val disj1_thm = thm "disjI1" 

1011 
val disj2_thm = thm "disjI2" 

1012 

1013 
local 

1014 
val th = thm "not_def" 

17894  1015 
val thy = theory_of_thm th 
1016 
val pp = reflexive (cterm_of thy (Const("Trueprop",boolT>propT))) 

14516  1017 
in 
1018 
val not_elim_thm = combination pp th 

1019 
end 

1020 

1021 
val not_intro_thm = symmetric not_elim_thm 

1022 
val abs_thm = thm "ext" 

1023 
val trans_thm = thm "trans" 

1024 
val symmetry_thm = thm "sym" 

1025 
val transitivity_thm = thm "trans" 

1026 
val eqmp_thm = thm "iffD1" 

1027 
val eqimp_thm = thm "HOL4Setup.eq_imp" 

1028 
val comb_thm = thm "cong" 

1029 

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

1031 
hypotheses!) *) 

1032 

1033 
fun beta_eta_thm th = 

1034 
let 

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

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

1037 
in 

1038 
th2 

1039 
end 

1040 

1041 
fun implies_elim_all th = 

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

1044 
fun norm_hyps th = 

1045 
th > beta_eta_thm 

1046 
> implies_elim_all 

1047 
> implies_intr_hyps 

1048 

1049 
fun mk_GEN v th sg = 

1050 
let 

1051 
val c = HOLogic.dest_Trueprop (concl_of th) 

1052 
val cv = cterm_of sg v 

1053 
val lc = Term.lambda v c 

1054 
val clc = Thm.cterm_of sg lc 

1055 
val cvty = ctyp_of_term cv 

1056 
val th1 = implies_elim_all th 

1057 
val th2 = beta_eta_thm (forall_intr cv th1) 

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

1061 
val (cold,cnew) = case c of 

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

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

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

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

1066 
val th4 = Thm.rename_boundvars cold cnew th3 

1067 
val res = implies_intr_hyps th4 

1068 
in 

1069 
res 

1070 
end 

1071 

19064  1072 
val permute_prems = Thm.permute_prems 
14516  1073 

1074 
fun rearrange sg tm th = 

1075 
let 

18929  1076 
val tm' = Envir.beta_eta_contract tm 
19066  1077 
fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th) 
18929  1078 
 find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) 
19066  1079 
then permute_prems n 1 th 
14516  1080 
else find ps (n+1) 
1081 
in 

1082 
find (prems_of th) 0 

1083 
end 

1084 

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

1086 
 zip [] [] = [] 

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

1088 

1089 
fun mk_INST dom rng th = 

1090 
th > forall_intr_list dom 

1091 
> forall_elim_list rng 

1092 

1093 
val collect_vars = 

1094 
let 

1095 
fun F vars (Bound _) = vars 

1096 
 F vars (tm as Free _) = 

1097 
if tm mem vars 

1098 
then vars 

1099 
else (tm::vars) 

1100 
 F vars (Const _) = vars 

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

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

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

1104 
in 

1105 
F [] 

1106 
end 

1107 

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

1109 

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

1111 

1112 
fun rens_of {vars,rens} = rens 

1113 

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

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

1116 

17322  1117 
fun disamb_term_from info tm = (info, tm) 
14516  1118 

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

1120 

17322  1121 
fun has_ren (HOLThm _) = false 
14516  1122 

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

1124 
app prin vars; 

1125 
writeln "Renaming:"; 

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

1127 

17322  1128 
fun disamb_thm_from info (HOLThm (_,thm)) = (info, thm) 
14516  1129 

17322  1130 
fun disamb_terms_from info tms = (info, tms) 
14516  1131 

17324  1132 
fun disamb_thms_from info hthms = (info, map hthm2thm hthms) 
14516  1133 

1134 
fun disamb_term tm = disamb_term_from disamb_info_empty tm 

1135 
fun disamb_terms tms = disamb_terms_from disamb_info_empty tms 

1136 
fun disamb_thm thm = disamb_thm_from disamb_info_empty thm 

1137 
fun disamb_thms thms = disamb_thms_from disamb_info_empty thms 

1138 

17322  1139 
fun norm_hthm sg (hth as HOLThm _) = hth 
14516  1140 

1141 
(* End of disambiguating code *) 

1142 

17657  1143 
fun disambiguate_frees thm = 
1144 
let 

1145 
fun ERR s = error ("Drule.disambiguate_frees: "^s) 

1146 
val ct = cprop_of thm 

1147 
val t = term_of ct 

1148 
val thy = theory_of_cterm ct 

1149 
val frees = term_frees t 

1150 
val freenames = add_term_free_names (t, []) 

1151 
fun is_old_name n = n mem_string freenames 

1152 
fun name_of (Free (n, _)) = n 

1153 
 name_of _ = ERR "name_of" 

1154 
fun new_name' bump map n = 

1155 
let val n' = n^bump in 

1156 
if is_old_name n' orelse Symtab.lookup map n' <> NONE then 

1157 
new_name' (Symbol.bump_string bump) map n 

1158 
else 

1159 
n' 

1160 
end 

1161 
val new_name = new_name' "a" 

1162 
fun replace_name n' (Free (n, t)) = Free (n', t) 

1163 
 replace_name n' _ = ERR "replace_name" 

19064  1164 
(* map: old or fresh name > old free, 
17657  1165 
invmap: old free which has fresh name assigned to it > fresh name *) 
1166 
fun dis (v, mapping as (map,invmap)) = 

1167 
let val n = name_of v in 

1168 
case Symtab.lookup map n of 

1169 
NONE => (Symtab.update (n, v) map, invmap) 

1170 
 SOME v' => 

1171 
if v=v' then 

1172 
mapping 

1173 
else 

1174 
let val n' = new_name map n in 

1175 
(Symtab.update (n', v) map, 

1176 
Termtab.update (v, n') invmap) 

1177 
end 

1178 
end 

1179 
in 

1180 
if (length freenames = length frees) then 

1181 
thm 

1182 
else 

1183 
let 

1184 
val (_, invmap) = 

1185 
List.foldl dis (Symtab.empty, Termtab.empty) frees 

1186 
fun make_subst ((oldfree, newname), (intros, elims)) = 

1187 
(cterm_of thy oldfree :: intros, 

1188 
cterm_of thy (replace_name newname oldfree) :: elims) 

1189 
val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap) 

1190 
in 

1191 
forall_elim_list elims (forall_intr_list intros thm) 

1192 
end 

1193 
end 

1194 

14516  1195 
val debug = ref false 
1196 

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

1198 
val message = if_debug writeln 

1199 

19064  1200 
val conjE_helper = permute_prems 0 1 conjE 
14516  1201 

1202 
fun get_hol4_thm thyname thmname thy = 

1203 
case get_hol4_theorem thyname thmname thy of 

15531  1204 
SOME hth => SOME (HOLThm hth) 
1205 
 NONE => 

14516  1206 
let 
1207 
val pending = HOL4Pending.get thy 

1208 
in 

17412  1209 
case StringPair.lookup pending (thyname,thmname) of 
15531  1210 
SOME hth => SOME (HOLThm hth) 
1211 
 NONE => NONE 

14516  1212 
end 
1213 

1214 
fun non_trivial_term_consts tm = 

15570  1215 
List.filter (fn c => not (c = "Trueprop" orelse 
14516  1216 
c = "All" orelse 
1217 
c = "op >" orelse 

1218 
c = "op &" orelse 

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

1220 

1221 
fun match_consts t (* th *) = 

1222 
let 

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

1224 
(case c of 

20854  1225 
"op =" => Library.insert (op =) "==" cs 
1226 
 "op >" => Library.insert (op =) "==>" cs 

14516  1227 
 "All" => cs 
1228 
 "all" => cs 

1229 
 "op &" => cs 

1230 
 "Trueprop" => cs 

20854  1231 
 _ => Library.insert (op =) c cs) 
14516  1232 
 add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) 
1233 
 add_consts (Abs (_, _, t), cs) = add_consts (t, cs) 

1234 
 add_consts (_, cs) = cs 

1235 
val t_consts = add_consts(t,[]) 

1236 
in 

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

1238 
end 

1239 

1240 
fun split_name str = 

1241 
let 

18489  1242 
val sub = Substring.full str 
14516  1243 
val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) 
19264  1244 
val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) 
14516  1245 
in 
1246 
if not (idx = "") andalso u = "_" 

15531  1247 
then SOME (newstr,valOf(Int.fromString idx)) 
1248 
else NONE 

14516  1249 
end 
15531  1250 
handle _ => NONE 
14516  1251 

1252 
fun rewrite_hol4_term t thy = 

1253 
let 

17894  1254 
val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) 
1255 
val hol4ss = Simplifier.theory_context thy empty_ss 

1256 
setmksimps single addsimps hol4rews1 

14516  1257 
in 
17894  1258 
Thm.transfer thy (Simplifier.full_rewrite hol4ss (cterm_of thy t)) 
14516  1259 
end 
1260 

1261 
fun get_isabelle_thm thyname thmname hol4conc thy = 

1262 
let 

1263 
val (info,hol4conc') = disamb_term hol4conc 

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

1265 
val isaconc = 

1266 
case concl_of i2h_conc of 

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

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

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

1270 
if_debug prin hol4conc'; 

1271 
message "Modified conclusion:"; 

1272 
if_debug prin isaconc) 

1273 

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

1275 
in 

1276 
case get_hol4_mapping thyname thmname thy of 

15531  1277 
SOME (SOME thmname) => 
14516  1278 
let 
18678  1279 
val th1 = (SOME (PureThy.get_thm thy (Name thmname)) 
1280 
handle ERROR _ => 

14516  1281 
(case split_name thmname of 
16486  1282 
SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy (Name listname),idx1)) 
15531  1283 
handle _ => NONE) 
1284 
 NONE => NONE)) 

14516  1285 
in 
1286 
case th1 of 

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

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

14516  1292 
end 
15531  1293 
 SOME NONE => error ("Trying to access ignored theorem " ^ thmname) 
1294 
 NONE => 

17607
7725da65f8e0
1) fixed bug in type_introduction: first stage uses different namespace than second stage
obua
parents:
17594
diff
changeset

1295 
let 
17626  1296 
val _ = (message "Looking for conclusion:"; 
14516  1297 
if_debug prin isaconc) 
1298 
val cs = non_trivial_term_consts isaconc 

17626  1299 
val _ = (message "Looking for consts:"; 
17630  1300 
message (commas cs)) 
14516  1301 
val pot_thms = Shuffler.find_potential thy isaconc 
17626  1302 
val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") 
14516  1303 
in 
1304 
case Shuffler.set_prop thy isaconc pot_thms of 

15531  1305 
SOME (isaname,th) => 
14516  1306 
let 
1307 
val hth as HOLThm args = mk_res th 

1308 
val thy' = thy > add_hol4_theorem thyname thmname args 

1309 
> add_hol4_mapping thyname thmname isaname 

19064  1310 
val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args) 
1311 
val _ = ImportRecorder.add_hol_mapping thyname thmname isaname 

14516  1312 
in 
15531  1313 
(thy',SOME hth) 
14516  1314 
end 
15531  1315 
 NONE => (thy,NONE) 
14516  1316 
end 
1317 
end 

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

17322  1320 
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy = 
1321 
let 

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

1323 
fun warn () = 

1324 
let 

1325 
val (info,hol4conc') = disamb_term hol4conc 

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

1327 
in 

1328 
case concl_of i2h_conc of 

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

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

1331 
writeln "Original conclusion:"; 

1332 
prin hol4conc'; 

1333 
writeln "Modified conclusion:"; 

1334 
prin lhs) 

1335 
 _ => () 

1336 
end 

1337 
in 

1338 
case b of 

17594  1339 
NONE => (warn () handle _ => (); (a,b)) 
1340 
 _ => (a, b) 

17322  1341 
end 
1342 

14516  1343 
fun get_thm thyname thmname thy = 
1344 
case get_hol4_thm thyname thmname thy of 

17594  1345 
SOME hth => (thy,SOME hth) 
17322  1346 
 NONE => ((case import_proof_concl thyname thmname thy of 
1347 
SOME f => get_isabelle_thm_and_warn thyname thmname (f thy) thy 

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

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

14516  1351 

1352 
fun rename_const thyname thy name = 

1353 
case get_hol4_const_renaming thyname name thy of 

15531  1354 
SOME cname => cname 
1355 
 NONE => name 

14516  1356 

1357 
fun get_def thyname constname rhs thy = 

1358 
let 

1359 
val constname = rename_const thyname thy constname 

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

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

1362 
in 

17322  1363 
get_isabelle_thm_and_warn thyname thmname (mk_teq (thyname ^ "." ^ constname) rhs thy') thy' 
14516  1364 
end 
1365 

1366 
fun get_axiom thyname axname thy = 

1367 
case get_thm thyname axname thy of 

15531  1368 
arg as (_,SOME _) => arg 
14516  1369 
 _ => raise ERR "get_axiom" ("Trying to retrieve axiom (" ^ axname ^ ")") 
1370 

1371 
fun intern_store_thm gen_output thyname thmname hth thy = 

1372 
let 

17894  1373 
val (hth' as HOLThm (args as (_,th))) = norm_hthm thy hth 
14516  1374 
val rew = rewrite_hol4_term (concl_of th) thy 
1375 
val th = equal_elim rew th 

1376 
val thy' = add_hol4_pending thyname thmname args thy 

19064  1377 
val _ = ImportRecorder.add_hol_pending thyname thmname (hthm2thm hth') 
17657  1378 
val th = disambiguate_frees th 
14516  1379 
val thy2 = if gen_output 
17644  1380 
then add_dump ("lemma " ^ (quotename thmname) ^ ": " ^ 
1381 
(smart_string_of_thm th) ^ "\n by (import " ^ 

1382 
thyname ^ " " ^ (quotename thmname) ^ ")") thy' 

14516  1383 
else thy' 
1384 
in 

1385 
(thy2,hth') 

1386 
end 

1387 

1388 
val store_thm = intern_store_thm true 

1389 

1390 
fun mk_REFL ctm = 

1391 
let 

1392 
val cty = Thm.ctyp_of_term ctm 

1393 
in 

15531  1394 
Drule.instantiate' [SOME cty] [SOME ctm] reflexivity_thm 
14516  1395 
end 
1396 

1397 
fun REFL tm thy = 

1398 
let 

1399 
val _ = message "REFL:" 

1400 
val (info,tm') = disamb_term tm 

17894  1401 
val ctm = Thm.cterm_of thy tm' 
14516  1402 
val res = HOLThm(rens_of info,mk_REFL ctm) 
1403 
val _ = if_debug pth res 

1404 
in 

1405 
(thy,res) 

1406 
end 

1407 

1408 
fun ASSUME tm thy = 

1409 
let 

1410 
val _ = message "ASSUME:" 

1411 
val (info,tm') = disamb_term tm 

17894  1412 
val ctm = Thm.cterm_of thy (HOLogic.mk_Trueprop tm') 
14516  1413 
val th = Thm.trivial ctm 
1414 
val res = HOLThm(rens_of info,th) 

1415 
val _ = if_debug pth res 

1416 
in 

1417 
(thy,res) 

1418 
end 

1419 

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

1421 
let 

1422 
val _ = message "INST_TYPE:" 

1423 
val _ = if_debug pth hth 