--- a/src/Doc/Isar_Ref/Proof.thy Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Apr 18 22:51:32 2016 +0200
@@ -970,7 +970,7 @@
@{rail \<open>
@@{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} * )
;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Apr 18 22:51:32 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))
--- a/src/HOL/Tools/Function/function.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/HOL/Tools/Function/function.ML Mon Apr 18 22:51:32 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,
--- a/src/HOL/Tools/inductive.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/HOL/Tools/inductive.ML Mon Apr 18 22:51:32 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;
--- a/src/HOL/Tools/typedef.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/HOL/Tools/typedef.ML Mon Apr 18 22:51:32 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 =
--- a/src/Pure/Isar/attrib.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/Isar/attrib.ML Mon Apr 18 22:51:32 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 ("<attribute>", 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 ("<attribute>", 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
--- a/src/Pure/Isar/obtain.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/Isar/obtain.ML Mon Apr 18 22:51:32 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 *)
--- a/src/Pure/Isar/specification.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/Isar/specification.ML Mon Apr 18 22:51:32 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
--- a/src/Pure/Isar/token.ML Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/Isar/token.ML Mon Apr 18 22:51:32 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;
--- a/src/Pure/PIDE/document.scala Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/PIDE/document.scala Mon Apr 18 22:51:32 2016 +0200
@@ -81,9 +81,9 @@
/* header and name */
sealed case class Header(
- imports: List[(Name, Position.T)],
- keywords: Thy_Header.Keywords,
- errors: List[String])
+ imports: List[(Name, Position.T)] = Nil,
+ keywords: Thy_Header.Keywords = Nil,
+ errors: List[String] = Nil)
{
def error(msg: String): Header = copy(errors = errors ::: List(msg))
@@ -91,8 +91,8 @@
copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
}
- val no_header = Header(Nil, Nil, Nil)
- def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
+ val no_header = Header()
+ def bad_header(msg: String): Header = Header(errors = List(msg))
object Name
{
--- a/src/Pure/PIDE/resources.scala Mon Apr 18 16:50:19 2016 +0100
+++ b/src/Pure/PIDE/resources.scala Mon Apr 18 22:51:32 2016 +0200
@@ -103,7 +103,7 @@
val imports =
header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
- Document.Node.Header(imports, header.keywords, Nil)
+ Document.Node.Header(imports, header.keywords)
}
catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
}