--- 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"
--- 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"
--- 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"
--- 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}
--- 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:
--- 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}
--- 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%
%
--- 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) =
--- 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
--- 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
--- 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 *}
--- 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"
--- 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]"
--- 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>
--- 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;
--- 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);
--- 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;
--- 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,
--- 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
--- 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
--- 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.
--- 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
--- 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";
--- 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.
--- 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,
--- /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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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 *}
--- 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*)
--- 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;
--- 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)
}
}
--- 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;
+
--- 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;
+
--- 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 *)
--- 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'',
--- 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;
--- 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,
--- 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);
--- 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)) =
--- 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') =>
--- 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);
--- 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;