Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
authorwenzelm
Thu Apr 07 12:13:11 2016 +0200 (2016-04-07)
changeset 62898fdc290b68ecd
parent 62897 8093203f0b89
child 62899 845ed4584e21
Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
src/Pure/Isar/attrib.ML
src/Pure/Pure.thy
     1.1 --- a/src/Pure/Isar/attrib.ML	Thu Apr 07 12:08:02 2016 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Apr 07 12:13:11 2016 +0200
     1.3 @@ -500,7 +500,78 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val _ = Theory.setup
     1.7 - (register_config Goal.quick_and_dirty_raw #>
     1.8 + (setup @{binding tagged} (Scan.lift (Args.name -- Args.name) >> Thm.tag) "tagged theorem" #>
     1.9 +  setup @{binding untagged} (Scan.lift Args.name >> Thm.untag) "untagged theorem" #>
    1.10 +  setup @{binding kind} (Scan.lift Args.name >> Thm.kind) "theorem kind" #>
    1.11 +  setup @{binding THEN}
    1.12 +    (Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- thm
    1.13 +      >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B))))
    1.14 +    "resolution with rule" #>
    1.15 +  setup @{binding OF}
    1.16 +    (thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs)))
    1.17 +    "rule resolved with facts" #>
    1.18 +  setup @{binding rename_abs}
    1.19 +    (Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    1.20 +      Thm.rule_attribute [] (K (Drule.rename_bvars' vs))))
    1.21 +    "rename bound variables in abstractions" #>
    1.22 +  setup @{binding unfolded}
    1.23 +    (thms >> (fn ths =>
    1.24 +      Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths)))
    1.25 +    "unfolded definitions" #>
    1.26 +  setup @{binding folded}
    1.27 +    (thms >> (fn ths =>
    1.28 +      Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths)))
    1.29 +    "folded definitions" #>
    1.30 +  setup @{binding consumes}
    1.31 +    (Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes)
    1.32 +    "number of consumed facts" #>
    1.33 +  setup @{binding constraints}
    1.34 +    (Scan.lift Parse.nat >> Rule_Cases.constraints)
    1.35 +    "number of equality constraints" #>
    1.36 +  setup @{binding case_names}
    1.37 +    (Scan.lift (Scan.repeat1 (Args.name --
    1.38 +      Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") []))
    1.39 +      >> (fn cs =>
    1.40 +        Rule_Cases.cases_hyp_names
    1.41 +          (map #1 cs)
    1.42 +          (map (map (the_default Rule_Cases.case_hypsN) o #2) cs)))
    1.43 +    "named rule cases" #>
    1.44 +  setup @{binding case_conclusion}
    1.45 +    (Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion)
    1.46 +    "named conclusion of rule cases" #>
    1.47 +  setup @{binding params}
    1.48 +    (Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params)
    1.49 +    "named rule parameters" #>
    1.50 +  setup @{binding rule_format}
    1.51 +    (Scan.lift (Args.mode "no_asm")
    1.52 +      >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format))
    1.53 +    "result put into canonical rule format" #>
    1.54 +  setup @{binding elim_format}
    1.55 +    (Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim)))
    1.56 +    "destruct rule turned into elimination rule format" #>
    1.57 +  setup @{binding no_vars}
    1.58 +    (Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
    1.59 +      let
    1.60 +        val ctxt = Variable.set_body false (Context.proof_of context);
    1.61 +        val ((_, [th']), _) = Variable.import true [th] ctxt;
    1.62 +      in th' end)))
    1.63 +    "imported schematic variables" #>
    1.64 +  setup @{binding atomize}
    1.65 +    (Scan.succeed Object_Logic.declare_atomize) "declaration of atomize rule" #>
    1.66 +  setup @{binding rulify}
    1.67 +    (Scan.succeed Object_Logic.declare_rulify) "declaration of rulify rule" #>
    1.68 +  setup @{binding rotated}
    1.69 +    (Scan.lift (Scan.optional Parse.int 1
    1.70 +      >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))) "rotated theorem premises" #>
    1.71 +  setup @{binding defn}
    1.72 +    (add_del Local_Defs.defn_add Local_Defs.defn_del)
    1.73 +    "declaration of definitional transformations" #>
    1.74 +  setup @{binding abs_def}
    1.75 +    (Scan.succeed (Thm.rule_attribute [] (fn context =>
    1.76 +      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
    1.77 +    "abstract over free variables of definitional theorem" #>
    1.78 +
    1.79 +  register_config Goal.quick_and_dirty_raw #>
    1.80    register_config Ast.trace_raw #>
    1.81    register_config Ast.stats_raw #>
    1.82    register_config Printer.show_brackets_raw #>
     2.1 --- a/src/Pure/Pure.thy	Thu Apr 07 12:08:02 2016 +0200
     2.2 +++ b/src/Pure/Pure.thy	Thu Apr 07 12:13:11 2016 +0200
     2.3 @@ -1281,109 +1281,6 @@
     2.4  in end\<close>
     2.5  
     2.6  
     2.7 -section \<open>Isar attributes\<close>
     2.8 -
     2.9 -attribute_setup tagged =
    2.10 -  \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
    2.11 -  "tagged theorem"
    2.12 -
    2.13 -attribute_setup untagged =
    2.14 -  \<open>Scan.lift Args.name >> Thm.untag\<close>
    2.15 -  "untagged theorem"
    2.16 -
    2.17 -attribute_setup kind =
    2.18 -  \<open>Scan.lift Args.name >> Thm.kind\<close>
    2.19 -  "theorem kind"
    2.20 -
    2.21 -attribute_setup THEN =
    2.22 -  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
    2.23 -    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
    2.24 -  "resolution with rule"
    2.25 -
    2.26 -attribute_setup OF =
    2.27 -  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
    2.28 -  "rule resolved with facts"
    2.29 -
    2.30 -attribute_setup rename_abs =
    2.31 -  \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    2.32 -    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
    2.33 -  "rename bound variables in abstractions"
    2.34 -
    2.35 -attribute_setup unfolded =
    2.36 -  \<open>Attrib.thms >> (fn ths =>
    2.37 -    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
    2.38 -  "unfolded definitions"
    2.39 -
    2.40 -attribute_setup folded =
    2.41 -  \<open>Attrib.thms >> (fn ths =>
    2.42 -    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
    2.43 -  "folded definitions"
    2.44 -
    2.45 -attribute_setup consumes =
    2.46 -  \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
    2.47 -  "number of consumed facts"
    2.48 -
    2.49 -attribute_setup constraints =
    2.50 -  \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
    2.51 -  "number of equality constraints"
    2.52 -
    2.53 -attribute_setup case_names =
    2.54 -  \<open>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))\<close>
    2.60 -  "named rule cases"
    2.61 -
    2.62 -attribute_setup case_conclusion =
    2.63 -  \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
    2.64 -  "named conclusion of rule cases"
    2.65 -
    2.66 -attribute_setup params =
    2.67 -  \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
    2.68 -  "named rule parameters"
    2.69 -
    2.70 -attribute_setup rule_format =
    2.71 -  \<open>Scan.lift (Args.mode "no_asm")
    2.72 -    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
    2.73 -  "result put into canonical rule format"
    2.74 -
    2.75 -attribute_setup elim_format =
    2.76 -  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
    2.77 -  "destruct rule turned into elimination rule format"
    2.78 -
    2.79 -attribute_setup no_vars =
    2.80 -  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
    2.81 -    let
    2.82 -      val ctxt = Variable.set_body false (Context.proof_of context);
    2.83 -      val ((_, [th']), _) = Variable.import true [th] ctxt;
    2.84 -    in th' end))\<close>
    2.85 -  "imported schematic variables"
    2.86 -
    2.87 -attribute_setup atomize =
    2.88 -  \<open>Scan.succeed Object_Logic.declare_atomize\<close>
    2.89 -  "declaration of atomize rule"
    2.90 -
    2.91 -attribute_setup rulify =
    2.92 -  \<open>Scan.succeed Object_Logic.declare_rulify\<close>
    2.93 -  "declaration of rulify rule"
    2.94 -
    2.95 -attribute_setup rotated =
    2.96 -  \<open>Scan.lift (Scan.optional Parse.int 1
    2.97 -    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
    2.98 -  "rotated theorem premises"
    2.99 -
   2.100 -attribute_setup defn =
   2.101 -  \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
   2.102 -  "declaration of definitional transformations"
   2.103 -
   2.104 -attribute_setup abs_def =
   2.105 -  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
   2.106 -    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
   2.107 -  "abstract over free variables of definitional theorem"
   2.108 -
   2.109 -
   2.110  section \<open>Further content for the Pure theory\<close>
   2.111  
   2.112  subsection \<open>Meta-level connectives in assumptions\<close>