# HG changeset patch # User wenzelm # Date 1236707546 -3600 # Node ID 09a757ca128fcc4343e8d4a2be39a3c9164e8bb6 # Parent c132175cae7e0f070d46cfcd66df154da154b89c# Parent aa8c5ab72cc6aac89c0a27edef54985ca28361de merged diff -r c132175cae7e -r 09a757ca128f src/HOL/ex/Sqrt.thy --- a/src/HOL/ex/Sqrt.thy Tue Mar 10 17:39:18 2009 +0000 +++ b/src/HOL/ex/Sqrt.thy Tue Mar 10 18:52:26 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) \ \" then obtain m n where n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = 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\ = p * n\" proof - from n and sqrt_rat have "real m = \sqrt (real p)\ * real n" by simp @@ -75,7 +67,7 @@ assume "sqrt (real p) \ \" then obtain m n where n: "n \ 0" and sqrt_rat: "\sqrt (real p)\ = 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 = \sqrt (real p)\ * real n" by simp then have "real (m\) = (sqrt (real p))\ * real (n\)" by (auto simp add: power2_eq_square) diff -r c132175cae7e -r 09a757ca128f src/Pure/General/binding.ML --- a/src/Pure/General/binding.ML Tue Mar 10 17:39:18 2009 +0000 +++ b/src/Pure/General/binding.ML Tue Mar 10 18:52:26 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; diff -r c132175cae7e -r 09a757ca128f src/Pure/General/name_space.ML --- a/src/Pure/General/name_space.ML Tue Mar 10 17:39:18 2009 +0000 +++ b/src/Pure/General/name_space.ML Tue Mar 10 18:52:26 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; diff -r c132175cae7e -r 09a757ca128f src/Pure/display.ML --- a/src/Pure/display.ML Tue Mar 10 17:39:18 2009 +0000 +++ b/src/Pure/display.ML Tue Mar 10 18:52:26 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), diff -r c132175cae7e -r 09a757ca128f src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Tue Mar 10 17:39:18 2009 +0000 +++ b/src/Pure/pure_setup.ML Tue Mar 10 18:52:26 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);