define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
authorwenzelm
Sat Jan 25 18:18:03 2014 +0100 (2014-01-25)
changeset 551407eb0c04e4c40
parent 55139 4d899933a51a
child 55141 863b4f9f6bd7
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
src/Pure/Isar/attrib.ML
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Isar/attrib.ML	Sat Jan 25 16:59:41 2014 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Sat Jan 25 18:18:03 2014 +0100
     1.3 @@ -37,6 +37,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 internal: (morphism -> attribute) -> src
     1.8    val add_del: attribute -> attribute -> attribute context_parser
     1.9    val thm_sel: Facts.interval list parser
    1.10    val thm: thm context_parser
    1.11 @@ -45,7 +46,6 @@
    1.12    val partial_evaluation: Proof.context ->
    1.13      (binding * (thm list * Args.src list) list) list ->
    1.14      (binding * (thm list * Args.src list) list) list
    1.15 -  val internal: (morphism -> attribute) -> src
    1.16    val print_options: Proof.context -> unit
    1.17    val config_bool: Binding.binding ->
    1.18      (Context.generic -> bool) -> bool Config.T * (theory -> theory)
    1.19 @@ -194,6 +194,15 @@
    1.20        ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
    1.21  
    1.22  
    1.23 +(* internal attribute *)
    1.24 +
    1.25 +fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
    1.26 +
    1.27 +val _ = Theory.setup
    1.28 + (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
    1.29 +    "internal attribute");
    1.30 +
    1.31 +
    1.32  (* add/del syntax *)
    1.33  
    1.34  fun add_del add del = Scan.lift (Args.add >> K add || Args.del >> K del || Scan.succeed add);
    1.35 @@ -318,119 +327,6 @@
    1.36  
    1.37  
    1.38  
    1.39 -(** basic attributes **)
    1.40 -
    1.41 -(* internal *)
    1.42 -
    1.43 -fun internal att = Args.src (("Pure.attribute", [Token.mk_attribute att]), Position.none);
    1.44 -
    1.45 -
    1.46 -(* rule composition *)
    1.47 -
    1.48 -val THEN_att =
    1.49 -  Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    1.50 -    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)));
    1.51 -
    1.52 -val OF_att =
    1.53 -  thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A));
    1.54 -
    1.55 -
    1.56 -(* rename_abs *)
    1.57 -
    1.58 -val rename_abs =
    1.59 -  Scan.repeat (Args.maybe Args.name)
    1.60 -  >> (fn args => Thm.rule_attribute (K (Drule.rename_bvars' args)));
    1.61 -
    1.62 -
    1.63 -(* unfold / fold definitions *)
    1.64 -
    1.65 -fun unfolded_syntax rule =
    1.66 -  thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
    1.67 -
    1.68 -val unfolded = unfolded_syntax Local_Defs.unfold;
    1.69 -val folded = unfolded_syntax Local_Defs.fold;
    1.70 -
    1.71 -
    1.72 -(* rule format *)
    1.73 -
    1.74 -fun rule_format true = Object_Logic.rule_format_no_asm
    1.75 -  | rule_format false = Object_Logic.rule_format;
    1.76 -
    1.77 -val elim_format = Thm.rule_attribute (K Tactic.make_elim);
    1.78 -
    1.79 -
    1.80 -(* case names *)
    1.81 -
    1.82 -val case_names =
    1.83 -  Scan.repeat1 (Args.name --
    1.84 -    Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []) >>
    1.85 -  (fn cs =>
    1.86 -    Rule_Cases.cases_hyp_names (map fst cs)
    1.87 -      (map (map (the_default Rule_Cases.case_hypsN) o snd) cs));
    1.88 -
    1.89 -
    1.90 -(* misc rules *)
    1.91 -
    1.92 -val no_vars = Thm.rule_attribute (fn context => fn th =>
    1.93 -  let
    1.94 -    val ctxt = Variable.set_body false (Context.proof_of context);
    1.95 -    val ((_, [th']), _) = Variable.import true [th] ctxt;
    1.96 -  in th' end);
    1.97 -
    1.98 -val eta_long =
    1.99 -  Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion));
   1.100 -
   1.101 -val rotated = Scan.optional Parse.int 1 >> (fn n => Thm.rule_attribute (K (rotate_prems n)));
   1.102 -
   1.103 -
   1.104 -(* theory setup *)
   1.105 -
   1.106 -val _ = Theory.setup
   1.107 - (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
   1.108 -    "internal attribute" #>
   1.109 -  setup (Binding.name "tagged") (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
   1.110 -  setup (Binding.name "untagged") (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
   1.111 -  setup (Binding.name "kind") (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
   1.112 -  setup (Binding.name "THEN") THEN_att "resolution with rule" #>
   1.113 -  setup (Binding.name "OF") OF_att "rule applied to facts" #>
   1.114 -  setup (Binding.name "rename_abs") (Scan.lift rename_abs)
   1.115 -    "rename bound variables in abstractions" #>
   1.116 -  setup (Binding.name "unfolded") unfolded "unfolded definitions" #>
   1.117 -  setup (Binding.name "folded") folded "folded definitions" #>
   1.118 -  setup (Binding.name "consumes") (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
   1.119 -    "number of consumed facts" #>
   1.120 -  setup (Binding.name "constraints") (Scan.lift Parse.nat >> Rule_Cases.constraints)
   1.121 -    "number of equality constraints" #>
   1.122 -  setup (Binding.name "case_names") (Scan.lift case_names) "named rule cases" #>
   1.123 -  setup (Binding.name "case_conclusion")
   1.124 -    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
   1.125 -    "named conclusion of rule cases" #>
   1.126 -  setup (Binding.name "params")
   1.127 -    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
   1.128 -    "named rule parameters" #>
   1.129 -  setup (Binding.name "standard") (Scan.succeed (Thm.rule_attribute (K Drule.export_without_context)))
   1.130 -    "result put into standard form (legacy)" #>
   1.131 -  setup (Binding.name "rule_format") (Scan.lift (Args.mode "no_asm") >> rule_format)
   1.132 -    "result put into canonical rule format" #>
   1.133 -  setup (Binding.name "elim_format") (Scan.succeed elim_format)
   1.134 -    "destruct rule turned into elimination rule format" #>
   1.135 -  setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
   1.136 -  setup (Binding.name "eta_long") (Scan.succeed eta_long)
   1.137 -    "put theorem into eta long beta normal form" #>
   1.138 -  setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
   1.139 -    "declaration of atomize rule" #>
   1.140 -  setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
   1.141 -    "declaration of rulify rule" #>
   1.142 -  setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   1.143 -  setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
   1.144 -    "declaration of definitional transformations" #>
   1.145 -  setup (Binding.name "abs_def")
   1.146 -    (Scan.succeed (Thm.rule_attribute (fn context =>
   1.147 -      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
   1.148 -    "abstract over free variables of definitional theorem");
   1.149 -
   1.150 -
   1.151 -
   1.152  (** configuration options **)
   1.153  
   1.154  (* naming *)
     2.1 --- a/src/Pure/Pure.thy	Sat Jan 25 16:59:41 2014 +0100
     2.2 +++ b/src/Pure/Pure.thy	Sat Jan 25 18:18:03 2014 +0100
     2.3 @@ -111,6 +111,117 @@
     2.4  ML_file "Tools/simplifier_trace.ML"
     2.5  
     2.6  
     2.7 +section {* Basic attributes *}
     2.8 +
     2.9 +attribute_setup tagged =
    2.10 +  "Scan.lift (Args.name -- Args.name) >> Thm.tag"
    2.11 +  "tagged theorem"
    2.12 +
    2.13 +attribute_setup untagged =
    2.14 +  "Scan.lift Args.name >> Thm.untag"
    2.15 +  "untagged theorem"
    2.16 +
    2.17 +attribute_setup kind =
    2.18 +  "Scan.lift Args.name >> Thm.kind"
    2.19 +  "theorem kind"
    2.20 +
    2.21 +attribute_setup THEN =
    2.22 +  "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
    2.23 +    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
    2.24 +  "resolution with rule"
    2.25 +
    2.26 +attribute_setup OF =
    2.27 +  "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
    2.28 +  "rule resolved with facts"
    2.29 +
    2.30 +attribute_setup rename_abs =
    2.31 +  "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    2.32 +    Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
    2.33 +  "rename bound variables in abstractions"
    2.34 +
    2.35 +attribute_setup unfolded =
    2.36 +  "Attrib.thms >> (fn ths =>
    2.37 +    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
    2.38 +  "unfolded definitions"
    2.39 +
    2.40 +attribute_setup folded =
    2.41 +  "Attrib.thms >> (fn ths =>
    2.42 +    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
    2.43 +  "folded definitions"
    2.44 +
    2.45 +attribute_setup consumes =
    2.46 +  "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
    2.47 +  "number of consumed facts"
    2.48 +
    2.49 +attribute_setup constraints =
    2.50 +  "Scan.lift Parse.nat >> Rule_Cases.constraints"
    2.51 +  "number of equality constraints"
    2.52 +
    2.53 +attribute_setup case_names = {*
    2.54 +  Scan.lift (Scan.repeat1 (Args.name --
    2.55 +    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
    2.56 +  >> (fn cs =>
    2.57 +      Rule_Cases.cases_hyp_names
    2.58 +        (map #1 cs)
    2.59 +        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))
    2.60 +*} "named rule cases"
    2.61 +
    2.62 +attribute_setup case_conclusion =
    2.63 +  "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
    2.64 +  "named conclusion of rule cases"
    2.65 +
    2.66 +attribute_setup params =
    2.67 +  "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
    2.68 +  "named rule parameters"
    2.69 +
    2.70 +attribute_setup standard =
    2.71 +  "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
    2.72 +  "result put into standard form (legacy)"
    2.73 +
    2.74 +attribute_setup rule_format = {*
    2.75 +  Scan.lift (Args.mode "no_asm")
    2.76 +    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
    2.77 +*} "result put into canonical rule format"
    2.78 +
    2.79 +attribute_setup elim_format =
    2.80 +  "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
    2.81 +  "destruct rule turned into elimination rule format"
    2.82 +
    2.83 +attribute_setup no_vars = {*
    2.84 +  Scan.succeed (Thm.rule_attribute (fn context => fn th =>
    2.85 +    let
    2.86 +      val ctxt = Variable.set_body false (Context.proof_of context);
    2.87 +      val ((_, [th']), _) = Variable.import true [th] ctxt;
    2.88 +    in th' end))
    2.89 +*} "imported schematic variables"
    2.90 +
    2.91 +attribute_setup eta_long =
    2.92 +  "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
    2.93 +  "put theorem into eta long beta normal form"
    2.94 +
    2.95 +attribute_setup atomize =
    2.96 +  "Scan.succeed Object_Logic.declare_atomize"
    2.97 +  "declaration of atomize rule"
    2.98 +
    2.99 +attribute_setup rulify =
   2.100 +  "Scan.succeed Object_Logic.declare_rulify"
   2.101 +  "declaration of rulify rule"
   2.102 +
   2.103 +attribute_setup rotated =
   2.104 +  "Scan.lift (Scan.optional Parse.int 1
   2.105 +    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   2.106 +  "rotated theorem premises"
   2.107 +
   2.108 +attribute_setup defn =
   2.109 +  "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   2.110 +  "declaration of definitional transformations"
   2.111 +
   2.112 +attribute_setup abs_def =
   2.113 +  "Scan.succeed (Thm.rule_attribute (fn context =>
   2.114 +    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   2.115 +  "abstract over free variables of definitional theorem"
   2.116 +
   2.117 +
   2.118  section {* Further content for the Pure theory *}
   2.119  
   2.120  subsection {* Meta-level connectives in assumptions *}