# HG changeset patch
# User haftmann
# Date 1230968394 -3600
# Node ID d8df32ab117288668305519b4e3d055183c7d4ba
# Parent  dfaf9d086868059b0a498300ff9d6707621961e1# Parent  52a384648d13cd7b23ce9eba6a9ee38a18d7ba1e
merged

diff -r dfaf9d086868 -r d8df32ab1172 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/Nat_Infinity.thy
-    ID:         $Id$
     Author:     David von Oheimb, TU Muenchen;  Florian Haftmann, TU Muenchen
 *)
 
@@ -9,6 +8,17 @@
 imports Plain "~~/src/HOL/Presburger"
 begin
 
+text {* FIXME: move to Nat.thy *}
+
+instantiation nat :: bot
+begin
+
+definition bot_nat :: nat where
+  "bot_nat = 0"
+
+instance proof
+qed (simp add: bot_nat_def)
+
 subsection {* Type definition *}
 
 text {*
@@ -16,6 +26,8 @@
   infinity.
 *}
 
+end
+
 datatype inat = Fin nat | Infty
 
 notation (xsymbols)
@@ -353,6 +365,20 @@
 apply (erule (1) le_less_trans)
 done
 
+instantiation inat :: "{bot, top}"
+begin
+
+definition bot_inat :: inat where
+  "bot_inat = 0"
+
+definition top_inat :: inat where
+  "top_inat = \<infinity>"
+
+instance proof
+qed (simp_all add: bot_inat_def top_inat_def)
+
+end
+
 
 subsection {* Well-ordering *}
 
diff -r dfaf9d086868 -r d8df32ab1172 src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/HOL/Rational.thy	Sat Jan 03 08:39:54 2009 +0100
@@ -851,7 +851,7 @@
 definition Fract_norm :: "int \<Rightarrow> int \<Rightarrow> rat" where
   [simp, code del]: "Fract_norm a b = Fract a b"
 
-lemma [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
+lemma Fract_norm_code [code]: "Fract_norm a b = (if a = 0 \<or> b = 0 then 0 else let c = zgcd a b in
   if b > 0 then Fract (a div c) (b div c) else Fract (- (a div c)) (- (b div c)))"
   by (simp add: eq_rat Zero_rat_def Let_def Fract_norm)
 
@@ -871,7 +871,7 @@
        then c = 0 \<or> d = 0
      else if d = 0
        then a = 0 \<or> b = 0
-     else a * d =  b * c)"
+     else a * d = b * c)"
   by (auto simp add: eq eq_rat)
 
 lemma rat_eq_refl [code nbe]:
diff -r dfaf9d086868 -r d8df32ab1172 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/Pure/General/binding.ML	Sat Jan 03 08:39:54 2009 +0100
@@ -26,6 +26,8 @@
   val base_name: T -> string
   val pos_of: T -> Position.T
   val dest: T -> (string * bool) list * string
+  val separator: string
+  val is_qualified: string -> bool
   val display: T -> string
 end
 
@@ -39,6 +41,17 @@
 val unique_names = ref true;
 
 
+(** qualification **)
+
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
+
+fun reject_qualified kind s =
+  if is_qualified s then
+    error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
+  else s;
+
+
 (** binding representation **)
 
 datatype T = Binding of ((string * bool) list * string) * Position.T;
@@ -54,13 +67,14 @@
 
 fun qualify_base path name =
   if path = "" orelse name = "" then name
-  else path ^ "." ^ name;
+  else path ^ separator ^ name;
 
 val qualify = map_base o qualify_base;
   (*FIXME should all operations on bare names move here from name_space.ML ?*)
 
 fun add_prefix sticky "" b = b
-  | add_prefix sticky prfx b = (map_binding o apfst) (cons (prfx, sticky)) b;
+  | add_prefix sticky prfx b = (map_binding o apfst)
+      (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
 
 fun map_prefix f (Binding ((prefix, name), pos)) =
   f prefix (name_pos (name, pos));
diff -r dfaf9d086868 -r d8df32ab1172 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/Pure/General/name_space.ML	Sat Jan 03 08:39:54 2009 +0100
@@ -59,10 +59,10 @@
 (** long identifiers **)
 
 fun hidden name = "??." ^ name;
-val is_hidden = String.isPrefix "??."
+val is_hidden = String.isPrefix "??.";
 
-val separator = ".";
-val is_qualified = exists_string (fn s => s = separator);
+val separator = Binding.separator;
+val is_qualified = Binding.is_qualified;
 
 val implode_name = space_implode separator;
 val explode_name = space_explode separator;
diff -r dfaf9d086868 -r d8df32ab1172 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/Pure/IsaMakefile	Sat Jan 03 08:39:54 2009 +0100
@@ -26,6 +26,7 @@
   Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
   Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
   General/alist.ML General/balanced_tree.ML General/basics.ML		\
+  General/binding.ML							\
   General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
   General/integer.ML General/lazy.ML General/markup.ML			\
   General/name_space.ML General/ord_list.ML General/output.ML		\
diff -r dfaf9d086868 -r d8df32ab1172 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML	Sat Jan 03 08:39:54 2009 +0100
@@ -55,9 +55,9 @@
 use "overloading.ML";
 use "locale.ML";
 use "new_locale.ML";
-use "expression.ML";
 use "class.ML";
 use "theory_target.ML";
+use "expression.ML";
 use "instance.ML";
 use "subclass.ML";
 
diff -r dfaf9d086868 -r d8df32ab1172 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jan 02 23:59:32 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Jan 03 08:39:54 2009 +0100
@@ -85,7 +85,7 @@
 
 end;
 
-structure New_Locale =
+(*structure New_Locale =
 struct
 
 val intro_locales_tac = Locale.intro_locales_tac; (*already forked!*)
@@ -106,7 +106,7 @@
 val parameters_of = NewLocale.params_of; (*why typ option?*)
 val add_locale = Expression.add_locale;
 
-end;
+end;*)
 
 structure Locale = Old_Locale;