author wenzelm Tue, 10 Mar 2009 17:54:49 +0100 changeset 30414 aa8c5ab72cc6 parent 30413 c41afa5607be (current diff) parent 30412 7f5b0a020ccd (diff) child 30417 09a757ca128f
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>)"
```--- 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
+  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);```