author  berghofe 
Fri, 15 Mar 1996 12:01:19 +0100  
changeset 1580  e3fd931e6095 
parent 1576  af8f43f742a0 
child 1597  54ece585bf62 
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 

1539  77 
 Oracle of theory * Sign.sg * exn; 
1529  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 
1539  153 

154 
val invoke_oracle : theory * Sign.sg * exn > thm 

250  155 
end; 
0  156 

1503  157 
structure Thm : THM = 
0  158 
struct 
250  159 

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

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

161 

250  162 
(** certified types **) 
163 

164 
(*certified typs under a signature*) 

165 

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

167 

168 
fun rep_ctyp (Ctyp args) = args; 

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

170 

171 
fun ctyp_of sign T = 

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

173 

174 
fun read_ctyp sign s = 

175 
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

176 

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

177 

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

178 

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

180 

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

182 

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

184 

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

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

187 

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

190 
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

191 
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

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

193 

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

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

196 

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

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

202 

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

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

204 

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

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

206 
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

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

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

209 
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

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

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

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

213 
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

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

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

216 

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

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

218 
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

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

220 
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

221 
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

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

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

224 

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

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

226 
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

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

228 
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

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

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

231 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  232 

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

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

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

237 
 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

238 

574  239 
(** read cterms **) (*exception ERROR*) 
250  240 

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

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

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

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

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

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

253 

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

254 
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

255 

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

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

257 
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

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

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

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

261 
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

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

265 
 _ => 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

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

269 
map (Sign.certify_typ sign) Ts, 

270 
map read (bs~~Ts)) 

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

271 
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

272 
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

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

274 

250  275 

276 

1529  277 
(*** Derivations ***) 
278 

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

280 
executed in ML.*) 

281 
datatype rule = 

282 
MinProof (*for building minimal proof terms*) 

283 
(*Axioms/theorems*) 

284 
 Axiom of theory * string 

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

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

287 
 Assume of cterm 

288 
 Implies_intr of cterm 

289 
 Implies_intr_shyps 

290 
 Implies_intr_hyps 

291 
 Implies_elim 

292 
 Forall_intr of cterm 

293 
 Forall_elim of cterm 

294 
 Reflexive of cterm 

295 
 Symmetric 

296 
 Transitive 

297 
 Beta_conversion of cterm 

298 
 Extensional 

299 
 Abstract_rule of string * cterm 

300 
 Combination 

301 
 Equal_intr 

302 
 Equal_elim 

303 
(*derived rules for tactical proof*) 

304 
 Trivial of cterm 

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

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

307 
 Lift_rule of cterm * int 

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

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

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

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

312 
(*other derived rules*) 

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

314 
 VarifyT 

315 
 FreezeT 

316 
(*for the simplifier*) 

317 
 RewriteC of cterm 

318 
 CongC of cterm 

319 
 Rewrite_cterm of cterm 

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

321 
 Rename_params_rule of string list * int; 

322 

323 

324 
datatype deriv = Infer of rule * deriv list 

1539  325 
 Oracle of theory * Sign.sg * exn; 
1529  326 

327 

328 
val full_deriv = ref false; 

329 

330 

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

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

333 
 squash_derivs (der :: ders) = der :: squash_derivs ders 

334 
 squash_derivs [] = []; 

335 

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

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

338 

339 
(*Make a minimal inference*) 

340 
fun make_min_infer [] = min_infer 

341 
 make_min_infer [der] = der 

342 
 make_min_infer ders = Infer (MinProof, ders); 

343 

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

345 
 infer_derivs (rl, ders) = 

346 
if !full_deriv then Infer (rl, ders) 

347 
else make_min_infer (squash_derivs ders); 

348 

349 

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

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

351 

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

357 
hyps: term list, (*hypotheses*) 

358 
prop: term}; (*conclusion*) 

0  359 

250  360 
fun rep_thm (Thm args) = args; 
0  361 

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

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

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

366 
hyps = map (ctermf ~1) hyps, 

367 
prop = ctermf maxidx prop} 

1517  368 
end; 
369 

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

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

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

373 

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

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

375 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  376 

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

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

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

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

381 

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

382 

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

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

384 
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

385 

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

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

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

388 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  389 

390 
(*counts premises in a rule*) 

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

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

392 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  393 

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

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

395 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  396 

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

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

399 
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

400 

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

401 

0  402 

1238  403 
(** sort contexts of theorems **) 
404 

405 
(* basic utils *) 

406 

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

408 
to improve efficiency a bit*) 

409 

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

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

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

413 
and add_typs_sorts ([], Ss) = Ss 

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

415 

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

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

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

419 
 add_term_sorts (Bound _, Ss) = Ss 

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

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

422 

423 
fun add_terms_sorts ([], Ss) = Ss 

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

425 

1258  426 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
427 

428 
fun add_env_sorts (env, Ss) = 

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

430 
add_typs_sorts (env_codT env, Ss)); 

431 

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

434 

435 
fun add_thms_shyps ([], Ss) = Ss 

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

437 
add_thms_shyps (ths, shyps union Ss); 

438 

439 

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

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

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

443 

444 

445 
(* fix_shyps *) 

446 

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

448 
fun fix_shyps thms Ts thm = 

449 
let 

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

453 
in 

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

456 
maxidx = maxidx, 

457 
shyps = shyps, hyps = hyps, prop = prop} 

1238  458 
end; 
459 

460 

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

462 

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

464 

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

466 
fun strip_shyps thm = 

467 
let 

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

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

472 
in 

1529  473 
Thm {sign = sign, der = der, maxidx = maxidx, 
474 
shyps = 

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

476 
else (* FIXME tmp *) 

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

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

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

1238  480 
sorts)), 
1529  481 
hyps = hyps, 
482 
prop = prop} 

1238  483 
end; 
484 

485 

486 
(* implies_intr_shyps *) 

487 

488 
(*discharge all extra sort hypotheses*) 

489 
fun implies_intr_shyps thm = 

490 
(case extra_shyps thm of 

491 
[] => thm 

492 
 xshyps => 

493 
let 

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

497 
val names = 

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

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

500 

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

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

503 
in 

1529  504 
Thm {sign = sign, 
505 
der = infer_derivs (Implies_intr_shyps, [der]), 

506 
maxidx = maxidx, 

507 
shyps = shyps', 

508 
hyps = hyps, 

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

1238  510 
end); 
511 

512 

1529  513 
(** Axioms **) 
387
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 
(*look up the named axiom in the theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

518 
fun get_ax [] = raise Match 
1529  519 
 get_ax (thy :: thys) = 
1539  520 
let val {sign, new_axioms, parents, ...} = rep_theory thy 
1529  521 
in case Symtab.lookup (new_axioms, name) of 
522 
Some t => fix_shyps [] [] 

523 
(Thm {sign = sign, 

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

525 
maxidx = maxidx_of_term t, 

526 
shyps = [], 

527 
hyps = [], 

528 
prop = t}) 

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

530 
end; 

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

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

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

533 
=> raise THEORY ("get_axiom: no axiom " ^ quote name, [theory]) 
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 

1529  536 

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

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

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

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

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

541 

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

544 
Thm {sign = sign, 

1566  545 
der = Infer (Theorem(thy,name), [der]), 
1529  546 
maxidx = maxidx, 
547 
shyps = shyps, 

548 
hyps = hyps, 

549 
prop = prop} 

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

0  551 

552 

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

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

556 
Thm {sign = sign, 

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

558 
maxidx = maxidx, 

559 
shyps = shyps, 

560 
hyps = map Term.compress_term hyps, 

561 
prop = Term.compress_term prop}; 

564  562 

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

563 

1529  564 
(*** Meta rules ***) 
0  565 

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

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

567 
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

568 
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

569 

1220  570 
(** 'primitive' rules **) 
571 

572 
(*discharge all assumptions t from ts*) 

0  573 
val disch = gen_rem (op aconv); 
574 

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

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

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

1529  583 
else Thm{sign = sign, 
584 
der = infer_derivs (Assume ct, []), 

585 
maxidx = ~1, 

586 
shyps = add_term_sorts(prop,[]), 

587 
hyps = [prop], 

588 
prop = prop} 

0  589 
end; 
590 

1220  591 
(*Implication introduction 
592 
A  B 

593 
 

594 
A ==> B 

595 
*) 

1529  596 
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

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

603 
maxidx = max[maxidxA, maxidx], 

604 
shyps = [], 

605 
hyps = disch(hyps,A), 

606 
prop = implies$A$prop}) 

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

609 
end; 

610 

1529  611 

1220  612 
(*Implication elimination 
613 
A ==> B A 

614 
 

615 
B 

616 
*) 

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

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

1220  624 
then fix_shyps [thAB, thA] [] 
625 
(Thm{sign= merge_thm_sgs(thAB,thA), 

1529  626 
der = infer_derivs (Implies_elim, [der,derA]), 
627 
maxidx = max[maxA,maxidx], 

628 
shyps = [], 

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

630 
prop = B}) 

250  631 
else err("major premise") 
632 
 _ => err("major premise") 

0  633 
end; 
250  634 

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

637 
 

638 
!!x.A 

639 
*) 

1529  640 
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

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

645 
maxidx = maxidx, 

646 
shyps = [], 

647 
hyps = hyps, 

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

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

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

653 
else result(a,T) 

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

656 
end; 

657 

1220  658 
(*Forall elimination 
659 
!!x.A 

660 
 

661 
A[t/x] 

662 
*) 

1529  663 
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

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

668 
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

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

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

673 
shyps = [], 

674 
hyps = hyps, 

675 
prop = betapply(A,t)}) 

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

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

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

682 

1220  683 
(* Equality *) 
0  684 

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

689 
shyps = [], 

690 
hyps = [], 

691 
maxidx = 0, 

692 
prop = term_of (read_cterm Sign.proto_pure 

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

0  694 

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

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

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

701 
shyps = [], 

702 
hyps = [], 

703 
maxidx = maxidx, 

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

0  705 
end; 
706 

707 
(*The symmetry rule 

1220  708 
t==u 
709 
 

710 
u==t 

711 
*) 

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

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

718 
maxidx = maxidx, 

719 
shyps = shyps, 

720 
hyps = hyps, 

721 
prop = eq$u$t} 

0  722 
 _ => raise THM("symmetric", 0, [th]); 
723 

724 
(*The transitive rule 

1220  725 
t1==u u==t2 
726 
 

727 
t1==t2 

728 
*) 

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

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

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

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

739 
maxidx = max[max1,max2], 

740 
shyps = [], 

741 
hyps = hyps1 union hyps2, 

742 
prop = eq$t1$t2}) 

0  743 
 _ => err"premises" 
744 
end; 

745 

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

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

753 
maxidx = maxidx_of_term t, 

754 
shyps = [], 

755 
hyps = [], 

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

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

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

1220  761 
f(x) == g(x) 
762 
 

763 
f == g 

764 
*) 

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

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

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

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

774 
 Var _ => 

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

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

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

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

781 
maxidx = maxidx, 

782 
shyps = shyps, 

783 
hyps = hyps, 

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

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

787 

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

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

1220  790 
t == u 
791 
 

792 
%x.t == %x.u 

793 
*) 

1529  794 
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

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

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

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

802 
maxidx = maxidx, 

803 
shyps = [], 

804 
hyps = hyps, 

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

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

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

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

811 
else result T 

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

814 
end; 

815 

816 
(*The combination rule 

1220  817 
f==g t==u 
818 
 

819 
f(t)==g(u) 

820 
*) 

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

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

825 
prop=prop2,...} = th2 

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

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

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

831 
maxidx = max[max1,max2], 

832 
shyps = shyps1 union shyps2, 

833 
hyps = hyps1 union hyps2, 

834 
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

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

838 

839 

840 
(* Equality introduction 

1220  841 
A==>B B==>A 
842 
 

843 
A==B 

844 
*) 

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

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

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

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

851 
in case (prop1,prop2) of 

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

853 
if A aconv A' andalso B aconv B' 

854 
then 

855 
(*no fix_shyps*) 

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

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

858 
maxidx = max[max1,max2], 

859 
shyps = shyps1 union shyps2, 

860 
hyps = hyps1 union hyps2, 

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

862 
else err"not equal" 

863 
 _ => err"premises" 

864 
end; 

865 

866 

867 
(*The equal propositions rule 

868 
A==B A 

869 
 

870 
B 

871 
*) 

872 
fun equal_elim th1 th2 = 

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

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

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

876 
in case prop1 of 

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

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

879 
fix_shyps [th1, th2] [] 

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

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

882 
maxidx = max[max1,max2], 

883 
shyps = [], 

884 
hyps = hyps1 union hyps2, 

885 
prop = B}) 

886 
 _ => err"major premise" 

887 
end; 

0  888 

1220  889 

890 

0  891 
(**** Derived rules ****) 
892 

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

899 
maxidx = maxidx, 

900 
shyps = shyps, 

901 
hyps = disch(As,A), 

902 
prop = implies$A$prop}) 

0  903 
 implies_intr_hyps th = th; 
904 

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

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

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

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

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

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

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

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

921 
maxidx = maxidx_of_term newprop, 

922 
shyps = [], 

923 
hyps = hyps, 

924 
prop = newprop}) 

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

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

931 
(*Instantiation of Vars 

1220  932 
A 
933 
 

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

935 
*) 

0  936 

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

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

939 

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

941 
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

942 
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

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

946 
end; 

947 

948 
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

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

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

953 
Instantiates distinct Vars by terms of same type. 

954 
Normalizes the new theorem! *) 

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

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

250  959 
val newprop = 
960 
Envir.norm_term (Envir.empty 0) 

961 
(subst_atomic tpairs 

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

1220  963 
val newth = 
964 
fix_shyps [th] (map snd vTs) 

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

967 
maxidx = maxidx_of_term newprop, 

968 
shyps = [], 

969 
hyps = hyps, 

970 
prop = newprop}) 

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

974 
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

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

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

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

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

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

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

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

991 
maxidx = maxidx, 

992 
shyps = [], 

993 
hyps = [], 

994 
prop = implies$A$A}) 

0  995 
end; 
996 

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

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

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

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

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

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

1007 
maxidx = maxidx, 

1008 
shyps = [], 

1009 
hyps = [], 

1010 
prop = t}) 

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

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

1012 

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

1013 

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

1020 
maxidx = max[0,maxidx], 

1021 
shyps = shyps, 

1022 
hyps = hyps, 

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

0  1024 
end; 
1025 

1026 
(* Replace all TVars by new TFrees *) 

1529  1027 
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

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

1032 
maxidx = maxidx_of_term prop', 

1033 
shyps = shyps, 

1034 
hyps = hyps, 

1035 
prop = prop'} 

1220  1036 
end; 
0  1037 

1038 

1039 
(*** Inference rules for tactics ***) 

1040 

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

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

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

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

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

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

1047 
end 

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

1049 

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

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

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

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

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

1063 
maxidx = maxidx+smax+1, 

1064 
shyps=sshyps union shyps, 

1065 
hyps=hyps, 

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

1067 
map lift_all As, 

1068 
lift_all B)} 

0  1069 
end; 
1070 

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

1072 
fun assumption i state = 

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

1079 
maxidx = maxidx, 

1080 
shyps = [], 

1081 
hyps = hyps, 

1082 
prop = 

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

1084 
Logic.rule_of (tpairs, Bs, C) 

1085 
else (*normalize the new rule fully*) 

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

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

1089 
(Sequence.mapp newth 

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

0  1092 
in addprfs (Logic.assum_pairs Bi) end; 
1093 

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

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

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

1103 
maxidx = maxidx, 

1104 
shyps = [], 

1105 
hyps = hyps, 

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

0  1107 
else raise THM("eq_assumption", 0, [state]) 
1108 
end; 

1109 

1110 

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

1112 

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

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

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

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

1117 
fun rename_params_rule (cs, i) state = 

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

1121 
val short = length iparams  length cs 

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

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

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

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

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1130 
 [] => (case cs inter_string freenames of 
0  1131 
a::_ => error ("Bound/Free variable clash: " ^ a) 
1220  1132 
 [] => fix_shyps [state] [] 
1529  1133 
(Thm{sign = sign, 
1134 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1135 
maxidx = maxidx, 

1136 
shyps = [], 

1137 
hyps = hyps, 

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

0  1139 
end; 
1140 

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

1142 

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

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

1150 

1151 
(* strip abstractions created by parameters *) 

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

1153 

1154 

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

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

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

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

1162 
 strip(A,_) = f A 

0  1163 
in strip end; 
1164 

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

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

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

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

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

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

1172 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1175 
(case assoc(al,x) of 

1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1176 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1177 
else Var((y,i),T) 
1178 
 None=> t) 

0  1179 
 rename(Abs(x,T,t)) = 
1576
af8f43f742a0
Added some optimized versions of functions dealing with sets
berghofe
parents:
1569
diff
changeset

1180 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1181 
T, rename t) 
0  1182 
 rename(f$t) = rename f $ rename t 
1183 
 rename(t) = t; 

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

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

1188 
fun rename_bvars(dpairs, tpairs, B) = 

250  1189 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1190 

1191 

1192 
(*** RESOLUTION ***) 

1193 

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

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

1195 

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

250  1198 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1199 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

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

1204 
 strip_assums2 BB = BB; 

1205 

1206 

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

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

1208 
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

1209 
 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

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

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

1214 
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

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

1217 
 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

1218 

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

1219 

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

1224 
If eres_flg then simultaneously proves A1 by assumption. 

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

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

1234 
prop=rprop,...} = orule 

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

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

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

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

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

1243 
val normp = 

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

1245 
else 

1246 
let val ntps = map (pairself normt) tpairs 

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

1249 
if lifted 

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

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

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

1255 
end 

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

1259 
1 + length Bs, nsubgoal, env), 

1260 
[rder,sder]), 

1261 
maxidx = maxidx, 

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

1263 
hyps = rhyps union shyps, 

1264 
prop = Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1291 
(*ordinary resolution*) 

1292 
fun res(None) = null 

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

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

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

1298 
end; 

1299 
end; (*open Sequence*) 

1300 

1301 

1302 
fun bicompose match arg i state = 

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

1304 

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

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

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

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

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

1311 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1312 
end; 
1313 

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

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

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

1320 
val Hs = Logic.strip_assums_hyp Bi; 

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

1322 
fun res [] = Sequence.null 

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

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

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

1328 
else res brules 

0  1329 
in Sequence.flats (res brules) end; 
1330 

1331 

1332 

1333 
(*** Meta simp sets ***) 

1334 

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

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

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

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

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

1342 
net: discrimination net of rewrite rules 

1343 
congs: association list of congruence rules 

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

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

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

1348 

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

1352 
exception SIMPLIFIER of string * thm; 

1353 

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

1354 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1355 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1356 
fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t)); 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1357 

209  1358 
val trace_simp = ref false; 
1359 

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

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

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

1363 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1364 
fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else (); 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1365 

e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1366 
fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop; 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1367 

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

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

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

1370 
 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

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

1372 

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

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

1374 
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

1375 

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

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

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

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

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

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

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

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

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

1388 
*) 

0  1389 

1238  1390 
fun mk_rrule raw_thm = 
1391 
let 

1258  1392 
val thm = strip_shyps raw_thm; 
1238  < 