added command 'alias' and 'type_alias';
authorwenzelm
Mon Jul 03 13:51:55 2017 +0200 (21 months ago)
changeset 66248df85956228c2
parent 66247 8d966b4a7469
child 66249 f50e6e31a0ee
added command 'alias' and 'type_alias';
NEWS
src/Doc/Isar_Ref/Spec.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/Pure/Isar/specification.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Mon Jul 03 09:57:26 2017 +0200
     1.2 +++ b/NEWS	Mon Jul 03 13:51:55 2017 +0200
     1.3 @@ -62,6 +62,10 @@
     1.4  src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
     1.5  tutorial on code generation.
     1.6  
     1.7 +* Commands 'alias' and 'type_alias' introduce aliases for constants and
     1.8 +type constructors, respectively. This allows adhoc changes to name-space
     1.9 +accesses within global or local theory contexts, e.g. within a 'bundle'.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 09:57:26 2017 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Jul 03 13:51:55 2017 +0200
     2.3 @@ -1311,6 +1311,8 @@
     2.4  
     2.5  text \<open>
     2.6    \begin{matharray}{rcl}
     2.7 +    @{command_def "alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     2.8 +    @{command_def "type_alias"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     2.9      @{command_def "hide_class"} & : & \<open>theory \<rightarrow> theory\<close> \\
    2.10      @{command_def "hide_type"} & : & \<open>theory \<rightarrow> theory\<close> \\
    2.11      @{command_def "hide_const"} & : & \<open>theory \<rightarrow> theory\<close> \\
    2.12 @@ -1318,8 +1320,10 @@
    2.13    \end{matharray}
    2.14  
    2.15    @{rail \<open>
    2.16 -    ( @{command hide_class} | @{command hide_type} |
    2.17 -      @{command hide_const} | @{command hide_fact} ) ('(' @'open' ')')? (@{syntax name} + )
    2.18 +    (@{command alias} | @{command type_alias}) @{syntax name} '=' @{syntax name}
    2.19 +    ;
    2.20 +    (@{command hide_class} | @{command hide_type} |
    2.21 +      @{command hide_const} | @{command hide_fact}) ('(' @'open' ')')? (@{syntax name} + )
    2.22    \<close>}
    2.23  
    2.24    Isabelle organizes any kind of name declarations (of types, constants,
    2.25 @@ -1327,6 +1331,12 @@
    2.26    the user does not have to control the behaviour of name spaces by hand, yet
    2.27    the following commands provide some way to do so.
    2.28  
    2.29 +  \<^descr> \<^theory_text>\<open>alias\<close> and \<^theory_text>\<open>type_alias\<close> introduce aliases for constants and type
    2.30 +  constructors, respectively. This allows adhoc changes to name-space
    2.31 +  accesses.
    2.32 +
    2.33 +  \<^descr> \<^theory_text>\<open>type_alias b = c\<close> introduces an alias for an existing type constructor.
    2.34 +
    2.35    \<^descr> \<^theory_text>\<open>hide_class names\<close> fully removes class declarations from a given name
    2.36    space; with the \<open>(open)\<close> option, only the unqualified base name is hidden.
    2.37  
     3.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 09:57:26 2017 +0200
     3.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 13:51:55 2017 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4    "primcorec" :: thy_decl
     3.5  begin
     3.6  
     3.7 -setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
     3.8 +alias proj = Equiv_Relations.proj
     3.9  
    3.10  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    3.11    by simp
     4.1 --- a/src/Pure/Isar/specification.ML	Mon Jul 03 09:57:26 2017 +0200
     4.2 +++ b/src/Pure/Isar/specification.ML	Mon Jul 03 13:51:55 2017 +0200
     4.3 @@ -45,6 +45,10 @@
     4.4      (binding * typ option * mixfix) list -> term -> bool -> local_theory -> local_theory
     4.5    val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option ->
     4.6      (binding * string option * mixfix) list -> string -> bool -> local_theory -> local_theory
     4.7 +  val alias: binding * string -> local_theory -> local_theory
     4.8 +  val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
     4.9 +  val type_alias: binding * string -> local_theory -> local_theory
    4.10 +  val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
    4.11    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
    4.12    val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
    4.13      local_theory -> local_theory
    4.14 @@ -305,6 +309,27 @@
    4.15  val abbreviation_cmd = gen_abbrev read_spec_open;
    4.16  
    4.17  
    4.18 +(* alias *)
    4.19 +
    4.20 +fun gen_alias decl check (b, arg) lthy =
    4.21 +  let
    4.22 +    val (c, reports) = check {proper = true, strict = false} lthy arg;
    4.23 +    val _ = Position.reports reports;
    4.24 +  in decl b c lthy end;
    4.25 +
    4.26 +val alias =
    4.27 +  gen_alias Local_Theory.const_alias (K (K (fn c => (c, []))));
    4.28 +val alias_cmd =
    4.29 +  gen_alias Local_Theory.const_alias
    4.30 +    (fn flags => fn ctxt => fn (c, pos) =>
    4.31 +      apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos])));
    4.32 +
    4.33 +val type_alias =
    4.34 +  gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));
    4.35 +val type_alias_cmd =
    4.36 +  gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
    4.37 +
    4.38 +
    4.39  (* notation *)
    4.40  
    4.41  local
     5.1 --- a/src/Pure/Pure.thy	Mon Jul 03 09:57:26 2017 +0200
     5.2 +++ b/src/Pure/Pure.thy	Mon Jul 03 13:51:55 2017 +0200
     5.3 @@ -18,7 +18,7 @@
     5.4    and "typedecl" "type_synonym" "nonterminal" "judgment"
     5.5      "consts" "syntax" "no_syntax" "translations" "no_translations"
     5.6      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     5.7 -    "no_notation" "axiomatization" "lemmas" "declare"
     5.8 +    "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
     5.9      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    5.10    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
    5.11    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
    5.12 @@ -374,6 +374,16 @@
    5.13        Scan.optional (Parse.where_ |-- Parse.!!! axiomatization) ([], [], [])
    5.14        >> (fn (a, (b, c, d)) => Toplevel.theory (#2 o Specification.axiomatization_cmd a b c d)));
    5.15  
    5.16 +val _ =
    5.17 +  Outer_Syntax.local_theory @{command_keyword alias} "name-space alias for constant"
    5.18 +    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
    5.19 +      >> Specification.alias_cmd);
    5.20 +
    5.21 +val _ =
    5.22 +  Outer_Syntax.local_theory @{command_keyword type_alias} "name-space alias for type constructor"
    5.23 +    (Parse.binding -- (Parse.!!! @{keyword =} |-- Parse.position Parse.name)
    5.24 +      >> Specification.type_alias_cmd);
    5.25 +
    5.26  in end\<close>
    5.27  
    5.28