author  wenzelm 
Tue, 01 Aug 1995 17:21:57 +0200  
changeset 1220  3b0b8408fc5f 
parent 1195  686e3eb613b9 
child 1229  f191f25a5ec8 
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 = 
12 
sig 

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

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

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

15 
structure Sign : SIGN 
1160  16 

17 
(*certified types*) 

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

18 
type ctyp 
1160  19 
val rep_ctyp : ctyp > {sign: Sign.sg, T: typ} 
20 
val typ_of : ctyp > typ 

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

21 
val ctyp_of : Sign.sg > typ > ctyp 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

22 
val read_ctyp : Sign.sg > string > ctyp 
1160  23 

24 
(*certified terms*) 

25 
type cterm 

26 
val rep_cterm : cterm > {sign: Sign.sg, t: term, T: typ, maxidx: int} 

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

27 
val term_of : cterm > term 
1160  28 
val cterm_of : Sign.sg > term > cterm 
29 
val read_cterm : Sign.sg > string * typ > cterm 

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

30 
val cterm_fun : (term > term) > (cterm > cterm) 
1160  31 
val dest_cimplies : cterm > cterm * cterm 
32 
val read_def_cterm : 

33 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 

34 
string list > bool > string * typ > cterm * (indexname * typ) list 

35 

36 
(*meta theorems*) 

37 
type thm 

38 
exception THM of string * int * thm list 

1220  39 
val rep_thm : thm > {sign: Sign.sg, maxidx: int, 
40 
shyps: sort list, hyps: term list, prop: term} 

1160  41 
val stamps_of_thm : thm > string ref list 
42 
val tpairs_of : thm > (term * term) list 

43 
val prems_of : thm > term list 

44 
val nprems_of : thm > int 

45 
val concl_of : thm > term 

46 
val cprop_of : thm > cterm 

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

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

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

50 

51 
(*theories*) 

52 
type theory 

53 
exception THEORY of string * theory list 

54 
val rep_theory : theory > 

55 
{sign: Sign.sg, new_axioms: term Sign.Symtab.table, parents: theory list} 

56 
val sign_of : theory > Sign.sg 

57 
val syn_of : theory > Sign.Syntax.syntax 

58 
val stamps_of_thy : theory > string ref list 

59 
val parents_of : theory > theory list 

60 
val subthy : theory * theory > bool 

61 
val eq_thy : theory * theory > bool 

62 
val get_axiom : theory > string > thm 

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

64 
val proto_pure_thy : theory 

65 
val pure_thy : theory 

66 
val cpure_thy : theory 

564  67 
local open Sign.Syntax in 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

68 
val add_classes : (class * class list) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

69 
val add_classrel : (class * class) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

70 
val add_defsort : sort > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

71 
val add_types : (string * int * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

72 
val add_tyabbrs : (string * string list * string * mixfix) list 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

74 
val add_tyabbrs_i : (string * string list * typ * mixfix) list 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

76 
val add_arities : (string * sort list * sort) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

77 
val add_consts : (string * string * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

78 
val add_consts_i : (string * typ * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

79 
val add_syntax : (string * string * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

80 
val add_syntax_i : (string * typ * mixfix) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

82 
(string * (ast list > ast)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

83 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

84 
(string * (term list > term)) list * 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

85 
(string * (ast list > ast)) list > theory > theory 
1160  86 
val add_trrules : (string * string) trrule list > theory > theory 
87 
val add_trrules_i : ast trrule list > theory > theory 

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

88 
val add_axioms : (string * string) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

89 
val add_axioms_i : (string * term) list > theory > theory 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

91 
end 
1160  92 
val merge_theories : theory * theory > theory 
93 
val merge_thy_list : bool > theory list > theory 

94 

95 
(*meta rules*) 

1220  96 
val force_strip_shyps : bool ref (* FIXME tmp *) 
97 
val strip_shyps : thm > thm 

98 
val implies_intr_shyps: thm > thm 

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

99 
val assume : cterm > thm 
1160  100 
val implies_intr : cterm > thm > thm 
101 
val implies_elim : thm > thm > thm 

102 
val forall_intr : cterm > thm > thm 

103 
val forall_elim : cterm > thm > thm 

104 
val flexpair_def : thm 

105 
val reflexive : cterm > thm 

106 
val symmetric : thm > thm 

107 
val transitive : thm > thm > thm 

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

108 
val beta_conversion : cterm > thm 
1160  109 
val extensional : thm > thm 
110 
val abstract_rule : string > cterm > thm > thm 

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

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

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

113 
val equal_elim : thm > thm > thm 
1160  114 
val implies_intr_hyps : thm > thm 
721
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

115 
val flexflex_rule : thm > thm Sequence.seq 
1160  116 
val instantiate : 
117 
(indexname * ctyp) list * (cterm * cterm) list > thm > thm 

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

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

119 
val class_triv : theory > class > thm 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

120 
val varifyT : thm > thm 
1160  121 
val freezeT : thm > thm 
122 
val dest_state : thm * int > 

123 
(term * term) list * term list * term * term 

124 
val lift_rule : (thm * int) > thm > thm 

125 
val assumption : int > thm > thm Sequence.seq 

126 
val eq_assumption : int > thm > thm 

127 
val rename_params_rule: string list * int > thm > thm 

128 
val bicompose : bool > bool * thm * int > 

129 
int > thm > thm Sequence.seq 

130 
val biresolution : bool > (bool * thm) list > 

131 
int > thm > thm Sequence.seq 

132 

133 
(*meta simplification*) 

134 
type meta_simpset 

135 
exception SIMPLIFIER of string * thm 

136 
val empty_mss : meta_simpset 

137 
val add_simps : meta_simpset * thm list > meta_simpset 

138 
val del_simps : meta_simpset * thm list > meta_simpset 

139 
val mss_of : thm list > meta_simpset 

140 
val add_congs : meta_simpset * thm list > meta_simpset 

141 
val add_prems : meta_simpset * thm list > meta_simpset 

142 
val prems_of_mss : meta_simpset > thm list 

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

144 
val mk_rews_of_mss : meta_simpset > thm > thm list 

145 
val trace_simp : bool ref 

146 
val rewrite_cterm : bool * bool > meta_simpset > 

147 
(meta_simpset > thm > thm option) > cterm > thm 

250  148 
end; 
0  149 

250  150 
functor ThmFun (structure Logic: LOGIC and Unify: UNIFY and Pattern: PATTERN 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

151 
and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM = 
0  152 
struct 
250  153 

0  154 
structure Sequence = Unify.Sequence; 
155 
structure Envir = Unify.Envir; 

156 
structure Sign = Unify.Sign; 

157 
structure Type = Sign.Type; 

158 
structure Syntax = Sign.Syntax; 

159 
structure Symtab = Sign.Symtab; 

160 

161 

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

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

163 

250  164 
(** certified types **) 
165 

166 
(*certified typs under a signature*) 

167 

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

169 

170 
fun rep_ctyp (Ctyp args) = args; 

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

172 

173 
fun ctyp_of sign T = 

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

175 

176 
fun read_ctyp sign s = 

177 
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

178 

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

179 

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

180 

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

182 

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

184 

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

186 

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

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

189 

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

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

193 
in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} 

194 
end handle TYPE (msg, _, _) 

195 
=> raise TERM ("Term not in signature\n" ^ msg, [tm]); 

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

196 

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

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

199 

250  200 
(*dest_implies for cterms. Note T=prop below*) 
201 
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

202 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  203 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
204 
 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

205 

250  206 

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

207 

574  208 
(** read cterms **) (*exception ERROR*) 
250  209 

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

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

211 
fun read_def_cterm (sign, types, sorts) used freeze (a, T) = 
250  212 
let 
574  213 
val T' = Sign.certify_typ sign T 
214 
handle TYPE (msg, _, _) => error msg; 

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

216 
val (_, t', tye) = 
959  217 
Sign.infer_types sign types sorts used freeze (ts, T'); 
574  218 
val ct = cterm_of sign t' 
219 
handle TERM (msg, _) => error msg; 

250  220 
in (ct, tye) end; 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

221 

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

222 
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

223 

250  224 

225 

1220  226 
(* FIXME > library.ML *) 
227 

228 
fun unions [] = [] 

229 
 unions (xs :: xss) = foldr (op union) (xss, xs); 

230 

231 

232 
(* FIXME > term.ML *) 

233 

234 
(*accumulates the sorts in a type, suppressing duplicates*) 

235 
fun add_typ_sorts (Type (_, Ts), Ss) = foldr add_typ_sorts (Ts, Ss) 

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

237 
 add_typ_sorts (TVar (_, S), Ss) = S ins Ss; 

238 

239 
val add_term_sorts = it_term_types add_typ_sorts; 

240 

241 
fun typ_sorts T = add_typ_sorts (T, []); 

242 
fun term_sorts t = add_term_sorts (t, []); 

243 

244 

245 
(* FIXME move? *) 

246 

247 
fun env_codT (Envir.Envir {iTs, ...}) = map snd iTs; 

248 

249 

250 

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

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

252 

0  253 
datatype thm = Thm of 
1220  254 
{sign: Sign.sg, maxidx: int, 
255 
shyps: sort list, hyps: term list, prop: term}; 

0  256 

250  257 
fun rep_thm (Thm args) = args; 
0  258 

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

259 
(*errors involving theorems*) 
0  260 
exception THM of string * int * thm list; 
261 

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

262 

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

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

264 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  265 

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

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

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

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

270 

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

271 

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

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

273 
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

274 

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

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

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

277 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  278 

279 
(*counts premises in a rule*) 

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

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

281 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  282 

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

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

284 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  285 

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

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

288 
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

289 

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

290 

0  291 

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

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

293 

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

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

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

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

298 
parents: theory list}; 
0  299 

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

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

301 

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

302 
(*errors involving theories*) 
0  303 
exception THEORY of string * theory list; 
304 

305 

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

306 
val sign_of = #sign o rep_theory; 
0  307 
val syn_of = #syn o Sign.rep_sg o sign_of; 
308 

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

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

310 
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

311 

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

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

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

314 

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

315 

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

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

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

318 
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

319 

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

320 

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

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

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

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

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

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

326 
(case Symtab.lookup (new_axioms, name) of 
1220  327 
Some t => Thm {sign = sign, maxidx = maxidx_of_term t, 
328 
shyps = [], hyps = [], prop = t} 

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

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

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

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

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

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

334 

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

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

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

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

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

339 

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

340 

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

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

342 

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

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

344 
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

345 

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

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

347 
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

348 

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

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

350 
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

351 

0  352 

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

353 

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

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

355 

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

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

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

358 

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

359 
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

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

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

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

363 
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

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

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

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

367 
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

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

369 

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

370 

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

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

372 

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

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

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

375 

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

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

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

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

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

381 
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

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

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

384 
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

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

386 
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

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

388 
val add_trrules = ext_sg Sign.add_trrules; 
1160  389 
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

390 
val add_thyname = ext_sg Sign.add_name; 
0  391 

392 

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

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

394 

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

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

396 
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

397 

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

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

399 
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

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

401 

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

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

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

404 
val Cterm {t, T, ...} = cterm_of sg raw_tm 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

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

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

411 

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

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

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

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

415 

564  416 
fun inferT_axm sg (name, pre_tm) = 
959  417 
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

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

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

420 
handle ERROR => err_in_axm name; 
564  421 

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

422 

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

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

424 

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

425 
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

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

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

428 
val axioms = map (apsnd Logic.varify o prep_axm sign) axms; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

432 

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

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

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

435 

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

436 

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

437 

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

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

439 

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

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

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

442 
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

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

444 

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

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

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

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

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

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

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

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

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

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

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

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

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

457 
end; 
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 
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

460 

0  461 

462 

1220  463 
(*** Meta rules ***) 
464 

465 
(** sort contexts **) 

466 

467 
(*account for lost sort constraints*) 

468 
fun fix_shyps ths Ts th = 

469 
let 

470 
fun thm_sorts (Thm {shyps, hyps, prop, ...}) = 

471 
unions (shyps :: term_sorts prop :: map term_sorts hyps); 

472 
val lost_sorts = 

473 
unions (map thm_sorts ths @ map typ_sorts Ts) \\ thm_sorts th; 

474 
val Thm {sign, maxidx, shyps, hyps, prop} = th; 

475 
in 

476 
Thm {sign = sign, maxidx = maxidx, 

477 
shyps = lost_sorts @ shyps, hyps = hyps, prop = prop} 

478 
end; 

479 

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

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

482 
fun strip_shyps th = 

483 
let 

484 
fun sort_hyps_of t = 

485 
term_tfrees t @ map (apfst Syntax.string_of_vname) (term_tvars t); 

0  486 

1220  487 
val Thm {sign, maxidx, shyps, hyps, prop} = th; 
488 
(* FIXME no varnames (?) *) 

489 
val sort_hyps = unions (sort_hyps_of prop :: map sort_hyps_of hyps); 

490 
(* FIXME improve (e.g. only minimal sorts) *) 

491 
val shyps' = filter_out (Sign.nonempty_sort sign sort_hyps) shyps; 

492 
in 

493 
Thm {sign = sign, maxidx = maxidx, 

494 
shyps = 

495 
(if null shyps' orelse not (! force_strip_shyps) then shyps' 

496 
else (* FIXME tmp *) 

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

498 
commas (map Type.str_of_sort shyps')); 

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

500 
[])), 

501 
hyps = hyps, prop = prop} 

502 
end; 

503 

504 
(*discharge all sort hypotheses*) 

505 
fun implies_intr_shyps (th as Thm {shyps = [], ...}) = th 

506 
 implies_intr_shyps (Thm {sign, maxidx, shyps, hyps, prop}) = 

507 
let 

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

509 
val names = 

510 
tl (variantlist (replicate (length shyps + 1) "'", used_names)); 

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

512 

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

514 
val sort_hyps = flat (map2 mk_insort (tfrees, shyps)); 

515 
in 

516 
Thm {sign = sign, maxidx = maxidx, shyps = [], 

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

518 
end; 

519 

520 

521 

522 
(** 'primitive' rules **) 

523 

524 
(*discharge all assumptions t from ts*) 

0  525 
val disch = gen_rem (op aconv); 
526 

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

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

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

1220  535 
else Thm{sign = sign, maxidx = ~1, shyps = [], hyps = [prop], prop = prop} 
0  536 
end; 
537 

1220  538 
(*Implication introduction 
539 
A  B 

540 
 

541 
A ==> B 

542 
*) 

543 
fun implies_intr cA (thB as Thm{sign,maxidx,shyps,hyps,prop}) : thm = 

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

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

1220  548 
shyps = shyps, hyps= disch(hyps,A), prop= implies$A$prop} 
0  549 
handle TERM _ => 
550 
raise THM("implies_intr: incompatible signatures", 0, [thB]) 

551 
end; 

552 

1220  553 
(*Implication elimination 
554 
A ==> B A 

555 
 

556 
B 

557 
*) 

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

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

0  562 
in case prop of 
250  563 
imp$A$B => 
564 
if imp=implies andalso A aconv propA 

1220  565 
then fix_shyps [thAB, thA] [] 
566 
(Thm{sign= merge_thm_sgs(thAB,thA), 

250  567 
maxidx= max[maxA,maxidx], 
1220  568 
shyps= [], 
250  569 
hyps= hypsA union hyps, (*dups suppressed*) 
1220  570 
prop= B}) 
250  571 
else err("major premise") 
572 
 _ => err("major premise") 

0  573 
end; 
250  574 

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

577 
 

578 
!!x.A 

579 
*) 

580 
fun forall_intr cx (th as Thm{sign,maxidx,shyps,hyps,prop}) = 

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

581 
let val x = term_of cx; 
1220  582 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, shyps= shyps, hyps= hyps, 
250  583 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 
0  584 
in case x of 
250  585 
Free(a,T) => 
586 
if exists (apl(x, Logic.occs)) hyps 

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

588 
else result(a,T) 

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

591 
end; 

592 

1220  593 
(*Forall elimination 
594 
!!x.A 

595 
 

596 
A[t/x] 

597 
*) 

598 
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

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

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

1220  604 
else fix_shyps [th] [] 
605 
(Thm{sign= Sign.merge(sign,signt), 

250  606 
maxidx= max[maxidx, maxt], 
1220  607 
shyps= [], hyps= hyps, prop= betapply(A,t)}) 
250  608 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 
0  609 
end 
610 
handle TERM _ => 

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

613 

1220  614 
(* Equality *) 
0  615 

1220  616 
(* Definition of the relation =?= *) 
0  617 
val flexpair_def = 
1220  618 
Thm{sign= Sign.proto_pure, shyps= [], hyps= [], maxidx= 0, 
250  619 
prop= term_of 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
900
diff
changeset

620 
(read_cterm Sign.proto_pure 
250  621 
("(?t =?= ?u) == (?t == ?u::?'a::{})", propT))}; 
0  622 

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

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

625 
let val {sign, t, T, maxidx} = rep_cterm ct 
1220  626 
in Thm{sign= sign, shyps= [], hyps= [], maxidx= maxidx, 
627 
prop= Logic.mk_equals(t,t)} 

0  628 
end; 
629 

630 
(*The symmetry rule 

1220  631 
t==u 
632 
 

633 
u==t 

634 
*) 

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

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

1220  638 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
0  639 
 _ => raise THM("symmetric", 0, [th]); 
640 

641 
(*The transitive rule 

1220  642 
t1==u u==t2 
643 
 

644 
t1==t2 

645 
*) 

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

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

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

650 
in case (prop1,prop2) of 

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

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

655 
hyps= hyps1 union hyps2, 

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

0  657 
 _ => err"premises" 
658 
end; 

659 

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

662 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  663 
in case t of 
250  664 
Abs(_,_,bodt) $ u => 
1220  665 
Thm{sign= sign, shyps= [], hyps= [], 
250  666 
maxidx= maxidx_of_term t, 
667 
prop= Logic.mk_equals(t, subst_bounds([u],bodt))} 

668 
 _ => raise THM("beta_conversion: not a redex", 0, []) 

0  669 
end; 
670 

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

1220  672 
f(x) == g(x) 
673 
 

674 
f == g 

675 
*) 

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

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

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

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

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

685 
 Var _ => 

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

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

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

1220  689 
Thm{sign=sign, shyps=shyps, hyps=hyps, maxidx=maxidx, 
250  690 
prop= Logic.mk_equals(f,g)} 
0  691 
end 
692 
 _ => raise THM("extensional: premise", 0, [th]); 

693 

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

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

1220  696 
t == u 
697 
 

698 
%x.t == %x.u 

699 
*) 

700 
fun abstract_rule a cx (th as Thm{sign,maxidx,shyps,hyps,prop}) = 

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

701 
let val x = term_of cx; 
250  702 
val (t,u) = Logic.dest_equals prop 
703 
handle TERM _ => 

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

0  705 
fun result T = 
1220  706 
Thm{sign= sign, maxidx= maxidx, shyps= shyps, hyps= hyps, 
250  707 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
708 
Abs(a, T, abstract_over (x,u)))} 

0  709 
in case x of 
250  710 
Free(_,T) => 
711 
if exists (apl(x, Logic.occs)) hyps 

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

713 
else result T 

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

716 
end; 

717 

718 
(*The combination rule 

1220  719 
f==g t==u 
720 
 

721 
f(t)==g(u) 

722 
*) 

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

0  726 
in case (prop1,prop2) of 
727 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 

1220  728 
Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
729 
hyps= hyps1 union hyps2, 

250  730 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 
0  731 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
732 
end; 

733 

734 

735 
(*The equal propositions rule 

1220  736 
A==B A 
737 
 

738 
B 

739 
*) 

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

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

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

744 
in case prop1 of 

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

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

749 
hyps= hyps1 union hyps2, 

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

0  751 
 _ => err"major premise" 
752 
end; 

753 

754 

755 
(* Equality introduction 

1220  756 
A==>B B==>A 
757 
 

758 
A==B 

759 
*) 

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

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

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

250  766 
if A aconv A' andalso B aconv B' 
1220  767 
then Thm{sign= merge_thm_sgs(th1,th2), shyps= shyps1 union shyps2, 
768 
hyps= hyps1 union hyps2, 

250  769 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 
770 
else err"not equal" 

0  771 
 _ => err"premises" 
772 
end; 

773 

1220  774 

775 

0  776 
(**** Derived rules ****) 
777 

778 
(*Discharge all hypotheses (need not verify cterms) 

779 
Repeated hypotheses are discharged only once; fold cannot do this*) 

1220  780 
fun implies_intr_hyps (Thm{sign, maxidx, shyps, hyps=A::As, prop}) = 
0  781 
implies_intr_hyps 
1220  782 
(Thm{sign=sign, maxidx=maxidx, shyps=shyps, 
250  783 
hyps= disch(As,A), prop= implies$A$prop}) 
0  784 
 implies_intr_hyps th = th; 
785 

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

250  787 
Instantiates the theorem and deletes trivial tpairs. 
0  788 
Resulting sequence may contain multiple elements if the tpairs are 
789 
not all flexflex. *) 

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

793 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

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

799 
maxidx= maxidx_of_term newprop, prop= newprop}) 

250  800 
end; 
0  801 
val (tpairs,_) = Logic.strip_flexpairs prop 
802 
in Sequence.maps newthm 

250  803 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  804 
end; 
805 

806 
(*Instantiation of Vars 

1220  807 
A 
808 
 

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

810 
*) 

0  811 

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

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

814 

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

816 
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

817 
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

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

821 
end; 

822 

823 
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

824 
let val {T,sign} = rep_ctyp ctyp 
0  825 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
826 

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

828 
Instantiates distinct Vars by terms of same type. 

829 
Normalizes the new theorem! *) 

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

250  833 
val newprop = 
834 
Envir.norm_term (Envir.empty 0) 

835 
(subst_atomic tpairs 

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

1220  837 
val newth = 
838 
fix_shyps [th] (map snd vTs) 

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

840 
maxidx= maxidx_of_term newprop, prop= newprop}) 

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

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

845 
else (*Check types of Vars for agreement*) 

846 
case findrep (map (#1 o dest_Var) (term_vars newprop)) of 

250  847 
ix::_ => raise THM("instantiate: conflicting types for variable " ^ 
848 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

849 
 [] => 

850 
case findrep (map #1 (term_tvars newprop)) of 

851 
ix::_ => raise THM 

852 
("instantiate: conflicting sorts for type variable " ^ 

853 
Syntax.string_of_vname ix ^ "\n", 0, [newth]) 

193  854 
 [] => newth 
0  855 
end 
250  856 
handle TERM _ => 
0  857 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  858 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  859 

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

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

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

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

1220  866 
else Thm{sign= sign, maxidx= maxidx, shyps= [], hyps= [], 
867 
prop= implies$A$A} 

0  868 
end; 
869 

1160  870 
(*Axiomscheme reflecting signature contents: "OFCLASS(?'a::c, c_class)"  
1220  871 
essentially just an instance of A==>A.*) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

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

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

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

876 
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

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

878 
in 
1220  879 
Thm {sign = sign, maxidx = maxidx, shyps = [], hyps = [], prop = t} 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

881 

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

882 

0  883 
(* Replace all TFrees not in the hyps by new TVars *) 
1220  884 
fun varifyT(Thm{sign,maxidx,shyps,hyps,prop}) = 
0  885 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 
1220  886 
in Thm{sign=sign, maxidx=max[0,maxidx], shyps=shyps, hyps=hyps, 
250  887 
prop= Type.varify(prop,tfrees)} 
0  888 
end; 
889 

890 
(* Replace all TVars by new TFrees *) 

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

892 
let val prop' = Type.freeze prop 
1220  893 
in Thm{sign=sign, maxidx=maxidx_of_term prop', shyps=shyps, hyps=hyps, 
894 
prop=prop'} 

895 
end; 

0  896 

897 

898 
(*** Inference rules for tactics ***) 

899 

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

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

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

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

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

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

906 
end 

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

908 

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

912 
let val Thm{prop=sprop,maxidx=smax,...} = state; 

913 
val (Bi::_, _) = Logic.strip_prems(i, [], Logic.skip_flexpairs sprop) 

250  914 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  915 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
1220  916 
val (Thm{sign,maxidx,hyps,prop,...}) = orule 
0  917 
val (tpairs,As,B) = Logic.strip_horn prop 
1220  918 
in fix_shyps [state, orule] [] 
919 
(Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 

920 
shyps=[], maxidx= maxidx+smax+1, 

250  921 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 
1220  922 
map lift_all As, lift_all B)}) 
0  923 
end; 
924 

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

926 
fun assumption i state = 

1220  927 
let val Thm{sign,maxidx,hyps,prop,...} = state; 
0  928 
val (tpairs, Bs, Bi, C) = dest_state(state,i) 
250  929 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
1220  930 
fix_shyps [state] (env_codT env) 
931 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, prop= 

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

934 
else (*normalize the new rule fully*) 

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

938 
(Sequence.mapp newth 

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

0  941 
in addprfs (Logic.assum_pairs Bi) end; 
942 

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

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

1220  949 
then fix_shyps [state] [] 
950 
(Thm{sign=sign, shyps=[], hyps=hyps, maxidx=maxidx, 

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

0  952 
else raise THM("eq_assumption", 0, [state]) 
953 
end; 

954 

955 

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

957 

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

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

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

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

962 
fun rename_params_rule (cs, i) state = 

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

966 
val short = length iparams  length cs 

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

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

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

250  972 
in 
0  973 
case findrep cs of 
974 
c::_ => error ("Bound variables not distinct: " ^ c) 

975 
 [] => (case cs inter freenames of 

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

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

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

0  980 
end; 
981 

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

983 

250  984 
(*Scan a pair of terms; while they are similar, 
0  985 
accumulate corresponding bound vars in "al"*) 
1195
686e3eb613b9
match_bvs no longer puts a name in the alist if it is null ("")
lcp
parents:
1160
diff
changeset

986 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
686e3eb613b9
match_bvs no longer puts a name in the alist if it is null ("")
lcp
parents:
1160
diff
changeset

987 
match_bvs(s, t, if x="" orelse y="" then al 
686e3eb613b9
match_bvs no longer puts a name in the alist if it is null ("")
lcp
parents:
1160
diff
changeset

988 
else (x,y)::al) 
0  989 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 
990 
 match_bvs(_,_,al) = al; 

991 

992 
(* strip abstractions created by parameters *) 

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

994 

995 

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

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

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

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

1003 
 strip(A,_) = f A 

0  1004 
in strip end; 
1005 

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

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

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

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

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

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

1013 
(*unknowns appearing elsewhere be preserved!*) 

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

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

1016 
(case assoc(al,x) of 

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

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

1019 
 None=> t) 

0  1020 
 rename(Abs(x,T,t)) = 
250  1021 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
1022 
T, rename t) 

0  1023 
 rename(f$t) = rename f $ rename t 
1024 
 rename(t) = t; 

250  1025 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  1026 
in strip_ren end; 
1027 

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

1029 
fun rename_bvars(dpairs, tpairs, B) = 

250  1030 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  1031 

1032 

1033 
(*** RESOLUTION ***) 

1034 

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

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

1036 

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

250  1039 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
1040 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  1041 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  1042 
Const("all",_)$Abs(_,_,t2)) = 
0  1043 
let val (B1,B2) = strip_assums2 (t1,t2) 
1044 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

1045 
 strip_assums2 BB = BB; 

1046 

1047 

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

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

1049 
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

1050 
 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

1051 
let val Envir.Envir{iTs, ...} = env 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1052 
val T' = typ_subst_TVars iTs T 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1053 
(*Must instantiate types of parameters because they are flattened; 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

1055 
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

1056 
 norm_term_skip env n (Const("==>", _) $ A $ B) = 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1057 
implies $ A $ norm_term_skip env (n1) B 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1058 
 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

1059 

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

1060 

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

1065 
If eres_flg then simultaneously proves A1 by assumption. 

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

1069 
local open Sequence; exception Bicompose 

1070 
in 

250  1071 
fun bicompose_aux match (state, (stpairs, Bs, Bi, C), lifted) 
0  1072 
(eres_flg, orule, nsubgoal) = 
1073 
let val Thm{maxidx=smax, hyps=shyps, ...} = state 

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

1074 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1075 
(*How many hyps to skip over during normalization*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1076 
and nlift = Logic.count_prems(strip_all_body Bi, 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1077 
if eres_flg then ~1 else 0) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

1083 
val normp = 

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

1085 
else 

1086 
let val ntps = map (pairself normt) tpairs 

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

1087 
in if the (Envir.minidx env) > smax then 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1088 
(*no assignments in state; normalize the rule only*) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

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

1090 
then (ntps, Bs @ map (norm_term_skip env nlift) As, C) 
479832ff2d29
Pure/thm/norm_term_skip: new, for skipping normalization of the context
lcp
parents:
678
diff
changeset

1091 
else (ntps, Bs @ map normt As, C) 
250  1092 
else if match then raise Bicompose 
1093 
else (*normalize the new rule fully*) 

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

1095 
end 

1220  1096 
val th = 
1097 
fix_shyps [state, orule] (env_codT env) 

1098 
(Thm{sign=sign, shyps=[], hyps=rhyps union shyps, 

1099 
maxidx=maxidx, prop= Logic.rule_of normp}) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1126 
(*ordinary resolution*) 

1127 
fun res(None) = null 

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

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

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

1133 
end; 

1134 
end; (*open Sequence*) 

1135 

1136 

1137 
fun bicompose match arg i state = 

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

1139 

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

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

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

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

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

1146 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1147 
end; 
1148 

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

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

250  1151 
fun biresolution match brules i state = 
0  1152 
let val lift = lift_rule(state, i); 
250  1153 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1154 
val B = Logic.strip_assums_concl Bi; 

1155 
val Hs = Logic.strip_assums_hyp Bi; 

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

1157 
fun res [] = Sequence.null 

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

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

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

1163 
else res brules 

0  1164 
in Sequence.flats (res brules) end; 
1165 

1166 

1167 

1168 
(*** Meta simp sets ***) 

1169 

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

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

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

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

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

1177 
net: discrimination net of rewrite rules 

1178 
congs: association list of congruence rules 

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

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

1180 
for generating new names when rewriting under lambda abstractions 
0  1181 
mk_rews: used when local assumptions are added 
1182 
*) 

1183 

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

1184 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1185 
mk_rews = K[]}; 
1186 

1187 
exception SIMPLIFIER of string * thm; 

1188 

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

1189 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1190 

209  1191 
val trace_simp = ref false; 
1192 

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

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

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

1196 

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

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

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

1199 
 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

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

1201 

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

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

1203 
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

1204 

0  1205 
(*simple test for looping rewrite*) 
1206 
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

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

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

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

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

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

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

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

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

1217 
*) 

0  1218 

1220  1219 
fun mk_rrule (thm as Thm{sign,prop,maxidx,...}) = 
0  1220 
let val prems = Logic.strip_imp_prems prop 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

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

1222 
val (lhs,_) = Logic.dest_equals concl handle TERM _ => 
0  1223 
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

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

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

1226 
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

1227 
andalso not(is_Var(elhs)) 
1220  1228 
in 
1229 
if not (null (#shyps (rep_thm (strip_shyps thm)))) then (* FIXME tmp hack *) 

1230 
raise SIMPLIFIER ("Rewrite rule may not contain sort hypotheses", thm) 

1231 
else if not perm andalso loops sign prems (elhs,erhs) then 

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

1233 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1234 
end; 
1235 

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

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

1239 
in 

1240 

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

1241 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1242 
thm as Thm{sign,prop,...}) = 
87  1243 
case mk_rrule thm of 
1244 
None => mss 

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

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

1248 
handle Net.INSERT => 

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

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

1251 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1252 

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

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

1256 
None => mss 

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

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

1259 
handle Net.INSERT => 

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

1261 
net)), 

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

1262 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1263 

1264 
end; 

0  1265 

1266 
val add_simps = foldl add_simp; 

87  1267 
val del_simps = foldl del_simp; 
0  1268 

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

1270 

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

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

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

1274 
(* val lhs = Pattern.eta_contract lhs*) 
0  1275 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 
1276 
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

1277 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1278 
prems=prems, mk_rews=mk_rews} 
1279 
end; 

1280 

1281 
val (op add_congs) = foldl add_cong; 

1282 

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

1283 
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

1284 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1285 

1286 
fun prems_of_mss(Mss{prems,...}) = prems; 

1287 

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

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

1289 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1290 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1291 

1292 

250  1293 
(*** Metalevel rewriting 
0  1294 
uses conversions, omitting proofs for efficiency. See 
250  1295 
L C Paulson, A higherorder implementation of rewriting, 
1296 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1297 

1298 
type prover = meta_simpset > thm > thm option; 

1299 
type termrec = (Sign.sg * term list) * term; 

1300 
type conv = meta_simpset > termrec > termrec; 

1301 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1302 
datatype order = LESS  EQUAL  GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1303 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1304 
fun stringord(a,b:string) = if a<b then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1305 
if a=b then EQUAL else GREATER; 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1306 

4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1307 
fun intord(i,j:int) = if i<j then LESS else 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1308 
if i=j then EQUAL else GREATER; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1309 

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

1310 
(* NB: nonlinearity of the ordering is not a soundness problem *) 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1311 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1312 
(* FIXME: "***ABSTRACTION***" is a hack and makes the ordering nonlinear *) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1313 
fun string_of_hd(Const(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1314 
 string_of_hd(Free(a,_)) = a 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1315 
 string_of_hd(Var(v,_)) = Syntax.string_of_vname v 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1316 
 string_of_hd(Bound i) = string_of_int i 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1317 
 string_of_hd(Abs _) = "***ABSTRACTION***"; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1318 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1319 
(* a strict (not reflexive) linear wellfounded ACcompatible ordering 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1320 
* for terms: 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1321 
* s < t <=> 1. size(s) < size(t) or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1322 
2. size(s) = size(t) and s=f(...) and t = g(...) and f<g or 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1323 
3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1324 
(s1..sn) < (t1..tn) (lexicographically) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

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

1326 

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

1327 
(* FIXME: should really take types into account as well. 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1328 
* Otherwise nonlinear *) 
622
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1329 
fun termord(Abs(_,_,t),Abs(_,_,u)) = termord(t,u) 
bf9821f58781
Modified termord to take account of the AbsAbs case.
nipkow
parents:
574
diff
changeset

1330 
 termord(t,u) = 
305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1331 
(case intord(size_of_term t,size_of_term u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1332 
EQUAL => let val (f,ts) = strip_comb t and (g,us) = strip_comb u 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1333 
in case stringord(string_of_hd f, string_of_hd g) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1334 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1335 
 ord => ord 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1336 
end 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1337 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1338 
and lextermord(t::ts,u::us) = 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1339 
(case termord(t,u) of 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1340 
EQUAL => lextermord(ts,us) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1341 
 ord => ord) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1342 
 lextermord([],[]) = EQUAL 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1343 
 lextermord _ = error("lextermord"); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1344 

305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1345 
fun termless tu = (termord tu = LESS); 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1346 

1065
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1347 
fun check_conv(thm as Thm{hyps,prop,sign,maxidx,...}, prop0) = 
432  1348 
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; 
1349 
trace_term "Should have proved" sign prop0; 

1350 
None) 

0  1351 
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0) 
1352 
in case prop of 

1353 
Const("==",_) $ lhs $ rhs => 

1354 
if (lhs = lhs0) orelse 

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

1355 
(lhs aconv Envir.norm_term (Envir.empty 0) lhs0) 
1065
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1356 
then (trace_thm "SUCCEEDED" thm; Some(hyps,maxidx,rhs)) 
0  1357 
else err() 
1358 
 _ => err() 

1359 
end; 

1360 

659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1361 
fun ren_inst(insts,prop,pat,obj) = 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1362 
let val ren = match_bvs(pat,obj,[]) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1363 
fun renAbs(Abs(x,T,b)) = 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1364 
Abs(case assoc(ren,x) of None => x  Some(y) => y, T, renAbs(b)) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1365 
 renAbs(f$t) = renAbs(f) $ renAbs(t) 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1366 
 renAbs(t) = t 
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1367 
in subst_vars insts (if null(ren) then prop else renAbs(prop)) end; 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1368 

659
95ed2ccb4438
Prepared the code for preservation of bound var names during rewriting. Still
nipkow
parents:
623
diff
changeset

1369 

0  1370 
(*Conversion to apply the meta simpset to a term*) 
1065
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1371 
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,maxidxt,t) = 
678
6151b7f3b606
Modified pattern.ML to perform proper matching of HigherOrder Patterns.
nipkow
parents:
659
diff
changeset

1372 
let val etat = Pattern.eta_contract t; 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1373 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = 
250  1374 
let val unit = if Sign.subsig(sign,signt) then () 
446
3ee5c9314efe
rewritec now uses trace_thm for it's "rewrite rule from different theory"
clasohm
parents:
432
diff
changeset

1375 
else (trace_thm"Warning: rewrite rule from different theory" 
3ee5c9314efe
rewritec now uses trace_thm for it's "rewrite rule from different theory"
clasohm
parents:
432
diff
changeset

1376 
thm; 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1377 
raise Pattern.MATCH) 
1065
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1378 
val rprop = if maxidxt = ~1 then prop 
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1379 
else Logic.incr_indexes([],maxidxt+1) prop; 
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1380 
val rlhs = if maxidxt = ~1 then lhs 
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1381 
else fst(Logic.dest_equals(Logic.strip_imp_concl rprop)) 
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1382 
val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (rlhs,etat) 
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1383 
val prop' = ren_inst(insts,rprop,rlhs,t); 
0  1384 
val hyps' = hyps union hypst; 
1065
8425cb5acb77
Fixed old bug in the simplifier. Term to be simplified now carries around its
nipkow
parents:
1028
diff
changeset

1385 
val maxidx' = maxidx_of_term prop' 