merged

--- a/src/HOL/ex/Sqrt.thy	Tue Mar 10 16:36:22 2009 +0100
+++ b/src/HOL/ex/Sqrt.thy	Tue Mar 10 17:54:49 2009 +0100
@@ -1,6 +1,5 @@
 (*  Title:      HOL/ex/Sqrt.thy
     Author:     Markus Wenzel, TU Muenchen
-
 *)
 
 header {*  Square roots of primes are irrational *}
@@ -9,13 +8,6 @@
 imports Complex_Main Primes
 begin
 
-text {* The definition and the key representation theorem for the set of
-rational numbers has been moved to a core theory.  *}
-
-declare Rats_abs_nat_div_natE[elim?]
-
-subsection {* Main theorem *}
-
 text {*
   The square root of any prime number (including @{text 2}) is
   irrational.
@@ -29,7 +21,7 @@
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<twosuperior> = p * n\<twosuperior>"
   proof -
     from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
@@ -75,7 +67,7 @@
   assume "sqrt (real p) \<in> \<rat>"
   then obtain m n where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt (real p)\<bar> = real m / real n"
-    and gcd: "gcd m n = 1" ..
+    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
   from n and sqrt_rat have "real m = \<bar>sqrt (real p)\<bar> * real n" by simp
   then have "real (m\<twosuperior>) = (sqrt (real p))\<twosuperior> * real (n\<twosuperior>)"
     by (auto simp add: power2_eq_square)

--- a/src/Pure/General/binding.ML	Tue Mar 10 16:36:22 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 10 17:54:49 2009 +0100
@@ -11,7 +11,6 @@
 sig
   type binding
   val dest: binding -> (string * bool) list * bstring
-  val str_of: binding -> string
   val make: bstring * Position.T -> binding
   val pos_of: binding -> Position.T
   val name: bstring -> binding
@@ -22,11 +21,13 @@
   val eq_name: binding * binding -> bool
   val empty: binding
   val is_empty: binding -> bool
+  val qualify: bool -> string -> binding -> binding
   val qualified_name: bstring -> binding
-  val qualify: bool -> string -> binding -> binding
+  val qualified_name_of: binding -> bstring
   val prefix_of: binding -> (string * bool) list
   val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val prefix: bool -> string -> binding -> binding
+  val str_of: binding -> string
 end;
 
 structure Binding:> BINDING =
@@ -50,12 +51,6 @@
 
 fun dest (Binding {prefix, qualifier, name, ...}) = (prefix @ qualifier, name);
 
-fun str_of (Binding {prefix, qualifier, name, pos}) =
-  let
-    val text = Long_Name.implode (map #1 qualifier @ [name]);
-    val props = Position.properties_of pos;
-  in Markup.markup (Markup.properties props (Markup.binding name)) text end;
-
 
 
 (** basic operations **)
@@ -80,14 +75,17 @@
 
 (* user qualifier *)
 
+fun qualify _ "" = I
+  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
+      (prefix, (qual, mandatory) :: qualifier, name, pos));
+
 fun qualified_name "" = empty
   | qualified_name s =
       let val (qualifier, name) = split_last (Long_Name.explode s)
       in make_binding ([], map (rpair false) qualifier, name, Position.none) end;
 
-fun qualify _ "" = I
-  | qualify strict qual = map_binding (fn (prefix, qualifier, name, pos) =>
-      (prefix, (qual, strict) :: qualifier, name, pos));
+fun qualified_name_of (Binding {qualifier, name, ...}) =
+  Long_Name.implode (map #1 qualifier @ [name]);
 
 
 (* system prefix *)
@@ -98,7 +96,16 @@
   (f prefix, qualifier, name, pos));
 
 fun prefix _ "" = I
-  | prefix strict prfx = map_prefix (cons (prfx, strict));
+  | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
+
+
+(* str_of *)
+
+fun str_of binding =
+  let
+    val text = qualified_name_of binding;
+    val props = Position.properties_of (pos_of binding);
+  in Markup.markup (Markup.properties props (Markup.binding (name_of binding))) text end;
 
 end;
 

--- a/src/Pure/General/name_space.ML	Tue Mar 10 16:36:22 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 10 17:54:49 2009 +0100
@@ -32,7 +32,6 @@
   val declare: naming -> binding -> T -> string * T
   val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
-  val path_of: naming -> string
   val add_path: string -> naming -> naming
   val no_base_names: naming -> naming
   val qualified_names: naming -> naming
@@ -50,38 +49,14 @@
 structure NameSpace: NAME_SPACE =
 struct
 
-(** long identifiers **)
+
+(** name spaces **)
+
+(* hidden entries *)
 
 fun hidden name = "??." ^ name;
 val is_hidden = String.isPrefix "??.";
 
-(* standard accesses *)
-
-infixr 6 @@;
-fun ([] @@ yss) = []
-  | ((xs :: xss) @@ yss) = map (fn ys => xs @ ys) yss @ (xss @@ yss);
-
-fun suffixes_prefixes list =
-  let
-    val (xs, ws) = chop (length list - 1) list;
-    val sfxs = suffixes xs @@ [ws];
-    val pfxs = prefixes1 xs @@ [ws];
-  in (sfxs @ pfxs, sfxs) end;
-
-fun suffixes_prefixes_split i k list =
-  let
-    val (((xs, ys), zs), ws) = list |> chop i ||>> chop k ||>> chop (length list - (i + k + 1));
-    val sfxs =
-      [ys] @@ suffixes zs @@ [ws] @
-      suffixes1 xs @@ [ys @ zs @ ws];
-    val pfxs =
-      prefixes1 xs @@ [ys @ ws] @
-      [xs @ ys] @@ prefixes1 zs @@ [ws];
-  in (sfxs @ pfxs, sfxs) end;
-
-
-
-(** name spaces **)
 
 (* datatype T *)
 
@@ -196,74 +171,95 @@
 (* datatype naming *)
 
 datatype naming = Naming of
-  string *                                                 (*path*)
-  ((string -> string -> string) *                          (*qualify*)
-   (string list -> string list list * string list list));  (*accesses*)
+ {path: (string * bool) list,
+  no_base_names: bool,
+  qualified_names: bool};
 
-fun path_of (Naming (path, _)) = path;
-fun accesses (Naming (_, (_, accs))) = accs;
+fun make_naming (path, no_base_names, qualified_names) =
+  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
 
-fun external_names naming = map Long_Name.implode o #2 o accesses naming o Long_Name.explode;
+fun map_naming f (Naming {path, no_base_names, qualified_names}) =
+  make_naming (f (path, no_base_names, qualified_names));
+
+fun path_of (Naming {path, ...}) = path;
 
 
-(* manipulate namings *)
-
-fun reject_qualified name =
-  if Long_Name.is_qualified name then
-    error ("Attempt to declare qualified name " ^ quote name)
-  else name;
+(* configure naming *)
 
-val default_naming =
-  Naming ("", (fn path => Long_Name.qualify path o reject_qualified, suffixes_prefixes));
-
-fun add_path elems (Naming (path, policy)) =
-  if elems = "//" then Naming ("", (Long_Name.qualify, #2 policy))
-  else if elems = "/" then Naming ("", policy)
-  else if elems = ".." then Naming (Long_Name.qualifier path, policy)
-  else Naming (Long_Name.append path elems, policy);
+val default_naming = make_naming ([], false, false);
 
-fun no_base_names (Naming (path, (qualify, accs))) =
-  Naming (path, (qualify, pairself (filter_out (fn [_] => true | _ => false)) o accs));
-
-fun qualified_names (Naming (path, (_, accs))) = Naming (path, (Long_Name.qualify, accs));
+fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
+  if elems = "//" then ([], no_base_names, true)
+  else if elems = "/" then ([], no_base_names, qualified_names)
+  else if elems = ".." then (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names)
+  else (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
 
-fun sticky_prefix prfx (Naming (path, (qualify, _))) =
-  Naming (Long_Name.append path prfx,
-    (qualify,
-      suffixes_prefixes_split (length (Long_Name.explode path)) (length (Long_Name.explode prfx))));
+fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
+  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
 
-val apply_prefix =
-  let
-    fun mk_prefix (prfx, true) = sticky_prefix prfx
-      | mk_prefix (prfx, false) = add_path prfx;
-  in fold mk_prefix end;
+val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
+val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
 
 
 (* full name *)
 
-fun full (Naming (path, (qualify, _))) = qualify path;
+fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
 
-fun full_name naming binding =
+fun name_spec (Naming {path, qualified_names, ...}) binding =
   let
-    val (prfx, bname) = Binding.dest binding;
-    val naming' = apply_prefix prfx naming;
-  in full naming' bname end;
+    val (prefix, name) = Binding.dest binding;
+    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
+
+    val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
+    val spec2 =
+      (case try split_last (Long_Name.explode name) of
+        NONE => []
+      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
+
+    val spec = spec1 @ spec2;
+    val _ =
+      exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec
+      andalso err_bad binding;
+  in if null spec2 then [] else spec end;
+
+fun full naming = name_spec naming #> map fst;
+fun full_name naming = full naming #> Long_Name.implode;
+
+
+(* accesses *)
+
+fun mandatory xs = map_filter (fn (x, true) => SOME x | _ => NONE) xs;
+
+fun mandatory_prefixes xs = mandatory xs :: mandatory_prefixes1 xs
+and mandatory_prefixes1 [] = []
+  | mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
+  | mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
+
+fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
+fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
+
+fun accesses (naming as Naming {no_base_names, ...}) binding =
+  let
+    val spec = name_spec naming binding;
+    val sfxs = mandatory_suffixes spec;
+    val pfxs = mandatory_prefixes spec;
+  in
+    (sfxs @ pfxs, sfxs)
+    |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
+    |> pairself (map Long_Name.implode)
+  end;
+
+fun external_names naming = #2 o accesses naming o Binding.qualified_name;
 
 
 (* declaration *)
 
 fun declare naming binding space =
   let
-    val (prfx, bname) = Binding.dest binding;
-    val naming' = apply_prefix prfx naming;
-    val name = full naming' bname;
-    val names = Long_Name.explode name;
-
-    val _ = (null names orelse exists (fn s => s = "" orelse s = "??") names
-        orelse exists_string (fn s => s = "\"") name) andalso
-      error ("Bad name declaration " ^ quote (Binding.str_of binding));
-
-    val (accs, accs') = pairself (map Long_Name.implode) (accesses naming' names);
+    val names = full naming binding;
+    val name = Long_Name.implode names;
+    val _ = name = "" andalso err_bad binding;
+    val (accs, accs') = accesses naming binding;
     val space' = space |> fold (add_name name) accs |> put_accesses name accs';
   in (name, space') end;
 

--- a/src/Pure/display.ML	Tue Mar 10 16:36:22 2009 +0100
+++ b/src/Pure/display.ML	Tue Mar 10 17:54:49 2009 +0100
@@ -213,8 +213,7 @@
     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   in
     [Pretty.strs ("names:" :: Context.display_names thy)] @
-    [Pretty.strs ["name prefix:", NameSpace.path_of naming],
-      Pretty.big_list "classes:" (map pretty_classrel clsses),
+    [Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),

--- a/src/Pure/pure_setup.ML	Tue Mar 10 16:36:22 2009 +0100
+++ b/src/Pure/pure_setup.ML	Tue Mar 10 17:54:49 2009 +0100
@@ -33,7 +33,7 @@
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.str_of));
+install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of));
 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);