author  wenzelm 
Thu, 09 Oct 1997 14:52:36 +0200  
changeset 3812  66fa30839377 
parent 3789  5802db941718 
child 3893  5a1f22e7b359 
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 
3812  46 
 Oracle of theory * string * 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 

3812  101 
val get_axiom : theory > xstring > 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 * 
3577
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

155 
(string * cterm list * (Sign.sg > thm list > term > thm option) * stamp) list 
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

156 
> meta_simpset 
2509  157 
val del_simprocs : meta_simpset * 
3577
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

158 
(string * cterm list * (Sign.sg > thm list > term > thm option) * stamp) list 
9715b6e3ec5f
added prems argument to simplification procedures;
wenzelm
parents:
3565
diff
changeset

159 
> meta_simpset 
1238  160 
val add_prems : meta_simpset * thm list > meta_simpset 
161 
val prems_of_mss : meta_simpset > thm list 

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

163 
val mk_rews_of_mss : meta_simpset > thm > thm list 

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

1529  167 
(meta_simpset > thm > thm option) > cterm > thm 
1539  168 

3812  169 
val invoke_oracle : theory > xstring > Sign.sg * exn > thm 
250  170 
end; 
0  171 

3550  172 
structure Thm: THM = 
0  173 
struct 
250  174 

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

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

176 

250  177 
(** certified types **) 
178 

179 
(*certified typs under a signature*) 

180 

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

182 

183 
fun rep_ctyp (Ctyp args) = args; 

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

185 

186 
fun ctyp_of sign T = 

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

188 

189 
fun read_ctyp sign s = 

190 
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

191 

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

192 

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

193 

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

195 

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

197 

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

199 

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

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

202 

2671  203 
fun ctyp_of_term (Cterm {sign, T, ...}) = Ctyp {sign=sign, T=T}; 
204 

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

207 
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

208 
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

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

210 

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

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

213 

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

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

215 

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

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

217 
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

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

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

220 
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

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

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

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

224 
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

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

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

227 

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

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

229 
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

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

231 
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

232 
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

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

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

235 

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

238 
if maxidx = ~1 then ct 

239 
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

240 

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

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

242 
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

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

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

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

247 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  248 

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

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

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

254 

2509  255 

256 

574  257 
(** read cterms **) (*exception ERROR*) 
250  258 

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

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

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

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

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

271 

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

272 
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

273 

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

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

275 
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

276 
not practical.*) 
3789  277 
fun read_cterms sg (bs, Ts) = 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

278 
let 
3789  279 
val {tsig, syn, ...} = Sign.rep_sg sg; 
2979  280 
fun read (b, T) = 
281 
(case Syntax.read syn T b of 

282 
[t] => t 

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

284 

3789  285 
val prt = setmp Syntax.show_brackets true (Sign.pretty_term sg); 
286 
val prT = Sign.pretty_typ sg; 

2979  287 
val (us, _) = 
3789  288 
(* FIXME Sign.infer_types!? *) 
289 
Type.infer_types prt prT tsig (Sign.const_type sg) (K None) (K None) 

290 
(Sign.intern_const sg) (Sign.intern_tycons sg) (Sign.intern_sort sg) 

291 
[] true (map (Sign.certify_typ sg) Ts) (ListPair.map read (bs, Ts)); 

292 
in map (cterm_of sg) us end 

2979  293 
handle TYPE (msg, _, _) => error msg 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

295 

250  296 

297 

1529  298 
(*** Derivations ***) 
299 

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

301 
executed in ML.*) 

302 
datatype rule = 

2386  303 
MinProof (*for building minimal proof terms*) 
3812  304 
 Oracle of theory * string * Sign.sg * exn (*oracles*) 
1529  305 
(*Axioms/theorems*) 
2386  306 
 Axiom of theory * string 
307 
 Theorem of string 

1529  308 
(*primitive inferences and compound versions of them*) 
2386  309 
 Assume of cterm 
310 
 Implies_intr of cterm 

1529  311 
 Implies_intr_shyps 
312 
 Implies_intr_hyps 

313 
 Implies_elim 

2386  314 
 Forall_intr of cterm 
315 
 Forall_elim of cterm 

316 
 Reflexive of cterm 

1529  317 
 Symmetric 
318 
 Transitive 

2386  319 
 Beta_conversion of cterm 
1529  320 
 Extensional 
2386  321 
 Abstract_rule of string * cterm 
1529  322 
 Combination 
323 
 Equal_intr 

324 
 Equal_elim 

325 
(*derived rules for tactical proof*) 

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

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

329 
 Lift_rule of cterm * int 

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

2671  331 
 Rotate_rule of int * int 
2386  332 
 Instantiate of (indexname * ctyp) list * (cterm * cterm) list 
333 
 Bicompose of bool * bool * int * int * Envir.env 

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

1529  335 
(*other derived rules*) 
2509  336 
 Class_triv of theory * class 
1529  337 
 VarifyT 
338 
 FreezeT 

339 
(*for the simplifier*) 

2386  340 
 RewriteC of cterm 
341 
 CongC of cterm 

342 
 Rewrite_cterm of cterm 

1529  343 
(*Logical identities, recorded since they are part of the proof process*) 
2386  344 
 Rename_params_rule of string list * int; 
1529  345 

346 

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

347 
type deriv = rule mtree; 
1529  348 

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

349 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  350 

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

351 
val keep_derivs = ref MinDeriv; 
1529  352 

353 

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

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

355 
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

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

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

358 
(case der of 
2386  359 
Join (Oracle _, _) => der :: squash_derivs ders 
360 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 

361 
then der :: squash_derivs ders 

362 
else squash_derivs (der'::ders) 

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

364 
then der :: squash_derivs ders 

365 
else squash_derivs ders 

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

367 
 _ => der :: squash_derivs ders); 

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

368 

1529  369 

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

371 
val min_infer = Join (MinProof, []); 
1529  372 

373 
(*Make a minimal inference*) 

374 
fun make_min_infer [] = min_infer 

375 
 make_min_infer [der] = der 

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

376 
 make_min_infer ders = Join (MinProof, ders); 
1529  377 

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

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

380 
if !keep_derivs=FullDeriv then Join (rl, ders) 
1529  381 
else make_min_infer (squash_derivs ders); 
382 

383 

2509  384 

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

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

386 

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

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

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

392 
hyps: term list, (*hypotheses*) 

393 
prop: term}; (*conclusion*) 

0  394 

250  395 
fun rep_thm (Thm args) = args; 
0  396 

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

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

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

401 
hyps = map (ctermf ~1) hyps, 

402 
prop = ctermf maxidx prop} 

1517  403 
end; 
404 

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

405 
(*errors involving theorems*) 
0  406 
exception THM of string * int * thm list; 
407 

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

408 

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

409 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 
0  410 

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

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

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

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

415 

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

418 
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

419 

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

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

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

422 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  423 

424 
(*counts premises in a rule*) 

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

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

426 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  427 

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

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

429 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  430 

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

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

433 
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

434 

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

435 

0  436 

1238  437 
(** sort contexts of theorems **) 
438 

439 
(* basic utils *) 

440 

2163  441 
(*accumulate sorts suppressing duplicates; these are coded low levelly 
1238  442 
to improve efficiency a bit*) 
443 

444 
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

445 
 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

446 
 add_typ_sorts (TVar (_, S), Ss) = ins_sort(S,Ss) 
1238  447 
and add_typs_sorts ([], Ss) = Ss 
448 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

449 

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

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

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

453 
 add_term_sorts (Bound _, Ss) = Ss 

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

454 
 add_term_sorts (Abs (_,T,t), Ss) = add_term_sorts (t, add_typ_sorts (T,Ss)) 
1238  455 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 
456 

457 
fun add_terms_sorts ([], Ss) = Ss 

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

458 
 add_terms_sorts (t::ts, Ss) = add_terms_sorts (ts, add_term_sorts (t,Ss)); 
1238  459 

1258  460 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
461 

462 
fun add_env_sorts (env, Ss) = 

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

464 
add_typs_sorts (env_codT env, Ss)); 

465 

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

468 

469 
fun add_thms_shyps ([], Ss) = Ss 

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

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

471 
add_thms_shyps (ths, union_sort(shyps,Ss)); 
1238  472 

473 

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

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

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

477 

478 

479 
(* fix_shyps *) 

480 

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

482 
fun fix_shyps thms Ts thm = 

483 
let 

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

487 
in 

1529  488 
Thm {sign = sign, 
2386  489 
der = der, (*No new derivation, as other rules call this*) 
490 
maxidx = maxidx, 

491 
shyps = shyps, hyps = hyps, prop = prop} 

1238  492 
end; 
493 

494 

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

496 

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

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

500 
fun strip_shyps thm = 

501 
let 

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

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

510 
not (!force_strip_shyps) then shyps' 

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

1238  518 
end; 
519 

520 

521 
(* implies_intr_shyps *) 

522 

523 
(*discharge all extra sort hypotheses*) 

524 
fun implies_intr_shyps thm = 

525 
(case extra_shyps thm of 

526 
[] => thm 

527 
 xshyps => 

528 
let 

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

530 
val shyps' = ins_sort (logicS, shyps \\ xshyps); 
1238  531 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 
532 
val names = 

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

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

535 

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

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

542 
shyps = shyps', 

543 
hyps = hyps, 

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

1238  545 
end); 
546 

547 

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

549 

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

550 
(*look up the named axiom in the theory*) 
3812  551 
fun get_axiom theory raw_name = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

552 
let 
3812  553 
val name = Sign.intern (sign_of theory) Theory.thmK raw_name; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

561 
maxidx = maxidx_of_term t, 

562 
shyps = [], 

563 
hyps = [], 

564 
prop = t}) 

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

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

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

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

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

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

571 

1529  572 

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

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

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

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

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

577 

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

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

579 
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

580 
Thm {sign = sign, 
2386  581 
der = Join (Theorem name, [der]), 
582 
maxidx = maxidx, 

583 
shyps = shyps, 

584 
hyps = hyps, 

585 
prop = prop}; 

0  586 

587 

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

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

591 
Thm {sign = sign, 

2386  592 
der = der, (*No derivation recorded!*) 
593 
maxidx = maxidx, 

594 
shyps = shyps, 

595 
hyps = map Term.compress_term hyps, 

596 
prop = Term.compress_term prop}; 

564  597 

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

598 

2509  599 

1529  600 
(*** Meta rules ***) 
0  601 

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

604 
recurrence.*) 

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

606 
(Sign.nodup_Vars prop; 

607 
Thm {sign = sign, 

2386  608 
der = der, 
609 
maxidx = maxidx_of_term prop, 

610 
shyps = shyps, 

611 
hyps = hyps, 

612 
prop = prop}) 

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

614 

1220  615 
(** 'primitive' rules **) 
616 

617 
(*discharge all assumptions t from ts*) 

0  618 
val disch = gen_rem (op aconv); 
619 

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

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

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

1529  628 
else Thm{sign = sign, 
2386  629 
der = infer_derivs (Assume ct, []), 
630 
maxidx = ~1, 

631 
shyps = add_term_sorts(prop,[]), 

632 
hyps = [prop], 

633 
prop = prop} 

0  634 
end; 
635 

1220  636 
(*Implication introduction 
3529  637 
[A] 
638 
: 

639 
B 

1220  640 
 
641 
A ==> B 

642 
*) 

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

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

651 
shyps = [], 

652 
hyps = disch(hyps,A), 

653 
prop = implies$A$prop}) 

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

656 
end; 

657 

1529  658 

1220  659 
(*Implication elimination 
660 
A ==> B A 

661 
 

662 
B 

663 
*) 

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

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

1220  671 
then fix_shyps [thAB, thA] [] 
672 
(Thm{sign= merge_thm_sgs(thAB,thA), 

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

675 
shyps = [], 

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

677 
prop = B}) 

250  678 
else err("major premise") 
679 
 _ => err("major premise") 

0  680 
end; 
250  681 

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

684 
 

685 
!!x.A 

686 
*) 

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

688 
let val x = term_of cx; 
1238  689 
fun result(a,T) = fix_shyps [th] [] 
1529  690 
(Thm{sign = sign, 
2386  691 
der = infer_derivs (Forall_intr cx, [der]), 
692 
maxidx = maxidx, 

693 
shyps = [], 

694 
hyps = hyps, 

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

0  696 
in case x of 
250  697 
Free(a,T) => 
698 
if exists (apl(x, Logic.occs)) hyps 

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

700 
else result(a,T) 

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

703 
end; 

704 

1220  705 
(*Forall elimination 
706 
!!x.A 

707 
 

708 
A[t/x] 

709 
*) 

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

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

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

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

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

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

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

720 
shyps = [], 

721 
hyps = hyps, 

722 
prop = betapply(A,t)}) 

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

724 
then nodup_Vars thm "forall_elim" 

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

726 
end 

2147  727 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  728 
end 
729 
handle TERM _ => 

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

732 

1220  733 
(* Equality *) 
0  734 

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

738 
der = Join(Axiom(pure_thy, "flexpair_def"), []), 
1529  739 
shyps = [], 
740 
hyps = [], 

741 
maxidx = 0, 

742 
prop = term_of (read_cterm Sign.proto_pure 

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

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

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

747 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  748 
in fix_shyps [] [] 
1529  749 
(Thm{sign= sign, 
2386  750 
der = infer_derivs (Reflexive ct, []), 
751 
shyps = [], 

752 
hyps = [], 

753 
maxidx = maxidx, 

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

0  755 
end; 
756 

757 
(*The symmetry rule 

1220  758 
t==u 
759 
 

760 
u==t 

761 
*) 

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

1238  765 
(*no fix_shyps*) 
2386  766 
Thm{sign = sign, 
767 
der = infer_derivs (Symmetric, [der]), 

768 
maxidx = maxidx, 

769 
shyps = shyps, 

770 
hyps = hyps, 

771 
prop = eq$u$t} 

0  772 
 _ => raise THM("symmetric", 0, [th]); 
773 

774 
(*The transitive rule 

1220  775 
t1==u u==t2 
776 
 

777 
t1==t2 

778 
*) 

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

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

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

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

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

793 
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

794 
in if max1 >= 0 andalso max2 >= 0 
2147  795 
then nodup_Vars thm "transitive" 
796 
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

797 
end 
0  798 
 _ => err"premises" 
799 
end; 

800 

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

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

809 
shyps = [], 

810 
hyps = [], 

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

250  812 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  813 
end; 
814 

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

1220  816 
f(x) == g(x) 
817 
 

818 
f == g 

819 
*) 

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

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

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

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

829 
 Var _ => 

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

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

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

1238  833 
(*no fix_shyps*) 
1529  834 
Thm{sign = sign, 
2386  835 
der = infer_derivs (Extensional, [der]), 
836 
maxidx = maxidx, 

837 
shyps = shyps, 

838 
hyps = hyps, 

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

842 

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

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

1220  845 
t == u 
846 
 

847 
%x.t == %x.u 

848 
*) 

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

850 
let val x = term_of cx; 
250  851 
val (t,u) = Logic.dest_equals prop 
852 
handle TERM _ => 

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

1238  854 
fun result T = fix_shyps [th] [] 
2386  855 
(Thm{sign = sign, 
856 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

857 
maxidx = maxidx, 

858 
shyps = [], 

859 
hyps = hyps, 

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

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

0  862 
in case x of 
250  863 
Free(_,T) => 
864 
if exists (apl(x, Logic.occs)) hyps 

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

866 
else result T 

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

869 
end; 

870 

871 
(*The combination rule 

3529  872 
f == g t == u 
873 
 

874 
f(t) == g(u) 

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

881 
fun chktypes (f,t) = 
2386  882 
(case fastype_of f of 
883 
Type("fun",[T1,T2]) => 

884 
if T1 <> fastype_of t then 

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

886 
else () 

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

888 
[th1,th2])) 

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

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

891 
let val _ = chktypes (f,t) 
2386  892 
val thm = (*no fix_shyps*) 
893 
Thm{sign = merge_thm_sgs(th1,th2), 

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

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

896 
shyps = union_sort(shyps1,shyps2), 

897 
hyps = union_term(hyps1,hyps2), 

898 
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

899 
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

900 
then nodup_Vars thm "combination" 
2386  901 
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

902 
end 
0  903 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
904 
end; 

905 

906 

907 
(* Equality introduction 

3529  908 
A ==> B B ==> A 
909 
 

910 
A == B 

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

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

2386  920 
if A aconv A' andalso B aconv B' 
921 
then 

922 
(*no fix_shyps*) 

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

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

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

926 
shyps = union_sort(shyps1,shyps2), 

927 
hyps = union_term(hyps1,hyps2), 

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

929 
else err"not equal" 

1529  930 
 _ => err"premises" 
931 
end; 

932 

933 

934 
(*The equal propositions rule 

3529  935 
A == B A 
1529  936 
 
937 
B 

938 
*) 

939 
fun equal_elim th1 th2 = 

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

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

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

943 
in case prop1 of 

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

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

946 
fix_shyps [th1, th2] [] 

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

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

950 
shyps = [], 

951 
hyps = union_term(hyps1,hyps2), 

952 
prop = B}) 

1529  953 
 _ => err"major premise" 
954 
end; 

0  955 

1220  956 

957 

0  958 
(**** Derived rules ****) 
959 

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

967 
shyps = shyps, 

1529  968 
hyps = disch(As,A), 
2386  969 
prop = implies$A$prop}) 
0  970 
 implies_intr_hyps th = th; 
971 

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

250  973 
Instantiates the theorem and deletes trivial tpairs. 
0  974 
Resulting sequence may contain multiple elements if the tpairs are 
975 
not all flexflex. *) 

1529  976 
fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = 
250  977 
let fun newthm env = 
1529  978 
if Envir.is_empty env then th 
979 
else 

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

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

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

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

1220  985 
in fix_shyps [th] (env_codT env) 
1529  986 
(Thm{sign = sign, 
2386  987 
der = infer_derivs (Flexflex_rule env, [der]), 
988 
maxidx = maxidx_of_term newprop, 

989 
shyps = [], 

990 
hyps = hyps, 

991 
prop = newprop}) 

250  992 
end; 
0  993 
val (tpairs,_) = Logic.strip_flexpairs prop 
994 
in Sequence.maps newthm 

250  995 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  996 
end; 
997 

998 
(*Instantiation of Vars 

1220  999 
A 
1000 
 

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

1002 
*) 

0  1003 

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

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

1006 

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

1008 
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

1009 
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

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

1013 
end; 

1014 

1015 
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

1016 
let val {T,sign} = rep_ctyp ctyp 
0  1017 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
1018 

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

1020 
Instantiates distinct Vars by terms of same type. 

1021 
Normalizes the new theorem! *) 

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

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

250  1026 
val newprop = 
1027 
Envir.norm_term (Envir.empty 0) 

1028 
(subst_atomic tpairs 

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

1220  1030 
val newth = 
1031 
fix_shyps [th] (map snd vTs) 

1529  1032 
(Thm{sign = newsign, 
2386  1033 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 
1034 
maxidx = maxidx_of_term newprop, 

1035 
shyps = [], 

1036 
hyps = hyps, 

1037 
prop = newprop}) 

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

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

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

0  1048 

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

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

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

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

1238  1055 
else fix_shyps [] [] 
1529  1056 
(Thm{sign = sign, 
2386  1057 
der = infer_derivs (Trivial ct, []), 
1058 
maxidx = maxidx, 

1059 
shyps = [], 

1060 
hyps = [], 

1061 
prop = implies$A$A}) 

0  1062 
end; 
1063 

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

1065 
fun class_triv thy c = 
1529  1066 
let val sign = sign_of thy; 
1067 
val Cterm {t, maxidx, ...} = 

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

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

1070 
in 
1238  1071 
fix_shyps [] [] 
1529  1072 
(Thm {sign = sign, 
2386  1073 
der = infer_derivs (Class_triv(thy,c), []), 
1074 
maxidx = maxidx, 

1075 
shyps = [], 

1076 
hyps = [], 

1077 
prop = t}) 

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

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

1079 

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

1080 

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

1088 
shyps = shyps, 

1089 
hyps = hyps, 

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

0  1094 
end; 
1095 

1096 
(* Replace all TVars by new TFrees *) 

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

1103 
shyps = shyps, 

1104 
hyps = hyps, 

1529  1105 
prop = prop'} 
1220  1106 
end; 
0  1107 

1108 

1109 
(*** Inference rules for tactics ***) 

1110 

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

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

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

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

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

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

1117 
end 

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

1119 

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

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

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

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

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

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

1134 
shyps=union_sort(sshyps,shyps), 
2386  1135 
hyps=hyps, 
1529  1136 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 
2386  1137 
map lift_all As, 
1138 
lift_all B)} 

0  1139 
end; 
1140 

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

1142 
fun assumption i state = 

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

1150 
shyps = [], 

1151 
hyps = hyps, 

1152 
prop = 

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

1154 
Logic.rule_of (tpairs, Bs, C) 

1155 
else (*normalize the new rule fully*) 

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

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

1159 
(Sequence.mapp newth 

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

0  1162 
in addprfs (Logic.assum_pairs Bi) end; 
1163 

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

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

1220  1170 
then fix_shyps [state] [] 
1529  1171 
(Thm{sign = sign, 
2386  1172 
der = infer_derivs (Assumption (i,None), [der]), 
1173 
maxidx = maxidx, 

1174 
shyps = [], 

1175 
hyps = hyps, 

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

0  1177 
else raise THM("eq_assumption", 0, [state]) 
1178 
end; 

1179 

1180 

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

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

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

1185 
val params = Logic.strip_params Bi 

1186 
and asms = Logic.strip_assums_hyp Bi 

1187 
and concl = Logic.strip_assums_concl Bi 

1188 
val n = length asms 

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

1190 
else if 0<m andalso m<n 

1191 
then list_all 

1192 
(params, 

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

1194 
List.take(asms, m), 

1195 
concl)) 

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

1197 
in Thm{sign = sign, 

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

1199 
maxidx = maxidx, 

1200 
shyps = shyps, 

1201 
hyps = hyps, 

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

1203 
end; 

1204 

1205 

0  1206 
(** User renaming of parameters in a subgoal **) 
1207 

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

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

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

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

1212 
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

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

1216 
val short = length iparams  length cs 

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

1219 
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

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

1224 
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

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

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

1227 
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

1228 
state) 
1220  1229 
 [] => fix_shyps [state] [] 
2386  1230 
(Thm{sign = sign, 
1231 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1232 
maxidx = maxidx, 

1233 
shyps = [], 

1234 
hyps = hyps, 

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

0  1236 
end; 
1237 

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

1239 

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

1243 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1244 
else (x,y)::al) 
0  1245 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1246 
 match_bvs(_,_,al) = al; 

1247 

1248 
(* strip abstractions created by parameters *) 

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

1250 

1251 

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

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

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

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

1259 
 strip(A,_) = f A 

0  1260 
in strip end; 
1261 

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

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

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

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

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

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

1269 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1272 
(case assoc(al,x) of 

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

1273 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1274 
else Var((y,i),T) 
1275 
 None=> t) 

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

1277 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1278 
T, rename t) 
0  1279 
 rename(f$t) = rename f $ rename t 
1280 
 rename(t) = t; 

250  1281 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1282 
in strip_ren end; 
1283 

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

1285 
fun rename_bvars(dpairs, tpairs, B) = 

250  1286 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1287 

1288 

1289 
(*** RESOLUTION ***) 

1290 

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

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

1292 

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

250  1295 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1296 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1297 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1298 
Const("all",_)$Abs(_,_,t2)) = 
0  1299 
let val (B1,B2) = strip_assums2 (t1,t2) 
1300 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1301 
 strip_assums2 BB = BB; 

1302 

1303 

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

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

1305 
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

1306 
 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

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

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

1311 
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

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

1314 
 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

1315 

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

1316 

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

1321 
If eres_flg then simultaneously proves A1 by assumption. 

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

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

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

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

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

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

1340 
val normp = 

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

1342 
else 

1343 
let val ntps = map (pairself normt) tpairs 

2147  1344 
in if Envir.above (smax, env) then 
1238  1345 
(*no assignments in state; normalize the rule only*) 
1346 
if lifted 

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

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

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

1352 
end 

1258  1353 
val th = (*tuned fix_shyps*) 
1529  1354 
Thm{sign = sign, 
2386  1355 
der = infer_derivs (Bicompose(match, eres_flg, 
1356 
1 + length Bs, nsubgoal, env), 

1357 
[rder,sder]), 

1358 
maxidx = maxidx, 

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

1360 
hyps = union_term(rhyps,shyps), 

1361 
prop = Logic.rule_of normp} 

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

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

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

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

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

250  1369 
else map (rename_bvars(dpairs,tpairs,B)) As0 
0  1370 
in (map (Logic.flatten_params n) As1) 
250  1371 
handle TERM _ => 
9b5a069285ce
extend_theory: changed type of "abbrs" arg;
wenzelm 