author  paulson 
Fri, 01 Mar 1996 10:19:51 +0100  
changeset 1529  09d9ad015269 
parent 1517  d2f865740d8e 
child 1539  f21c8fab7c3c 
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 
1529  7 
theorems, meta rules (including resolution and simplification). 
0  8 
*) 
9 

250  10 
signature THM = 
1503  11 
sig 
1160  12 
(*certified types*) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

13 
type ctyp 
1238  14 
val rep_ctyp : ctyp > {sign: Sign.sg, T: typ} 
15 
val typ_of : ctyp > typ 

16 
val ctyp_of : Sign.sg > typ > ctyp 

17 
val read_ctyp : Sign.sg > string > ctyp 

1160  18 

19 
(*certified terms*) 

20 
type cterm 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

21 
exception CTERM of string 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

22 
val rep_cterm : cterm > {sign: Sign.sg, t: term, T: typ, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

23 
maxidx: int} 
1238  24 
val term_of : cterm > term 
25 
val cterm_of : Sign.sg > term > cterm 

26 
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

27 
val read_cterms : Sign.sg > string list * typ list > cterm list 
1238  28 
val cterm_fun : (term > term) > (cterm > cterm) 
29 
val dest_cimplies : cterm > cterm * cterm 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

30 
val dest_comb : cterm > cterm * cterm 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

31 
val dest_abs : cterm > cterm * cterm 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

32 
val capply : cterm > cterm > cterm 
1517  33 
val cabs : cterm > cterm > cterm 
1238  34 
val read_def_cterm : 
1160  35 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
36 
string list > bool > string * typ > cterm * (indexname * typ) list 

37 

1529  38 
(*theories*) 
39 

40 
(*proof terms [must duplicate declaration as a specification]*) 

41 
val full_deriv : bool ref 

42 
datatype rule = 

43 
MinProof 

44 
 Axiom of theory * string 

45 
 Theorem of theory * string 

46 
 Assume of cterm 

47 
 Implies_intr of cterm 

48 
 Implies_intr_shyps 

49 
 Implies_intr_hyps 

50 
 Implies_elim 

51 
 Forall_intr of cterm 

52 
 Forall_elim of cterm 

53 
 Reflexive of cterm 

54 
 Symmetric 

55 
 Transitive 

56 
 Beta_conversion of cterm 

57 
 Extensional 

58 
 Abstract_rule of string * cterm 

59 
 Combination 

60 
 Equal_intr 

61 
 Equal_elim 

62 
 Trivial of cterm 

63 
 Lift_rule of cterm * int 

64 
 Assumption of int * Envir.env option 

65 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 

66 
 Bicompose of bool * bool * int * int * Envir.env 

67 
 Flexflex_rule of Envir.env 

68 
 Class_triv of theory * class 

69 
 VarifyT 

70 
 FreezeT 

71 
 RewriteC of cterm 

72 
 CongC of cterm 

73 
 Rewrite_cterm of cterm 

74 
 Rename_params_rule of string list * int; 

75 

76 
datatype deriv = Infer of rule * deriv list 

77 
 Oracle of string * exn ; 

78 

1160  79 
(*meta theorems*) 
80 
type thm 

81 
exception THM of string * int * thm list 

1529  82 
val rep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 
83 
shyps: sort list, hyps: term list, 

84 
prop: term} 

85 
val crep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 

86 
shyps: sort list, hyps: cterm list, 

87 
prop: cterm} 

1238  88 
val stamps_of_thm : thm > string ref list 
89 
val tpairs_of : thm > (term * term) list 

90 
val prems_of : thm > term list 

91 
val nprems_of : thm > int 

92 
val concl_of : thm > term 

93 
val cprop_of : thm > cterm 

94 
val extra_shyps : thm > sort list 

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

96 
val strip_shyps : thm > thm 

97 
val implies_intr_shyps: thm > thm 

98 
val get_axiom : theory > string > thm 

1529  99 
val name_thm : theory * string * thm > thm 
1238  100 
val axioms_of : theory > (string * thm) list 
1160  101 

102 
(*meta rules*) 

1238  103 
val assume : cterm > thm 
1416  104 
val compress : thm > thm 
1238  105 
val implies_intr : cterm > thm > thm 
106 
val implies_elim : thm > thm > thm 

107 
val forall_intr : cterm > thm > thm 

108 
val forall_elim : cterm > thm > thm 

109 
val flexpair_def : thm 

110 
val reflexive : cterm > thm 

111 
val symmetric : thm > thm 

112 
val transitive : thm > thm > thm 

113 
val beta_conversion : cterm > thm 

114 
val extensional : thm > thm 

115 
val abstract_rule : string > cterm > thm > thm 

116 
val combination : thm > thm > thm 

117 
val equal_intr : thm > thm > thm 

118 
val equal_elim : thm > thm > thm 

119 
val implies_intr_hyps : thm > thm 

120 
val flexflex_rule : thm > thm Sequence.seq 

121 
val instantiate : 

1160  122 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 
1238  123 
val trivial : cterm > thm 
124 
val class_triv : theory > class > thm 

125 
val varifyT : thm > thm 

126 
val freezeT : thm > thm 

127 
val dest_state : thm * int > 

1160  128 
(term * term) list * term list * term * term 
1238  129 
val lift_rule : (thm * int) > thm > thm 
130 
val assumption : int > thm > thm Sequence.seq 

131 
val eq_assumption : int > thm > thm 

1160  132 
val rename_params_rule: string list * int > thm > thm 
1238  133 
val bicompose : bool > bool * thm * int > 
1160  134 
int > thm > thm Sequence.seq 
1238  135 
val biresolution : bool > (bool * thm) list > 
1160  136 
int > thm > thm Sequence.seq 
137 

138 
(*meta simplification*) 

139 
type meta_simpset 

140 
exception SIMPLIFIER of string * thm 

1238  141 
val empty_mss : meta_simpset 
142 
val add_simps : meta_simpset * thm list > meta_simpset 

143 
val del_simps : meta_simpset * thm list > meta_simpset 

144 
val mss_of : thm list > meta_simpset 

145 
val add_congs : meta_simpset * thm list > meta_simpset 

146 
val add_prems : meta_simpset * thm list > meta_simpset 

147 
val prems_of_mss : meta_simpset > thm list 

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

149 
val mk_rews_of_mss : meta_simpset > thm > thm list 

150 
val trace_simp : bool ref 

151 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  152 
(meta_simpset > thm > thm option) > cterm > thm 
250  153 
end; 
0  154 

1503  155 
structure Thm : THM = 
0  156 
struct 
250  157 

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

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

159 

250  160 
(** certified types **) 
161 

162 
(*certified typs under a signature*) 

163 

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

165 

166 
fun rep_ctyp (Ctyp args) = args; 

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

168 

169 
fun ctyp_of sign T = 

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

171 

172 
fun read_ctyp sign s = 

173 
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

174 

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

175 

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

176 

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

178 

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

180 

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

182 

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

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

185 

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

188 
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

189 
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

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

191 

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

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

194 

250  195 
(*dest_implies for cterms. Note T=prop below*) 
196 
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

197 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  198 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
199 
 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

200 

1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

201 
exception CTERM of string; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

202 

e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

203 
(*Destruct application in cterms*) 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

204 
fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) = 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

205 
let val typeA = fastype_of A; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

206 
val typeB = 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

207 
case typeA of Type("fun",[S,T]) => S 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

208 
 _ => error "Function type expected in dest_comb"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

209 
in 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

210 
(Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA}, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

211 
Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB}) 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

212 
end 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

213 
 dest_comb _ = raise CTERM "dest_comb"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

214 

e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

215 
(*Destruct abstraction in cterms*) 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

216 
fun dest_abs (Cterm {sign, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

217 
let val (y,N) = variant_abs (x,ty,M) 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

218 
in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)}, 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

219 
Cterm {sign = sign, T = S, maxidx = maxidx, t = N}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

220 
end 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

221 
 dest_abs _ = raise CTERM "dest_abs"; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

222 

1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

223 
(*Form cterm out of a function and an argument*) 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

224 
fun capply (Cterm {t=f, sign=sign1, T=Type("fun",[dty,rty]), maxidx=maxidx1}) 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

225 
(Cterm {t=x, sign=sign2, T, maxidx=maxidx2}) = 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

226 
if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty, 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

227 
maxidx=max[maxidx1, maxidx2]} 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

228 
else raise CTERM "capply: types don't agree" 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

229 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  230 

1517  231 
fun cabs (Cterm {t=Free(a,ty), sign=sign1, T=T1, maxidx=maxidx1}) 
232 
(Cterm {t=t2, sign=sign2, T=T2, maxidx=maxidx2}) = 

233 
Cterm {t=absfree(a,ty,t2), sign=Sign.merge(sign1,sign2), 

234 
T = ty > T2, maxidx=max[maxidx1, maxidx2]} 

235 
 cabs _ _ = raise CTERM "cabs: first arg is not a free variable"; 

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

236 

574  237 
(** read cterms **) (*exception ERROR*) 
250  238 

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

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

240 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  241 
let 
574  242 
val T' = Sign.certify_typ sign T 
243 
handle TYPE (msg, _, _) => error msg; 

623  244 
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

245 
val (_, t', tye) = 
959  246 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  247 
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

248 
handle TYPE arg => error (Sign.exn_type_msg sign arg) 
1460  249 
 TERM (msg, _) => error msg; 
250  250 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

251 

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

252 
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

253 

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

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

255 
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

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

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

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

259 
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

260 
fun read (b,T) = 
1460  261 
case Syntax.read syn T b of 
262 
[t] => t 

263 
 _ => error("Error or ambiguity in parsing of " ^ b) 

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

264 
val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
1460  265 
K None, K None, 
266 
[], true, 

267 
map (Sign.certify_typ sign) Ts, 

268 
map read (bs~~Ts)) 

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

269 
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

270 
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

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

272 

250  273 

274 

1529  275 
(*** Derivations ***) 
276 

277 
(*Names of rules in derivations. Includes logically trivial rules, if 

278 
executed in ML.*) 

279 
datatype rule = 

280 
MinProof (*for building minimal proof terms*) 

281 
(*Axioms/theorems*) 

282 
 Axiom of theory * string 

283 
 Theorem of theory * string (*via theorem db*) 

284 
(*primitive inferences and compound versions of them*) 

285 
 Assume of cterm 

286 
 Implies_intr of cterm 

287 
 Implies_intr_shyps 

288 
 Implies_intr_hyps 

289 
 Implies_elim 

290 
 Forall_intr of cterm 

291 
 Forall_elim of cterm 

292 
 Reflexive of cterm 

293 
 Symmetric 

294 
 Transitive 

295 
 Beta_conversion of cterm 

296 
 Extensional 

297 
 Abstract_rule of string * cterm 

298 
 Combination 

299 
 Equal_intr 

300 
 Equal_elim 

301 
(*derived rules for tactical proof*) 

302 
 Trivial of cterm 

303 
(*For lift_rule, the proof state is not a premise. 

304 
Use cterm instead of thm to avoid mutual recursion.*) 

305 
 Lift_rule of cterm * int 

306 
 Assumption of int * Envir.env option (*includes eq_assumption*) 

307 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 

308 
 Bicompose of bool * bool * int * int * Envir.env 

309 
 Flexflex_rule of Envir.env (*identifies unifier chosen*) 

310 
(*other derived rules*) 

311 
 Class_triv of theory * class (*derived rule????*) 

312 
 VarifyT 

313 
 FreezeT 

314 
(*for the simplifier*) 

315 
 RewriteC of cterm 

316 
 CongC of cterm 

317 
 Rewrite_cterm of cterm 

318 
(*Logical identities, recorded since they are part of the proof process*) 

319 
 Rename_params_rule of string list * int; 

320 

321 

322 
datatype deriv = Infer of rule * deriv list 

323 
 Oracle of string * exn (*???*); 

324 

325 

326 
val full_deriv = ref false; 

327 

328 

329 
(*Suppress all atomic inferences, if using minimal derivations*) 

330 
fun squash_derivs (Infer (_, []) :: drvs) = squash_derivs drvs 

331 
 squash_derivs (der :: ders) = der :: squash_derivs ders 

332 
 squash_derivs [] = []; 

333 

334 
(*Ensure sharing of the most likely derivation, the empty one!*) 

335 
val min_infer = Infer (MinProof, []); 

336 

337 
(*Make a minimal inference*) 

338 
fun make_min_infer [] = min_infer 

339 
 make_min_infer [der] = der 

340 
 make_min_infer ders = Infer (MinProof, ders); 

341 

342 
fun infer_derivs (rl, []) = Infer (rl, []) 

343 
 infer_derivs (rl, ders) = 

344 
if !full_deriv then Infer (rl, ders) 

345 
else make_min_infer (squash_derivs ders); 

346 

347 

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

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

349 

0  350 
datatype thm = Thm of 
1460  351 
{sign: Sign.sg, (*signature for hyps and prop*) 
1529  352 
der: deriv, (*derivation*) 
1460  353 
maxidx: int, (*maximum index of any Var or TVar*) 
354 
shyps: sort list, (* FIXME comment *) 

355 
hyps: term list, (*hypotheses*) 

356 
prop: term}; (*conclusion*) 

0  357 

250  358 
fun rep_thm (Thm args) = args; 
0  359 

1529  360 
(*Version of rep_thm returning cterms instead of terms*) 
361 
fun crep_thm (Thm {sign, der, maxidx, shyps, hyps, prop}) = 

362 
let fun ctermf max t = Cterm{sign=sign, t=t, T=propT, maxidx=max}; 

363 
in {sign=sign, der=der, maxidx=maxidx, shyps=shyps, 

364 
hyps = map (ctermf ~1) hyps, 

365 
prop = ctermf maxidx prop} 

1517  366 
end; 
367 

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

368 
(*errors involving theorems*) 
0  369 
exception THM of string * int * thm list; 
370 

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

371 

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

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

373 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  374 

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

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

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

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

379 

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

380 

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

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

382 
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

383 

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

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

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

386 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  387 

388 
(*counts premises in a rule*) 

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

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

390 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  391 

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

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

393 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  394 

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

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

397 
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

398 

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

399 

0  400 

1238  401 
(** sort contexts of theorems **) 
402 

403 
(* basic utils *) 

404 

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

406 
to improve efficiency a bit*) 

407 

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

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

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

411 
and add_typs_sorts ([], Ss) = Ss 

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

413 

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

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

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

417 
 add_term_sorts (Bound _, Ss) = Ss 

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

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

420 

421 
fun add_terms_sorts ([], Ss) = Ss 

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

423 

1258  424 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
425 

426 
fun add_env_sorts (env, Ss) = 

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

428 
add_typs_sorts (env_codT env, Ss)); 

429 

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

432 

433 
fun add_thms_shyps ([], Ss) = Ss 

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

435 
add_thms_shyps (ths, shyps union Ss); 

436 

437 

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

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

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

441 

442 

443 
(* fix_shyps *) 

444 

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

446 
fun fix_shyps thms Ts thm = 

447 
let 

1529  448 
val Thm {sign, der, maxidx, hyps, prop, ...} = thm; 
1238  449 
val shyps = 
450 
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); 

451 
in 

1529  452 
Thm {sign = sign, 
453 
der = der, (*No new derivation, as other rules call this*) 

454 
maxidx = maxidx, 

455 
shyps = shyps, hyps = hyps, prop = prop} 

1238  456 
end; 
457 

458 

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

460 

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

462 

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

464 
fun strip_shyps thm = 

465 
let 

1529  466 
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; 
1238  467 
val sorts = add_thm_sorts (thm, []); 
468 
val maybe_empty = not o Sign.nonempty_sort sign sorts; 

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

470 
in 

1529  471 
Thm {sign = sign, der = der, maxidx = maxidx, 
472 
shyps = 

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

474 
else (* FIXME tmp *) 

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

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

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

1238  478 
sorts)), 
1529  479 
hyps = hyps, 
480 
prop = prop} 

1238  481 
end; 
482 

483 

484 
(* implies_intr_shyps *) 

485 

486 
(*discharge all extra sort hypotheses*) 

487 
fun implies_intr_shyps thm = 

488 
(case extra_shyps thm of 

489 
[] => thm 

490 
 xshyps => 

491 
let 

1529  492 
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; 
1238  493 
val shyps' = logicS ins (shyps \\ xshyps); 
494 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 

495 
val names = 

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

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

498 

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

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

501 
in 

1529  502 
Thm {sign = sign, 
503 
der = infer_derivs (Implies_intr_shyps, [der]), 

504 
maxidx = maxidx, 

505 
shyps = shyps', 

506 
hyps = hyps, 

507 
prop = Logic.list_implies (sort_hyps, prop)} 

1238  508 
end); 
509 

510 

1529  511 
(** Axioms **) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

512 

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

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

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

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

516 
fun get_ax [] = raise Match 
1529  517 
 get_ax (thy :: thys) = 
518 
let val {sign, new_axioms, parents} = rep_theory thy 

519 
in case Symtab.lookup (new_axioms, name) of 

520 
Some t => fix_shyps [] [] 

521 
(Thm {sign = sign, 

522 
der = infer_derivs (Axiom(theory,name), []), 

523 
maxidx = maxidx_of_term t, 

524 
shyps = [], 

525 
hyps = [], 

526 
prop = t}) 

527 
 None => get_ax parents handle Match => get_ax thys 

528 
end; 

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

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

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

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

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

533 

1529  534 

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

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

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

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

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

539 

1529  540 
fun name_thm (thy, name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
541 
if Sign.eq_sg (sign, sign_of thy) then 

542 
Thm {sign = sign, 

543 
der = Infer (Theorem(thy,name), []), 

544 
maxidx = maxidx, 

545 
shyps = shyps, 

546 
hyps = hyps, 

547 
prop = prop} 

548 
else raise THM ("name_thm", 0, [th]); 

0  549 

550 

1529  551 
(*Compression of theorems  a separate rule, not integrated with the others, 
552 
as it could be slow.*) 

553 
fun compress (Thm {sign, der, maxidx, shyps, hyps, prop}) = 

554 
Thm {sign = sign, 

555 
der = der, (*No derivation recorded!*) 

556 
maxidx = maxidx, 

557 
shyps = shyps, 

558 
hyps = map Term.compress_term hyps, 

559 
prop = Term.compress_term prop}; 

564  560 

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

561 

1529  562 
(*** Meta rules ***) 
0  563 

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

564 
(* check that term does not contain same var with different typing/sorting *) 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

565 
fun nodup_Vars(thm as Thm{prop,...}) s = 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

566 
Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]); 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

567 

1220  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, []) 

1529  581 
else Thm{sign = sign, 
582 
der = infer_derivs (Assume ct, []), 

583 
maxidx = ~1, 

584 
shyps = add_term_sorts(prop,[]), 

585 
hyps = [prop], 

586 
prop = prop} 

0  587 
end; 
588 

1220  589 
(*Implication introduction 
590 
A  B 

591 
 

592 
A ==> B 

593 
*) 

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

595 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  596 
in if T<>propT then 
250  597 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  598 
else fix_shyps [thB] [] 
1529  599 
(Thm{sign = Sign.merge (sign,signA), 
600 
der = infer_derivs (Implies_intr cA, [der]), 

601 
maxidx = max[maxidxA, maxidx], 

602 
shyps = [], 

603 
hyps = disch(hyps,A), 

604 
prop = implies$A$prop}) 

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

607 
end; 

608 

1529  609 

1220  610 
(*Implication elimination 
611 
A ==> B A 

612 
 

613 
B 

614 
*) 

0  615 
fun implies_elim thAB thA : thm = 
1529  616 
let val Thm{maxidx=maxA, der=derA, hyps=hypsA, prop=propA,...} = thA 
617 
and Thm{sign, der, maxidx, hyps, prop,...} = thAB; 

250  618 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 
0  619 
in case prop of 
250  620 
imp$A$B => 
621 
if imp=implies andalso A aconv propA 

1220  622 
then fix_shyps [thAB, thA] [] 
623 
(Thm{sign= merge_thm_sgs(thAB,thA), 

1529  624 
der = infer_derivs (Implies_elim, [der,derA]), 
625 
maxidx = max[maxA,maxidx], 

626 
shyps = [], 

627 
hyps = hypsA union hyps, (*dups suppressed*) 

628 
prop = B}) 

250  629 
else err("major premise") 
630 
 _ => err("major premise") 

0  631 
end; 
250  632 

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

635 
 

636 
!!x.A 

637 
*) 

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

639 
let val x = term_of cx; 
1238  640 
fun result(a,T) = fix_shyps [th] [] 
1529  641 
(Thm{sign = sign, 
642 
der = infer_derivs (Forall_intr cx, [der]), 

643 
maxidx = maxidx, 

644 
shyps = [], 

645 
hyps = hyps, 

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

0  647 
in case x of 
250  648 
Free(a,T) => 
649 
if exists (apl(x, Logic.occs)) hyps 

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

651 
else result(a,T) 

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

654 
end; 

655 

1220  656 
(*Forall elimination 
657 
!!x.A 

658 
 

659 
A[t/x] 

660 
*) 

1529  661 
fun forall_elim ct (th as Thm{sign,der,maxidx,hyps,prop,...}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

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

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

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

667 
else let val thm = fix_shyps [th] [] 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

668 
(Thm{sign= Sign.merge(sign,signt), 
1529  669 
der = infer_derivs (Forall_elim ct, [der]), 
670 
maxidx = max[maxidx, maxt], 

671 
shyps = [], 

672 
hyps = hyps, 

673 
prop = betapply(A,t)}) 

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

674 
in nodup_Vars thm "forall_elim"; thm end 
250  675 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  676 
end 
677 
handle TERM _ => 

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

680 

1220  681 
(* Equality *) 
0  682 

1220  683 
(* Definition of the relation =?= *) 
1238  684 
val flexpair_def = fix_shyps [] [] 
1529  685 
(Thm{sign= Sign.proto_pure, 
686 
der = Infer(Axiom(pure_thy, "flexpair_def"), []), 

687 
shyps = [], 

688 
hyps = [], 

689 
maxidx = 0, 

690 
prop = term_of (read_cterm Sign.proto_pure 

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

0  692 

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

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

695 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  696 
in fix_shyps [] [] 
1529  697 
(Thm{sign= sign, 
698 
der = infer_derivs (Reflexive ct, []), 

699 
shyps = [], 

700 
hyps = [], 

701 
maxidx = maxidx, 

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

0  703 
end; 
704 

705 
(*The symmetry rule 

1220  706 
t==u 
707 
 

708 
u==t 

709 
*) 

1529  710 
fun symmetric (th as Thm{sign,der,maxidx,shyps,hyps,prop}) = 
0  711 
case prop of 
712 
(eq as Const("==",_)) $ t $ u => 

1238  713 
(*no fix_shyps*) 
1529  714 
Thm{sign = sign, 
715 
der = infer_derivs (Symmetric, [der]), 

716 
maxidx = maxidx, 

717 
shyps = shyps, 

718 
hyps = hyps, 

719 
prop = eq$u$t} 

0  720 
 _ => raise THM("symmetric", 0, [th]); 
721 

722 
(*The transitive rule 

1220  723 
t1==u u==t2 
724 
 

725 
t1==t2 

726 
*) 

0  727 
fun transitive th1 th2 = 
1529  728 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 
729 
and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

0  730 
fun err(msg) = raise THM("transitive: "^msg, 0, [th1,th2]) 
731 
in case (prop1,prop2) of 

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

250  733 
if not (u aconv u') then err"middle term" else 
1220  734 
fix_shyps [th1, th2] [] 
1529  735 
(Thm{sign= merge_thm_sgs(th1,th2), 
736 
der = infer_derivs (Transitive, [der1, der2]), 

737 
maxidx = max[max1,max2], 

738 
shyps = [], 

739 
hyps = hyps1 union hyps2, 

740 
prop = eq$t1$t2}) 

0  741 
 _ => err"premises" 
742 
end; 

743 

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

746 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  747 
in case t of 
1238  748 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
1529  749 
(Thm{sign = sign, 
750 
der = infer_derivs (Beta_conversion ct, []), 

751 
maxidx = maxidx_of_term t, 

752 
shyps = [], 

753 
hyps = [], 

754 
prop = Logic.mk_equals(t, subst_bounds([u],bodt))}) 

250  755 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  756 
end; 
757 

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

1220  759 
f(x) == g(x) 
760 
 

761 
f == g 

762 
*) 

1529  763 
fun extensional (th as Thm{sign, der, maxidx,shyps,hyps,prop}) = 
0  764 
case prop of 
765 
(Const("==",_)) $ (f$x) $ (g$y) => 

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

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

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

772 
 Var _ => 

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

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

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

1238  776 
(*no fix_shyps*) 
1529  777 
Thm{sign = sign, 
778 
der = infer_derivs (Extensional, [der]), 

779 
maxidx = maxidx, 

780 
shyps = shyps, 

781 
hyps = hyps, 

782 
prop = Logic.mk_equals(f,g)} 

0  783 
end 
784 
 _ => raise THM("extensional: premise", 0, [th]); 

785 

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

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

1220  788 
t == u 
789 
 

790 
%x.t == %x.u 

791 
*) 

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

793 
let val x = term_of cx; 
250  794 
val (t,u) = Logic.dest_equals prop 
795 
handle TERM _ => 

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

1238  797 
fun result T = fix_shyps [th] [] 
1529  798 
(Thm{sign = sign, 
799 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

800 
maxidx = maxidx, 

801 
shyps = [], 

802 
hyps = hyps, 

803 
prop = Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 

804 
Abs(a, T, abstract_over (x,u)))}) 

0  805 
in case x of 
250  806 
Free(_,T) => 
807 
if exists (apl(x, Logic.occs)) hyps 

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

809 
else result T 

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

812 
end; 

813 

814 
(*The combination rule 

1220  815 
f==g t==u 
816 
 

817 
f(t)==g(u) 

818 
*) 

0  819 
fun combination th1 th2 = 
1529  820 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
821 
prop=prop1,...} = th1 

822 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 

823 
prop=prop2,...} = th2 

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

824 
in case (prop1,prop2) of 
0  825 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

826 
let val thm = (*no fix_shyps*) 
1529  827 
Thm{sign = merge_thm_sgs(th1,th2), 
828 
der = infer_derivs (Combination, [der1, der2]), 

829 
maxidx = max[max1,max2], 

830 
shyps = shyps1 union shyps2, 

831 
hyps = hyps1 union hyps2, 

832 
prop = Logic.mk_equals(f$t, g$u)} 

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

833 
in nodup_Vars thm "combination"; thm end 
0  834 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
835 
end; 

836 

837 

838 
(* Equality introduction 

1220  839 
A==>B B==>A 
840 
 

841 
A==B 

842 
*) 

0  843 
fun equal_intr th1 th2 = 
1529  844 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
845 
prop=prop1,...} = th1 

846 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 

847 
prop=prop2,...} = th2; 

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

849 
in case (prop1,prop2) of 

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

851 
if A aconv A' andalso B aconv B' 

852 
then 

853 
(*no fix_shyps*) 

854 
Thm{sign = merge_thm_sgs(th1,th2), 

855 
der = infer_derivs (Equal_intr, [der1, der2]), 

856 
maxidx = max[max1,max2], 

857 
shyps = shyps1 union shyps2, 

858 
hyps = hyps1 union hyps2, 

859 
prop = Logic.mk_equals(A,B)} 

860 
else err"not equal" 

861 
 _ => err"premises" 

862 
end; 

863 

864 

865 
(*The equal propositions rule 

866 
A==B A 

867 
 

868 
B 

869 
*) 

870 
fun equal_elim th1 th2 = 

871 
let val Thm{der=der1, maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

872 
and Thm{der=der2, maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

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

874 
in case prop1 of 

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

876 
if not (prop2 aconv A) then err"not equal" else 

877 
fix_shyps [th1, th2] [] 

878 
(Thm{sign= merge_thm_sgs(th1,th2), 

879 
der = infer_derivs (Equal_elim, [der1, der2]), 

880 
maxidx = max[max1,max2], 

881 
shyps = [], 

882 
hyps = hyps1 union hyps2, 

883 
prop = B}) 

884 
 _ => err"major premise" 

885 
end; 

0  886 

1220  887 

888 

0  889 
(**** Derived rules ****) 
890 

1503  891 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  892 
Repeated hypotheses are discharged only once; fold cannot do this*) 
1529  893 
fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = 
1238  894 
implies_intr_hyps (*no fix_shyps*) 
1529  895 
(Thm{sign = sign, 
896 
der = infer_derivs (Implies_intr_hyps, [der]), 

897 
maxidx = maxidx, 

898 
shyps = shyps, 

899 
hyps = disch(As,A), 

900 
prop = implies$A$prop}) 

0  901 
 implies_intr_hyps th = th; 
902 

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

250  904 
Instantiates the theorem and deletes trivial tpairs. 
0  905 
Resulting sequence may contain multiple elements if the tpairs are 
906 
not all flexflex. *) 

1529  907 
fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = 
250  908 
let fun newthm env = 
1529  909 
if Envir.is_empty env then th 
910 
else 

250  911 
let val (tpairs,horn) = 
912 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

1220  916 
in fix_shyps [th] (env_codT env) 
1529  917 
(Thm{sign = sign, 
918 
der = infer_derivs (Flexflex_rule env, [der]), 

919 
maxidx = maxidx_of_term newprop, 

920 
shyps = [], 

921 
hyps = hyps, 

922 
prop = newprop}) 

250  923 
end; 
0  924 
val (tpairs,_) = Logic.strip_flexpairs prop 
925 
in Sequence.maps newthm 

250  926 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  927 
end; 
928 

929 
(*Instantiation of Vars 

1220  930 
A 
931 
 

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

933 
*) 

0  934 

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

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

937 

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

939 
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

940 
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

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

944 
end; 

945 

946 
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

947 
let val {T,sign} = rep_ctyp ctyp 
0  948 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
949 

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

951 
Instantiates distinct Vars by terms of same type. 

952 
Normalizes the new theorem! *) 

1529  953 
fun instantiate ([], []) th = th 
954 
 instantiate (vcTs,ctpairs) (th as Thm{sign,der,maxidx,hyps,prop,...}) = 

0  955 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
956 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  957 
val newprop = 
958 
Envir.norm_term (Envir.empty 0) 

959 
(subst_atomic tpairs 

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

1220  961 
val newth = 
962 
fix_shyps [th] (map snd vTs) 

1529  963 
(Thm{sign = newsign, 
964 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 

965 
maxidx = maxidx_of_term newprop, 

966 
shyps = [], 

967 
hyps = hyps, 

968 
prop = newprop}) 

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

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

1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

973 
else nodup_Vars newth "instantiate"; 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

974 
newth 
0  975 
end 
250  976 
handle TERM _ => 
0  977 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  978 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  979 

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

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

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

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

1238  986 
else fix_shyps [] [] 
1529  987 
(Thm{sign = sign, 
988 
der = infer_derivs (Trivial ct, []), 

989 
maxidx = maxidx, 

990 
shyps = [], 

991 
hyps = [], 

992 
prop = implies$A$A}) 

0  993 
end; 
994 

1503  995 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)" *) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

996 
fun class_triv thy c = 
1529  997 
let val sign = sign_of thy; 
998 
val Cterm {t, maxidx, ...} = 

999 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 

1000 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 

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

1001 
in 
1238  1002 
fix_shyps [] [] 
1529  1003 
(Thm {sign = sign, 
1004 
der = infer_derivs (Class_triv(thy,c), []), 

1005 
maxidx = maxidx, 

1006 
shyps = [], 

1007 
hyps = [], 

1008 
prop = t}) 

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

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

1010 

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

1011 

0  1012 
(* Replace all TFrees not in the hyps by new TVars *) 
1529  1013 
fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
0  1014 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1238  1015 
in (*no fix_shyps*) 
1529  1016 
Thm{sign = sign, 
1017 
der = infer_derivs (VarifyT, [der]), 

1018 
maxidx = max[0,maxidx], 

1019 
shyps = shyps, 

1020 
hyps = hyps, 

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

0  1022 
end; 
1023 

1024 
(* Replace all TVars by new TFrees *) 

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

1026 
let val prop' = Type.freeze prop 
1238  1027 
in (*no fix_shyps*) 
1529  1028 
Thm{sign = sign, 
1029 
der = infer_derivs (FreezeT, [der]), 

1030 
maxidx = maxidx_of_term prop', 

1031 
shyps = shyps, 

1032 
hyps = hyps, 

1033 
prop = prop'} 

1220  1034 
end; 
0  1035 

1036 

1037 
(*** Inference rules for tactics ***) 

1038 

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

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

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

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

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

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

1045 
end 

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

1047 

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

1529  1051 
let val Thm{shyps=sshyps, prop=sprop, maxidx=smax, sign=ssign,...} = state 
0  1052 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 
1529  1053 
handle TERM _ => raise THM("lift_rule", i, [orule,state]) 
1054 
val ct_Bi = Cterm {sign=ssign, maxidx=smax, T=propT, t=Bi} 

1055 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1) 

1056 
val (Thm{sign, der, maxidx,shyps,hyps,prop}) = orule 

0  1057 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1058 
in (*no fix_shyps*) 
1529  1059 
Thm{sign = merge_thm_sgs(state,orule), 
1060 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 

1061 
maxidx = maxidx+smax+1, 

1062 
shyps=sshyps union shyps, 

1063 
hyps=hyps, 

1064 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 

1065 
map lift_all As, 

1066 
lift_all B)} 

0  1067 
end; 
1068 

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

1070 
fun assumption i state = 

1529  1071 
let val Thm{sign,der,maxidx,hyps,prop,...} = state; 
0  1072 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  1073 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1074 
fix_shyps [state] (env_codT env) 
1529  1075 
(Thm{sign = sign, 
1076 
der = infer_derivs (Assumption (i, Some env), [der]), 

1077 
maxidx = maxidx, 

1078 
shyps = [], 

1079 
hyps = hyps, 

1080 
prop = 

1081 
if Envir.is_empty env then (*avoid wasted normalizations*) 

1082 
Logic.rule_of (tpairs, Bs, C) 

1083 
else (*normalize the new rule fully*) 

1084 
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); 

0  1085 
fun addprfs [] = Sequence.null 
1086 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

1087 
(Sequence.mapp newth 

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

0  1090 
in addprfs (Logic.assum_pairs Bi) end; 
1091 

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

1529  1095 
let val Thm{sign,der,maxidx,hyps,prop,...} = state; 
0  1096 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1097 
in if exists (op aconv) (Logic.assum_pairs Bi) 

1220  1098 
then fix_shyps [state] [] 
1529  1099 
(Thm{sign = sign, 
1100 
der = infer_derivs (Assumption (i,None), [der]), 

1101 
maxidx = maxidx, 

1102 
shyps = [], 

1103 
hyps = hyps, 

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

0  1105 
else raise THM("eq_assumption", 0, [state]) 
1106 
end; 

1107 

1108 

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

1110 

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

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

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

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

1115 
fun rename_params_rule (cs, i) state = 

1529  1116 
let val Thm{sign,der,maxidx,hyps,prop,...} = state 
0  1117 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1118 
val iparams = map #1 (Logic.strip_params Bi) 

1119 
val short = length iparams  length cs 

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

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

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

250  1125 
in 
0  1126 
case findrep cs of 
1127 
c::_ => error ("Bound variables not distinct: " ^ c) 

1128 
 [] => (case cs inter freenames of 

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

1220  1130 
 [] => fix_shyps [state] [] 
1529  1131 
(Thm{sign = sign, 
1132 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1133 
maxidx = maxidx, 

1134 
shyps = [], 

1135 
hyps = hyps, 

1136 
prop = Logic.rule_of(tpairs, Bs@[newBi], C)})) 

0  1137 
end; 
1138 

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

1140 

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

1144 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1145 
else (x,y)::al) 
0  1146 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1147 
 match_bvs(_,_,al) = al; 

1148 

1149 
(* strip abstractions created by parameters *) 

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

1151 

1152 

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

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

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

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

1160 
 strip(A,_) = f A 

0  1161 
in strip end; 
1162 

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

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

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

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

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

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

1170 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1173 
(case assoc(al,x) of 

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

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

1176 
 None=> t) 

0  1177 
 rename(Abs(x,T,t)) = 
250  1178 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1179 
T, rename t) 

0  1180 
 rename(f$t) = rename f $ rename t 
1181 
 rename(t) = t; 

250  1182 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1183 
in strip_ren end; 
1184 

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

1186 
fun rename_bvars(dpairs, tpairs, B) = 

250  1187 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1188 

1189 

1190 
(*** RESOLUTION ***) 

1191 

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

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

1193 

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

250  1196 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1197 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1198 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1199 
Const("all",_)$Abs(_,_,t2)) = 
0  1200 
let val (B1,B2) = strip_assums2 (t1,t2) 
1201 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1202 
 strip_assums2 BB = BB; 

1203 

1204 

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

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

1206 
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

1207 
 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

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

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

1212 
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

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

1215 
 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

1216 

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

1217 

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

1222 
If eres_flg then simultaneously proves A1 by assumption. 

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

1529  1226 
local open Sequence; exception COMPOSE 
0  1227 
in 
250  1228 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1229 
(eres_flg, orule, nsubgoal) = 
1529  1230 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1231 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

1232 
prop=rprop,...} = orule 

1233 
(*How many hyps to skip over during normalization*) 

1238  1234 
and nlift = Logic.count_prems(strip_all_body Bi, 
1235 
if eres_flg then ~1 else 0) 

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

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

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

1241 
val normp = 

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

1243 
else 

1244 
let val ntps = map (pairself normt) tpairs 

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

1247 
if lifted 

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

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

1529  1250 
else if match then raise COMPOSE 
250  1251 
else (*normalize the new rule fully*) 
1252 
(ntps, map normt (Bs @ As), normt C) 

1253 
end 

1258  1254 
val th = (*tuned fix_shyps*) 
1529  1255 
Thm{sign = sign, 
1256 
der = infer_derivs (Bicompose(match, eres_flg, 

1257 
1 + length Bs, nsubgoal, env), 

1258 
[rder,sder]), 

1259 
maxidx = maxidx, 

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

1261 
hyps = rhyps union shyps, 

1262 
prop = Logic.rule_of normp} 

1263 
in cons(th, thq) end handle COMPOSE => thq 

0  1264 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 
1265 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1289 
(*ordinary resolution*) 

1290 
fun res(None) = null 

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

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

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

1296 
end; 

1297 
end; (*open Sequence*) 

1298 

1299 

1300 
fun bicompose match arg i state = 

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

1302 

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

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

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

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

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

1309 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1310 
end; 
1311 

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

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

250  1314 
fun biresolution match brules i state = 
0  1315 
let val lift = lift_rule(state, i); 
250  1316 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1317 
val B = Logic.strip_assums_concl Bi; 

1318 
val Hs = Logic.strip_assums_hyp Bi; 

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

1320 
fun res [] = Sequence.null 

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

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

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

1326 
else res brules 

0  1327 
in Sequence.flats (res brules) end; 
1328 

1329 

1330 

1331 
(*** Meta simp sets ***) 

1332 

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

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

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

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

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

1340 
net: discrimination net of rewrite rules 

1341 
congs: association list of congruence rules 

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

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

1343 
for generating new names when rewriting under lambda abstractions 
0  1344 
mk_rews: used when local assumptions are added 
1345 
*) 

1346 

1529  1347 
val empty_mss = Mss{net = Net.empty, congs = [], bounds=[], prems = [], 
0  1348 
mk_rews = K[]}; 
1349 

1350 
exception SIMPLIFIER of string * thm; 

1351 

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

1352 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1353 

209  1354 
val trace_simp = ref false; 
1355 

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

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

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

1359 

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

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

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

1362 
 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

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

1364 

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

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

1366 
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

1367 

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

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

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

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

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

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

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

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

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

1380 
*) 

0  1381 

1238  1382 
fun mk_rrule raw_thm = 
1383 
let 

1258  1384 
val thm = strip_shyps raw_thm; 
1238  1385 
val Thm{sign,prop,maxidx,...} = thm; 
1386 
val prems = Logic.strip_imp_prems prop 

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

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

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

1390 
val econcl = Pattern.eta_contract concl 