author  paulson 
Fri, 16 Feb 1996 13:29:22 +0100  
changeset 1503  7dba648ee25c 
parent 1495  b8b54847c77f 
child 1516  96286c4e32de 
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 
7 
theorems, theories, meta rules (including resolution and 

8 
simplification). 

0  9 
*) 
10 

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

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

17 
val ctyp_of : Sign.sg > typ > ctyp 

18 
val read_ctyp : Sign.sg > string > ctyp 

1160  19 

20 
(*certified terms*) 

21 
type cterm 

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

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

23 
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

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

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) 
30 
val dest_cimplies : cterm > cterm * cterm 

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

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

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

33 
val mk_prop : 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 

38 
(*meta theorems*) 

39 
type thm 

40 
exception THM of string * int * thm list 

1238  41 
val rep_thm : thm > {sign: Sign.sg, maxidx: int, 
1220  42 
shyps: sort list, hyps: term list, prop: term} 
1238  43 
val stamps_of_thm : thm > string ref list 
44 
val tpairs_of : thm > (term * term) list 

45 
val prems_of : thm > term list 

46 
val nprems_of : thm > int 

47 
val concl_of : thm > term 

48 
val cprop_of : thm > cterm 

49 
val extra_shyps : thm > sort list 

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

51 
val strip_shyps : thm > thm 

52 
val implies_intr_shyps: thm > thm 

53 
val cert_axm : Sign.sg > string * term > string * term 

54 
val read_axm : Sign.sg > string * string > string * term 

55 
val inferT_axm : Sign.sg > string * term > string * term 

1160  56 

57 
(*theories*) 

58 
type theory 

59 
exception THEORY of string * theory list 

1238  60 
val rep_theory : theory > 
1503  61 
{sign: Sign.sg, new_axioms: term Symtab.table, parents: theory list} 
1238  62 
val sign_of : theory > Sign.sg 
1503  63 
val syn_of : theory > Syntax.syntax 
1238  64 
val stamps_of_thy : theory > string ref list 
65 
val parents_of : theory > theory list 

66 
val subthy : theory * theory > bool 

67 
val eq_thy : theory * theory > bool 

68 
val get_axiom : theory > string > thm 

69 
val axioms_of : theory > (string * thm) list 

70 
val proto_pure_thy : theory 

71 
val pure_thy : theory 

72 
val cpure_thy : theory 

1503  73 
(*theory primitives*) 
74 
val add_classes : (class * class list) list > theory > theory 

75 
val add_classrel : (class * class) list > theory > theory 

76 
val add_defsort : sort > theory > theory 

77 
val add_types : (string * int * mixfix) list > theory > theory 

78 
val add_tyabbrs : (string * string list * string * mixfix) list 

79 
> theory > theory 

80 
val add_tyabbrs_i : (string * string list * typ * mixfix) list 

81 
> theory > theory 

82 
val add_arities : (string * sort list * sort) list > theory > theory 

83 
val add_consts : (string * string * mixfix) list > theory > theory 

84 
val add_consts_i : (string * typ * mixfix) list > theory > theory 

85 
val add_syntax : (string * string * mixfix) list > theory > theory 

86 
val add_syntax_i : (string * typ * mixfix) list > theory > theory 

87 
val add_trfuns : 

88 
(string * (Syntax.ast list > Syntax.ast)) list * 

89 
(string * (term list > term)) list * 

90 
(string * (term list > term)) list * 

91 
(string * (Syntax.ast list > Syntax.ast)) list > theory > theory 

92 
val add_trrules : (string * string)Syntax.trrule list > theory > theory 

93 
val add_trrules_i : Syntax.ast Syntax.trrule list > theory > theory 

94 
val add_axioms : (string * string) list > theory > theory 

95 
val add_axioms_i : (string * term) list > theory > theory 

96 
val add_thyname : string > theory > theory 

97 

1238  98 
val merge_theories : theory * theory > theory 
99 
val merge_thy_list : bool > theory list > theory 

1160  100 

101 
(*meta rules*) 

1238  102 
val assume : cterm > thm 
1416  103 
val compress : thm > thm 
1238  104 
val implies_intr : cterm > thm > thm 
105 
val implies_elim : thm > thm > thm 

106 
val forall_intr : cterm > thm > thm 

107 
val forall_elim : cterm > thm > thm 

108 
val flexpair_def : thm 

109 
val reflexive : cterm > thm 

110 
val symmetric : thm > thm 

111 
val transitive : thm > thm > thm 

112 
val beta_conversion : cterm > thm 

113 
val extensional : thm > thm 

114 
val abstract_rule : string > cterm > thm > thm 

115 
val combination : thm > thm > thm 

116 
val equal_intr : thm > thm > thm 

117 
val equal_elim : thm > thm > thm 

118 
val implies_intr_hyps : thm > thm 

119 
val flexflex_rule : thm > thm Sequence.seq 

120 
val instantiate : 

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

124 
val varifyT : thm > thm 

125 
val freezeT : thm > thm 

126 
val dest_state : thm * int > 

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

130 
val eq_assumption : int > thm > thm 

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

137 
(*meta simplification*) 

138 
type meta_simpset 

139 
exception SIMPLIFIER of string * thm 

1238  140 
val empty_mss : meta_simpset 
141 
val add_simps : meta_simpset * thm list > meta_simpset 

142 
val del_simps : meta_simpset * thm list > meta_simpset 

143 
val mss_of : thm list > meta_simpset 

144 
val add_congs : meta_simpset * thm list > meta_simpset 

145 
val add_prems : meta_simpset * thm list > meta_simpset 

146 
val prems_of_mss : meta_simpset > thm list 

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

148 
val mk_rews_of_mss : meta_simpset > thm > thm list 

149 
val trace_simp : bool ref 

150 
val rewrite_cterm : bool * bool > meta_simpset > 

1160  151 
(meta_simpset > thm > thm option) > cterm > thm 
250  152 
end; 
0  153 

1503  154 
structure Thm : THM = 
0  155 
struct 
250  156 

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

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

158 

250  159 
(** certified types **) 
160 

161 
(*certified typs under a signature*) 

162 

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

164 

165 
fun rep_ctyp (Ctyp args) = args; 

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

167 

168 
fun ctyp_of sign T = 

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

170 

171 
fun read_ctyp sign s = 

172 
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

173 

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

174 

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

175 

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

177 

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

179 

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

181 

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

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

184 

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

187 
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

188 
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

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

190 

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

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

193 

250  194 
(*dest_implies for cterms. Note T=prop below*) 
195 
fun dest_cimplies (Cterm{sign, T, maxidx, t=Const("==>", _) $ A $ B}) = 

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

196 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  197 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
198 
 dest_cimplies ct = raise TERM ("dest_cimplies", [term_of ct]); 

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

199 

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

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

201 

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

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

203 
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

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

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

206 
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

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

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

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

210 
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

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

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

213 

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

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

215 
fun dest_abs (Cterm{sign, T, maxidx, t = tm as Abs(s,ty,M)}) = 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

216 
let fun mk_var{Name,Ty} = Free(Name,Ty); 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

217 
val v = mk_var{Name = s, Ty = ty}; 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

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

221 
in (Cterm{sign = sign, T = ty, maxidx = maxidx, t = v}, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

222 
Cterm{sign = sign, T = ty2, maxidx = maxidx, t = betapply (tm,v)}) 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

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

225 

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

226 
(*Convert cterm of type "o" to "prop" by using Trueprop*) 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

227 
fun mk_prop (ct as Cterm{sign, T, maxidx, t = Const("Trueprop",_) $ _}) = ct 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

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

229 
if T = Type("o",[]) then 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

230 
Cterm{sign = sign, T = Type("prop",[]), maxidx = maxidx, 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

231 
t = Const("Trueprop", Type("o",[]) > Type("prop",[])) $ t} 
e936723cb94d
added dest_comb, dest_abs and mk_prop for manipulating cterms
clasohm
parents:
1460
diff
changeset

232 
else error "Type o expected in mk_prop"; 
250  233 

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

234 

574  235 
(** read cterms **) (*exception ERROR*) 
250  236 

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

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

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

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

243 
val (_, t', tye) = 
959  244 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  245 
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

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

249 

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

250 
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

251 

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

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

253 
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

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

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

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

257 
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

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

261 
 _ => 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

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

265 
map (Sign.certify_typ sign) Ts, 

266 
map read (bs~~Ts)) 

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

267 
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

268 
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

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

270 

250  271 

272 

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

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

274 

0  275 
datatype thm = Thm of 
1460  276 
{sign: Sign.sg, (*signature for hyps and prop*) 
277 
maxidx: int, (*maximum index of any Var or TVar*) 

278 
shyps: sort list, (* FIXME comment *) 

279 
hyps: term list, (*hypotheses*) 

280 
prop: term}; (*conclusion*) 

0  281 

250  282 
fun rep_thm (Thm args) = args; 
0  283 

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

284 
(*errors involving theorems*) 
0  285 
exception THM of string * int * thm list; 
286 

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

287 

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

288 
val sign_of_thm = #sign o rep_thm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

289 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  290 

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

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

292 
fun merge_thm_sgs (th1, th2) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

293 
Sign.merge (pairself sign_of_thm (th1, th2)) 
574  294 
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

295 

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

296 

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

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

298 
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

299 

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

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

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

302 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  303 

304 
(*counts premises in a rule*) 

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

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

306 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  307 

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

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

309 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  310 

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

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

313 
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

314 

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

315 

0  316 

1238  317 
(** sort contexts of theorems **) 
318 

319 
(* basic utils *) 

320 

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

322 
to improve efficiency a bit*) 

323 

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

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

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

327 
and add_typs_sorts ([], Ss) = Ss 

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

329 

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

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

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

333 
 add_term_sorts (Bound _, Ss) = Ss 

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

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

336 

337 
fun add_terms_sorts ([], Ss) = Ss 

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

339 

1258  340 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 
341 

342 
fun add_env_sorts (env, Ss) = 

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

344 
add_typs_sorts (env_codT env, Ss)); 

345 

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

348 

349 
fun add_thms_shyps ([], Ss) = Ss 

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

351 
add_thms_shyps (ths, shyps union Ss); 

352 

353 

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

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

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

357 

358 

1416  359 
(*Compression of theorems  a separate rule, not integrated with the others, 
360 
as it could be slow.*) 

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

362 
Thm {sign = sign, 

1460  363 
maxidx = maxidx, 
364 
shyps = shyps, 

365 
hyps = map Term.compress_term hyps, 

366 
prop = Term.compress_term prop}; 

1416  367 

368 

1238  369 
(* fix_shyps *) 
370 

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

372 
fun fix_shyps thms Ts thm = 

373 
let 

374 
val Thm {sign, maxidx, hyps, prop, ...} = thm; 

375 
val shyps = 

376 
add_thm_sorts (thm, add_typs_sorts (Ts, add_thms_shyps (thms, []))); 

377 
in 

378 
Thm {sign = sign, maxidx = maxidx, 

379 
shyps = shyps, hyps = hyps, prop = prop} 

380 
end; 

381 

382 

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

384 

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

386 

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

388 
fun strip_shyps thm = 

389 
let 

390 
val Thm {sign, maxidx, shyps, hyps, prop} = thm; 

391 
val sorts = add_thm_sorts (thm, []); 

392 
val maybe_empty = not o Sign.nonempty_sort sign sorts; 

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

394 
in 

395 
Thm {sign = sign, maxidx = maxidx, 

396 
shyps = 

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

398 
else (* FIXME tmp *) 

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

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

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

402 
sorts)), 

403 
hyps = hyps, prop = prop} 

404 
end; 

405 

406 

407 
(* implies_intr_shyps *) 

408 

409 
(*discharge all extra sort hypotheses*) 

410 
fun implies_intr_shyps thm = 

411 
(case extra_shyps thm of 

412 
[] => thm 

413 
 xshyps => 

414 
let 

415 
val Thm {sign, maxidx, shyps, hyps, prop} = thm; 

416 
val shyps' = logicS ins (shyps \\ xshyps); 

417 
val used_names = foldr add_term_tfree_names (prop :: hyps, []); 

418 
val names = 

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

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

421 

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

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

424 
in 

425 
Thm {sign = sign, maxidx = maxidx, shyps = shyps', 

426 
hyps = hyps, prop = Logic.list_implies (sort_hyps, prop)} 

427 
end); 

428 

429 

430 

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

431 
(*** Theories ***) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

432 

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

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

435 
sign: Sign.sg, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

436 
new_axioms: term Symtab.table, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

437 
parents: theory list}; 
0  438 

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

439 
fun rep_theory (Theory args) = args; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

440 

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

441 
(*errors involving theories*) 
0  442 
exception THEORY of string * theory list; 
443 

444 

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

445 
val sign_of = #sign o rep_theory; 
0  446 
val syn_of = #syn o Sign.rep_sg o sign_of; 
447 

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

448 
(*stamps associated with a theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

449 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

450 

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

451 
(*return the immediate ancestors*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

452 
val parents_of = #parents o rep_theory; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

453 

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

454 

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

455 
(*compare theories*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

456 
val subthy = Sign.subsig o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

457 
val eq_thy = Sign.eq_sg o pairself sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

458 

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

459 

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

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

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

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

463 
fun get_ax [] = raise Match 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

464 
 get_ax (Theory {sign, new_axioms, parents} :: thys) = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

465 
(case Symtab.lookup (new_axioms, name) of 
1238  466 
Some t => fix_shyps [] [] 
467 
(Thm {sign = sign, maxidx = maxidx_of_term t, 

468 
shyps = [], hyps = [], prop = t}) 

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

469 
 None => get_ax parents handle Match => get_ax thys); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

474 

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

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

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

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

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

479 

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

480 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

481 
(* the Pure theories *) 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

482 

196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

483 
val proto_pure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

484 
Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

485 

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

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

487 
Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []}; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

488 

922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

489 
val cpure_thy = 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

490 
Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []}; 
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

491 

0  492 

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

493 

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

494 
(** extend theory **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

495 

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

496 
fun err_dup_axms names = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

497 
error ("Duplicate axiom name(s) " ^ commas_quote names); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

498 

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

499 
fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms = 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

501 
val draft = Sign.is_draft sign; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

503 
Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

504 
handle Symtab.DUPS names => err_dup_axms names; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

505 
val parents1 = if draft then parents else [thy]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

507 
Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1} 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

509 

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

510 

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

511 
(* extend signature of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

512 

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

513 
fun ext_sg extfun decls (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

514 
ext_thy thy (extfun decls sign) []; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

515 

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

516 
val add_classes = ext_sg Sign.add_classes; 
421  517 
val add_classrel = ext_sg Sign.add_classrel; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

518 
val add_defsort = ext_sg Sign.add_defsort; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

519 
val add_types = ext_sg Sign.add_types; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

520 
val add_tyabbrs = ext_sg Sign.add_tyabbrs; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

521 
val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

522 
val add_arities = ext_sg Sign.add_arities; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

523 
val add_consts = ext_sg Sign.add_consts; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

524 
val add_consts_i = ext_sg Sign.add_consts_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

525 
val add_syntax = ext_sg Sign.add_syntax; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

526 
val add_syntax_i = ext_sg Sign.add_syntax_i; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

527 
val add_trfuns = ext_sg Sign.add_trfuns; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

528 
val add_trrules = ext_sg Sign.add_trrules; 
1160  529 
val add_trrules_i = ext_sg Sign.add_trrules_i; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

530 
val add_thyname = ext_sg Sign.add_name; 
0  531 

532 

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

533 
(* prepare axioms *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

534 

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

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

536 
error ("The error(s) above occurred in axiom " ^ quote name); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

537 

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

538 
fun no_vars tm = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

539 
if null (term_vars tm) andalso null (term_tvars tm) then tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

540 
else error "Illegal schematic variable(s) in term"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

541 

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

542 
fun cert_axm sg (name, raw_tm) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

544 
val Cterm {t, T, ...} = cterm_of sg raw_tm 
1394
a1d2735f5ade
New function read_cterms is a combination of read_def_cterm and
paulson
parents:
1258
diff
changeset

545 
handle TYPE arg => error (Sign.exn_type_msg sg arg) 
1460  546 
 TERM (msg, _) => error msg; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

548 
assert (T = propT) "Term not of type prop"; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

549 
(name, no_vars t) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

551 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

552 

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

553 
fun read_axm sg (name, str) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

554 
(name, no_vars (term_of (read_cterm sg (str, propT)))) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

555 
handle ERROR => err_in_axm name; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

556 

564  557 
fun inferT_axm sg (name, pre_tm) = 
959  558 
let val t = #2(Sign.infer_types sg (K None) (K None) [] true 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

559 
([pre_tm], propT)) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

560 
in (name, no_vars t) end 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
922
diff
changeset

561 
handle ERROR => err_in_axm name; 
564  562 

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

563 

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

564 
(* extend axioms of a theory *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

565 

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

566 
fun ext_axms prep_axm axms (thy as Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

568 
val sign1 = Sign.make_draft sign; 
1416  569 
val axioms = map (apsnd (Term.compress_term o Logic.varify) o 
1460  570 
prep_axm sign) 
571 
axms; 

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

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

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

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

575 

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

576 
val add_axioms = ext_axms read_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

577 
val add_axioms_i = ext_axms cert_axm; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

578 

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

579 

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

580 

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

581 
(** merge theories **) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

582 

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

583 
fun merge_thy_list mk_draft thys = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

585 
fun is_union thy = forall (fn t => subthy (t, thy)) thys; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

586 
val is_draft = Sign.is_draft o sign_of; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

587 

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

588 
fun add_sign (sg, Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

589 
Sign.merge (sg, sign) handle TERM (msg, _) => error msg; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

591 
(case (find_first is_union thys, exists is_draft thys) of 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

592 
(Some thy, _) => thy 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

593 
 (None, true) => raise THEORY ("Illegal merge of draft theories", thys) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

594 
 (None, false) => Theory { 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

596 
(if mk_draft then Sign.make_draft else I) 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

597 
(foldl add_sign (Sign.proto_pure, thys)), 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

598 
new_axioms = Symtab.null, 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

599 
parents = thys}) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

601 

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

602 
fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2]; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

603 

0  604 

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

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

606 
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

607 
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

608 

0  609 

1220  610 
(*** Meta rules ***) 
611 

612 
(** 'primitive' rules **) 

613 

614 
(*discharge all assumptions t from ts*) 

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

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

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

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

1238  625 
else fix_shyps [] [] 
626 
(Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop}) 

0  627 
end; 
628 

1220  629 
(*Implication introduction 
630 
A  B 

631 
 

632 
A ==> B 

633 
*) 

1238  634 
fun implies_intr cA (thB as Thm{sign,maxidx,hyps,prop,...}) : thm = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

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

640 
shyps= [], hyps= disch(hyps,A), prop= implies$A$prop}) 

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

643 
end; 

644 

1220  645 
(*Implication elimination 
646 
A ==> B A 

647 
 

648 
B 

649 
*) 

0  650 
fun implies_elim thAB thA : thm = 
651 
let val Thm{maxidx=maxA, hyps=hypsA, prop=propA,...} = thA 

250  652 
and Thm{sign, maxidx, hyps, prop,...} = thAB; 
653 
fun err(a) = raise THM("implies_elim: "^a, 0, [thAB,thA]) 

0  654 
in case prop of 
250  655 
imp$A$B => 
656 
if imp=implies andalso A aconv propA 

1220  657 
then fix_shyps [thAB, thA] [] 
658 
(Thm{sign= merge_thm_sgs(thAB,thA), 

250  659 
maxidx= max[maxA,maxidx], 
1220  660 
shyps= [], 
250  661 
hyps= hypsA union hyps, (*dups suppressed*) 
1220  662 
prop= B}) 
250  663 
else err("major premise") 
664 
 _ => err("major premise") 

0  665 
end; 
250  666 

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

669 
 

670 
!!x.A 

671 
*) 

1238  672 
fun forall_intr cx (th as Thm{sign,maxidx,hyps,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

673 
let val x = term_of cx; 
1238  674 
fun result(a,T) = fix_shyps [th] [] 
675 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps, 

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

0  677 
in case x of 
250  678 
Free(a,T) => 
679 
if exists (apl(x, Logic.occs)) hyps 

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

681 
else result(a,T) 

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

684 
end; 

685 

1220  686 
(*Forall elimination 
687 
!!x.A 

688 
 

689 
A[t/x] 

690 
*) 

691 
fun forall_elim ct (th as Thm{sign,maxidx,hyps,prop,...}) : thm = 

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

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

696 
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

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

698 
(Thm{sign= Sign.merge(sign,signt), 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

699 
maxidx= max[maxidx, maxt], 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

700 
shyps= [], hyps= hyps, prop= betapply(A,t)}) 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

701 
in nodup_Vars thm "forall_elim"; thm end 
250  702 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  703 
end 
704 
handle TERM _ => 

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

707 

1220  708 
(* Equality *) 
0  709 

1220  710 
(* Definition of the relation =?= *) 
1238  711 
val flexpair_def = fix_shyps [] [] 
712 
(Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0, 

713 
prop= term_of (read_cterm Sign.proto_pure 

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

0  715 

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

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

718 
let val {sign, t, T, maxidx} = rep_cterm ct 
1238  719 
in fix_shyps [] [] 
720 
(Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, 

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

0  722 
end; 
723 

724 
(*The symmetry rule 

1220  725 
t==u 
726 
 

727 
u==t 

728 
*) 

729 
fun symmetric (th as Thm{sign,shyps,hyps,prop,maxidx}) = 

0  730 
case prop of 
731 
(eq as Const("==",_)) $ t $ u => 

1238  732 
(*no fix_shyps*) 
733 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 

0  734 
 _ => raise THM("symmetric", 0, [th]); 
735 

736 
(*The transitive rule 

1220  737 
t1==u u==t2 
738 
 

739 
t1==t2 

740 
*) 

0  741 
fun transitive th1 th2 = 
742 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

743 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

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

745 
in case (prop1,prop2) of 

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

250  747 
if not (u aconv u') then err"middle term" else 
1220  748 
fix_shyps [th1, th2] [] 
749 
(Thm{sign= merge_thm_sgs(th1,th2), shyps= [], 

750 
hyps= hyps1 union hyps2, 

751 
maxidx= max[max1,max2], prop= eq$t1$t2}) 

0  752 
 _ => err"premises" 
753 
end; 

754 

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

757 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  758 
in case t of 
1238  759 
Abs(_,_,bodt) $ u => fix_shyps [] [] 
760 
(Thm{sign= sign, shyps= [], hyps= [], 

250  761 
maxidx= maxidx_of_term t, 
1238  762 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))}) 
250  763 
 _ => raise THM("beta_conversion: not a redex", 0, []) 
0  764 
end; 
765 

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

1220  767 
f(x) == g(x) 
768 
 

769 
f == g 

770 
*) 

771 
fun extensional (th as Thm{sign,maxidx,shyps,hyps,prop}) = 

0  772 
case prop of 
773 
(Const("==",_)) $ (f$x) $ (g$y) => 

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

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

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

780 
 Var _ => 

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

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

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

1238  784 
(*no fix_shyps*) 
1220  785 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, 
250  786 
prop= Logic.mk_equals(f,g)} 
0  787 
end 
788 
 _ => raise THM("extensional: premise", 0, [th]); 

789 

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

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

1220  792 
t == u 
793 
 

794 
%x.t == %x.u 

795 
*) 

1238  796 
fun abstract_rule a cx (th as Thm{sign,maxidx,hyps,prop,...}) = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

797 
let val x = term_of cx; 
250  798 
val (t,u) = Logic.dest_equals prop 
799 
handle TERM _ => 

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

1238  801 
fun result T = fix_shyps [th] [] 
802 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= hyps, 

250  803 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
1238  804 
Abs(a, T, abstract_over (x,u)))}) 
0  805 
in case x of 
250  806 
Free(_,T) => 
807 
if exists (apl(x, Logic.occs)) hyps 

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

809 
else result T 

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

812 
end; 

813 

814 
(*The combination rule 

1220  815 
f==g t==u 
816 
 

817 
f(t)==g(u) 

818 
*) 

0  819 
fun combination th1 th2 = 
1220  820 
let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 
821 
and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2 

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

822 
in case (prop1,prop2) of 
0  823 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 
1495
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

824 
let val thm = (*no fix_shyps*) 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

825 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

826 
hyps= hyps1 union hyps2, 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

827 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 
b8b54847c77f
Added check for duplicate vars with distinct types/sorts (nodup_Vars)
nipkow
parents:
1493
diff
changeset

828 
in nodup_Vars thm "combination"; thm end 
0  829 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
830 
end; 

831 

832 

833 
(*The equal propositions rule 

1220  834 
A==B A 
835 
 

836 
B 

837 
*) 

0  838 
fun equal_elim th1 th2 = 
839 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

840 
and Thm{maxidx=max2, hyps=hyps2, prop=prop2,...} = th2; 

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

842 
in case prop1 of 

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

250  844 
if not (prop2 aconv A) then err"not equal" else 
1220  845 
fix_shyps [th1, th2] [] 
846 
(Thm{sign= merge_thm_sgs(th1,th2), shyps= [], 

847 
hyps= hyps1 union hyps2, 

848 
maxidx= max[max1,max2], prop= B}) 

0  849 
 _ => err"major premise" 
850 
end; 

851 

852 

853 
(* Equality introduction 

1220  854 
A==>B B==>A 
855 
 

856 
A==B 

857 
*) 

0  858 
fun equal_intr th1 th2 = 
1220  859 
let val Thm{maxidx=max1, shyps=shyps1, hyps=hyps1, prop=prop1,...} = th1 
860 
and Thm{maxidx=max2, shyps=shyps2, hyps=hyps2, prop=prop2,...} = th2; 

0  861 
fun err(msg) = raise THM("equal_intr: "^msg, 0, [th1,th2]) 
862 
in case (prop1,prop2) of 

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

250  864 
if A aconv A' andalso B aconv B' 
1238  865 
then 
866 
(*no fix_shyps*) 

867 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 

868 
hyps= hyps1 union hyps2, 

869 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 

250  870 
else err"not equal" 
0  871 
 _ => err"premises" 
872 
end; 

873 

1220  874 

875 

0  876 
(**** Derived rules ****) 
877 

1503  878 
(*Discharge all hypotheses. Need not verify cterms or call fix_shyps. 
0  879 
Repeated hypotheses are discharged only once; fold cannot do this*) 
1220  880 
fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = 
1238  881 
implies_intr_hyps (*no fix_shyps*) 
1220  882 
(Thm{sign=sign, maxidx=maxidx, shyps=shyps, 
250  883 
hyps= disch(As,A), prop= implies$A$prop}) 
0  884 
 implies_intr_hyps th = th; 
885 

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

250  887 
Instantiates the theorem and deletes trivial tpairs. 
0  888 
Resulting sequence may contain multiple elements if the tpairs are 
889 
not all flexflex. *) 

1220  890 
fun flexflex_rule (th as Thm{sign,maxidx,hyps,prop,...}) = 
250  891 
let fun newthm env = 
892 
let val (tpairs,horn) = 

893 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

1220  897 
in fix_shyps [th] (env_codT env) 
898 
(Thm{sign= sign, shyps= [], hyps= hyps, 

899 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  900 
end; 
0  901 
val (tpairs,_) = Logic.strip_flexpairs prop 
902 
in Sequence.maps newthm 

250  903 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  904 
end; 
905 

906 
(*Instantiation of Vars 

1220  907 
A 
908 
 

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

910 
*) 

0  911 

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

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

914 

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

916 
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

917 
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

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

921 
end; 

922 

923 
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

924 
let val {T,sign} = rep_ctyp ctyp 
0  925 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
926 

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

928 
Instantiates distinct Vars by terms of same type. 

929 
Normalizes the new theorem! *) 

1220  930 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop,...}) = 
0  931 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
932 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  933 
val newprop = 
934 
Envir.norm_term (Envir.empty 0) 

935 
(subst_atomic tpairs 

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

1220  937 
val newth = 
938 
fix_shyps [th] (map snd vTs) 

939 
(Thm{sign= newsign, shyps= [], hyps= hyps, 

940 
maxidx= maxidx_of_term newprop, prop= newprop}) 

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

944 
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

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

946 
newth 
0  947 
end 
250  948 
handle TERM _ => 
0  949 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  950 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  951 

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

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

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

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

1238  958 
else fix_shyps [] [] 
959 
(Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], 

960 
prop= implies$A$A}) 

0  961 
end; 
962 

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

964 
fun class_triv thy c = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

966 
val sign = sign_of thy; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

967 
val Cterm {t, maxidx, ...} = 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

968 
cterm_of sign (Logic.mk_inclass (TVar (("'a", 0), [c]), c)) 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

969 
handle TERM (msg, _) => raise THM ("class_triv: " ^ msg, 0, []); 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

970 
in 
1238  971 
fix_shyps [] [] 
972 
(Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t}) 

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

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

974 

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

975 

0  976 
(* Replace all TFrees not in the hyps by new TVars *) 
1220  977 
fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) = 
0  978 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1238  979 
in (*no fix_shyps*) 
980 
Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps, 

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

0  982 
end; 
983 

984 
(* Replace all TVars by new TFrees *) 

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

986 
let val prop' = Type.freeze prop 
1238  987 
in (*no fix_shyps*) 
988 
Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, 

989 
prop=prop'} 

1220  990 
end; 
0  991 

992 

993 
(*** Inference rules for tactics ***) 

994 

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

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

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

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

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

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

1001 
end 

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

1003 

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

1238  1007 
let val Thm{shyps=sshyps,prop=sprop,maxidx=smax,...} = state; 
0  1008 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 
250  1009 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  1010 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
1238  1011 
val (Thm{sign,maxidx,shyps,hyps,prop}) = orule 
0  1012 
val (tpairs,As,B) = Logic.strip_horn prop 
1238  1013 
in (*no fix_shyps*) 
1014 
Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 

1015 
shyps=sshyps union shyps, maxidx= maxidx+smax+1, 

250  1016 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 
1238  1017 
map lift_all As, lift_all B)} 
0  1018 
end; 
1019 

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

1021 
fun assumption i state = 

1220  1022 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  1023 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  1024 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  1025 
fix_shyps [state] (env_codT env) 
1026 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

250  1027 
if Envir.is_empty env then (*avoid wasted normalizations*) 
1028 
Logic.rule_of (tpairs, Bs, C) 

1029 
else (*normalize the new rule fully*) 

1220  1030 
Envir.norm_term env (Logic.rule_of (tpairs, Bs, C))}); 
0  1031 
fun addprfs [] = Sequence.null 
1032 
 addprfs ((t,u)::apairs) = Sequence.seqof (fn()=> Sequence.pull 

1033 
(Sequence.mapp newth 

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

0  1036 
in addprfs (Logic.assum_pairs Bi) end; 
1037 

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

1220  1041 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  1042 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1043 
in if exists (op aconv) (Logic.assum_pairs Bi) 

1220  1044 
then fix_shyps [state] [] 
1045 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, 

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

0  1047 
else raise THM("eq_assumption", 0, [state]) 
1048 
end; 

1049 

1050 

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

1052 

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

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

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

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

1057 
fun rename_params_rule (cs, i) state = 

1220  1058 
let val Thm{sign,maxidx,hyps,prop,...} = state 
0  1059 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
1060 
val iparams = map #1 (Logic.strip_params Bi) 

1061 
val short = length iparams  length cs 

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

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

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

250  1067 
in 
0  1068 
case findrep cs of 
1069 
c::_ => error ("Bound variables not distinct: " ^ c) 

1070 
 [] => (case cs inter freenames of 

1071 
a::_ => error ("Bound/Free variable clash: " ^ a) 

1220  1072 
 [] => fix_shyps [state] [] 
1073 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

1074 
Logic.rule_of(tpairs, Bs@[newBi], C)})) 

0  1075 
end; 
1076 

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

1078 

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

1082 
match_bvs(s, t, if x="" orelse y="" then al 
1238  1083 
else (x,y)::al) 
0  1084 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
1085 
 match_bvs(_,_,al) = al; 

1086 

1087 
(* strip abstractions created by parameters *) 

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

1089 

1090 

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

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

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

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

1098 
 strip(A,_) = f A 

0  1099 
in strip end; 
1100 

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

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

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

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

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

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

1108 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1111 
(case assoc(al,x) of 

1112 
Some(y) => if x mem vids orelse y mem vids then t 

1113 
else Var((y,i),T) 

1114 
 None=> t) 

0  1115 
 rename(Abs(x,T,t)) = 
250  1116 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1117 
T, rename t) 

0  1118 
 rename(f$t) = rename f $ rename t 
1119 
 rename(t) = t; 

250  1120 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1121 
in strip_ren end; 
1122 

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

1124 
fun rename_bvars(dpairs, tpairs, B) = 

250  1125 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1126 

1127 

1128 
(*** RESOLUTION ***) 

1129 

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

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

1131 

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

250  1134 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1135 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1136 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1137 
Const("all",_)$Abs(_,_,t2)) = 
0  1138 
let val (B1,B2) = strip_assums2 (t1,t2) 
1139 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1140 
 strip_assums2 BB = BB; 

1141 

1142 

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

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

1144 
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

1145 
 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

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

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

1150 
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

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

1153 
 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

1154 

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

1155 

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

1160 
If eres_flg then simultaneously proves A1 by assumption. 

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

1164 
local open Sequence; exception Bicompose 

1165 
in 

250  1166 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1167 
(eres_flg, orule, nsubgoal) = 
1258  1168 
let val Thm{maxidx=smax, shyps=sshyps, hyps=shyps, ...} = state 
1169 
and Thm{maxidx=rmax, shyps=rshyps, hyps=rhyps, prop=rprop,...} = orule 

1238  1170 
(*How many hyps to skip over during normalization*) 
1171 
and nlift = Logic.count_prems(strip_all_body Bi, 

1172 
if eres_flg then ~1 else 0) 

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

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

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

1178 
val normp = 

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

1180 
else 

1181 
let val ntps = map (pairself normt) tpairs 

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

1184 
if lifted 

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

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

250  1187 
else if match then raise Bicompose 
1188 
else (*normalize the new rule fully*) 

1189 
(ntps, map normt (Bs @ As), normt C) 

1190 
end 

1258  1191 
val th = (*tuned fix_shyps*) 
1192 
Thm{sign=sign, 

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

1194 
hyps=rhyps union shyps, 

1195 
maxidx=maxidx, prop= Logic.rule_of normp} 

0  1196 
in cons(th, thq) end handle Bicompose => thq 
1197 
val (rtpairs,rhorn) = Logic.strip_flexpairs(rprop); 

1198 
val (rAs,B) = Logic.strip_prems(nsubgoal, [], rhorn) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1222 
(*ordinary resolution*) 

1223 
fun res(None) = null 

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

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

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

1229 
end; 

1230 
end; (*open Sequence*) 

1231 

1232 

1233 
fun bicompose match arg i state = 

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

1235 

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

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

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

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

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

1242 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1243 
end; 
1244 

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

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

250  1247 
fun biresolution match brules i state = 
0  1248 
let val lift = lift_rule(state, i); 
250  1249 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1250 
val B = Logic.strip_assums_concl Bi; 

1251 
val Hs = Logic.strip_assums_hyp Bi; 

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

1253 
fun res [] = Sequence.null 

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

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

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

1259 
else res brules 

0  1260 
in Sequence.flats (res brules) end; 
1261 

1262 

1263 

1264 
(*** Meta simp sets ***) 

1265 

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

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

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

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

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

1273 
net: discrimination net of rewrite rules 

1274 
congs: association list of congruence rules 

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

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

1276 
for generating new names when rewriting under lambda abstractions 
0  1277 
mk_rews: used when local assumptions are added 
1278 
*) 

1279 

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

1280 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1281 
mk_rews = K[]}; 
1282 

1283 
exception SIMPLIFIER of string * thm; 

1284 

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

1285 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1286 

209  1287 
val trace_simp = ref false; 
1288 

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

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

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

1292 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1293 
fun vperm(Var _, Var _) = true 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1294 
 vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1295 
 vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1296 
 vperm(t,u) = (t=u); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1297 

427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1298 
fun var_perm(t,u) = vperm(t,u) andalso 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1299 
eq_set(add_term_vars(t,[]), add_term_vars(u,[])) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1300 

0  1301 
(*simple test for looping rewrite*) 
1302 
fun loops sign prems (lhs,rhs) = 

1023
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1303 
is_Var(lhs) 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1304 
orelse 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1305 
(exists (apl(lhs, Logic.occs)) (rhs::prems)) 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1306 
orelse 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1307 
(null(prems) andalso 
f5f36bdc8003
Fixed bug in the simplifier: added uses of maxidx_of_term to make sure that
nipkow
parents:
979
diff
changeset

1308 
Pattern.matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
1028  1309 
(* the condition "null(prems)" in the last case is necessary because 
1310 
conditional rewrites with extra variables in the conditions may terminate 

1311 
although the rhs is an instance of the lhs. Example: 

1312 
?m < ?n ==> f(?n) == f(?m) 

1313 
*) 

0  1314 

1238  1315 
fun mk_rrule raw_thm = 
1316 
let 

1258  1317 
val thm = strip_shyps raw_thm; 
1238  1318 
val Thm{sign,prop,maxidx,...} = thm; 
1319 
val prems = Logic.strip_imp_prems prop 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1320 
val concl = Logic.strip_imp_concl prop 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1321 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1322 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm) 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1323 
val econcl = Pattern.eta_contract concl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1324 
val (elhs,erhs) = Logic.dest_equals econcl 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1325 
val perm = var_perm(elhs,erhs) andalso not(elhs aconv erhs) 
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1326 
andalso not(is_Var(elhs)) 
1220  1327 
in 
1258  1328 
if not perm andalso loops sign prems (elhs,erhs) then 
1220  1329 
(prtm "Warning: ignoring looping rewrite rule" sign prop; None) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1330 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1331 
end; 
1332 

87  1333 
local 
1334 
fun eq({thm=Thm{prop=p1,...},...}:rrule, 

1335 
{thm=Thm{prop=p2,...},...}:rrule) = p1 aconv p2 

1336 
in 

1337 

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

1338 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1339 
thm as Thm{sign,prop,...}) = 
87  1340 
case mk_rrule thm of 
1341 
None => mss 

1342 
 Some(rrule as {lhs,...}) => 

209  1343 
(trace_thm "Adding rewrite rule:" thm; 
1344 
Mss{net= (Net.insert_term((lhs,rrule),net,eq) 

1345 
handle Net.INSERT => 

87  1346 
(prtm "Warning: ignoring duplicate rewrite rule" sign prop; 
1347 
net)), 

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

1348 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1349 

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

1350 
fun del_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
87  1351 
thm as Thm{sign,prop,...}) = 
1352 
case mk_rrule thm of 

1353 
None => mss 

1354 
 Some(rrule as {lhs,...}) => 

1355 
Mss{net= (Net.delete_term((lhs,rrule),net,eq) 

1356 
handle Net.INSERT => 

1357 
(prtm "Warning: rewrite rule not in simpset" sign prop; 

1358 
net)), 

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

1359 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1360 

1361 
end; 

0  1362 

1363 
val add_simps = foldl add_simp; 

87  1364 
val del_simps = foldl del_simp; 
0  1365 

1366 
fun mss_of thms = add_simps(empty_mss,thms); 

1367 

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

1368 
fun add_cong(Mss{net,congs,bounds,prems,mk_rews},thm) = 
0  1369 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => 
1370 
raise SIMPLIFIER("Congruence not a metaequality",thm) 

678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1371 
(* val lhs = Pattern.eta_contract lhs*) 
0  1372 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1373 
raise SIMPLIFIER("Congruence must start with a constant",thm) 

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

1374 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1375 
prems=prems, mk_rews=mk_rews} 
1376 
end; 

1377 

1378 
val (op add_congs) = foldl add_cong; 

1379 

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

1380 
fun add_prems(Mss{net,congs,bounds,prems,mk_rews},thms) = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1381 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 