--- a/NEWS Mon Jul 03 09:57:26 2017 +0200
+++ b/NEWS Mon Jul 03 13:51:55 2017 +0200
@@ -62,6 +62,10 @@
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
+* Commands 'alias' and 'type_alias' introduce aliases for constants and
+type constructors, respectively. This allows adhoc changes to name-space
+accesses within global or local theory contexts, e.g. within a 'bundle'.
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Spec.thy Mon Jul 03 09:57:26 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Jul 03 13:51:55 2017 +0200
@@ -1311,6 +1311,8 @@
text \<open>
\begin{matharray}{rcl}
+ @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
@@ -1318,8 +1320,10 @@
\end{matharray}
@{rail \<open>
- ( @{command hide_class} | @{command hide_type} |
- @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
+ (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
+ ;
+ (@{command hide_class} | @{command hide_type} |
+ @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
\<close>}
Isabelle organizes any kind of name declarations (of types, constants,
@@ -1327,6 +1331,12 @@
the user does not have to control the behaviour of name spaces by hand, yet
the following commands provide some way to do so.
+ \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
+ constructors, respectively. This allows adhoc changes to name-space
+ accesses.
+
+ \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
+
\<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.
--- a/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 09:57:26 2017 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy Mon Jul 03 13:51:55 2017 +0200
@@ -17,7 +17,7 @@
"primcorec" :: thy_decl
begin
-setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
+alias proj = Equiv_Relations.proj
lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
by simp
--- a/src/Pure/Isar/specification.ML Mon Jul 03 09:57:26 2017 +0200
+++ b/src/Pure/Isar/specification.ML Mon Jul 03 13:51:55 2017 +0200
@@ -45,6 +45,10 @@
(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 alias: binding * string -> local_theory -> local_theory
+ val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
+ val type_alias: binding * string -> local_theory -> local_theory
+ val type_alias_cmd: binding * (xstring * Position.T) -> 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
@@ -305,6 +309,27 @@
val abbreviation_cmd = gen_abbrev read_spec_open;
+(* alias *)
+
+fun gen_alias decl check (b, arg) lthy =
+ let
+ val (c, reports) = check {proper = true, strict = false} lthy arg;
+ val _ = Position.reports reports;
+ in decl b c lthy end;
+
+val alias =
+ gen_alias Local_Theory.const_alias (K (K (fn c => (c, []))));
+val alias_cmd =
+ gen_alias Local_Theory.const_alias
+ (fn flags => fn ctxt => fn (c, pos) =>
+ apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos])));
+
+val type_alias =
+ gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));
+val type_alias_cmd =
+ gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
+
+
(* notation *)
local
--- a/src/Pure/Pure.thy Mon Jul 03 09:57:26 2017 +0200
+++ b/src/Pure/Pure.thy Mon Jul 03 13:51:55 2017 +0200
@@ -18,7 +18,7 @@
and "typedecl" "type_synonym" "nonterminal" "judgment"
"consts" "syntax" "no_syntax" "translations" "no_translations"
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
- "no_notation" "axiomatization" "lemmas" "declare"
+ "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
@@ -374,6 +374,16 @@
Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
>> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
+val _ =
+ Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant"
+ (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
+ >> Specification.alias_cmd);
+
+val _ =
+ Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor"
+ (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
+ >> Specification.type_alias_cmd);
+
in end\<close>