author  wenzelm 
Fri, 13 Dec 1996 17:38:17 +0100  
changeset 2386  58f8ff014009 
parent 2266  82aef6857c5b 
child 2509  0a7169d89b7a 
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) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

30 
val dest_abs : cterm > cterm * cterm 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

31 
val adjust_maxidx : 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]*) 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

41 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
2386  42 
val keep_derivs : deriv_kind ref 
1529  43 
datatype rule = 
2386  44 
MinProof 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

45 
 Oracle of theory * Sign.sg * exn 
2386  46 
 Axiom of theory * string 
47 
 Theorem of string 

48 
 Assume of cterm 

49 
 Implies_intr of cterm 

1529  50 
 Implies_intr_shyps 
51 
 Implies_intr_hyps 

52 
 Implies_elim 

2386  53 
 Forall_intr of cterm 
54 
 Forall_elim of cterm 

55 
 Reflexive of cterm 

1529  56 
 Symmetric 
57 
 Transitive 

2386  58 
 Beta_conversion of cterm 
1529  59 
 Extensional 
2386  60 
 Abstract_rule of string * cterm 
1529  61 
 Combination 
62 
 Equal_intr 

63 
 Equal_elim 

2386  64 
 Trivial of cterm 
65 
 Lift_rule of cterm * int 

66 
 Assumption of int * Envir.env option 

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

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

69 
 Flexflex_rule of Envir.env 

70 
 Class_triv of theory * class 

1529  71 
 VarifyT 
72 
 FreezeT 

2386  73 
 RewriteC of cterm 
74 
 CongC of cterm 

75 
 Rewrite_cterm of cterm 

1529  76 
 Rename_params_rule of string list * int; 
77 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

78 
type deriv (* = rule mtree *) 
1529  79 

1160  80 
(*meta theorems*) 
81 
type thm 

82 
exception THM of string * int * thm list 

1529  83 
val rep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 
2386  84 
shyps: sort list, hyps: term list, 
85 
prop: term} 

1529  86 
val crep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 
2386  87 
shyps: sort list, hyps: cterm list, 
88 
prop: cterm} 

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

91 
val prems_of : thm > term list 

92 
val nprems_of : thm > int 

93 
val concl_of : thm > term 

94 
val cprop_of : thm > cterm 

95 
val extra_shyps : thm > sort list 

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

97 
val strip_shyps : thm > thm 

98 
val implies_intr_shyps: thm > thm 

99 
val get_axiom : theory > string > thm 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

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

103 
(*meta rules*) 

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

108 
val forall_intr : cterm > thm > thm 

109 
val forall_elim : cterm > thm > thm 

110 
val flexpair_def : thm 

111 
val reflexive : cterm > thm 

112 
val symmetric : thm > thm 

113 
val transitive : thm > thm > thm 

114 
val beta_conversion : cterm > thm 

115 
val extensional : thm > thm 

116 
val abstract_rule : string > cterm > thm > thm 

117 
val combination : thm > thm > thm 

118 
val equal_intr : thm > thm > thm 

119 
val equal_elim : thm > thm > thm 

120 
val implies_intr_hyps : thm > thm 

121 
val flexflex_rule : thm > thm Sequence.seq 

122 
val instantiate : 

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

126 
val varifyT : thm > thm 

127 
val freezeT : thm > thm 

128 
val dest_state : thm * int > 

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

132 
val eq_assumption : int > thm > thm 

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

139 
(*meta simplification*) 

140 
type meta_simpset 

141 
exception SIMPLIFIER of string * thm 

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

144 
val del_simps : meta_simpset * thm list > meta_simpset 

145 
val mss_of : thm list > meta_simpset 

146 
val add_congs : meta_simpset * thm list > meta_simpset 

147 
val add_prems : meta_simpset * thm list > meta_simpset 

148 
val prems_of_mss : meta_simpset > thm list 

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

150 
val mk_rews_of_mss : meta_simpset > thm > thm list 

151 
val trace_simp : bool ref 

152 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  153 
(meta_simpset > thm > thm option) > cterm > thm 
1539  154 

2386  155 
val invoke_oracle : theory * Sign.sg * exn > thm 
250  156 
end; 
0  157 

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

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

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

162 

250  163 
(** certified types **) 
164 

165 
(*certified typs under a signature*) 

166 

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

168 

169 
fun rep_ctyp (Ctyp args) = args; 

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

171 

172 
fun ctyp_of sign T = 

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

174 

175 
fun read_ctyp sign s = 

176 
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

177 

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

178 

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

179 

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

181 

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

183 

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

185 

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

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

188 

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

191 
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

192 
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

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

194 

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

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

197 

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

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

199 

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

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

201 
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

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

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

204 
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

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

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

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

208 
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

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

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

211 

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

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

213 
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

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

215 
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

216 
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

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

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

219 

2147  220 
(*Makes maxidx precise: it is often too big*) 
221 
fun adjust_maxidx (ct as Cterm {sign, T, t, maxidx, ...}) = 

222 
if maxidx = ~1 then ct 

223 
else Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t}; 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
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, 
2147  229 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
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), 

2147  236 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  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) 
2386  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) = 
2386  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, 
2386  267 
K None, K None, 
268 
[], true, 

269 
map (Sign.certify_typ sign) Ts, 

270 
ListPair.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 = 

2386  282 
MinProof (*for building minimal proof terms*) 
283 
 Oracle of theory * Sign.sg * exn (*oracles*) 

1529  284 
(*Axioms/theorems*) 
2386  285 
 Axiom of theory * string 
286 
 Theorem of string 

1529  287 
(*primitive inferences and compound versions of them*) 
2386  288 
 Assume of cterm 
289 
 Implies_intr of cterm 

1529  290 
 Implies_intr_shyps 
291 
 Implies_intr_hyps 

292 
 Implies_elim 

2386  293 
 Forall_intr of cterm 
294 
 Forall_elim of cterm 

295 
 Reflexive of cterm 

1529  296 
 Symmetric 
297 
 Transitive 

2386  298 
 Beta_conversion of cterm 
1529  299 
 Extensional 
2386  300 
 Abstract_rule of string * cterm 
1529  301 
 Combination 
302 
 Equal_intr 

303 
 Equal_elim 

304 
(*derived rules for tactical proof*) 

2386  305 
 Trivial of cterm 
306 
(*For lift_rule, the proof state is not a premise. 

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

308 
 Lift_rule of cterm * int 

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

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

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

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

1529  313 
(*other derived rules*) 
2386  314 
 Class_triv of theory * class (*derived rule????*) 
1529  315 
 VarifyT 
316 
 FreezeT 

317 
(*for the simplifier*) 

2386  318 
 RewriteC of cterm 
319 
 CongC of cterm 

320 
 Rewrite_cterm of cterm 

1529  321 
(*Logical identities, recorded since they are part of the proof process*) 
2386  322 
 Rename_params_rule of string list * int; 
1529  323 

324 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

325 
type deriv = rule mtree; 
1529  326 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

327 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  328 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

329 
val keep_derivs = ref MinDeriv; 
1529  330 

331 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

332 
(*Build a minimal derivation. Keep oracles; suppress atomic inferences; 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

333 
retain Theorems or their underlying links; keep anything else*) 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

334 
fun squash_derivs [] = [] 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

335 
 squash_derivs (der::ders) = 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

336 
(case der of 
2386  337 
Join (Oracle _, _) => der :: squash_derivs ders 
338 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

339 
then der :: squash_derivs ders 

340 
else squash_derivs (der'::ders) 

341 
 Join (Axiom _, _) => if !keep_derivs=ThmDeriv 

342 
then der :: squash_derivs ders 

343 
else squash_derivs ders 

344 
 Join (_, []) => squash_derivs ders 

345 
 _ => der :: squash_derivs ders); 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

346 

1529  347 

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

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

349 
val min_infer = Join (MinProof, []); 
1529  350 

351 
(*Make a minimal inference*) 

352 
fun make_min_infer [] = min_infer 

353 
 make_min_infer [der] = der 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

354 
 make_min_infer ders = Join (MinProof, ders); 
1529  355 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

356 
fun infer_derivs (rl, []) = Join (rl, []) 
1529  357 
 infer_derivs (rl, ders) = 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

358 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  359 
else make_min_infer (squash_derivs ders); 
360 

361 

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

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

363 

0  364 
datatype thm = Thm of 
2386  365 
{sign: Sign.sg, (*signature for hyps and prop*) 
366 
der: deriv, (*derivation*) 

367 
maxidx: int, (*maximum index of any Var or TVar*) 

368 
shyps: sort list, (*sort hypotheses*) 

369 
hyps: term list, (*hypotheses*) 

370 
prop: term}; (*conclusion*) 

0  371 

250  372 
fun rep_thm (Thm args) = args; 
0  373 

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

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

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

378 
hyps = map (ctermf ~1) hyps, 

379 
prop = ctermf maxidx prop} 

1517  380 
end; 
381 

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

382 
(*errors involving theorems*) 
0  383 
exception THM of string * int * thm list; 
384 

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

385 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

386 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 
0  387 

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

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

389 
fun merge_thm_sgs (th1, th2) = 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

390 
Sign.merge (pairself (#sign o rep_thm) (th1, th2)) 
574  391 
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

392 

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

393 

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

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

395 
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

396 

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

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

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

399 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  400 

401 
(*counts premises in a rule*) 

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

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

403 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  404 

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

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

406 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  407 

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

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

410 
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

411 

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

412 

0  413 

1238  414 
(** sort contexts of theorems **) 
415 

416 
(* basic utils *) 

417 

2163  418 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  419 
to improve efficiency a bit*) 
420 

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

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

422 
 add_typ_sorts (TFree (_, S), Ss) = ins_sort(S,Ss) 
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

423 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  424 
and add_typs_sorts ([], Ss) = Ss 
425 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

426 

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

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

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

430 
 add_term_sorts (Bound _, Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

431 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  432 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
433 

434 
fun add_terms_sorts ([], Ss) = Ss 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

435 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  436 

1258  437 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
438 

439 
fun add_env_sorts (env, Ss) = 

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

441 
add_typs_sorts (env_codT env, Ss)); 

442 

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

445 

446 
fun add_thms_shyps ([], Ss) = Ss 

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

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

448 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  449 

450 

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

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

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

454 

455 

456 
(* fix_shyps *) 

457 

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

459 
fun fix_shyps thms Ts thm = 

460 
let 

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

464 
in 

1529  465 
Thm {sign = sign, 
2386  466 
der = der, (*No new derivation, as other rules call this*) 
467 
maxidx = maxidx, 

468 
shyps = shyps, hyps = hyps, prop = prop} 

1238  469 
end; 
470 

471 

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

473 

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

475 

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

477 
fun strip_shyps thm = 

478 
let 

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

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

482 
val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps; 
1238  483 
in 
1529  484 
Thm {sign = sign, der = der, maxidx = maxidx, 
2386  485 
shyps = 
486 
(if eq_set_sort (shyps',sorts) orelse 

487 
not (!force_strip_shyps) then shyps' 

488 
else (* FIXME tmp *) 

489 
(warning ("Removed sort hypotheses: " ^ 

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

491 
warning "Let's hope these sorts are nonempty!"; 

1238  492 
sorts)), 
1529  493 
hyps = hyps, 
494 
prop = prop} 

1238  495 
end; 
496 

497 

498 
(* implies_intr_shyps *) 

499 

500 
(*discharge all extra sort hypotheses*) 

501 
fun implies_intr_shyps thm = 

502 
(case extra_shyps thm of 

503 
[] => thm 

504 
 xshyps => 

505 
let 

1529  506 
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; 
2182
29e56f003599
Removal of polymorphic equality via mem, subset, eq_set, etc
paulson
parents:
2177
diff
changeset

507 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  508 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
509 
val names = 

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

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

512 

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

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

515 
in 

1529  516 
Thm {sign = sign, 
2386  517 
der = infer_derivs (Implies_intr_shyps, [der]), 
518 
maxidx = maxidx, 

519 
shyps = shyps', 

520 
hyps = hyps, 

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

1238  522 
end); 
523 

524 

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

526 

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

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

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

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

530 
fun get_ax [] = raise Match 
1529  531 
 get_ax (thy :: thys) = 
2386  532 
let val {sign, new_axioms, parents, ...} = rep_theory thy 
1529  533 
in case Symtab.lookup (new_axioms, name) of 
2386  534 
Some t => fix_shyps [] [] 
535 
(Thm {sign = sign, 

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

537 
maxidx = maxidx_of_term t, 

538 
shyps = [], 

539 
hyps = [], 

540 
prop = t}) 

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

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

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

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

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

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

547 

1529  548 

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

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

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

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

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

553 

1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

554 
(*Attach a label to a theorem to make proof objects more readable*) 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

555 
fun name_thm (name, th as Thm {sign, der, maxidx, shyps, hyps, prop}) = 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

556 
Thm {sign = sign, 
2386  557 
der = Join (Theorem name, [der]), 
558 
maxidx = maxidx, 

559 
shyps = shyps, 

560 
hyps = hyps, 

561 
prop = prop}; 

0  562 

563 

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

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

567 
Thm {sign = sign, 

2386  568 
der = der, (*No derivation recorded!*) 
569 
maxidx = maxidx, 

570 
shyps = shyps, 

571 
hyps = map Term.compress_term hyps, 

572 
prop = Term.compress_term prop}; 

564  573 

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

574 

1529  575 
(*** Meta rules ***) 
0  576 

2147  577 
(*Check that term does not contain same var with different typing/sorting. 
578 
If this check must be made, recalculate maxidx in hope of preventing its 

579 
recurrence.*) 

580 
fun nodup_Vars (thm as Thm{sign, der, maxidx, shyps, hyps, prop}) s = 

581 
(Sign.nodup_Vars prop; 

582 
Thm {sign = sign, 

2386  583 
der = der, 
584 
maxidx = maxidx_of_term prop, 

585 
shyps = shyps, 

586 
hyps = hyps, 

587 
prop = prop}) 

2147  588 
handle TYPE(msg,Ts,ts) => raise TYPE(s^": "^msg,Ts,ts); 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

589 

1220  590 
(** 'primitive' rules **) 
591 

592 
(*discharge all assumptions t from ts*) 

0  593 
val disch = gen_rem (op aconv); 
594 

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

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

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

1529  603 
else Thm{sign = sign, 
2386  604 
der = infer_derivs (Assume ct, []), 
605 
maxidx = ~1, 

606 
shyps = add_term_sorts(prop,[]), 

607 
hyps = [prop], 

608 
prop = prop} 

0  609 
end; 
610 

1220  611 
(*Implication introduction 
612 
A  B 

613 
 

614 
A ==> B 

615 
*) 

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

617 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  618 
in if T<>propT then 
250  619 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  620 
else fix_shyps [thB] [] 
1529  621 
(Thm{sign = Sign.merge (sign,signA), 
2386  622 
der = infer_derivs (Implies_intr cA, [der]), 
623 
maxidx = Int.max(maxidxA, maxidx), 

624 
shyps = [], 

625 
hyps = disch(hyps,A), 

626 
prop = implies$A$prop}) 

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

629 
end; 

630 

1529  631 

1220  632 
(*Implication elimination 
633 
A ==> B A 

634 
 

635 
B 

636 
*) 

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

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

1220  644 
then fix_shyps [thAB, thA] [] 
645 
(Thm{sign= merge_thm_sgs(thAB,thA), 

2386  646 
der = infer_derivs (Implies_elim, [der,derA]), 
647 
maxidx = Int.max(maxA,maxidx), 

648 
shyps = [], 

649 
hyps = union_term(hypsA,hyps), (*dups suppressed*) 

650 
prop = B}) 

250  651 
else err("major premise") 
652 
 _ => err("major premise") 

0  653 
end; 
250  654 

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

657 
 

658 
!!x.A 

659 
*) 

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

661 
let val x = term_of cx; 
1238  662 
fun result(a,T) = fix_shyps [th] [] 
1529  663 
(Thm{sign = sign, 
2386  664 
der = infer_derivs (Forall_intr cx, [der]), 
665 
maxidx = maxidx, 

666 
shyps = [], 

667 
hyps = hyps, 

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

0  669 
in case x of 
250  670 
Free(a,T) => 
671 
if exists (apl(x, Logic.occs)) hyps 

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

673 
else result(a,T) 

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

676 
end; 

677 

1220  678 
(*Forall elimination 
679 
!!x.A 

680 
 

681 
A[t/x] 

682 
*) 

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

684 
let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct 
0  685 
in case prop of 
2386  686 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
687 
if T<>qary then 

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

689 
else let val thm = fix_shyps [th] [] 

690 
(Thm{sign= Sign.merge(sign,signt), 

691 
der = infer_derivs (Forall_elim ct, [der]), 

692 
maxidx = Int.max(maxidx, maxt), 

693 
shyps = [], 

694 
hyps = hyps, 

695 
prop = betapply(A,t)}) 

696 
in if maxt >= 0 andalso maxidx >= 0 

697 
then nodup_Vars thm "forall_elim" 

698 
else thm (*no new Vars: no expensive check!*) 

699 
end 

2147  700 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  701 
end 
702 
handle TERM _ => 

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

705 

1220  706 
(* Equality *) 
0  707 

1220  708 
(* Definition of the relation =?= *) 
1238  709 
val flexpair_def = fix_shyps [] [] 
1529  710 
(Thm{sign= Sign.proto_pure, 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

711 
der = Join(Axiom(pure_thy, "flexpair_def"), []), 
1529  712 
shyps = [], 
713 
hyps = [], 

714 
maxidx = 0, 

715 
prop = term_of (read_cterm Sign.proto_pure 

2386  716 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); 
0  717 

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

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

720 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  721 
in fix_shyps [] [] 
1529  722 
(Thm{sign= sign, 
2386  723 
der = infer_derivs (Reflexive ct, []), 
724 
shyps = [], 

725 
hyps = [], 

726 
maxidx = maxidx, 

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

0  728 
end; 
729 

730 
(*The symmetry rule 

1220  731 
t==u 
732 
 

733 
u==t 

734 
*) 

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

1238  738 
(*no fix_shyps*) 
2386  739 
Thm{sign = sign, 
740 
der = infer_derivs (Symmetric, [der]), 

741 
maxidx = maxidx, 

742 
shyps = shyps, 

743 
hyps = hyps, 

744 
prop = eq$u$t} 

0  745 
 _ => raise THM("symmetric", 0, [th]); 
746 

747 
(*The transitive rule 

1220  748 
t1==u u==t2 
749 
 

750 
t1==t2 

751 
*) 

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

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

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

1634  758 
if not (u aconv u') then err"middle term" 
759 
else let val thm = 

1220  760 
fix_shyps [th1, th2] [] 
1529  761 
(Thm{sign= merge_thm_sgs(th1,th2), 
2386  762 
der = infer_derivs (Transitive, [der1, der2]), 
2147  763 
maxidx = Int.max(max1,max2), 
2386  764 
shyps = [], 
765 
hyps = union_term(hyps1,hyps2), 

766 
prop = eq$t1$t2}) 

2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

767 
in if max1 >= 0 andalso max2 >= 0 
2147  768 
then nodup_Vars thm "transitive" 
769 
else thm (*no new Vars: no expensive check!*) 

2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

770 
end 
0  771 
 _ => err"premises" 
772 
end; 

773 

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

776 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  777 
in case t of 
1238  778 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
1529  779 
(Thm{sign = sign, 
2386  780 
der = infer_derivs (Beta_conversion ct, []), 
781 
maxidx = maxidx, 

782 
shyps = [], 

783 
hyps = [], 

784 
prop = Logic.mk_equals(t, subst_bound (u,bodt))}) 

250  785 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  786 
end; 
787 

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

1220  789 
f(x) == g(x) 
790 
 

791 
f == g 

792 
*) 

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

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

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

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

802 
 Var _ => 

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

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

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

1238  806 
(*no fix_shyps*) 
1529  807 
Thm{sign = sign, 
2386  808 
der = infer_derivs (Extensional, [der]), 
809 
maxidx = maxidx, 

810 
shyps = shyps, 

811 
hyps = hyps, 

1529  812 
prop = Logic.mk_equals(f,g)} 
0  813 
end 
814 
 _ => raise THM("extensional: premise", 0, [th]); 

815 

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

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

1220  818 
t == u 
819 
 

820 
%x.t == %x.u 

821 
*) 

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

823 
let val x = term_of cx; 
250  824 
val (t,u) = Logic.dest_equals prop 
825 
handle TERM _ => 

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

1238  827 
fun result T = fix_shyps [th] [] 
2386  828 
(Thm{sign = sign, 
829 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

830 
maxidx = maxidx, 

831 
shyps = [], 

832 
hyps = hyps, 

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

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

0  835 
in case x of 
250  836 
Free(_,T) => 
837 
if exists (apl(x, Logic.occs)) hyps 

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

839 
else result T 

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

842 
end; 

843 

844 
(*The combination rule 

1220  845 
f==g t==u 
846 
 

847 
f(t)==g(u) 

848 
*) 

0  849 
fun combination th1 th2 = 
1529  850 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  851 
prop=prop1,...} = th1 
1529  852 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  853 
prop=prop2,...} = th2 
1836
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

854 
fun chktypes (f,t) = 
2386  855 
(case fastype_of f of 
856 
Type("fun",[T1,T2]) => 

857 
if T1 <> fastype_of t then 

858 
raise THM("combination: types", 0, [th1,th2]) 

859 
else () 

860 
 _ => raise THM("combination: not function type", 0, 

861 
[th1,th2])) 

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

862 
in case (prop1,prop2) of 
0  863 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 
1836
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

864 
let val _ = chktypes (f,t) 
2386  865 
val thm = (*no fix_shyps*) 
866 
Thm{sign = merge_thm_sgs(th1,th2), 

867 
der = infer_derivs (Combination, [der1, der2]), 

868 
maxidx = Int.max(max1,max2), 

869 
shyps = union_sort(shyps1,shyps2), 

870 
hyps = union_term(hyps1,hyps2), 

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

2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

872 
in if max1 >= 0 andalso max2 >= 0 
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

873 
then nodup_Vars thm "combination" 
2386  874 
else thm (*no new Vars: no expensive check!*) 
2139
2c59b204b540
Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
paulson
parents:
2047
diff
changeset

875 
end 
0  876 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
877 
end; 

878 

879 

880 
(* Equality introduction 

1220  881 
A==>B B==>A 
882 
 

883 
A==B 

884 
*) 

0  885 
fun equal_intr th1 th2 = 
1529  886 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  887 
prop=prop1,...} = th1 
1529  888 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  889 
prop=prop2,...} = th2; 
1529  890 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
891 
in case (prop1,prop2) of 

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

2386  893 
if A aconv A' andalso B aconv B' 
894 
then 

895 
(*no fix_shyps*) 

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

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

898 
maxidx = Int.max(max1,max2), 

899 
shyps = union_sort(shyps1,shyps2), 

900 
hyps = union_term(hyps1,hyps2), 

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

902 
else err"not equal" 

1529  903 
 _ => err"premises" 
904 
end; 

905 

906 

907 
(*The equal propositions rule 

908 
A==B A 

909 
 

910 
B 

911 
*) 

912 
fun equal_elim th1 th2 = 

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

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

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

916 
in case prop1 of 

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

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

919 
fix_shyps [th1, th2] [] 

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

2386  921 
der = infer_derivs (Equal_elim, [der1, der2]), 
922 
maxidx = Int.max(max1,max2), 

923 
shyps = [], 

924 
hyps = union_term(hyps1,hyps2), 

925 
prop = B}) 

1529  926 
 _ => err"major premise" 
927 
end; 

0  928 

1220  929 

930 

0  931 
(**** Derived rules ****) 
932 

1503  933 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  934 
Repeated hypotheses are discharged only once; fold cannot do this*) 
1529  935 
fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = 
1238  936 
implies_intr_hyps (*no fix_shyps*) 
1529  937 
(Thm{sign = sign, 
2386  938 
der = infer_derivs (Implies_intr_hyps, [der]), 
939 
maxidx = maxidx, 

940 
shyps = shyps, 

1529  941 
hyps = disch(As,A), 
2386  942 
prop = implies$A$prop}) 
0  943 
 implies_intr_hyps th = th; 
944 

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

250  946 
Instantiates the theorem and deletes trivial tpairs. 
0  947 
Resulting sequence may contain multiple elements if the tpairs are 
948 
not all flexflex. *) 

1529  949 
fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = 
250  950 
let fun newthm env = 
1529  951 
if Envir.is_empty env then th 
952 
else 

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

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

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

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

1220  958 
in fix_shyps [th] (env_codT env) 
1529  959 
(Thm{sign = sign, 
2386  960 
der = infer_derivs (Flexflex_rule env, [der]), 
961 
maxidx = maxidx_of_term newprop, 

962 
shyps = [], 

963 
hyps = hyps, 

964 
prop = newprop}) 

250  965 
end; 
0  966 
val (tpairs,_) = Logic.strip_flexpairs prop 
967 
in Sequence.maps newthm 

250  968 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  969 
end; 
970 

971 
(*Instantiation of Vars 

1220  972 
A 
973 
 

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

975 
*) 

0  976 

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

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

979 

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

981 
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

982 
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

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

986 
end; 

987 

988 
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

989 
let val {T,sign} = rep_ctyp ctyp 
0  990 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
991 

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

993 
Instantiates distinct Vars by terms of same type. 

994 
Normalizes the new theorem! *) 

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

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

250  999 
val newprop = 
1000 
Envir.norm_term (Envir.empty 0) 

1001 
(subst_atomic tpairs 

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

1220  1003 
val newth = 
1004 
fix_shyps [th] (map snd vTs) 

1529  1005 
(Thm{sign = newsign, 
2386  1006 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1007 
maxidx = maxidx_of_term newprop, 

1008 
shyps = [], 

1009 
hyps = hyps, 

1010 
prop = newprop}) 

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

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

2147  1015 
else nodup_Vars newth "instantiate" 
0  1016 
end 
250  1017 
handle TERM _ => 
0  1018 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  1019 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  1020 

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

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

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

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

1238  1027 
else fix_shyps [] [] 
1529  1028 
(Thm{sign = sign, 
2386  1029 
der = infer_derivs (Trivial ct, []), 
1030 
maxidx = maxidx, 

1031 
shyps = [], 

1032 
hyps = [], 

1033 
prop = implies$A$A}) 

0  1034 
end; 
1035 

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

1037 
fun class_triv thy c = 
1529  1038 
let val sign = sign_of thy; 
1039 
val Cterm {t, maxidx, ...} = 

2386  1040 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
1041 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 

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

1042 
in 
1238  1043 
fix_shyps [] [] 
1529  1044 
(Thm {sign = sign, 
2386  1045 
der = infer_derivs (Class_triv(thy,c), []), 
1046 
maxidx = maxidx, 

1047 
shyps = [], 

1048 
hyps = [], 

1049 
prop = t}) 

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

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

1051 

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

1052 

0  1053 
(* Replace all TFrees not in the hyps by new TVars *) 
1529  1054 
fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
0  1055 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1634  1056 
in let val thm = (*no fix_shyps*) 
1529  1057 
Thm{sign = sign, 
2386  1058 
der = infer_derivs (VarifyT, [der]), 
1059 
maxidx = Int.max(0,maxidx), 

1060 
shyps = shyps, 

1061 
hyps = hyps, 

1529  1062 
prop = Type.varify(prop,tfrees)} 
2147  1063 
in nodup_Vars thm "varifyT" end 
1634  1064 
(* this nodup_Vars check can be removed if thms are guaranteed not to contain 
1065 
duplicate TVars with differnt sorts *) 

0  1066 
end; 
1067 

1068 
(* Replace all TVars by new TFrees *) 

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

1070 
let val prop' = Type.freeze prop 
1238  1071 
in (*no fix_shyps*) 
1529  1072 
Thm{sign = sign, 
2386  1073 
der = infer_derivs (FreezeT, [der]), 
1074 
maxidx = maxidx_of_term prop', 

1075 
shyps = shyps, 

1076 
hyps = hyps, 

1529  1077 
prop = prop'} 
1220  1078 
end; 
0  1079 

1080 

1081 
(*** Inference rules for tactics ***) 

1082 

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

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

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

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

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

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

1089 
end 

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

1091 

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

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

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

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

0  1101 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1102 
in (*no fix_shyps*) 
1529  1103 
Thm{sign = merge_thm_sgs(state,orule), 
2386  1104 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1105 
maxidx = maxidx+smax+1, 

2177
8b365a3a6ed1
Changed some mem, ins and union calls to be monomorphic
paulson
parents:
2163
diff
changeset

1106 
shyps=union_sort(sshyps,shyps), 
2386  1107 
hyps=hyps, 
1529  1108 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1109 
map lift_all As, 
1110 
lift_all B)} 

0  1111 
end; 
1112 

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

1114 
fun assumption i state = 

1529  1115 
let val Thm{sign,der,maxidx,hyps,prop,...} = state; 
0  1116 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  1117 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1118 
fix_shyps [state] (env_codT env) 
1529  1119 
(Thm{sign = sign, 
2386  1120 
der = infer_derivs (Assumption (i, Some env), [der]), 
1121 
maxidx = maxidx, 

1122 
shyps = [], 

1123 
hyps = hyps, 

1124 
prop = 

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

1126 
Logic.rule_of (tpairs, Bs, C) 

1127 
else (*normalize the new rule fully*) 

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

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

1131 
(Sequence.mapp newth 

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

0  1134 
in addprfs (Logic.assum_pairs Bi) end; 
1135 

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

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

1220  1142 
then fix_shyps [state] [] 
1529  1143 
(Thm{sign = sign, 
2386  1144 
der = infer_derivs (Assumption (i,None), [der]), 
1145 
maxidx = maxidx, 

1146 
shyps = [], 

1147 
hyps = hyps, 

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

0  1149 
else raise THM("eq_assumption", 0, [state]) 
1150 
end; 

1151 

1152 

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

1154 

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

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

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

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

1159 
fun rename_params_rule (cs, i) state = 

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

1163 
val short = length iparams  length cs 

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

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

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

250  1169 
in 
0  1170 
case findrep cs of 
1171 
c::_ => error ("Bound variables not distinct: " ^ c) 

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

1172 
 [] => (case cs inter_string freenames of 
0  1173 
a::_ => error ("Bound/Free variable clash: " ^ a) 
1220  1174 
 [] => fix_shyps [state] [] 
2386  1175 
(Thm{sign = sign, 
1176 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1177 
maxidx = maxidx, 

1178 
shyps = [], 

1179 
hyps = hyps, 

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

0  1181 
end; 
1182 

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

1184 

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

1188 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1189 
else (x,y)::al) 
0  1190 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1191 
 match_bvs(_,_,al) = al; 

1192 

1193 
(* strip abstractions created by parameters *) 

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

1195 

1196 

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

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

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

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

1204 
 strip(A,_) = f A 

0  1205 
in strip end; 
1206 

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

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

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

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

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

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

1214 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1217 
(case assoc(al,x) of 

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

1218 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1219 
else Var((y,i),T) 
1220 
 None=> t) 

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

1222 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1223 
T, rename t) 
0  1224 
 rename(f$t) = rename f $ rename t 
1225 
 rename(t) = t; 

250  1226 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1227 
in strip_ren end; 
1228 

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

1230 
fun rename_bvars(dpairs, tpairs, B) = 

250  1231 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1232 

1233 

1234 
(*** RESOLUTION ***) 

1235 

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

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

1237 

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

250  1240 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1241 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1242 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1243 
Const("all",_)$Abs(_,_,t2)) = 
0  1244 
let val (B1,B2) = strip_assums2 (t1,t2) 
1245 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1246 
 strip_assums2 BB = BB; 

1247 

1248 

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

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

1250 
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

1251 
 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

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

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

1256 
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

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

1259 
 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

1260 

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

1261 

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

1266 
If eres_flg then simultaneously proves A1 by assumption. 

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

1529  1270 
local open Sequence; exception COMPOSE 
0  1271 
in 
250  1272 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1273 
(eres_flg, orule, nsubgoal) = 
1529  1274 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1275 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

2386  1276 
prop=rprop,...} = orule 
1529  1277 
(*How many hyps to skip over during normalization*) 
1238  1278 
and nlift = Logic.count_prems(strip_all_body Bi, 
1279 
if eres_flg then ~1 else 0) 

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

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

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

1285 
val normp = 

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

1287 
else 

1288 
let val ntps = map (pairself normt) tpairs 

2147  1289 
in if Envir.above (smax, env) then 
1238  1290 
(*no assignments in state; normalize the rule only*) 
1291 
if lifted 

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

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

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

1297 
end 

1258  1298 
val th = (*tuned fix_shyps*) 
1529  1299 
Thm{sign = sign, 
2386  1300 
der = infer_derivs (Bicompose(match, eres_flg, 
1301 
1 + length Bs, nsubgoal, env), 

1302 
[rder,sder]), 

1303 
maxidx = maxidx, 

1304 
shyps = add_env_sorts (env, union_sort(rshyps,sshyps)), 

1305 
hyps = union_term(rhyps,shyps), 

1306 
prop = Logic.rule_of normp} 

1529  1307 
in cons(th, thq) end handle COMPOSE => thq 
0  1308 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 
1309 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

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

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

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

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

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

0  1318 
end; 
2147  1319 
val env = Envir.empty(Int.max(rmax,smax)); 
0  1320 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 
1321 
val dpairs = BBi :: (rtpairs@stpairs); 

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

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

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

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

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

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

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

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

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

1333 
(*ordinary resolution*) 

1334 
fun res(None) = null 

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

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

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

1340 
end; 

1341 
end; (*open Sequence*) 

1342 

1343 

1344 
fun bicompose match arg i state = 

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

1346 

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

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

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

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

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

1353 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1354 
end; 
1355 

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

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

250  1358 
fun biresolution match brules i state = 
0  1359 
let val lift = lift_rule(state, i); 
250  1360 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1361 
val B = Logic.strip_assums_concl Bi; 

1362 
val Hs = Logic.strip_assums_hyp Bi; 

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

1364 
fun res [] = Sequence.null 

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

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

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

1370 
else res brules 

0  1371 
in Sequence.flats (res brules) end; 
1372 

1373 

1374 

1375 
(*** Meta simp sets ***) 

1376 
