src/Pure/Pure.thy
changeset 62898 fdc290b68ecd
parent 62873 2f9c8a18f832
child 62902 3c0f53eae166
     1.1 --- a/src/Pure/Pure.thy	Thu Apr 07 12:08:02 2016 +0200
     1.2 +++ b/src/Pure/Pure.thy	Thu Apr 07 12:13:11 2016 +0200
     1.3 @@ -1281,109 +1281,6 @@
     1.4  in end\<close>
     1.5  
     1.6  
     1.7 -section \<open>Isar attributes\<close>
     1.8 -
     1.9 -attribute_setup tagged =
    1.10 -  \<open>Scan.lift (Args.name -- Args.name) >> Thm.tag\<close>
    1.11 -  "tagged theorem"
    1.12 -
    1.13 -attribute_setup untagged =
    1.14 -  \<open>Scan.lift Args.name >> Thm.untag\<close>
    1.15 -  "untagged theorem"
    1.16 -
    1.17 -attribute_setup kind =
    1.18 -  \<open>Scan.lift Args.name >> Thm.kind\<close>
    1.19 -  "theorem kind"
    1.20 -
    1.21 -attribute_setup THEN =
    1.22 -  \<open>Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
    1.23 -    >> (fn (i, B) => Thm.rule_attribute [B] (fn _ => fn A => A RSN (i, B)))\<close>
    1.24 -  "resolution with rule"
    1.25 -
    1.26 -attribute_setup OF =
    1.27 -  \<open>Attrib.thms >> (fn Bs => Thm.rule_attribute Bs (fn _ => fn A => A OF Bs))\<close>
    1.28 -  "rule resolved with facts"
    1.29 -
    1.30 -attribute_setup rename_abs =
    1.31 -  \<open>Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    1.32 -    Thm.rule_attribute [] (K (Drule.rename_bvars' vs)))\<close>
    1.33 -  "rename bound variables in abstractions"
    1.34 -
    1.35 -attribute_setup unfolded =
    1.36 -  \<open>Attrib.thms >> (fn ths =>
    1.37 -    Thm.rule_attribute ths (fn context => Local_Defs.unfold (Context.proof_of context) ths))\<close>
    1.38 -  "unfolded definitions"
    1.39 -
    1.40 -attribute_setup folded =
    1.41 -  \<open>Attrib.thms >> (fn ths =>
    1.42 -    Thm.rule_attribute ths (fn context => Local_Defs.fold (Context.proof_of context) ths))\<close>
    1.43 -  "folded definitions"
    1.44 -
    1.45 -attribute_setup consumes =
    1.46 -  \<open>Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes\<close>
    1.47 -  "number of consumed facts"
    1.48 -
    1.49 -attribute_setup constraints =
    1.50 -  \<open>Scan.lift Parse.nat >> Rule_Cases.constraints\<close>
    1.51 -  "number of equality constraints"
    1.52 -
    1.53 -attribute_setup case_names =
    1.54 -  \<open>Scan.lift (Scan.repeat1 (Args.name --
    1.55 -    Scan.optional (@{keyword "["} |-- Scan.repeat1 (Args.maybe Args.name) --| @{keyword "]"}) []))
    1.56 -    >> (fn cs =>
    1.57 -      Rule_Cases.cases_hyp_names
    1.58 -        (map #1 cs)
    1.59 -        (map (map (the_default Rule_Cases.case_hypsN) o #2) cs))\<close>
    1.60 -  "named rule cases"
    1.61 -
    1.62 -attribute_setup case_conclusion =
    1.63 -  \<open>Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion\<close>
    1.64 -  "named conclusion of rule cases"
    1.65 -
    1.66 -attribute_setup params =
    1.67 -  \<open>Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params\<close>
    1.68 -  "named rule parameters"
    1.69 -
    1.70 -attribute_setup rule_format =
    1.71 -  \<open>Scan.lift (Args.mode "no_asm")
    1.72 -    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)\<close>
    1.73 -  "result put into canonical rule format"
    1.74 -
    1.75 -attribute_setup elim_format =
    1.76 -  \<open>Scan.succeed (Thm.rule_attribute [] (K Tactic.make_elim))\<close>
    1.77 -  "destruct rule turned into elimination rule format"
    1.78 -
    1.79 -attribute_setup no_vars =
    1.80 -  \<open>Scan.succeed (Thm.rule_attribute [] (fn context => fn th =>
    1.81 -    let
    1.82 -      val ctxt = Variable.set_body false (Context.proof_of context);
    1.83 -      val ((_, [th']), _) = Variable.import true [th] ctxt;
    1.84 -    in th' end))\<close>
    1.85 -  "imported schematic variables"
    1.86 -
    1.87 -attribute_setup atomize =
    1.88 -  \<open>Scan.succeed Object_Logic.declare_atomize\<close>
    1.89 -  "declaration of atomize rule"
    1.90 -
    1.91 -attribute_setup rulify =
    1.92 -  \<open>Scan.succeed Object_Logic.declare_rulify\<close>
    1.93 -  "declaration of rulify rule"
    1.94 -
    1.95 -attribute_setup rotated =
    1.96 -  \<open>Scan.lift (Scan.optional Parse.int 1
    1.97 -    >> (fn n => Thm.rule_attribute [] (fn _ => rotate_prems n)))\<close>
    1.98 -  "rotated theorem premises"
    1.99 -
   1.100 -attribute_setup defn =
   1.101 -  \<open>Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del\<close>
   1.102 -  "declaration of definitional transformations"
   1.103 -
   1.104 -attribute_setup abs_def =
   1.105 -  \<open>Scan.succeed (Thm.rule_attribute [] (fn context =>
   1.106 -    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))\<close>
   1.107 -  "abstract over free variables of definitional theorem"
   1.108 -
   1.109 -
   1.110  section \<open>Further content for the Pure theory\<close>
   1.111  
   1.112  subsection \<open>Meta-level connectives in assumptions\<close>