# HG changeset patch
# User huffman
# Date 1233124781 28800
# Node ID fd39a59cbeb49c46e81760925269769e7a036b11
# Parent  c8c67557f1874fc14b0ae0da4c5267929f126f08# Parent  12070638fe29183b0b2e3240f6a9504dd70a92ba
merged

diff -r c8c67557f187 -r fd39a59cbeb4 Admin/isatest/settings/at-mac-poly-5.1-para
--- a/Admin/isatest/settings/at-mac-poly-5.1-para	Thu Jan 22 06:42:05 2009 -0800
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para	Tue Jan 27 22:39:41 2009 -0800
@@ -25,4 +25,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i false -d false -M 4"
 
-HOL_USEDIR_OPTIONS="-p 2"
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
diff -r c8c67557f187 -r fd39a59cbeb4 Admin/isatest/settings/at-poly-5.1-para-e
--- a/Admin/isatest/settings/at-poly-5.1-para-e	Thu Jan 22 06:42:05 2009 -0800
+++ b/Admin/isatest/settings/at-poly-5.1-para-e	Tue Jan 27 22:39:41 2009 -0800
@@ -24,4 +24,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 20"
 
-HOL_USEDIR_OPTIONS="-p 2"
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
diff -r c8c67557f187 -r fd39a59cbeb4 Admin/isatest/settings/at64-poly-5.1-para
--- a/Admin/isatest/settings/at64-poly-5.1-para	Thu Jan 22 06:42:05 2009 -0800
+++ b/Admin/isatest/settings/at64-poly-5.1-para	Tue Jan 27 22:39:41 2009 -0800
@@ -24,4 +24,4 @@
 
 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -M 2"
 
-HOL_USEDIR_OPTIONS="-p 2"
+HOL_USEDIR_OPTIONS="-p 2 -Q false"
diff -r c8c67557f187 -r fd39a59cbeb4 Admin/makedist
--- a/Admin/makedist	Thu Jan 22 06:42:05 2009 -0800
+++ b/Admin/makedist	Tue Jan 27 22:39:41 2009 -0800
@@ -1,12 +1,10 @@
 #!/usr/bin/env bash
 #
-# $Id$
-#
 # makedist -- make Isabelle source distribution
 
 ## global settings
 
-REPOS="http://isabelle.in.tum.de/repos/isabelle"
+REPOS="https://isabelle.in.tum.de/repos/isabelle"
 
 DISTPREFIX=${DISTPREFIX:-~/tmp/isadist}
 
diff -r c8c67557f187 -r fd39a59cbeb4 NEWS
--- a/NEWS	Thu Jan 22 06:42:05 2009 -0800
+++ b/NEWS	Tue Jan 27 22:39:41 2009 -0800
@@ -193,6 +193,8 @@
 
 *** HOL ***
 
+* Entry point to Word library now simply named "Word".  INCOMPATIBILITY.
+
 * Made source layout more coherent with logical distribution
 structure:
 
diff -r c8c67557f187 -r fd39a59cbeb4 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -291,7 +291,7 @@
   in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.
 *}
 
-section {* Linear transformations *}
+section {* Linear transformations \label{sec:ML-linear-trans} *}
 
 text %mlref {*
   \begin{mldecls}
diff -r c8c67557f187 -r fd39a59cbeb4 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Thu Jan 22 06:42:05 2009 -0800
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Tue Jan 27 22:39:41 2009 -0800
@@ -319,7 +319,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Linear transformations%
+\isamarkupsection{Linear transformations \label{sec:ML-linear-trans}%
 }
 \isamarkuptrue%
 %
diff -r c8c67557f187 -r fd39a59cbeb4 doc-src/more_antiquote.ML
--- a/doc-src/more_antiquote.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/doc-src/more_antiquote.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -113,13 +113,13 @@
   val parse_const_terms = Scan.repeat1 Args.term
     >> (fn ts => fn thy => map (Code_Unit.check_const thy) ts);
   val parse_consts = Scan.lift (Args.parens (Args.$$$ "consts")) |-- parse_const_terms
-    >> (fn mk_cs => fn thy => fn naming => map (the o Code_Thingol.lookup_const naming) (mk_cs thy));
+    >> (fn mk_cs => fn thy => fn naming => map_filter (Code_Thingol.lookup_const naming) (mk_cs thy));
   val parse_types = Scan.lift (Args.parens (Args.$$$ "types") |-- Scan.repeat1 Args.name)
-    >> (fn tycos => fn thy => fn naming => map (the o Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos);
+    >> (fn tycos => fn thy => fn naming => map_filter (Code_Thingol.lookup_tyco naming o Sign.intern_type thy) tycos);
   val parse_classes = Scan.lift (Args.parens (Args.$$$ "classes") |-- Scan.repeat1 Args.name)
-    >> (fn classes => fn thy => fn naming => map (the o Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
+    >> (fn classes => fn thy => fn naming => map_filter (Code_Thingol.lookup_class naming o Sign.intern_class thy) classes);
   val parse_instances = Scan.lift (Args.parens (Args.$$$ "instances") |-- Scan.repeat1 (Args.name --| Args.$$$ "::" -- Args.name))
-    >> (fn insts => fn thy => fn naming => map (the o Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
+    >> (fn insts => fn thy => fn naming => map_filter (Code_Thingol.lookup_instance naming o apsnd (Sign.intern_type thy) o apfst (Sign.intern_class thy) o swap) insts);
   val parse_names = parse_consts || parse_types || parse_classes || parse_instances; 
 
   fun code_stmts src ctxt ((mk_cs, mk_stmtss), target) =
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Int.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Int.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
                 Tobias Nipkow, Florian Haftmann, TU Muenchen
     Copyright   1994  University of Cambridge
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/IsaMakefile	Tue Jan 27 22:39:41 2009 -0800
@@ -974,7 +974,7 @@
   Word/Size.thy Word/BinGeneral.thy Word/BinOperations.thy		\
   Word/BinBoolList.thy Word/BitSyntax.thy Word/WordDefinition.thy	\
   Word/WordArith.thy Word/WordBitwise.thy Word/WordShift.thy		\
-  Word/WordGenLib.thy Word/WordMain.thy Word/document/root.tex		\
+  Word/WordGenLib.thy Word/Word.thy Word/document/root.tex		\
   Word/document/root.bib
 	@cd Word; $(ISABELLE_TOOL) usedir -b -g true $(OUT)/HOL HOL-Word
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Library/Boolean_Algebra.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,8 +1,5 @@
-(* 
-  ID:     $Id$
-  Author: Brian Huffman
-
-  Boolean algebras as locales.
+(*  Title:      HOL/Library/Boolean_Algebra.thy
+    Author:     Brian Huffman
 *)
 
 header {* Boolean Algebras *}
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Library/Numeral_Type.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,11 +1,8 @@
-(*
-  ID:     $Id$
-  Author: Brian Huffman
-
-  Numeral Syntax for Types
+(*  Title:      HOL/Library/Numeral_Type.thy
+    Author:     Brian Huffman
 *)
 
-header "Numeral Syntax for Types"
+header {* Numeral Syntax for Types *}
 
 theory Numeral_Type
 imports Plain "~~/src/HOL/Presburger"
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/List.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -2887,6 +2887,35 @@
 apply (auto simp: sorted_distinct_set_unique)
 done
 
+lemma sorted_take:
+  "sorted xs \<Longrightarrow> sorted (take n xs)"
+proof (induct xs arbitrary: n rule: sorted.induct)
+  case 1 show ?case by simp
+next
+  case 2 show ?case by (cases n) simp_all
+next
+  case (3 x y xs)
+  then have "x \<le> y" by simp
+  show ?case proof (cases n)
+    case 0 then show ?thesis by simp
+  next
+    case (Suc m) 
+    with 3 have "sorted (take m (y # xs))" by simp
+    with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
+  qed
+qed
+
+lemma sorted_drop:
+  "sorted xs \<Longrightarrow> sorted (drop n xs)"
+proof (induct xs arbitrary: n rule: sorted.induct)
+  case 1 show ?case by simp
+next
+  case 2 show ?case by (cases n) simp_all
+next
+  case 3 then show ?case by (cases n) simp_all
+qed
+
+
 end
 
 lemma sorted_upt[simp]: "sorted[i..<j]"
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Map.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -503,6 +503,15 @@
 lemma map_add_comm: "dom m1 \<inter> dom m2 = {} \<Longrightarrow> m1++m2 = m2++m1"
 by (rule ext) (force simp: map_add_def dom_def split: option.split)
 
+lemma dom_const [simp]:
+  "dom (\<lambda>x. Some y) = UNIV"
+  by auto
+
+lemma dom_if:
+  "dom (\<lambda>x. if P x then f x else g x) = dom f \<inter> {x. P x} \<union> dom g \<inter> {x. \<not> P x}"
+  by (auto split: if_splits)
+
+
 (* Due to John Matthews - could be rephrased with dom *)
 lemma finite_map_freshness:
   "finite (dom (f :: 'a \<rightharpoonup> 'b)) \<Longrightarrow> \<not> finite (UNIV :: 'a set) \<Longrightarrow>
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/ROOT.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -1,6 +1,7 @@
 (* Classical Higher-order Logic -- batteries included *)
 
 use_thy "Main";
+share_common_data ();
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Tools/atp_manager.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -89,13 +89,14 @@
   oldest_heap: ThreadHeap.T,
   active: (Thread.thread * (Time.time * Time.time * string)) list,
   cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
-  messages: string list};
+  messages: string list,
+  store: string list};
 
-fun make_state timeout_heap oldest_heap active cancelling messages =
+fun make_state timeout_heap oldest_heap active cancelling messages store =
   State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
-    active = active, cancelling = cancelling, messages = messages};
+    active = active, cancelling = cancelling, messages = messages, store = store};
 
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] []);
+val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] [] []);
 
 
 (* the managing thread *)
@@ -106,31 +107,27 @@
 
 (* unregister thread *)
 
-fun unregister (success, message) thread = Synchronized.change_result state
-  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+fun unregister (success, message) thread = Synchronized.change state
+  (fn state as State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     (case lookup_thread active thread of
       SOME (birthtime, _, description) =>
         let
           val (group, active') =
             if success then List.partition (fn (_, (tb, _, _)) => tb = birthtime) active
             else List.partition (fn (th, _) => Thread.equal (th, thread)) active
-          (* do not interrupt successful thread, as it needs to print out its message
-          (and terminates afterwards - see start_prover )*)
-          val group' = if success then delete_thread thread group else group
 
           val now = Time.now ()
           val cancelling' =
-            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group' cancelling
+            fold (fn (th, (tb, _, desc)) => update_thread (th, (tb, now, desc))) group cancelling
 
-          val msg = description ^ "\n" ^ message
-          val message' = "Sledgehammer: " ^ msg ^
+          val message' = description ^ "\n" ^ message ^
             (if length group <= 1 then ""
              else "\nInterrupted " ^ string_of_int (length group - 1) ^ " other group members")
-          val messages' = msg ::
-            (if length messages <= message_store_limit then messages
-             else #1 (chop message_store_limit messages))
-        in (message', make_state timeout_heap oldest_heap active' cancelling' messages') end
-    | NONE => ("", state)));
+          val store' = message' ::
+            (if length store <= message_store_limit then store
+             else #1 (chop message_store_limit store))
+        in make_state timeout_heap oldest_heap active' cancelling' (message' :: messages) store' end
+    | NONE =>state));
 
 
 (* kill excessive atp threads *)
@@ -144,13 +141,13 @@
 fun kill_oldest () =
   let exception Unchanged in
     Synchronized.change_result state
-      (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+      (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
         if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
         then raise Unchanged
         else
           let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
-          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end)
-      |> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)"))
+          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages store) end)
+      |> unregister (false, "Interrupted (maximum number of ATPs exceeded)")
     handle Unchanged => ()
   end;
 
@@ -162,6 +159,13 @@
 
 end;
 
+fun print_new_messages () =
+  let val to_print = Synchronized.change_result state
+    (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
+    (messages, make_state timeout_heap oldest_heap active cancelling [] store))  
+  in if null to_print then ()
+  else priority ("Sledgehammer: " ^ (space_implode "\n\n" to_print)) end;
+
 
 (* start a watching thread which runs forever -- only one may exist *)
 
@@ -178,8 +182,8 @@
           NONE => SOME (Time.+ (Time.now (), max_wait_time))
         | SOME (time, _) => SOME time)
 
-      (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
-      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) =
+      (* action: find threads whose timeout is reached, and interrupt cancelling threads *)
+      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages, store}) =
         let val (timeout_threads, timeout_heap') =
           ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
         in
@@ -189,15 +193,16 @@
             let
               val _ = List.app (SimpleThread.interrupt o #1) cancelling
               val cancelling' = filter (Thread.isActive o #1) cancelling
-              val state' = make_state timeout_heap' oldest_heap active cancelling' messages
+              val state' = make_state timeout_heap' oldest_heap active cancelling' messages store
             in SOME (map #2 timeout_threads, state') end
         end
     in
       while true do
        (Synchronized.timed_access state time_limit action
         |> these
-        |> List.app (priority o unregister (false, "Interrupted (reached timeout)"));
+        |> List.app (unregister (false, "Interrupted (reached timeout)"));
         kill_excessive ();
+        print_new_messages ();
         (*give threads time to respond to interrupt*)
         OS.Process.sleep min_wait_time)
     end)));
@@ -208,12 +213,12 @@
 fun register birthtime deadtime (thread, desc) =
  (check_thread_manager ();
   Synchronized.change state
-    (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+    (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
       let
         val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
         val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
         val active' = update_thread (thread, (birthtime, deadtime, desc)) active
-      in make_state timeout_heap' oldest_heap' active' cancelling messages end));
+      in make_state timeout_heap' oldest_heap' active' cancelling messages store end));
 
 
 
@@ -222,9 +227,9 @@
 (* kill: move all threads to cancelling *)
 
 fun kill () = Synchronized.change state
-  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages, store} =>
     let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
-    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end);
+    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages store end);
 
 
 (* ATP info *)
@@ -255,7 +260,7 @@
 fun messages opt_limit =
   let
     val limit = the_default message_display_limit opt_limit;
-    val State {messages = msgs, ...} = Synchronized.value state
+    val State {store = msgs, ...} = Synchronized.value state
     val header = "Recent ATP messages" ^
       (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
   in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
@@ -307,7 +312,7 @@
                 => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
               | ERROR msg
                 => (false, "Error: " ^ msg)
-            val _ = priority (unregister result (Thread.self ()))
+            val _ = unregister result (Thread.self ())
           in () end handle Interrupt => ())
       in () end);
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Tools/datatype_case.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -419,21 +419,21 @@
 
 (* destruct nested patterns *)
 
-fun strip_case' dest (pat, rhs) =
+fun strip_case'' dest (pat, rhs) =
   case dest (Term.add_free_names pat []) rhs of
     SOME (exp as Free _, clauses) =>
       if member op aconv (OldTerm.term_frees pat) exp andalso
         not (exists (fn (_, rhs') =>
           member op aconv (OldTerm.term_frees rhs') exp) clauses)
       then
-        maps (strip_case' dest) (map (fn (pat', rhs') =>
+        maps (strip_case'' dest) (map (fn (pat', rhs') =>
           (subst_free [(exp, pat')] pat, rhs')) clauses)
       else [(pat, rhs)]
   | _ => [(pat, rhs)];
 
 fun gen_strip_case dest t = case dest [] t of
     SOME (x, clauses) =>
-      SOME (x, maps (strip_case' dest) clauses)
+      SOME (x, maps (strip_case'' dest) clauses)
   | NONE => NONE;
 
 val strip_case = gen_strip_case oo dest_case;
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/BinBoolList.thy
--- a/src/HOL/Word/BinBoolList.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/BinBoolList.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Jeremy Dawson, NICTA
 
   contains theorems to do with integers, expressed using Pls, Min, BIT,
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/BinGeneral.thy
--- a/src/HOL/Word/BinGeneral.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/BinGeneral.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Jeremy Dawson, NICTA
 
   contains basic definition to do with integers
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/BinOperations.thy
--- a/src/HOL/Word/BinOperations.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/BinOperations.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Jeremy Dawson and Gerwin Klein, NICTA
 
   definition and basic theorems for bit-wise logical operations 
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/BitSyntax.thy
--- a/src/HOL/Word/BitSyntax.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/BitSyntax.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Brian Huffman, PSU and Gerwin Klein, NICTA
 
   Syntactic class for bitwise operations.
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/Examples/WordExamples.thy
--- a/src/HOL/Word/Examples/WordExamples.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/Examples/WordExamples.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Gerwin Klein, NICTA
 
   Examples demonstrating and testing various word operations.
@@ -7,9 +6,14 @@
 
 header "Examples of word operations"
 
-theory WordExamples imports WordMain
+theory WordExamples
+imports Word
 begin
 
+types word32 = "32 word"
+types word8 = "8 word"
+types byte = word8
+
 -- "modulus"
 
 lemma "(27 :: 4 word) = -5" by simp
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/ROOT.ML
--- a/src/HOL/Word/ROOT.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/ROOT.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -1,2 +1,1 @@
-no_document use_thys ["Infinite_Set"];
-use_thy "WordMain";
+use_thy "Word";
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/Size.thy
--- a/src/HOL/Word/Size.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/Size.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-    ID:         $Id$
     Author:     John Matthews, Galois Connections, Inc., copyright 2006
 
     A typeclass for parameterizing types by size.
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/TdThs.thy
--- a/src/HOL/Word/TdThs.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/TdThs.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-    ID:         $Id$
     Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
   consequences of type definition theorems, 
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/Word.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Word/Word.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -0,0 +1,13 @@
+(*  Title:      HOL/Word/Word.thy
+    Author:     Gerwin Klein, NICTA
+*)
+
+header {* Word Library interafce *}
+
+theory Word
+imports WordGenLib
+begin
+
+text {* see @{text "Examples/WordExamples.thy"} for examples *}
+
+end
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/WordArith.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-    ID:         $Id$
     Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
   contains arithmetic theorems for word, instantiations to
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/WordBitwise.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-    ID:         $Id$
     Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
   contains theorems to do with bit-wise (logical) operations on words
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordDefinition.thy
--- a/src/HOL/Word/WordDefinition.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/WordDefinition.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-  ID:     $Id$
   Author: Jeremy Dawson and Gerwin Klein, NICTA
   
   Basic definition of word type and basic theorems following from 
@@ -12,8 +11,50 @@
 imports Size BinBoolList TdThs
 begin
 
-typedef (open word) 'a word
-  = "{(0::int) ..< 2^len_of TYPE('a::len0)}" by auto
+subsection {* Type definition *}
+
+typedef (open word) 'a word = "{(0::int) ..< 2^len_of TYPE('a::len0)}"
+  morphisms uint Abs_word by auto
+
+definition word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word" where
+  -- {* representation of words using unsigned or signed bins, 
+        only difference in these is the type class *}
+  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
+
+lemma uint_word_of_int [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = w mod 2 ^ len_of TYPE('a)"
+  by (auto simp add: word_of_int_def bintrunc_mod2p intro: Abs_word_inverse)
+
+code_datatype word_of_int
+
+
+subsection {* Type conversions and casting *}
+
+definition sint :: "'a :: len word => int" where
+  -- {* treats the most-significant-bit as a sign bit *}
+  sint_uint: "sint w = sbintrunc (len_of TYPE ('a) - 1) (uint w)"
+
+definition unat :: "'a :: len0 word => nat" where
+  "unat w = nat (uint w)"
+
+definition uints :: "nat => int set" where
+  -- "the sets of integers representing the words"
+  "uints n = range (bintrunc n)"
+
+definition sints :: "nat => int set" where
+  "sints n = range (sbintrunc (n - 1))"
+
+definition unats :: "nat => nat set" where
+  "unats n = {i. i < 2 ^ n}"
+
+definition norm_sint :: "nat => int => int" where
+  "norm_sint n w = (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+
+definition scast :: "'a :: len word => 'b :: len word" where
+  -- "cast a word to a different length"
+  "scast w = word_of_int (sint w)"
+
+definition ucast :: "'a :: len0 word => 'b :: len0 word" where
+  "ucast w = word_of_int (uint w)"
 
 instantiation word :: (len0) size
 begin
@@ -25,83 +66,39 @@
 
 end
 
-definition
-  -- {* representation of words using unsigned or signed bins, 
-        only difference in these is the type class *}
-  word_of_int :: "int \<Rightarrow> 'a\<Colon>len0 word"
-where
-  [code del]: "word_of_int w = Abs_word (bintrunc (len_of TYPE ('a)) w)" 
-
-code_datatype word_of_int
-
+definition source_size :: "('a :: len0 word => 'b) => nat" where
+  -- "whether a cast (or other) function is to a longer or shorter length"
+  "source_size c = (let arb = undefined ; x = c arb in size arb)"  
 
-subsection "Type conversions and casting"
+definition target_size :: "('a => 'b :: len0 word) => nat" where
+  "target_size c = size (c undefined)"
 
-constdefs
-  -- {* uint and sint cast a word to an integer,
-        uint treats the word as unsigned,
-        sint treats the most-significant-bit as a sign bit *}
-  uint :: "'a :: len0 word => int"
-  "uint w == Rep_word w"
-  sint :: "'a :: len word => int"
-  sint_uint: "sint w == sbintrunc (len_of TYPE ('a) - 1) (uint w)"
-  unat :: "'a :: len0 word => nat"
-  "unat w == nat (uint w)"
+definition is_up :: "('a :: len0 word => 'b :: len0 word) => bool" where
+  "is_up c \<longleftrightarrow> source_size c <= target_size c"
 
-  -- "the sets of integers representing the words"
-  uints :: "nat => int set"
-  "uints n == range (bintrunc n)"
-  sints :: "nat => int set"
-  "sints n == range (sbintrunc (n - 1))"
-  unats :: "nat => nat set"
-  "unats n == {i. i < 2 ^ n}"
-  norm_sint :: "nat => int => int"
-  "norm_sint n w == (w + 2 ^ (n - 1)) mod 2 ^ n - 2 ^ (n - 1)"
+definition is_down :: "('a :: len0 word => 'b :: len0 word) => bool" where
+  "is_down c \<longleftrightarrow> target_size c <= source_size c"
 
-  -- "cast a word to a different length"
-  scast :: "'a :: len word => 'b :: len word"
-  "scast w == word_of_int (sint w)"
-  ucast :: "'a :: len0 word => 'b :: len0 word"
-  "ucast w == word_of_int (uint w)"
+definition of_bl :: "bool list => 'a :: len0 word" where
+  "of_bl bl = word_of_int (bl_to_bin bl)"
 
-  -- "whether a cast (or other) function is to a longer or shorter length"
-  source_size :: "('a :: len0 word => 'b) => nat"
-  "source_size c == let arb = undefined ; x = c arb in size arb"  
-  target_size :: "('a => 'b :: len0 word) => nat"
-  "target_size c == size (c undefined)"
-  is_up :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_up c == source_size c <= target_size c"
-  is_down :: "('a :: len0 word => 'b :: len0 word) => bool"
-  "is_down c == target_size c <= source_size c"
+definition to_bl :: "'a :: len0 word => bool list" where
+  "to_bl w = bin_to_bl (len_of TYPE ('a)) (uint w)"
 
-constdefs
-  of_bl :: "bool list => 'a :: len0 word" 
-  "of_bl bl == word_of_int (bl_to_bin bl)"
-  to_bl :: "'a :: len0 word => bool list"
-  "to_bl w == 
-  bin_to_bl (len_of TYPE ('a)) (uint w)"
+definition word_reverse :: "'a :: len0 word => 'a word" where
+  "word_reverse w = of_bl (rev (to_bl w))"
 
-  word_reverse :: "'a :: len0 word => 'a word"
-  "word_reverse w == of_bl (rev (to_bl w))"
-
-constdefs
-  word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b"
-  "word_int_case f w == f (uint w)"
+definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
+  "word_int_case f w = f (uint w)"
 
 syntax
   of_int :: "int => 'a"
 translations
-  "case x of of_int y => b" == "word_int_case (%y. b) x"
+  "case x of of_int y => b" == "CONST word_int_case (%y. b) x"
 
 
 subsection  "Arithmetic operations"
 
-declare uint_def [code del]
-
-lemma [code]: "uint (word_of_int w \<Colon> 'a\<Colon>len0 word) = bintrunc (len_of TYPE('a)) w"
-  by (auto simp add: uint_def word_of_int_def intro!: Abs_word_inverse)
-    (insert range_bintrunc, auto)
-
 instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
 begin
 
@@ -186,8 +183,6 @@
 
 subsection "Bit-wise operations"
 
-
-
 instantiation word :: (len0) bits
 begin
 
@@ -337,21 +332,21 @@
   unfolding atLeastLessThan_alt by auto
 
 lemma 
-  Rep_word_0:"0 <= Rep_word x" and 
-  Rep_word_lt: "Rep_word (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
-  by (auto simp: Rep_word [simplified])
+  uint_0:"0 <= uint x" and 
+  uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
+  by (auto simp: uint [simplified])
 
-lemma Rep_word_mod_same:
-  "Rep_word x mod 2 ^ len_of TYPE('a) = Rep_word (x::'a::len0 word)"
-  by (simp add: int_mod_eq Rep_word_lt Rep_word_0)
+lemma uint_mod_same:
+  "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
+  by (simp add: int_mod_eq uint_lt uint_0)
 
 lemma td_ext_uint: 
   "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0))) 
     (%w::int. w mod 2 ^ len_of TYPE('a))"
   apply (unfold td_ext_def')
-  apply (simp add: uints_num uint_def word_of_int_def bintrunc_mod2p)
-  apply (simp add: Rep_word_mod_same Rep_word_0 Rep_word_lt
-                   word.Rep_word_inverse word.Abs_word_inverse int_mod_lem)
+  apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
+  apply (simp add: uint_mod_same uint_0 uint_lt
+                   word.uint_inverse word.Abs_word_inverse int_mod_lem)
   done
 
 lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
@@ -793,10 +788,7 @@
 lemmas is_down = is_down_def [unfolded source_size target_size]
 lemmas is_up = is_up_def [unfolded source_size target_size]
 
-lemmas is_up_down = 
-  trans [OF is_up [THEN meta_eq_to_obj_eq] 
-            is_down [THEN meta_eq_to_obj_eq, symmetric], 
-         standard]
+lemmas is_up_down =  trans [OF is_up is_down [symmetric], standard]
 
 lemma down_cast_same': "uc = ucast ==> is_down uc ==> uc = scast"
   apply (unfold is_down)
@@ -950,4 +942,17 @@
 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
 lemmas word_log_bin_defs = word_log_defs
 
+text {* Executable equality *}
+
+instantiation word :: ("{len0}") eq
+begin
+
+definition eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool" where
+  "eq_word k l \<longleftrightarrow> HOL.eq (uint k) (uint l)"
+
+instance proof
+qed (simp add: eq eq_word_def)
+
 end
+
+end
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordGenLib.thy
--- a/src/HOL/Word/WordGenLib.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/WordGenLib.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* Author: Gerwin Klein, Jeremy Dawson
-   $Id$
 
    Miscellaneous additional library definitions and lemmas for 
    the word type. Instantiation to boolean algebras, definition
@@ -452,4 +451,13 @@
   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   by unat_arith
 
+
+lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
+lemmas word_no_0 [simp] = word_0_no [symmetric]
+
+declare word_0_bl [simp]
+declare bin_to_bl_def [simp]
+declare to_bl_0 [simp]
+declare of_bl_True [simp]
+
 end
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordMain.thy
--- a/src/HOL/Word/WordMain.thy	Thu Jan 22 06:42:05 2009 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,30 +0,0 @@
-(* 
-  ID:     $Id$
-  Author: Gerwin Klein, NICTA
-
-  The main interface of the word library to other theories.
-*)
-
-header {* Main Word Library *}
-
-theory WordMain
-imports WordGenLib
-begin
-
-lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
-lemmas word_no_0 [simp] = word_0_no [symmetric]
-
-declare word_0_bl [simp]
-declare bin_to_bl_def [simp]
-declare to_bl_0 [simp]
-declare of_bl_True [simp]
-
-text "Examples"
-
-types word32 = "32 word"
-types word8 = "8 word"
-types byte = word8
-
-text {* for more see WordExamples.thy *}
-
-end
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOL/Word/WordShift.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -1,5 +1,4 @@
 (* 
-    ID:         $Id$
     Author:     Jeremy Dawson and Gerwin Klein, NICTA
 
   contains theorems to do with shifting, rotating, splitting words
diff -r c8c67557f187 -r fd39a59cbeb4 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/HOLCF/Pcpo.thy	Tue Jan 27 22:39:41 2009 -0800
@@ -14,7 +14,7 @@
 
 class cpo = po +
         -- {* class axiom: *}
-  assumes cpo:   "chain S \<Longrightarrow> \<exists>x. range S <<| x"
+  assumes cpo:   "chain S \<Longrightarrow> \<exists>x :: 'a::po. range S <<| x"
 
 text {* in cpo's everthing equal to THE lub has lub properties for every chain *}
 
@@ -257,10 +257,10 @@
 class finite_po = finite + po
 
 class chfin = po +
-  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n Y"
+  assumes chfin: "chain Y \<Longrightarrow> \<exists>n. max_in_chain n (Y :: nat => 'a::po)"
 
 class flat = pcpo +
-  assumes ax_flat: "x \<sqsubseteq> y \<Longrightarrow> (x = \<bottom>) \<or> (x = y)"
+  assumes ax_flat: "(x :: 'a::pcpo) \<sqsubseteq> y \<Longrightarrow> x = \<bottom> \<or> x = y"
 
 text {* finite partial orders are chain-finite *}
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Isar/class.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -33,11 +33,15 @@
     val empty_ctxt = ProofContext.init thy;
 
     (* instantiation of canonical interpretation *)
-    (*FIXME inst_morph should be calculated manually and not instantiate constraint*)
     val aT = TFree (Name.aT, base_sort);
+    val param_map_const = (map o apsnd) Const param_map;
+    val param_map_inst = (map o apsnd)
+      (Const o apsnd (map_atyps (K aT))) param_map;
+    val const_morph = Element.inst_morphism thy
+      (Symtab.empty, Symtab.make param_map_inst);
     val (([props], [(_, inst_morph)], export_morph), _) = empty_ctxt
       |> Expression.cert_goal_expression ([(class, (("", false),
-           Expression.Named ((map o apsnd) Const param_map)))], []);
+           Expression.Named param_map_const))], []);
 
     (* witness for canonical interpretation *)
     val prop = try the_single props;
@@ -63,20 +67,18 @@
     (* assm_intro *)
     fun prove_assm_intro thm = 
       let
-        val prop = thm |> Thm.prop_of |> Logic.unvarify
-          |> Morphism.term (inst_morph $> eq_morph) 
-          |> (map_types o map_atyps) (K aT);
-        fun tac ctxt = LocalDefs.unfold_tac ctxt (map Thm.symmetric defs) (*FIXME*)
-          THEN ALLGOALS (ProofContext.fact_tac [thm]);
-      in Goal.prove_global thy [] [] prop (tac o #context) end;
+        val ((_, [thm']), _) = Variable.import_thms true [thm] empty_ctxt;
+        val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
+        val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
+      in Goal.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     val assm_intro = Option.map prove_assm_intro
       (fst (Locale.intros_of thy class));
 
     (* of_class *)
     val of_class_prop_concl = Logic.mk_inclass (aT, class);
     val of_class_prop = case prop of NONE => of_class_prop_concl
-      | SOME prop => Logic.mk_implies (Morphism.term inst_morph prop,
-          of_class_prop_concl) |> (map_types o map_atyps) (K aT)
+      | SOME prop => Logic.mk_implies (Morphism.term const_morph
+          ((map_types o map_atyps) (K aT) prop), of_class_prop_concl);
     val sup_of_classes = map (snd o rules thy) sups;
     val loc_axiom_intros = map Drule.standard' (Locale.axioms_of thy class);
     val axclass_intro = #intro (AxClass.get_info thy class);
@@ -89,20 +91,32 @@
 
   in (base_morph, morph, export_morph, axiom, assm_intro, of_class) end;
 
+val reject_bcd_etc = (map o map_atyps) (fn T as TFree (v, sort) =>
+      if v = Name.aT then T
+      else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification")
+  | T => T);
+
+fun singleton_fixate thy algebra Ts =
+  let
+    fun extract f = (fold o fold_atyps) f Ts [];
+    val tfrees = extract
+      (fn TFree (v, sort) => insert (op =) (v, sort) | _ => I);
+    val inferred_sort = extract
+      (fn TVar (_, sort) => curry (Sorts.inter_sort algebra) sort | _ => I);
+    val fixate_sort = if null tfrees then inferred_sort
+      else let val a_sort = (snd o the_single) tfrees
+      in if Sorts.sort_le algebra (a_sort, inferred_sort)
+        then Sorts.inter_sort algebra (a_sort, inferred_sort)
+        else error ("Type inference imposes additional sort constraint "
+          ^ Syntax.string_of_sort_global thy inferred_sort
+          ^ " of type parameter " ^ Name.aT ^ " of sort "
+          ^ Syntax.string_of_sort_global thy a_sort)
+      end
+  in (map o map_atyps) (K (TFree (Name.aT, fixate_sort))) Ts end;
+
 fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
   let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
 
-val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
-      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
-      else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
-        (*FIXME does not occur*)
-  | T as TFree (v, sort) =>
-      if v = Name.aT then T
-      else error ("No type variable other than " ^ Name.aT ^ " allowed in class specification"));
-
-val singleton_fixate = (map o map_atyps) (fn TVar (vi, sort)
-  => TFree (Name.aT, sort) | T => T);
-
 fun add_tfrees_of_element (Element.Fixes fxs) = fold (fn (_, SOME T, _) => Term.add_tfreesT T
       | _ => I) fxs
   | add_tfrees_of_element (Element.Constrains cnstrs) = fold (Term.add_tfreesT o snd) cnstrs
@@ -140,8 +154,9 @@
         (these_operations thy sups);
     val ((_, _, inferred_elems), _) = ProofContext.init thy
       |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
-      |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
-      |> add_typ_check ~2 "singleton_fixate" singleton_fixate
+      |> redeclare_operations thy sups
+      |> add_typ_check 10 "reject_bcd_etc" reject_bcd_etc
+      |> add_typ_check ~10 "singleton_fixate" (singleton_fixate thy (Sign.classes_of thy))
       |> prep_decl supexpr raw_elems;
     (*FIXME check for *all* side conditions here, extra check function for elements,
       less side-condition checks in check phase*)
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Isar/class_target.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -29,6 +29,7 @@
     -> (string * mixfix) * term -> theory -> theory
   val class_prefix: string -> string
   val refresh_syntax: class -> Proof.context -> Proof.context
+  val redeclare_operations: theory -> sort -> Proof.context -> Proof.context
 
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
@@ -298,6 +299,10 @@
 fun these_unchecks thy =
   map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
 
+fun redeclare_const thy c =
+  let val b = Sign.base_name c
+  in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
+
 fun synchronize_class_syntax sort base_sort ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -308,9 +313,6 @@
       (map o apsnd) (subst_class_typ base_sort o fst o snd) operations;
     val secondary_constraints =
       (map o apsnd) (fn (class, (ty, _)) => subst_class_typ [class] ty) operations;
-    fun declare_const (c, _) =
-      let val b = Sign.base_name c
-      in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
     fun improve (c, ty) = (case AList.lookup (op =) primary_constraints c
      of SOME ty' => (case try (Type.raw_match (ty', ty)) Vartab.empty
          of SOME tyenv => (case Vartab.lookup tyenv (Name.aT, 0)
@@ -326,7 +328,7 @@
     val unchecks = these_unchecks thy sort;
   in
     ctxt
-    |> fold declare_const primary_constraints
+    |> fold (redeclare_const thy o fst) primary_constraints
     |> Overloading.map_improvable_syntax (K (((primary_constraints, secondary_constraints),
         (((improve, subst), true), unchecks)), false))
     |> Overloading.set_primary_constraints
@@ -338,6 +340,9 @@
     val base_sort = base_sort thy class;
   in synchronize_class_syntax [class] base_sort ctxt end;
 
+fun redeclare_operations thy sort =
+  fold (redeclare_const thy o fst) (these_operations thy sort);
+
 fun begin sort base_sort ctxt =
   ctxt
   |> Variable.declare_term
@@ -489,7 +494,8 @@
   let
     val _ = if null tycos then error "At least one arity must be given" else ();
     val params = these_params thy sort;
-    fun get_param tyco (param, (_, (c, ty))) = if can (AxClass.param_of_inst thy) (c, tyco)
+    fun get_param tyco (param, (_, (c, ty))) =
+      if can (AxClass.param_of_inst thy) (c, tyco)
       then NONE else SOME ((c, tyco),
         (param ^ "_" ^ type_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
     val inst_params = map_product get_param tycos params |> map_filter I;
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Isar/isar_document.scala	Tue Jan 27 22:39:41 2009 -0800
@@ -6,36 +6,39 @@
 
 package isabelle
 
-
-object IsarDocument
-{
+object IsarDocument {
   /* unique identifiers */
 
   type State_ID = String
   type Command_ID = String
   type Document_ID = String
+}
+
+trait IsarDocument extends IsabelleProcess
+{
+  import IsarDocument._
 
 
   /* commands */
 
-  def define_command(proc: IsabelleProcess, id: Command_ID, text: String) {
-    proc.output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
+  def define_command(id: Command_ID, text: String) {
+    output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
       IsabelleSyntax.encode_string(text))
   }
 
 
   /* documents */
 
-  def begin_document(proc: IsabelleProcess, id: Document_ID, path: String) {
-    proc.output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
+  def begin_document(id: Document_ID, path: String) {
+    output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
        IsabelleSyntax.encode_string(path))
   }
 
-  def end_document(proc: IsabelleProcess, id: Document_ID) {
-    proc.output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
+  def end_document(id: Document_ID) {
+    output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
   }
 
-  def edit_document(proc: IsabelleProcess, old_id: Document_ID, new_id: Document_ID,
+  def edit_document(old_id: Document_ID, new_id: Document_ID,
       edits: List[(Command_ID, Option[Command_ID])])
   {
     def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
@@ -56,6 +59,6 @@
     IsabelleSyntax.append_string(new_id, buf)
     buf.append(" ")
     IsabelleSyntax.append_list(append_edit, edits, buf)
-    proc.output_sync(buf.toString)
+    output_sync(buf.toString)
   }
 }
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -10,3 +10,5 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -8,3 +8,6 @@
 use "ML-Systems/polyml_old_compiler5.ML";
 
 val pointer_eq = PolyML.pointerEq;
+
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -12,6 +12,8 @@
 
 val pointer_eq = PolyML.pointerEq;
 
+fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
+
 
 (* runtime compilation *)
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Proof/extraction.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -546,7 +546,7 @@
 
       | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
           let
-            val prf = force_proof body;
+            val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
             val T = etype_of thy' vs' [] prop;
@@ -570,7 +570,7 @@
                       (proof_combt
                          (PThm (serial (),
                           ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                            Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
+                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop))
                   in
                     ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
@@ -636,7 +636,7 @@
 
       | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
           let
-            val prf = force_proof body;
+            val prf = join_proof body;
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
           in
@@ -681,7 +681,7 @@
                       (proof_combt
                         (PThm (serial (),
                          ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
-                           Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
+                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
                       (map (get_var_type corr_prop) (vfs_of prop));
                   in
                     ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -228,7 +228,7 @@
     val prop = Thm.full_prop_of thm;
     val prf = Thm.proof_of thm;
     val prf' = (case strip_combt (fst (strip_combP prf)) of
-        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf
+        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
       | _ => prf)
   in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Proof/reconstruct.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -358,7 +358,7 @@
                     val _ = message ("Reconstructing proof of " ^ a);
                     val _ = message (Syntax.string_of_term_global thy prop);
                     val prf' = forall_intr_vfs_prf prop
-                      (reconstruct_proof thy prop (force_proof body));
+                      (reconstruct_proof thy prop (join_proof body));
                     val (maxidx', prfs', prf) = expand
                       (maxidx_proof prf' ~1) prfs prf'
                   in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -256,7 +256,7 @@
   (case Thm.proof_body_of th of 
     PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
       if Thm.has_name_hint th andalso Thm.get_name_hint th = name
-      then add_proof_body (Lazy.force body)
+      then add_proof_body (Future.join body)
       else I
   | body => add_proof_body body);
 
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/Tools/xml_syntax.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -158,7 +158,7 @@
   | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
       (* FIXME? *)
       PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
-        Lazy.value (Proofterm.make_proof_body MinProof)))
+        Future.value (Proofterm.make_proof_body MinProof)))
   | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
       PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
   | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/proofterm.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -21,10 +21,10 @@
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
    | Promise of serial * term * typ list
-   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
+   | PThm of serial * ((string * term * typ list option) * proof_body future)
   and proof_body = PBody of
     {oracles: (string * term) OrdList.T,
-     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
+     thms: (serial * (string * term * proof_body future)) OrdList.T,
      proof: proof}
 
   val %> : proof * term -> proof
@@ -35,10 +35,10 @@
   include BASIC_PROOFTERM
 
   type oracle = string * term
-  type pthm = serial * (string * term * proof_body lazy)
-  val force_body: proof_body lazy ->
+  type pthm = serial * (string * term * proof_body future)
+  val join_body: proof_body future ->
     {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
-  val force_proof: proof_body lazy -> proof
+  val join_proof: proof_body future -> proof
   val proof_of: proof_body -> proof
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
@@ -110,7 +110,7 @@
   val promise_proof: theory -> serial -> term -> proof
   val fulfill_proof: theory -> (serial * proof) list -> proof_body -> proof_body
   val thm_proof: theory -> string -> term list -> term ->
-    (serial * proof) list lazy -> proof_body -> pthm * proof
+    (serial * proof future) list -> proof_body -> pthm * proof
   val get_name: term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
@@ -142,17 +142,17 @@
  | PAxm of string * term * typ list option
  | Oracle of string * term * typ list option
  | Promise of serial * term * typ list
- | PThm of serial * ((string * term * typ list option) * proof_body lazy)
+ | PThm of serial * ((string * term * typ list option) * proof_body future)
 and proof_body = PBody of
   {oracles: (string * term) OrdList.T,
-   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
+   thms: (serial * (string * term * proof_body future)) OrdList.T,
    proof: proof};
 
 type oracle = string * term;
-type pthm = serial * (string * term * proof_body lazy);
+type pthm = serial * (string * term * proof_body future);
 
-val force_body = Lazy.force #> (fn PBody args => args);
-val force_proof = #proof o force_body;
+val join_body = Future.join #> (fn PBody args => args);
+val join_proof = #proof o join_body;
 
 fun proof_of (PBody {proof, ...}) = proof;
 
@@ -165,7 +165,7 @@
       if Inttab.defined seen i then (x, seen)
       else
         let
-          val body' = Lazy.force body;
+          val body' = Future.join body;
           val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
         in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
@@ -180,7 +180,7 @@
           if Inttab.defined seen i then (x, seen)
           else
             let val (x', seen') =
-              (if all then app (force_proof body) else I) (x, Inttab.update (i, ()) seen)
+              (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
             in (f prf x', seen') end)
       | app prf = (fn (x, seen) => (f prf x, seen));
   in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
@@ -233,7 +233,7 @@
 
 fun strip_thm (body as PBody {proof, ...}) =
   (case strip_combt (fst (strip_combP proof)) of
-    (PThm (_, (_, body')), _) => Lazy.force body'
+    (PThm (_, (_, body')), _) => Future.join body'
   | _ => body);
 
 val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
@@ -1227,6 +1227,11 @@
         val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
       in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
+fun fulfill_proof_future _ [] body = Future.value body
+  | fulfill_proof_future thy promises body =
+      Future.fork_deps (map snd promises) (fn () =>
+        fulfill_proof thy (map (apsnd Future.join) promises) body);
+
 
 (***** theorems *****)
 
@@ -1243,11 +1248,9 @@
       if ! proofs = 2 then
         #4 (shrink_proof thy [] 0 (rew_proof thy (fold_rev implies_intr_proof hyps prf)))
       else MinProof;
+    val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
 
-    fun new_prf () = (serial (), name, prop,
-      Lazy.lazy (fn () => fulfill_proof thy (Lazy.force promises)
-        (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
-
+    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
     val (i, name, prop, body') =
       (case strip_combt (fst (strip_combP prf)) of
         (PThm (i, ((old_name, prop', NONE), body')), args') =>
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/pure_setup.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -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", "T"] (Pretty.pprint o Pretty.str o Binding.display));
+install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
 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);
diff -r c8c67557f187 -r fd39a59cbeb4 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Jan 22 06:42:05 2009 -0800
+++ b/src/Pure/thm.ML	Tue Jan 27 22:39:41 2009 -0800
@@ -1658,7 +1658,7 @@
     val {thy_ref, hyps, prop, tpairs, ...} = args;
     val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
 
-    val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
+    val ps = map (apsnd (Future.map proof_of)) promises;
     val thy = Theory.deref thy_ref;
     val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;