modernized attribute setup;
authorwenzelm
Sat May 30 15:25:46 2009 +0200 (2009-05-30)
changeset 31305a16f4d4f5b24
parent 31304 00a9c674cf40
child 31306 a74ee84288a0
modernized attribute setup;
removed obsolete no_args, add_del_args;
src/Pure/Isar/attrib.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat May 30 15:00:23 2009 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat May 30 15:25:46 2009 +0200
     1.3 @@ -31,9 +31,7 @@
     1.4    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     1.5    val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     1.6      theory -> theory
     1.7 -  val no_args: attribute -> src -> attribute
     1.8    val add_del: attribute -> attribute -> attribute context_parser
     1.9 -  val add_del_args: attribute -> attribute -> src -> attribute
    1.10    val thm_sel: Facts.interval list parser
    1.11    val thm: thm context_parser
    1.12    val thms: thm list context_parser
    1.13 @@ -175,12 +173,9 @@
    1.14      ("(" ^ ML_Syntax.make_binding name ^ ", " ^ txt ^ ", " ^ ML_Syntax.print_string cmt ^ ")"));
    1.15  
    1.16  
    1.17 -(* basic syntax *)
    1.18 +(* add/del syntax *)
    1.19  
    1.20 -fun no_args x = syntax (Scan.succeed x);
    1.21 -
    1.22 -fun add_del add del = (Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add));
    1.23 -fun add_del_args add del = syntax (add_del add del);
    1.24 +fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
    1.25  
    1.26  
    1.27  
    1.28 @@ -237,113 +232,99 @@
    1.29  
    1.30  fun internal att = Args.src (("Pure.attribute", [T.mk_attribute att]), Position.none);
    1.31  
    1.32 -val internal_att =
    1.33 -  syntax (Scan.lift Args.internal_attribute >> Morphism.form);
    1.34 -
    1.35 -
    1.36 -(* tags *)
    1.37 -
    1.38 -val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
    1.39 -val untagged = syntax (Scan.lift Args.name >> Thm.untag);
    1.40 -
    1.41 -val kind = syntax (Scan.lift Args.name >> Thm.kind);
    1.42 -
    1.43  
    1.44  (* rule composition *)
    1.45  
    1.46  val COMP_att =
    1.47 -  syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.48 -    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B))));
    1.49 +  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.50 +    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)));
    1.51  
    1.52  val THEN_att =
    1.53 -  syntax (Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.54 -    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B))));
    1.55 +  Scan.lift (Scan.optional (Args.bracks P.nat) 1) -- thm
    1.56 +    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
    1.57  
    1.58  val OF_att =
    1.59 -  syntax (thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A)));
    1.60 +  thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
    1.61  
    1.62  
    1.63  (* rename_abs *)
    1.64  
    1.65 -val rename_abs = syntax
    1.66 -  (Scan.lift (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')));
    1.67 +val rename_abs = Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars');
    1.68  
    1.69  
    1.70  (* unfold / fold definitions *)
    1.71  
    1.72  fun unfolded_syntax rule =
    1.73 -  syntax (thms >>
    1.74 -    (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
    1.75 +  thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
    1.76  
    1.77  val unfolded = unfolded_syntax LocalDefs.unfold;
    1.78  val folded = unfolded_syntax LocalDefs.fold;
    1.79  
    1.80  
    1.81 -(* rule cases *)
    1.82 -
    1.83 -val consumes = syntax (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes);
    1.84 -val case_names = syntax (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names);
    1.85 -val case_conclusion =
    1.86 -  syntax (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion);
    1.87 -val params = syntax (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params);
    1.88 -
    1.89 -
    1.90  (* rule format *)
    1.91  
    1.92 -val rule_format = syntax (Args.mode "no_asm"
    1.93 -  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format));
    1.94 +val rule_format = Args.mode "no_asm"
    1.95 +  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
    1.96  
    1.97 -val elim_format = no_args (Thm.rule_attribute (K Tactic.make_elim));
    1.98 +val elim_format = Thm.rule_attribute (K Tactic.make_elim);
    1.99  
   1.100  
   1.101  (* misc rules *)
   1.102  
   1.103 -val standard = no_args (Thm.rule_attribute (K Drule.standard));
   1.104 -
   1.105 -val no_vars = no_args (Thm.rule_attribute (fn context => fn th =>
   1.106 +val no_vars = Thm.rule_attribute (fn context => fn th =>
   1.107    let
   1.108      val ctxt = Variable.set_body false (Context.proof_of context);
   1.109      val ((_, [th']), _) = Variable.import_thms true [th] ctxt;
   1.110 -  in th' end));
   1.111 +  in th' end);
   1.112  
   1.113  val eta_long =
   1.114 -  no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion)));
   1.115 +  Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
   1.116  
   1.117 -val rotated = syntax
   1.118 -  (Scan.lift (Scan.optional P.int 1) >> (fn n => Thm.rule_attribute (K (rotate_prems n))));
   1.119 -
   1.120 -val abs_def = no_args (Thm.rule_attribute (K Drule.abs_def));
   1.121 +val rotated = Scan.optional P.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
   1.122  
   1.123  
   1.124  (* theory setup *)
   1.125  
   1.126  val _ = Context.>> (Context.map_theory
   1.127 - (add_attributes
   1.128 -   [("attribute", internal_att, "internal attribute"),
   1.129 -    ("tagged", tagged, "tagged theorem"),
   1.130 -    ("untagged", untagged, "untagged theorem"),
   1.131 -    ("kind", kind, "theorem kind"),
   1.132 -    ("COMP", COMP_att, "direct composition with rules (no lifting)"),
   1.133 -    ("THEN", THEN_att, "resolution with rule"),
   1.134 -    ("OF", OF_att, "rule applied to facts"),
   1.135 -    ("rename_abs", rename_abs, "rename bound variables in abstractions"),
   1.136 -    ("unfolded", unfolded, "unfolded definitions"),
   1.137 -    ("folded", folded, "folded definitions"),
   1.138 -    ("standard", standard, "result put into standard form"),
   1.139 -    ("elim_format", elim_format, "destruct rule turned into elimination rule format"),
   1.140 -    ("no_vars", no_vars, "frozen schematic vars"),
   1.141 -    ("eta_long", eta_long, "put theorem into eta long beta normal form"),
   1.142 -    ("consumes", consumes, "number of consumed facts"),
   1.143 -    ("case_names", case_names, "named rule cases"),
   1.144 -    ("case_conclusion", case_conclusion, "named conclusion of rule cases"),
   1.145 -    ("params", params, "named rule parameters"),
   1.146 -    ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
   1.147 -    ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
   1.148 -    ("rule_format", rule_format, "result put into standard rule format"),
   1.149 -    ("rotated", rotated, "rotated theorem premises"),
   1.150 -    ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
   1.151 -      "declaration of definitional transformations"),
   1.152 -    ("abs_def", abs_def, "abstract over free variables of a definition")]));
   1.153 + (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
   1.154 +    "internal attribute" #>
   1.155 +  setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
   1.156 +  setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
   1.157 +  setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
   1.158 +  setup (Binding.name "COMP") COMP_att "direct composition with rules (no lifting)" #>
   1.159 +  setup (Binding.name "THEN") THEN_att "resolution with rule" #>
   1.160 +  setup (Binding.name "OF") OF_att "rule applied to facts" #>
   1.161 +  setup (Binding.name "rename_abs") (Scan.lift rename_abs)
   1.162 +    "rename bound variables in abstractions" #>
   1.163 +  setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   1.164 +  setup (Binding.name "folded") folded "folded definitions" #>
   1.165 +  setup (Binding.name "consumes") (Scan.lift (Scan.optional P.nat 1) >> RuleCases.consumes)
   1.166 +    "number of consumed facts" #>
   1.167 +  setup (Binding.name "case_names") (Scan.lift (Scan.repeat1 Args.name) >> RuleCases.case_names)
   1.168 +    "named rule cases" #>
   1.169 +  setup (Binding.name "case_conclusion")
   1.170 +    (Scan.lift (Args.name -- Scan.repeat Args.name) >> RuleCases.case_conclusion)
   1.171 +    "named conclusion of rule cases" #>
   1.172 +  setup (Binding.name "params")
   1.173 +    (Scan.lift (P.and_list1 (Scan.repeat Args.name)) >> RuleCases.params)
   1.174 +    "named rule parameters" #>
   1.175 +  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.standard)))
   1.176 +    "result put into standard form (legacy)" #>
   1.177 +  setup (Binding.name "rule_format") rule_format "result put into canonical rule format" #>
   1.178 +  setup (Binding.name "elim_format") (Scan.succeed elim_format)
   1.179 +    "destruct rule turned into elimination rule format" #>
   1.180 +  setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
   1.181 +  setup (Binding.name "eta_long") (Scan.succeed eta_long)
   1.182 +    "put theorem into eta long beta normal form" #>
   1.183 +  setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
   1.184 +    "declaration of atomize rule" #>
   1.185 +  setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
   1.186 +    "declaration of rulify rule" #>
   1.187 +  setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   1.188 +  setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
   1.189 +    "declaration of definitional transformations" #>
   1.190 +  setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
   1.191 +    "abstract over free variables of a definition"));
   1.192  
   1.193  
   1.194