author  wenzelm 
Thu, 26 May 1994 16:43:24 +0200  
changeset 399  86cc2b98f9e0 
parent 387  69f4356d915d 
child 405  c97514f63633 
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 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

42 
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

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

44 
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

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

46 
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

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

48 
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

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

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

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

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

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

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

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

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

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

60 
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

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

64 
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

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

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

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

71 
val combination: thm > thm > thm 

72 
val concl_of: thm > term 

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

73 
val cprop_of: thm > cterm 
87  74 
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

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

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

81 
val extend_theory: theory > string 

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

84 
* (string * string list * string) list 

85 
* (string list * (sort list * class))list 

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

87 
> (string*string)list > theory 

88 
val extensional: thm > thm 

89 
val flexflex_rule: thm > thm Sequence.seq 

90 
val flexpair_def: thm 

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

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

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

95 
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

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

101 
val merge_theories: theory * theory > theory 

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

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

105 
val nprems_of: thm > int 

106 
val parents_of: theory > theory list 

107 
val prems_of: thm > term list 

108 
val prems_of_mss: meta_simpset > thm list 

109 
val pure_thy: theory 

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

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

111 
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

112 
string * typ > cterm * (indexname * typ) list 
250  113 
val reflexive: cterm > thm 
0  114 
val rename_params_rule: string list * int > thm > thm 
115 
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

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

117 
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

118 
> cterm > thm 
0  119 
val set_mk_rews: meta_simpset * (thm > thm list) > meta_simpset 
399
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

120 
val rep_theory: theory > {sign: Sign.sg, new_axioms: term Sign.Symtab.table, 
86cc2b98f9e0
added class_triv: theory > class > thm (for axclasses);
wenzelm
parents:
387
diff
changeset

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

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

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

127 
val stamps_of_thy: theory > string ref list 

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

131 
val transitive: thm > thm > thm 

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

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

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

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

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

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

143 
structure Sign = Unify.Sign; 

144 
structure Type = Sign.Type; 

145 
structure Syntax = Sign.Syntax; 

146 
structure Symtab = Sign.Symtab; 

147 

148 

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

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

150 

250  151 
(** certified types **) 
152 

153 
(*certified typs under a signature*) 

154 

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

156 

157 
fun rep_ctyp (Ctyp args) = args; 

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

159 

160 
fun ctyp_of sign T = 

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

162 

163 
fun read_ctyp sign s = 

164 
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

165 

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 

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

169 

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

171 

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

173 

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

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

176 

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

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

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

181 
end handle TYPE (msg, _, _) 

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

183 

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

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

186 

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

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

192 

250  193 

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

194 

250  195 
(** read cterms **) 
196 

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

198 

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

200 
let 

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

202 
val showtyp = Sign.string_of_typ sign; 

203 
val showterm = Sign.string_of_term sign; 

204 

205 
fun termerr [] = "" 

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

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

208 

209 
val T' = Sign.certify_typ sign T 

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

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

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

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

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

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

216 
in (ct, tye) end; 

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

217 

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

218 
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

219 

250  220 

221 

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

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

223 

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

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

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

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

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

232 

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

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

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

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

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

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

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

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

240 

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

243 
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

244 

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

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

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

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

249 
(*counts premises in a rule*) 

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

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

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

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

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

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

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

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

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

258 
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

259 

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

260 

0  261 

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

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

263 

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

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

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

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

268 
parents: theory list}; 
0  269 

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

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

271 

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

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

275 

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

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

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

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

280 
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

281 

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

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

283 
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

284 

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

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

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

287 

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

288 

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

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

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

291 
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

292 

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 
(*look up the named axiom in the theory*) 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

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

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

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

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

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

301 
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

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

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

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

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

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

307 

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

310 

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

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

312 
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

313 

0  314 

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

315 

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

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

317 

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

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

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

320 

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

321 
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

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

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

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

325 
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

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

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

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

329 
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

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

331 

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

334 

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

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

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

337 

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

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

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

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

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

342 
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

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

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

345 
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

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

347 
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

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

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

350 
val add_thyname = ext_sg Sign.add_name; 
0  351 

352 

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

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

354 

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

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

356 
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

357 

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

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

359 
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

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

361 

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

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

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

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

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

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

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

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

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

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

371 

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

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

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

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

375 

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

376 

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

377 
(* extend axioms of a theory *) 
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 
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

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

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

382 
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

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

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

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

386 

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

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

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

389 

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

390 

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

391 
(* extend theory (old) *) (* FIXME remove *) 
0  392 

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

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

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

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

396 

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

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

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

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

400 

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

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

402 
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

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

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

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

406 

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

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

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

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

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

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

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

413 

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

414 

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 
(** merge theories **) 
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 
fun merge_thy_list mk_draft thys = 
69f4356d915d
new datatype theory, supports 'draft theories' and incremental extension:
wenzelm
parents:
309
diff
changeset

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

420 
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

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

422 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

436 

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

437 
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

438 

0  439 

440 

441 
(**** Primitive rules ****) 

442 

443 
(* discharge all assumptions t from ts *) 

444 
val disch = gen_rem (op aconv); 

445 

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

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

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

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

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

456 

250  457 
(* Implication introduction 
458 
A  B 

459 
 

460 
A ==> B *) 

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

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

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

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

469 
end; 

470 

471 
(* Implication elimination 

250  472 
A ==> B A 
473 
 

474 
B *) 

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

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

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

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

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

485 
prop= B} 

486 
else err("major premise") 

487 
 _ => err("major premise") 

0  488 
end; 
250  489 

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

492 
 

493 
!!x.A *) 

494 
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

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

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

502 
else result(a,T) 

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

505 
end; 

506 

507 
(* Forall elimination 

250  508 
!!x.A 
509 
 

510 
A[t/x] *) 

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

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

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

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

518 
maxidx= max[maxidx, maxt], 

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

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

0  521 
end 
522 
handle TERM _ => 

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

525 

526 
(*** Equality ***) 

527 

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

529 
val flexpair_def = 

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

532 
(read_cterm Sign.pure 

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

0  534 

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

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

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

540 

541 
(*The symmetry rule 

542 
t==u 

543 
 

544 
u==t *) 

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

546 
case prop of 

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

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

551 
(*The transitive rule 

552 
t1==u u==t2 

553 
 

554 
t1==t2 *) 

555 
fun transitive th1 th2 = 

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

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

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

559 
in case (prop1,prop2) of 

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

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

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

566 

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

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

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

573 
maxidx= maxidx_of_term t, 

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

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

0  576 
end; 
577 

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

579 
f(x) == g(x) 

580 
 

581 
f == g *) 

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

583 
case prop of 

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

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

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

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

591 
 Var _ => 

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

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

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

595 
Thm{sign=sign, hyps=hyps, maxidx=maxidx, 

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

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

599 

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

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

602 
t == u 

603 
 

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

605 
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

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

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

0  610 
fun result T = 
611 
Thm{sign= sign, maxidx= maxidx, hyps= hyps, 

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

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

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

618 
else result T 

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

621 
end; 

622 

623 
(*The combination rule 

624 
f==g t==u 

625 
 

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

627 
fun combination th1 th2 = 

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

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

630 
in case (prop1,prop2) of 

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

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

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

636 

637 

638 
(*The equal propositions rule 

639 
A==B A 

640 
 

641 
B *) 

642 
fun equal_elim th1 th2 = 

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

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

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

646 
in case prop1 of 

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

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

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

653 

654 

655 
(* Equality introduction 

656 
A==>B B==>A 

657 
 

658 
A==B *) 

659 
fun equal_intr th1 th2 = 

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

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

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

663 
in case (prop1,prop2) of 

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

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

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

0  669 
 _ => err"premises" 
670 
end; 

671 

672 
(**** Derived rules ****) 

673 

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

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

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

677 
implies_intr_hyps 

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

0  680 
 implies_intr_hyps th = th; 
681 

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

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

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

250  687 
let fun newthm env = 
688 
let val (tpairs,horn) = 

689 
Logic.strip_flexpairs (Envir.norm_term env prop) 

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

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

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

693 
in Thm{sign= sign, hyps= hyps, 

694 
maxidx= maxidx_of_term newprop, prop= newprop} 

695 
end; 

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

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

701 
(*Instantiation of Vars 

250  702 
A 
703 
 

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

0  705 

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

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

708 

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

710 
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

711 
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

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

715 
end; 

716 

717 
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

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

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

722 
Instantiates distinct Vars by terms of same type. 

723 
Normalizes the new theorem! *) 

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

250  727 
val newprop = 
728 
Envir.norm_term (Envir.empty 0) 

729 
(subst_atomic tpairs 

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

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

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

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

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

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

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

741 
 [] => 

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

743 
ix::_ => raise THM 

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

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

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

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

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

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

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

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

760 

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

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

762 
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

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

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

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

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

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

768 
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

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

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

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

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

773 

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

774 

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

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

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

250  779 
prop= Type.varify(prop,tfrees)} 
0  780 
end; 
781 

782 
(* Replace all TVars by new TFrees *) 

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

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

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

786 

787 

788 
(*** Inference rules for tactics ***) 

789 

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

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

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

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

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

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

796 
end 

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

798 

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

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

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

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

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

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

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

811 
map lift_all As, lift_all B)} 

0  812 
end; 
813 

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

815 
fun assumption i state = 

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

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

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

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

821 
Logic.rule_of (tpairs, Bs, C) 

822 
else (*normalize the new rule fully*) 

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

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

826 
(Sequence.mapp newth 

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

0  829 
in addprfs (Logic.assum_pairs Bi) end; 
830 

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

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

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

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

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

0  839 
else raise THM("eq_assumption", 0, [state]) 
840 
end; 

841 

842 

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

844 

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

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

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

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

849 
fun rename_params_rule (cs, i) state = 

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

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

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

853 
val short = length iparams  length cs 

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

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

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

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

862 
 [] => (case cs inter freenames of 

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

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

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

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

869 

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

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

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

875 

876 
(* strip abstractions created by parameters *) 

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

878 

879 

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

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

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

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

887 
 strip(A,_) = f A 

0  888 
in strip end; 
889 

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

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

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

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

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

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

897 
(*unknowns appearing elsewhere be preserved!*) 

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

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

900 
(case assoc(al,x) of 

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

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

903 
 None=> t) 

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

0  907 
 rename(f$t) = rename f $ rename t 
908 
 rename(t) = t; 

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

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

913 
fun rename_bvars(dpairs, tpairs, B) = 

250  914 
rename_bvs(foldr match_bvars (dpairs,[]), dpairs, tpairs, B); 
0  915 

916 

917 
(*** RESOLUTION ***) 

918 

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

920 
identical because of lifting*) 

250  921 
fun strip_assums2 (Const("==>", _) $ _ $ B1, 
922 
Const("==>", _) $ _ $ B2) = strip_assums2 (B1,B2) 

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

927 
 strip_assums2 BB = BB; 

928 

929 

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

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

934 
If eres_flg then simultaneously proves A1 by assumption. 

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

938 
local open Sequence; exception Bicompose 

939 
in 

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

943 
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

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

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

949 
val normp = 

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

951 
else 

952 
let val ntps = map (pairself normt) tpairs 

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

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

955 
else if match then raise Bicompose 

956 
else (*normalize the new rule fully*) 

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

958 
end 

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

960 
prop= Logic.rule_of normp} 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

987 
(*ordinary resolution*) 

988 
fun res(None) = null 

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

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

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

994 
end; 

995 
end; (*open Sequence*) 

996 

997 

998 
fun bicompose match arg i state = 

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

1000 

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

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

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

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

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

1007 
(not eres_flg orelse could_reshyp (prems_of rule)) 

0  1008 
end; 
1009 

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

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

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

1016 
val Hs = Logic.strip_assums_hyp Bi; 

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

1018 
fun res [] = Sequence.null 

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

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

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

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

1023 
res brules)) 

1024 
else res brules 

0  1025 
in Sequence.flats (res brules) end; 
1026 

1027 

1028 

1029 
(*** Meta simp sets ***) 

1030 

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

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

1032 
type cong = {thm:thm, lhs:term}; 
0  1033 
datatype meta_simpset = 
288
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

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

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

1038 
net: discrimination net of rewrite rules 

1039 
congs: association list of congruence rules 

1040 
primes: offset for generating unique new names 

1041 
for rewriting under lambda abstractions 

1042 
mk_rews: used when local assumptions are added 

1043 
*) 

1044 

1045 
val empty_mss = Mss{net= Net.empty, congs= [], primes="", prems= [], 

1046 
mk_rews = K[]}; 

1047 

1048 
exception SIMPLIFIER of string * thm; 

1049 

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

1050 
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t)); 
0  1051 

209  1052 
val trace_simp = ref false; 
1053 

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

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

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

1057 

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

1058 
fun var_perm(Var _, Var _) = true 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1059 
 var_perm(Abs(_,_,s), Abs(_,_,t)) = var_perm(s,t) 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1060 
 var_perm(t1$t2, u1$u2) = var_perm(t1,u1) andalso var_perm(t2,u2) 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

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

1062 

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

1063 

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

1066 
null(prems) andalso 

1067 
Pattern.eta_matches (#tsig(Sign.rep_sg sign)) (lhs,rhs); 

1068 

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

1070 
let val prems = Logic.strip_imp_prems prop 

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

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

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

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

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

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

1077 
else Some{thm=thm,lhs=lhs,perm=perm} 
0  1078 
end; 
1079 

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

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

1083 
in 

1084 

0  1085 
fun add_simp(mss as Mss{net,congs,primes,prems,mk_rews}, 
1086 
thm as Thm{sign,prop,...}) = 

87  1087 
case mk_rrule thm of 
1088 
None => mss 

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

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

1092 
handle Net.INSERT => 

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

209  1095 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews}); 
87  1096 

1097 
fun del_simp(mss as Mss{net,congs,primes,prems,mk_rews}, 

1098 
thm as Thm{sign,prop,...}) = 

1099 
case mk_rrule thm of 

1100 
None => mss 

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

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

1103 
handle Net.INSERT => 

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

1105 
net)), 

0  1106 
congs=congs, primes=primes, prems=prems,mk_rews=mk_rews} 
87  1107 

1108 
end; 

0  1109 

1110 
val add_simps = foldl add_simp; 

87  1111 
val del_simps = foldl del_simp; 
0  1112 

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

1114 

1115 
fun add_cong(Mss{net,congs,primes,prems,mk_rews},thm) = 

1116 
let val (lhs,_) = Logic.dest_equals(concl_of thm) handle TERM _ => 

1117 
raise SIMPLIFIER("Congruence not a metaequality",thm) 

1118 
val lhs = Pattern.eta_contract lhs 

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

1120 
raise SIMPLIFIER("Congruence must start with a constant",thm) 

1121 
in Mss{net=net, congs=(a,{lhs=lhs,thm=thm})::congs, primes=primes, 

1122 
prems=prems, mk_rews=mk_rews} 

1123 
end; 

1124 

1125 
val (op add_congs) = foldl add_cong; 

1126 

1127 
fun add_prems(Mss{net,congs,primes,prems,mk_rews},thms) = 

1128 
Mss{net=net, congs=congs, primes=primes, prems=thms@prems, mk_rews=mk_rews}; 

1129 

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

1131 

1132 
fun set_mk_rews(Mss{net,congs,primes,prems,...},mk_rews) = 

1133 
Mss{net=net, congs=congs, primes=primes, prems=prems, mk_rews=mk_rews}; 

1134 
fun mk_rews_of_mss(Mss{mk_rews,...}) = mk_rews; 

1135 

1136 

250  1137 
(*** Metalevel rewriting 
0  1138 
uses conversions, omitting proofs for efficiency. See 
250  1139 
L C Paulson, A higherorder implementation of rewriting, 
1140 
Science of Computer Programming 3 (1983), pages 119149. ***) 

0  1141 

1142 
type prover = meta_simpset > thm > thm option; 

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

1144 
type conv = meta_simpset > termrec > termrec; 

1145 

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

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

1147 

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

1148 
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

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

1150 

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

1151 
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

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

1153 

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

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

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

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

1157 
 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

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

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

1160 

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

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

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

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

1164 
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

1165 
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

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

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

1168 

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

1169 
(* FIXME: should really take types into account as well. 
305
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

1170 
* Otherwise not linear *) 
4c2bbb5de471
Changed term ordering for permutative rewrites to be ACcompatible.
nipkow
parents:
288
diff
changeset

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

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

1173 
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

1174 
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

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

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

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

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

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

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

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

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

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

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

1185 

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

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

1187 

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

1188 
fun check_conv(thm as Thm{hyps,prop,...}, prop0) = 
112
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1189 
let fun err() = (trace_thm "Proved wrong thm (Check subgoaler?)" thm; None) 
0  1190 
val (lhs0,_) = Logic.dest_equals(Logic.strip_imp_concl prop0) 
1191 
in case prop of 

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

1193 
if (lhs = lhs0) orelse 

1194 
(lhs aconv (Envir.norm_term (Envir.empty 0) lhs0)) 

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

1195 
then (trace_thm "SUCCEEDED" thm; Some(hyps,rhs)) 
0  1196 
else err() 
1197 
 _ => err() 

1198 
end; 

1199 

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

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

1201 
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

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

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

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

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

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

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

1210 
val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} 
0  1211 
in if nprems_of thm' = 0 
1212 
then let val (_,rhs) = Logic.dest_equals prop' 

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

1213 
in if perm andalso not(termless(rhs,t)) then None 
b00ce6a1fe27
Implemented "ordered rewriting": rules which merely permute variables, such
nipkow
parents:
274
diff
changeset

1214 
else (trace_thm "Rewriting:" thm'; Some(hyps',rhs)) end 
0  1215 
else (trace_thm "Trying to rewrite:" thm'; 
1216 
case prover mss thm' of 

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

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

1218 
 Some(thm2) => check_conv(thm2,prop')) 
0  1219 
end 
1220 

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

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

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

1223 
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

1224 
in case opt of None => rews rrules  some => some end; 
0  1225 

1226 
in case t of 

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

1227 
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

1228 
 _ => rews(Net.match_term net t) 
0  1229 
end; 
1230 

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

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

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

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

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

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

1239 
val prop' = subst_vars insts prop; 

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

1240 
val thm' = Thm{sign=signt, hyps=hyps union hypst, 
0  1241 
prop=prop', maxidx=maxidx} 
1242 
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

1243 
fun err() = error("Failed congruence proof!") 
0  1244 

1245 
in case prover thm' of 

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

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

1247 
 Some(thm2) => (case check_conv(thm2,prop') of 
009ae5c85ae9
Changed the simplifier: if the subgoaler proves an unexpected thm, chances
nipkow
parents:
87
diff
changeset

1248 
None => err()  Some(x) => x) 
0  1249 
end; 
1250 

1251 

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

1252 
fun bottomc ((simprem,useprem),prover,sign) = 
0  1253 
let fun botc mss trec = let val trec1 = subc mss trec 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1254 
in case rewritec (prover,sign) mss trec1 of 
0  1255 
None => trec1 
1256 
 Some(trec2) => botc mss trec2 

1257 
end 

1258 

1259 
and subc (mss as Mss{net,congs,primes,prems,mk_rews}) 

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

1260 
(trec as (hyps,t)) = 
0  1261 
(case t of 
1262 
Abs(a,T,t) => 

1263 
let val v = Free(".subc." ^ primes,T) 

1264 
val mss' = Mss{net=net, congs=congs, primes=primes^"'", 

1265 
prems=prems,mk_rews=mk_rews} 

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

1266 
val (hyps',t') = botc mss' (hyps,subst_bounds([v],t)) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1267 
in (hyps', Abs(a, T, abstract_over(v,t'))) end 
0  1268 
 t$u => (case t of 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1269 
Const("==>",_)$s => impc(hyps,s,u,mss) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1270 
 Abs(_,_,body) => subc mss (hyps,subst_bounds([u], body)) 
0  1271 
 _ => 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1272 
let fun appc() = let val (hyps1,t1) = botc mss (hyps,t) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1273 
val (hyps2,u1) = botc mss (hyps1,u) 
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1274 
in (hyps2,t1$u1) end 
0  1275 
val (h,ts) = strip_comb t 
1276 
in case h of 

1277 
Const(a,_) => 

1278 
(case assoc(congs,a) of 

1279 
None => appc() 

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

1280 
 Some(cong) => congc (prover mss,sign) cong trec) 
0  1281 
 _ => appc() 
1282 
end) 

1283 
 _ => trec) 

1284 

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

1285 
and impc(hyps,s,u,mss as Mss{mk_rews,...}) = 
214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1286 
let val (hyps1,s') = if simprem then botc mss (hyps,s) else (hyps,s) 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1287 
val mss' = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
209
diff
changeset

1288 
if not useprem orelse maxidx_of_term s' <> ~1 then mss 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

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

1290 
in add_simps(add_prems(mss,[thm]), mk_rews thm) end 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1291 
val (hyps2,u') = botc mss' (hyps1,u) 
134
595fda4879b6
Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
nipkow
parents:
112
diff
changeset

1292 
val hyps2' = if s' mem hyps1 then hyps2 else hyps2\s' 
208
342f88d2e8ab
optimized simplifier  signature of rewritten term stays constant
nipkow
parents:
200
diff
changeset

1293 
in (hyps2', Logic.mk_implies(s',u')) end 
0  1294 

1295 
in botc end; 

1296 

1297 

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

1299 
(* Parameters: 

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

1303 
*) 

1304 

1305 
(*** FIXME: check that #primes(mss) does not "occur" in ct alread ***) 

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

1306 
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

1307 
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

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

1310 
in Thm{sign= sign, hyps= hyps, maxidx= maxidx_of_term prop, prop= prop} 
0  1311 
end 
1312 

1313 
end; 

250  1314 