author  wenzelm 
Fri, 01 Sep 1995 13:11:09 +0200  
changeset 1238  289c573327f0 
parent 1229  f191f25a5ec8 
child 1258  2a2d8c74a756 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
0  2 
ID: $Id$ 
250  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 
Copyright 1994 University of Cambridge 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

5 

1160  6 
The core of Isabelle's Meta Logic: certified types and terms, meta 
7 
theorems, theories, meta rules (including resolution and 

8 
simplification). 

0  9 
*) 
10 

250  11 
signature THM = 
12 
sig 

1238  13 
structure Envir : ENVIR 
14 
structure Sequence : SEQUENCE 

15 
structure Sign : SIGN 

1160  16 

17 
(*certified types*) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

18 
type ctyp 
1238  19 
val rep_ctyp : ctyp > {sign: Sign.sg, T: typ} 
20 
val typ_of : ctyp > typ 

21 
val ctyp_of : Sign.sg > typ > ctyp 

22 
val read_ctyp : Sign.sg > string > ctyp 

1160  23 

24 
(*certified terms*) 

25 
type cterm 

1238  26 
val rep_cterm : cterm > {sign: Sign.sg, t: term, T: typ, maxidx: int} 
27 
val term_of : cterm > term 

28 
val cterm_of : Sign.sg > term > cterm 

29 
val read_cterm : Sign.sg > string * typ > cterm 

30 
val cterm_fun : (term > term) > (cterm > cterm) 

31 
val dest_cimplies : cterm > cterm * cterm 

32 
val read_def_cterm : 

1160  33 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
34 
string list > bool > string * typ > cterm * (indexname * typ) list 

35 

36 
(*meta theorems*) 

37 
type thm 

38 
exception THM of string * int * thm list 

1238  39 
val rep_thm : thm > {sign: Sign.sg, maxidx: int, 
1220  40 
shyps: sort list, hyps: term list, prop: term} 
1238  41 
val stamps_of_thm : thm > string ref list 
42 
val tpairs_of : thm > (term * term) list 

43 
val prems_of : thm > term list 

44 
val nprems_of : thm > int 

45 
val concl_of : thm > term 

46 
val cprop_of : thm > cterm 

47 
val extra_shyps : thm > sort list 

48 
val force_strip_shyps : bool ref (* FIXME tmp *) 

49 
val strip_shyps : thm > thm 

50 
val implies_intr_shyps: thm > thm 

51 
val cert_axm : Sign.sg > string * term > string * term 

52 
val read_axm : Sign.sg > string * string > string * term 

53 
val inferT_axm : Sign.sg > string * term > string * term 

1160  54 

55 
(*theories*) 

56 
type theory 

57 
exception THEORY of string * theory list 

1238  58 
val rep_theory : theory > 
1160  59 
{sign: Sign.sg, new_axioms: term Sign.Symtab.table, parents: theory list} 
1238  60 
val sign_of : theory > Sign.sg 
61 
val syn_of : theory > Sign.Syntax.syntax 

62 
val stamps_of_thy : theory > string ref list 

63 
val parents_of : theory > theory list 

64 
val subthy : theory * theory > bool 

65 
val eq_thy : theory * theory > bool 

66 
val get_axiom : theory > string > thm 

67 
val axioms_of : theory > (string * thm) list 

68 
val proto_pure_thy : theory 

69 
val pure_thy : theory 

70 
val cpure_thy : theory 

564  71 
local open Sign.Syntax in 
1238  72 
val add_classes : (class * class list) list > theory > theory 
73 
val add_classrel : (class * class) list > theory > theory 

74 
val add_defsort : sort > theory > theory 

75 
val add_types : (string * int * mixfix) list > theory > theory 

76 
val add_tyabbrs : (string * string list * string * mixfix) list 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

77 
> theory > theory 
1238  78 
val add_tyabbrs_i : (string * string list * typ * mixfix) list 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

79 
> theory > theory 
1238  80 
val add_arities : (string * sort list * sort) list > theory > theory 
81 
val add_consts : (string * string * mixfix) list > theory > theory 

82 
val add_consts_i : (string * typ * mixfix) list > theory > theory 

83 
val add_syntax : (string * string * mixfix) list > theory > theory 

84 
val add_syntax_i : (string * typ * mixfix) list > theory > theory 

85 
val add_trfuns : 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

86 
(string * (ast list > ast)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

87 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

88 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

89 
(string * (ast list > ast)) list > theory > theory 
1238  90 
val add_trrules : (string * string) trrule list > theory > theory 
91 
val add_trrules_i : ast trrule list > theory > theory 

92 
val add_axioms : (string * string) list > theory > theory 

93 
val add_axioms_i : (string * term) list > theory > theory 

94 
val add_thyname : string > theory > theory 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

95 
end 
1238  96 
val merge_theories : theory * theory > theory 
97 
val merge_thy_list : bool > theory list > theory 

1160  98 

99 
(*meta rules*) 

1238  100 
val assume : cterm > thm 
101 
val implies_intr : cterm > thm > thm 

102 
val implies_elim : thm > thm > thm 

103 
val forall_intr : cterm > thm > thm 

104 
val forall_elim : cterm > thm > thm 

105 
val flexpair_def : thm 

106 
val reflexive : cterm > thm 

107 
val symmetric : thm > thm 

108 
val transitive : thm > thm > thm 

109 
val beta_conversion : cterm > thm 

110 
val extensional : thm > thm 

111 
val abstract_rule : string > cterm > thm > thm 

112 
val combination : thm > thm > thm 

113 
val equal_intr : thm > thm > thm 

114 
val equal_elim : thm > thm > thm 

115 
val implies_intr_hyps : thm > thm 

116 
val flexflex_rule : thm > thm Sequence.seq 

117 
val instantiate : 

1160  118 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
1238  119 
val trivial : cterm > thm 
120 
val class_triv : theory > class > thm 

121 
val varifyT : thm > thm 

122 
val freezeT : thm > thm 

123 
val dest_state : thm * int > 

1160  124 
(term * term) list * term list * term * term 
1238  125 
val lift_rule : (thm * int) > thm > thm 
126 
val assumption : int > thm > thm Sequence.seq 

127 
val eq_assumption : int > thm > thm 

1160  128 
val rename_params_rule: string list * int > thm > thm 
1238  129 
val bicompose : bool > bool * thm * int > 
1160  130 
int > thm > thm Sequence.seq 
1238  131 
val biresolution : bool > (bool * thm) list > 
1160  132 
int > thm > thm Sequence.seq 
133 

134 
(*meta simplification*) 

135 
type meta_simpset 

136 
exception SIMPLIFIER of string * thm 

1238  137 
val empty_mss : meta_simpset 
138 
val add_simps : meta_simpset * thm list > meta_simpset 

139 
val del_simps : meta_simpset * thm list > meta_simpset 

140 
val mss_of : thm list > meta_simpset 

141 
val add_congs : meta_simpset * thm list > meta_simpset 

142 
val add_prems : meta_simpset * thm list > meta_simpset 

143 
val prems_of_mss : meta_simpset > thm list 

144 
val set_mk_rews : meta_simpset * (thm > thm list) > meta_simpset 

145 
val mk_rews_of_mss : meta_simpset > thm > thm list 

146 
val trace_simp : bool ref 

147 
val rewrite_cterm : bool * bool > meta_simpset > 

1160  148 
(meta_simpset > thm > thm option) > cterm > thm 
250  149 
end; 
0  150 

250  151 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

152 
and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM = 
0  153 
struct 
250  154 

0  155 
structure Sequence = Unify.Sequence; 
156 
structure Envir = Unify.Envir; 

157 
structure Sign = Unify.Sign; 

158 
structure Type = Sign.Type; 

159 
structure Syntax = Sign.Syntax; 

160 
structure Symtab = Sign.Symtab; 

161 

162 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

163 
(*** Certified terms and types ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

164 

250  165 
(** certified types **) 
166 

167 
(*certified typs under a signature*) 

168 

169 
datatype ctyp = Ctyp of {sign: Sign.sg, T: typ}; 

170 

171 
fun rep_ctyp (Ctyp args) = args; 

172 
fun typ_of (Ctyp {T, ...}) = T; 

173 

174 
fun ctyp_of sign T = 

175 
Ctyp {sign = sign, T = Sign.certify_typ sign T}; 

176 

177 
fun read_ctyp sign s = 

178 
Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s}; 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

179 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

180 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

181 

250  182 
(** certified terms **) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

183 

250  184 
(*certified terms under a signature, with checked typ and maxidx of Vars*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

185 

250  186 
datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

187 

4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

188 
fun rep_cterm (Cterm args) = args; 
250  189 
fun term_of (Cterm {t, ...}) = t; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

190 

250  191 
(*create a cterm by checking a "raw" term with respect to a signature*) 
192 
fun cterm_of sign tm = 

193 
let val (t, T, maxidx) = Sign.certify_term sign tm 

194 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 

195 
end handle TYPE (msg, _, _) 

196 
=> raise TERM ("Term not in signature\n" ^ msg, [tm]); 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

197 

250  198 
fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); 
199 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

200 

250  201 
(*dest_implies for cterms. Note T=prop below*) 
202 
fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

203 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  204 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
205 
 dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]); 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

206 

250  207 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

208 

574  209 
(** read cterms **) (*exception ERROR*) 
250  210 

211 
(*read term, infer types, certify term*) 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

212 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  213 
let 
574  214 
val T' = Sign.certify_typ sign T 
215 
handle TYPE (msg, _, _) => error msg; 

623  216 
val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

217 
val (_, t', tye) = 
959  218 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  219 
val ct = cterm_of sign t' 
220 
handle TERM (msg, _) => error msg; 

250  221 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

222 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

223 
fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

224 

250  225 

226 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

227 
(*** Meta theorems ***) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

228 

1238  229 
(* FIXME comment *) 
0  230 
datatype thm = Thm of 
1220  231 
{sign: Sign.sg, maxidx: int, 
232 
shyps: sort list, hyps: term list, prop: term}; 

0  233 

250  234 
fun rep_thm (Thm args) = args; 
0  235 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

236 
(*errors involving theorems*) 
0  237 
exception THM of string * int * thm list; 
238 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

239 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

240 
val sign_of_thm = #sign o rep_thm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

241 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  242 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

243 
(*merge signatures of two theorems; raise exception if incompatible*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

244 
fun merge_thm_sgs (th1, th2) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

245 
Sign.merge (pairself sign_of_thm (th1, th2)) 
574  246 
handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]); 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

247 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

248 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

249 
(*maps objectrule to tpairs*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

250 
fun tpairs_of (Thm {prop, ...}) = #1 (Logic.strip_flexpairs prop); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

251 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

252 
(*maps objectrule to premises*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

253 
fun prems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

254 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  255 

256 
(*counts premises in a rule*) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

257 
fun nprems_of (Thm {prop, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

258 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  259 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

260 
(*maps objectrule to conclusion*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

261 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  262 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

263 
(*the statement of any thm is a cterm*) 
1160  264 
fun cprop_of (Thm {sign, maxidx, prop, ...}) = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

265 
Cterm {sign = sign, maxidx = maxidx, T = propT, t = prop}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

266 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

267 

0  268 

1238  269 
(** sort contexts of theorems **) 
270 

271 
(* basic utils *) 

272 

273 
(*accumulate sorts suppressing duplicates; these are coded low level 

274 
to improve efficiency a bit*) 

275 

276 
fun add_typ_sorts (Type (_, Ts), Ss) = add_typs_sorts (Ts, Ss) 

277 
 add_typ_sorts (TFree (_, S), Ss) = S ins Ss 

278 
 add_typ_sorts (TVar (_, S), Ss) = S ins Ss 

279 
and add_typs_sorts ([], Ss) = Ss 

280 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

281 

282 
fun add_term_sorts (Const (_, T), Ss) = add_typ_sorts (T, Ss) 

283 
 add_term_sorts (Free (_, T), Ss) = add_typ_sorts (T, Ss) 

284 
 add_term_sorts (Var (_, T), Ss) = add_typ_sorts (T, Ss) 

285 
 add_term_sorts (Bound _, Ss) = Ss 

286 
 add_term_sorts (Abs (_, T, t), Ss) = add_term_sorts (t, add_typ_sorts (T, Ss)) 

287 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 

288 

289 
fun add_terms_sorts ([], Ss) = Ss 

290 
 add_terms_sorts (t :: ts, Ss) = add_terms_sorts (ts, add_term_sorts (t, Ss)); 

291 

292 
fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) = 

293 
add_terms_sorts (hyps, add_term_sorts (prop, Ss)); 

294 

295 
fun add_thms_shyps ([], Ss) = Ss 

296 
 add_thms_shyps (Thm {shyps, ...} :: ths, Ss) = 

297 
add_thms_shyps (ths, shyps union Ss); 

298 

299 

300 
(*get 'dangling' sort constraints of a thm*) 

301 
fun extra_shyps (th as Thm {shyps, ...}) = 

302 
shyps \\ add_thm_sorts (th, []); 

303 

304 

305 
(* fix_shyps *) 

306 

307 
(*preserve sort contexts of rule premises and substituted types*) 

308 
fun fix_shyps thms Ts thm = 

309 
let 

310 
val Thm {sign, maxidx, hyps, prop, ...} = thm; 

311 
val shyps = 

312 
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); 

313 
in 

314 
Thm {sign = sign, maxidx = maxidx, 

315 
shyps = shyps, hyps = hyps, prop = prop} 

316 
end; 

317 

318 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 

319 

320 

321 
(* strip_shyps *) (* FIXME improve? (e.g. only minimal extra sorts) *) 

322 

323 
val force_strip_shyps = ref true; (* FIXME tmp *) 

324 

325 
(*remove extra sorts that are known to be syntactically nonempty*) 

326 
fun strip_shyps thm = 

327 
let 

328 
val Thm {sign, maxidx, shyps, hyps, prop} = thm; 

329 
val sorts = add_thm_sorts (thm, []); 

330 
val maybe_empty = not o Sign.nonempty_sort sign sorts; 

331 
val shyps' = filter (fn S => S mem sorts orelse maybe_empty S) shyps; 

332 
in 

333 
Thm {sign = sign, maxidx = maxidx, 

334 
shyps = 

335 
(if eq_set (shyps', sorts) orelse not (! force_strip_shyps) then shyps' 

336 
else (* FIXME tmp *) 

337 
(writeln ("WARNING Removed sort hypotheses: " ^ 

338 
commas (map Type.str_of_sort (shyps' \\ sorts))); 

339 
writeln "WARNING Let's hope these sorts are nonempty!"; 

340 
sorts)), 

341 
hyps = hyps, prop = prop} 

342 
end; 

343 

344 

345 
(* implies_intr_shyps *) 

346 

347 
(*discharge all extra sort hypotheses*) 

348 
fun implies_intr_shyps thm = 

349 
(case extra_shyps thm of 

350 
[] => thm 

351 
 xshyps => 

352 
let 

353 
val Thm {sign, maxidx, shyps, hyps, prop} = thm; 

354 
val shyps' = logicS ins (shyps \\ xshyps); 

355 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 

356 
val names = 

357 
tl (variantlist (replicate (length xshyps + 1) "'", used_names)); 

358 
val tfrees = map (TFree o rpair logicS) names; 

359 

360 
fun mk_insort (T, S) = map (Logic.mk_inclass o pair T) S; 

361 
val sort_hyps = flat (map2 mk_insort (tfrees, xshyps)); 

362 
in 

363 
Thm {sign = sign, maxidx = maxidx, shyps = shyps', 

364 
hyps = hyps, prop = Logic.list_implies (sort_hyps, prop)} 

365 
end); 

366 

367 

368 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

369 
(*** Theories ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

370 

0  371 
datatype theory = 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

372 
Theory of { 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

373 
sign: Sign.sg, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

374 
new_axioms: term Symtab.table, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

375 
parents: theory list}; 
0  376 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

377 
fun rep_theory (Theory args) = args; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

378 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

379 
(*errors involving theories*) 
0  380 
exception THEORY of string * theory list; 
381 

382 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

383 
val sign_of = #sign o rep_theory; 
0  384 
val syn_of = #syn o Sign.rep_sg o sign_of; 
385 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

386 
(*stamps associated with a theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

387 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

388 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

389 
(*return the immediate ancestors*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

390 
val parents_of = #parents o rep_theory; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

391 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

392 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

393 
(*compare theories*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

394 
val subthy = Sign.subsig o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

395 
val eq_thy = Sign.eq_sg o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

396 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

397 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

398 
(*look up the named axiom in the theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

399 
fun get_axiom theory name = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

400 
let 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

401 
fun get_ax [] = raise Match 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

402 
 get_ax (Theory {sign, new_axioms, parents} :: thys) = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

403 
(case Symtab.lookup (new_axioms, name) of 
1238  404 
Some t => fix_shyps [] [] 
405 
(Thm {sign = sign, maxidx = maxidx_of_term t, 

406 
shyps = [], hyps = [], prop = t}) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

407 
 None => get_ax parents handle Match => get_ax thys); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

408 
in 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

409 
get_ax [theory] handle Match 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

410 
=> raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

411 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

412 

776
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

413 
(*return additional axioms of this theory node*) 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

414 
fun axioms_of thy = 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

415 
map (fn (s, _) => (s, get_axiom thy s)) 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

416 
(Symtab.dest (#new_axioms (rep_theory thy))); 
df8f91c0e57c
improved axioms_of: returns thms as the manual says;
wenzelm
parents:
721
diff
changeset

417 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

418 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

419 
(* the Pure theories *) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

420 

196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

421 
val proto_pure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

422 
Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

423 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

424 
val pure_thy = 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

425 
Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

426 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

427 
val cpure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

428 
Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

429 

0  430 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

431 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

432 
(** extend theory **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

433 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

434 
fun err_dup_axms names = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

435 
error ("Duplicate axiom name(s) " ^ commas_quote names); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

436 

399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

437 
fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

438 
let 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

439 
val draft = Sign.is_draft sign; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

440 
val new_axioms1 = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

441 
Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

442 
handle Symtab.DUPS names => err_dup_axms names; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

443 
val parents1 = if draft then parents else [thy]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

444 
in 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

445 
Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1} 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

446 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

447 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

448 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

449 
(* extend signature of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

450 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

451 
fun ext_sg extfun decls (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

452 
ext_thy thy (extfun decls sign) []; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

453 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

454 
val add_classes = ext_sg Sign.add_classes; 
421  455 
val add_classrel = ext_sg Sign.add_classrel; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

456 
val add_defsort = ext_sg Sign.add_defsort; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

457 
val add_types = ext_sg Sign.add_types; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

458 
val add_tyabbrs = ext_sg Sign.add_tyabbrs; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

459 
val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

460 
val add_arities = ext_sg Sign.add_arities; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

461 
val add_consts = ext_sg Sign.add_consts; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

462 
val add_consts_i = ext_sg Sign.add_consts_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

463 
val add_syntax = ext_sg Sign.add_syntax; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

464 
val add_syntax_i = ext_sg Sign.add_syntax_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

465 
val add_trfuns = ext_sg Sign.add_trfuns; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

466 
val add_trrules = ext_sg Sign.add_trrules; 
1160  467 
val add_trrules_i = ext_sg Sign.add_trrules_i; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

468 
val add_thyname = ext_sg Sign.add_name; 
0  469 

470 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

471 
(* prepare axioms *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

472 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

473 
fun err_in_axm name = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

474 
error ("The error(s) above occurred in axiom " ^ quote name); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

475 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

476 
fun no_vars tm = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

477 
if null (term_vars tm) andalso null (term_tvars tm) then tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

478 
else error "Illegal schematic variable(s) in term"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

479 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

480 
fun cert_axm sg (name, raw_tm) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

481 
let 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

482 
val Cterm {t, T, ...} = cterm_of sg raw_tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

483 
handle TERM (msg, _) => error msg; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

484 
in 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

485 
assert (T = propT) "Term not of type prop"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

486 
(name, no_vars t) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

487 
end 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

488 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

489 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

490 
fun read_axm sg (name, str) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

491 
(name, no_vars (term_of (read_cterm sg (str, propT)))) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

492 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

493 

564  494 
fun inferT_axm sg (name, pre_tm) = 
959  495 
let val t = #2(Sign.infer_types sg (K None) (K None) [] true 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

496 
([pre_tm], propT)) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

497 
in (name, no_vars t) end 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

498 
handle ERROR => err_in_axm name; 
564  499 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

500 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

501 
(* extend axioms of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

502 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

503 
fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

504 
let 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

505 
val sign1 = Sign.make_draft sign; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

506 
val axioms = map (apsnd Logic.varify o prep_axm sign) axms; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

507 
in 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

508 
ext_thy thy sign1 axioms 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

509 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

510 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

511 
val add_axioms = ext_axms read_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

512 
val add_axioms_i = ext_axms cert_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

513 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

514 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

515 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

516 
(** merge theories **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

517 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

518 
fun merge_thy_list mk_draft thys = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

519 
let 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

520 
fun is_union thy = forall (fn t => subthy (t, thy)) thys; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

521 
val is_draft = Sign.is_draft o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

522 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

523 
fun add_sign (sg, Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

524 
Sign.merge (sg, sign) handle TERM (msg, _) => error msg; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

525 
in 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

526 
(case (find_first is_union thys, exists is_draft thys) of 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

527 
(Some thy, _) => thy 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

528 
 (None, true) => raise THEORY ("Illegal merge of draft theories", thys) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

529 
 (None, false) => Theory { 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

530 
sign = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

531 
(if mk_draft then Sign.make_draft else I) 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

532 
(foldl add_sign (Sign.proto_pure, thys)), 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

533 
new_axioms = Symtab.null, 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

534 
parents = thys}) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

535 
end; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

536 

69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

537 
fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

538 

0  539 

540 

1220  541 
(*** Meta rules ***) 
542 

543 
(** 'primitive' rules **) 

544 

545 
(*discharge all assumptions t from ts*) 

0  546 
val disch = gen_rem (op aconv); 
547 

1220  548 
(*The assumption rule AA in a theory*) 
250  549 
fun assume ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

550 
let val {sign, t=prop, T, maxidx} = rep_cterm ct 
250  551 
in if T<>propT then 
552 
raise THM("assume: assumptions must have type prop", 0, []) 

0  553 
else if maxidx <> ~1 then 
250  554 
raise THM("assume: assumptions may not contain scheme variables", 
555 
maxidx, []) 

1238  556 
else fix_shyps [] [] 
557 
(Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop}) 

0  558 
end; 
559 

1220  560 
(*Implication introduction 
561 
A  B 

562 
 

563 
A ==> B 

564 
*) 

1238  565 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop,...}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

566 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  567 
in if T<>propT then 
250  568 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  569 
else fix_shyps [thB] [] 
570 
(Thm{sign= Sign.merge (sign,signA), maxidx= max[maxidxA, maxidx], 

571 
shyps= [], hyps= disch(hyps,A), prop= implies$A$prop}) 

0  572 
handle TERM _ => 
573 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

574 
end; 

575 

1220  576 
(*Implication elimination 
577 
A ==> B A 

578 
 

579 
B 

580 
*) 

0  581 
fun implies_elim thAB thA : thm = 
582 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA 

250  583 
and Thm{sign, maxidx, hyps, prop,...} = thAB; 
584 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 

0  585 
in case prop of 
250  586 
imp$A$B => 
587 
if imp=implies andalso A aconv propA 

1220  588 
then fix_shyps [thAB, thA] [] 
589 
(Thm{sign= merge_thm_sgs(thAB,thA), 

250  590 
maxidx= max[maxA,maxidx], 
1220  591 
shyps= [], 
250  592 
hyps= hypsA union hyps, (*dups suppressed*) 
1220  593 
prop= B}) 
250  594 
else err("major premise") 
595 
 _ => err("major premise") 

0  596 
end; 
250  597 

1220  598 
(*Forall introduction. The Free or Var x must not be free in the hypotheses. 
599 
A 

600 
 

601 
!!x.A 

602 
*) 

1238  603 
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

604 
let val x = term_of cx; 
1238  605 
fun result(a,T) = fix_shyps [th] [] 
606 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps, 

607 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))}) 

0  608 
in case x of 
250  609 
Free(a,T) => 
610 
if exists (apl(x, Logic.occs)) hyps 

611 
then raise THM("forall_intr: variable free in assumptions", 0, [th]) 

612 
else result(a,T) 

0  613 
 Var((a,_),T) => result(a,T) 
614 
 _ => raise THM("forall_intr: not a variable", 0, [th]) 

615 
end; 

616 

1220  617 
(*Forall elimination 
618 
!!x.A 

619 
 

620 
A[t/x] 

621 
*) 

622 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop,...}) : thm = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

623 
let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct 
0  624 
in case prop of 
250  625 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
626 
if T<>qary then 

627 
raise THM("forall_elim: type mismatch", 0, [th]) 

1220  628 
else fix_shyps [th] [] 
629 
(Thm{sign= Sign.merge(sign,signt), 

250  630 
maxidx= max[maxidx, maxt], 
1220  631 
shyps= [], hyps= hyps, prop= betapply(A,t)}) 
250  632 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  633 
end 
634 
handle TERM _ => 

250  635 
raise THM("forall_elim: incompatible signatures", 0, [th]); 
0  636 

637 

1220  638 
(* Equality *) 
0  639 

1220  640 
(* Definition of the relation =?= *) 
1238  641 
val flexpair_def = fix_shyps [] [] 
642 
(Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0, 

643 
prop= term_of (read_cterm Sign.proto_pure 

644 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); 

0  645 

646 
(*The reflexivity rule: maps t to the theorem t==t *) 

250  647 
fun reflexive ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

648 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  649 
in fix_shyps [] [] 
650 
(Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, 

651 
prop= Logic.mk_equals(t,t)}) 

0  652 
end; 
653 

654 
(*The symmetry rule 

1220  655 
t==u 
656 
 

657 
u==t 

658 
*) 

659 
fun symmetric (th as Thm{sign,shyps,hyps,prop,maxidx}) = 

0  660 
case prop of 
661 
(eq as Const("==",_)) $ t $ u => 

1238  662 
(*no fix_shyps*) 
663 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 

0  664 
 _ => raise THM("symmetric", 0, [th]); 
665 

666 
(*The transitive rule 

1220  667 
t1==u u==t2 
668 
 

669 
t1==t2 

670 
*) 

0  671 
fun transitive th1 th2 = 
672 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

673 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

674 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 

675 
in case (prop1,prop2) of 

676 
((eq as Const("==",_)) $ t1 $ u, Const("==",_) $ u' $ t2) => 

250  677 
if not (u aconv u') then err"middle term" else 
1220  678 
fix_shyps [th1, th2] [] 
679 
(Thm{sign= merge_thm_sgs(th1,th2), shyps= [], 

680 
hyps= hyps1 union hyps2, 

681 
maxidx= max[max1,max2], prop= eq$t1$t2}) 

0  682 
 _ => err"premises" 
683 
end; 

684 

1160  685 
(*Betaconversion: maps (%x.t)(u) to the theorem (%x.t)(u) == t[u/x] *) 
250  686 
fun beta_conversion ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

687 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  688 
in case t of 
1238  689 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
690 
(Thm{sign= sign, shyps= [], hyps= [], 

250  691 
maxidx= maxidx_of_term t, 
1238  692 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))}) 
250  693 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  694 
end; 
695 

696 
(*The extensionality rule (proviso: x not free in f, g, or hypotheses) 

1220  697 
f(x) == g(x) 
698 
 

699 
f == g 

700 
*) 

701 
fun extensional (th as Thm{sign,maxidx,shyps,hyps,prop}) = 

0  702 
case prop of 
703 
(Const("==",_)) $ (f$x) $ (g$y) => 

250  704 
let fun err(msg) = raise THM("extensional: "^msg, 0, [th]) 
0  705 
in (if x<>y then err"different variables" else 
706 
case y of 

250  707 
Free _ => 
708 
if exists (apl(y, Logic.occs)) (f::g::hyps) 

709 
then err"variable free in hyps or functions" else () 

710 
 Var _ => 

711 
if Logic.occs(y,f) orelse Logic.occs(y,g) 

712 
then err"variable free in functions" else () 

713 
 _ => err"not a variable"); 

1238  714 
(*no fix_shyps*) 
1220  715 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, 
250  716 
prop= Logic.mk_equals(f,g)} 
0  717 
end 
718 
 _ => raise THM("extensional: premise", 0, [th]); 

719 

720 
(*The abstraction rule. The Free or Var x must not be free in the hypotheses. 

721 
The bound variable will be named "a" (since x will be something like x320) 

1220  722 
t == u 
723 
 

724 
%x.t == %x.u 

725 
*) 

1238  726 
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

727 
let val x = term_of cx; 
250  728 
val (t,u) = Logic.dest_equals prop 
729 
handle TERM _ => 

730 
raise THM("abstract_rule: premise not an equality", 0, [th]) 

1238  731 
fun result T = fix_shyps [th] [] 
732 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps, 

250  733 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
1238  734 
Abs(a, T, abstract_over (x,u)))}) 
0  735 
in case x of 
250  736 
Free(_,T) => 
737 
if exists (apl(x, Logic.occs)) hyps 

738 
then raise THM("abstract_rule: variable free in assumptions", 0, [th]) 

739 
else result T 

0  740 
 Var(_,T) => result T 
741 
 _ => raise THM("abstract_rule: not a variable", 0, [th]) 

742 
end; 

743 

744 
(*The combination rule 

1220  745 
f==g t==u 
746 
 

747 
f(t)==g(u) 

748 
*) 

0  749 
fun combination th1 th2 = 
1220  750 
let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 
751 
and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2 

0  752 
in case (prop1,prop2) of 
753 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 

1238  754 
(*no fix_shyps*) 
1220  755 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
756 
hyps= hyps1 union hyps2, 

250  757 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 
0  758 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
759 
end; 

760 

761 

762 
(*The equal propositions rule 

1220  763 
A==B A 
764 
 

765 
B 

766 
*) 

0  767 
fun equal_elim th1 th2 = 
768 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

769 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

770 
fun err(msg) = raise THM("equal_elim: "^msg, 0, [th1,th2]) 

771 
in case prop1 of 

772 
Const("==",_) $ A $ B => 

250  773 
if not (prop2 aconv A) then err"not equal" else 
1220  774 
fix_shyps [th1, th2] [] 
775 
(Thm{sign= merge_thm_sgs(th1,th2), shyps= [], 

776 
hyps= hyps1 union hyps2, 

777 
maxidx= max[max1,max2], prop= B}) 

0  778 
 _ => err"major premise" 
779 
end; 

780 

781 

782 
(* Equality introduction 

1220  783 
A==>B B==>A 
784 
 

785 
A==B 

786 
*) 

0  787 
fun equal_intr th1 th2 = 
1220  788 
let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 
789 
and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2; 

0  790 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
791 
in case (prop1,prop2) of 

792 
(Const("==>",_) $ A $ B, Const("==>",_) $ B' $ A') => 

250  793 
if A aconv A' andalso B aconv B' 
1238  794 
then 
795 
(*no fix_shyps*) 

796 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 

797 
hyps= hyps1 union hyps2, 

798 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 

250  799 
else err"not equal" 
0  800 
 _ => err"premises" 
801 
end; 

802 

1220  803 

804 

0  805 
(**** Derived rules ****) 
806 

807 
(*Discharge all hypotheses (need not verify cterms) 

808 
Repeated hypotheses are discharged only once; fold cannot do this*) 

1220  809 
fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = 
1238  810 
implies_intr_hyps (*no fix_shyps*) 
1220  811 
(Thm{sign=sign, maxidx=maxidx, shyps=shyps, 
250  812 
hyps= disch(As,A), prop= implies$A$prop}) 
0  813 
 implies_intr_hyps th = th; 
814 

815 
(*Smash" unifies the list of term pairs leaving no flexflex pairs. 

250  816 
Instantiates the theorem and deletes trivial tpairs. 
0  817 
Resulting sequence may contain multiple elements if the tpairs are 
818 
not all flexflex. *) 

1220  819 
fun flexflex_rule (th as Thm{sign,maxidx,hyps,prop,...}) = 
250  820 
let fun newthm env = 
821 
let val (tpairs,horn) = 

822 
Logic.strip_flexpairs (Envir.norm_term env prop) 

823 
(*Remove trivial tpairs, of the form t=t*) 

824 
val distpairs = filter (not o op aconv) tpairs 

825 
val newprop = Logic.list_flexpairs(distpairs, horn) 

1220  826 
in fix_shyps [th] (env_codT env) 
827 
(Thm{sign= sign, shyps= [], hyps= hyps, 

828 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  829 
end; 
0  830 
val (tpairs,_) = Logic.strip_flexpairs prop 
831 
in Sequence.maps newthm 

250  832 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  833 
end; 
834 

835 
(*Instantiation of Vars 

1220  836 
A 
837 
 

838 
A[t1/v1,....,tn/vn] 

839 
*) 

0  840 

841 
(*Check that all the terms are Vars and are distinct*) 

842 
fun instl_ok ts = forall is_Var ts andalso null(findrep ts); 

843 

844 
(*For instantiate: process pair of cterms, merge theories*) 

845 
fun add_ctpair ((ct,cu), (sign,tpairs)) = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

846 
let val {sign=signt, t=t, T= T, ...} = rep_cterm ct 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

847 
and {sign=signu, t=u, T= U, ...} = rep_cterm cu 
0  848 
in if T=U then (Sign.merge(sign, Sign.merge(signt, signu)), (t,u)::tpairs) 
849 
else raise TYPE("add_ctpair", [T,U], [t,u]) 

850 
end; 

851 

852 
fun add_ctyp ((v,ctyp), (sign',vTs)) = 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

853 
let val {T,sign} = rep_ctyp ctyp 
0  854 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
855 

856 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

857 
Instantiates distinct Vars by terms of same type. 

858 
Normalizes the new theorem! *) 

1220  859 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop,...}) = 
0  860 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
861 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  862 
val newprop = 
863 
Envir.norm_term (Envir.empty 0) 

864 
(subst_atomic tpairs 

865 
(Type.inst_term_tvars(#tsig(Sign.rep_sg newsign),vTs) prop)) 

1220  866 
val newth = 
867 
fix_shyps [th] (map snd vTs) 

868 
(Thm{sign= newsign, shyps= [], hyps= hyps, 

869 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  870 
in if not(instl_ok(map #1 tpairs)) 
193  871 
then raise THM("instantiate: variables not distinct", 0, [th]) 
872 
else if not(null(findrep(map #1 vTs))) 

873 
then raise THM("instantiate: type variables not distinct", 0, [th]) 

874 
else (*Check types of Vars for agreement*) 

875 
case findrep (map (#1 o dest_Var) (term_vars newprop)) of 

250  876 
ix::_ => raise THM("instantiate: conflicting types for variable " ^ 
877 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

878 
 [] => 

879 
case findrep (map #1 (term_tvars newprop)) of 

880 
ix::_ => raise THM 

881 
("instantiate: conflicting sorts for type variable " ^ 

882 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

193  883 
 [] => newth 
0  884 
end 
250  885 
handle TERM _ => 
0  886 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  887 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  888 

889 
(*The trivial implication A==>A, justified by assume and forall rules. 

890 
A can contain Vars, not so for assume! *) 

250  891 
fun trivial ct : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

892 
let val {sign, t=A, T, maxidx} = rep_cterm ct 
250  893 
in if T<>propT then 
894 
raise THM("trivial: the term must have type prop", 0, []) 

1238  895 
else fix_shyps [] [] 
896 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], 

897 
prop= implies$A$A}) 

0  898 
end; 
899 

1160  900 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)"  
1220  901 
essentially just an instance of A==>A.*) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

902 
fun class_triv thy c = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

903 
let 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

904 
val sign = sign_of thy; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

905 
val Cterm {t, maxidx, ...} = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

906 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

907 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

908 
in 
1238  909 
fix_shyps [] [] 
910 
(Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}) 

399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

911 
end; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

912 

86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

913 

0  914 
(* Replace all TFrees not in the hyps by new TVars *) 
1220  915 
fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) = 
0  916 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1238  917 
in (*no fix_shyps*) 
918 
Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps, 

919 
prop= Type.varify(prop,tfrees)} 

0  920 
end; 
921 

922 
(* Replace all TVars by new TFrees *) 

1220  923 
fun freezeT(Thm{sign,maxidx,shyps,hyps,prop}) = 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

924 
let val prop' = Type.freeze prop 
1238  925 
in (*no fix_shyps*) 
926 
Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, 

927 
prop=prop'} 

1220  928 
end; 
0  929 

930 

931 
(*** Inference rules for tactics ***) 

932 

933 
(*Destruct proof state into constraints, other goals, goal(i), rest *) 

934 
fun dest_state (state as Thm{prop,...}, i) = 

935 
let val (tpairs,horn) = Logic.strip_flexpairs prop 

936 
in case Logic.strip_prems(i, [], horn) of 

937 
(B::rBs, C) => (tpairs, rev rBs, B, C) 

938 
 _ => raise THM("dest_state", i, [state]) 

939 
end 

940 
handle TERM _ => raise THM("dest_state", i, [state]); 

941 

309  942 
(*Increment variables and parameters of orule as required for 
0  943 
resolution with goal i of state. *) 
944 
fun lift_rule (state, i) orule = 

1238  945 
let val Thm{shyps=sshyps,prop=sprop,maxidx=smax,...} = state; 
0  946 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 
250  947 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  948 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
1238  949 
val (Thm{sign,maxidx,shyps,hyps,prop}) = orule 
0  950 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  951 
in (*no fix_shyps*) 
952 
Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 

953 
shyps=sshyps union shyps, maxidx= maxidx+smax+1, 

250  954 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 
1238  955 
map lift_all As, lift_all B)} 
0  956 
end; 
957 

958 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. *) 

959 
fun assumption i state = 

1220  960 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  961 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  962 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  963 
fix_shyps [state] (env_codT env) 
964 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

250  965 
if Envir.is_empty env then (*avoid wasted normalizations*) 
966 
Logic.rule_of (tpairs, Bs, C) 

967 
else (*normalize the new rule fully*) 

1220  968 
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); 
0  969 
fun addprfs [] = Sequence.null 
970 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

971 
(Sequence.mapp newth 

250  972 
(Unify.unifiers(sign,Envir.empty maxidx, (t,u)::tpairs)) 
973 
(addprfs apairs))) 

0  974 
in addprfs (Logic.assum_pairs Bi) end; 
975 

250  976 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  977 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
978 
fun eq_assumption i state = 

1220  979 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  980 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
981 
in if exists (op aconv) (Logic.assum_pairs Bi) 

1220  982 
then fix_shyps [state] [] 
983 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, 

984 
prop=Logic.rule_of(tpairs, Bs, C)}) 

0  985 
else raise THM("eq_assumption", 0, [state]) 
986 
end; 

987 

988 

989 
(** User renaming of parameters in a subgoal **) 

990 

991 
(*Calls error rather than raising an exception because it is intended 

992 
for toplevel use  exception handling would not make sense here. 

993 
The names in cs, if distinct, are used for the innermost parameters; 

994 
preceding parameters may be renamed to make all params distinct.*) 

995 
fun rename_params_rule (cs, i) state = 

1220  996 
let val Thm{sign,maxidx,hyps,prop,...} = state 
0  997 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
998 
val iparams = map #1 (Logic.strip_params Bi) 

999 
val short = length iparams  length cs 

250  1000 
val newnames = 
1001 
if short<0 then error"More names than abstractions!" 

1002 
else variantlist(take (short,iparams), cs) @ cs 

0  1003 
val freenames = map (#1 o dest_Free) (term_frees prop) 
1004 
val newBi = Logic.list_rename_params (newnames, Bi) 

250  1005 
in 
0  1006 
case findrep cs of 
1007 
c::_ => error ("Bound variables not distinct: " ^ c) 

1008 
 [] => (case cs inter freenames of 

1009 
a::_ => error ("Bound/Free variable clash: " ^ a) 

1220  1010 
 [] => fix_shyps [state] [] 
1011 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

1012 
Logic.rule_of(tpairs, Bs@[newBi], C)})) 

0  1013 
end; 
1014 

1015 
(*** Preservation of bound variable names ***) 

1016 

250  1017 
(*Scan a pair of terms; while they are similar, 
0  1018 
accumulate corresponding bound vars in "al"*) 
1238  1019 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
1195
686e3eb613b9
match_bvs no longer puts a name in the alist if it is null ("")
lcp
parents:
1160
diff
changeset

1020 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1021 
else (x,y)::al) 
0  1022 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1023 
 match_bvs(_,_,al) = al; 

1024 

1025 
(* strip abstractions created by parameters *) 

1026 
fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); 

1027 

1028 

250  1029 
(* strip_apply f A(,B) strips off all assumptions/parameters from A 
0  1030 
introduced by lifting over B, and applies f to remaining part of A*) 
1031 
fun strip_apply f = 

1032 
let fun strip(Const("==>",_)$ A1 $ B1, 

250  1033 
Const("==>",_)$ _ $ B2) = implies $ A1 $ strip(B1,B2) 
1034 
 strip((c as Const("all",_)) $ Abs(a,T,t1), 

1035 
Const("all",_) $ Abs(_,_,t2)) = c$Abs(a,T,strip(t1,t2)) 

1036 
 strip(A,_) = f A 

0  1037 
in strip end; 
1038 

1039 
(*Use the alist to rename all bound variables and some unknowns in a term 

1040 
dpairs = current disagreement pairs; tpairs = permanent ones (flexflex); 

1041 
Preserves unknowns in tpairs and on lhs of dpairs. *) 

1042 
fun rename_bvs([],_,_,_) = I 

1043 
 rename_bvs(al,dpairs,tpairs,B) = 

250  1044 
let val vars = foldr add_term_vars 
1045 
(map fst dpairs @ map fst tpairs @ map snd tpairs, []) 

1046 
(*unknowns appearing elsewhere be preserved!*) 

1047 
val vids = map (#1 o #1 o dest_Var) vars; 

1048 
fun rename(t as Var((x,i),T)) = 

1049 
(case assoc(al,x) of 

1050 
Some(y) => if x mem vids orelse y mem vids then t 

1051 
else Var((y,i),T) 

1052 
 None=> t) 

0  1053 
 rename(Abs(x,T,t)) = 
250  1054 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1055 
T, rename t) 

0  1056 
 rename(f$t) = rename f $ rename t 
1057 
 rename(t) = t; 

250  1058 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1059 
in strip_ren end; 
1060 

1061 
(*Function to rename bounds/unknowns in the argument, lifted over B*) 

1062 
fun rename_bvars(dpairs, tpairs, B) = 

250  1063 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1064 

1065 

1066 
(*** RESOLUTION ***) 

1067 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1068 
(** Lifting optimizations **) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1069 

0  1070 
(*strip off pairs of assumptions/parameters in parallel  they are 
1071 
identical because of lifting*) 

250  1072 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1073 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1074 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1075 
Const("all",_)$Abs(_,_,t2)) = 
0  1076 
let val (B1,B2) = strip_assums2 (t1,t2) 
1077 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1078 
 strip_assums2 BB = BB; 

1079 

1080 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1081 
(*Faster normalization: skip assumptions that were lifted over*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1082 
fun norm_term_skip env 0 t = Envir.norm_term env t 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1083 
 norm_term_skip env n (Const("all",_)$Abs(a,T,t)) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1084 
let val Envir.Envir{iTs, ...} = env 
1238  1085 
val T' = typ_subst_TVars iTs T 
1086 
(*Must instantiate types of parameters because they are flattened; 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1087 
this could be a NEW parameter*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1088 
in all T' $ Abs(a, T', norm_term_skip env n t) end 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1089 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1090 
implies $ A $ norm_term_skip env (n1) B 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1091 
 norm_term_skip env n t = error"norm_term_skip: too few assumptions??"; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1092 

479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1093 

0  1094 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 
250  1095 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  1096 
If match then forbid instantiations in proof state 
1097 
If lifted then shorten the dpair using strip_assums2. 

1098 
If eres_flg then simultaneously proves A1 by assumption. 

250  1099 
nsubgoal is the number of new subgoals (written m above). 
0  1100 
Curried so that resolution calls dest_state only once. 
1101 
*) 

1102 
local open Sequence; exception Bicompose 

1103 
in 

250  1104 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1105 
(eres_flg, orule, nsubgoal) = 
1106 
let val Thm{maxidx=smax, hyps=shyps, ...} = state 

721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1107 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule 
1238  1108 
(*How many hyps to skip over during normalization*) 
1109 
and nlift = Logic.count_prems(strip_all_body Bi, 

1110 
if eres_flg then ~1 else 0) 

387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

1111 
val sign = merge_thm_sgs(state,orule); 
0  1112 
(** Add new theorem with prop = '[ Bs; As ] ==> C' to thq **) 
250  1113 
fun addth As ((env as Envir.Envir {maxidx, ...}, tpairs), thq) = 
1114 
let val normt = Envir.norm_term env; 

1115 
(*perform minimal copying here by examining env*) 

1116 
val normp = 

1117 
if Envir.is_empty env then (tpairs, Bs @ As, C) 

1118 
else 

1119 
let val ntps = map (pairself normt) tpairs 

1238  1120 
in if the (Envir.minidx env) > smax then 
1121 
(*no assignments in state; normalize the rule only*) 

1122 
if lifted 

1123 
then (ntps, Bs @ map (norm_term_skip env nlift) As, C) 

1124 
else (ntps, Bs @ map normt As, C) 

250  1125 
else if match then raise Bicompose 
1126 
else (*normalize the new rule fully*) 

1127 
(ntps, map normt (Bs @ As), normt C) 

1128 
end 

1238  1129 
val th = (* FIXME improve *) 
1220  1130 
fix_shyps [state, orule] (env_codT env) 
1131 
(Thm{sign=sign, shyps=[], hyps=rhyps union shyps, 

1132 
maxidx=maxidx, prop= Logic.rule_of normp}) 

0  1133 
in cons(th, thq) end handle Bicompose => thq 
1134 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 

1135 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

1136 
handle TERM _ => raise THM("bicompose: rule", 0, [orule,state]); 

1137 
(*Modify assumptions, deleting nth if n>0 for eresolution*) 

1138 
fun newAs(As0, n, dpairs, tpairs) = 

1139 
let val As1 = if !Logic.auto_rename orelse not lifted then As0 

250  1140 
else map (rename_bvars(dpairs,tpairs,B)) As0 
0  1141 
in (map (Logic.flatten_params n) As1) 
250  1142 
handle TERM _ => 
1143 
raise THM("bicompose: 1st premise", 0, [orule]) 

0  1144 
end; 
1145 
val env = Envir.empty(max[rmax,smax]); 

1146 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 

1147 
val dpairs = BBi :: (rtpairs@stpairs); 

1148 
(*elimresolution: try each assumption in turn. Initially n=1*) 

1149 
fun tryasms (_, _, []) = null 

1150 
 tryasms (As, n, (t,u)::apairs) = 

250  1151 
(case pull(Unify.unifiers(sign, env, (t,u)::dpairs)) of 
1152 
None => tryasms (As, n+1, apairs) 

1153 
 cell as Some((_,tpairs),_) => 

1154 
its_right (addth (newAs(As, n, [BBi,(u,t)], tpairs))) 

1155 
(seqof (fn()=> cell), 

1156 
seqof (fn()=> pull (tryasms (As, n+1, apairs))))); 

0  1157 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) 
1158 
 eres (A1::As) = tryasms (As, 1, Logic.assum_pairs A1); 

1159 
(*ordinary resolution*) 

1160 
fun res(None) = null 

250  1161 
 res(cell as Some((_,tpairs),_)) = 
1162 
its_right (addth(newAs(rev rAs, 0, [BBi], tpairs))) 

1163 
(seqof (fn()=> cell), null) 

0  1164 
in if eres_flg then eres(rev rAs) 
1165 
else res(pull(Unify.unifiers(sign, env, dpairs))) 

1166 
end; 

1167 
end; (*open Sequence*) 

1168 

1169 

1170 
fun bicompose match arg i state = 

1171 
bicompose_aux match (state, dest_state(state,i), false) arg; 

1172 

1173 
(*Quick test whether rule is resolvable with the subgoal with hyps Hs 

1174 
and conclusion B. If eres_flg then checks 1st premise of rule also*) 

1175 
fun could_bires (Hs, B, eres_flg, rule) = 

1176 
let fun could_reshyp (A1::_) = exists (apl(A1,could_unify)) Hs 

250  1177 
 could_reshyp [] = false; (*no premise  illegal*) 
1178 
in could_unify(concl_of rule, B) andalso 

1179 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1180 
end; 
1181 

1182 
(*Biresolution of a state with a list of (flag,rule) pairs. 

1183 
Puts the rule above: rule/state. Renames vars in the rules. *) 

250  1184 
fun biresolution match brules i state = 
0  1185 
let val lift = lift_rule(state, i); 
250  1186 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1187 
val B = Logic.strip_assums_concl Bi; 

1188 
val Hs = Logic.strip_assums_hyp Bi; 

1189 
val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true); 

1190 
fun res [] = Sequence.null 

1191 
 res ((eres_flg, rule)::brules) = 

1192 
if could_bires (Hs, B, eres_flg, rule) 

1160  1193 
then Sequence.seqof (*delay processing remainder till needed*) 
250  1194 
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule), 
1195 
res brules)) 

1196 
else res brules 

0  1197 
in Sequence.flats (res brules) end; 
1198 

1199 

1200 

1201 
(*** Meta simp sets ***) 

1202 

288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1203 
type rrule = {thm:thm, lhs:term, perm:bool}; 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1204 
type cong = {thm:thm, lhs:term}; 
0  1205 
datatype meta_simpset = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1206 
Mss of {net:rrule Net.net, congs:(string * cong)list, bounds:string list, 
0  1207 
prems: thm list, mk_rews: thm > thm list}; 
1208 

1209 
(*A "mss" contains data needed during conversion: 

1210 
net: discrimination net of rewrite rules 

1211 
congs: association list of congruence rules 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1212 
bounds: names of bound variables already used; 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1213 
for generating new names when rewriting under lambda abstractions 
0  1214 
mk_rews: used when local assumptions are added 
1215 
*) 

1216 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1217 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1218 
mk_rews = K[]}; 
1219 

1220 
exception SIMPLIFIER of string * thm; 

1221 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

1222 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1223 

209  1224 
val trace_simp = ref false; 
1225 

229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

1226 
fun trace_term a sign t = if !trace_simp then prtm a sign t else (); 
209  1227 

1228 
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop; 

1229 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1230 
fun vperm(Var _, Var _) = true 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1231 
 vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1232 
 vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1233 
 vperm(t,u) = (t=u); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1234 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1235 
fun var_perm(t,u) = vperm(t,u) andalso 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1236 
eq_set(add_term_vars(t,[]), add_term_vars(u,[])) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1237 

0  1238 
(*simple test for looping rewrite*) 
1239 
fun loops sign prems (lhs,rhs) = 

1023
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1240 
is_Var(lhs) 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1241 
orelse 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1242 
(exists (apl(lhs, Logic.occs)) (rhs::prems)) 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1243 
orelse 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1244 
(null(prems) andalso 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1245 
Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
1028  1246 
(* the condition "null(prems)" in the last case is necessary because 
1247 
conditional rewrites with extra variables in the conditions may terminate 

1248 
although the rhs is an instance of the lhs. Example: 

1249 
?m < ?n ==> f(?n) == f(?m) 

1250 
*) 

0  1251 

1238  1252 
fun mk_rrule raw_thm = 
1253 
let 

1254 
val thm = strip_shyps raw_thm; (* FIXME tmp *) 

1255 
val Thm{sign,prop,maxidx,...} = thm; 

1256 
val prems = Logic.strip_imp_prems prop 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1257 
val concl = Logic.strip_imp_concl prop 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1258 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1259 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1260 
val econcl = Pattern.eta_contract concl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1261 
val (elhs,erhs) = Logic.dest_equals econcl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1262 
val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1263 
andalso not(is_Var(elhs)) 
1220  1264 
in 
1238  1265 
if not (null (extra_shyps thm)) then (* FIXME tmp *) 
1266 
raise SIMPLIFIER ("Rewrite rule may not contain extra sort hypotheses", thm) 

1220  1267 
else if not perm andalso loops sign prems (elhs,erhs) then 
1268 
(prtm "Warning: ignoring looping rewrite rule" sign prop; None) 

288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1269 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1270 
end; 
1271 

87  1272 
local 
1273 
fun eq({thm=Thm{prop=p1,...},...}:rrule, 

1274 
{thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2 

1275 
in 

1276 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1277 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1278 
thm as Thm{sign,prop,...}) = 
87  1279 
case mk_rrule thm of 
1280 
None => mss 

1281 
 Some(rrule as {lhs,...}) => 

209  1282 
(trace_thm "Adding rewrite rule:" thm; 
1283 
Mss{net= (Net.insert_term((lhs,rrule),net,eq) 

1284 
handle Net.INSERT => 

87  1285 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop; 
1286 
net)), 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1287 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1288 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1289 
fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
87  1290 
thm as Thm{sign,prop,...}) = 
1291 
case mk_rrule thm of 

1292 
None => mss 

1293 
 Some(rrule as {lhs,...}) => 

1294 
Mss{net= (Net.delete_term((lhs,rrule),net,eq) 

1295 
handle Net.INSERT => 

1296 
(prtm "Warning: rewrite rule not in simpset" sign prop; 

1297 
net)), 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1298 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1299 

1300 
end; 

0  1301 

1302 
val add_simps = foldl add_simp; 

87  1303 
val del_simps = foldl del_simp; 
0  1304 

1305 
fun mss_of thms = add_simps(empty_mss,thms); 

1306 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1307 
fun add_cong(Mss{net,congs,bounds,prems,mk_rews},thm) = 
0  1308 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => 
1309 
raise SIMPLIFIER("Congruence not a metaequality",thm) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1310 
(* val lhs = Pattern.eta_contract lhs*) 
0  1311 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1312 
raise SIMPLIFIER("Congruence must start with a constant",thm) 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1313 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1314 
prems=prems, mk_rews=mk_rews} 
1315 
end; 

1316 

1317 
val (op add_congs) = foldl add_cong; 

1318 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1319 
fun add_prems(Mss{net,congs,bounds,prems,mk_rews},thms) = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1320 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1321 

1322 
fun prems_of_mss(Mss{prems,...}) = prems; 

1323 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1324 
fun set_mk_rews(Mss{net,congs,bounds,prems,...},mk_rews) = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1325 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1326 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1327 

1328 

250  1329 
(*** Metalevel rewriting 
0  1330 
uses conversions, omitting proofs for efficiency. See 
250  1331 
L C Paulson, A higherorder implementation of rewriting, 
1332 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1333 

1334 
type prover = meta_simpset > thm > thm option; 

1335 
type termrec = (Sign.sg * term list) * term; 

1336 
type conv = meta_simpset > termrec > termrec; 

1337 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1338 
datatype order = LESS  EQUAL  GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1339 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1340 
fun stringord(a,b:string) = if a<b then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1341 
if a=b then EQUAL else GREATER; 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1342 

4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1343 
fun intord(i,j:int) = if i<j then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1344 
if i=j then EQUAL else GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1345 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1346 
(* NB: nonlinearity of the ordering is not a soundness problem *) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1347 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1348 
(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering nonlinear *) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1349 
fun string_of_hd(Const(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1350 
 string_of_hd(Free(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1351 
 string_of_hd(Var(v,_)) = Syntax.string_of_vname v 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1352 
 string_of_hd(Bound i) = string_of_int i 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1353 
 string_of_hd(Abs _) = "***ABSTRACTION***"; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1354 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1355 
(* a strict (not reflexive) linear wellfounded ACcompatible ordering 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1356 
* for terms: 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1357 
* s < t <=> 1. size(s) < size(t) or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1358 
2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1359 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1360 
(s1..sn) < (t1..tn) (lexicographically) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1361 
*) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1362 

b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1363 
(* FIXME: should really take types into account as well. 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1364 
* Otherwise nonlinear *) 
622
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1365 
fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u) 
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1366 
 termord(t,u) = 
305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1367 
(case intord(size_of_term t,size_of_term u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1368 
EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1369 
in case stringord(string_of_hd f, string_of_hd g) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1370 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1371 
 ord => ord 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1372 
end 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1373 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1374 
and lextermord(t::ts,u::us) = 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1375 
(case termord(t,u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1376 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1377 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1378 
 lextermord([],[]) = EQUAL 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1379 
 lextermord _ = error("lextermord"); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1380 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1381 
fun termless tu = (termord tu = LESS); 