# HG changeset patch # User wenzelm # Date 968353077 -7200 # Node ID 1ea354905d888a2e60489c08fd9e7acdab35a578 # Parent 09a142decdda57348c87774bef4100717e2a1441 improved att names / msgs; diff -r 09a142decdda -r 1ea354905d88 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Sep 07 20:57:22 2000 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Sep 07 20:57:57 2000 +0200 @@ -165,8 +165,8 @@ (* tags *) -fun gen_tag x = syntax (tag >> Drule.tag) x; -fun gen_untag x = syntax (Scan.lift Args.name >> Drule.untag) x; +fun gen_tagged x = syntax (tag >> Drule.tag) x; +fun gen_untagged x = syntax (Scan.lift Args.name >> Drule.untag) x; (* COMP *) @@ -174,8 +174,8 @@ fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B)); fun gen_COMP thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> comp); -val global_COMP = gen_COMP global_thm; -val local_COMP = gen_COMP local_thm; +val COMP_global = gen_COMP global_thm; +val COMP_local = gen_COMP local_thm; (* RS *) @@ -183,16 +183,16 @@ fun resolve (i, B) (x, A) = (x, A RSN (i, B)); fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve); -val global_RS = gen_RS global_thm; -val local_RS = gen_RS local_thm; +val RS_global = gen_RS global_thm; +val RS_local = gen_RS local_thm; -(* APP *) +(* OF *) fun apply Bs (x, A) = (x, Bs MRS A); -val global_APP = syntax (global_thmss >> apply); -val local_APP = syntax (local_thmss >> apply); +val OF_global = syntax (global_thmss >> apply); +val OF_local = syntax (local_thmss >> apply); (* where: named instantiations *) @@ -222,11 +222,11 @@ fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of)); -val global_where = gen_where ProofContext.init; -val local_where = gen_where I; +val where_global = gen_where ProofContext.init; +val where_local = gen_where I; -(* with: positional instantiations *) +(* of: positional instantiations *) fun read_instantiate' context_of (args, concl_args) x thm = let @@ -244,20 +244,20 @@ val inst_args = Scan.repeat inst_arg; fun insts' x = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x; -fun gen_with context_of = syntax (insts' >> (Drule.rule_attribute o read_instantiate' context_of)); +fun gen_of context_of = syntax (insts' >> (Drule.rule_attribute o read_instantiate' context_of)); -val global_with = gen_with ProofContext.init; -val local_with = gen_with I; +val of_global = gen_of ProofContext.init; +val of_local = gen_of I; (* unfold / fold definitions *) fun gen_rewrite rew defs (x, thm) = (x, rew defs thm); -val global_unfold = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule); -val local_unfold = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule); -val global_fold = syntax (global_thmss >> gen_rewrite Tactic.fold_rule); -val local_fold = syntax (local_thmss >> gen_rewrite Tactic.fold_rule); +val unfolded_global = syntax (global_thmss >> gen_rewrite Tactic.rewrite_rule); +val unfolded_local = syntax (local_thmss >> gen_rewrite Tactic.rewrite_rule); +val folded_global = syntax (global_thmss >> gen_rewrite Tactic.fold_rule); +val folded_local = syntax (local_thmss >> gen_rewrite Tactic.fold_rule); (* rule cases *) @@ -269,11 +269,11 @@ (* misc rules *) fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x; -fun elimify x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x; +fun elimified x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x; fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x; -fun global_export x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x; -fun local_export x = no_args (Drule.rule_attribute Proof.export_thm) x; +fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x; +fun exported_local x = no_args (Drule.rule_attribute Proof.export_thm) x; @@ -282,30 +282,28 @@ (* pure_attributes *) val pure_attributes = - [("tag", (gen_tag, gen_tag), "tag theorem"), - ("untag", (gen_untag, gen_untag), "untag theorem"), - ("COMP", (global_COMP, local_COMP), "compose rules (no lifting)"), - ("THEN", (global_RS, local_RS), "resolve with rule"), - ("OF", (global_APP, local_APP), "resolve with rule -- apply rule to rules"), - ("where", (global_where, local_where), "named instantiation of theorem"), - ("of", (global_with, local_with), "positional instantiation of theorem -- apply rule to terms"), - ("unfold", (global_unfold, local_unfold), "unfold definitions"), - ("fold", (global_fold, local_fold), "fold definitions"), - ("standard", (standard, standard), "put theorem into standard form"), - ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"), - ("no_vars", (no_vars, no_vars), "freeze schematic vars"), - ("case_names", (case_names, case_names), "name rule cases"), - ("params", (params, params), "name rule parameters"), - ("export", (global_export, local_export), "export theorem from context")]; + [("tagged", (gen_tagged, gen_tagged), "tagged theorem"), + ("untagged", (gen_untagged, gen_untagged), "untagged theorem"), + ("COMP", (COMP_global, COMP_local), "direct composition with rules (no lifting)"), + ("THEN", (RS_global, RS_local), "resolution with rule"), + ("OF", (OF_global, OF_local), "rule applied to facts"), + ("where", (where_global, where_local), "named instantiation of theorem"), + ("of", (of_global, of_local), "rule applied to terms"), + ("unfolded", (unfolded_global, unfolded_local), "unfolded definitions"), + ("folded", (folded_global, folded_local), "folded definitions"), + ("standard", (standard, standard), "result put into standard form"), + ("elimified", (elimified, elimified), "destruct rule turned into elimination rule"), + ("no_vars", (no_vars, no_vars), "frozen schematic vars"), + ("case_names", (case_names, case_names), "named rule cases"), + ("params", (params, params), "named rule parameters"), + ("exported", (exported_global, exported_local), "theorem exported from context")]; (* setup *) val setup = [AttributesData.init, add_attributes pure_attributes]; - end; - structure BasicAttrib: BASIC_ATTRIB = Attrib; open BasicAttrib;