author  paulson 
Tue, 22 Jul 1997 11:14:18 +0200  
changeset 3538  ed9de44032e0 
parent 3529  31186470665f 
child 3550  2c833cb21f8d 
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 

3061  98 
val force_strip_shyps : bool ref (* FIXME tmp (since 1995/08/01) *) 
1238  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 

3061  491 
val force_strip_shyps = ref true; (* FIXME tmp (since 1995/08/01) *) 
1238  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' 

3061  505 
else (* FIXME tmp (since 1995/08/01) *) 
2386  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 
3529  630 
[A] 
631 
: 

632 
B 

1220  633 
 
634 
A ==> B 

635 
*) 

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

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

644 
shyps = [], 

645 
hyps = disch(hyps,A), 

646 
prop = implies$A$prop}) 

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

649 
end; 

650 

1529  651 

1220  652 
(*Implication elimination 
653 
A ==> B A 

654 
 

655 
B 

656 
*) 

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

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

1220  664 
then fix_shyps [thAB, thA] [] 
665 
(Thm{sign= merge_thm_sgs(thAB,thA), 

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

668 
shyps = [], 

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

670 
prop = B}) 

250  671 
else err("major premise") 
672 
 _ => err("major premise") 

0  673 
end; 
250  674 

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

677 
 

678 
!!x.A 

679 
*) 

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

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

686 
shyps = [], 

687 
hyps = hyps, 

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

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

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

693 
else result(a,T) 

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

696 
end; 

697 

1220  698 
(*Forall elimination 
699 
!!x.A 

700 
 

701 
A[t/x] 

702 
*) 

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

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

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

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

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

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

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

713 
shyps = [], 

714 
hyps = hyps, 

715 
prop = betapply(A,t)}) 

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

717 
then nodup_Vars thm "forall_elim" 

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

719 
end 

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

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

725 

1220  726 
(* Equality *) 
0  727 

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

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

734 
maxidx = 0, 

735 
prop = term_of (read_cterm Sign.proto_pure 

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

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

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

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

745 
hyps = [], 

746 
maxidx = maxidx, 

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

0  748 
end; 
749 

750 
(*The symmetry rule 

1220  751 
t==u 
752 
 

753 
u==t 

754 
*) 

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

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

761 
maxidx = maxidx, 

762 
shyps = shyps, 

763 
hyps = hyps, 

764 
prop = eq$u$t} 

0  765 
 _ => raise THM("symmetric", 0, [th]); 
766 

767 
(*The transitive rule 

1220  768 
t1==u u==t2 
769 
 

770 
t1==t2 

771 
*) 

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

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

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

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

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

786 
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

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

790 
end 
0  791 
 _ => err"premises" 
792 
end; 

793 

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

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

802 
shyps = [], 

803 
hyps = [], 

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

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

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

1220  809 
f(x) == g(x) 
810 
 

811 
f == g 

812 
*) 

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

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

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

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

822 
 Var _ => 

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

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

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

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

830 
shyps = shyps, 

831 
hyps = hyps, 

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

835 

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

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

1220  838 
t == u 
839 
 

840 
%x.t == %x.u 

841 
*) 

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

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

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

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

850 
maxidx = maxidx, 

851 
shyps = [], 

852 
hyps = hyps, 

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

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

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

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

859 
else result T 

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

862 
end; 

863 

864 
(*The combination rule 

3529  865 
f == g t == u 
866 
 

867 
f(t) == g(u) 

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

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

877 
if T1 <> fastype_of t then 

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

879 
else () 

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

881 
[th1,th2])) 

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

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

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

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

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

889 
shyps = union_sort(shyps1,shyps2), 

890 
hyps = union_term(hyps1,hyps2), 

891 
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

892 
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

893 
then nodup_Vars thm "combination" 
2386  894 
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

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

898 

899 

900 
(* Equality introduction 

3529  901 
A ==> B B ==> A 
902 
 

903 
A == B 

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

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

2386  913 
if A aconv A' andalso B aconv B' 
914 
then 

915 
(*no fix_shyps*) 

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

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

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

919 
shyps = union_sort(shyps1,shyps2), 

920 
hyps = union_term(hyps1,hyps2), 

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

922 
else err"not equal" 

1529  923 
 _ => err"premises" 
924 
end; 

925 

926 

927 
(*The equal propositions rule 

3529  928 
A == B A 
1529  929 
 
930 
B 

931 
*) 

932 
fun equal_elim th1 th2 = 

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

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

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

936 
in case prop1 of 

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

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

939 
fix_shyps [th1, th2] [] 

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

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

943 
shyps = [], 

944 
hyps = union_term(hyps1,hyps2), 

945 
prop = B}) 

1529  946 
 _ => err"major premise" 
947 
end; 

0  948 

1220  949 

950 

0  951 
(**** Derived rules ****) 
952 

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

960 
shyps = shyps, 

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

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

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

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

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

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

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

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

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

982 
shyps = [], 

983 
hyps = hyps, 

984 
prop = newprop}) 

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

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

991 
(*Instantiation of Vars 

1220  992 
A 
993 
 

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

995 
*) 

0  996 

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

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

999 

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

1001 
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

1002 
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

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

1006 
end; 

1007 

1008 
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

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

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

1013 
Instantiates distinct Vars by terms of same type. 

1014 
Normalizes the new theorem! *) 

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

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

250  1019 
val newprop = 
1020 
Envir.norm_term (Envir.empty 0) 

1021 
(subst_atomic tpairs 

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

1220  1023 
val newth = 
1024 
fix_shyps [th] (map snd vTs) 

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

1028 
shyps = [], 

1029 
hyps = hyps, 

1030 
prop = newprop}) 

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

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

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

0  1041 

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

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

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

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

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

1052 
shyps = [], 

1053 
hyps = [], 

1054 
prop = implies$A$A}) 

0  1055 
end; 
1056 

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

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

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

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

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

1068 
shyps = [], 

1069 
hyps = [], 

1070 
prop = t}) 

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

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

1072 

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

1073 

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

1081 
shyps = shyps, 

1082 
hyps = hyps, 

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

0  1087 
end; 
1088 

1089 
(* Replace all TVars by new TFrees *) 

1529  1090 
fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
3410  1091 
let val (prop',_) = Type.freeze_thaw prop 
1238  1092 
in (*no fix_shyps*) 
1529  1093 
Thm{sign = sign, 
2386  1094 
der = infer_derivs (FreezeT, [der]), 
1095 
maxidx = maxidx_of_term prop', 

1096 
shyps = shyps, 

1097 
hyps = hyps, 

1529  1098 
prop = prop'} 
1220  1099 
end; 
0  1100 

1101 

1102 
(*** Inference rules for tactics ***) 

1103 

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

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

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

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

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

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

1110 
end 

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

1112 

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

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

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

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

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

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

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

0  1132 
end; 
1133 

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

1135 
fun assumption i state = 

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

1143 
shyps = [], 

1144 
hyps = hyps, 

1145 
prop = 

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

1147 
Logic.rule_of (tpairs, Bs, C) 

1148 
else (*normalize the new rule fully*) 

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

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

1152 
(Sequence.mapp newth 

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

0  1155 
in addprfs (Logic.assum_pairs Bi) end; 
1156 

250  1157 
(*Solve subgoal Bi of proof state B1...Bn/C by assumption. 
0  1158 
Checks if Bi's conclusion is alphaconvertible to one of its assumptions*) 
1159 
fun eq_assumption 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 
in if exists (op aconv) (Logic.assum_pairs Bi) 

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

1167 
shyps = [], 

1168 
hyps = hyps, 

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

0  1170 
else raise THM("eq_assumption", 0, [state]) 
1171 
end; 

1172 

1173 

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

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

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

1178 
val params = Logic.strip_params Bi 

1179 
and asms = Logic.strip_assums_hyp Bi 

1180 
and concl = Logic.strip_assums_concl Bi 

1181 
val n = length asms 

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

1183 
else if 0<m andalso m<n 

1184 
then list_all 

1185 
(params, 

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

1187 
List.take(asms, m), 

1188 
concl)) 

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

1190 
in Thm{sign = sign, 

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

1192 
maxidx = maxidx, 

1193 
shyps = shyps, 

1194 
hyps = hyps, 

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

1196 
end; 

1197 

1198 

0  1199 
(** User renaming of parameters in a subgoal **) 
1200 

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

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

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

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

1205 
fun rename_params_rule (cs, i) state = 

3037
99ed078e6ae7
rename_params_rule used to check if the new name clashed with a free name in
nipkow
parents:
3012
diff
changeset

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

1209 
val short = length iparams  length cs 

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

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

3037
99ed078e6ae7
rename_params_rule used to check if the new name clashed with a free name in
nipkow
parents:
3012
diff
changeset

1213 
val freenames = map (#1 o dest_Free) (term_frees Bi) 
0  1214 
val newBi = Logic.list_rename_params (newnames, Bi) 
250  1215 
in 
0  1216 
case findrep cs of 
1217 
c::_ => error ("Bound variables not distinct: " ^ c) 

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

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

1223 
maxidx = maxidx, 

1224 
shyps = [], 

1225 
hyps = hyps, 

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

0  1227 
end; 
1228 

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

1230 

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

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

1238 

1239 
(* strip abstractions created by parameters *) 

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

1241 

1242 

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

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

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

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

1250 
 strip(A,_) = f A 

0  1251 
in strip end; 
1252 

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

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

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

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

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

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

1260 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1263 
(case assoc(al,x) of 

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

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

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

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

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

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

1276 
fun rename_bvars(dpairs, tpairs, B) = 

250  1277 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1278 

1279 

1280 
(*** RESOLUTION ***) 

1281 

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

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

1283 

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

250  1286 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1287 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

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

1292 
 strip_assums2 BB = BB; 

1293 

1294 

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

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

1296 
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

1297 
 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

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

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

1302 
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

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

1305 
 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

1306 

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

1307 

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

1312 
If eres_flg then simultaneously proves A1 by assumption. 

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

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

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

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

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

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

1331 
val normp = 

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

1333 
else 

1334 
let val ntps = map (pairself normt) tpairs 

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

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

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

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

1343 
end 

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

1348 
[rder,sder]), 

1349 
maxidx = maxidx, 

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

1351 
hyps = union_term(rhyps,shyps), 

1352 
prop = Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

9b5a069285ce
ext 