author  paulson 
Fri, 08 Dec 1995 10:39:52 +0100  
changeset 1394  a1d2735f5ade 
parent 1258  2a2d8c74a756 
child 1416  f59857e32972 
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 

1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

30 
val read_cterms : Sign.sg > string list * typ list > cterm list 
1238  31 
val cterm_fun : (term > term) > (cterm > cterm) 
32 
val dest_cimplies : cterm > cterm * cterm 

33 
val read_def_cterm : 

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

36 

37 
(*meta theorems*) 

38 
type thm 

39 
exception THM of string * int * thm list 

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

44 
val prems_of : thm > term list 

45 
val nprems_of : thm > int 

46 
val concl_of : thm > term 

47 
val cprop_of : thm > cterm 

48 
val extra_shyps : thm > sort list 

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

50 
val strip_shyps : thm > thm 

51 
val implies_intr_shyps: thm > thm 

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

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

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

1160  55 

56 
(*theories*) 

57 
type theory 

58 
exception THEORY of string * theory list 

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

63 
val stamps_of_thy : theory > string ref list 

64 
val parents_of : theory > theory list 

65 
val subthy : theory * theory > bool 

66 
val eq_thy : theory * theory > bool 

67 
val get_axiom : theory > string > thm 

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

69 
val proto_pure_thy : theory 

70 
val pure_thy : theory 

71 
val cpure_thy : theory 

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

75 
val add_defsort : sort > theory > theory 

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

77 
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

78 
> theory > theory 
1238  79 
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

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

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

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

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

86 
val add_trfuns : 

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

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

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

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

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

95 
val add_thyname : string > theory > theory 

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

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

1160  99 

100 
(*meta rules*) 

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

103 
val implies_elim : thm > thm > thm 

104 
val forall_intr : cterm > thm > thm 

105 
val forall_elim : cterm > thm > thm 

106 
val flexpair_def : thm 

107 
val reflexive : cterm > thm 

108 
val symmetric : thm > thm 

109 
val transitive : thm > thm > thm 

110 
val beta_conversion : cterm > thm 

111 
val extensional : thm > thm 

112 
val abstract_rule : string > cterm > thm > thm 

113 
val combination : thm > thm > thm 

114 
val equal_intr : thm > thm > thm 

115 
val equal_elim : thm > thm > thm 

116 
val implies_intr_hyps : thm > thm 

117 
val flexflex_rule : thm > thm Sequence.seq 

118 
val instantiate : 

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

122 
val varifyT : thm > thm 

123 
val freezeT : thm > thm 

124 
val dest_state : thm * int > 

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

128 
val eq_assumption : int > thm > thm 

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

135 
(*meta simplification*) 

136 
type meta_simpset 

137 
exception SIMPLIFIER of string * thm 

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

140 
val del_simps : meta_simpset * thm list > meta_simpset 

141 
val mss_of : thm list > meta_simpset 

142 
val add_congs : meta_simpset * thm list > meta_simpset 

143 
val add_prems : meta_simpset * thm list > meta_simpset 

144 
val prems_of_mss : meta_simpset > thm list 

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

146 
val mk_rews_of_mss : meta_simpset > thm > thm list 

147 
val trace_simp : bool ref 

148 
val rewrite_cterm : bool * bool > meta_simpset > 

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

250  152 
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

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

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

158 
structure Sign = Unify.Sign; 

159 
structure Type = Sign.Type; 

160 
structure Syntax = Sign.Syntax; 

161 
structure Symtab = Sign.Symtab; 

162 

163 

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

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

165 

250  166 
(** certified types **) 
167 

168 
(*certified typs under a signature*) 

169 

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

171 

172 
fun rep_ctyp (Ctyp args) = args; 

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

174 

175 
fun ctyp_of sign T = 

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

177 

178 
fun read_ctyp sign s = 

179 
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

180 

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

181 

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

182 

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

184 

250  185 
(*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

186 

250  187 
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

188 

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

189 
fun rep_cterm (Cterm args) = args; 
250  190 
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

191 

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

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

1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

195 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

196 
end; 
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' 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

220 
handle TYPE arg => error (Sign.exn_type_msg sign arg) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

223 

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

224 
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

225 

1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

226 
(*read a list of terms, matching them against a list of expected types. 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

227 
NO disambiguation of alternative parses via typechecking  it is just 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

228 
not practical.*) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

229 
fun read_cterms sign (bs, Ts) = 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

230 
let 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

231 
val {tsig, syn, ...} = Sign.rep_sg sign 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

232 
fun read (b,T) = 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

233 
case Syntax.read syn T b of 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

234 
[t] => t 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

235 
 _ => error("Error or ambiguity in parsing of " ^ b) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

236 
val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

237 
K None, K None, 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

238 
[], true, 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

239 
map (Sign.certify_typ sign) Ts, 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

240 
map read (bs~~Ts)) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

241 
in map (cterm_of sign) us end 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

242 
handle TYPE arg => error (Sign.exn_type_msg sign arg) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

243 
 TERM (msg, _) => error msg; 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

244 

250  245 

246 

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

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

248 

1238  249 
(* FIXME comment *) 
0  250 
datatype thm = Thm of 
1220  251 
{sign: Sign.sg, maxidx: int, 
252 
shyps: sort list, hyps: term list, prop: term}; 

0  253 

250  254 
fun rep_thm (Thm args) = args; 
0  255 

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

256 
(*errors involving theorems*) 
0  257 
exception THM of string * int * thm list; 
258 

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

259 

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

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

261 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  262 

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

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

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

265 
Sign.merge (pairself sign_of_thm (th1, th2)) 
574  266 
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

267 

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

268 

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

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

270 
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

271 

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

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

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

274 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  275 

276 
(*counts premises in a rule*) 

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

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

278 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  279 

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

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

281 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  282 

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

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

285 
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

286 

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

287 

0  288 

1238  289 
(** sort contexts of theorems **) 
290 

291 
(* basic utils *) 

292 

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

294 
to improve efficiency a bit*) 

295 

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

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

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

299 
and add_typs_sorts ([], Ss) = Ss 

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

301 

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

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

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

305 
 add_term_sorts (Bound _, Ss) = Ss 

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

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

308 

309 
fun add_terms_sorts ([], Ss) = Ss 

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

311 

1258  312 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
313 

314 
fun add_env_sorts (env, Ss) = 

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

316 
add_typs_sorts (env_codT env, Ss)); 

317 

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

320 

321 
fun add_thms_shyps ([], Ss) = Ss 

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

323 
add_thms_shyps (ths, shyps union Ss); 

324 

325 

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

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

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

329 

330 

331 
(* fix_shyps *) 

332 

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

334 
fun fix_shyps thms Ts thm = 

335 
let 

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

337 
val shyps = 

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

339 
in 

340 
Thm {sign = sign, maxidx = maxidx, 

341 
shyps = shyps, hyps = hyps, prop = prop} 

342 
end; 

343 

344 

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

346 

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

348 

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

350 
fun strip_shyps thm = 

351 
let 

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

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

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

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

356 
in 

357 
Thm {sign = sign, maxidx = maxidx, 

358 
shyps = 

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

360 
else (* FIXME tmp *) 

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

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

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

364 
sorts)), 

365 
hyps = hyps, prop = prop} 

366 
end; 

367 

368 

369 
(* implies_intr_shyps *) 

370 

371 
(*discharge all extra sort hypotheses*) 

372 
fun implies_intr_shyps thm = 

373 
(case extra_shyps thm of 

374 
[] => thm 

375 
 xshyps => 

376 
let 

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

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

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

380 
val names = 

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

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

383 

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

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

386 
in 

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

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

389 
end); 

390 

391 

392 

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

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

394 

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

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

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

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

399 
parents: theory list}; 
0  400 

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

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

402 

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

403 
(*errors involving theories*) 
0  404 
exception THEORY of string * theory list; 
405 

406 

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

407 
val sign_of = #sign o rep_theory; 
0  408 
val syn_of = #syn o Sign.rep_sg o sign_of; 
409 

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

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

411 
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

412 

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

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

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

415 

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

416 

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

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

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

419 
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

420 

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

421 

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

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

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

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

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

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

427 
(case Symtab.lookup (new_axioms, name) of 
1238  428 
Some t => fix_shyps [] [] 
429 
(Thm {sign = sign, maxidx = maxidx_of_term t, 

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

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

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

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

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

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

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

436 

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

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

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

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

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

441 

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

442 

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

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

444 

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

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

446 
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

447 

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

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

449 
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

450 

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

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

452 
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

453 

0  454 

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

455 

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

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

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

460 

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

461 
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

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

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

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

465 
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

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

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

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

469 
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

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

471 

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

472 

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

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

474 

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

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

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

477 

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

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

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

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

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

483 
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

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

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

486 
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

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

488 
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

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

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

492 
val add_thyname = ext_sg Sign.add_name; 
0  493 

494 

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

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

496 

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

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

498 
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

499 

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

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

501 
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

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

503 

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

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

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

506 
val Cterm {t, T, ...} = cterm_of sg raw_tm 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

507 
handle TYPE arg => error (Sign.exn_type_msg sg arg) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

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

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

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

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

513 
handle ERROR => err_in_axm name; 
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 
fun read_axm sg (name, str) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

518 

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

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

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

523 
handle ERROR => err_in_axm name; 
564  524 

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

525 

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

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

527 

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

528 
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

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

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

531 
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

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

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

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

535 

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

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

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

538 

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

539 

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

542 

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

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

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

545 
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

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

547 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

561 

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

562 
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

563 

0  564 

565 

1220  566 
(*** Meta rules ***) 
567 

568 
(** 'primitive' rules **) 

569 

570 
(*discharge all assumptions t from ts*) 

0  571 
val disch = gen_rem (op aconv); 
572 

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

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

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

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

0  583 
end; 
584 

1220  585 
(*Implication introduction 
586 
A  B 

587 
 

588 
A ==> B 

589 
*) 

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

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

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

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

599 
end; 

600 

1220  601 
(*Implication elimination 
602 
A ==> B A 

603 
 

604 
B 

605 
*) 

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

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

0  610 
in case prop of 
250  611 
imp$A$B => 
612 
if imp=implies andalso A aconv propA 

1220  613 
then fix_shyps [thAB, thA] [] 
614 
(Thm{sign= merge_thm_sgs(thAB,thA), 

250  615 
maxidx= max[maxA,maxidx], 
1220  616 
shyps= [], 
250  617 
hyps= hypsA union hyps, (*dups suppressed*) 
1220  618 
prop= B}) 
250  619 
else err("major premise") 
620 
 _ => err("major premise") 

0  621 
end; 
250  622 

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

625 
 

626 
!!x.A 

627 
*) 

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

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

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

0  633 
in case x of 
250  634 
Free(a,T) => 
635 
if exists (apl(x, Logic.occs)) hyps 

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

637 
else result(a,T) 

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

640 
end; 

641 

1220  642 
(*Forall elimination 
643 
!!x.A 

644 
 

645 
A[t/x] 

646 
*) 

647 
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

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

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

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

250  655 
maxidx= max[maxidx, maxt], 
1220  656 
shyps= [], hyps= hyps, prop= betapply(A,t)}) 
250  657 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  658 
end 
659 
handle TERM _ => 

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

662 

1220  663 
(* Equality *) 
0  664 

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

668 
prop= term_of (read_cterm Sign.proto_pure 

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

0  670 

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

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

673 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  674 
in fix_shyps [] [] 
675 
(Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, 

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

0  677 
end; 
678 

679 
(*The symmetry rule 

1220  680 
t==u 
681 
 

682 
u==t 

683 
*) 

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

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

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

0  689 
 _ => raise THM("symmetric", 0, [th]); 
690 

691 
(*The transitive rule 

1220  692 
t1==u u==t2 
693 
 

694 
t1==t2 

695 
*) 

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

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

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

700 
in case (prop1,prop2) of 

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

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

705 
hyps= hyps1 union hyps2, 

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

0  707 
 _ => err"premises" 
708 
end; 

709 

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

712 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  713 
in case t of 
1238  714 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
715 
(Thm{sign= sign, shyps= [], hyps= [], 

250  716 
maxidx= maxidx_of_term t, 
1238  717 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))}) 
250  718 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  719 
end; 
720 

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

1220  722 
f(x) == g(x) 
723 
 

724 
f == g 

725 
*) 

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

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

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

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

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

735 
 Var _ => 

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

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

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

1238  739 
(*no fix_shyps*) 
1220  740 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, 
250  741 
prop= Logic.mk_equals(f,g)} 
0  742 
end 
743 
 _ => raise THM("extensional: premise", 0, [th]); 

744 

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

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

1220  747 
t == u 
748 
 

749 
%x.t == %x.u 

750 
*) 

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

752 
let val x = term_of cx; 
250  753 
val (t,u) = Logic.dest_equals prop 
754 
handle TERM _ => 

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

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

250  758 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
1238  759 
Abs(a, T, abstract_over (x,u)))}) 
0  760 
in case x of 
250  761 
Free(_,T) => 
762 
if exists (apl(x, Logic.occs)) hyps 

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

764 
else result T 

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

767 
end; 

768 

769 
(*The combination rule 

1220  770 
f==g t==u 
771 
 

772 
f(t)==g(u) 

773 
*) 

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

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

1238  779 
(*no fix_shyps*) 
1220  780 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
781 
hyps= hyps1 union hyps2, 

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

785 

786 

787 
(*The equal propositions rule 

1220  788 
A==B A 
789 
 

790 
B 

791 
*) 

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

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

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

796 
in case prop1 of 

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

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

801 
hyps= hyps1 union hyps2, 

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

0  803 
 _ => err"major premise" 
804 
end; 

805 

806 

807 
(* Equality introduction 

1220  808 
A==>B B==>A 
809 
 

810 
A==B 

811 
*) 

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

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

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

250  818 
if A aconv A' andalso B aconv B' 
1238  819 
then 
820 
(*no fix_shyps*) 

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

822 
hyps= hyps1 union hyps2, 

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

250  824 
else err"not equal" 
0  825 
 _ => err"premises" 
826 
end; 

827 

1220  828 

829 

0  830 
(**** Derived rules ****) 
831 

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

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

1220  834 
fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = 
1238  835 
implies_intr_hyps (*no fix_shyps*) 
1220  836 
(Thm{sign=sign, maxidx=maxidx, shyps=shyps, 
250  837 
hyps= disch(As,A), prop= implies$A$prop}) 
0  838 
 implies_intr_hyps th = th; 
839 

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

250  841 
Instantiates the theorem and deletes trivial tpairs. 
0  842 
Resulting sequence may contain multiple elements if the tpairs are 
843 
not all flexflex. *) 

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

847 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

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

853 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  854 
end; 
0  855 
val (tpairs,_) = Logic.strip_flexpairs prop 
856 
in Sequence.maps newthm 

250  857 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  858 
end; 
859 

860 
(*Instantiation of Vars 

1220  861 
A 
862 
 

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

864 
*) 

0  865 

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

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

868 

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

870 
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

871 
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

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

875 
end; 

876 

877 
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

878 
let val {T,sign} = rep_ctyp ctyp 
0  879 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
880 

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

882 
Instantiates distinct Vars by terms of same type. 

883 
Normalizes the new theorem! *) 

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

250  887 
val newprop = 
888 
Envir.norm_term (Envir.empty 0) 

889 
(subst_atomic tpairs 

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

1220  891 
val newth = 
892 
fix_shyps [th] (map snd vTs) 

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

894 
maxidx= maxidx_of_term newprop, prop= newprop}) 

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

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

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

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

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

903 
 [] => 

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

905 
ix::_ => raise THM 

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

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

193  908 
 [] => newth 
0  909 
end 
250  910 
handle TERM _ => 
0  911 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  912 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  913 

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

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

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

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

1238  920 
else fix_shyps [] [] 
921 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], 

922 
prop= implies$A$A}) 

0  923 
end; 
924 

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

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

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

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

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

931 
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

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

933 
in 
1238  934 
fix_shyps [] [] 
935 
(Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}) 

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

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

937 

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

938 

0  939 
(* Replace all TFrees not in the hyps by new TVars *) 
1220  940 
fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) = 
0  941 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1238  942 
in (*no fix_shyps*) 
943 
Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps, 

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

0  945 
end; 
946 

947 
(* Replace all TVars by new TFrees *) 

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

949 
let val prop' = Type.freeze prop 
1238  950 
in (*no fix_shyps*) 
951 
Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, 

952 
prop=prop'} 

1220  953 
end; 
0  954 

955 

956 
(*** Inference rules for tactics ***) 

957 

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

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

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

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

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

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

964 
end 

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

966 

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

1238  970 
let val Thm{shyps=sshyps,prop=sprop,maxidx=smax,...} = state; 
0  971 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 
250  972 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  973 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
1238  974 
val (Thm{sign,maxidx,shyps,hyps,prop}) = orule 
0  975 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  976 
in (*no fix_shyps*) 
977 
Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 

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

250  979 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 
1238  980 
map lift_all As, lift_all B)} 
0  981 
end; 
982 

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

984 
fun assumption i state = 

1220  985 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  986 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  987 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  988 
fix_shyps [state] (env_codT env) 
989 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

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

992 
else (*normalize the new rule fully*) 

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

996 
(Sequence.mapp newth 

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

0  999 
in addprfs (Logic.assum_pairs Bi) end; 
1000 

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

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

1220  1007 
then fix_shyps [state] [] 
1008 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, 

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

0  1010 
else raise THM("eq_assumption", 0, [state]) 
1011 
end; 

1012 

1013 

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

1015 

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

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

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

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

1020 
fun rename_params_rule (cs, i) state = 

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

1024 
val short = length iparams  length cs 

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

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

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

250  1030 
in 
0  1031 
case findrep cs of 
1032 
c::_ => error ("Bound variables not distinct: " ^ c) 

1033 
 [] => (case cs inter freenames of 

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

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

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

0  1038 
end; 
1039 

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

1041 

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

1045 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1046 
else (x,y)::al) 
0  1047 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1048 
 match_bvs(_,_,al) = al; 

1049 

1050 
(* strip abstractions created by parameters *) 

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

1052 

1053 

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

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

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

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

1061 
 strip(A,_) = f A 

0  1062 
in strip end; 
1063 

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

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

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

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

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

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

1071 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1074 
(case assoc(al,x) of 

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

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

1077 
 None=> t) 

0  1078 
 rename(Abs(x,T,t)) = 
250  1079 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1080 
T, rename t) 

0  1081 
 rename(f$t) = rename f $ rename t 
1082 
 rename(t) = t; 

250  1083 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1084 
in strip_ren end; 
1085 

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

1087 
fun rename_bvars(dpairs, tpairs, B) = 

250  1088 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1089 

1090 

1091 
(*** RESOLUTION ***) 

1092 

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

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

1094 

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

250  1097 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1098 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1099 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1100 
Const("all",_)$Abs(_,_,t2)) = 
0  1101 
let val (B1,B2) = strip_assums2 (t1,t2) 
1102 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1103 
 strip_assums2 BB = BB; 

1104 

1105 

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

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

1107 
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

1108 
 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

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

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

1113 
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

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

1116 
 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

1117 

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

1118 

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

1123 
If eres_flg then simultaneously proves A1 by assumption. 

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

1127 
local open Sequence; exception Bicompose 

1128 
in 

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

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

1135 
if eres_flg then ~1 else 0) 

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

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

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

1141 
val normp = 

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

1143 
else 

1144 
let val ntps = map (pairself normt) tpairs 

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

1147 
if lifted 

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

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

250  1150 
else if match then raise Bicompose 
1151 
else (*normalize the new rule fully*) 

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

1153 
end 

1258  1154 
val th = (*tuned fix_shyps*) 
1155 
Thm{sign=sign, 

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

1157 
hyps=rhyps union shyps, 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1185 
(*ordinary resolution*) 

1186 
fun res(None) = null 

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

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

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

1192 
end; 

1193 
end; (*open Sequence*) 

1194 

1195 

1196 
fun bicompose match arg i state = 

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

1198 

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

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

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

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

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

1205 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1206 
end; 
1207 

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

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

250  1210 
fun biresolution match brules i state = 
0  1211 
let val lift = lift_rule(state, i); 
250  1212 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1213 
val B = Logic.strip_assums_concl Bi; 

1214 
val Hs = Logic.strip_assums_hyp Bi; 

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

1216 
fun res [] = Sequence.null 

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

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

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

1222 
else res brules 

0  1223 
in Sequence.flats (res brules) end; 
1224 

1225 

1226 

1227 
(*** Meta simp sets ***) 

1228 

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

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

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

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

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

1236 
net: discrimination net of rewrite rules 

1237 
congs: association list of congruence rules 

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

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

1239 
for generating new names when rewriting under lambda abstractions 
0  1240 
mk_rews: used when local assumptions are added 
1241 
*) 

1242 

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

1243 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1244 
mk_rews = K[]}; 
1245 

1246 
exception SIMPLIFIER of string * thm; 

1247 

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

1248 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1249 

209  1250 
val trace_simp = ref false; 
1251 

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

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

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

1255 

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

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

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

1258 
 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

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

1260 

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

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

1262 
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

1263 

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

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

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

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

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

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

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

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

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

1276 
*) 

0  1277 

1238  1278 
fun mk_rrule raw_thm = 
1279 
let 

1258  1280 
val thm = strip_shyps raw_thm; 
1238  1281 
val Thm{sign,prop,maxidx,...} = thm; 
1282 
val prems = Logic.strip_imp_prems prop 

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

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

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

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

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

1288 
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

1289 
andalso not(is_Var(elhs)) 
1220  1290 
in 
1258  1291 
if not perm andalso loops sign prems (elhs,erhs) then 
1220  1292 
(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

1293 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1294 
end; 
1295 

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

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

1299 
in 

1300 

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

1301 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1302 
thm as Thm{sign,prop,...}) = 
87  1303 
case mk_rrule thm of 
1304 
None => mss 

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

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

1308 
handle Net.INSERT => 

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

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

1311 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1312 

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

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

1316 
None => mss 

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

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

1319 
handle Net.INSERT => 

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

1321 
net)), 

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

1322 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1323 

1324 
end; 

0  1325 

1326 
val add_simps = foldl add_simp; 

87  1327 
val del_simps = foldl del_simp; 
0  1328 

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

1330 

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

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

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

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

1337 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1338 
prems=prems, mk_rews=mk_rews} 
1339 
end; 

1340 

1341 
val (op add_congs) = foldl add_cong; 

1342 

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

1343 
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

1344 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1345 

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

1347 

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

1348 
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

1349 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1350 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1351 

1352 

250  1353 
(*** Metalevel rewriting 
0  1354 
uses conversions, omitting proofs for efficiency. See 
250  1355 
L C Paulson, A higherorder implementation of rewriting, 
1356 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1357 

1358 
type prover = meta_simpset > thm > thm option; 

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

1360 
type conv = meta_simpset > termrec > termrec; 

1361 

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

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

1363 

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

1364 
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

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

1366 

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

1367 
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

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

1369 

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

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

1371 

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

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

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

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

1375 
 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

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

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

1378 

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

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

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

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

1382 
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

1383 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and </ 