author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 29585  c23295521af5 
child 30346  90efbb8a8cb2 
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 
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

2 
Author: Sebastian Skalberg and Steven Obua, TU Muenchen 
14620
1be590fd2422
Minor cleanup of headers and some speedup of the HOL4 import.
skalberg
parents:
14518
diff
changeset

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

4 

14516  5 
signature ProofKernel = 
6 
sig 

7 
type hol_type 

8 
type tag 

9 
type term 

10 
type thm 

11 
type ('a,'b) subst 

24707  12 

14516  13 
type proof_info 
14 
datatype proof = Proof of proof_info * proof_content 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

15 
and proof_content 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

16 
= PRefl of term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

17 
 PInstT of proof * (hol_type,hol_type) subst 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

18 
 PSubst of proof list * term * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

19 
 PAbs of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

20 
 PDisch of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

21 
 PMp of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

22 
 PHyp of term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

23 
 PAxm of string * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

24 
 PDef of string * string * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

25 
 PTmSpec of string * string list * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

26 
 PTyDef of string * string * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

27 
 PTyIntro of string * string * string * string * term * term * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

28 
 POracle of tag * term list * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

29 
 PDisk 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

30 
 PSpec of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

31 
 PInst of proof * (term,term) subst 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

32 
 PGen of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

33 
 PGenAbs of proof * term option * term list 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

34 
 PImpAS of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

35 
 PSym of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

36 
 PTrans of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

37 
 PComb of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

38 
 PEqMp of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

39 
 PEqImp of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

40 
 PExists of proof * term * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

41 
 PChoose of term * proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

42 
 PConj of proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

43 
 PConjunct1 of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

44 
 PConjunct2 of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

45 
 PDisj1 of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

46 
 PDisj2 of proof * term 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

47 
 PDisjCases of proof * proof * proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

48 
 PNotI of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

49 
 PNotE of proof 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

50 
 PContr of proof * term 
14516  51 

52 
exception PK of string * string 

53 

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

54 
val get_proof_dir: string > theory > string option 
17657  55 
val disambiguate_frees : Thm.thm > Thm.thm 
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 

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

77 
val REFL : term > theory > theory * thm 

78 
val ASSUME : term > theory > theory * thm 

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

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

81 
val EQ_MP : thm > thm > theory > theory * thm 

82 
val EQ_IMP_RULE : thm > theory > theory * thm 

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

84 
val DISJ_CASES : thm > thm > thm > theory > theory * thm 

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

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

87 
val IMP_ANTISYM: thm > thm > theory > theory * thm 

88 
val SYM : thm > theory > theory * thm 

89 
val MP : thm > thm > theory > theory * thm 

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

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

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

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

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

95 
val TRANS : thm > thm > theory > theory * thm 

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

97 
val CONJ : thm > thm > theory > theory * thm 

98 
val CONJUNCT1: thm > theory > theory * thm 

99 
val CONJUNCT2: thm > theory > theory * thm 

100 
val NOT_INTRO: thm > theory > theory * thm 

101 
val NOT_ELIM : thm > theory > theory * thm 

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

103 
val COMB : thm > thm > theory > theory * thm 

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

105 

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

107 

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

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

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

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

112 

24707  113 
val prin : term > unit 
114 
val protect_factname : string > string 

19067  115 
val replay_protect_varname : string > string > unit 
19068  116 
val replay_add_dump : string > theory > theory 
14516  117 
end 
118 

119 
structure ProofKernel :> ProofKernel = 

120 
struct 

121 
type hol_type = Term.typ 

122 
type term = Term.term 

123 
datatype tag = Tag of string list 

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

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

126 

24707  127 
fun hthm2thm (HOLThm (_, th)) = th 
17324  128 

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

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

133 

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

24707  136 

14516  137 
datatype proof = Proof of proof_info * proof_content 
138 
and proof_content 

139 
= PRefl of term 

140 
 PInstT of proof * (hol_type,hol_type) subst 

141 
 PSubst of proof list * term * proof 

142 
 PAbs of proof * term 

143 
 PDisch of proof * term 

144 
 PMp of proof * proof 

145 
 PHyp of term 

146 
 PAxm of string * term 

147 
 PDef of string * string * term 

148 
 PTmSpec of string * string list * proof 

149 
 PTyDef of string * string * proof 

150 
 PTyIntro of string * string * string * string * term * term * proof 

151 
 POracle of tag * term list * term 

152 
 PDisk 

153 
 PSpec of proof * term 

154 
 PInst of proof * (term,term) subst 

155 
 PGen of proof * term 

156 
 PGenAbs of proof * term option * term list 

157 
 PImpAS of proof * proof 

158 
 PSym of proof 

159 
 PTrans of proof * proof 

160 
 PComb of proof * proof 

161 
 PEqMp of proof * proof 

162 
 PEqImp of proof 

163 
 PExists of proof * term * term 

164 
 PChoose of term * proof * proof 

165 
 PConj of proof * proof 

166 
 PConjunct1 of proof 

167 
 PConjunct2 of proof 

168 
 PDisj1 of proof * term 

169 
 PDisj2 of proof * term 

170 
 PDisjCases of proof * proof * proof 

171 
 PNotI of proof 

172 
 PNotE of proof 

173 
 PContr of proof * term 

174 

175 
exception PK of string * string 

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

177 

24707  178 
fun print_exn e = 
14516  179 
case e of 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

180 
PK (m,s) => (writeln ("PK (" ^ m ^ "): " ^ s); raise e) 
17959  181 
 _ => OldGoals.print_exn e 
14516  182 

183 
(* Compatibility. *) 

184 

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

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

14673  191 
fun quotename c = 
27353
71c4dd53d4cb
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents:
27187
diff
changeset

192 
if Syntax.is_identifier c andalso not (OuterKeyword.is_keyword c) then c else quote c 
14516  193 

17652  194 
fun simple_smart_string_of_cterm ct = 
195 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

196 
val thy = Thm.theory_of_cterm ct; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

197 
val {t,T,...} = rep_cterm ct 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

198 
(* Hack to avoid parse errors with Trueprop *) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

199 
val ct = (cterm_of thy (HOLogic.dest_Trueprop t) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

200 
handle TERM _ => ct) 
17652  201 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

202 
quote( 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

203 
PrintMode.setmp [] ( 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

204 
Library.setmp show_brackets false ( 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

205 
Library.setmp show_all_types true ( 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

206 
Library.setmp Syntax.ambiguity_is_error false ( 
26928  207 
Library.setmp show_sorts true Display.string_of_cterm)))) 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

208 
ct) 
17652  209 
end 
210 

19064  211 
exception SMART_STRING 
212 

14516  213 
fun smart_string_of_cterm ct = 
214 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

215 
val thy = Thm.theory_of_cterm ct 
24707  216 
val ctxt = ProofContext.init thy 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

217 
val {t,T,...} = rep_cterm ct 
14516  218 
(* Hack to avoid parse errors with Trueprop *) 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

219 
val ct = (cterm_of thy (HOLogic.dest_Trueprop t) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

220 
handle TERM _ => ct) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

221 
fun match u = t aconv u 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

222 
fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

223 
 G 1 = Library.setmp show_brackets true (G 0) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

224 
 G 2 = Library.setmp show_all_types true (G 0) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

225 
 G 3 = Library.setmp show_brackets true (G 2) 
24707  226 
 G _ = raise SMART_STRING 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

227 
fun F n = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

228 
let 
26928  229 
val str = Library.setmp show_brackets false (G n Display.string_of_cterm) ct 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

230 
val u = Syntax.parse_term ctxt str 
24707  231 
> TypeInfer.constrain T > Syntax.check_term ctxt 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

232 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

233 
if match u 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

234 
then quote str 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

235 
else F (n+1) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

236 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

237 
handle ERROR mesg => F (n+1) 
27187  238 
 SMART_STRING => error ("smart_string failed for: "^(G 0 Display.string_of_cterm ct)) 
14516  239 
in 
24634  240 
PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0 
14516  241 
end 
18678  242 
handle ERROR mesg => simple_smart_string_of_cterm ct 
24707  243 

14516  244 
val smart_string_of_thm = smart_string_of_cterm o cprop_of 
245 

26928  246 
fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm th) 
247 
fun prc ct = writeln (PrintMode.setmp [] Display.string_of_cterm ct) 

26939
1035c89b4c02
moved global pretty/string_of functions from Sign to Syntax;
wenzelm
parents:
26928
diff
changeset

248 
fun prin t = writeln (PrintMode.setmp [] (fn () => Syntax.string_of_term_global (the_context ()) t) ()); 
14516  249 
fun pth (HOLThm(ren,thm)) = 
250 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

251 
(*val _ = writeln "Renaming:" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

252 
val _ = app (fn(v,w) => (prin v; writeln " >"; prin w)) ren*) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

253 
val _ = prth thm 
14516  254 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

255 
() 
14516  256 
end 
257 

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

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

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

15531  263 
disk_info := SOME(thyname,thmname) 
14516  264 

265 
structure Lib = 

266 
struct 

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

268 

269 
fun assoc x = 

270 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

271 
fun F [] = raise PK("Lib.assoc","Not found") 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

272 
 F ((x',y)::rest) = if x = x' 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

273 
then y 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

274 
else F rest 
14516  275 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

276 
F 
14516  277 
end 
24707  278 
fun i mem L = 
279 
let fun itr [] = false 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

280 
 itr (a::rst) = i=a orelse itr rst 
14516  281 
in itr L end; 
24707  282 

14516  283 
fun mk_set [] = [] 
29289  284 
 mk_set (a::rst) = insert (op =) a (mk_set rst) 
24707  285 

14516  286 
fun [] union S = S 
287 
 S union [] = S 

29289  288 
 (a::rst) union S2 = rst union (insert (op =) a S2) 
24707  289 

14516  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 

24707  304 
(* Actual code. *) 
14516  305 

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

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

335 
fun F [] toks = (c,toks) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

336 
 F (c::cs) toks = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

337 
case LazySeq.getItem toks of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

338 
SOME(c',toks') => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

339 
if c = c' 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

340 
then F cs toks' 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

341 
else raise SyntaxError 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

342 
 NONE => raise SyntaxError 
14516  343 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

344 
F (String.explode str) 
14516  345 
end 
346 

347 
local 

348 
val scan_entity = 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

349 
(scan_string "amp;" #"&") 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

350 
 scan_string "quot;" #"\"" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

351 
 scan_string "gt;" #">" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

357 
SOME (c,toks') => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

358 
(case c of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

359 
#"\"" => raise SyntaxError 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

360 
 #"&" => scan_entity toks' 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

361 
 c => (c,toks')) 
15531  362 
 NONE => raise SyntaxError 
14516  363 
end 
364 

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

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

366 
String.implode 
14516  367 

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

369 

370 
val scan_start_of_tag = $$ #"<"  scan_id  

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

371 
repeat ($$ #" "  scan_attribute) 
14516  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 >> 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

381 
(fn (chldr,id') => if id = id' 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

382 
then chldr 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

383 
else raise XML "Tag mismatch") 
14516  384 
and scan_tag toks = 
385 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

386 
val ((id,atts),toks2) = scan_start_of_tag toks 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

387 
val (chldr,toks3) = (scan_children id  scan_end_of_tag) toks2 
14516  388 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

389 
(Elem (id,atts,chldr),toks3) 
14516  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

400 
val ty = type_of rhs 
14516  401 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

407 
val ty = type_of rhs 
14516  408 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

414 
SOME (_,cname,_) => cname 
15531  415 
 NONE => (case get_hol4_const_renaming thyname const thy of 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

416 
SOME cname => Sign.intern_const thy (thyname ^ "." ^ cname) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

24707  434 
local 
435 
fun get_const sg thyname name = 

17894  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

456 
fun no_quest s = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

457 
if Char.contains s #"?" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

458 
then String.translate (fn #"?" => "q_"  c => Char.toString c) s 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

459 
else s 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

460 
fun beg_prime s = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

461 
if String.isPrefix "'" s 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

462 
then s 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

463 
else "'" ^ s 
14516  464 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

465 
s > no_quest > beg_prime 
14516  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) 
24630
351a308ab58d
simplified type int (eliminated IntInf.int, integer);
wenzelm
parents:
22709
diff
changeset

469 
val invented_isavar = ref 0 
17444  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 = 
24707  476 
can (fn () => Syntax.read_term_global check_name_thy ("SOME "^s^". True")) (); 
18678  477 

478 
fun valid_varname s = 

24707  479 
can (fn () => Syntax.read_term_global check_name_thy s) (); 
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 

24707  485 
 NONE => 
17444  486 
let 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

487 
val _ = inc invented_isavar 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

488 
val t = "u_" ^ string_of_int (!invented_isavar) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

489 
val _ = ImportRecorder.protect_varname s t 
17444  490 
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) 
491 
in 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

492 
t 
17444  493 
end 
14516  494 

19067  495 
exception REPLAY_PROTECT_VARNAME of string*string*string 
496 

24707  497 
fun replay_protect_varname s t = 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

498 
case Symtab.lookup (!protected_varnames) s of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

499 
SOME t' => raise REPLAY_PROTECT_VARNAME (s, t, t') 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

500 
 NONE => 
19067  501 
let 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

502 
val _ = inc invented_isavar 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

503 
val t = "u_" ^ string_of_int (!invented_isavar) 
19067  504 
val _ = protected_varnames := Symtab.update (s, t) (!protected_varnames) 
505 
in 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

506 
() 
24707  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]); 
24707  514 

515 
fun replacestr x y s = 

17440
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 
24707  521 
 isprefix _ _ = false 
17440
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 [] = [] 
24707  525 
 r (S as (s::ss)) = if isp S then r (chg S) else s::(r ss) 
17440
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)) 
24707  528 
end 
17440
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 
24707  531 
fun unprotect_factname s = replacestr "_dot_" "." s 
17440
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 

24707  537 
fun protect_tyname tyn = 
17322  538 
let 
24707  539 
val tyn' = 
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 

24707  546 
fun protect_constname tcn = tcn 
17444  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

556 
SOME i => (case Array.sub(types,i) of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

557 
FullType ty => ty 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

558 
 XMLty xty => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

559 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

560 
val ty = get_type_from_xml thy thyname types xty 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

561 
val _ = Array.update(types,i,FullType ty) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

562 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

563 
ty 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

564 
end) 
14516  565 
 NONE => raise ERR "get_type_from_index" "Bad index" 
566 
and get_type_from_xml thy thyname types = 

567 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

568 
fun gtfx (Elem("tyi",[("i",iS)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

569 
get_type_from_index thy thyname types iS 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

570 
 gtfx (Elem("tyc",atts,[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

571 
mk_thy_type thy 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

572 
(get_segment thyname atts) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

573 
(protect_tyname (get_name atts)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

574 
[] 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

575 
 gtfx (Elem("tyv",[("n",s)],[])) = mk_vartype (protect_tyvarname s) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

576 
 gtfx (Elem("tya",[],(Elem("tyc",atts,[]))::tys)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

577 
mk_thy_type thy 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

578 
(get_segment thyname atts) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

579 
(protect_tyname (get_name atts)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

580 
(map gtfx tys) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

581 
 gtfx _ = raise ERR "get_type" "Bad type" 
14516  582 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

583 
gtfx 
14516  584 
end 
585 

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

587 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

588 
val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[]))) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

589 
fun IT _ [] = () 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

590 
 IT n (xty::xtys) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

591 
(Array.update(types,n,XMLty xty); 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

592 
IT (n+1) xtys) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

593 
val _ = IT 0 xtys 
14516  594 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

595 
types 
14516  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

605 
SOME i => (case Array.sub(terms,i) of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

606 
FullTerm tm => tm 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

607 
 XMLtm xtm => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

608 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

609 
val tm = get_term_from_xml thy thyname types terms xtm 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

610 
val _ = Array.update(terms,i,FullTerm tm) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

611 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

612 
tm 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

613 
end) 
14516  614 
 NONE => raise ERR "get_term_from_index" "Bad index" 
615 
and get_term_from_xml thy thyname types terms = 

616 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

617 
fun get_type [] = NONE 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

618 
 get_type [ty] = SOME (TypeNet.get_type_from_xml thy thyname types ty) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

621 
fun gtfx (Elem("tmv",[("n",name),("t",tyi)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

622 
mk_var(protect_varname name,TypeNet.get_type_from_index thy thyname types tyi) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

623 
 gtfx (Elem("tmc",atts,[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

624 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

625 
val segment = get_segment thyname atts 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

626 
val name = protect_constname(get_name atts) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

627 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

628 
mk_thy_const thy segment name (TypeNet.get_type_from_index thy thyname types (Lib.assoc "t" atts)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

629 
handle PK _ => prim_mk_const thy segment name 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

630 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

631 
 gtfx (Elem("tma",[("f",tmf),("a",tma)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

632 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

633 
val f = get_term_from_index thy thyname types terms tmf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

634 
val a = get_term_from_index thy thyname types terms tma 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

635 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

636 
mk_comb(f,a) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

637 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

638 
 gtfx (Elem("tml",[("x",tmx),("a",tma)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

639 
let 
24707  640 
val x = get_term_from_index thy thyname types terms tmx 
17490  641 
val a = get_term_from_index thy thyname types terms tma 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

642 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

643 
mk_lambda x a 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

644 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

645 
 gtfx (Elem("tmi",[("i",iS)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

646 
get_term_from_index thy thyname types terms iS 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

647 
 gtfx (Elem(tag,_,_)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

648 
raise ERR "get_term" ("Not a term: "^tag) 
14516  649 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

650 
gtfx 
14516  651 
end 
652 

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

654 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

657 
fun IT _ [] = () 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

658 
 IT n (xtm::xtms) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

659 
(Array.update(terms,n,XMLtm xtm); 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

660 
IT (n+1) xtms) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

661 
val _ = IT 0 xtms 
14516  662 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

663 
terms 
14516  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

670 
val import_segment = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

671 
case get_segment2 thyname thy of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

672 
SOME seg => seg 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

673 
 NONE => get_import_segment thy 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

674 
val path = space_explode ":" (getenv "HOL4_PROOFS") 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

675 
fun find [] = NONE 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

676 
 find (p::ps) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

677 
(let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

678 
val dir = OS.Path.joinDirFile {dir = p,file=import_segment} 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

679 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

680 
if OS.FileSys.isDir dir 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

681 
then SOME dir 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

682 
else find ps 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

683 
end) handle OS.SysErr _ => find ps 
14516  684 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

685 
Option.map (fn p => OS.Path.joinDirFile {dir = p, file = thyname}) (find path) 
14516  686 
end 
24707  687 

14516  688 
fun proof_file_name thyname thmname thy = 
689 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

690 
val path = case get_proof_dir thyname thy of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

691 
SOME p => p 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

692 
 NONE => error "Cannot find proof files" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

693 
val _ = OS.FileSys.mkDir path handle OS.SysErr _ => () 
14516  694 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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

14516  698 
fun xml_to_proof thyname types terms prf thy = 
699 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

700 
val xml_to_hol_type = TypeNet.get_type_from_xml thy thyname types 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

701 
val xml_to_term = TermNet.get_term_from_xml thy thyname types terms 
14516  702 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

703 
fun index_to_term is = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

704 
TermNet.get_term_from_index thy thyname types terms is 
14516  705 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

706 
fun x2p (Elem("prefl",[("i",is)],[])) = mk_proof (PRefl (index_to_term is)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

707 
 x2p (Elem("pinstt",[],p::lambda)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

708 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

709 
val p = x2p p 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

710 
val lambda = implode_subst (map xml_to_hol_type lambda) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

711 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

712 
mk_proof (PInstT(p,lambda)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

713 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

714 
 x2p (Elem("psubst",[("i",is)],prf::prfs)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

715 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

716 
val tm = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

717 
val prf = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

718 
val prfs = map x2p prfs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

719 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

720 
mk_proof (PSubst(prfs,tm,prf)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

721 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

722 
 x2p (Elem("pabs",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

723 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

724 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

725 
val t = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

726 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

727 
mk_proof (PAbs (p,t)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

728 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

729 
 x2p (Elem("pdisch",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

730 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

731 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

732 
val t = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

733 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

734 
mk_proof (PDisch (p,t)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

735 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

736 
 x2p (Elem("pmp",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

737 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

738 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

739 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

740 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

741 
mk_proof (PMp(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

742 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

743 
 x2p (Elem("phyp",[("i",is)],[])) = mk_proof (PHyp (index_to_term is)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

744 
 x2p (Elem("paxiom",[("n",n),("i",is)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

745 
mk_proof (PAxm(n,index_to_term is)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

746 
 x2p (Elem("pfact",atts,[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

747 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

748 
val thyname = get_segment thyname atts 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

749 
val thmname = protect_factname (get_name atts) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

750 
val p = mk_proof PDisk 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

751 
val _ = set_disk_info_of p thyname thmname 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

752 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

753 
p 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

754 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

755 
 x2p (Elem("pdef",[("s",seg),("n",name),("i",is)],[])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

756 
mk_proof (PDef(seg,protect_constname name,index_to_term is)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

757 
 x2p (Elem("ptmspec",[("s",seg)],p::names)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

758 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

759 
val names = map (fn Elem("name",[("n",name)],[]) => name 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

760 
 _ => raise ERR "x2p" "Bad proof (ptmspec)") names 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

761 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

762 
mk_proof (PTmSpec(seg,names,x2p p)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

763 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

764 
 x2p (Elem("ptyintro",[("s",seg),("n",name),("a",abs_name),("r",rep_name)],[xP,xt,p])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

765 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

766 
val P = xml_to_term xP 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

767 
val t = xml_to_term xt 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

768 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

769 
mk_proof (PTyIntro(seg,protect_tyname name,protect_constname abs_name,protect_constname rep_name,P,t,x2p p)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

770 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

771 
 x2p (Elem("ptydef",[("s",seg),("n",name)],[p])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

772 
mk_proof (PTyDef(seg,protect_tyname name,x2p p)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

773 
 x2p (xml as Elem("poracle",[],chldr)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

774 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

775 
val (oracles,terms) = List.partition (fn (Elem("oracle",_,_)) => true  _ => false) chldr 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

776 
val ors = map (fn (Elem("oracle",[("n",name)],[])) => name  xml => raise ERR "x2p" "bad oracle") oracles 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

777 
val (c,asl) = case terms of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

778 
[] => raise ERR "x2p" "Bad oracle description" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

779 
 (hd::tl) => (hd,tl) 
30190  780 
val tg = List.foldr (fn (oracle,tg) => Tag.merge (Tag.read oracle) tg) Tag.empty_tag ors 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

781 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

782 
mk_proof (POracle(tg,map xml_to_term asl,xml_to_term c)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

783 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

784 
 x2p (Elem("pspec",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

785 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

786 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

787 
val tm = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

788 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

789 
mk_proof (PSpec(p,tm)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

790 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

791 
 x2p (Elem("pinst",[],p::theta)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

792 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

793 
val p = x2p p 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

794 
val theta = implode_subst (map xml_to_term theta) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

795 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

796 
mk_proof (PInst(p,theta)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

797 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

798 
 x2p (Elem("pgen",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

799 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

800 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

801 
val tm = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

802 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

803 
mk_proof (PGen(p,tm)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

804 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

805 
 x2p (Elem("pgenabs",[],prf::tms)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

806 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

807 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

808 
val tml = map xml_to_term tms 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

809 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

810 
mk_proof (PGenAbs(p,NONE,tml)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

811 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

812 
 x2p (Elem("pgenabs",[("i",is)],prf::tms)) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

813 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

814 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

815 
val tml = map xml_to_term tms 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

816 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

817 
mk_proof (PGenAbs(p,SOME (index_to_term is),tml)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

818 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

819 
 x2p (Elem("pimpas",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

820 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

821 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

822 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

823 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

824 
mk_proof (PImpAS(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

825 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

826 
 x2p (Elem("psym",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

827 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

828 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

829 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

830 
mk_proof (PSym p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

831 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

832 
 x2p (Elem("ptrans",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

833 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

834 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

835 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

836 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

837 
mk_proof (PTrans(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

838 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

839 
 x2p (Elem("pcomb",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

840 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

841 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

842 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

843 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

844 
mk_proof (PComb(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

845 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

846 
 x2p (Elem("peqmp",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

847 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

848 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

849 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

850 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

851 
mk_proof (PEqMp(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

852 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

853 
 x2p (Elem("peqimp",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

854 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

855 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

856 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

857 
mk_proof (PEqImp p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

858 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

859 
 x2p (Elem("pexists",[("e",ise),("w",isw)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

860 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

861 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

862 
val ex = index_to_term ise 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

863 
val w = index_to_term isw 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

864 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

865 
mk_proof (PExists(p,ex,w)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

866 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

867 
 x2p (Elem("pchoose",[("i",is)],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

868 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

869 
val v = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

870 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

871 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

872 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

873 
mk_proof (PChoose(v,p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

874 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

875 
 x2p (Elem("pconj",[],[prf1,prf2])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

876 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

877 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

878 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

879 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

880 
mk_proof (PConj(p1,p2)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

881 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

882 
 x2p (Elem("pconjunct1",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

883 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

884 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

885 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

886 
mk_proof (PConjunct1 p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

887 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

888 
 x2p (Elem("pconjunct2",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

889 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

890 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

891 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

892 
mk_proof (PConjunct2 p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

893 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

894 
 x2p (Elem("pdisj1",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

895 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

896 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

897 
val t = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

898 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

899 
mk_proof (PDisj1 (p,t)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

900 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

901 
 x2p (Elem("pdisj2",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

902 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

903 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

904 
val t = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

905 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

906 
mk_proof (PDisj2 (p,t)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

907 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

908 
 x2p (Elem("pdisjcases",[],[prf1,prf2,prf3])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

909 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

910 
val p1 = x2p prf1 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

911 
val p2 = x2p prf2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

912 
val p3 = x2p prf3 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

913 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

914 
mk_proof (PDisjCases(p1,p2,p3)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

915 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

916 
 x2p (Elem("pnoti",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

917 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

918 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

919 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

920 
mk_proof (PNotI p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

921 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

922 
 x2p (Elem("pnote",[],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

923 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

924 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

925 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

926 
mk_proof (PNotE p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

927 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

928 
 x2p (Elem("pcontr",[("i",is)],[prf])) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

929 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

930 
val p = x2p prf 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

931 
val t = index_to_term is 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

932 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

933 
mk_proof (PContr (p,t)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

934 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

935 
 x2p xml = raise ERR "x2p" "Bad proof" 
14516  936 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

937 
x2p prf 
14516  938 
end 
939 

24707  940 
fun import_proof_concl thyname thmname thy = 
17322  941 
let 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

942 
val is = TextIO.openIn(proof_file_name thyname thmname thy) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

943 
val (proof_xml,_) = scan_tag (LazySeq.of_instream is) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

944 
val _ = TextIO.closeIn is 
24707  945 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

946 
case proof_xml of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

947 
Elem("proof",[],xtypes::xterms::prf::rest) => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

948 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

949 
val types = TypeNet.input_types thyname xtypes 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

950 
val terms = TermNet.input_terms thyname types xterms 
24707  951 
fun f xtm thy = TermNet.get_term_from_xml thy thyname types terms xtm 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

952 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

953 
case rest of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

954 
[] => NONE 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

955 
 [xtm] => SOME (f xtm) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

956 
 _ => raise ERR "import_proof" "Bad argument list" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

957 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

958 
 _ => raise ERR "import_proof" "Bad proof" 
17322  959 
end 
960 

14516  961 
fun import_proof thyname thmname thy = 
962 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

963 
val is = TextIO.openIn(proof_file_name thyname thmname thy) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

964 
val (proof_xml,_) = scan_tag (LazySeq.of_instream is) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

965 
val _ = TextIO.closeIn is 
24707  966 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

967 
case proof_xml of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

968 
Elem("proof",[],xtypes::xterms::prf::rest) => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

969 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

970 
val types = TypeNet.input_types thyname xtypes 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

971 
val terms = TermNet.input_terms thyname types xterms 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

972 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

973 
(case rest of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

974 
[] => NONE 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

975 
 [xtm] => SOME (fn thy => TermNet.get_term_from_xml thy thyname types terms xtm) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

976 
 _ => raise ERR "import_proof" "Bad argument list", 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

977 
xml_to_proof thyname types terms prf) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

978 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

979 
 _ => raise ERR "import_proof" "Bad proof" 
14516  980 
end 
981 

982 
fun uniq_compose m th i st = 

983 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

984 
val res = bicompose false (false,th,m) i st 
14516  985 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

986 
case Seq.pull res of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

987 
SOME (th,rest) => (case Seq.pull rest of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

988 
SOME _ => raise ERR "uniq_compose" "Not unique!" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

989 
 NONE => th) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1035 
val th1 = Thm.equal_elim (Thm.beta_conversion true (cprop_of th)) th 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1036 
val th2 = Thm.equal_elim (Thm.eta_conversion (cprop_of th1)) th1 
14516  1037 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1038 
th2 
14516  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1051 
val c = HOLogic.dest_Trueprop (concl_of th) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1052 
val cv = cterm_of sg v 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1053 
val lc = Term.lambda v c 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1054 
val clc = Thm.cterm_of sg lc 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1055 
val cvty = ctyp_of_term cv 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1056 
val th1 = implies_elim_all th 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1057 
val th2 = beta_eta_thm (forall_intr cv th1) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1058 
val th3 = th2 COMP (beta_eta_thm (Drule.instantiate' [SOME cvty] [SOME clc] gen_thm)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1059 
val c = prop_of th3 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1060 
val vname = fst(dest_Free v) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1061 
val (cold,cnew) = case c of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1062 
tpc $ (Const("All",allT) $ Abs(oldname,ty,body)) => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1063 
(Abs(oldname,dummyT,Bound 0),Abs(vname,dummyT,Bound 0)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1064 
 tpc $ (Const("All",allT) $ rest) => (tpc,tpc) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1065 
 _ => raise ERR "mk_GEN" "Unknown conclusion" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1066 
val th4 = Thm.rename_boundvars cold cnew th3 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1067 
val res = implies_intr_hyps th4 
14516  1068 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1069 
res 
14516  1070 
end 
1071 

24707  1072 
val permute_prems = Thm.permute_prems 
14516  1073 

1074 
fun rearrange sg tm th = 

1075 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1076 
val tm' = Envir.beta_eta_contract tm 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1077 
fun find [] n = permute_prems 0 1 (implies_intr (Thm.cterm_of sg tm) th) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1078 
 find (p::ps) n = if tm' aconv (Envir.beta_eta_contract p) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1079 
then permute_prems n 1 th 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1080 
else find ps (n+1) 
14516  1081 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1082 
find (prems_of th) 0 
14516  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1095 
fun F vars (Bound _) = vars 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1096 
 F vars (tm as Free _) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1097 
if tm mem vars 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1098 
then vars 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1099 
else (tm::vars) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1100 
 F vars (Const _) = vars 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1101 
 F vars (tm1 $ tm2) = F (F vars tm1) tm2 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1102 
 F vars (Abs(_,_,body)) = F vars body 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1103 
 F vars (Var _) = raise ERR "collect_vars" "Schematic variable found" 
14516  1104 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1105 
F [] 
14516  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:"; 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1124 
app prin vars; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1125 
writeln "Renaming:"; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1126 
app (fn(x,y)=>(prin x; writeln " >"; prin y)) rens) 
14516  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 

29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset

1149 
val frees = OldTerm.term_frees t 
29281  1150 
val freenames = Term.add_free_names t [] 
1151 
val is_old_name = member (op =) freenames 

17657  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 

24707  1156 
if is_old_name n' orelse Symtab.lookup map n' <> NONE then 
17657  1157 
new_name' (Symbol.bump_string bump) map n 
1158 
else 

1159 
n' 

24707  1160 
end 
17657  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" 

24707  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) 

24707  1170 
 SOME v' => 
1171 
if v=v' then 

1172 
mapping 

17657  1173 
else 
1174 
let val n' = new_name map n in 

24707  1175 
(Symtab.update (n', v) map, 
17657  1176 
Termtab.update (v, n') invmap) 
1177 
end 

1178 
end 

1179 
in 

1180 
if (length freenames = length frees) then 

1181 
thm 

1182 
else 

24707  1183 
let 
1184 
val (_, invmap) = 

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

17657  1186 
fun make_subst ((oldfree, newname), (intros, elims)) = 
24707  1187 
(cterm_of thy oldfree :: intros, 
17657  1188 
cterm_of thy (replace_name newname oldfree) :: elims) 
1189 
val (intros, elims) = List.foldl make_subst ([], []) (Termtab.dest invmap) 

24707  1190 
in 
17657  1191 
forall_elim_list elims (forall_intr_list intros thm) 
24707  1192 
end 
17657  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 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1204 
SOME hth => SOME (HOLThm hth) 
24707  1205 
 NONE => 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1206 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1207 
val pending = HOL4Pending.get thy 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1208 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1209 
case StringPair.lookup pending (thyname,thmname) of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1210 
SOME hth => SOME (HOLThm hth) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1211 
 NONE => NONE 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1212 
end 
14516  1213 

29289  1214 
fun non_trivial_term_consts t = fold_aterms 
1215 
(fn Const (c, _) => 

1216 
if c = "Trueprop" orelse c = "All" orelse c = "op >" orelse c = "op &" orelse c = "op =" 

1217 
then I else insert (op =) c 

1218 
 _ => I) t []; 

14516  1219 

1220 
fun match_consts t (* th *) = 

1221 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1222 
fun add_consts (Const (c, _), cs) = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1223 
(case c of 
29289  1224 
"op =" => insert (op =) "==" cs 
1225 
 "op >" => insert (op =) "==>" cs 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1226 
 "All" => cs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1227 
 "all" => cs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1228 
 "op &" => cs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1229 
 "Trueprop" => cs 
29289  1230 
 _ => insert (op =) c cs) 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1231 
 add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1232 
 add_consts (Abs (_, _, t), cs) = add_consts (t, cs) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1233 
 add_consts (_, cs) = cs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1234 
val t_consts = add_consts(t,[]) 
14516  1235 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1236 
fn th => eq_set(t_consts,add_consts(prop_of th,[])) 
14516  1237 
end 
1238 

1239 
fun split_name str = 

1240 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1241 
val sub = Substring.full str 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1242 
val (f,idx) = apsnd Substring.string (Substring.splitr Char.isDigit sub) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1243 
val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f) 
14516  1244 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1245 
if not (idx = "") andalso u = "_" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1246 
then SOME (newstr,valOf(Int.fromString idx)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1247 
else NONE 
14516  1248 
end 
28397
389c5e494605
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents:
27691
diff
changeset

1249 
handle _ => NONE (* FIXME avoid handle _ *) 
14516  1250 

1251 
fun rewrite_hol4_term t thy = 

1252 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1253 
val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1254 
val hol4ss = Simplifier.theory_context thy empty_ss 
17894  1255 
setmksimps single addsimps hol4rews1 
14516  1256 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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

1260 
fun get_isabelle_thm thyname thmname hol4conc thy = 

1261 
let 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1262 
val (info,hol4conc') = disamb_term hol4conc 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1263 
val i2h_conc = symmetric (rewrite_hol4_term (HOLogic.mk_Trueprop hol4conc') thy) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1264 
val isaconc = 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1265 
case concl_of i2h_conc of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1266 
Const("==",_) $ lhs $ _ => lhs 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1267 
 _ => error "get_isabelle_thm" "Bad rewrite rule" 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1268 
val _ = (message "Original conclusion:"; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1269 
if_debug prin hol4conc'; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1270 
message "Modified conclusion:"; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1271 
if_debug prin isaconc) 
14516  1272 

26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1273 
fun mk_res th = HOLThm(rens_of info,equal_elim i2h_conc th) 
14516  1274 
in 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1275 
case get_hol4_mapping thyname thmname thy of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1276 
SOME (SOME thmname) => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1277 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1278 
val th1 = (SOME (PureThy.get_thm thy thmname) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1279 
handle ERROR _ => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1280 
(case split_name thmname of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1281 
SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx1)) 
28397
389c5e494605
handle _ should be avoided (spurious Interrupt will spoil the game);
wenzelm
parents:
27691
diff
changeset

1282 
handle _ => NONE) (* FIXME avoid handle _ *) 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1283 
 NONE => NONE)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1284 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1285 
case th1 of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1286 
SOME th2 => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1287 
(case Shuffler.set_prop thy isaconc [(thmname,th2)] of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1288 
SOME (_,th) => (message "YES";(thy, SOME (mk_res th))) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1289 
 NONE => (message "NO2";error "get_isabelle_thm" "Bad mapping")) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1290 
 NONE => (message "NO1";error "get_isabelle_thm" "Bad mapping") 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1291 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1292 
 SOME NONE => error ("Trying to access ignored theorem " ^ thmname) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1293 
 NONE => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1294 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1295 
val _ = (message "Looking for conclusion:"; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1296 
if_debug prin isaconc) 
29289  1297 
val cs = non_trivial_term_consts isaconc; 
26626
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1298 
val _ = (message "Looking for consts:"; 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1299 
message (commas cs)) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1300 
val pot_thms = Shuffler.find_potential thy isaconc 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1301 
val _ = message ((Int.toString (length pot_thms)) ^ " potential theorems") 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1302 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1303 
case Shuffler.set_prop thy isaconc pot_thms of 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1304 
SOME (isaname,th) => 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1305 
let 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1306 
val hth as HOLThm args = mk_res th 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1307 
val thy' = thy > add_hol4_theorem thyname thmname args 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1308 
> add_hol4_mapping thyname thmname isaname 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1309 
val _ = ImportRecorder.add_hol_theorem thyname thmname (snd args) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1310 
val _ = ImportRecorder.add_hol_mapping thyname thmname isaname 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1311 
in 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1312 
(thy',SOME hth) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1313 
end 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

1314 
 NONE => (thy,NONE) 
c6231d64d264
rep_cterm/rep_thm: no longer dereference theory_ref;
wenzelm
parents:
26343
diff
changeset

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

17322  1319 
fun get_isabelle_thm_and_warn thyname thmname hol4conc thy = 
1320 
let 

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

1322 
fun warn () = 

