author  paulson 
Wed, 23 Jul 1997 11:54:32 +0200  
changeset 3565  c64410e701fb 
parent 3558  258eee1a056e 
child 3577  9715b6e3ec5f 
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*) 

3550  143 
exception SIMPLIFIER of string * thm 
1160  144 
type meta_simpset 
3550  145 
val dest_mss : meta_simpset > 
146 
{simps: thm list, congs: thm list, procs: (string * cterm list) list} 

1238  147 
val empty_mss : meta_simpset 
3550  148 
val merge_mss : meta_simpset * meta_simpset > meta_simpset 
1238  149 
val add_simps : meta_simpset * thm list > meta_simpset 
150 
val del_simps : meta_simpset * thm list > meta_simpset 

151 
val mss_of : thm list > meta_simpset 

152 
val add_congs : meta_simpset * thm list > meta_simpset 

2626  153 
val del_congs : meta_simpset * thm list > meta_simpset 
2509  154 
val add_simprocs : meta_simpset * 
3550  155 
(string * cterm list * (Sign.sg > term > thm option) * stamp) list > meta_simpset 
2509  156 
val del_simprocs : meta_simpset * 
3550  157 
(string * cterm list * (Sign.sg > term > thm option) * stamp) list > meta_simpset 
1238  158 
val add_prems : meta_simpset * thm list > meta_simpset 
159 
val prems_of_mss : meta_simpset > thm list 

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

161 
val mk_rews_of_mss : meta_simpset > thm > thm list 

2509  162 
val set_termless : meta_simpset * (term * term > bool) > meta_simpset 
1238  163 
val trace_simp : bool ref 
164 
val rewrite_cterm : bool * bool > meta_simpset > 

1529  165 
(meta_simpset > thm > thm option) > cterm > thm 
1539  166 

2386  167 
val invoke_oracle : theory * Sign.sg * exn > thm 
250  168 
end; 
0  169 

3550  170 
structure Thm: THM = 
0  171 
struct 
250  172 

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

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

174 

250  175 
(** certified types **) 
176 

177 
(*certified typs under a signature*) 

178 

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

180 

181 
fun rep_ctyp (Ctyp args) = args; 

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

183 

184 
fun ctyp_of sign T = 

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

186 

187 
fun read_ctyp sign s = 

188 
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

189 

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

190 

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

191 

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

193 

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

195 

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

197 

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

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

200 

2671  201 
fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T}; 
202 

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

205 
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

206 
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

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

208 

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

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

211 

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

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

213 

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

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

215 
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

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

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

218 
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

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

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

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

222 
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

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

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

225 

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

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

227 
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

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

229 
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

230 
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

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

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

233 

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

236 
if maxidx = ~1 then ct 

237 
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

238 

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

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

240 
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

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

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

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

245 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  246 

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

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

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

252 

2509  253 

254 

574  255 
(** read cterms **) (*exception ERROR*) 
250  256 

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

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

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

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

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

269 

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

270 
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

271 

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

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

273 
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

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

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

276 
let 
2979  277 
val {tsig, syn, ...} = Sign.rep_sg sign; 
278 
fun read (b, T) = 

279 
(case Syntax.read syn T b of 

280 
[t] => t 

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

282 

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

284 
val prT = Sign.pretty_typ sign; 

285 
val (us, _) = 

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

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

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

289 
in map (cterm_of sign) us end 

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

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

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

292 

250  293 

294 

1529  295 
(*** Derivations ***) 
296 

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

298 
executed in ML.*) 

299 
datatype rule = 

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

1529  302 
(*Axioms/theorems*) 
2386  303 
 Axiom of theory * string 
304 
 Theorem of string 

1529  305 
(*primitive inferences and compound versions of them*) 
2386  306 
 Assume of cterm 
307 
 Implies_intr of cterm 

1529  308 
 Implies_intr_shyps 
309 
 Implies_intr_hyps 

310 
 Implies_elim 

2386  311 
 Forall_intr of cterm 
312 
 Forall_elim of cterm 

313 
 Reflexive of cterm 

1529  314 
 Symmetric 
315 
 Transitive 

2386  316 
 Beta_conversion of cterm 
1529  317 
 Extensional 
2386  318 
 Abstract_rule of string * cterm 
1529  319 
 Combination 
320 
 Equal_intr 

321 
 Equal_elim 

322 
(*derived rules for tactical proof*) 

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

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

326 
 Lift_rule of cterm * int 

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

2671  328 
 Rotate_rule of int * int 
2386  329 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
330 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  332 
(*other derived rules*) 
2509  333 
 Class_triv of theory * class 
1529  334 
 VarifyT 
335 
 FreezeT 

336 
(*for the simplifier*) 

2386  337 
 RewriteC of cterm 
338 
 CongC of cterm 

339 
 Rewrite_cterm of cterm 

1529  340 
(*Logical identities, recorded since they are part of the proof process*) 
2386  341 
 Rename_params_rule of string list * int; 
1529  342 

343 

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

344 
type deriv = rule mtree; 
1529  345 

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

346 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  347 

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

348 
val keep_derivs = ref MinDeriv; 
1529  349 

350 

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

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

352 
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

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

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

355 
(case der of 
2386  356 
Join (Oracle _, _) => der :: squash_derivs ders 
357 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

358 
then der :: squash_derivs ders 

359 
else squash_derivs (der'::ders) 

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

361 
then der :: squash_derivs ders 

362 
else squash_derivs ders 

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

364 
 _ => der :: squash_derivs ders); 

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

365 

1529  366 

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

368 
val min_infer = Join (MinProof, []); 
1529  369 

370 
(*Make a minimal inference*) 

371 
fun make_min_infer [] = min_infer 

372 
 make_min_infer [der] = der 

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

373 
 make_min_infer ders = Join (MinProof, ders); 
1529  374 

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

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

377 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  378 
else make_min_infer (squash_derivs ders); 
379 

380 

2509  381 

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

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

383 

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

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

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

389 
hyps: term list, (*hypotheses*) 

390 
prop: term}; (*conclusion*) 

0  391 

250  392 
fun rep_thm (Thm args) = args; 
0  393 

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

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

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

398 
hyps = map (ctermf ~1) hyps, 

399 
prop = ctermf maxidx prop} 

1517  400 
end; 
401 

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

402 
(*errors involving theorems*) 
0  403 
exception THM of string * int * thm list; 
404 

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

405 

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

406 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 
0  407 

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

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

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

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

412 

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 tpairs*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

415 
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

416 

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

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

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

419 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  420 

421 
(*counts premises in a rule*) 

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

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

423 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  424 

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

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

426 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  427 

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

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

430 
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

431 

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

432 

0  433 

1238  434 
(** sort contexts of theorems **) 
435 

436 
(* basic utils *) 

437 

2163  438 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  439 
to improve efficiency a bit*) 
440 

441 
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

442 
 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

443 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  444 
and add_typs_sorts ([], Ss) = Ss 
445 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

446 

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

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

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

450 
 add_term_sorts (Bound _, Ss) = Ss 

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

451 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  452 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
453 

454 
fun add_terms_sorts ([], Ss) = Ss 

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

455 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  456 

1258  457 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
458 

459 
fun add_env_sorts (env, Ss) = 

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

461 
add_typs_sorts (env_codT env, Ss)); 

462 

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

465 

466 
fun add_thms_shyps ([], Ss) = Ss 

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

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

468 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  469 

470 

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

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

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

474 

475 

476 
(* fix_shyps *) 

477 

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

479 
fun fix_shyps thms Ts thm = 

480 
let 

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

484 
in 

1529  485 
Thm {sign = sign, 
2386  486 
der = der, (*No new derivation, as other rules call this*) 
487 
maxidx = maxidx, 

488 
shyps = shyps, hyps = hyps, prop = prop} 

1238  489 
end; 
490 

491 

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

493 

3061  494 
val force_strip_shyps = ref true; (* FIXME tmp (since 1995/08/01) *) 
1238  495 

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

497 
fun strip_shyps thm = 

498 
let 

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

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

507 
not (!force_strip_shyps) then shyps' 

3061  508 
else (* FIXME tmp (since 1995/08/01) *) 
2386  509 
(warning ("Removed sort hypotheses: " ^ 
2962  510 
commas (map Sorts.str_of_sort (shyps' \\ sorts))); 
2386  511 
warning "Let's hope these sorts are nonempty!"; 
1238  512 
sorts)), 
1529  513 
hyps = hyps, 
514 
prop = prop} 

1238  515 
end; 
516 

517 

518 
(* implies_intr_shyps *) 

519 

520 
(*discharge all extra sort hypotheses*) 

521 
fun implies_intr_shyps thm = 

522 
(case extra_shyps thm of 

523 
[] => thm 

524 
 xshyps => 

525 
let 

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

527 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  528 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
529 
val names = 

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

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

532 

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

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

539 
shyps = shyps', 

540 
hyps = hyps, 

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

1238  542 
end); 
543 

544 

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

546 

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

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

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

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

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

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

557 
maxidx = maxidx_of_term t, 

558 
shyps = [], 

559 
hyps = [], 

560 
prop = t}) 

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

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

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

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

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

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

567 

1529  568 

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

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

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

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

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

573 

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

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

575 
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

576 
Thm {sign = sign, 
2386  577 
der = Join (Theorem name, [der]), 
578 
maxidx = maxidx, 

579 
shyps = shyps, 

580 
hyps = hyps, 

581 
prop = prop}; 

0  582 

583 

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

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

587 
Thm {sign = sign, 

2386  588 
der = der, (*No derivation recorded!*) 
589 
maxidx = maxidx, 

590 
shyps = shyps, 

591 
hyps = map Term.compress_term hyps, 

592 
prop = Term.compress_term prop}; 

564  593 

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

594 

2509  595 

1529  596 
(*** Meta rules ***) 
0  597 

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

600 
recurrence.*) 

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

602 
(Sign.nodup_Vars prop; 

603 
Thm {sign = sign, 

2386  604 
der = der, 
605 
maxidx = maxidx_of_term prop, 

606 
shyps = shyps, 

607 
hyps = hyps, 

608 
prop = prop}) 

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

610 

1220  611 
(** 'primitive' rules **) 
612 

613 
(*discharge all assumptions t from ts*) 

0  614 
val disch = gen_rem (op aconv); 
615 

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

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

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

1529  624 
else Thm{sign = sign, 
2386  625 
der = infer_derivs (Assume ct, []), 
626 
maxidx = ~1, 

627 
shyps = add_term_sorts(prop,[]), 

628 
hyps = [prop], 

629 
prop = prop} 

0  630 
end; 
631 

1220  632 
(*Implication introduction 
3529  633 
[A] 
634 
: 

635 
B 

1220  636 
 
637 
A ==> B 

638 
*) 

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

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

647 
shyps = [], 

648 
hyps = disch(hyps,A), 

649 
prop = implies$A$prop}) 

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

652 
end; 

653 

1529  654 

1220  655 
(*Implication elimination 
656 
A ==> B A 

657 
 

658 
B 

659 
*) 

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

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

1220  667 
then fix_shyps [thAB, thA] [] 
668 
(Thm{sign= merge_thm_sgs(thAB,thA), 

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

671 
shyps = [], 

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

673 
prop = B}) 

250  674 
else err("major premise") 
675 
 _ => err("major premise") 

0  676 
end; 
250  677 

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

680 
 

681 
!!x.A 

682 
*) 

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

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

689 
shyps = [], 

690 
hyps = hyps, 

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

0  692 
in case x of 
250  693 
Free(a,T) => 
694 
if exists (apl(x, Logic.occs)) hyps 

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

696 
else result(a,T) 

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

699 
end; 

700 

1220  701 
(*Forall elimination 
702 
!!x.A 

703 
 

704 
A[t/x] 

705 
*) 

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

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

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

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

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

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

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

716 
shyps = [], 

717 
hyps = hyps, 

718 
prop = betapply(A,t)}) 

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

720 
then nodup_Vars thm "forall_elim" 

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

722 
end 

2147  723 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  724 
end 
725 
handle TERM _ => 

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

728 

1220  729 
(* Equality *) 
0  730 

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

734 
der = Join(Axiom(pure_thy, "flexpair_def"), []), 
1529  735 
shyps = [], 
736 
hyps = [], 

737 
maxidx = 0, 

738 
prop = term_of (read_cterm Sign.proto_pure 

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

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

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

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

748 
hyps = [], 

749 
maxidx = maxidx, 

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

0  751 
end; 
752 

753 
(*The symmetry rule 

1220  754 
t==u 
755 
 

756 
u==t 

757 
*) 

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

1238  761 
(*no fix_shyps*) 
2386  762 
Thm{sign = sign, 
763 
der = infer_derivs (Symmetric, [der]), 

764 
maxidx = maxidx, 

765 
shyps = shyps, 

766 
hyps = hyps, 

767 
prop = eq$u$t} 

0  768 
 _ => raise THM("symmetric", 0, [th]); 
769 

770 
(*The transitive rule 

1220  771 
t1==u u==t2 
772 
 

773 
t1==t2 

774 
*) 

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

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

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

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

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

789 
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

790 
in if max1 >= 0 andalso max2 >= 0 
2147  791 
then nodup_Vars thm "transitive" 
792 
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

793 
end 
0  794 
 _ => err"premises" 
795 
end; 

796 

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

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

805 
shyps = [], 

806 
hyps = [], 

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

250  808 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  809 
end; 
810 

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

1220  812 
f(x) == g(x) 
813 
 

814 
f == g 

815 
*) 

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

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

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

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

825 
 Var _ => 

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

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

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

1238  829 
(*no fix_shyps*) 
1529  830 
Thm{sign = sign, 
2386  831 
der = infer_derivs (Extensional, [der]), 
832 
maxidx = maxidx, 

833 
shyps = shyps, 

834 
hyps = hyps, 

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

838 

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

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

1220  841 
t == u 
842 
 

843 
%x.t == %x.u 

844 
*) 

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

846 
let val x = term_of cx; 
250  847 
val (t,u) = Logic.dest_equals prop 
848 
handle TERM _ => 

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

1238  850 
fun result T = fix_shyps [th] [] 
2386  851 
(Thm{sign = sign, 
852 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

853 
maxidx = maxidx, 

854 
shyps = [], 

855 
hyps = hyps, 

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

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

0  858 
in case x of 
250  859 
Free(_,T) => 
860 
if exists (apl(x, Logic.occs)) hyps 

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

862 
else result T 

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

865 
end; 

866 

867 
(*The combination rule 

3529  868 
f == g t == u 
869 
 

870 
f(t) == g(u) 

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

877 
fun chktypes (f,t) = 
2386  878 
(case fastype_of f of 
879 
Type("fun",[T1,T2]) => 

880 
if T1 <> fastype_of t then 

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

882 
else () 

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

884 
[th1,th2])) 

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

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

887 
let val _ = chktypes (f,t) 
2386  888 
val thm = (*no fix_shyps*) 
889 
Thm{sign = merge_thm_sgs(th1,th2), 

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

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

892 
shyps = union_sort(shyps1,shyps2), 

893 
hyps = union_term(hyps1,hyps2), 

894 
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

895 
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

896 
then nodup_Vars thm "combination" 
2386  897 
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

898 
end 
0  899 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
900 
end; 

901 

902 

903 
(* Equality introduction 

3529  904 
A ==> B B ==> A 
905 
 

906 
A == B 

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

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

2386  916 
if A aconv A' andalso B aconv B' 
917 
then 

918 
(*no fix_shyps*) 

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

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

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

922 
shyps = union_sort(shyps1,shyps2), 

923 
hyps = union_term(hyps1,hyps2), 

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

925 
else err"not equal" 

1529  926 
 _ => err"premises" 
927 
end; 

928 

929 

930 
(*The equal propositions rule 

3529  931 
A == B A 
1529  932 
 
933 
B 

934 
*) 

935 
fun equal_elim th1 th2 = 

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

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

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

939 
in case prop1 of 

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

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

942 
fix_shyps [th1, th2] [] 

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

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

946 
shyps = [], 

947 
hyps = union_term(hyps1,hyps2), 

948 
prop = B}) 

1529  949 
 _ => err"major premise" 
950 
end; 

0  951 

1220  952 

953 

0  954 
(**** Derived rules ****) 
955 

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

963 
shyps = shyps, 

1529  964 
hyps = disch(As,A), 
2386  965 
prop = implies$A$prop}) 
0  966 
 implies_intr_hyps th = th; 
967 

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

250  969 
Instantiates the theorem and deletes trivial tpairs. 
0  970 
Resulting sequence may contain multiple elements if the tpairs are 
971 
not all flexflex. *) 

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

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

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

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

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

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

985 
shyps = [], 

986 
hyps = hyps, 

987 
prop = newprop}) 

250  988 
end; 
0  989 
val (tpairs,_) = Logic.strip_flexpairs prop 
990 
in Sequence.maps newthm 

250  991 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  992 
end; 
993 

994 
(*Instantiation of Vars 

1220  995 
A 
996 
 

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

998 
*) 

0  999 

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

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

1002 

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

1004 
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

1005 
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

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

1009 
end; 

1010 

1011 
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

1012 
let val {T,sign} = rep_ctyp ctyp 
0  1013 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
1014 

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

1016 
Instantiates distinct Vars by terms of same type. 

1017 
Normalizes the new theorem! *) 

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

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

250  1022 
val newprop = 
1023 
Envir.norm_term (Envir.empty 0) 

1024 
(subst_atomic tpairs 

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

1220  1026 
val newth = 
1027 
fix_shyps [th] (map snd vTs) 

1529  1028 
(Thm{sign = newsign, 
2386  1029 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1030 
maxidx = maxidx_of_term newprop, 

1031 
shyps = [], 

1032 
hyps = hyps, 

1033 
prop = newprop}) 

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

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

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

0  1044 

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

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

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

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

1238  1051 
else fix_shyps [] [] 
1529  1052 
(Thm{sign = sign, 
2386  1053 
der = infer_derivs (Trivial ct, []), 
1054 
maxidx = maxidx, 

1055 
shyps = [], 

1056 
hyps = [], 

1057 
prop = implies$A$A}) 

0  1058 
end; 
1059 

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

1061 
fun class_triv thy c = 
1529  1062 
let val sign = sign_of thy; 
1063 
val Cterm {t, maxidx, ...} = 

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

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

1066 
in 
1238  1067 
fix_shyps [] [] 
1529  1068 
(Thm {sign = sign, 
2386  1069 
der = infer_derivs (Class_triv(thy,c), []), 
1070 
maxidx = maxidx, 

1071 
shyps = [], 

1072 
hyps = [], 

1073 
prop = t}) 

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

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

1075 

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

1076 

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

1084 
shyps = shyps, 

1085 
hyps = hyps, 

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

0  1090 
end; 
1091 

1092 
(* Replace all TVars by new TFrees *) 

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

1099 
shyps = shyps, 

1100 
hyps = hyps, 

1529  1101 
prop = prop'} 
1220  1102 
end; 
0  1103 

1104 

1105 
(*** Inference rules for tactics ***) 

1106 

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

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

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

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

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

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

1113 
end 

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

1115 

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

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

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

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

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

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

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

0  1135 
end; 
1136 

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

1138 
fun assumption i state = 

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

1146 
shyps = [], 

1147 
hyps = hyps, 

1148 
prop = 

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

1150 
Logic.rule_of (tpairs, Bs, C) 

1151 
else (*normalize the new rule fully*) 

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

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

1155 
(Sequence.mapp newth 

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

0  1158 
in addprfs (Logic.assum_pairs Bi) end; 
1159 

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

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

1220  1166 
then fix_shyps [state] [] 
1529  1167 
(Thm{sign = sign, 
2386  1168 
der = infer_derivs (Assumption (i,None), [der]), 
1169 
maxidx = maxidx, 

1170 
shyps = [], 

1171 
hyps = hyps, 

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

0  1173 
else raise THM("eq_assumption", 0, [state]) 
1174 
end; 

1175 

1176 

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

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

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

1181 
val params = Logic.strip_params Bi 

1182 
and asms = Logic.strip_assums_hyp Bi 

1183 
and concl = Logic.strip_assums_concl Bi 

1184 
val n = length asms 

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

1186 
else if 0<m andalso m<n 

1187 
then list_all 

1188 
(params, 

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

1190 
List.take(asms, m), 

1191 
concl)) 

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

1193 
in Thm{sign = sign, 

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

1195 
maxidx = maxidx, 

1196 
shyps = shyps, 

1197 
hyps = hyps, 

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

1199 
end; 

1200 

1201 

0  1202 
(** User renaming of parameters in a subgoal **) 
1203 

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

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

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

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

1208 
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

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

1212 
val short = length iparams  length cs 

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

1215 
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

1216 
val freenames = map (#1 o dest_Free) (term_frees Bi) 
0  1217 
val newBi = Logic.list_rename_params (newnames, Bi) 
250  1218 
in 
0  1219 
case findrep cs of 
3565
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1220 
c::_ => (warning ("Can't rename. Bound variables not distinct: " ^ c); 
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

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

1222 
 [] => (case cs inter_string freenames of 
3565
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1223 
a::_ => (warning ("Can't rename. Bound/Free variable clash: " ^ a); 
c64410e701fb
Now rename_params_rule merely issues warningsand does nothingif the
paulson
parents:
3558
diff
changeset

1224 
state) 
1220  1225 
 [] => fix_shyps [state] [] 
2386  1226 
(Thm{sign = sign, 
1227 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1228 
maxidx = maxidx, 

1229 
shyps = [], 

1230 
hyps = hyps, 

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

0  1232 
end; 
1233 

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

1235 

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

1239 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1240 
else (x,y)::al) 
0  1241 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1242 
 match_bvs(_,_,al) = al; 

1243 

1244 
(* strip abstractions created by parameters *) 

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

1246 

1247 

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

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

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

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

1255 
 strip(A,_) = f A 

0  1256 
in strip end; 
1257 

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

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

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

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

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

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

1265 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1268 
(case assoc(al,x) of 

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

1269 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1270 
else Var((y,i),T) 
1271 
 None=> t) 

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

1273 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1274 
T, rename t) 
0  1275 
 rename(f$t) = rename f $ rename t 
1276 
 rename(t) = t; 

250  1277 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1278 
in strip_ren end; 
1279 

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

1281 
fun rename_bvars(dpairs, tpairs, B) = 

250  1282 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1283 

1284 

1285 
(*** RESOLUTION ***) 

1286 

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

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

1288 

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

250  1291 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1292 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1293 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1294 
Const("all",_)$Abs(_,_,t2)) = 
0  1295 
let val (B1,B2) = strip_assums2 (t1,t2) 
1296 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1297 
 strip_assums2 BB = BB; 

1298 

1299 

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

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

1301 
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

1302 
 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

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

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

1307 
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

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

1310 
 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

1311 

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

1312 

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

1317 
If eres_flg then simultaneously proves A1 by assumption. 

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

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

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

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

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

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

1336 
val normp = 

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

1338 
else 

1339 
let val ntps = map (pairself normt) tpairs 

2147  1340 
in if Envir.above (smax, env) then 
1238  1341 
(*no assignments in state; normalize the rule only*) 
1342 
if lifted 

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

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

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

1348 
end 

1258  1349 
val th = (*tuned fix_shyps*) 
1529  1350 
Thm{sign = sign, 
2386  1351 
der = infer_derivs (Bicompose(match, eres_flg, 
1352 
1 + length Bs, nsubgoal, env), 

1353 
[rder,sder]), 

1354 
maxidx = maxidx, 

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

1356 
hyps = union_term(rhyps,shyps), 

1357 
prop = Logic.rule_of normp} 

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

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

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

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

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

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

0  1369 
end; 
2147  1370 
val env = Envir.empty(Int.max(rmax,smax)); 
0  1371 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 
1372 
val dpairs = BBi :: (rtpairs@stpairs); 
