# HG changeset patch # User wenzelm # Date 1461003859 -7200 # Node ID 80ef19b5149313340b5efae35e65467a5bc618a3 # Parent 00f4461fa99f79fd676d737b5ab6f422330d4bfa prefer internal attribute source; diff -r 00f4461fa99f -r 80ef19b51493 src/Doc/Isar_Ref/Proof.thy --- a/src/Doc/Isar_Ref/Proof.thy Mon Apr 18 15:51:48 2016 +0100 +++ b/src/Doc/Isar_Ref/Proof.thy Mon Apr 18 20:24:19 2016 +0200 @@ -970,7 +970,7 @@ @{rail \ @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')') ; - @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +) + @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) *) ']' ) ? ) +) ; @@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) ; diff -r 00f4461fa99f -r 80ef19b51493 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 18 20:24:19 2016 +0200 @@ -834,16 +834,14 @@ |> Thm.close_derivation |> rotate_prems ~1; - val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); val cases_set_attr = Attrib.internal (K (Induct.cases_pred (name_of_set set))); val ctr_names = quasi_unambiguous_case_names (flat (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs))); - val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); in (* TODO: @{attributes [elim?]} *) - (thm, [consumes_attr, cases_set_attr, case_names_attr]) + (thm, [Attrib.consumes 1, cases_set_attr, Attrib.case_names ctr_names]) end) setAs) end; @@ -925,11 +923,8 @@ let val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms; val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs); - val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); - val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); - val cases_pred_attr = Attrib.internal o K o Induct.cases_pred; in - (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) + (thm, [Attrib.case_names ctr_names, Attrib.consumes 1] @ @{attributes [cases pred]}) end; val case_transfer_thm = derive_case_transfer rel_case_thm; @@ -1395,12 +1390,8 @@ else funpow nn (fn thm => unfold_thms ctxt @{thms conj_assoc} (thm RS prop_conj)) thm)); fun mk_induct_attrs ctrss = - let - val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); - val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases)); - in - [induct_case_names_attr] - end; + let val induct_cases = quasi_unambiguous_case_names (maps (map name_of_ctr) ctrss); + in [Attrib.case_names induct_cases] end; fun derive_rel_induct_thms_for_types lthy nn fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs = @@ -1611,17 +1602,13 @@ val coinduct_conclss = @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; - val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); - - val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases)); + val coinduct_case_names_attr = Attrib.case_names coinduct_cases; val coinduct_case_concl_attrs = - map2 (fn casex => fn concls => - Attrib.internal (K (Rule_Cases.case_conclusion (casex, concls)))) + map2 (fn casex => fn concls => Attrib.case_conclusion (casex, concls)) coinduct_cases coinduct_conclss; val common_coinduct_attrs = coinduct_case_names_attr :: coinduct_case_concl_attrs; - val coinduct_attrs = - coinduct_consumes_attr :: coinduct_case_names_attr :: coinduct_case_concl_attrs; + val coinduct_attrs = Attrib.consumes 1 :: coinduct_case_names_attr :: coinduct_case_concl_attrs; in (coinduct_attrs, common_coinduct_attrs) end; @@ -1776,13 +1763,12 @@ exhausts set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses) |> Thm.close_derivation; - val case_names_attr = - Attrib.internal (K (Rule_Cases.case_names (quasi_unambiguous_case_names case_names))); + val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names); val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets; in (thm, case_names_attr :: induct_set_attrs) end - val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); + val consumes_attr = Attrib.consumes 1; in map (mk_thm lthy fpTs ctrss #> nn = 1 ? map_prod (fn thm => rotate_prems ~1 (thm RS bspec)) (cons consumes_attr)) diff -r 00f4461fa99f -r 80ef19b51493 src/HOL/Tools/Function/function.ML --- a/src/HOL/Tools/Function/function.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/HOL/Tools/Function/function.ML Mon Apr 18 20:24:19 2016 +0200 @@ -50,9 +50,8 @@ val psimp_attribs = @{attributes [nitpick_psimp]} -fun note_qualified suffix attrs (fname, thms) = - Local_Theory.note ((derived_name fname suffix, map (Attrib.internal o K) attrs), thms) - #> apfst snd +fun note_derived (a, atts) (fname, thms) = + Local_Theory.note ((derived_name fname a, atts), thms) #> apfst snd fun add_simps fnames post sort extra_qualify label mod_binding moreatts simps lthy = let @@ -107,15 +106,14 @@ "psimps" concealed_partial psimp_attribs psimps ||>> Local_Theory.notes [((concealed_partial (derived_name defname "pinduct"), []), simple_pinducts |> map (fn th => ([th], - [Attrib.internal (K (Rule_Cases.case_names cnames)), - Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), - Attrib.internal (K (Induct.induct_pred ""))])))] + [Attrib.case_names cnames, Attrib.consumes (1 - Thm.nprems_of th)] @ + @{attributes [induct pred]})))] ||>> (apfst snd o Local_Theory.note ((Binding.concealed (derived_name defname "termination"), []), [termination])) - ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) - (fnames ~~ map single cases) (* TODO: case names *) - ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) + ||>> fold_map (note_derived ("cases", [Attrib.case_names cnames])) + (fnames ~~ map single cases) + ||>> fold_map (note_derived ("pelims", [Attrib.consumes 1, Attrib.constraints 1])) (fnames ~~ pelims) ||> (case domintros of NONE => I | SOME thms => Local_Theory.note ((derived_name defname "domintros", []), thms) #> snd) @@ -198,9 +196,8 @@ lthy |> add_simps I "simps" I simp_attribs tsimps ||>> Local_Theory.note - ((derived_name defname "induct", [Attrib.internal (K (Rule_Cases.case_names case_names))]), - tinduct) - ||>> fold_map (note_qualified "elims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) + ((derived_name defname "induct", [Attrib.case_names case_names]), tinduct) + ||>> fold_map (note_derived ("elims", [Attrib.consumes 1, Attrib.constraints 1])) (fnames ~~ telims) |-> (fn ((simps,(_,inducts)), elims) => fn lthy => let val info' = { is_partial=false, defname=defname, fnames=fnames, add_simps=add_simps, diff -r 00f4461fa99f -r 80ef19b51493 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/HOL/Tools/inductive.ML Mon Apr 18 20:24:19 2016 +0200 @@ -898,23 +898,19 @@ val intr_names = map Binding.name_of intr_bindings; val ind_case_names = if forall (equal "") intr_names then [] - else [Attrib.internal (K (Rule_Cases.case_names intr_names))]; + else [Attrib.case_names intr_names]; val induct = if coind then (raw_induct, - map (Attrib.internal o K) - [Rule_Cases.case_names [rec_name], - Rule_Cases.case_conclusion (rec_name, intr_names), - Rule_Cases.consumes (1 - Thm.nprems_of raw_induct), - Induct.coinduct_pred (hd cnames)]) + [Attrib.case_names [rec_name], + Attrib.case_conclusion (rec_name, intr_names), + Attrib.consumes (1 - Thm.nprems_of raw_induct), + Attrib.internal (K (Induct.coinduct_pred (hd cnames)))]) else if no_ind orelse length cnames > 1 then - (raw_induct, - ind_case_names @ - [Attrib.internal (K (Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))))]) + (raw_induct, ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))]) else (raw_induct RSN (2, rev_mp), - ind_case_names @ - [Attrib.internal (K (Rule_Cases.consumes (~ (Thm.nprems_of raw_induct))))]); + ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))]); val (intrs', lthy1) = lthy |> @@ -922,8 +918,7 @@ (if coind then Spec_Rules.Co_Inductive else Spec_Rules.Inductive) (preds, intrs) |> Local_Theory.notes (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ - map (fn th => [([th], - [Attrib.internal (K (Context_Rules.intro_query NONE))])]) intrs) |>> + map (fn th => [([th], @{attributes [Pure.intro?]})]) intrs) |>> map (hd o snd); val (((_, elims'), (_, [induct'])), lthy2) = lthy1 |> @@ -931,12 +926,10 @@ fold_map (fn (name, (elim, cases, k)) => Local_Theory.note ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"), - map (Attrib.internal o K) - ((if forall (equal "") cases then [] else [Rule_Cases.case_names cases]) @ - [Rule_Cases.consumes (1 - Thm.nprems_of elim), - Rule_Cases.constraints k, - Induct.cases_pred name, - Context_Rules.elim_query NONE])), [elim]) #> + ((if forall (equal "") cases then [] else [Attrib.case_names cases]) @ + [Attrib.consumes (1 - Thm.nprems_of elim), Attrib.constraints k, + Attrib.internal (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})), + [elim]) #> apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>> Local_Theory.note ((rec_qualified true (Binding.name (coind_prefix coind ^ "induct")), #2 induct), @@ -956,7 +949,7 @@ Local_Theory.notes [((rec_qualified true (Binding.name "inducts"), []), inducts |> map (fn (name, th) => ([th], ind_case_names @ - [Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))), + [Attrib.consumes (1 - Thm.nprems_of th), Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd end; in (intrs', elims', eqs', induct', inducts, lthy4) end; diff -r 00f4461fa99f -r 80ef19b51493 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/HOL/Tools/typedef.ML Mon Apr 18 20:24:19 2016 +0200 @@ -240,8 +240,7 @@ (* result *) fun note ((b, atts), th) = - Local_Theory.note ((b, map (Attrib.internal o K) atts), [th]) - #>> (fn (_, [th']) => th'); + Local_Theory.note ((b, atts), [th]) #>> (fn (_, [th']) => th'); fun typedef_result inhabited lthy1 = let @@ -260,16 +259,20 @@ ||>> note ((Binding.suffix_name "_inject" Abs_name, []), make @{thm type_definition.Abs_inject}) ||>> note ((Binding.suffix_name "_cases" Rep_name, - [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]), + [Attrib.case_names [Binding.name_of Rep_name], + Attrib.internal (K (Induct.cases_pred full_name))]), make @{thm type_definition.Rep_cases}) ||>> note ((Binding.suffix_name "_cases" Abs_name, - [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]), + [Attrib.case_names [Binding.name_of Abs_name], + Attrib.internal (K (Induct.cases_type full_name))]), make @{thm type_definition.Abs_cases}) ||>> note ((Binding.suffix_name "_induct" Rep_name, - [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]), + [Attrib.case_names [Binding.name_of Rep_name], + Attrib.internal (K (Induct.induct_pred full_name))]), make @{thm type_definition.Rep_induct}) ||>> note ((Binding.suffix_name "_induct" Abs_name, - [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]), + [Attrib.case_names [Binding.name_of Abs_name], + Attrib.internal (K (Induct.induct_type full_name))]), make @{thm type_definition.Abs_induct}); val info = diff -r 00f4461fa99f -r 80ef19b51493 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/Pure/Isar/attrib.ML Mon Apr 18 20:24:19 2016 +0200 @@ -78,6 +78,11 @@ val setup_option_int: string * Position.T -> int Config.T val setup_option_real: string * Position.T -> real Config.T val setup_option_string: string * Position.T -> string Config.T + val consumes: int -> Token.src + val constraints: int -> Token.src + val cases_open: Token.src + val case_names: string list -> Token.src + val case_conclusion: string * string list -> Token.src end; structure Attrib: ATTRIB = @@ -235,15 +240,21 @@ (* internal attribute *) -fun internal att = - Token.make_src ("Pure.attribute", Position.none) - [Token.make_string ("", Position.none) |> Token.assign (SOME (Token.Attribute att))]; - val _ = Theory.setup (setup (Binding.make ("attribute", @{here})) (Scan.lift Args.internal_attribute >> Morphism.form) "internal attribute"); +fun internal_name ctxt name = + Token.make_src (name, Position.none) [] |> check_src ctxt |> hd; + +val internal_attribute_name = + internal_name (Context.the_local_context ()) "attribute"; + +fun internal att = + internal_attribute_name :: + [Token.make_string ("", Position.none) |> Token.assign (SOME (Token.Attribute att))]; + (* add/del syntax *) @@ -528,8 +539,11 @@ setup @{binding constraints} (Scan.lift Parse.nat >> Rule_Cases.constraints) "number of equality constraints" #> + setup @{binding cases_open} + (Scan.succeed Rule_Cases.cases_open) + "rule with open parameters" #> setup @{binding case_names} - (Scan.lift (Scan.repeat1 (Args.name -- + (Scan.lift (Scan.repeat (Args.name -- Scan.optional (Parse.$$$ "[" |-- Scan.repeat1 (Args.maybe Args.name) --| Parse.$$$ "]") [])) >> (fn cs => Rule_Cases.cases_hyp_names @@ -607,4 +621,29 @@ register_config Raw_Simplifier.simp_debug_raw #> register_config Raw_Simplifier.simp_trace_raw); + +(* internal source *) + +local + +val internal = internal_name (Context.the_local_context ()); + +val consumes_name = internal "consumes"; +val constraints_name = internal "constraints"; +val cases_open_name = internal "cases_open"; +val case_names_name = internal "case_names"; +val case_conclusion_name = internal "case_conclusion"; + +fun make_string s = Token.make_string (s, Position.none); + +in + +fun consumes i = consumes_name :: Token.make_int i; +fun constraints i = constraints_name :: Token.make_int i; +val cases_open = [cases_open_name]; +fun case_names names = case_names_name :: map make_string names; +fun case_conclusion (name, names) = case_conclusion_name :: map make_string (name :: names); + end; + +end; \ No newline at end of file diff -r 00f4461fa99f -r 80ef19b51493 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/Pure/Isar/obtain.ML Mon Apr 18 20:24:19 2016 +0200 @@ -8,6 +8,7 @@ sig val obtain_thesis: Proof.context -> ((string * typ) * term) * Proof.context val obtains_attributes: ('typ, 'term) Element.obtain list -> attribute list + val obtains_attribs: ('typ, 'term) Element.obtain list -> Token.src list val read_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list val cert_obtains: Proof.context -> term -> Element.obtains_i -> (binding * term) list val parse_obtains: Proof.context -> term -> Element.obtains -> (binding * term) list @@ -70,11 +71,15 @@ (* result declaration *) -fun obtains_attributes (obtains: ('typ, 'term) Element.obtain list) = - let - val case_names = obtains |> map_index (fn (i, (b, _)) => - if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b); - in [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names case_names] end; +fun case_names (obtains: ('typ, 'term) Element.obtain list) = + obtains |> map_index (fn (i, (b, _)) => + if Binding.is_empty b then string_of_int (i + 1) else Name_Space.base_name b); + +fun obtains_attributes obtains = + [Rule_Cases.consumes (~ (length obtains)), Rule_Cases.case_names (case_names obtains)]; + +fun obtains_attribs obtains = + [Attrib.consumes (~ (length obtains)), Attrib.case_names (case_names obtains)]; (* obtain thesis *) diff -r 00f4461fa99f -r 80ef19b51493 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/Pure/Isar/specification.ML Mon Apr 18 20:24:19 2016 +0200 @@ -376,9 +376,8 @@ val ([(_, that')], that_ctxt) = asms_ctxt |> Proof_Context.note_thmss "" [((Binding.name Auto_Bind.thatN, []), [(that, [])])]; - val more_atts = map (Attrib.internal o K) (Obtain.obtains_attributes raw_obtains); val stmt' = [((Binding.empty, []), [(#2 (#1 (Obtain.obtain_thesis ctxt)), [])])]; - in ((more_atts, prems, stmt', SOME that'), that_ctxt) end) + in ((Obtain.obtains_attribs raw_obtains, prems, stmt', SOME that'), that_ctxt) end) end; fun gen_theorem schematic bundle_includes prep_att prep_stmt diff -r 00f4461fa99f -r 80ef19b51493 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Mon Apr 18 15:51:48 2016 +0100 +++ b/src/Pure/Isar/token.ML Mon Apr 18 20:24:19 2016 +0200 @@ -93,6 +93,7 @@ val explode: Keyword.keywords -> Position.T -> string -> T list val make: (int * int) * string -> Position.T -> T * Position.T val make_string: string * Position.T -> T + val make_int: int -> T list val make_src: string * Position.T -> T list -> src type 'a parser = T list -> 'a * T list type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) @@ -675,6 +676,8 @@ val pos' = Position.no_range_position pos; in Token ((x, (pos', pos')), y, z) end; +val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int; + fun make_src a args = make_string a :: args;