clarified check_open_spec / read_open_spec;
allow 'for' fixes in 'abbreviation', 'definition';
--- a/NEWS Sat May 28 23:55:41 2016 +0200
+++ b/NEWS Sun May 29 15:40:25 2016 +0200
@@ -66,14 +66,14 @@
*** Isar ***
-* Many specification elements support structured statements with 'if'
-eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
-'function'.
-
* Command 'axiomatization' has become more restrictive to correspond
better to internal axioms as singleton facts with mandatory name. Minor
INCOMPATIBILITY.
+* Many specification elements support structured statements with 'if' /
+'for' eigen-context, e.g. 'axiomatization', 'abbreviation',
+'definition', 'inductive', 'function'.
+
* Toplevel theorem statements support eigen-context notation with 'if' /
'for' (in postix), which corresponds to 'assumes' / 'fixes' in the
traditional long statement form (in prefix). Local premises are called
--- a/src/Doc/Isar_Ref/Spec.thy Sat May 28 23:55:41 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Sun May 29 15:40:25 2016 +0200
@@ -285,14 +285,19 @@
``abbreviation''.
@{rail \<open>
- @@{command definition} (decl @'where')? @{syntax thmdecl}? @{syntax prop}
+ @@{command definition} decl? definition
;
- @@{command abbreviation} @{syntax mode}? \<newline>
- (decl @'where')? @{syntax prop}
- ;
- decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
+ @@{command abbreviation} @{syntax mode}? decl? abbreviation
;
@@{command print_abbrevs} ('!'?)
+ ;
+ decl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}? @'where'
+ ;
+ definition: @{syntax thmdecl}? @{syntax prop} prems @{syntax for_fixes}
+ ;
+ prems: (@'if' ((@{syntax prop}+) + @'and'))?
+ ;
+ abbreviation: @{syntax prop} @{syntax for_fixes}
\<close>}
\<^descr> \<^theory_text>\<open>definition c where eq\<close> produces an internal definition \<open>c \<equiv> t\<close> according
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun May 29 15:40:25 2016 +0200
@@ -175,7 +175,7 @@
Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))))
val ((_, (_, below_ldef)), lthy) = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort po})
- |> Specification.definition NONE []
+ |> Specification.definition NONE [] []
((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun May 29 15:40:25 2016 +0200
@@ -138,17 +138,17 @@
val lthy = thy
|> Class.instantiation ([full_tname], lhs_tfrees, @{sort domain})
val ((_, (_, emb_ldef)), lthy) =
- Specification.definition NONE [] (emb_bind, emb_eqn) lthy
+ Specification.definition NONE [] [] (emb_bind, emb_eqn) lthy
val ((_, (_, prj_ldef)), lthy) =
- Specification.definition NONE [] (prj_bind, prj_eqn) lthy
+ Specification.definition NONE [] [] (prj_bind, prj_eqn) lthy
val ((_, (_, defl_ldef)), lthy) =
- Specification.definition NONE [] (defl_bind, defl_eqn) lthy
+ Specification.definition NONE [] [] (defl_bind, defl_eqn) lthy
val ((_, (_, liftemb_ldef)), lthy) =
- Specification.definition NONE [] (liftemb_bind, liftemb_eqn) lthy
+ Specification.definition NONE [] [] (liftemb_bind, liftemb_eqn) lthy
val ((_, (_, liftprj_ldef)), lthy) =
- Specification.definition NONE [] (liftprj_bind, liftprj_eqn) lthy
+ Specification.definition NONE [] [] (liftprj_bind, liftprj_eqn) lthy
val ((_, (_, liftdefl_ldef)), lthy) =
- Specification.definition NONE [] (liftdefl_bind, liftdefl_eqn) lthy
+ Specification.definition NONE [] [] (liftdefl_bind, liftdefl_eqn) lthy
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
val emb_def = singleton (Proof_Context.export lthy ctxt_thy) emb_ldef
val prj_def = singleton (Proof_Context.export lthy ctxt_thy) prj_ldef
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sun May 29 15:40:25 2016 +0200
@@ -1020,7 +1020,7 @@
"\ndoes not match type " ^ ty' ^ " in definition");
val id' = mk_rulename id;
val ((t', (_, th)), lthy') = Named_Target.theory_init thy
- |> Specification.definition NONE []
+ |> Specification.definition NONE [] []
((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq (Free (s, T), t)));
val phi =
Proof_Context.export_morphism lthy'
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Sun May 29 15:40:25 2016 +0200
@@ -623,11 +623,11 @@
else if Binding.eq_name (b, equal_binding) then
pair (Term.lambda u exist_xs_u_eq_ctr, refl)
else
- Specification.definition (SOME (b, NONE, NoSyn)) []
+ Specification.definition (SOME (b, NONE, NoSyn)) [] []
((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr) #>> apsnd snd)
ks exist_xs_u_eq_ctrs disc_bindings
||>> apfst split_list o fold_map (fn (b, proto_sels) =>
- Specification.definition (SOME (b, NONE, NoSyn)) []
+ Specification.definition (SOME (b, NONE, NoSyn)) [] []
((Thm.def_binding b, []), sel_spec b proto_sels) #>> apsnd snd) sel_infos
||> `Local_Theory.close_target;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Sun May 29 15:40:25 2016 +0200
@@ -93,7 +93,7 @@
mk_Trueprop_eq (mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})
|> Syntax.check_term lthy;
val ((_, (_, raw_def)), lthy') =
- Specification.definition NONE [] (Attrib.empty_binding, spec) lthy;
+ Specification.definition NONE [] [] (Attrib.empty_binding, spec) lthy;
val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy');
val def = singleton (Proof_Context.export lthy' thy_ctxt) raw_def;
in
--- a/src/HOL/Tools/Lifting/lifting_setup.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sun May 29 15:40:25 2016 +0200
@@ -89,7 +89,7 @@
val rhs = relcomp_op $ param_rel_fixed $ fixed_crel
val definition_term = Logic.mk_equals (lhs, rhs)
fun note_def lthy =
- Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) []
+ Specification.definition (SOME (pcrel_name, SOME relator_type, NoSyn)) [] []
((Binding.empty, []), definition_term) lthy |>> (snd #> snd);
fun raw_def lthy =
let
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun May 29 15:40:25 2016 +0200
@@ -56,7 +56,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort partial_term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun May 29 15:40:25 2016 +0200
@@ -266,7 +266,7 @@
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
- Specification.definition NONE []
+ Specification.definition NONE [] []
((Binding.concealed Binding.empty, []), random_def)) random_defs')
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
--- a/src/HOL/Tools/code_evaluation.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML Sun May 29 15:40:25 2016 +0200
@@ -43,7 +43,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.name (triv_name_of eq), []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
--- a/src/HOL/Tools/inductive.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/inductive.ML Sun May 29 15:40:25 2016 +0200
@@ -610,7 +610,7 @@
fun ind_cases_rules ctxt raw_props raw_fixes =
let
- val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
+ val (props, ctxt') = Specification.read_props raw_props raw_fixes ctxt;
val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
in rules end;
--- a/src/HOL/Tools/record.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/record.ML Sun May 29 15:40:25 2016 +0200
@@ -1734,7 +1734,7 @@
thy
|> Class.instantiation ([tyco], vs, sort)
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] ((Binding.concealed Binding.empty, []), eq))
+ |-> (fn eq => Specification.definition NONE [] [] ((Binding.concealed Binding.empty, []), eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
@@ -1781,7 +1781,7 @@
|> fold Code.add_default_eqn simps
|> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
|-> (fn (_, (_, eq_def)) =>
Class.prove_instantiation_exit_result Morphism.thm tac eq_def)
|-> (fn eq_def => fn thy =>
--- a/src/HOL/Typerep.thy Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Typerep.thy Sun May 29 15:40:25 2016 +0200
@@ -58,7 +58,7 @@
thy
|> Class.instantiation ([tyco], vs, @{sort typerep})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition NONE [] (Attrib.empty_binding, eq))
+ |-> (fn eq => Specification.definition NONE [] [] (Attrib.empty_binding, eq))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
--- a/src/Pure/Isar/parse_spec.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Isar/parse_spec.ML Sun May 29 15:40:25 2016 +0200
@@ -12,7 +12,6 @@
val simple_spec: (Attrib.binding * string) parser
val simple_specs: (Attrib.binding * string list) parser
val if_assumes: string list parser
- val spec: (string list * (Attrib.binding * string)) parser
val multi_specs: Specification.multi_specs_cmd parser
val where_multi_specs: Specification.multi_specs_cmd parser
val constdecl: (binding * string option * mixfix) parser
@@ -59,8 +58,6 @@
Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat))
[];
-val spec = (opt_thm_name ":" -- Parse.prop) -- if_assumes >> swap;
-
val multi_specs =
Parse.enum1 "|"
(opt_thm_name ":" -- Parse.prop -- if_assumes --|
--- a/src/Pure/Isar/specification.ML Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Isar/specification.ML Sun May 29 15:40:25 2016 +0200
@@ -11,14 +11,14 @@
term list * Proof.context
val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
term * Proof.context
- val check_spec: (binding * typ option * mixfix) list ->
- term list -> Attrib.binding * term -> Proof.context ->
- ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
- * Proof.context
- val read_spec: (binding * string option * mixfix) list ->
- string list -> Attrib.binding * string -> Proof.context ->
- ((((binding * typ) * mixfix) list * (Attrib.binding * term)) * (string -> Position.T))
- * Proof.context
+ val check_spec_open: (binding * typ option * mixfix) list ->
+ (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
+ ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+ Proof.context
+ val read_spec_open: (binding * string option * mixfix) list ->
+ (binding * string option * mixfix) list -> string list -> string -> Proof.context ->
+ ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
+ Proof.context
type multi_specs = ((Attrib.binding * term) * term list) list
type multi_specs_cmd = ((Attrib.binding * string) * string list) list
val check_multi_specs: (binding * typ option * mixfix) list -> multi_specs -> Proof.context ->
@@ -32,16 +32,19 @@
(binding * string option * mixfix) list -> string list ->
(Attrib.binding * string) list -> theory -> (term list * thm list) * theory
val axiom: Attrib.binding * term -> theory -> thm * theory
- val definition: (binding * typ option * mixfix) option -> term list ->
- Attrib.binding * term -> local_theory -> (term * (string * thm)) * local_theory
- val definition': (binding * typ option * mixfix) option -> term list ->
- Attrib.binding * term -> bool -> local_theory -> (term * (string * thm)) * local_theory
- val definition_cmd: (binding * string option * mixfix) option -> string list ->
- Attrib.binding * string -> bool -> local_theory -> (term * (string * thm)) * local_theory
- val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option -> term ->
- bool -> local_theory -> local_theory
- val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option -> string ->
- bool -> local_theory -> local_theory
+ val definition: (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
+ local_theory -> (term * (string * thm)) * local_theory
+ val definition': (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term list -> Attrib.binding * term ->
+ bool -> local_theory -> (term * (string * thm)) * local_theory
+ val definition_cmd: (binding * string option * mixfix) option ->
+ (binding * string option * mixfix) list -> string list -> Attrib.binding * string ->
+ bool -> local_theory -> (term * (string * thm)) * local_theory
+ val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option ->
+ (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
+ val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
+ (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
local_theory -> local_theory
@@ -96,14 +99,30 @@
local
-fun close_form ctxt auto_close prems concl =
- if not auto_close andalso null prems then concl
- else
- let
- val xs =
- if auto_close then rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) [])
- else [];
- in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
+fun prep_decls prep_var raw_vars ctxt =
+ let
+ val (vars, ctxt') = fold_map prep_var raw_vars ctxt;
+ val (xs, ctxt'') = ctxt'
+ |> Context_Position.set_visible false
+ |> Proof_Context.add_fixes vars
+ ||> Context_Position.restore_visible ctxt';
+ val _ =
+ Context_Position.reports ctxt''
+ (map (Binding.pos_of o #1) vars ~~
+ map (Variable.markup_entity_def ctxt'' ##> Properties.remove Markup.kindN) xs);
+ in ((vars, xs), ctxt'') end;
+
+fun close_form ctxt prems concl =
+ let val xs = rev (fold (Variable.add_free_names ctxt) (prems @ [concl]) []);
+ in Logic.close_prop_constraint (Variable.default_type ctxt) (xs ~~ xs) prems concl end;
+
+fun dummy_frees ctxt xs tss =
+ let
+ val names =
+ Variable.names_of ((fold o fold) Variable.declare_term tss ctxt)
+ |> fold Name.declare xs;
+ val (tss', _) = (fold_map o fold_map) Term.free_dummy_patterns tss names;
+ in tss' end;
fun get_positions ctxt x =
let
@@ -118,60 +137,58 @@
| get _ _ = [];
in get [] end;
-fun prep_specs prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
+fun prep_spec_open prep_var parse_prop raw_vars raw_params raw_prems raw_concl ctxt =
let
- val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
- val (xs, params_ctxt) = vars_ctxt
- |> Context_Position.set_visible false
- |> Proof_Context.add_fixes vars
- ||> Context_Position.restore_visible vars_ctxt;
- val _ =
- Context_Position.reports params_ctxt
- (map (Binding.pos_of o #1) vars ~~
- map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
+ val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
+ val (ys, params_ctxt) = vars_ctxt |> fold_map prep_var raw_params |-> Proof_Context.add_fixes;
+
+ val props =
+ map (parse_prop params_ctxt) (raw_concl :: raw_prems)
+ |> singleton (dummy_frees params_ctxt (xs @ ys));
+
+ val concl :: prems = Syntax.check_props params_ctxt props;
+ val spec = Logic.list_implies (prems, concl);
+ val spec_ctxt = Variable.declare_term spec params_ctxt;
+
+ fun get_pos x =
+ (case maps (get_positions spec_ctxt x) props of
+ [] => Position.none
+ | pos :: _ => pos);
+ in ((vars, xs, get_pos, spec), spec_ctxt) end;
+
+fun prep_specs prep_var parse_prop prep_att raw_vars raw_specss ctxt =
+ let
+ val ((vars, xs), vars_ctxt) = prep_decls prep_var raw_vars ctxt;
val propss0 =
map (fn ((_, raw_concl), raw_prems) => raw_concl :: raw_prems) raw_specss
- |> burrow (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
- val names =
- Variable.names_of (params_ctxt |> (fold o fold) Variable.declare_term propss0)
- |> fold Name.declare xs;
+ |> burrow (grouped 10 Par_List.map_independent (parse_prop vars_ctxt));
val props =
- (fold_map o fold_map) Term.free_dummy_patterns propss0 names
- |> fst |> map (fn concl :: prems => close_form params_ctxt auto_close prems concl);
+ dummy_frees vars_ctxt xs propss0
+ |> map (fn concl :: prems => close_form vars_ctxt prems concl);
- val specs = Syntax.check_props params_ctxt props;
- val specs_ctxt = params_ctxt |> fold Variable.declare_term specs;
+ val specs = Syntax.check_props vars_ctxt props;
+ val specs_ctxt = vars_ctxt |> fold Variable.declare_term specs;
val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
val name_atts: Attrib.binding list =
map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (map #1 raw_specss);
-
- fun get_pos x =
- (case maps (get_positions specs_ctxt x) props of
- [] => Position.none
- | pos :: _ => pos);
- in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
+ in ((params, name_atts ~~ specs), specs_ctxt) end;
in
-fun check_spec xs As B =
- prep_specs Proof_Context.cert_var (K I) (K I) false xs [(B, As)] #>
- (apfst o apfst o apsnd) the_single;
-
-fun read_spec xs As B =
- prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src false xs [(B, As)] #>
- (apfst o apfst o apsnd) the_single;
+val check_spec_open = prep_spec_open Proof_Context.cert_var (K I);
+val read_spec_open = prep_spec_open Proof_Context.read_var Syntax.parse_prop;
type multi_specs = ((Attrib.binding * term) * term list) list;
type multi_specs_cmd = ((Attrib.binding * string) * string list) list;
fun check_multi_specs xs specs =
- prep_specs Proof_Context.cert_var (K I) (K I) true xs specs #>> #1;
+ prep_specs Proof_Context.cert_var (K I) (K I) xs specs;
fun read_multi_specs xs specs =
- prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src true xs specs #>> #1;
+ prep_specs Proof_Context.read_var Syntax.parse_prop Attrib.check_src xs specs;
end;
@@ -219,23 +236,23 @@
(* definition *)
-fun gen_def prep raw_var raw_prems raw_spec int lthy =
+fun gen_def prep_spec prep_att raw_var raw_params raw_prems ((a, raw_atts), raw_spec) int lthy =
let
- val ((vars, ((raw_name, atts), prop)), get_pos) =
- fst (prep (the_list raw_var) raw_prems raw_spec lthy);
- val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
+ val atts = map (prep_att lthy) raw_atts;
+
+ val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ |> prep_spec (the_list raw_var) raw_params raw_prems raw_spec;
+ val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} spec;
val _ = Name.reject_internal (x, []);
val (b, mx) =
- (case vars of
- [] => (Binding.make (x, get_pos x), NoSyn)
- | [((b, _), mx)] =>
- let
- val y = Variable.check_name b;
- val _ = x = y orelse
- error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.here (Binding.pos_of b));
- in (b, mx) end);
- val name = Thm.def_binding_optional b raw_name;
+ (case (vars, xs) of
+ ([], []) => (Binding.make (x, get_pos x), NoSyn)
+ | ([(b, _, mx)], [y]) =>
+ if x = y then (b, mx)
+ else
+ error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.here (Binding.pos_of b)));
+ val name = Thm.def_binding_optional b a;
val ((lhs, (_, raw_th)), lthy2) = lthy
|> Local_Theory.define_internal ((b, mx), ((Binding.suffix_name "_raw" name, []), rhs));
@@ -252,32 +269,29 @@
(member (op =) (Term.add_frees lhs' [])) [(x, T)];
in ((lhs, (def_name, th')), lthy4) end;
-val definition' = gen_def check_spec;
-fun definition xs As B = definition' xs As B false;
-val definition_cmd = gen_def read_spec;
+val definition' = gen_def check_spec_open (K I);
+fun definition xs ys As B = definition' xs ys As B false;
+val definition_cmd = gen_def read_spec_open Attrib.check_src;
(* abbreviation *)
-fun gen_abbrev prep mode raw_var raw_prop int lthy =
+fun gen_abbrev prep_spec mode raw_var raw_params raw_spec int lthy =
let
- val lthy1 = lthy
- |> Proof_Context.set_syntax_mode mode;
- val (((vars, (_, prop)), get_pos), _) =
- prep (the_list raw_var) [] (Attrib.empty_binding, raw_prop)
- (lthy1 |> Proof_Context.set_mode Proof_Context.mode_abbrev);
- val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 prop));
+ val lthy1 = lthy |> Proof_Context.set_syntax_mode mode;
+ val ((vars, xs, get_pos, spec), spec_ctxt) = lthy
+ |> Proof_Context.set_mode Proof_Context.mode_abbrev
+ |> prep_spec (the_list raw_var) raw_params [] raw_spec;
+ val ((x, T), rhs) = Local_Defs.abs_def (#2 (Local_Defs.cert_def lthy1 spec));
val _ = Name.reject_internal (x, []);
val (b, mx) =
- (case vars of
- [] => (Binding.make (x, get_pos x), NoSyn)
- | [((b, _), mx)] =>
- let
- val y = Variable.check_name b;
- val _ = x = y orelse
- error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
- Position.here (Binding.pos_of b));
- in (b, mx) end);
+ (case (vars, xs) of
+ ([], []) => (Binding.make (x, get_pos x), NoSyn)
+ | ([(b, _, mx)], [y]) =>
+ if x = y then (b, mx)
+ else
+ error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
+ Position.here (Binding.pos_of b)));
val lthy2 = lthy1
|> Local_Theory.abbrev mode ((b, mx), rhs) |> snd
|> Proof_Context.restore_syntax_mode lthy;
@@ -285,8 +299,8 @@
val _ = Proof_Display.print_consts int (Position.thread_data ()) lthy2 (K false) [(x, T)];
in lthy2 end;
-val abbreviation = gen_abbrev check_spec;
-val abbreviation_cmd = gen_abbrev read_spec;
+val abbreviation = gen_abbrev check_spec_open;
+val abbreviation_cmd = gen_abbrev read_spec_open;
(* notation *)
--- a/src/Pure/Pure.thy Sat May 28 23:55:41 2016 +0200
+++ b/src/Pure/Pure.thy Sun May 29 15:40:25 2016 +0200
@@ -343,13 +343,14 @@
val _ =
Outer_Syntax.local_theory' @{command_keyword definition} "constant definition"
- (Scan.option Parse_Spec.constdecl -- Parse_Spec.spec
- >> (fn (a, (b, c)) => #2 oo Specification.definition_cmd a b c));
+ (Scan.option Parse_Spec.constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop) --
+ Parse_Spec.if_assumes -- Parse.for_fixes >> (fn (((decl, spec), prems), params) =>
+ #2 oo Specification.definition_cmd decl params prems spec));
val _ =
Outer_Syntax.local_theory' @{command_keyword abbreviation} "constant abbreviation"
- (Parse.syntax_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
- >> (fn (mode, (a, b)) => Specification.abbreviation_cmd mode a b));
+ (Parse.syntax_mode -- Scan.option Parse_Spec.constdecl -- Parse.prop -- Parse.for_fixes
+ >> (fn (((mode, decl), spec), params) => Specification.abbreviation_cmd mode decl params spec));
val axiomatization =
Parse.and_list1 (Parse_Spec.thm_name ":" -- Parse.prop) --