author  wenzelm 
Wed, 23 Apr 1997 10:08:51 +0200  
changeset 3012  0d683397b74b 
parent 2979  db6941221197 
child 3037  99ed078e6ae7 
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 

2671  26 
val ctyp_of_term : cterm > ctyp 
1238  27 
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

28 
val read_cterms : Sign.sg > string list * typ list > cterm list 
1238  29 
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

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 
1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

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

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

38 

1529  39 
(*theories*) 
40 

2671  41 
(*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

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

46 
 Oracle of theory * Sign.sg * exn 
2671  47 
 Axiom of theory * string 
48 
 Theorem of string 

49 
 Assume of cterm 

50 
 Implies_intr of cterm 

1529  51 
 Implies_intr_shyps 
52 
 Implies_intr_hyps 

53 
 Implies_elim 

2671  54 
 Forall_intr of cterm 
55 
 Forall_elim of cterm 

56 
 Reflexive of cterm 

1529  57 
 Symmetric 
58 
 Transitive 

2671  59 
 Beta_conversion of cterm 
1529  60 
 Extensional 
2671  61 
 Abstract_rule of string * cterm 
1529  62 
 Combination 
63 
 Equal_intr 

64 
 Equal_elim 

2671  65 
 Trivial of cterm 
66 
 Lift_rule of cterm * int 

67 
 Assumption of int * Envir.env option 

68 
 Rotate_rule of int * int 

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

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

71 
 Flexflex_rule of Envir.env 

72 
 Class_triv of theory * class 

1529  73 
 VarifyT 
74 
 FreezeT 

2671  75 
 RewriteC of cterm 
76 
 CongC of cterm 

77 
 Rewrite_cterm of cterm 

78 
 Rename_params_rule of string list * int; 

1529  79 

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

80 
type deriv (* = rule mtree *) 
1529  81 

1160  82 
(*meta theorems*) 
83 
type thm 

84 
exception THM of string * int * thm list 

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

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

1238  91 
val stamps_of_thm : thm > string ref list 
92 
val tpairs_of : thm > (term * term) list 

93 
val prems_of : thm > term list 

94 
val nprems_of : thm > int 

95 
val concl_of : thm > term 

96 
val cprop_of : thm > cterm 

97 
val extra_shyps : thm > sort list 

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

99 
val strip_shyps : thm > thm 

100 
val implies_intr_shyps: thm > thm 

101 
val get_axiom : theory > string > thm 

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

102 
val name_thm : string * thm > thm 
1238  103 
val axioms_of : theory > (string * thm) list 
1160  104 

105 
(*meta rules*) 

1238  106 
val assume : cterm > thm 
1416  107 
val compress : thm > thm 
1238  108 
val implies_intr : cterm > thm > thm 
109 
val implies_elim : thm > thm > thm 

110 
val forall_intr : cterm > thm > thm 

111 
val forall_elim : cterm > thm > thm 

112 
val flexpair_def : thm 

113 
val reflexive : cterm > thm 

114 
val symmetric : thm > thm 

115 
val transitive : thm > thm > thm 

116 
val beta_conversion : cterm > thm 

117 
val extensional : thm > thm 

118 
val abstract_rule : string > cterm > thm > thm 

119 
val combination : thm > thm > thm 

120 
val equal_intr : thm > thm > thm 

121 
val equal_elim : thm > thm > thm 

122 
val implies_intr_hyps : thm > thm 

123 
val flexflex_rule : thm > thm Sequence.seq 

124 
val instantiate : 

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

128 
val varifyT : thm > thm 

129 
val freezeT : thm > thm 

130 
val dest_state : thm * int > 

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

134 
val eq_assumption : int > thm > thm 

2671  135 
val rotate_rule : int > int > thm > thm 
1160  136 
val rename_params_rule: string list * int > thm > thm 
1238  137 
val bicompose : bool > bool * thm * int > 
1160  138 
int > thm > thm Sequence.seq 
1238  139 
val biresolution : bool > (bool * thm) list > 
1160  140 
int > thm > thm Sequence.seq 
141 

142 
(*meta simplification*) 

143 
type meta_simpset 

144 
exception SIMPLIFIER of string * thm 

1238  145 
val empty_mss : meta_simpset 
146 
val add_simps : meta_simpset * thm list > meta_simpset 

147 
val del_simps : meta_simpset * thm list > meta_simpset 

148 
val mss_of : thm list > meta_simpset 

149 
val add_congs : meta_simpset * thm list > meta_simpset 

2626  150 
val del_congs : meta_simpset * thm list > meta_simpset 
2509  151 
val add_simprocs : meta_simpset * 
152 
(Sign.sg * term * (Sign.sg > term > thm option) * stamp) list > meta_simpset 

153 
val del_simprocs : meta_simpset * 

154 
(Sign.sg * term * (Sign.sg > term > thm option) * stamp) list > meta_simpset 

1238  155 
val add_prems : meta_simpset * thm list > meta_simpset 
156 
val prems_of_mss : meta_simpset > thm list 

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

158 
val mk_rews_of_mss : meta_simpset > thm > thm list 

2509  159 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  160 
val trace_simp : bool ref 
161 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  162 
(meta_simpset > thm > thm option) > cterm > thm 
1539  163 

2386  164 
val invoke_oracle : theory * Sign.sg * exn > thm 
250  165 
end; 
0  166 

1503  167 
structure Thm : THM = 
0  168 
struct 
250  169 

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

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

171 

250  172 
(** certified types **) 
173 

174 
(*certified typs under a signature*) 

175 

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

177 

178 
fun rep_ctyp (Ctyp args) = args; 

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

180 

181 
fun ctyp_of sign T = 

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

183 

184 
fun read_ctyp sign s = 

185 
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

186 

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

187 

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

188 

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

190 

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

192 

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

194 

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

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

197 

2671  198 
fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T}; 
199 

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

202 
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

203 
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

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

205 

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

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

208 

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

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

210 

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

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

212 
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

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

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

215 
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

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

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

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

219 
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

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

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

222 

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

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

224 
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

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

226 
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

227 
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

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

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

230 

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

233 
if maxidx = ~1 then ct 

234 
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

235 

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

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

237 
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

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

239 
if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty, 
2147  240 
maxidx=Int.max(maxidx1, maxidx2)} 
1516
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

242 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  243 

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

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

2147  247 
T = ty > T2, maxidx=Int.max(maxidx1, maxidx2)} 
1517  248 
 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

249 

2509  250 

251 

574  252 
(** read cterms **) (*exception ERROR*) 
250  253 

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

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

255 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  256 
let 
574  257 
val T' = Sign.certify_typ sign T 
258 
handle TYPE (msg, _, _) => error msg; 

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

260 
val (_, t', tye) = 
959  261 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  262 
val ct = cterm_of sign t' 
2979  263 
handle TYPE (msg, _, _) => error msg 
2386  264 
 TERM (msg, _) => error msg; 
250  265 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

266 

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

267 
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

268 

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

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

270 
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

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

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

273 
let 
2979  274 
val {tsig, syn, ...} = Sign.rep_sg sign; 
275 
fun read (b, T) = 

276 
(case Syntax.read syn T b of 

277 
[t] => t 

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

279 

280 
val prt = setmp Syntax.show_brackets true (Sign.pretty_term sign); 

281 
val prT = Sign.pretty_typ sign; 

282 
val (us, _) = 

283 
Type.infer_types prt prT tsig (Sign.const_type sign) 

284 
(K None) (K None) [] true (map (Sign.certify_typ sign) Ts) 

285 
(ListPair.map read (bs, Ts)); 

286 
in map (cterm_of sign) us end 

287 
handle TYPE (msg, _, _) => error msg 

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

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

289 

250  290 

291 

1529  292 
(*** Derivations ***) 
293 

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

295 
executed in ML.*) 

296 
datatype rule = 

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

1529  299 
(*Axioms/theorems*) 
2386  300 
 Axiom of theory * string 
301 
 Theorem of string 

1529  302 
(*primitive inferences and compound versions of them*) 
2386  303 
 Assume of cterm 
304 
 Implies_intr of cterm 

1529  305 
 Implies_intr_shyps 
306 
 Implies_intr_hyps 

307 
 Implies_elim 

2386  308 
 Forall_intr of cterm 
309 
 Forall_elim of cterm 

310 
 Reflexive of cterm 

1529  311 
 Symmetric 
312 
 Transitive 

2386  313 
 Beta_conversion of cterm 
1529  314 
 Extensional 
2386  315 
 Abstract_rule of string * cterm 
1529  316 
 Combination 
317 
 Equal_intr 

318 
 Equal_elim 

319 
(*derived rules for tactical proof*) 

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

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

323 
 Lift_rule of cterm * int 

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

2671  325 
 Rotate_rule of int * int 
2386  326 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
327 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  329 
(*other derived rules*) 
2509  330 
 Class_triv of theory * class 
1529  331 
 VarifyT 
332 
 FreezeT 

333 
(*for the simplifier*) 

2386  334 
 RewriteC of cterm 
335 
 CongC of cterm 

336 
 Rewrite_cterm of cterm 

1529  337 
(*Logical identities, recorded since they are part of the proof process*) 
2386  338 
 Rename_params_rule of string list * int; 
1529  339 

340 

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

341 
type deriv = rule mtree; 
1529  342 

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

343 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  344 

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

345 
val keep_derivs = ref MinDeriv; 
1529  346 

347 

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

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

349 
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

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

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

352 
(case der of 
2386  353 
Join (Oracle _, _) => der :: squash_derivs ders 
354 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

355 
then der :: squash_derivs ders 

356 
else squash_derivs (der'::ders) 

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

358 
then der :: squash_derivs ders 

359 
else squash_derivs ders 

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

361 
 _ => der :: squash_derivs ders); 

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

362 

1529  363 

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

365 
val min_infer = Join (MinProof, []); 
1529  366 

367 
(*Make a minimal inference*) 

368 
fun make_min_infer [] = min_infer 

369 
 make_min_infer [der] = der 

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

370 
 make_min_infer ders = Join (MinProof, ders); 
1529  371 

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

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

374 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  375 
else make_min_infer (squash_derivs ders); 
376 

377 

2509  378 

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

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

380 

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

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

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

386 
hyps: term list, (*hypotheses*) 

387 
prop: term}; (*conclusion*) 

0  388 

250  389 
fun rep_thm (Thm args) = args; 
0  390 

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

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

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

395 
hyps = map (ctermf ~1) hyps, 

396 
prop = ctermf maxidx prop} 

1517  397 
end; 
398 

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

399 
(*errors involving theorems*) 
0  400 
exception THM of string * int * thm list; 
401 

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

402 

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

403 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 
0  404 

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

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

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

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

409 

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

410 

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

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

412 
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

413 

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

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

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

416 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  417 

418 
(*counts premises in a rule*) 

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

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

420 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  421 

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

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

423 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  424 

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

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

427 
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

428 

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

429 

0  430 

1238  431 
(** sort contexts of theorems **) 
432 

433 
(* basic utils *) 

434 

2163  435 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  436 
to improve efficiency a bit*) 
437 

438 
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

439 
 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

440 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  441 
and add_typs_sorts ([], Ss) = Ss 
442 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

443 

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

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

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

447 
 add_term_sorts (Bound _, Ss) = Ss 

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

448 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  449 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
450 

451 
fun add_terms_sorts ([], Ss) = Ss 

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

452 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  453 

1258  454 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
455 

456 
fun add_env_sorts (env, Ss) = 

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

458 
add_typs_sorts (env_codT env, Ss)); 

459 

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

462 

463 
fun add_thms_shyps ([], Ss) = Ss 

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

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

465 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  466 

467 

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

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

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

471 

472 

473 
(* fix_shyps *) 

474 

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

476 
fun fix_shyps thms Ts thm = 

477 
let 

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

481 
in 

1529  482 
Thm {sign = sign, 
2386  483 
der = der, (*No new derivation, as other rules call this*) 
484 
maxidx = maxidx, 

485 
shyps = shyps, hyps = hyps, prop = prop} 

1238  486 
end; 
487 

488 

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

490 

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

492 

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

494 
fun strip_shyps thm = 

495 
let 

1529  496 
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; 
1238  497 
val sorts = add_thm_sorts (thm, []); 
498 
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

499 
val shyps' = filter (fn S => mem_sort(S,sorts) orelse maybe_empty S) shyps; 
1238  500 
in 
1529  501 
Thm {sign = sign, der = der, maxidx = maxidx, 
2386  502 
shyps = 
503 
(if eq_set_sort (shyps',sorts) orelse 

504 
not (!force_strip_shyps) then shyps' 

505 
else (* FIXME tmp *) 

506 
(warning ("Removed sort hypotheses: " ^ 

2962  507 
commas (map Sorts.str_of_sort (shyps' \\ sorts))); 
2386  508 
warning "Let's hope these sorts are nonempty!"; 
1238  509 
sorts)), 
1529  510 
hyps = hyps, 
511 
prop = prop} 

1238  512 
end; 
513 

514 

515 
(* implies_intr_shyps *) 

516 

517 
(*discharge all extra sort hypotheses*) 

518 
fun implies_intr_shyps thm = 

519 
(case extra_shyps thm of 

520 
[] => thm 

521 
 xshyps => 

522 
let 

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

524 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  525 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
526 
val names = 

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

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

529 

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

2671  531 
val sort_hyps = List.concat (map2 mk_insort (tfrees, xshyps)); 
1238  532 
in 
1529  533 
Thm {sign = sign, 
2386  534 
der = infer_derivs (Implies_intr_shyps, [der]), 
535 
maxidx = maxidx, 

536 
shyps = shyps', 

537 
hyps = hyps, 

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

1238  539 
end); 
540 

541 

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

543 

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

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

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

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

547 
fun get_ax [] = raise Match 
1529  548 
 get_ax (thy :: thys) = 
2386  549 
let val {sign, new_axioms, parents, ...} = rep_theory thy 
1529  550 
in case Symtab.lookup (new_axioms, name) of 
2386  551 
Some t => fix_shyps [] [] 
552 
(Thm {sign = sign, 

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

554 
maxidx = maxidx_of_term t, 

555 
shyps = [], 

556 
hyps = [], 

557 
prop = t}) 

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

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

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

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

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

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

564 

1529  565 

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

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

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

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

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

570 

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

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

572 
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

573 
Thm {sign = sign, 
2386  574 
der = Join (Theorem name, [der]), 
575 
maxidx = maxidx, 

576 
shyps = shyps, 

577 
hyps = hyps, 

578 
prop = prop}; 

0  579 

580 

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

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

584 
Thm {sign = sign, 

2386  585 
der = der, (*No derivation recorded!*) 
586 
maxidx = maxidx, 

587 
shyps = shyps, 

588 
hyps = map Term.compress_term hyps, 

589 
prop = Term.compress_term prop}; 

564  590 

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

591 

2509  592 

1529  593 
(*** Meta rules ***) 
0  594 

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

597 
recurrence.*) 

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

599 
(Sign.nodup_Vars prop; 

600 
Thm {sign = sign, 

2386  601 
der = der, 
602 
maxidx = maxidx_of_term prop, 

603 
shyps = shyps, 

604 
hyps = hyps, 

605 
prop = prop}) 

2147  606 
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

607 

1220  608 
(** 'primitive' rules **) 
609 

610 
(*discharge all assumptions t from ts*) 

0  611 
val disch = gen_rem (op aconv); 
612 

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

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

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

1529  621 
else Thm{sign = sign, 
2386  622 
der = infer_derivs (Assume ct, []), 
623 
maxidx = ~1, 

624 
shyps = add_term_sorts(prop,[]), 

625 
hyps = [prop], 

626 
prop = prop} 

0  627 
end; 
628 

1220  629 
(*Implication introduction 
630 
A  B 

631 
 

632 
A ==> B 

633 
*) 

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

635 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  636 
in if T<>propT then 
250  637 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  638 
else fix_shyps [thB] [] 
1529  639 
(Thm{sign = Sign.merge (sign,signA), 
2386  640 
der = infer_derivs (Implies_intr cA, [der]), 
641 
maxidx = Int.max(maxidxA, maxidx), 

642 
shyps = [], 

643 
hyps = disch(hyps,A), 

644 
prop = implies$A$prop}) 

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

647 
end; 

648 

1529  649 

1220  650 
(*Implication elimination 
651 
A ==> B A 

652 
 

653 
B 

654 
*) 

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

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

1220  662 
then fix_shyps [thAB, thA] [] 
663 
(Thm{sign= merge_thm_sgs(thAB,thA), 

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

666 
shyps = [], 

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

668 
prop = B}) 

250  669 
else err("major premise") 
670 
 _ => err("major premise") 

0  671 
end; 
250  672 

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

675 
 

676 
!!x.A 

677 
*) 

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

679 
let val x = term_of cx; 
1238  680 
fun result(a,T) = fix_shyps [th] [] 
1529  681 
(Thm{sign = sign, 
2386  682 
der = infer_derivs (Forall_intr cx, [der]), 
683 
maxidx = maxidx, 

684 
shyps = [], 

685 
hyps = hyps, 

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

0  687 
in case x of 
250  688 
Free(a,T) => 
689 
if exists (apl(x, Logic.occs)) hyps 

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

691 
else result(a,T) 

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

694 
end; 

695 

1220  696 
(*Forall elimination 
697 
!!x.A 

698 
 

699 
A[t/x] 

700 
*) 

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

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

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

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

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

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

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

711 
shyps = [], 

712 
hyps = hyps, 

713 
prop = betapply(A,t)}) 

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

715 
then nodup_Vars thm "forall_elim" 

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

717 
end 

2147  718 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  719 
end 
720 
handle TERM _ => 

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

723 

1220  724 
(* Equality *) 
0  725 

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

729 
der = Join(Axiom(pure_thy, "flexpair_def"), []), 
1529  730 
shyps = [], 
731 
hyps = [], 

732 
maxidx = 0, 

733 
prop = term_of (read_cterm Sign.proto_pure 

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

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

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

738 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  739 
in fix_shyps [] [] 
1529  740 
(Thm{sign= sign, 
2386  741 
der = infer_derivs (Reflexive ct, []), 
742 
shyps = [], 

743 
hyps = [], 

744 
maxidx = maxidx, 

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

0  746 
end; 
747 

748 
(*The symmetry rule 

1220  749 
t==u 
750 
 

751 
u==t 

752 
*) 

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

1238  756 
(*no fix_shyps*) 
2386  757 
Thm{sign = sign, 
758 
der = infer_derivs (Symmetric, [der]), 

759 
maxidx = maxidx, 

760 
shyps = shyps, 

761 
hyps = hyps, 

762 
prop = eq$u$t} 

0  763 
 _ => raise THM("symmetric", 0, [th]); 
764 

765 
(*The transitive rule 

1220  766 
t1==u u==t2 
767 
 

768 
t1==t2 

769 
*) 

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

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

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

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

1220  778 
fix_shyps [th1, th2] [] 
1529  779 
(Thm{sign= merge_thm_sgs(th1,th2), 
2386  780 
der = infer_derivs (Transitive, [der1, der2]), 
2147  781 
maxidx = Int.max(max1,max2), 
2386  782 
shyps = [], 
783 
hyps = union_term(hyps1,hyps2), 

784 
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

785 
in if max1 >= 0 andalso max2 >= 0 
2147  786 
then nodup_Vars thm "transitive" 
787 
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

788 
end 
0  789 
 _ => err"premises" 
790 
end; 

791 

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

794 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  795 
in case t of 
1238  796 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
1529  797 
(Thm{sign = sign, 
2386  798 
der = infer_derivs (Beta_conversion ct, []), 
799 
maxidx = maxidx, 

800 
shyps = [], 

801 
hyps = [], 

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

250  803 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  804 
end; 
805 

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

1220  807 
f(x) == g(x) 
808 
 

809 
f == g 

810 
*) 

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

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

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

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

820 
 Var _ => 

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

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

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

1238  824 
(*no fix_shyps*) 
1529  825 
Thm{sign = sign, 
2386  826 
der = infer_derivs (Extensional, [der]), 
827 
maxidx = maxidx, 

828 
shyps = shyps, 

829 
hyps = hyps, 

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

833 

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

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

1220  836 
t == u 
837 
 

838 
%x.t == %x.u 

839 
*) 

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

841 
let val x = term_of cx; 
250  842 
val (t,u) = Logic.dest_equals prop 
843 
handle TERM _ => 

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

1238  845 
fun result T = fix_shyps [th] [] 
2386  846 
(Thm{sign = sign, 
847 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

848 
maxidx = maxidx, 

849 
shyps = [], 

850 
hyps = hyps, 

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

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

0  853 
in case x of 
250  854 
Free(_,T) => 
855 
if exists (apl(x, Logic.occs)) hyps 

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

857 
else result T 

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

860 
end; 

861 

862 
(*The combination rule 

1220  863 
f==g t==u 
864 
 

865 
f(t)==g(u) 

866 
*) 

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

872 
fun chktypes (f,t) = 
2386  873 
(case fastype_of f of 
874 
Type("fun",[T1,T2]) => 

875 
if T1 <> fastype_of t then 

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

877 
else () 

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

879 
[th1,th2])) 

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

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

882 
let val _ = chktypes (f,t) 
2386  883 
val thm = (*no fix_shyps*) 
884 
Thm{sign = merge_thm_sgs(th1,th2), 

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

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

887 
shyps = union_sort(shyps1,shyps2), 

888 
hyps = union_term(hyps1,hyps2), 

889 
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

890 
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

891 
then nodup_Vars thm "combination" 
2386  892 
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

893 
end 
0  894 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
895 
end; 

896 

897 

898 
(* Equality introduction 

1220  899 
A==>B B==>A 
900 
 

901 
A==B 

902 
*) 

0  903 
fun equal_intr th1 th2 = 
1529  904 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
2386  905 
prop=prop1,...} = th1 
1529  906 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 
2386  907 
prop=prop2,...} = th2; 
1529  908 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
909 
in case (prop1,prop2) of 

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

2386  911 
if A aconv A' andalso B aconv B' 
912 
then 

913 
(*no fix_shyps*) 

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

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

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

917 
shyps = union_sort(shyps1,shyps2), 

918 
hyps = union_term(hyps1,hyps2), 

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

920 
else err"not equal" 

1529  921 
 _ => err"premises" 
922 
end; 

923 

924 

925 
(*The equal propositions rule 

926 
A==B A 

927 
 

928 
B 

929 
*) 

930 
fun equal_elim th1 th2 = 

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

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

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

934 
in case prop1 of 

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

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

937 
fix_shyps [th1, th2] [] 

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

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

941 
shyps = [], 

942 
hyps = union_term(hyps1,hyps2), 

943 
prop = B}) 

1529  944 
 _ => err"major premise" 
945 
end; 

0  946 

1220  947 

948 

0  949 
(**** Derived rules ****) 
950 

1503  951 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  952 
Repeated hypotheses are discharged only once; fold cannot do this*) 
1529  953 
fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = 
1238  954 
implies_intr_hyps (*no fix_shyps*) 
1529  955 
(Thm{sign = sign, 
2386  956 
der = infer_derivs (Implies_intr_hyps, [der]), 
957 
maxidx = maxidx, 

958 
shyps = shyps, 

1529  959 
hyps = disch(As,A), 
2386  960 
prop = implies$A$prop}) 
0  961 
 implies_intr_hyps th = th; 
962 

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

250  964 
Instantiates the theorem and deletes trivial tpairs. 
0  965 
Resulting sequence may contain multiple elements if the tpairs are 
966 
not all flexflex. *) 

1529  967 
fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = 
250  968 
let fun newthm env = 
1529  969 
if Envir.is_empty env then th 
970 
else 

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

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

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

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

1220  976 
in fix_shyps [th] (env_codT env) 
1529  977 
(Thm{sign = sign, 
2386  978 
der = infer_derivs (Flexflex_rule env, [der]), 
979 
maxidx = maxidx_of_term newprop, 

980 
shyps = [], 

981 
hyps = hyps, 

982 
prop = newprop}) 

250  983 
end; 
0  984 
val (tpairs,_) = Logic.strip_flexpairs prop 
985 
in Sequence.maps newthm 

250  986 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  987 
end; 
988 

989 
(*Instantiation of Vars 

1220  990 
A 
991 
 

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

993 
*) 

0  994 

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

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

997 

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

999 
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

1000 
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

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

1004 
end; 

1005 

1006 
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

1007 
let val {T,sign} = rep_ctyp ctyp 
0  1008 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
1009 

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

1011 
Instantiates distinct Vars by terms of same type. 

1012 
Normalizes the new theorem! *) 

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

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

250  1017 
val newprop = 
1018 
Envir.norm_term (Envir.empty 0) 

1019 
(subst_atomic tpairs 

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

1220  1021 
val newth = 
1022 
fix_shyps [th] (map snd vTs) 

1529  1023 
(Thm{sign = newsign, 
2386  1024 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1025 
maxidx = maxidx_of_term newprop, 

1026 
shyps = [], 

1027 
hyps = hyps, 

1028 
prop = newprop}) 

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

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

2147  1033 
else nodup_Vars newth "instantiate" 
0  1034 
end 
250  1035 
handle TERM _ => 
0  1036 
raise THM("instantiate: incompatible signatures",0,[th]) 
2671  1037 
 TYPE (msg,_,_) => raise THM("instantiate: type conflict: " ^ msg, 
1038 
0, [th]); 

0  1039 

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

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

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

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

1238  1046 
else fix_shyps [] [] 
1529  1047 
(Thm{sign = sign, 
2386  1048 
der = infer_derivs (Trivial ct, []), 
1049 
maxidx = maxidx, 

1050 
shyps = [], 

1051 
hyps = [], 

1052 
prop = implies$A$A}) 

0  1053 
end; 
1054 

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

1056 
fun class_triv thy c = 
1529  1057 
let val sign = sign_of thy; 
1058 
val Cterm {t, maxidx, ...} = 

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

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

1061 
in 
1238  1062 
fix_shyps [] [] 
1529  1063 
(Thm {sign = sign, 
2386  1064 
der = infer_derivs (Class_triv(thy,c), []), 
1065 
maxidx = maxidx, 

1066 
shyps = [], 

1067 
hyps = [], 

1068 
prop = t}) 

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

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

1070 

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

1071 

0  1072 
(* Replace all TFrees not in the hyps by new TVars *) 
1529  1073 
fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
0  1074 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1634  1075 
in let val thm = (*no fix_shyps*) 
1529  1076 
Thm{sign = sign, 
2386  1077 
der = infer_derivs (VarifyT, [der]), 
1078 
maxidx = Int.max(0,maxidx), 

1079 
shyps = shyps, 

1080 
hyps = hyps, 

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

0  1085 
end; 
1086 

1087 
(* Replace all TVars by new TFrees *) 

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

1089 
let val prop' = Type.freeze prop 
1238  1090 
in (*no fix_shyps*) 
1529  1091 
Thm{sign = sign, 
2386  1092 
der = infer_derivs (FreezeT, [der]), 
1093 
maxidx = maxidx_of_term prop', 

1094 
shyps = shyps, 

1095 
hyps = hyps, 

1529  1096 
prop = prop'} 
1220  1097 
end; 
0  1098 

1099 

1100 
(*** Inference rules for tactics ***) 

1101 

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

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

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

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

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

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

1108 
end 

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

1110 

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

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

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

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

0  1120 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1121 
in (*no fix_shyps*) 
1529  1122 
Thm{sign = merge_thm_sgs(state,orule), 
2386  1123 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 
1124 
maxidx = maxidx+smax+1, 

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

1125 
shyps=union_sort(sshyps,shyps), 
2386  1126 
hyps=hyps, 
1529  1127 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1128 
map lift_all As, 
1129 
lift_all B)} 

0  1130 
end; 
1131 

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

1133 
fun assumption i state = 

1529  1134 
let val Thm{sign,der,maxidx,hyps,prop,...} = state; 
0  1135 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  1136 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1137 
fix_shyps [state] (env_codT env) 
1529  1138 
(Thm{sign = sign, 
2386  1139 
der = infer_derivs (Assumption (i, Some env), [der]), 
1140 
maxidx = maxidx, 

1141 
shyps = [], 

1142 
hyps = hyps, 

1143 
prop = 

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

1145 
Logic.rule_of (tpairs, Bs, C) 

1146 
else (*normalize the new rule fully*) 

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

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

1150 
(Sequence.mapp newth 

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

0  1153 
in addprfs (Logic.assum_pairs Bi) end; 
1154 

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

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

1220  1161 
then fix_shyps [state] [] 
1529  1162 
(Thm{sign = sign, 
2386  1163 
der = infer_derivs (Assumption (i,None), [der]), 
1164 
maxidx = maxidx, 

1165 
shyps = [], 

1166 
hyps = hyps, 

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

0  1168 
else raise THM("eq_assumption", 0, [state]) 
1169 
end; 

1170 

1171 

2671  1172 
(*For rotate_tac: fast rotation of assumptions of subgoal i*) 
1173 
fun rotate_rule k i state = 

1174 
let val Thm{sign,der,maxidx,hyps,prop,shyps} = state; 

1175 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 

1176 
val params = Logic.strip_params Bi 

1177 
and asms = Logic.strip_assums_hyp Bi 

1178 
and concl = Logic.strip_assums_concl Bi 

1179 
val n = length asms 

1180 
fun rot m = if 0=m orelse m=n then Bi 

1181 
else if 0<m andalso m<n 

1182 
then list_all 

1183 
(params, 

1184 
Logic.list_implies(List.drop(asms, m) @ 

1185 
List.take(asms, m), 

1186 
concl)) 

1187 
else raise THM("rotate_rule", m, [state]) 

1188 
in Thm{sign = sign, 

1189 
der = infer_derivs (Rotate_rule (k,i), [der]), 

1190 
maxidx = maxidx, 

1191 
shyps = shyps, 

1192 
hyps = hyps, 

1193 
prop = Logic.rule_of(tpairs, Bs@[rot (if k<0 then n+k else k)], C)} 

1194 
end; 

1195 

1196 

0  1197 
(** User renaming of parameters in a subgoal **) 
1198 

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

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

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

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

1203 
fun rename_params_rule (cs, i) state = 

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

1207 
val short = length iparams  length cs 

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

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

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

250  1213 
in 
0  1214 
case findrep cs of 
1215 
c::_ => error ("Bound variables not distinct: " ^ c) 

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

1216 
 [] => (case cs inter_string freenames of 
0  1217 
a::_ => error ("Bound/Free variable clash: " ^ a) 
1220  1218 
 [] => fix_shyps [state] [] 
2386  1219 
(Thm{sign = sign, 
1220 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1221 
maxidx = maxidx, 

1222 
shyps = [], 

1223 
hyps = hyps, 

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

0  1225 
end; 
1226 

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

1228 

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

1232 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1233 
else (x,y)::al) 
0  1234 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1235 
 match_bvs(_,_,al) = al; 

1236 

1237 
(* strip abstractions created by parameters *) 

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

1239 

1240 

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

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

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

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

1248 
 strip(A,_) = f A 

0  1249 
in strip end; 
1250 

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

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

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

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

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

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

1258 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1261 
(case assoc(al,x) of 

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

1262 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1263 
else Var((y,i),T) 
1264 
 None=> t) 

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

1266 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1267 
T, rename t) 
0  1268 
 rename(f$t) = rename f $ rename t 
1269 
 rename(t) = t; 

250  1270 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1271 
in strip_ren end; 
1272 

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

1274 
fun rename_bvars(dpairs, tpairs, B) = 

250  1275 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1276 

1277 

1278 
(*** RESOLUTION ***) 

1279 

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

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

1281 

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

250  1284 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1285 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1286 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1287 
Const("all",_)$Abs(_,_,t2)) = 
0  1288 
let val (B1,B2) = strip_assums2 (t1,t2) 
1289 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1290 
 strip_assums2 BB = BB; 

1291 

1292 

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

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

1294 
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

1295 
 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

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

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

1300 
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

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

1303 
 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

1304 

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

1305 

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

1310 
If eres_flg then simultaneously proves A1 by assumption. 

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

1529  1314 
local open Sequence; exception COMPOSE 
0  1315 
in 
250  1316 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1317 
(eres_flg, orule, nsubgoal) = 
1529  1318 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1319 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

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

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

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

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

1329 
val normp = 

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

1331 
else 

1332 
let val ntps = map (pairself normt) tpairs 

2147  1333 
in if Envir.above (smax, env) then 
1238  1334 
(*no assignments in state; normalize the rule only*) 
1335 
if lifted 

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

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

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

1341 
end 

1258  1342 
val th = (*tuned fix_shyps*) 
1529  1343 
Thm{sign = sign, 
2386  1344 
der = infer_derivs (Bicompose(match, eres_flg, 
1345 
1 + length Bs, nsubgoal, env), 

1346 
[rder,sder]), 

1347 
maxidx = maxidx, 

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

1349 
hyps = union_term(rhyps,shyps), 

1350 
prop = Logic.rule_of normp} 

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

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

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

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

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

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

0  1362 
end; 
2147  1363 
val env = Envir.empty(Int.max(rmax,smax)); 
0  1364 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 
1365 
val dpairs = BBi :: (rtpairs@stpairs); 

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

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

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

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

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

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

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

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

0  1375 
fun eres [] = raise THM("bicompose: no premises", 0, [orule,state]) 