# HG changeset patch # User wenzelm # Date 1499082715 -7200 # Node ID df85956228c2901b25a8381f9eb3f0847be6f790 # Parent 8d966b4a7469233d1c894bafb04a04f1cf650eaa added command 'alias' and 'type_alias'; diff -r 8d966b4a7469 -r df85956228c2 NEWS --- 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 *** diff -r 8d966b4a7469 -r df85956228c2 src/Doc/Isar_Ref/Spec.thy --- 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 \ \begin{matharray}{rcl} + @{command_def "alias"} & : & \local_theory \ local_theory\ \\ + @{command_def "type_alias"} & : & \local_theory \ local_theory\ \\ @{command_def "hide_class"} & : & \theory \ theory\ \\ @{command_def "hide_type"} & : & \theory \ theory\ \\ @{command_def "hide_const"} & : & \theory \ theory\ \\ @@ -1318,8 +1320,10 @@ \end{matharray} @{rail \ - ( @{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} + ) \} 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>\alias\ and \<^theory_text>\type_alias\ introduce aliases for constants and type + constructors, respectively. This allows adhoc changes to name-space + accesses. + + \<^descr> \<^theory_text>\type_alias b = c\ introduces an alias for an existing type constructor. + \<^descr> \<^theory_text>\hide_class names\ fully removes class declarations from a given name space; with the \(open)\ option, only the unqualified base name is hidden. diff -r 8d966b4a7469 -r df85956228c2 src/HOL/BNF_Greatest_Fixpoint.thy --- 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 \Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\ +alias proj = Equiv_Relations.proj lemma one_pointE: "\\x. s = x \ P\ \ P" by simp diff -r 8d966b4a7469 -r df85956228c2 src/Pure/Isar/specification.ML --- 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 diff -r 8d966b4a7469 -r df85956228c2 src/Pure/Pure.thy --- 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\