author  wenzelm 
Thu, 21 Sep 1995 11:26:44 +0200  
changeset 1258  2a2d8c74a756 
parent 1238  289c573327f0 
child 1394  a1d2735f5ade 
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 

1258  292 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
293 

294 
fun add_env_sorts (env, Ss) = 

295 
add_terms_sorts (map snd (Envir.alist_of env), 

296 
add_typs_sorts (env_codT env, Ss)); 

297 

1238  298 
fun add_thm_sorts (Thm {hyps, prop, ...}, Ss) = 
299 
add_terms_sorts (hyps, add_term_sorts (prop, Ss)); 

300 

301 
fun add_thms_shyps ([], Ss) = Ss 

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

303 
add_thms_shyps (ths, shyps union Ss); 

304 

305 

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

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

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

309 

310 

311 
(* fix_shyps *) 

312 

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

314 
fun fix_shyps thms Ts thm = 

315 
let 

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

317 
val shyps = 

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

319 
in 

320 
Thm {sign = sign, maxidx = maxidx, 

321 
shyps = shyps, hyps = hyps, prop = prop} 

322 
end; 

323 

324 

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

326 

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

328 

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

330 
fun strip_shyps thm = 

331 
let 

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

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

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

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

336 
in 

337 
Thm {sign = sign, maxidx = maxidx, 

338 
shyps = 

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

340 
else (* FIXME tmp *) 

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

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

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

344 
sorts)), 

345 
hyps = hyps, prop = prop} 

346 
end; 

347 

348 

349 
(* implies_intr_shyps *) 

350 

351 
(*discharge all extra sort hypotheses*) 

352 
fun implies_intr_shyps thm = 

353 
(case extra_shyps thm of 

354 
[] => thm 

355 
 xshyps => 

356 
let 

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

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

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

360 
val names = 

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

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

363 

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

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

366 
in 

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

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

369 
end); 

370 

371 

372 

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

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

374 

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

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

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

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

379 
parents: theory list}; 
0  380 

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

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

382 

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

383 
(*errors involving theories*) 
0  384 
exception THEORY of string * theory list; 
385 

386 

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

387 
val sign_of = #sign o rep_theory; 
0  388 
val syn_of = #syn o Sign.rep_sg o sign_of; 
389 

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

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

391 
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

392 

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

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

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

395 

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 
(*compare theories*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

399 
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

400 

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

401 

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

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

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

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

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

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

407 
(case Symtab.lookup (new_axioms, name) of 
1238  408 
Some t => fix_shyps [] [] 
409 
(Thm {sign = sign, maxidx = maxidx_of_term t, 

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

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

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

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

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

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

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

416 

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

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

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

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

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

421 

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

422 

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

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

424 

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

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

426 
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

427 

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

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

429 
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

430 

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

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

432 
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

433 

0  434 

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

435 

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

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

437 

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

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

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

440 

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

441 
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

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

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

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

445 
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

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

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

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

449 
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

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

451 

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

452 

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

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

454 

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

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

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

457 

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

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

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

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

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

463 
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

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

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

466 
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

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

468 
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

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

470 
val add_trrules = ext_sg Sign.add_trrules; 
1160  471 
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

472 
val add_thyname = ext_sg Sign.add_name; 
0  473 

474 

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

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

476 

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

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

478 
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

479 

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

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

481 
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

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

483 

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

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

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

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

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

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

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

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

491 
end 
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 

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

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

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

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

497 

564  498 
fun inferT_axm sg (name, pre_tm) = 
959  499 
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

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

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

502 
handle ERROR => err_in_axm name; 
564  503 

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

504 

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

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

506 

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

507 
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

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

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

510 
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

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

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

513 
end; 
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 
val add_axioms = ext_axms read_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

516 
val add_axioms_i = ext_axms cert_axm; 
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 

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

519 

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

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

521 

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

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

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

524 
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

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

526 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

540 

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

541 
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

542 

0  543 

544 

1220  545 
(*** Meta rules ***) 
546 

547 
(** 'primitive' rules **) 

548 

549 
(*discharge all assumptions t from ts*) 

0  550 
val disch = gen_rem (op aconv); 
551 

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

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

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

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

0  562 
end; 
563 

1220  564 
(*Implication introduction 
565 
A  B 

566 
 

567 
A ==> B 

568 
*) 

1238  569 
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

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

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

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

578 
end; 

579 

1220  580 
(*Implication elimination 
581 
A ==> B A 

582 
 

583 
B 

584 
*) 

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

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

0  589 
in case prop of 
250  590 
imp$A$B => 
591 
if imp=implies andalso A aconv propA 

1220  592 
then fix_shyps [thAB, thA] [] 
593 
(Thm{sign= merge_thm_sgs(thAB,thA), 

250  594 
maxidx= max[maxA,maxidx], 
1220  595 
shyps= [], 
250  596 
hyps= hypsA union hyps, (*dups suppressed*) 
1220  597 
prop= B}) 
250  598 
else err("major premise") 
599 
 _ => err("major premise") 

0  600 
end; 
250  601 

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

604 
 

605 
!!x.A 

606 
*) 

1238  607 
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

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

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

0  612 
in case x of 
250  613 
Free(a,T) => 
614 
if exists (apl(x, Logic.occs)) hyps 

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

616 
else result(a,T) 

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

619 
end; 

620 

1220  621 
(*Forall elimination 
622 
!!x.A 

623 
 

624 
A[t/x] 

625 
*) 

626 
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

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

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

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

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

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

641 

1220  642 
(* Equality *) 
0  643 

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

647 
prop= term_of (read_cterm Sign.proto_pure 

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

0  649 

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

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

652 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  653 
in fix_shyps [] [] 
654 
(Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, 

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

0  656 
end; 
657 

658 
(*The symmetry rule 

1220  659 
t==u 
660 
 

661 
u==t 

662 
*) 

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

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

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

0  668 
 _ => raise THM("symmetric", 0, [th]); 
669 

670 
(*The transitive rule 

1220  671 
t1==u u==t2 
672 
 

673 
t1==t2 

674 
*) 

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

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

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

679 
in case (prop1,prop2) of 

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

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

684 
hyps= hyps1 union hyps2, 

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

0  686 
 _ => err"premises" 
687 
end; 

688 

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

691 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  692 
in case t of 
1238  693 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
694 
(Thm{sign= sign, shyps= [], hyps= [], 

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

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

1220  701 
f(x) == g(x) 
702 
 

703 
f == g 

704 
*) 

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

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

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

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

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

714 
 Var _ => 

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

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

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

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

723 

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

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

1220  726 
t == u 
727 
 

728 
%x.t == %x.u 

729 
*) 

1238  730 
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

731 
let val x = term_of cx; 
250  732 
val (t,u) = Logic.dest_equals prop 
733 
handle TERM _ => 

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

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

250  737 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
1238  738 
Abs(a, T, abstract_over (x,u)))}) 
0  739 
in case x of 
250  740 
Free(_,T) => 
741 
if exists (apl(x, Logic.occs)) hyps 

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

743 
else result T 

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

746 
end; 

747 

748 
(*The combination rule 

1220  749 
f==g t==u 
750 
 

751 
f(t)==g(u) 

752 
*) 

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

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

1238  758 
(*no fix_shyps*) 
1220  759 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
760 
hyps= hyps1 union hyps2, 

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

764 

765 

766 
(*The equal propositions rule 

1220  767 
A==B A 
768 
 

769 
B 

770 
*) 

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

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

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

775 
in case prop1 of 

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

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

780 
hyps= hyps1 union hyps2, 

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

0  782 
 _ => err"major premise" 
783 
end; 

784 

785 

786 
(* Equality introduction 

1220  787 
A==>B B==>A 
788 
 

789 
A==B 

790 
*) 

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

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

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

250  797 
if A aconv A' andalso B aconv B' 
1238  798 
then 
799 
(*no fix_shyps*) 

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

801 
hyps= hyps1 union hyps2, 

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

250  803 
else err"not equal" 
0  804 
 _ => err"premises" 
805 
end; 

806 

1220  807 

808 

0  809 
(**** Derived rules ****) 
810 

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

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

1220  813 
fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = 
1238  814 
implies_intr_hyps (*no fix_shyps*) 
1220  815 
(Thm{sign=sign, maxidx=maxidx, shyps=shyps, 
250  816 
hyps= disch(As,A), prop= implies$A$prop}) 
0  817 
 implies_intr_hyps th = th; 
818 

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

250  820 
Instantiates the theorem and deletes trivial tpairs. 
0  821 
Resulting sequence may contain multiple elements if the tpairs are 
822 
not all flexflex. *) 

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

826 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

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

832 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  833 
end; 
0  834 
val (tpairs,_) = Logic.strip_flexpairs prop 
835 
in Sequence.maps newthm 

250  836 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  837 
end; 
838 

839 
(*Instantiation of Vars 

1220  840 
A 
841 
 

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

843 
*) 

0  844 

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

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

847 

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

849 
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

850 
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

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

854 
end; 

855 

856 
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

857 
let val {T,sign} = rep_ctyp ctyp 
0  858 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
859 

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

861 
Instantiates distinct Vars by terms of same type. 

862 
Normalizes the new theorem! *) 

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

250  866 
val newprop = 
867 
Envir.norm_term (Envir.empty 0) 

868 
(subst_atomic tpairs 

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

1220  870 
val newth = 
871 
fix_shyps [th] (map snd vTs) 

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

873 
maxidx= maxidx_of_term newprop, prop= newprop}) 

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

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

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

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

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

882 
 [] => 

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

884 
ix::_ => raise THM 

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

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

193  887 
 [] => newth 
0  888 
end 
250  889 
handle TERM _ => 
0  890 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  891 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  892 

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

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

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

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

1238  899 
else fix_shyps [] [] 
900 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], 

901 
prop= implies$A$A}) 

0  902 
end; 
903 

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

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

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

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

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

910 
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

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

912 
in 
1238  913 
fix_shyps [] [] 
914 
(Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}) 

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

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

916 

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

917 

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

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

0  924 
end; 
925 

926 
(* Replace all TVars by new TFrees *) 

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

928 
let val prop' = Type.freeze prop 
1238  929 
in (*no fix_shyps*) 
930 
Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, 

931 
prop=prop'} 

1220  932 
end; 
0  933 

934 

935 
(*** Inference rules for tactics ***) 

936 

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

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

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

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

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

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

943 
end 

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

945 

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

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

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

250  958 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 
1238  959 
map lift_all As, lift_all B)} 
0  960 
end; 
961 

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

963 
fun assumption i state = 

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

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

971 
else (*normalize the new rule fully*) 

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

975 
(Sequence.mapp newth 

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

0  978 
in addprfs (Logic.assum_pairs Bi) end; 
979 

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

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

1220  986 
then fix_shyps [state] [] 
987 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, 

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

0  989 
else raise THM("eq_assumption", 0, [state]) 
990 
end; 

991 

992 

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

994 

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

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

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

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

999 
fun rename_params_rule (cs, i) state = 

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

1003 
val short = length iparams  length cs 

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

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

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

250  1009 
in 
0  1010 
case findrep cs of 
1011 
c::_ => error ("Bound variables not distinct: " ^ c) 

1012 
 [] => (case cs inter freenames of 

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

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

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

0  1017 
end; 
1018 

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

1020 

250  1021 
(*Scan a pair of terms; while they are similar, 
0  1022 
accumulate corresponding bound vars in "al"*) 
1238  1023 
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

1024 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1025 
else (x,y)::al) 
0  1026 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1027 
 match_bvs(_,_,al) = al; 

1028 

1029 
(* strip abstractions created by parameters *) 

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

1031 

1032 

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

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

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

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

1040 
 strip(A,_) = f A 

0  1041 
in strip end; 
1042 

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

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

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

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

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

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

1050 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1053 
(case assoc(al,x) of 

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

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

1056 
 None=> t) 

0  1057 
 rename(Abs(x,T,t)) = 
250  1058 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1059 
T, rename t) 

0  1060 
 rename(f$t) = rename f $ rename t 
1061 
 rename(t) = t; 

250  1062 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1063 
in strip_ren end; 
1064 

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

1066 
fun rename_bvars(dpairs, tpairs, B) = 

250  1067 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1068 

1069 

1070 
(*** RESOLUTION ***) 

1071 

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

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

1073 

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

250  1076 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1077 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1078 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1079 
Const("all",_)$Abs(_,_,t2)) = 
0  1080 
let val (B1,B2) = strip_assums2 (t1,t2) 
1081 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1082 
 strip_assums2 BB = BB; 

1083 

1084 

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

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

1086 
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

1087 
 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

1088 
let val Envir.Envir{iTs, ...} = env 
1238  1089 
val T' = typ_subst_TVars iTs T 
1090 
(*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

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

1092 
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

1093 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
1238  1094 
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

1095 
 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

1096 

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

1097 

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

1102 
If eres_flg then simultaneously proves A1 by assumption. 

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

1106 
local open Sequence; exception Bicompose 

1107 
in 

250  1108 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1109 
(eres_flg, orule, nsubgoal) = 
1258  1110 
let val Thm{maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1111 
and Thm{maxidx=rmax, shyps=rshyps, hyps=rhyps, prop=rprop,...} = orule 

1238  1112 
(*How many hyps to skip over during normalization*) 
1113 
and nlift = Logic.count_prems(strip_all_body Bi, 

1114 
if eres_flg then ~1 else 0) 

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

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

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

1120 
val normp = 

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

1122 
else 

1123 
let val ntps = map (pairself normt) tpairs 

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

1126 
if lifted 

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

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

250  1129 
else if match then raise Bicompose 
1130 
else (*normalize the new rule fully*) 

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

1132 
end 

1258  1133 
val th = (*tuned fix_shyps*) 
1134 
Thm{sign=sign, 

1135 
shyps=add_env_sorts (env, rshyps union sshyps), 

1136 
hyps=rhyps union shyps, 

1137 
maxidx=maxidx, prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1164 
(*ordinary resolution*) 

1165 
fun res(None) = null 

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

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

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

1171 
end; 

1172 
end; (*open Sequence*) 

1173 

1174 

1175 
fun bicompose match arg i state = 

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

1177 

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

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

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

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

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

1184 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1185 
end; 
1186 

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

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

250  1189 
fun biresolution match brules i state = 
0  1190 
let val lift = lift_rule(state, i); 
250  1191 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1192 
val B = Logic.strip_assums_concl Bi; 

1193 
val Hs = Logic.strip_assums_hyp Bi; 

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

1195 
fun res [] = Sequence.null 

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

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

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

1201 
else res brules 

0  1202 
in Sequence.flats (res brules) end; 
1203 

1204 

1205 

1206 
(*** Meta simp sets ***) 

1207 

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

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

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

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

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

1215 
net: discrimination net of rewrite rules 

1216 
congs: association list of congruence rules 

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

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

1218 
for generating new names when rewriting under lambda abstractions 
0  1219 
mk_rews: used when local assumptions are added 
1220 
*) 

1221 

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

1222 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1223 
mk_rews = K[]}; 
1224 

1225 
exception SIMPLIFIER of string * thm; 

1226 

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

1227 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1228 

209  1229 
val trace_simp = ref false; 
1230 

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

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

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

1234 

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

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

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

1237 
 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

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

1239 

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

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

1241 
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

1242 

0  1243 
(*simple test for looping rewrite*) 
1244 
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

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

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

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

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

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

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

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

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

1255 
*) 

0  1256 

1238  1257 
fun mk_rrule raw_thm = 
1258 
let 

1258  1259 
val thm = strip_shyps raw_thm; 
1238  1260 
val Thm{sign,prop,maxidx,...} = thm; 
1261 
val prems = Logic.strip_imp_prems prop 

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

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

1263 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1264 
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

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

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

1267 
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

1268 
andalso not(is_Var(elhs)) 
1220  1269 
in 
1258  1270 
if not perm andalso loops sign prems (elhs,erhs) then 
1220  1271 
(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

1272 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1273 
end; 
1274 

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

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

1278 
in 

1279 

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

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

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

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

1287 
handle Net.INSERT => 

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

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

1290 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1291 

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

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

1295 
None => mss 

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

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

1298 
handle Net.INSERT => 

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

1300 
net)), 

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

1301 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1302 

1303 
end; 

0  1304 

1305 
val add_simps = foldl add_simp; 

87  1306 
val del_simps = foldl del_simp; 
0  1307 

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

1309 

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

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

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

1313 
(* val lhs = Pattern.eta_contract lhs*) 
0  1314 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1315 
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

1316 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1317 
prems=prems, mk_rews=mk_rews} 
1318 
end; 

1319 

1320 
val (op add_congs) = foldl add_cong; 

1321 

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

1322 
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

1323 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1324 

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

1326 

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

1327 
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

1328 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1329 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1330 

1331 

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

0  1336 

1337 
type prover = meta_simpset > thm > thm option; 

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

1339 
type conv = meta_simpset > termrec > termrec; 

1340 

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

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

1342 

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

1343 
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

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

1345 

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

1346 
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

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

1348 

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

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

1350 

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

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

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

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

1354 
 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

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

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

1357 

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

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

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

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

1361 
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

1362 
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

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

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

1365 

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

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

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

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

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

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

1371 
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

1372 
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

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

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

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

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

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

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

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

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

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

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

1383 

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