author  berghofe 
Mon, 24 Jan 2005 17:56:18 +0100  
changeset 15456  956d6acacf89 
parent 15117  b860e444c1db 
child 15531  08c8dad8e399 
permissions  rwrr 
5823  1 
(* Title: Pure/Isar/attrib.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Symbolic theorem attributes. 

6 
*) 

7 

8 
signature BASIC_ATTRIB = 

9 
sig 

10 
val print_attributes: theory > unit 

5879  11 
val Attribute: bstring > (Args.src > theory attribute) * (Args.src > Proof.context attribute) 
12 
> string > unit 

5823  13 
end; 
14 

15 
signature ATTRIB = 

16 
sig 

17 
include BASIC_ATTRIB 

5912  18 
exception ATTRIB_FAIL of (string * Position.T) * exn 
5823  19 
val global_attribute: theory > Args.src > theory attribute 
20 
val local_attribute: theory > Args.src > Proof.context attribute 

5912  21 
val local_attribute': Proof.context > Args.src > Proof.context attribute 
7673
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

22 
val undef_global_attribute: theory attribute 
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

23 
val undef_local_attribute: Proof.context attribute 
5823  24 
val add_attributes: (bstring * ((Args.src > theory attribute) * 
25 
(Args.src > Proof.context attribute)) * string) list > theory > theory 

6091  26 
val global_thm: theory * Args.T list > thm * (theory * Args.T list) 
27 
val global_thms: theory * Args.T list > thm list * (theory * Args.T list) 

28 
val global_thmss: theory * Args.T list > thm list * (theory * Args.T list) 

29 
val local_thm: Proof.context * Args.T list > thm * (Proof.context * Args.T list) 

30 
val local_thms: Proof.context * Args.T list > thm list * (Proof.context * Args.T list) 

31 
val local_thmss: Proof.context * Args.T list > thm list * (Proof.context * Args.T list) 

5879  32 
val syntax: ('a * Args.T list > 'a attribute * ('a * Args.T list)) > Args.src > 'a attribute 
5823  33 
val no_args: 'a attribute > Args.src > 'a attribute 
8633  34 
val add_del_args: 'a attribute > 'a attribute > Args.src > 'a attribute 
5823  35 
val setup: (theory > theory) list 
36 
end; 

37 

38 
structure Attrib: ATTRIB = 

39 
struct 

40 

41 

42 
(** attributes theory data **) 

43 

44 
(* data kind 'Isar/attributes' *) 

45 

46 
structure AttributesDataArgs = 

47 
struct 

48 
val name = "Isar/attributes"; 

49 
type T = 

50 
{space: NameSpace.T, 

51 
attrs: 

52 
((((Args.src > theory attribute) * (Args.src > Proof.context attribute)) 

53 
* string) * stamp) Symtab.table}; 

54 

55 
val empty = {space = NameSpace.empty, attrs = Symtab.empty}; 

6546  56 
val copy = I; 
5823  57 
val prep_ext = I; 
58 

59 
fun merge ({space = space1, attrs = attrs1}, {space = space2, attrs = attrs2}) = 

60 
{space = NameSpace.merge (space1, space2), 

61 
attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups => 

62 
error ("Attempt to merge different versions of attributes " ^ commas_quote dups)}; 

63 

9216  64 
fun print _ {space, attrs} = 
5823  65 
let 
66 
fun prt_attr (name, ((_, comment), _)) = Pretty.block 

6846  67 
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment]; 
5823  68 
in 
8720  69 
[Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))] 
9216  70 
> Pretty.chunks > Pretty.writeln 
5823  71 
end; 
72 
end; 

73 

74 
structure AttributesData = TheoryDataFun(AttributesDataArgs); 

75 
val print_attributes = AttributesData.print; 

7611  76 

5823  77 

78 
(* get global / local attributes *) 

79 

5912  80 
exception ATTRIB_FAIL of (string * Position.T) * exn; 
81 

5823  82 
fun gen_attribute which thy = 
83 
let 

84 
val {space, attrs} = AttributesData.get thy; 

85 

5879  86 
fun attr src = 
87 
let 

88 
val ((raw_name, _), pos) = Args.dest_src src; 

89 
val name = NameSpace.intern space raw_name; 

90 
in 

5823  91 
(case Symtab.lookup (attrs, name) of 
92 
None => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) 

5912  93 
 Some ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src)) 
5823  94 
end; 
95 
in attr end; 

96 

97 
val global_attribute = gen_attribute fst; 

98 
val local_attribute = gen_attribute snd; 

5879  99 
val local_attribute' = local_attribute o ProofContext.theory_of; 
5823  100 

7673
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

101 
val undef_global_attribute: theory attribute = 
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

102 
fn _ => error "attribute undefined in theory context"; 
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

103 

b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

104 
val undef_local_attribute: Proof.context attribute = 
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

105 
fn _ => error "attribute undefined in proof context"; 
b8e7fa177d62
added undef_global_attribute, undef_local_attribute;
wenzelm
parents:
7668
diff
changeset

106 

5823  107 

108 
(* add_attributes *) 

109 

110 
fun add_attributes raw_attrs thy = 

111 
let 

112 
val full = Sign.full_name (Theory.sign_of thy); 

113 
val new_attrs = 

114 
map (fn (name, (f, g), comment) => (full name, (((f, g), comment), stamp ()))) raw_attrs; 

115 

116 
val {space, attrs} = AttributesData.get thy; 

117 
val space' = NameSpace.extend (space, map fst new_attrs); 

118 
val attrs' = Symtab.extend (attrs, new_attrs) handle Symtab.DUPS dups => 

119 
error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); 

120 
in thy > AttributesData.put {space = space', attrs = attrs'} end; 

121 

5879  122 
(*implicit version*) 
123 
fun Attribute name att cmt = Context.>> (add_attributes [(name, att, cmt)]); 

5823  124 

5879  125 

126 

127 
(** attribute parsers **) 

128 

129 
(* tags *) 

5823  130 

5879  131 
fun tag x = Scan.lift (Args.name  Scan.repeat Args.name) x; 
132 

133 

134 
(* theorems *) 

135 

15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset

136 
val thm_sel = Args.parens (Scan.pass () (Args.enum1 "," (Scan.lift 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset

137 
( Args.nat  Args.$$$ ""  Args.nat >> op upto 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset

138 
 Args.nat >> single)) >> flat)); 
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset

139 

5879  140 
fun gen_thm get attrib app = 
15456
956d6acacf89
Specific theorems in a named list of theorems can now be referred to
berghofe
parents:
15117
diff
changeset

141 
Scan.depend (fn st => Args.name  Scan.option thm_sel  Args.opt_attribs >> 
5879  142 
(fn (name, srcs) => app ((st, get st name), map (attrib st) srcs))); 
5823  143 

6091  144 
val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes; 
145 
val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes; 

5879  146 
val global_thmss = Scan.repeat global_thms >> flat; 
147 

6091  148 
val local_thm = gen_thm ProofContext.get_thm local_attribute' Thm.apply_attributes; 
149 
val local_thms = gen_thm ProofContext.get_thms local_attribute' Thm.applys_attributes; 

5879  150 
val local_thmss = Scan.repeat local_thms >> flat; 
151 

5823  152 

5879  153 

154 
(** attribute syntax **) 

5823  155 

5879  156 
fun syntax scan src (st, th) = 
8282  157 
let val (st', f) = Args.syntax "attribute" scan src st 
5879  158 
in f (st', th) end; 
159 

160 
fun no_args x = syntax (Scan.succeed x); 

5823  161 

10034  162 
fun add_del_args add del x = syntax 
163 
(Scan.lift (Args.add >> K add  Args.del >> K del  Scan.succeed add)) x; 

8633  164 

5823  165 

166 

167 
(** Pure attributes **) 

168 

169 
(* tags *) 

170 

9902  171 
fun gen_tagged x = syntax (tag >> Drule.tag) x; 
172 
fun gen_untagged x = syntax (Scan.lift Args.name >> Drule.untag) x; 

5823  173 

174 

6772  175 
(* COMP *) 
176 

6948  177 
fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B)); 
6772  178 

10151  179 
fun gen_COMP thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1)  thm >> comp); 
9902  180 
val COMP_global = gen_COMP global_thm; 
181 
val COMP_local = gen_COMP local_thm; 

6772  182 

183 

15117  184 
(* THEN, which corresponds to RS *) 
5879  185 

6091  186 
fun resolve (i, B) (x, A) = (x, A RSN (i, B)); 
5879  187 

15117  188 
fun gen_THEN thm = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1)  thm >> resolve); 
189 
val THEN_global = gen_THEN global_thm; 

190 
val THEN_local = gen_THEN local_thm; 

5879  191 

192 

9902  193 
(* OF *) 
5879  194 

6091  195 
fun apply Bs (x, A) = (x, Bs MRS A); 
5879  196 

9902  197 
val OF_global = syntax (global_thmss >> apply); 
198 
val OF_local = syntax (local_thmss >> apply); 

5879  199 

200 

14718  201 
(* where *) 
202 

203 
(*named instantiations; permits instantiation of type and term variables*) 

5879  204 

10807  205 
fun read_instantiate _ [] _ thm = thm 
206 
 read_instantiate context_of insts x thm = 

207 
let 

208 
val ctxt = context_of x; 

209 
val sign = ProofContext.sign_of ctxt; 

210 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

211 
(* Separate type and term insts, 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

212 
type insts must occur strictly before term insts *) 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

213 
fun has_type_var ((x, _), _) = (case Symbol.explode x of 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

214 
"'"::cs => true  cs => false); 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

215 
val (Tinst, tinsts) = take_prefix has_type_var insts; 
14718  216 
val _ = if exists has_type_var tinsts 
14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

217 
then error 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

218 
"Type instantiations must occur before term instantiations." 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

219 
else (); 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

220 

f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

221 
val Tinsts = filter has_type_var insts; 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

222 
val tinsts = filter_out has_type_var insts; 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

223 

f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

224 
(* Type instantiations first *) 
14718  225 
(* Process type insts: Tinsts_env *) 
226 
fun absent xi = error 

227 
("No such type variable in theorem: " ^ 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

228 
Syntax.string_of_vname xi); 
14718  229 
val (rtypes, rsorts) = types_sorts thm; 
230 
fun readT (xi, s) = 

231 
let val S = case rsorts xi of Some S => S  None => absent xi; 

232 
val T = ProofContext.read_typ ctxt s; 

233 
in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T) 

234 
else error 

235 
("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") 

236 
end; 

237 
val Tinsts_env = map readT Tinsts; 

238 
val cenvT = map (apsnd (Thm.ctyp_of sign)) (Tinsts_env); 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

239 
val thm' = Thm.instantiate (cenvT, []) thm; 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

240 
(* Instantiate, but don't normalise: *) 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

241 
(* this happens after term insts anyway. *) 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

242 

f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

243 
(* Term instantiations *) 
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

244 
val vars = Drule.vars_of thm'; 
10807  245 
fun get_typ xi = 
246 
(case assoc (vars, xi) of 

247 
Some T => T 

248 
 None => error ("No such variable in theorem: " ^ Syntax.string_of_vname xi)); 

5879  249 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

250 
val (xs, ss) = Library.split_list tinsts; 
10807  251 
val Ts = map get_typ xs; 
5879  252 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

253 
val used = add_term_tvarnames (prop_of thm',[]) 
14718  254 
(* Names of TVars occuring in thm'. read_def_termTs ensures 
14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14082
diff
changeset

255 
that new TVars introduced when reading the instantiation string 
14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

256 
are distinct from those occuring in the theorem. *) 
14257
a7ef3f7588c5
Type inference bug in Isar attributes "where" and "of" fixed.
ballarin
parents:
14082
diff
changeset

257 

14718  258 
val (ts, envT) = 
259 
ProofContext.read_termTs ctxt (K false) (K None) (K None) used (ss ~~ Ts); 

260 

10807  261 
val cenvT = map (apsnd (Thm.ctyp_of sign)) envT; 
262 
val cenv = 

263 
map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) 

264 
(gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts)); 

265 
in 

14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

266 
thm' 
10807  267 
> Drule.instantiate (cenvT, cenv) 
268 
> RuleCases.save thm 

269 
end; 

5879  270 

6448  271 
fun insts x = Args.and_list (Scan.lift (Args.var  Args.$$$ "="  Args.name)) x; 
5879  272 

6091  273 
fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of)); 
5823  274 

9902  275 
val where_global = gen_where ProofContext.init; 
276 
val where_local = gen_where I; 

5879  277 

278 

9902  279 
(* of: positional instantiations *) 
14287
f630017ed01c
Isar: where attribute supports instantiation of type variables.
ballarin
parents:
14257
diff
changeset

280 
(* permits instantiation of term variables only *) 
5912  281 

10807  282 
fun read_instantiate' _ ([], []) _ thm = thm 
283 
 read_instantiate' context_of (args, concl_args) x thm = 

284 
let 

285 
fun zip_vars _ [] = [] 

286 
 zip_vars (_ :: xs) (None :: opt_ts) = zip_vars xs opt_ts 

287 
 zip_vars ((x, _) :: xs) (Some t :: opt_ts) = (x, t) :: zip_vars xs opt_ts 

288 
 zip_vars [] _ = error "More instantiations than variables in theorem"; 

289 
val insts = 

12804  290 
zip_vars (Drule.vars_of_terms [Thm.prop_of thm]) args @ 
10807  291 
zip_vars (Drule.vars_of_terms [Thm.concl_of thm]) concl_args; 
292 
in 

293 
thm 

294 
> read_instantiate context_of insts x 

295 
> RuleCases.save thm 

296 
end; 

5912  297 

10807  298 
val concl = Args.$$$ "concl"  Args.colon; 
8687  299 
val inst_arg = Scan.unless concl Args.name_dummy; 
5912  300 
val inst_args = Scan.repeat inst_arg; 
10807  301 
fun insts' x = (inst_args  Scan.optional (concl  Args.!!! inst_args) []) x; 
5912  302 

10807  303 
fun gen_of context_of = 
304 
syntax (Scan.lift insts' >> (Drule.rule_attribute o read_instantiate' context_of)); 

5912  305 

9902  306 
val of_global = gen_of ProofContext.init; 
307 
val of_local = gen_of I; 

5912  308 

309 

13782
44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

310 
(* rename_abs *) 
44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

311 

44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

312 
fun rename_abs src = syntax 
14082
c69d5bf3047d
Moved function for renaming bound variables to Pure/drule.ML
berghofe
parents:
13782
diff
changeset

313 
(Scan.lift (Scan.repeat Args.name_dummy >> (apsnd o Drule.rename_bvars'))) src; 
13782
44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

314 

44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

315 

7598  316 
(* unfold / fold definitions *) 
317 

318 
fun gen_rewrite rew defs (x, thm) = (x, rew defs thm); 

319 

9902  320 
val unfolded_global = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule); 
321 
val unfolded_local = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule); 

322 
val folded_global = syntax (global_thmss >> gen_rewrite Tactic.fold_rule); 

323 
val folded_local = syntax (local_thmss >> gen_rewrite Tactic.fold_rule); 

7598  324 

325 

8368  326 
(* rule cases *) 
327 

10528  328 
fun consumes x = syntax (Scan.lift (Scan.optional Args.nat 1) >> RuleCases.consumes) x; 
8368  329 
fun case_names x = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names) x; 
330 
fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x; 

331 

332 

11770  333 
(* rule_format *) 
334 

335 
fun rule_format_att x = syntax 

336 
(Scan.lift (Args.parens (Args.$$$ "no_asm") 

337 
>> K ObjectLogic.rule_format_no_asm  Scan.succeed ObjectLogic.rule_format)) x; 

338 

339 

5879  340 
(* misc rules *) 
341 

6091  342 
fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x; 
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9902
diff
changeset

343 
fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x; 
9216  344 
fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x; 
5879  345 

346 

13370  347 
(* rule declarations *) 
348 

349 
local 

350 

351 
fun add_args a b c x = syntax 

352 
(Scan.lift ((Args.bang >> K a  Args.query >> K c  Scan.succeed b)  (Scan.option Args.nat)) 

353 
>> (fn (f, n) => f n)) x; 

354 

355 
fun del_args att = syntax (Scan.lift Args.del >> K att); 

356 

357 
open ContextRules; 

358 

359 
in 

360 

361 
val rule_atts = 

362 
[("intro", 

363 
(add_args intro_bang_global intro_global intro_query_global, 

364 
add_args intro_bang_local intro_local intro_query_local), 

365 
"declaration of introduction rule"), 

366 
("elim", 

367 
(add_args elim_bang_global elim_global elim_query_global, 

368 
add_args elim_bang_local elim_local elim_query_local), 

369 
"declaration of elimination rule"), 

370 
("dest", 

371 
(add_args dest_bang_global dest_global dest_query_global, 

372 
add_args dest_bang_local dest_local dest_query_local), 

373 
"declaration of destruction rule"), 

374 
("rule", (del_args rule_del_global, del_args rule_del_local), 

375 
"remove declaration of intro/elim/dest rule")]; 

376 

377 
end; 

378 

379 

11770  380 

5879  381 
(** theory setup **) 
5823  382 

383 
(* pure_attributes *) 

384 

385 
val pure_attributes = 

9902  386 
[("tagged", (gen_tagged, gen_tagged), "tagged theorem"), 
387 
("untagged", (gen_untagged, gen_untagged), "untagged theorem"), 

388 
("COMP", (COMP_global, COMP_local), "direct composition with rules (no lifting)"), 

15117  389 
("THEN", (THEN_global, THEN_local), "resolution with rule"), 
9902  390 
("OF", (OF_global, OF_local), "rule applied to facts"), 
391 
("where", (where_global, where_local), "named instantiation of theorem"), 

392 
("of", (of_global, of_local), "rule applied to terms"), 

13782
44de406a7273
Added rename_abs attribute for renaming bound variables.
berghofe
parents:
13414
diff
changeset

393 
("rename_abs", (rename_abs, rename_abs), "rename bound variables in abstractions"), 
9902  394 
("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"), 
395 
("folded", (folded_global, folded_local), "folded definitions"), 

396 
("standard", (standard, standard), "result put into standard form"), 

9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9902
diff
changeset

397 
("elim_format", (elim_format, elim_format), "destruct rule turned into elimination rule format"), 
9902  398 
("no_vars", (no_vars, no_vars), "frozen schematic vars"), 
10528  399 
("consumes", (consumes, consumes), "number of consumed facts"), 
9902  400 
("case_names", (case_names, case_names), "named rule cases"), 
401 
("params", (params, params), "named rule parameters"), 

11770  402 
("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute), 
403 
"declaration of atomize rule"), 

404 
("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute), 

405 
"declaration of rulify rule"), 

13370  406 
("rule_format", (rule_format_att, rule_format_att), "result put into standard rule format")] @ 
407 
rule_atts; 

5823  408 

409 

5879  410 
(* setup *) 
5823  411 

412 
val setup = [AttributesData.init, add_attributes pure_attributes]; 

413 

414 
end; 

415 

416 
structure BasicAttrib: BASIC_ATTRIB = Attrib; 

417 
open BasicAttrib; 