src/Pure/Pure.thy
changeset 55140 7eb0c04e4c40
parent 55030 9a9049d12e21
child 55141 863b4f9f6bd7
     1.1 --- a/src/Pure/Pure.thy	Sat Jan 25 16:59:41 2014 +0100
     1.2 +++ b/src/Pure/Pure.thy	Sat Jan 25 18:18:03 2014 +0100
     1.3 @@ -111,6 +111,117 @@
     1.4  ML_file "Tools/simplifier_trace.ML"
     1.5  
     1.6  
     1.7 +section {* Basic attributes *}
     1.8 +
     1.9 +attribute_setup tagged =
    1.10 +  "Scan.lift (Args.name -- Args.name) >> Thm.tag"
    1.11 +  "tagged theorem"
    1.12 +
    1.13 +attribute_setup untagged =
    1.14 +  "Scan.lift Args.name >> Thm.untag"
    1.15 +  "untagged theorem"
    1.16 +
    1.17 +attribute_setup kind =
    1.18 +  "Scan.lift Args.name >> Thm.kind"
    1.19 +  "theorem kind"
    1.20 +
    1.21 +attribute_setup THEN =
    1.22 +  "Scan.lift (Scan.optional (Args.bracks Parse.nat) 1) -- Attrib.thm
    1.23 +    >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))"
    1.24 +  "resolution with rule"
    1.25 +
    1.26 +attribute_setup OF =
    1.27 +  "Attrib.thms >> (fn Bs => Thm.rule_attribute (fn _ => fn A => A OF Bs))"
    1.28 +  "rule resolved with facts"
    1.29 +
    1.30 +attribute_setup rename_abs =
    1.31 +  "Scan.lift (Scan.repeat (Args.maybe Args.name)) >> (fn vs =>
    1.32 +    Thm.rule_attribute (K (Drule.rename_bvars' vs)))"
    1.33 +  "rename bound variables in abstractions"
    1.34 +
    1.35 +attribute_setup unfolded =
    1.36 +  "Attrib.thms >> (fn ths =>
    1.37 +    Thm.rule_attribute (fn context => Local_Defs.unfold (Context.proof_of context) ths))"
    1.38 +  "unfolded definitions"
    1.39 +
    1.40 +attribute_setup folded =
    1.41 +  "Attrib.thms >> (fn ths =>
    1.42 +    Thm.rule_attribute (fn context => Local_Defs.fold (Context.proof_of context) ths))"
    1.43 +  "folded definitions"
    1.44 +
    1.45 +attribute_setup consumes =
    1.46 +  "Scan.lift (Scan.optional Parse.int 1) >> Rule_Cases.consumes"
    1.47 +  "number of consumed facts"
    1.48 +
    1.49 +attribute_setup constraints =
    1.50 +  "Scan.lift Parse.nat >> Rule_Cases.constraints"
    1.51 +  "number of equality constraints"
    1.52 +
    1.53 +attribute_setup case_names = {*
    1.54 +  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))
    1.60 +*} "named rule cases"
    1.61 +
    1.62 +attribute_setup case_conclusion =
    1.63 +  "Scan.lift (Args.name -- Scan.repeat Args.name) >> Rule_Cases.case_conclusion"
    1.64 +  "named conclusion of rule cases"
    1.65 +
    1.66 +attribute_setup params =
    1.67 +  "Scan.lift (Parse.and_list1 (Scan.repeat Args.name)) >> Rule_Cases.params"
    1.68 +  "named rule parameters"
    1.69 +
    1.70 +attribute_setup standard =
    1.71 +  "Scan.succeed (Thm.rule_attribute (K Drule.export_without_context))"
    1.72 +  "result put into standard form (legacy)"
    1.73 +
    1.74 +attribute_setup rule_format = {*
    1.75 +  Scan.lift (Args.mode "no_asm")
    1.76 +    >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format)
    1.77 +*} "result put into canonical rule format"
    1.78 +
    1.79 +attribute_setup elim_format =
    1.80 +  "Scan.succeed (Thm.rule_attribute (K Tactic.make_elim))"
    1.81 +  "destruct rule turned into elimination rule format"
    1.82 +
    1.83 +attribute_setup no_vars = {*
    1.84 +  Scan.succeed (Thm.rule_attribute (fn context => fn th =>
    1.85 +    let
    1.86 +      val ctxt = Variable.set_body false (Context.proof_of context);
    1.87 +      val ((_, [th']), _) = Variable.import true [th] ctxt;
    1.88 +    in th' end))
    1.89 +*} "imported schematic variables"
    1.90 +
    1.91 +attribute_setup eta_long =
    1.92 +  "Scan.succeed (Thm.rule_attribute (fn _ => Conv.fconv_rule Drule.eta_long_conversion))"
    1.93 +  "put theorem into eta long beta normal form"
    1.94 +
    1.95 +attribute_setup atomize =
    1.96 +  "Scan.succeed Object_Logic.declare_atomize"
    1.97 +  "declaration of atomize rule"
    1.98 +
    1.99 +attribute_setup rulify =
   1.100 +  "Scan.succeed Object_Logic.declare_rulify"
   1.101 +  "declaration of rulify rule"
   1.102 +
   1.103 +attribute_setup rotated =
   1.104 +  "Scan.lift (Scan.optional Parse.int 1
   1.105 +    >> (fn n => Thm.rule_attribute (fn _ => rotate_prems n)))"
   1.106 +  "rotated theorem premises"
   1.107 +
   1.108 +attribute_setup defn =
   1.109 +  "Attrib.add_del Local_Defs.defn_add Local_Defs.defn_del"
   1.110 +  "declaration of definitional transformations"
   1.111 +
   1.112 +attribute_setup abs_def =
   1.113 +  "Scan.succeed (Thm.rule_attribute (fn context =>
   1.114 +    Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def))"
   1.115 +  "abstract over free variables of definitional theorem"
   1.116 +
   1.117 +
   1.118  section {* Further content for the Pure theory *}
   1.119  
   1.120  subsection {* Meta-level connectives in assumptions *}