author  wenzelm 
Tue, 01 Oct 1996 10:43:58 +0200  
changeset 2047  a3701c4343ea 
parent 2046  fd26cd4da8cf 
child 2139  2c59b204b540 
permissions  rwrr 
250  1 
(* Title: Pure/thm.ML 
0  2 
ID: $Id$ 
250  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

4 
Copyright 1994 University of Cambridge 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

5 

1160  6 
The core of Isabelle's Meta Logic: certified types and terms, meta 
1529  7 
theorems, meta rules (including resolution and simplification). 
0  8 
*) 
9 

250  10 
signature THM = 
1503  11 
sig 
1160  12 
(*certified types*) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

13 
type ctyp 
1238  14 
val rep_ctyp : ctyp > {sign: Sign.sg, T: typ} 
15 
val typ_of : ctyp > typ 

16 
val ctyp_of : Sign.sg > typ > ctyp 

17 
val read_ctyp : Sign.sg > string > ctyp 

1160  18 

19 
(*certified terms*) 

20 
type cterm 

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

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

22 
val rep_cterm : cterm > {sign: Sign.sg, t: term, T: typ, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

23 
maxidx: int} 
1238  24 
val term_of : cterm > term 
25 
val cterm_of : Sign.sg > term > cterm 

26 
val read_cterm : Sign.sg > string * typ > cterm 

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

27 
val read_cterms : Sign.sg > string list * typ list > cterm list 
1238  28 
val cterm_fun : (term > term) > (cterm > cterm) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

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

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

37 

1529  38 
(*theories*) 
39 

40 
(*proof terms [must duplicate declaration as a specification]*) 

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

41 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

42 
val keep_derivs : deriv_kind ref 
1529  43 
datatype rule = 
44 
MinProof 

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

45 
 Oracle of theory * Sign.sg * exn 
1529  46 
 Axiom of theory * string 
1597
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

47 
 Theorem of string 
1529  48 
 Assume of cterm 
49 
 Implies_intr of cterm 

50 
 Implies_intr_shyps 

51 
 Implies_intr_hyps 

52 
 Implies_elim 

53 
 Forall_intr of cterm 

54 
 Forall_elim of cterm 

55 
 Reflexive of cterm 

56 
 Symmetric 

57 
 Transitive 

58 
 Beta_conversion of cterm 

59 
 Extensional 

60 
 Abstract_rule of string * cterm 

61 
 Combination 

62 
 Equal_intr 

63 
 Equal_elim 

64 
 Trivial of cterm 

65 
 Lift_rule of cterm * int 

66 
 Assumption of int * Envir.env option 

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

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

69 
 Flexflex_rule of Envir.env 

70 
 Class_triv of theory * class 

71 
 VarifyT 

72 
 FreezeT 

73 
 RewriteC of cterm 

74 
 CongC of cterm 

75 
 Rewrite_cterm of cterm 

76 
 Rename_params_rule of string list * int; 

77 

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

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

1160  80 
(*meta theorems*) 
81 
type thm 

82 
exception THM of string * int * thm list 

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

85 
prop: term} 

86 
val crep_thm : thm > {sign: Sign.sg, der: deriv, maxidx: int, 

87 
shyps: sort list, hyps: cterm list, 

88 
prop: cterm} 

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

91 
val prems_of : thm > term list 

92 
val nprems_of : thm > int 

93 
val concl_of : thm > term 

94 
val cprop_of : thm > cterm 

95 
val extra_shyps : thm > sort list 

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

97 
val strip_shyps : thm > thm 

98 
val implies_intr_shyps: thm > thm 

99 
val get_axiom : theory > string > thm 

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

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

103 
(*meta rules*) 

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

108 
val forall_intr : cterm > thm > thm 

109 
val forall_elim : cterm > thm > thm 

110 
val flexpair_def : thm 

111 
val reflexive : cterm > thm 

112 
val symmetric : thm > thm 

113 
val transitive : thm > thm > thm 

114 
val beta_conversion : cterm > thm 

115 
val extensional : thm > thm 

116 
val abstract_rule : string > cterm > thm > thm 

117 
val combination : thm > thm > thm 

118 
val equal_intr : thm > thm > thm 

119 
val equal_elim : thm > thm > thm 

120 
val implies_intr_hyps : thm > thm 

121 
val flexflex_rule : thm > thm Sequence.seq 

122 
val instantiate : 

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

126 
val varifyT : thm > thm 

127 
val freezeT : thm > thm 

128 
val dest_state : thm * int > 

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

132 
val eq_assumption : int > thm > thm 

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

139 
(*meta simplification*) 

140 
type meta_simpset 

141 
exception SIMPLIFIER of string * thm 

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

144 
val del_simps : meta_simpset * thm list > meta_simpset 

145 
val mss_of : thm list > meta_simpset 

146 
val add_congs : meta_simpset * thm list > meta_simpset 

147 
val add_prems : meta_simpset * thm list > meta_simpset 

148 
val prems_of_mss : meta_simpset > thm list 

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

150 
val mk_rews_of_mss : meta_simpset > thm > thm list 

151 
val trace_simp : bool ref 

152 
val rewrite_cterm : bool * bool > meta_simpset > 

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

155 
val invoke_oracle : theory * Sign.sg * exn > thm 

250  156 
end; 
0  157 

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

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

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

162 

250  163 
(** certified types **) 
164 

165 
(*certified typs under a signature*) 

166 

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

168 

169 
fun rep_ctyp (Ctyp args) = args; 

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

171 

172 
fun ctyp_of sign T = 

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

174 

175 
fun read_ctyp sign s = 

176 
Ctyp {sign = sign, T = Sign.read_typ (sign, K None) s}; 

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

177 

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

178 

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

179 

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

181 

250  182 
(*certified terms under a signature, with checked typ and maxidx of Vars*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

183 

250  184 
datatype cterm = Cterm of {sign: Sign.sg, t: term, T: typ, maxidx: int}; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

185 

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

186 
fun rep_cterm (Cterm args) = args; 
250  187 
fun term_of (Cterm {t, ...}) = t; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

188 

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

191 
let val (t, T, maxidx) = Sign.certify_term sign tm 

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

192 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

194 

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

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

197 

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

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

199 

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

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

201 
fun dest_comb (Cterm{sign, T, maxidx, t = A $ B}) = 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

204 
case typeA of Type("fun",[S,T]) => S 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

207 
(Cterm {sign=sign, maxidx=maxidx, t=A, T=typeA}, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

208 
Cterm {sign=sign, maxidx=maxidx, t=B, T=typeB}) 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

211 

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

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

213 
fun dest_abs (Cterm {sign, T as Type("fun",[_,S]), maxidx, t=Abs(x,ty,M)}) = 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

215 
in (Cterm {sign = sign, T = ty, maxidx = 0, t = Free(y,ty)}, 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

216 
Cterm {sign = sign, T = S, maxidx = maxidx, t = N}) 
1493
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

219 

1703
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

220 
fun adjust_maxidx (Cterm {sign, T, t, ...}) = 
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

221 
Cterm {sign = sign, T = T, maxidx = maxidx_of_term t, t = t} 
e22ad43bab5f
moved dest_cimplies to drule.ML; added adjust_maxidx
clasohm
parents:
1659
diff
changeset

222 

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

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

224 
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

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

226 
if T = dty then Cterm{t=f$x, sign=Sign.merge(sign1,sign2), T=rty, 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

227 
maxidx=max[maxidx1, maxidx2]} 
96286c4e32de
removed mk_prop; added capply; simplified dest_abs
clasohm
parents:
1503
diff
changeset

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

229 
 capply _ _ = raise CTERM "capply: first arg is not a function" 
250  230 

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

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

234 
T = ty > T2, maxidx=max[maxidx1, maxidx2]} 

235 
 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

236 

574  237 
(** read cterms **) (*exception ERROR*) 
250  238 

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

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

240 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  241 
let 
574  242 
val T' = Sign.certify_typ sign T 
243 
handle TYPE (msg, _, _) => error msg; 

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

245 
val (_, t', tye) = 
959  246 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  247 
val ct = cterm_of sign t' 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

248 
handle TYPE arg => error (Sign.exn_type_msg sign arg) 
1460  249 
 TERM (msg, _) => error msg; 
250  250 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

251 

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

252 
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

253 

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

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

255 
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

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

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

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

259 
val {tsig, syn, ...} = Sign.rep_sg sign 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

260 
fun read (b,T) = 
1460  261 
case Syntax.read syn T b of 
262 
[t] => t 

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

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

264 
val (us,_) = Type.infer_types(tsig, Sign.const_type sign, 
1460  265 
K None, K None, 
266 
[], true, 

267 
map (Sign.certify_typ sign) Ts, 

268 
map read (bs~~Ts)) 

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

269 
in map (cterm_of sign) us end 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

270 
handle TYPE arg => error (Sign.exn_type_msg sign arg) 
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

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

272 

250  273 

274 

1529  275 
(*** Derivations ***) 
276 

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

278 
executed in ML.*) 

279 
datatype rule = 

280 
MinProof (*for building minimal proof terms*) 

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

281 
 Oracle of theory * Sign.sg * exn (*oracles*) 
1529  282 
(*Axioms/theorems*) 
283 
 Axiom of theory * string 

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

284 
 Theorem of string 
1529  285 
(*primitive inferences and compound versions of them*) 
286 
 Assume of cterm 

287 
 Implies_intr of cterm 

288 
 Implies_intr_shyps 

289 
 Implies_intr_hyps 

290 
 Implies_elim 

291 
 Forall_intr of cterm 

292 
 Forall_elim of cterm 

293 
 Reflexive of cterm 

294 
 Symmetric 

295 
 Transitive 

296 
 Beta_conversion of cterm 

297 
 Extensional 

298 
 Abstract_rule of string * cterm 

299 
 Combination 

300 
 Equal_intr 

301 
 Equal_elim 

302 
(*derived rules for tactical proof*) 

303 
 Trivial of cterm 

304 
(*For lift_rule, the proof state is not a premise. 

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

306 
 Lift_rule of cterm * int 

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

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

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

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

311 
(*other derived rules*) 

312 
 Class_triv of theory * class (*derived rule????*) 

313 
 VarifyT 

314 
 FreezeT 

315 
(*for the simplifier*) 

316 
 RewriteC of cterm 

317 
 CongC of cterm 

318 
 Rewrite_cterm of cterm 

319 
(*Logical identities, recorded since they are part of the proof process*) 

320 
 Rename_params_rule of string list * int; 

321 

322 

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

323 
type deriv = rule mtree; 
1529  324 

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

325 
datatype deriv_kind = MinDeriv  ThmDeriv  FullDeriv; 
1529  326 

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

327 
val keep_derivs = ref MinDeriv; 
1529  328 

329 

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

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

331 
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

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

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

334 
(case der of 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

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

336 
 Join (Theorem _, [der']) => if !keep_derivs=ThmDeriv 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

337 
then der :: squash_derivs ders 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

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

339 
 Join (Axiom _, _) => if !keep_derivs=ThmDeriv 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

340 
then der :: squash_derivs ders 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

341 
else squash_derivs ders 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

342 
 Join (_, []) => squash_derivs ders 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

343 
 _ => der :: squash_derivs ders); 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

344 

1529  345 

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

347 
val min_infer = Join (MinProof, []); 
1529  348 

349 
(*Make a minimal inference*) 

350 
fun make_min_infer [] = min_infer 

351 
 make_min_infer [der] = der 

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

352 
 make_min_infer ders = Join (MinProof, ders); 
1529  353 

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

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

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

359 

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

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

361 

0  362 
datatype thm = Thm of 
1460  363 
{sign: Sign.sg, (*signature for hyps and prop*) 
1529  364 
der: deriv, (*derivation*) 
1460  365 
maxidx: int, (*maximum index of any Var or TVar*) 
2047  366 
shyps: sort list, (*sort hypotheses*) 
1460  367 
hyps: term list, (*hypotheses*) 
368 
prop: term}; (*conclusion*) 

0  369 

250  370 
fun rep_thm (Thm args) = args; 
0  371 

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

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

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

376 
hyps = map (ctermf ~1) hyps, 

377 
prop = ctermf maxidx prop} 

1517  378 
end; 
379 

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

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

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

383 

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

384 
val stamps_of_thm = #stamps o Sign.rep_sg o #sign o rep_thm; 
0  385 

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

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

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

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

390 

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

391 

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

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

393 
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

394 

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

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

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

397 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  398 

399 
(*counts premises in a rule*) 

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

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

401 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  402 

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

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

404 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  405 

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

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

408 
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

409 

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

410 

0  411 

1238  412 
(** sort contexts of theorems **) 
413 

414 
(* basic utils *) 

415 

416 
(*accumulate sorts suppressing duplicates; these are coded low level 

417 
to improve efficiency a bit*) 

418 

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

420 
 add_typ_sorts (TFree (_, S), Ss) = S ins Ss 

421 
 add_typ_sorts (TVar (_, S), Ss) = S ins Ss 

422 
and add_typs_sorts ([], Ss) = Ss 

423 
 add_typs_sorts (T :: Ts, Ss) = add_typs_sorts (Ts, add_typ_sorts (T, Ss)); 

424 

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

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

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

428 
 add_term_sorts (Bound _, Ss) = Ss 

429 
 add_term_sorts (Abs (_, T, t), Ss) = add_term_sorts (t, add_typ_sorts (T, Ss)) 

430 
 add_term_sorts (t $ u, Ss) = add_term_sorts (t, add_term_sorts (u, Ss)); 

431 

432 
fun add_terms_sorts ([], Ss) = Ss 

433 
 add_terms_sorts (t :: ts, Ss) = add_terms_sorts (ts, add_term_sorts (t, Ss)); 

434 

1258  435 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
436 

437 
fun add_env_sorts (env, Ss) = 

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

439 
add_typs_sorts (env_codT env, Ss)); 

440 

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

443 

444 
fun add_thms_shyps ([], Ss) = Ss 

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

446 
add_thms_shyps (ths, shyps union Ss); 

447 

448 

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

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

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

452 

453 

454 
(* fix_shyps *) 

455 

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

457 
fun fix_shyps thms Ts thm = 

458 
let 

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

462 
in 

1529  463 
Thm {sign = sign, 
464 
der = der, (*No new derivation, as other rules call this*) 

465 
maxidx = maxidx, 

466 
shyps = shyps, hyps = hyps, prop = prop} 

1238  467 
end; 
468 

469 

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

471 

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

473 

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

475 
fun strip_shyps thm = 

476 
let 

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

480 
val shyps' = filter (fn S => S mem sorts orelse maybe_empty S) shyps; 

481 
in 

1529  482 
Thm {sign = sign, der = der, maxidx = maxidx, 
483 
shyps = 

484 
(if eq_set (shyps',sorts) orelse not (!force_strip_shyps) then shyps' 

485 
else (* FIXME tmp *) 

486 
(writeln ("WARNING Removed sort hypotheses: " ^ 

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

488 
writeln "WARNING Let's hope these sorts are nonempty!"; 

1238  489 
sorts)), 
1529  490 
hyps = hyps, 
491 
prop = prop} 

1238  492 
end; 
493 

494 

495 
(* implies_intr_shyps *) 

496 

497 
(*discharge all extra sort hypotheses*) 

498 
fun implies_intr_shyps thm = 

499 
(case extra_shyps thm of 

500 
[] => thm 

501 
 xshyps => 

502 
let 

1529  503 
val Thm {sign, der, maxidx, shyps, hyps, prop} = thm; 
1238  504 
val shyps' = logicS ins (shyps \\ xshyps); 
505 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 

506 
val names = 

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

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

509 

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

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

512 
in 

1529  513 
Thm {sign = sign, 
514 
der = infer_derivs (Implies_intr_shyps, [der]), 

515 
maxidx = maxidx, 

516 
shyps = shyps', 

517 
hyps = hyps, 

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

1238  519 
end); 
520 

521 

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

523 

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

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

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

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

527 
fun get_ax [] = raise Match 
1529  528 
 get_ax (thy :: thys) = 
1539  529 
let val {sign, new_axioms, parents, ...} = rep_theory thy 
1529  530 
in case Symtab.lookup (new_axioms, name) of 
531 
Some t => fix_shyps [] [] 

532 
(Thm {sign = sign, 

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

534 
maxidx = maxidx_of_term t, 

535 
shyps = [], 

536 
hyps = [], 

537 
prop = t}) 

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

539 
end; 

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

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

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

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

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

544 

1529  545 

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

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

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

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

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

550 

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

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

552 
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

553 
Thm {sign = sign, 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

554 
der = Join (Theorem name, [der]), 
54ece585bf62
name_thm no longer takes a theory argument, as the
paulson
parents:
1580
diff
changeset

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

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

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

558 
prop = prop}; 
0  559 

560 

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

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

564 
Thm {sign = sign, 

565 
der = der, (*No derivation recorded!*) 

566 
maxidx = maxidx, 

567 
shyps = shyps, 

568 
hyps = map Term.compress_term hyps, 

569 
prop = Term.compress_term prop}; 

564  570 

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

571 

1529  572 
(*** Meta rules ***) 
0  573 

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

574 
(* check that term does not contain same var with different typing/sorting *) 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

575 
fun nodup_Vars(thm as Thm{prop,...}) s = 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

576 
Sign.nodup_Vars prop handle TYPE(msg,_,_) => raise THM(s^": "^msg,0,[thm]); 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

577 

1220  578 
(** 'primitive' rules **) 
579 

580 
(*discharge all assumptions t from ts*) 

0  581 
val disch = gen_rem (op aconv); 
582 

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

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

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

1529  591 
else Thm{sign = sign, 
592 
der = infer_derivs (Assume ct, []), 

593 
maxidx = ~1, 

594 
shyps = add_term_sorts(prop,[]), 

595 
hyps = [prop], 

596 
prop = prop} 

0  597 
end; 
598 

1220  599 
(*Implication introduction 
600 
A  B 

601 
 

602 
A ==> B 

603 
*) 

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

605 
let val {sign=signA, t=A, T, maxidx=maxidxA} = rep_cterm cA 
0  606 
in if T<>propT then 
250  607 
raise THM("implies_intr: assumptions must have type prop", 0, [thB]) 
1238  608 
else fix_shyps [thB] [] 
1529  609 
(Thm{sign = Sign.merge (sign,signA), 
610 
der = infer_derivs (Implies_intr cA, [der]), 

611 
maxidx = max[maxidxA, maxidx], 

612 
shyps = [], 

613 
hyps = disch(hyps,A), 

614 
prop = implies$A$prop}) 

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

617 
end; 

618 

1529  619 

1220  620 
(*Implication elimination 
621 
A ==> B A 

622 
 

623 
B 

624 
*) 

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

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

1220  632 
then fix_shyps [thAB, thA] [] 
633 
(Thm{sign= merge_thm_sgs(thAB,thA), 

1529  634 
der = infer_derivs (Implies_elim, [der,derA]), 
635 
maxidx = max[maxA,maxidx], 

636 
shyps = [], 

637 
hyps = hypsA union hyps, (*dups suppressed*) 

638 
prop = B}) 

250  639 
else err("major premise") 
640 
 _ => err("major premise") 

0  641 
end; 
250  642 

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

645 
 

646 
!!x.A 

647 
*) 

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

649 
let val x = term_of cx; 
1238  650 
fun result(a,T) = fix_shyps [th] [] 
1529  651 
(Thm{sign = sign, 
652 
der = infer_derivs (Forall_intr cx, [der]), 

653 
maxidx = maxidx, 

654 
shyps = [], 

655 
hyps = hyps, 

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

0  657 
in case x of 
250  658 
Free(a,T) => 
659 
if exists (apl(x, Logic.occs)) hyps 

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

661 
else result(a,T) 

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

664 
end; 

665 

1220  666 
(*Forall elimination 
667 
!!x.A 

668 
 

669 
A[t/x] 

670 
*) 

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

672 
let val {sign=signt, t, T, maxidx=maxt} = rep_cterm ct 
0  673 
in case prop of 
250  674 
Const("all",Type("fun",[Type("fun",[qary,_]),_])) $ A => 
675 
if T<>qary then 

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

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

677 
else let val thm = fix_shyps [th] [] 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

678 
(Thm{sign= Sign.merge(sign,signt), 
1529  679 
der = infer_derivs (Forall_elim ct, [der]), 
680 
maxidx = max[maxidx, maxt], 

681 
shyps = [], 

682 
hyps = hyps, 

683 
prop = betapply(A,t)}) 

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

684 
in nodup_Vars thm "forall_elim"; thm end 
250  685 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  686 
end 
687 
handle TERM _ => 

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

690 

1220  691 
(* Equality *) 
0  692 

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

696 
der = Join(Axiom(pure_thy, "flexpair_def"), []), 
1529  697 
shyps = [], 
698 
hyps = [], 

699 
maxidx = 0, 

700 
prop = term_of (read_cterm Sign.proto_pure 

701 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}); 

0  702 

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

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

705 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  706 
in fix_shyps [] [] 
1529  707 
(Thm{sign= sign, 
708 
der = infer_derivs (Reflexive ct, []), 

709 
shyps = [], 

710 
hyps = [], 

711 
maxidx = maxidx, 

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

0  713 
end; 
714 

715 
(*The symmetry rule 

1220  716 
t==u 
717 
 

718 
u==t 

719 
*) 

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

1238  723 
(*no fix_shyps*) 
1529  724 
Thm{sign = sign, 
725 
der = infer_derivs (Symmetric, [der]), 

726 
maxidx = maxidx, 

727 
shyps = shyps, 

728 
hyps = hyps, 

729 
prop = eq$u$t} 

0  730 
 _ => raise THM("symmetric", 0, [th]); 
731 

732 
(*The transitive rule 

1220  733 
t1==u u==t2 
734 
 

735 
t1==t2 

736 
*) 

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

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

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

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

1220  745 
fix_shyps [th1, th2] [] 
1529  746 
(Thm{sign= merge_thm_sgs(th1,th2), 
747 
der = infer_derivs (Transitive, [der1, der2]), 

748 
maxidx = max[max1,max2], 

749 
shyps = [], 

750 
hyps = hyps1 union hyps2, 

751 
prop = eq$t1$t2}) 

1634  752 
in nodup_Vars thm "transitive"; thm end 
0  753 
 _ => err"premises" 
754 
end; 

755 

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

758 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  759 
in case t of 
1238  760 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
1529  761 
(Thm{sign = sign, 
762 
der = infer_derivs (Beta_conversion ct, []), 

763 
maxidx = maxidx_of_term t, 

764 
shyps = [], 

765 
hyps = [], 

766 
prop = Logic.mk_equals(t, subst_bounds([u],bodt))}) 

250  767 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  768 
end; 
769 

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

1220  771 
f(x) == g(x) 
772 
 

773 
f == g 

774 
*) 

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

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

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

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

784 
 Var _ => 

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

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

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

1238  788 
(*no fix_shyps*) 
1529  789 
Thm{sign = sign, 
790 
der = infer_derivs (Extensional, [der]), 

791 
maxidx = maxidx, 

792 
shyps = shyps, 

793 
hyps = hyps, 

794 
prop = Logic.mk_equals(f,g)} 

0  795 
end 
796 
 _ => raise THM("extensional: premise", 0, [th]); 

797 

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

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

1220  800 
t == u 
801 
 

802 
%x.t == %x.u 

803 
*) 

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

805 
let val x = term_of cx; 
250  806 
val (t,u) = Logic.dest_equals prop 
807 
handle TERM _ => 

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

1238  809 
fun result T = fix_shyps [th] [] 
1529  810 
(Thm{sign = sign, 
811 
der = infer_derivs (Abstract_rule (a,cx), [der]), 

812 
maxidx = maxidx, 

813 
shyps = [], 

814 
hyps = hyps, 

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

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

0  817 
in case x of 
250  818 
Free(_,T) => 
819 
if exists (apl(x, Logic.occs)) hyps 

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

821 
else result T 

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

824 
end; 

825 

826 
(*The combination rule 

1220  827 
f==g t==u 
828 
 

829 
f(t)==g(u) 

830 
*) 

0  831 
fun combination th1 th2 = 
1529  832 
let val Thm{der=der1, maxidx=max1, shyps=shyps1, hyps=hyps1, 
833 
prop=prop1,...} = th1 

834 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 

835 
prop=prop2,...} = th2 

1836
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

836 
fun chktypes (f,t) = 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

837 
(case fastype_of f of 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

838 
Type("fun",[T1,T2]) => 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

839 
if T1 <> fastype_of t then 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

840 
raise THM("combination: types", 0, [th1,th2]) 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

841 
else () 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

842 
 _ => raise THM("combination: not function type", 0, 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

843 
[th1,th2])) 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

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

846 
let val _ = chktypes (f,t) 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

847 
val thm = (*no fix_shyps*) 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

848 
Thm{sign = merge_thm_sgs(th1,th2), 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

849 
der = infer_derivs (Combination, [der1, der2]), 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

850 
maxidx = max[max1,max2], 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

851 
shyps = shyps1 union shyps2, 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

852 
hyps = hyps1 union hyps2, 
861e29c7cada
Added typechecking to rule "combination". This corrects a fault
paulson
parents:
1802
diff
changeset

853 
prop = Logic.mk_equals(f$t, g$u)} 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

854 
in nodup_Vars thm "combination"; thm end 
0  855 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
856 
end; 

857 

858 

859 
(* Equality introduction 

1220  860 
A==>B B==>A 
861 
 

862 
A==B 

863 
*) 

0  864 
fun equal_intr th1 th2 = 
1529  865 
let val Thm{der=der1,maxidx=max1, shyps=shyps1, hyps=hyps1, 
866 
prop=prop1,...} = th1 

867 
and Thm{der=der2, maxidx=max2, shyps=shyps2, hyps=hyps2, 

868 
prop=prop2,...} = th2; 

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

870 
in case (prop1,prop2) of 

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

872 
if A aconv A' andalso B aconv B' 

873 
then 

874 
(*no fix_shyps*) 

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

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

877 
maxidx = max[max1,max2], 

878 
shyps = shyps1 union shyps2, 

879 
hyps = hyps1 union hyps2, 

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

881 
else err"not equal" 

882 
 _ => err"premises" 

883 
end; 

884 

885 

886 
(*The equal propositions rule 

887 
A==B A 

888 
 

889 
B 

890 
*) 

891 
fun equal_elim th1 th2 = 

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

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

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

895 
in case prop1 of 

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

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

898 
fix_shyps [th1, th2] [] 

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

900 
der = infer_derivs (Equal_elim, [der1, der2]), 

901 
maxidx = max[max1,max2], 

902 
shyps = [], 

903 
hyps = hyps1 union hyps2, 

904 
prop = B}) 

905 
 _ => err"major premise" 

906 
end; 

0  907 

1220  908 

909 

0  910 
(**** Derived rules ****) 
911 

1503  912 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  913 
Repeated hypotheses are discharged only once; fold cannot do this*) 
1529  914 
fun implies_intr_hyps (Thm{sign, der, maxidx, shyps, hyps=A::As, prop}) = 
1238  915 
implies_intr_hyps (*no fix_shyps*) 
1529  916 
(Thm{sign = sign, 
917 
der = infer_derivs (Implies_intr_hyps, [der]), 

918 
maxidx = maxidx, 

919 
shyps = shyps, 

920 
hyps = disch(As,A), 

921 
prop = implies$A$prop}) 

0  922 
 implies_intr_hyps th = th; 
923 

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

250  925 
Instantiates the theorem and deletes trivial tpairs. 
0  926 
Resulting sequence may contain multiple elements if the tpairs are 
927 
not all flexflex. *) 

1529  928 
fun flexflex_rule (th as Thm{sign, der, maxidx, hyps, prop,...}) = 
250  929 
let fun newthm env = 
1529  930 
if Envir.is_empty env then th 
931 
else 

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

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

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

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

1220  937 
in fix_shyps [th] (env_codT env) 
1529  938 
(Thm{sign = sign, 
939 
der = infer_derivs (Flexflex_rule env, [der]), 

940 
maxidx = maxidx_of_term newprop, 

941 
shyps = [], 

942 
hyps = hyps, 

943 
prop = newprop}) 

250  944 
end; 
0  945 
val (tpairs,_) = Logic.strip_flexpairs prop 
946 
in Sequence.maps newthm 

250  947 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  948 
end; 
949 

950 
(*Instantiation of Vars 

1220  951 
A 
952 
 

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

954 
*) 

0  955 

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

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

958 

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

960 
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

961 
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

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

965 
end; 

966 

967 
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

968 
let val {T,sign} = rep_ctyp ctyp 
0  969 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
970 

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

972 
Instantiates distinct Vars by terms of same type. 

973 
Normalizes the new theorem! *) 

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

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

250  978 
val newprop = 
979 
Envir.norm_term (Envir.empty 0) 

980 
(subst_atomic tpairs 

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

1220  982 
val newth = 
983 
fix_shyps [th] (map snd vTs) 

1529  984 
(Thm{sign = newsign, 
985 
der = infer_derivs (Instantiate(vcTs,ctpairs), [der]), 

986 
maxidx = maxidx_of_term newprop, 

987 
shyps = [], 

988 
hyps = hyps, 

989 
prop = newprop}) 

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

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

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

994 
else nodup_Vars newth "instantiate"; 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

995 
newth 
0  996 
end 
250  997 
handle TERM _ => 
0  998 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  999 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  1000 

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

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

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

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

1238  1007 
else fix_shyps [] [] 
1529  1008 
(Thm{sign = sign, 
1009 
der = infer_derivs (Trivial ct, []), 

1010 
maxidx = maxidx, 

1011 
shyps = [], 

1012 
hyps = [], 

1013 
prop = implies$A$A}) 

0  1014 
end; 
1015 

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

1017 
fun class_triv thy c = 
1529  1018 
let val sign = sign_of thy; 
1019 
val Cterm {t, maxidx, ...} = 

1020 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 

1021 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 

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

1022 
in 
1238  1023 
fix_shyps [] [] 
1529  1024 
(Thm {sign = sign, 
1025 
der = infer_derivs (Class_triv(thy,c), []), 

1026 
maxidx = maxidx, 

1027 
shyps = [], 

1028 
hyps = [], 

1029 
prop = t}) 

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

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

1031 

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

1032 

0  1033 
(* Replace all TFrees not in the hyps by new TVars *) 
1529  1034 
fun varifyT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
0  1035 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1634  1036 
in let val thm = (*no fix_shyps*) 
1529  1037 
Thm{sign = sign, 
1038 
der = infer_derivs (VarifyT, [der]), 

1039 
maxidx = max[0,maxidx], 

1040 
shyps = shyps, 

1041 
hyps = hyps, 

1042 
prop = Type.varify(prop,tfrees)} 

1634  1043 
in nodup_Vars thm "varifyT"; thm end 
1044 
(* this nodup_Vars check can be removed if thms are guaranteed not to contain 

1045 
duplicate TVars with differnt sorts *) 

0  1046 
end; 
1047 

1048 
(* Replace all TVars by new TFrees *) 

1529  1049 
fun freezeT(Thm{sign,der,maxidx,shyps,hyps,prop}) = 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

1050 
let val prop' = Type.freeze prop 
1238  1051 
in (*no fix_shyps*) 
1529  1052 
Thm{sign = sign, 
1053 
der = infer_derivs (FreezeT, [der]), 

1054 
maxidx = maxidx_of_term prop', 

1055 
shyps = shyps, 

1056 
hyps = hyps, 

1057 
prop = prop'} 

1220  1058 
end; 
0  1059 

1060 

1061 
(*** Inference rules for tactics ***) 

1062 

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

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

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

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

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

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

1069 
end 

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

1071 

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

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

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

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

0  1081 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1082 
in (*no fix_shyps*) 
1529  1083 
Thm{sign = merge_thm_sgs(state,orule), 
1084 
der = infer_derivs (Lift_rule(ct_Bi, i), [der]), 

1085 
maxidx = maxidx+smax+1, 

1086 
shyps=sshyps union shyps, 

1087 
hyps=hyps, 

1088 
prop = Logic.rule_of (map (pairself lift_abs) tpairs, 

1089 
map lift_all As, 

1090 
lift_all B)} 

0  1091 
end; 
1092 

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

1094 
fun assumption i state = 

1529  1095 
let val Thm{sign,der,maxidx,hyps,prop,...} = state; 
0  1096 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  1097 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1098 
fix_shyps [state] (env_codT env) 
1529  1099 
(Thm{sign = sign, 
1100 
der = infer_derivs (Assumption (i, Some env), [der]), 

1101 
maxidx = maxidx, 

1102 
shyps = [], 

1103 
hyps = hyps, 

1104 
prop = 

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

1106 
Logic.rule_of (tpairs, Bs, C) 

1107 
else (*normalize the new rule fully*) 

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

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

1111 
(Sequence.mapp newth 

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

0  1114 
in addprfs (Logic.assum_pairs Bi) end; 
1115 

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

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

1220  1122 
then fix_shyps [state] [] 
1529  1123 
(Thm{sign = sign, 
1124 
der = infer_derivs (Assumption (i,None), [der]), 

1125 
maxidx = maxidx, 

1126 
shyps = [], 

1127 
hyps = hyps, 

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

0  1129 
else raise THM("eq_assumption", 0, [state]) 
1130 
end; 

1131 

1132 

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

1134 

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

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

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

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

1139 
fun rename_params_rule (cs, i) state = 

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

1143 
val short = length iparams  length cs 

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

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

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

250  1149 
in 
0  1150 
case findrep cs of 
1151 
c::_ => error ("Bound variables not distinct: " ^ c) 

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

1152 
 [] => (case cs inter_string freenames of 
0  1153 
a::_ => error ("Bound/Free variable clash: " ^ a) 
1220  1154 
 [] => fix_shyps [state] [] 
1529  1155 
(Thm{sign = sign, 
1156 
der = infer_derivs (Rename_params_rule(cs,i), [der]), 

1157 
maxidx = maxidx, 

1158 
shyps = [], 

1159 
hyps = hyps, 

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

0  1161 
end; 
1162 

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

1164 

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

1168 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1169 
else (x,y)::al) 
0  1170 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1171 
 match_bvs(_,_,al) = al; 

1172 

1173 
(* strip abstractions created by parameters *) 

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

1175 

1176 

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

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

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

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

1184 
 strip(A,_) = f A 

0  1185 
in strip end; 
1186 

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

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

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

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

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

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

1194 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1197 
(case assoc(al,x) of 

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

1198 
Some(y) => if x mem_string vids orelse y mem_string vids then t 
250  1199 
else Var((y,i),T) 
1200 
 None=> t) 

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

1202 
Abs(case assoc_string(al,x) of Some(y) => y  None => x, 
250  1203 
T, rename t) 
0  1204 
 rename(f$t) = rename f $ rename t 
1205 
 rename(t) = t; 

250  1206 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1207 
in strip_ren end; 
1208 

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

1210 
fun rename_bvars(dpairs, tpairs, B) = 

250  1211 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1212 

1213 

1214 
(*** RESOLUTION ***) 

1215 

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

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

1217 

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

250  1220 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1221 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1222 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1223 
Const("all",_)$Abs(_,_,t2)) = 
0  1224 
let val (B1,B2) = strip_assums2 (t1,t2) 
1225 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1226 
 strip_assums2 BB = BB; 

1227 

1228 

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

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

1230 
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

1231 
 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

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

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

1236 
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

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

1239 
 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

1240 

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

1241 

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

1246 
If eres_flg then simultaneously proves A1 by assumption. 

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

1529  1250 
local open Sequence; exception COMPOSE 
0  1251 
in 
250  1252 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1253 
(eres_flg, orule, nsubgoal) = 
1529  1254 
let val Thm{der=sder, maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1255 
and Thm{der=rder, maxidx=rmax, shyps=rshyps, hyps=rhyps, 

1256 
prop=rprop,...} = orule 

1257 
(*How many hyps to skip over during normalization*) 

1238  1258 
and nlift = Logic.count_prems(strip_all_body Bi, 
1259 
if eres_flg then ~1 else 0) 

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

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

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

1265 
val normp = 

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

1267 
else 

1268 
let val ntps = map (pairself normt) tpairs 

1238  1269 
in if the (Envir.minidx env) > smax then 
1270 
(*no assignments in state; normalize the rule only*) 

1271 
if lifted 

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

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

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

1277 
end 

1258  1278 
val th = (*tuned fix_shyps*) 
1529  1279 
Thm{sign = sign, 
1280 
der = infer_derivs (Bicompose(match, eres_flg, 

1281 
1 + length Bs, nsubgoal, env), 

1282 
[rder,sder]), 

1283 
maxidx = maxidx, 

1284 
shyps = add_env_sorts (env, rshyps union sshyps), 

1285 
hyps = rhyps union shyps, 

1286 
prop = Logic.rule_of normp} 

1287 
in cons(th, thq) end handle COMPOSE => thq 

0  1288 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 
1289 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

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

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

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

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

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

0  1298 
end; 
1299 
val env = Envir.empty(max[rmax,smax]); 

1300 
val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); 

1301 
val dpairs = BBi :: (rtpairs@stpairs); 

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

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

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

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

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

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

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

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

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

1313 
(*ordinary resolution*) 

1314 
fun res(None) = null 

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

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

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

1320 
end; 

1321 
end; (*open Sequence*) 

1322 

1323 

1324 
fun bicompose match arg i state = 

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

1326 

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

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

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

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

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

1333 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1334 
end; 
1335 

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

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

250  1338 
fun biresolution match brules i state = 
0  1339 
let val lift = lift_rule(state, i); 
250  1340 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1341 
val B = Logic.strip_assums_concl Bi; 

1342 
val Hs = Logic.strip_assums_hyp Bi; 

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

1344 
fun res [] = Sequence.null 

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

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

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

1350 
else res brules 

0  1351 
in Sequence.flats (res brules) end; 
1352 

1353 

1354 

1355 
(*** Meta simp sets ***) 

1356 

288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1357 
type rrule = {thm:thm, lhs:term, perm:bool}; 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1358 
type cong = {thm:thm, lhs:term}; 
0  1359 
datatype meta_simpset = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1360 
Mss of {net:rrule Net.net, congs:(string * cong)list, bounds:string list, 
0  1361 
prems: thm list, mk_rews: thm > thm list}; 
1362 

1363 
(*A "mss" contains data needed during conversion: 

1364 
net: discrimination net of rewrite rules 

1365 
congs: association list of congruence rules 

405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1366 
bounds: names of bound variables already used; 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1367 
for generating new names when rewriting under lambda abstractions 
0  1368 
mk_rews: used when local assumptions are added 
1369 
*) 

1370 

1529  1371 
val empty_mss = Mss{net = Net.empty, congs = [], bounds=[], prems = [], 
0  1372 
mk_rews = K[]}; 
1373 

1374 
exception SIMPLIFIER of string * thm; 

1375 

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

1376 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1377 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1378 
fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t)); 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1379 

209  1380 
val trace_simp = ref false; 
1381 

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

1382 
fun trace_term a sign t = if !trace_simp then prtm a sign t else (); 
209  1383 

1384 
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop; 

1385 

1580
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1386 
fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else (); 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1387 

e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1388 
fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop; 
e3fd931e6095
Added some functions which allow redirection of Isabelle's output
berghofe
parents:
1576
diff
changeset

1389 

427
