author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 432  0d1071ac599c 
child 446  3ee5c9314efe 
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 

250  6 
The abstract types "theory" and "thm". 
7 
Also "cterm" / "ctyp" (certified terms / typs under a signature). 

0  8 
*) 
9 

250  10 
signature THM = 
11 
sig 

0  12 
structure Envir : ENVIR 
13 
structure Sequence : SEQUENCE 

14 
structure Sign : SIGN 

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

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

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

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

18 
type theory 
0  19 
type meta_simpset 
20 
exception THM of string * int * thm list 

21 
exception THEORY of string * theory list 

22 
exception SIMPLIFIER of string * thm 

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

23 
(*certified terms/types; previously in sign.ML*) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

24 
val cterm_of: Sign.sg > term > cterm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

25 
val ctyp_of: Sign.sg > typ > ctyp 
250  26 
val read_ctyp: Sign.sg > string > ctyp 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

27 
val read_cterm: Sign.sg > string * typ > cterm 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

28 
val rep_cterm: cterm > {T: typ, t: term, sign: Sign.sg, maxidx: int} 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

29 
val rep_ctyp: ctyp > {T: typ, sign: Sign.sg} 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

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

31 
val typ_of: ctyp > typ 
250  32 
val cterm_fun: (term > term) > (cterm > cterm) 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

33 
(*end of cterm/ctyp functions*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

34 

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

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

36 
local open Sign.Syntax Sign.Syntax.Mixfix in (* FIXME remove ...Mixfix *) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

37 
val add_classes: (class list * class * class list) list > theory > theory 
421  38 
val add_classrel: (class * class) list > theory > theory 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

39 
val add_defsort: sort > theory > theory 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

40 
val add_types: (string * int * mixfix) list > theory > theory 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

55 
val add_trrules: xrule list > theory > theory 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

60 
val cert_axm: Sign.sg > string * term > string * term 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

61 
val read_axm: Sign.sg > string * string > string * term 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

62 
val abstract_rule: string > cterm > thm > thm 
0  63 
val add_congs: meta_simpset * thm list > meta_simpset 
64 
val add_prems: meta_simpset * thm list > meta_simpset 

65 
val add_simps: meta_simpset * thm list > meta_simpset 

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

66 
val assume: cterm > thm 
250  67 
val assumption: int > thm > thm Sequence.seq 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

68 
val axioms_of: theory > (string * term) list 
250  69 
val beta_conversion: cterm > thm 
70 
val bicompose: bool > bool * thm * int > int > thm > thm Sequence.seq 

71 
val biresolution: bool > (bool*thm)list > int > thm > thm Sequence.seq 

72 
val combination: thm > thm > thm 

73 
val concl_of: thm > term 

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

74 
val cprop_of: thm > cterm 
87  75 
val del_simps: meta_simpset * thm list > meta_simpset 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

76 
val dest_cimplies: cterm > cterm*cterm 
0  77 
val dest_state: thm * int > (term*term)list * term list * term * term 
78 
val empty_mss: meta_simpset 

250  79 
val eq_assumption: int > thm > thm 
0  80 
val equal_intr: thm > thm > thm 
81 
val equal_elim: thm > thm > thm 

82 
val extend_theory: theory > string 

250  83 
> (class * class list) list * sort 
84 
* (string list * int)list 

85 
* (string * string list * string) list 

86 
* (string list * (sort list * class))list 

87 
* (string list * string)list * Sign.Syntax.sext option 

88 
> (string*string)list > theory 

89 
val extensional: thm > thm 

90 
val flexflex_rule: thm > thm Sequence.seq 

91 
val flexpair_def: thm 

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

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

93 
val forall_intr: cterm > thm > thm 
0  94 
val freezeT: thm > thm 
95 
val get_axiom: theory > string > thm 

96 
val implies_elim: thm > thm > thm 

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

97 
val implies_intr: cterm > thm > thm 
0  98 
val implies_intr_hyps: thm > thm 
250  99 
val instantiate: (indexname*ctyp)list * (cterm*cterm)list 
0  100 
> thm > thm 
101 
val lift_rule: (thm * int) > thm > thm 

102 
val merge_theories: theory * theory > theory 

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

103 
val merge_thy_list: bool > theory list > theory 
0  104 
val mk_rews_of_mss: meta_simpset > thm > thm list 
105 
val mss_of: thm list > meta_simpset 

106 
val nprems_of: thm > int 

107 
val parents_of: theory > theory list 

108 
val prems_of: thm > term list 

109 
val prems_of_mss: meta_simpset > thm list 

110 
val pure_thy: theory 

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

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

112 
Sign.sg * (indexname > typ option) * (indexname > sort option) > 
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

113 
string * typ > cterm * (indexname * typ) list 
250  114 
val reflexive: cterm > thm 
0  115 
val rename_params_rule: string list * int > thm > thm 
116 
val rep_thm: thm > {prop: term, hyps: term list, maxidx: int, sign: Sign.sg} 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

117 
val rewrite_cterm: 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

118 
bool*bool > meta_simpset > (meta_simpset > thm > thm option) 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

119 
> cterm > thm 
0  120 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset 
421  121 
val rep_theory: theory > {sign: Sign.sg, new_axioms: term Sign.Symtab.table, 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

123 
val subthy: theory * theory > bool 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

124 
val eq_thy: theory * theory > bool 
250  125 
val sign_of: theory > Sign.sg 
0  126 
val syn_of: theory > Sign.Syntax.syntax 
127 
val stamps_of_thm: thm > string ref list 

128 
val stamps_of_thy: theory > string ref list 

250  129 
val symmetric: thm > thm 
0  130 
val tpairs_of: thm > (term*term)list 
131 
val trace_simp: bool ref 

132 
val transitive: thm > thm > thm 

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

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

134 
val class_triv: theory > class > thm 
0  135 
val varifyT: thm > thm 
250  136 
end; 
0  137 

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

139 
and Net:NET sharing type Pattern.type_sig = Unify.Sign.Type.type_sig): THM = 
0  140 
struct 
250  141 

0  142 
structure Sequence = Unify.Sequence; 
143 
structure Envir = Unify.Envir; 

144 
structure Sign = Unify.Sign; 

145 
structure Type = Sign.Type; 

146 
structure Syntax = Sign.Syntax; 

147 
structure Symtab = Sign.Symtab; 

148 

149 

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

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

151 

250  152 
(** certified types **) 
153 

154 
(*certified typs under a signature*) 

155 

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

157 

158 
fun rep_ctyp (Ctyp args) = args; 

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

160 

161 
fun ctyp_of sign T = 

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

163 

164 
fun read_ctyp sign s = 

165 
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

166 

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

167 

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

168 

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

170 

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

172 

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

174 

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

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

177 

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

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

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

182 
end handle TYPE (msg, _, _) 

183 
=> 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

184 

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

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

187 

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

190 
(Cterm{sign=sign, T=T, maxidx=maxidx, t=A}, 
250  191 
Cterm{sign=sign, T=T, maxidx=maxidx, t=B}) 
192 
 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

193 

250  194 

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

195 

250  196 
(** read cterms **) 
197 

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

199 

200 
fun read_def_cterm (sign, types, sorts) (a, T) = 

201 
let 

202 
val {tsig, const_tab, syn, ...} = Sign.rep_sg sign; 

203 
val showtyp = Sign.string_of_typ sign; 

204 
val showterm = Sign.string_of_term sign; 

205 

206 
fun termerr [] = "" 

207 
 termerr [t] = "\nInvolving this term:\n" ^ showterm t 

208 
 termerr ts = "\nInvolving these terms:\n" ^ cat_lines (map showterm ts); 

209 

210 
val T' = Sign.certify_typ sign T 

211 
handle TYPE (msg, _, _) => error msg; 

212 
val t = Syntax.read syn T' a; 

213 
val (t', tye) = Type.infer_types (tsig, const_tab, types, sorts, T', t) 

214 
handle TYPE (msg, Ts, ts) => error ("Type checking error: " ^ msg ^ "\n" 

215 
^ cat_lines (map showtyp Ts) ^ termerr ts); 

216 
val ct = cterm_of sign t' handle TERM (msg, _) => error msg; 

217 
in (ct, tye) end; 

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

218 

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

219 
fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None); 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

220 

250  221 

222 

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

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

224 

0  225 
datatype thm = Thm of 
250  226 
{sign: Sign.sg, maxidx: int, hyps: term list, prop: term}; 
0  227 

250  228 
fun rep_thm (Thm args) = args; 
0  229 

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

230 
(*errors involving theorems*) 
0  231 
exception THM of string * int * thm list; 
232 

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

233 

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

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

235 
val stamps_of_thm = #stamps o Sign.rep_sg o sign_of_thm; 
0  236 

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

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

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

239 
Sign.merge (pairself sign_of_thm (th1, th2)) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

240 
handle TERM _ => raise THM ("incompatible signatures", 0, [th1, th2]); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

241 

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

242 

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

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

244 
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

245 

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

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

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

248 
Logic.strip_imp_prems (Logic.skip_flexpairs prop); 
0  249 

250 
(*counts premises in a rule*) 

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

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

252 
Logic.count_prems (Logic.skip_flexpairs prop, 0); 
0  253 

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

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

255 
fun concl_of (Thm {prop, ...}) = Logic.strip_imp_concl prop; 
0  256 

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

257 
(*the statement of any thm is a cterm*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

258 
fun cprop_of (Thm {sign, maxidx, hyps, prop}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

259 
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

260 

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

261 

0  262 

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

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

264 

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

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

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

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

269 
parents: theory list}; 
0  270 

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

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

272 

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

273 
(*errors involving theories*) 
0  274 
exception THEORY of string * theory list; 
275 

276 

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

277 
val sign_of = #sign o rep_theory; 
0  278 
val syn_of = #syn o Sign.rep_sg o sign_of; 
279 

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

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

281 
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

282 

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

283 
(*return additional axioms of this theory node*) 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

284 
val axioms_of = Symtab.dest o #new_axioms o rep_theory; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

285 

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

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

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

288 

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

289 

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

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

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

292 
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

293 

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

294 

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

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

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

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

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

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

300 
(case Symtab.lookup (new_axioms, name) of 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

301 
Some t => 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

302 
Thm {sign = sign, maxidx = maxidx_of_term t, hyps = [], prop = t} 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

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

308 

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

309 

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

310 
(* the Pure theory *) 
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 
val pure_thy = 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

313 
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

314 

0  315 

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

316 

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

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

318 

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

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

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

321 

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

322 
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

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

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

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

326 
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

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

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

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

330 
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

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

332 

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

333 

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

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

335 

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

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

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

338 

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

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

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

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

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

344 
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

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

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

347 
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

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

349 
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

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

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

352 
val add_thyname = ext_sg Sign.add_name; 
0  353 

354 

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

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

356 

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

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

358 
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

359 

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

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

361 
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

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

363 

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

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

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

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

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

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

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

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

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

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

373 

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

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

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

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

377 

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

378 

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

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

380 

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

381 
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

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

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

384 
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

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

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

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

388 

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

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

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

391 

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

392 

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

393 
(* extend theory (old) *) (* FIXME remove *) 
0  394 

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

395 
(*converts Frees to Vars: axioms can be written without question marks*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

397 
Logic.varify (term_of (read_cterm sign (sP, propT))); 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

398 

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

399 
(*read an axiom for a new theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

400 
fun read_ax sign (a, sP) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

401 
(a, prepare_axiom sign sP) handle ERROR => err_in_axm a; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

402 

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

403 
(*extension of a theory with given classes, types, constants and syntax; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

404 
reads the axioms from strings: axpairs have the form (axname, axiom)*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

405 
fun extend_theory thy thyname ext axpairs = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

407 
val Theory {sign, ...} = thy; 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

408 

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

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

410 
val axioms = map (read_ax sign1) axpairs; 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

412 
writeln "WARNING: called obsolete function \"extend_theory\""; 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

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

415 

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

416 

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

417 

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

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

419 

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

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

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

422 
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

423 
val is_draft = Sign.is_draft o sign_of; 
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 add_sign (sg, Theory {sign, ...}) = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

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

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

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

433 
(if mk_draft then Sign.make_draft else I) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

438 

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

439 
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

440 

0  441 

442 

443 
(**** Primitive rules ****) 

444 

445 
(* discharge all assumptions t from ts *) 

446 
val disch = gen_rem (op aconv); 

447 

448 
(*The assumption rule AA in a theory *) 

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

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

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

0  456 
else Thm{sign = sign, maxidx = ~1, hyps = [prop], prop = prop} 
457 
end; 

458 

250  459 
(* Implication introduction 
460 
A  B 

461 
 

462 
A ==> B *) 

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

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

468 
hyps= disch(hyps,A), prop= implies$A$prop} 

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

471 
end; 

472 

473 
(* Implication elimination 

250  474 
A ==> B A 
475 
 

476 
B *) 

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

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

0  481 
in case prop of 
250  482 
imp$A$B => 
483 
if imp=implies andalso A aconv propA 

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

484 
then Thm{sign= merge_thm_sgs(thAB,thA), 
250  485 
maxidx= max[maxA,maxidx], 
486 
hyps= hypsA union hyps, (*dups suppressed*) 

487 
prop= B} 

488 
else err("major premise") 

489 
 _ => err("major premise") 

0  490 
end; 
250  491 

0  492 
(* Forall introduction. The Free or Var x must not be free in the hypotheses. 
493 
A 

494 
 

495 
!!x.A *) 

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

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

497 
let val x = term_of cx; 
0  498 
fun result(a,T) = Thm{sign= sign, maxidx= maxidx, hyps= hyps, 
250  499 
prop= all(T) $ Abs(a, T, abstract_over (x,prop))} 
0  500 
in case x of 
250  501 
Free(a,T) => 
502 
if exists (apl(x, Logic.occs)) hyps 

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

504 
else result(a,T) 

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

507 
end; 

508 

509 
(* Forall elimination 

250  510 
!!x.A 
511 
 

512 
A[t/x] *) 

0  513 
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

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

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

519 
else Thm{sign= Sign.merge(sign,signt), 

520 
maxidx= max[maxidx, maxt], 

521 
hyps= hyps, prop= betapply(A,t)} 

522 
 _ => raise THM("forall_elim: not quantified", 0, [th]) 

0  523 
end 
524 
handle TERM _ => 

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

527 

528 
(*** Equality ***) 

529 

530 
(*Definition of the relation =?= *) 

531 
val flexpair_def = 

250  532 
Thm{sign= Sign.pure, hyps= [], maxidx= 0, 
533 
prop= term_of 

534 
(read_cterm Sign.pure 

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

0  536 

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

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

539 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  540 
in Thm{sign= sign, hyps= [], maxidx= maxidx, prop= Logic.mk_equals(t,t)} 
541 
end; 

542 

543 
(*The symmetry rule 

544 
t==u 

545 
 

546 
u==t *) 

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

548 
case prop of 

549 
(eq as Const("==",_)) $ t $ u => 

250  550 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= eq$u$t} 
0  551 
 _ => raise THM("symmetric", 0, [th]); 
552 

553 
(*The transitive rule 

554 
t1==u u==t2 

555 
 

556 
t1==t2 *) 

557 
fun transitive th1 th2 = 

558 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

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

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

561 
in case (prop1,prop2) of 

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

250  563 
if not (u aconv u') then err"middle term" else 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

564 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  565 
maxidx= max[max1,max2], prop= eq$t1$t2} 
0  566 
 _ => err"premises" 
567 
end; 

568 

569 
(*Betaconversion: maps (%(x)t)(u) to the theorem (%(x)t)(u) == t[u/x] *) 

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

571 
let val {sign, t, T, maxidx} = rep_cterm ct 
0  572 
in case t of 
250  573 
Abs(_,_,bodt) $ u => 
574 
Thm{sign= sign, hyps= [], 

575 
maxidx= maxidx_of_term t, 

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

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

0  578 
end; 
579 

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

581 
f(x) == g(x) 

582 
 

583 
f == g *) 

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

585 
case prop of 

586 
(Const("==",_)) $ (f$x) $ (g$y) => 

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

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

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

593 
 Var _ => 

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

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

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

597 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

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

601 

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

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

604 
t == u 

605 
 

606 
%(x)t == %(x)u *) 

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

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

608 
let val x = term_of cx; 
250  609 
val (t,u) = Logic.dest_equals prop 
610 
handle TERM _ => 

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

0  612 
fun result T = 
613 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

250  614 
prop= Logic.mk_equals(Abs(a, T, abstract_over (x,t)), 
615 
Abs(a, T, abstract_over (x,u)))} 

0  616 
in case x of 
250  617 
Free(_,T) => 
618 
if exists (apl(x, Logic.occs)) hyps 

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

620 
else result T 

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

623 
end; 

624 

625 
(*The combination rule 

626 
f==g t==u 

627 
 

628 
f(t)==g(u) *) 

629 
fun combination th1 th2 = 

630 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

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

632 
in case (prop1,prop2) of 

633 
(Const("==",_) $ f $ g, Const("==",_) $ t $ u) => 

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

634 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  635 
maxidx= max[max1,max2], prop= Logic.mk_equals(f$t, g$u)} 
0  636 
 _ => raise THM("combination: premises", 0, [th1,th2]) 
637 
end; 

638 

639 

640 
(*The equal propositions rule 

641 
A==B A 

642 
 

643 
B *) 

644 
fun equal_elim th1 th2 = 

645 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

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

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

648 
in case prop1 of 

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

250  650 
if not (prop2 aconv A) then err"not equal" else 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

651 
Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  652 
maxidx= max[max1,max2], prop= B} 
0  653 
 _ => err"major premise" 
654 
end; 

655 

656 

657 
(* Equality introduction 

658 
A==>B B==>A 

659 
 

660 
A==B *) 

661 
fun equal_intr th1 th2 = 

662 
let val Thm{maxidx=max1, hyps=hyps1, prop=prop1,...} = th1 

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

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

665 
in case (prop1,prop2) of 

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

250  667 
if A aconv A' andalso B aconv B' 
387
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

668 
then Thm{sign= merge_thm_sgs(th1,th2), hyps= hyps1 union hyps2, 
250  669 
maxidx= max[max1,max2], prop= Logic.mk_equals(A,B)} 
670 
else err"not equal" 

0  671 
 _ => err"premises" 
672 
end; 

673 

674 
(**** Derived rules ****) 

675 

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

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

678 
fun implies_intr_hyps (Thm{sign, maxidx, hyps=A::As, prop}) = 

679 
implies_intr_hyps 

250  680 
(Thm{sign=sign, maxidx=maxidx, 
681 
hyps= disch(As,A), prop= implies$A$prop}) 

0  682 
 implies_intr_hyps th = th; 
683 

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

250  685 
Instantiates the theorem and deletes trivial tpairs. 
0  686 
Resulting sequence may contain multiple elements if the tpairs are 
687 
not all flexflex. *) 

688 
fun flexflex_rule (Thm{sign,maxidx,hyps,prop}) = 

250  689 
let fun newthm env = 
690 
let val (tpairs,horn) = 

691 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

695 
in Thm{sign= sign, hyps= hyps, 

696 
maxidx= maxidx_of_term newprop, prop= newprop} 

697 
end; 

0  698 
val (tpairs,_) = Logic.strip_flexpairs prop 
699 
in Sequence.maps newthm 

250  700 
(Unify.smash_unifiers(sign, Envir.empty maxidx, tpairs)) 
0  701 
end; 
702 

703 
(*Instantiation of Vars 

250  704 
A 
705 
 

706 
A[t1/v1,....,tn/vn] *) 

0  707 

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

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

710 

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

712 
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

713 
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

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

717 
end; 

718 

719 
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

720 
let val {T,sign} = rep_ctyp ctyp 
0  721 
in (Sign.merge(sign,sign'), (v,T)::vTs) end; 
722 

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

724 
Instantiates distinct Vars by terms of same type. 

725 
Normalizes the new theorem! *) 

250  726 
fun instantiate (vcTs,ctpairs) (th as Thm{sign,maxidx,hyps,prop}) = 
0  727 
let val (newsign,tpairs) = foldr add_ctpair (ctpairs, (sign,[])); 
728 
val (newsign,vTs) = foldr add_ctyp (vcTs, (newsign,[])); 

250  729 
val newprop = 
730 
Envir.norm_term (Envir.empty 0) 

731 
(subst_atomic tpairs 

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

0  733 
val newth = Thm{sign= newsign, hyps= hyps, 
250  734 
maxidx= maxidx_of_term newprop, prop= newprop} 
735 
in if not(instl_ok(map #1 tpairs)) 

193  736 
then raise THM("instantiate: variables not distinct", 0, [th]) 
737 
else if not(null(findrep(map #1 vTs))) 

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

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

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

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

743 
 [] => 

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

745 
ix::_ => raise THM 

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

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

193  748 
 [] => newth 
0  749 
end 
250  750 
handle TERM _ => 
0  751 
raise THM("instantiate: incompatible signatures",0,[th]) 
193  752 
 TYPE _ => raise THM("instantiate: type conflict", 0, [th]); 
0  753 

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

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

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

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

0  760 
else Thm{sign= sign, maxidx= maxidx, hyps= [], prop= implies$A$A} 
761 
end; 

762 

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

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

764 
Is weaker than some definition of c_class, e.g. "c_class == %x.T"; 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

765 
may be interpreted as an instance of A==>A.*) 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

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

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

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

770 
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

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

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

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

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

775 

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

776 

0  777 
(* Replace all TFrees not in the hyps by new TVars *) 
778 
fun varifyT(Thm{sign,maxidx,hyps,prop}) = 

779 
let val tfrees = foldr add_term_tfree_names (hyps,[]) 

780 
in Thm{sign=sign, maxidx=max[0,maxidx], hyps=hyps, 

250  781 
prop= Type.varify(prop,tfrees)} 
0  782 
end; 
783 

784 
(* Replace all TVars by new TFrees *) 

785 
fun freezeT(Thm{sign,maxidx,hyps,prop}) = 

786 
let val prop' = Type.freeze (K true) prop 

787 
in Thm{sign=sign, maxidx=maxidx_of_term prop', hyps=hyps, prop=prop'} end; 

788 

789 

790 
(*** Inference rules for tactics ***) 

791 

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

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

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

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

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

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

798 
end 

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

800 

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

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

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

250  806 
handle TERM _ => raise THM("lift_rule", i, [orule,state]); 
0  807 
val (lift_abs,lift_all) = Logic.lift_fns(Bi,smax+1); 
808 
val (Thm{sign,maxidx,hyps,prop}) = orule 

809 
val (tpairs,As,B) = Logic.strip_horn prop 

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

810 
in Thm{hyps=hyps, sign= merge_thm_sgs(state,orule), 
250  811 
maxidx= maxidx+smax+1, 
812 
prop= Logic.rule_of(map (pairself lift_abs) tpairs, 

813 
map lift_all As, lift_all B)} 

0  814 
end; 
815 

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

817 
fun assumption i state = 

818 
let val Thm{sign,maxidx,hyps,prop} = state; 

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

250  820 
fun newth (env as Envir.Envir{maxidx, ...}, tpairs) = 
821 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

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

823 
Logic.rule_of (tpairs, Bs, C) 

824 
else (*normalize the new rule fully*) 

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

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

828 
(Sequence.mapp newth 

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

0  831 
in addprfs (Logic.assum_pairs Bi) end; 
832 

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

836 
let val Thm{sign,maxidx,hyps,prop} = state; 

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

838 
in if exists (op aconv) (Logic.assum_pairs Bi) 

250  839 
then Thm{sign=sign, hyps=hyps, maxidx=maxidx, 
840 
prop=Logic.rule_of(tpairs, Bs, C)} 

0  841 
else raise THM("eq_assumption", 0, [state]) 
842 
end; 

843 

844 

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

846 

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

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

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

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

851 
fun rename_params_rule (cs, i) state = 

852 
let val Thm{sign,maxidx,hyps,prop} = state 

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

854 
val iparams = map #1 (Logic.strip_params Bi) 

855 
val short = length iparams  length cs 

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

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

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

250  861 
in 
0  862 
case findrep cs of 
863 
c::_ => error ("Bound variables not distinct: " ^ c) 

864 
 [] => (case cs inter freenames of 

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

866 
 [] => Thm{sign=sign, hyps=hyps, maxidx=maxidx, prop= 

250  867 
Logic.rule_of(tpairs, Bs@[newBi], C)}) 
0  868 
end; 
869 

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

871 

250  872 
(*Scan a pair of terms; while they are similar, 
0  873 
accumulate corresponding bound vars in "al"*) 
874 
fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al) 

875 
 match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) 

876 
 match_bvs(_,_,al) = al; 

877 

878 
(* strip abstractions created by parameters *) 

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

880 

881 

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

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

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

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

889 
 strip(A,_) = f A 

0  890 
in strip end; 
891 

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

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

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

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

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

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

899 
(*unknowns appearing elsewhere be preserved!*) 

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

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

902 
(case assoc(al,x) of 

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

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

905 
 None=> t) 

0  906 
 rename(Abs(x,T,t)) = 
250  907 
Abs(case assoc(al,x) of Some(y) => y  None => x, 
908 
T, rename t) 

0  909 
 rename(f$t) = rename f $ rename t 
910 
 rename(t) = t; 

250  911 
fun strip_ren Ai = strip_apply rename (Ai,B) 
0  912 
in strip_ren end; 
913 

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

915 
fun rename_bvars(dpairs, tpairs, B) = 

250  916 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  917 

918 

919 
(*** RESOLUTION ***) 

920 

921 
(*strip off pairs of assumptions/parameters in parallel  they are 

922 
identical because of lifting*) 

250  923 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
924 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

0  925 
 strip_assums2 (Const("all",_)$Abs(a,T,t1), 
250  926 
Const("all",_)$Abs(_,_,t2)) = 
0  927 
let val (B1,B2) = strip_assums2 (t1,t2) 
928 
in (Abs(a,T,B1), Abs(a,T,B2)) end 

929 
 strip_assums2 BB = BB; 

930 

931 

932 
(*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) 

250  933 
Unifies B with Bi, replacing subgoal i (1 <= i <= n) 
0  934 
If match then forbid instantiations in proof state 
935 
If lifted then shorten the dpair using strip_assums2. 

936 
If eres_flg then simultaneously proves A1 by assumption. 

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

940 
local open Sequence; exception Bicompose 

941 
in 

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

945 
and Thm{maxidx=rmax, hyps=rhyps, prop=rprop,...} = orule; 

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

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

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

951 
val normp = 

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

953 
else 

954 
let val ntps = map (pairself normt) tpairs 

955 
in if the (Envir.minidx env) > smax then (*no assignments in state*) 

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

957 
else if match then raise Bicompose 

958 
else (*normalize the new rule fully*) 

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

960 
end 

961 
val th = Thm{sign=sign, hyps=rhyps union shyps, maxidx=maxidx, 

962 
prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

989 
(*ordinary resolution*) 

990 
fun res(None) = null 

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

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

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

996 
end; 

997 
end; (*open Sequence*) 

998 

999 

1000 
fun bicompose match arg i state = 

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

1002 

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

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

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

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

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

1009 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1010 
end; 
1011 

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

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

250  1014 
fun biresolution match brules i state = 
0  1015 
let val lift = lift_rule(state, i); 
250  1016 
val (stpairs, Bs, Bi, C) = dest_state(state,i) 
1017 
val B = Logic.strip_assums_concl Bi; 

1018 
val Hs = Logic.strip_assums_hyp Bi; 

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

1020 
fun res [] = Sequence.null 

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

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

1023 
then Sequence.seqof (*delay processing remainder til needed*) 

1024 
(fn()=> Some(comp (eres_flg, lift rule, nprems_of rule), 

1025 
res brules)) 

1026 
else res brules 

0  1027 
in Sequence.flats (res brules) end; 
1028 

1029 

1030 

1031 
(*** Meta simp sets ***) 

1032 

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

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

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

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

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

1040 
net: discrimination net of rewrite rules 

1041 
congs: association list of congruence rules 

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

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

1043 
for generating new names when rewriting under lambda abstractions 
0  1044 
mk_rews: used when local assumptions are added 
1045 
*) 

1046 

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

1047 
val empty_mss = Mss{net= Net.empty, congs= [], bounds=[], prems= [], 
0  1048 
mk_rews = K[]}; 
1049 

1050 
exception SIMPLIFIER of string * thm; 

1051 

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

1052 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1053 

209  1054 
val trace_simp = ref false; 
1055 

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

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

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

1059 

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

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

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

1062 
 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

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

1064 

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

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

1066 
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

1067 

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

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

1070 
is_Var(lhs) orelse 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1071 
(null(prems) andalso 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1072 
Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs)); 
0  1073 

1074 
fun mk_rrule (thm as Thm{hyps,sign,prop,maxidx,...}) = 

1075 
let val prems = Logic.strip_imp_prems prop 

1076 
val concl = Pattern.eta_contract (Logic.strip_imp_concl prop) 

1077 
val (lhs,rhs) = Logic.dest_equals concl handle TERM _ => 

1078 
raise SIMPLIFIER("Rewrite rule not a metaequality",thm) 

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

1079 
val perm = var_perm(lhs,rhs) andalso not(lhs=rhs orelse is_Var(lhs)) 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1080 
in if not perm andalso loops sign prems (lhs,rhs) 
0  1081 
then (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

1082 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1083 
end; 
1084 

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

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

1088 
in 

1089 

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

1090 
fun add_simp(mss as Mss{net,congs,bounds,prems,mk_rews}, 
0  1091 
thm as Thm{sign,prop,...}) = 
87  1092 
case mk_rrule thm of 
1093 
None => mss 

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

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

1097 
handle Net.INSERT => 

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

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

1100 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}); 
87  1101 

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

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

1105 
None => mss 

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

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

1108 
handle Net.INSERT => 

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

1110 
net)), 

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

1111 
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews} 
87  1112 

1113 
end; 

0  1114 

1115 
val add_simps = foldl add_simp; 

87  1116 
val del_simps = foldl del_simp; 
0  1117 

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

1119 

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

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

1123 
val lhs = Pattern.eta_contract lhs 

1124 
val (a,_) = dest_Const (head_of lhs) handle TERM _ => 

1125 
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

1126 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, bounds=bounds, 
0  1127 
prems=prems, mk_rews=mk_rews} 
1128 
end; 

1129 

1130 
val (op add_congs) = foldl add_cong; 

1131 

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

1132 
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

1133 
Mss{net=net, congs=congs, bounds=bounds, prems=thms@prems, mk_rews=mk_rews}; 
0  1134 

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

1136 

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

1137 
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

1138 
Mss{net=net, congs=congs, bounds=bounds, prems=prems, mk_rews=mk_rews}; 
0  1139 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 
1140 

1141 

250  1142 
(*** Metalevel rewriting 
0  1143 
uses conversions, omitting proofs for efficiency. See 
250  1144 
L C Paulson, A higherorder implementation of rewriting, 
1145 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1146 

1147 
type prover = meta_simpset > thm > thm option; 

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

1149 
type conv = meta_simpset > termrec > termrec; 

1150 

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

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

1152 

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

1153 
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

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

1155 

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

1156 
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

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

1158 

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

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

1160 

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

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

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

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

1164 
 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

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

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

1167 

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

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

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

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

1171 
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

1172 
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

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

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

1175 

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

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

1177 
* Otherwise nonlinear *) 
305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

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

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

1180 
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

1181 
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

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

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

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

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

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

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

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

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

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

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

1192 

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

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

1194 

432  1195 
fun check_conv(thm as Thm{hyps,prop,sign,...}, prop0) = 
1196 
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; 

1197 
trace_term "Should have proved" sign prop0; 

1198 
None) 

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

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

1202 
if (lhs = lhs0) orelse 

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

1203 
(lhs aconv Envir.norm_term (Envir.empty 0) lhs0) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1204 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  1205 
else err() 
1206 
 _ => err() 

1207 
end; 

1208 

1209 
(*Conversion to apply the meta simpset to a term*) 

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

1210 
fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

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

1212 
fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = 
250  1213 
let val unit = if Sign.subsig(sign,signt) then () 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1214 
else (writeln"Warning: rewrite rule from different theory"; 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1215 
raise Pattern.MATCH) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1216 
val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t) 
0  1217 
val prop' = subst_vars insts prop; 
1218 
val hyps' = hyps union hypst; 

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

1219 
val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} 
427
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1220 
val (lhs',rhs') = Logic.dest_equals(Logic.strip_imp_concl prop') 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1221 
in if perm andalso not(termless(rhs',lhs')) then None else 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1222 
if Logic.count_prems(prop',0) = 0 
4ce2ce940faf
ordered rewriting applies to conditional rules as well now
nipkow
parents:
421
diff
changeset

1223 
then (trace_thm "Rewriting:" thm'; Some(hyps',rhs')) 
0  1224 
else (trace_thm "Trying to rewrite:" thm'; 
1225 
case prover mss thm' of 

1226 
None => (trace_thm "FAILED" thm'; None) 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1227 
 Some(thm2) => check_conv(thm2,prop')) 
0  1228 
end 
1229 

225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1230 
fun rews [] = None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1231 
 rews (rrule::rrules) = 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1232 
let val opt = rew rrule handle Pattern.MATCH => None 
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1233 
in case opt of None => rews rrules  some => some end; 
0  1234 

1235 
in case t of 

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

1236 
Abs(_,_,body) $ u => Some(hypst,subst_bounds([u], body)) 
225
76f60e6400e8
optimized net for matching of abstractions to speed up simplifier
nipkow
parents:
222
diff
changeset

1237 
 _ => rews(Net.match_term net t) 
0  1238 
end; 
1239 

1240 
(*Conversion to apply a congruence rule to a term*) 

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

1241 
fun congc (prover,signt) {thm=cong,lhs=lhs} (hypst,t) = 
0  1242 
let val Thm{sign,hyps,maxidx,prop,...} = cong 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1243 
val unit = if Sign.subsig(sign,signt) then () 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1244 
else error("Congruence rule from different theory") 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1245 
val tsig = #tsig(Sign.rep_sg signt) 
0  1246 
val insts = Pattern.match tsig (lhs,t) handle Pattern.MATCH => 
1247 
error("Congruence rule did not match") 

1248 
val prop' = subst_vars insts prop; 

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

1249 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  1250 
prop=prop', maxidx=maxidx} 
1251 
val unit = trace_thm "Applying congruence rule" thm'; 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1252 
fun err() = error("Failed congruence proof!") 
0  1253 

1254 
in case prover thm' of 

112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1255 
None => err() 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1256 
 Some(thm2) => (case check_conv(thm2,prop') of 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1257 
None => err()  some => some) 
0  1258 
end; 
1259 

1260 

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

1261 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1262 
fun bottomc ((simprem,useprem),prover,sign) = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1263 
let fun botc fail mss trec = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1264 
(case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1265 
some as Some(trec1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1266 
(case rewritec (prover,sign) mss trec1 of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1267 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1268 
 None => some) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1269 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1270 
(case rewritec (prover,sign) mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1271 
Some(trec2) => botc false mss trec2 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1272 
 None => if fail then None else Some(trec))) 
0  1273 

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

1274 
and try_botc mss trec = (case botc true mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1275 
Some(trec1) => trec1 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1276 
 None => trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1277 

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

1278 
and subc (mss as Mss{net,congs,bounds,prems,mk_rews}) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1279 
(trec as (hyps,t)) = 
0  1280 
(case t of 
1281 
Abs(a,T,t) => 

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

1282 
let val b = variant bounds a 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1283 
val v = Free("." ^ b,T) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1284 
val mss' = Mss{net=net, congs=congs, bounds=b::bounds, 
0  1285 
prems=prems,mk_rews=mk_rews} 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1286 
in case botc true mss' (hyps,subst_bounds([v],t)) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1287 
Some(hyps',t') => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1288 
Some(hyps', Abs(a, T, abstract_over(v,t'))) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1289 
 None => None 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1290 
end 
0  1291 
 t$u => (case t of 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1292 
Const("==>",_)$s => Some(impc(hyps,s,u,mss)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1293 
 Abs(_,_,body) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1294 
let val trec = (hyps,subst_bounds([u], body)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1295 
in case subc mss trec of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1296 
None => Some(trec) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1297 
 trec => trec 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

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

1299 
 _ => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1300 
let fun appc() = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1301 
(case botc true mss (hyps,t) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1302 
Some(hyps1,t1) => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1303 
(case botc true mss (hyps1,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1304 
Some(hyps2,u1) => Some(hyps2,t1$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1305 
 None => Some(hyps1,t1$u)) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1306 
 None => 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1307 
(case botc true mss (hyps,u) of 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1308 
Some(hyps1,u1) => Some(hyps1,t$u1) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1309 
 None => None)) 
0  1310 
val (h,ts) = strip_comb t 
1311 
in case h of 

1312 
Const(a,_) => 

1313 
(case assoc(congs,a) of 

1314 
None => appc() 

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

1315 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1316 
 _ => appc() 
1317 
end) 

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

1318 
 _ => None) 
0  1319 

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

1320 
and impc(hyps,s,u,mss as Mss{mk_rews,...}) = 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1321 
let val (hyps1,s1) = if simprem then try_botc mss (hyps,s) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1322 
else (hyps,s) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1323 
val mss1 = 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1324 
if not useprem orelse maxidx_of_term s1 <> ~1 then mss 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1325 
else let val thm = Thm{sign=sign,hyps=[s1],prop=s1,maxidx= ~1} 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1326 
in add_simps(add_prems(mss,[thm]), mk_rews thm) end 
405
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1327 
val (hyps2,u1) = try_botc mss1 (hyps1,u) 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1328 
val hyps3 = if s1 mem hyps1 then hyps2 else hyps2\s1 
c97514f63633
Internale optimization of the simplifier: in case a subterm stays unchanged,
nipkow
parents:
399
diff
changeset

1329 
in (hyps3, Logic.mk_implies(s1,u1)) end 
0  1330 

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

1331 
in try_botc end; 
0  1332 

1333 

1334 
(*** Metarewriting: rewrites t to u and returns the theorem t==u ***) 

1335 
(* Parameters: 

250  1336 
mode = (simplify A, use A in simplifying B) when simplifying A ==> B 
0  1337 
mss: contains equality theorems of the form [p1,...] ==> t==u 
1338 
prover: how to solve premises in conditional rewrites and congruences 

1339 
*) 

1340 

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

1341 
(*** FIXME: check that #bounds(mss) does not "occur" in ct alread ***) 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1342 
fun rewrite_cterm mode mss prover ct = 
229
4002c4cd450c
Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
lcp
parents:
225
diff
changeset

1343 
let val {sign, t, T, maxidx} = rep_cterm ct; 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1344 
val (hyps,u) = bottomc (mode,prover,sign) mss ([],t); 
0  1345 
val prop = Logic.mk_equals(t,u) 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1346 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1347 
end 
1348 

1349 
end; 

250  1350 