# HG changeset patch
# User wenzelm
# Date 1499084707 -7200
# Node ID 56a87a5093be1b103a12043390df9c4b3125916b
# Parent  4c999b5d78e24137b6f4ea71a750ff4ef0358ebb# Parent  f50e6e31a0eef017fa6953db33a9eb8c36d7e993
merged

diff -r 4c999b5d78e2 -r 56a87a5093be NEWS
--- a/NEWS	Mon Jul 03 12:19:49 2017 +0200
+++ b/NEWS	Mon Jul 03 14:25:07 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 ***
 
diff -r 4c999b5d78e2 -r 56a87a5093be src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 14:25:07 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.
 
diff -r 4c999b5d78e2 -r 56a87a5093be src/HOL/BNF_Greatest_Fixpoint.thy
--- a/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 14:25:07 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
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/General/name_space.ML	Mon Jul 03 14:25:07 2017 +0200
@@ -258,8 +258,8 @@
 fun completion context space (xname, pos) =
   Completion.make (xname, pos) (fn completed =>
     let
-      fun result_ord ((precise1, (xname1, (_, name1))), (precise2, (xname2, (_, name2)))) =
-        (case bool_ord (precise2, precise1) of
+      fun result_ord ((pri1, (xname1, (_, name1))), (pri2, (xname2, (_, name2)))) =
+        (case int_ord (pri2, pri1) of
           EQUAL =>
             (case bool_ord (apply2 (is_some o Long_Name.dest_local) (name2, name1)) of
               EQUAL =>
@@ -271,16 +271,21 @@
       val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val full = Name.clean xname = "";
+
+      fun complete xname' name =
+        if (completed xname' orelse exists completed (Long_Name.explode xname')) andalso
+          not (is_concealed space name)
+        then
+          let
+            val xname'' = ext name;
+            val pri = (if xname' = xname'' then 1 else 0) + (if completed xname' then 1 else 0);
+          in
+            if xname' <> xname'' andalso full then I
+            else cons (pri, (xname', (kind, name)))
+          end
+        else I;
     in
-      Change_Table.fold
-        (fn (xname', (name :: _, _)) =>
-              if completed xname' andalso not (is_concealed space name) then
-                let val xname'' = ext name in
-                  if xname' <> xname'' andalso full then I
-                  else cons (xname' = xname'', (xname', (kind, name)))
-                end
-              else I
-          | _ => I) internals []
+      Change_Table.fold (fn (xname', (name :: _, _)) => complete xname' name | _ => I) internals []
       |> sort_distinct result_ord
       |> map #2
     end);
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/local_theory.ML	Mon Jul 03 14:25:07 2017 +0200
@@ -63,7 +63,6 @@
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: Name_Space.naming -> operations -> Proof.context -> local_theory
@@ -294,7 +293,7 @@
       let val binding' = Morphism.binding phi binding in
         Context.mapping
           (Global_Theory.alias_fact binding' name)
-          (Proof_Context.fact_alias binding' name)
+          (Proof_Context.alias_fact binding' name)
       end));
 
 
@@ -335,7 +334,6 @@
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
-val class_alias = syntax_alias Sign.class_alias Proof_Context.class_alias;
 val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
 val const_alias = syntax_alias Sign.const_alias Proof_Context.const_alias;
 
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Jul 03 14:25:07 2017 +0200
@@ -132,6 +132,7 @@
   val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
+  val alias_fact: binding -> string -> Proof.context -> Proof.context
   val read_var: binding * string option * mixfix -> Proof.context ->
     (binding * typ option * mixfix) * Proof.context
   val cert_var: binding * typ option * mixfix -> Proof.context ->
@@ -158,10 +159,8 @@
     Context.generic -> Context.generic
   val generic_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
-  val class_alias: binding -> class -> Proof.context -> Proof.context
   val type_alias: binding -> string -> Proof.context -> Proof.context
   val const_alias: binding -> string -> Proof.context -> Proof.context
-  val fact_alias: binding -> string -> Proof.context -> Proof.context
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
@@ -1089,6 +1088,8 @@
 
 end;
 
+fun alias_fact b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
+
 
 
 (** basic logical entities **)
@@ -1184,10 +1185,8 @@
 
 (* aliases *)
 
-fun class_alias b c ctxt = (map_tsig o apfst) (Type.class_alias (naming_of ctxt) b c) ctxt;
 fun type_alias b c ctxt = (map_tsig o apfst) (Type.type_alias (naming_of ctxt) b c) ctxt;
 fun const_alias b c ctxt = (map_consts o apfst) (Consts.alias (naming_of ctxt) b c) ctxt;
-fun fact_alias b c ctxt = map_facts (Facts.alias (naming_of ctxt) b c) ctxt;
 
 
 (* local constants *)
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Isar/specification.ML	Mon Jul 03 14:25:07 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
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/Pure.thy	Mon Jul 03 14:25:07 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>
 
 
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/sign.ML	Mon Jul 03 14:25:07 2017 +0200
@@ -53,7 +53,6 @@
   val intern_class: theory -> xstring -> string
   val intern_type: theory -> xstring -> string
   val intern_const: theory -> xstring -> string
-  val class_alias: binding -> class -> theory -> theory
   val type_alias: binding -> string -> theory -> theory
   val const_alias: binding -> string -> theory -> theory
   val arity_number: theory -> string -> int
@@ -246,7 +245,6 @@
 val intern_type = Name_Space.intern o type_space;
 val intern_const = Name_Space.intern o const_space;
 
-fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy;
 fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy;
 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
 
diff -r 4c999b5d78e2 -r 56a87a5093be src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Jul 03 12:19:49 2017 +0200
+++ b/src/Pure/type.ML	Mon Jul 03 14:25:07 2017 +0200
@@ -29,7 +29,6 @@
   val change_ignore: tsig -> tsig
   val empty_tsig: tsig
   val class_space: tsig -> Name_Space.T
-  val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
@@ -202,9 +201,6 @@
 
 val class_space = #1 o #classes o rep_tsig;
 
-fun class_alias naming binding name = map_tsig (fn ((space, classes), default, types) =>
-  ((Name_Space.alias naming binding name space, classes), default, types));
-
 fun defaultS (TSig {default, ...}) = default;
 fun logical_types (TSig {log_types, ...}) = log_types;