merged
authorblanchet
Tue, 27 Oct 2009 12:16:26 +0100
changeset 33231 1711610c5b7d
parent 33220 11a1af478dac (diff)
parent 33230 8b770ed796f1 (current diff)
child 33232 f93390060bbe
merged
--- a/Admin/isatest/isatest-makeall	Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/isatest-makeall	Tue Oct 27 12:16:26 2009 +0100
@@ -63,7 +63,7 @@
         ;;
   
     sunbroy2)
-        MFLAGS="-k -j 6"
+        MFLAGS="-k -j 2"
         NICE="nice"
         ;;
 
--- a/Admin/isatest/isatest-makedist	Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/isatest-makedist	Tue Oct 27 12:16:26 2009 +0100
@@ -91,7 +91,7 @@
 
 ## spawn test runs
 
-#$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
+$SSH sunbroy2 "$MAKEALL $HOME/settings/sun-poly"
 # give test some time to copy settings and start
 sleep 15
 $SSH macbroy22 "$MAKEALL $HOME/settings/at-poly"
--- a/Admin/isatest/settings/sun-poly	Mon Oct 26 18:52:29 2009 +0100
+++ b/Admin/isatest/settings/sun-poly	Tue Oct 27 12:16:26 2009 +0100
@@ -23,6 +23,6 @@
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 
 #ISABELLE_USEDIR_OPTIONS="-i true -d dvi -g true -v true"
-ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 1"
+ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true -M 6 -q 2"
 
 HOL_USEDIR_OPTIONS="-p 0" 
--- a/doc/Contents	Mon Oct 26 18:52:29 2009 +0100
+++ b/doc/Contents	Tue Oct 27 12:16:26 2009 +0100
@@ -6,6 +6,7 @@
   classes         Tutorial on Type Classes
   functions       Tutorial on Function Definitions
   codegen         Tutorial on Code Generation
+  nitpick         User's Guide to Nitpick in Isabelle/HOL
   sugar           LaTeX Sugar for Isabelle documents
 
 Reference Manuals
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -2993,7 +2993,7 @@
  | Const(@{const_name "power"},_)$a$n => FRPar.Pw (num_of_term m a, dest_nat n)
  | Const(@{const_name "HOL.divide"},_)$a$b => FRPar.C (HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
  | _ => (FRPar.C (HOLogic.dest_number t |> snd,1) 
-         handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> valOf));
+         handle TERM _ => FRPar.Bound (AList.lookup (op aconv) m t |> the));
 
 fun tm_of_term m m' t = 
  case t of
@@ -3002,14 +3002,14 @@
  | Const(@{const_name "HOL.minus"},_)$a$b => FRPar.tm_Sub (tm_of_term m m' a, tm_of_term m m' b)
  | Const(@{const_name "HOL.times"},_)$a$b => FRPar.tm_Mul (num_of_term m' a, tm_of_term m m' b)
  | _ => (FRPar.CP (num_of_term m' t) 
-         handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf)
-              | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> valOf));
+         handle TERM _ => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the)
+              | Option => FRPar.tm_Bound (AList.lookup (op aconv) m t |> the));
 
 fun term_of_num T m t = 
  case t of
   FRPar.C (a,b) => (if b = 1 then num T a else if b=0 then (rz T) 
                                         else (divt T) $ num T a $ num T b)
-| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.Bound i => AList.lookup (op = : int*int -> bool) m i |> the
 | FRPar.Add(a,b) => (plust T)$(term_of_num T m a)$(term_of_num T m b)
 | FRPar.Mul(a,b) => (timest T)$(term_of_num T m a)$(term_of_num T m b)
 | FRPar.Sub(a,b) => (minust T)$(term_of_num T m a)$(term_of_num T m b)
@@ -3021,7 +3021,7 @@
 fun term_of_tm T m m' t = 
  case t of
   FRPar.CP p => term_of_num T m' p
-| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> valOf
+| FRPar.tm_Bound i => AList.lookup (op = : int*int -> bool) m i |> the
 | FRPar.tm_Add(a,b) => (plust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
 | FRPar.tm_Mul(a,b) => (timest T)$(term_of_num T m' a)$(term_of_tm T m m' b)
 | FRPar.tm_Sub(a,b) => (minust T)$(term_of_tm T m m' a)$(term_of_tm T m m' b)
--- a/src/HOL/Induct/LList.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Induct/LList.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Induct/LList.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
 
 Shares NIL, CONS, List_case with List.thy
@@ -906,8 +905,8 @@
 by (rule_tac l = l1 in llist_fun_equalityI, auto)
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
-                            (map dest_Const [@{term LNil}, @{term LCons}])
+  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+    (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 end
--- a/src/HOL/IsaMakefile	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/IsaMakefile	Tue Oct 27 12:16:26 2009 +0100
@@ -6,7 +6,20 @@
 
 default: HOL
 generate: HOL-Generate-HOL HOL-Generate-HOLLight
-images: HOL HOL-Base HOL-Plain HOL-Main HOL-Algebra HOL-Nominal HOL-NSA HOL-SMT HOL-Word TLA HOL4
+
+images: \
+  HOL \
+  HOL-Algebra \
+  HOL-Base \
+  HOL-Main \
+  HOL-Multivariate_Analysis \
+  HOL-NSA \
+  HOL-Nominal \
+  HOL-Plain \
+  HOL-SMT \
+  HOL-Word \
+  HOL4 \
+  TLA
 
 #Note: keep targets sorted (except for HOL-Library and HOL-ex)
 test: \
@@ -19,11 +32,11 @@
   HOL-Hahn_Banach \
   HOL-Hoare \
   HOL-Hoare_Parallel \
-  HOL-Import \
   HOL-IMP \
   HOL-IMPP \
   HOL-IOA \
   HOL-Imperative_HOL \
+  HOL-Import \
   HOL-Induct \
   HOL-Isar_Examples \
   HOL-Lambda \
@@ -33,7 +46,6 @@
   HOL-MicroJava \
   HOL-Mirabelle \
   HOL-Modelcheck \
-  HOL-Multivariate_Analysis \
   HOL-NanoJava \
   HOL-Nitpick_Examples \
   HOL-Nominal-Examples \
@@ -41,13 +53,13 @@
   HOL-Old_Number_Theory \
   HOL-Prolog \
   HOL-SET_Protocol \
+  HOL-SMT-Examples \
   HOL-SizeChange \
-  HOL-SMT-Examples \
   HOL-Statespace \
   HOL-Subst \
-  TLA-Buffer \
-  TLA-Inc \
-  TLA-Memory \
+      TLA-Buffer \
+      TLA-Inc \
+      TLA-Memory \
   HOL-UNITY \
   HOL-Unix \
   HOL-W0 \
--- a/src/HOL/Library/Coinductive_List.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -850,8 +850,8 @@
 qed
 
 setup {*
-Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
-                            (map dest_Const [@{term LNil}, @{term LCons}])
+  Nitpick.register_codatatype @{typ "'a llist"} @{const_name llist_case}
+    (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
 end
--- a/src/HOL/Rational.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Rational.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -1064,22 +1064,22 @@
 *}
 
 setup {*
-Nitpick.register_frac_type @{type_name rat}
-    [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
-     (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
-     (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
-     (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
-     (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
-     (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
-     (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
-     (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
-     (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
-     (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
+  Nitpick.register_frac_type @{type_name rat}
+   [(@{const_name zero_rat_inst.zero_rat}, @{const_name Nitpick.zero_frac}),
+    (@{const_name one_rat_inst.one_rat}, @{const_name Nitpick.one_frac}),
+    (@{const_name plus_rat_inst.plus_rat}, @{const_name Nitpick.plus_frac}),
+    (@{const_name times_rat_inst.times_rat}, @{const_name Nitpick.times_frac}),
+    (@{const_name uminus_rat_inst.uminus_rat}, @{const_name Nitpick.uminus_frac}),
+    (@{const_name number_rat_inst.number_of_rat}, @{const_name Nitpick.number_of_frac}),
+    (@{const_name inverse_rat_inst.inverse_rat}, @{const_name Nitpick.inverse_frac}),
+    (@{const_name ord_rat_inst.less_eq_rat}, @{const_name Nitpick.less_eq_frac}),
+    (@{const_name field_char_0_class.of_rat}, @{const_name Nitpick.of_frac}),
+    (@{const_name field_char_0_class.Rats}, @{const_name UNIV})]
 *}
 
 lemmas [nitpick_def] = inverse_rat_inst.inverse_rat
-    number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
-    plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
-    zero_rat_inst.zero_rat
+  number_rat_inst.number_of_rat one_rat_inst.one_rat ord_rat_inst.less_eq_rat
+  plus_rat_inst.plus_rat times_rat_inst.times_rat uminus_rat_inst.uminus_rat
+  zero_rat_inst.zero_rat
 
 end
--- a/src/HOL/RealDef.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/RealDef.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -1186,15 +1186,15 @@
 *}
 
 setup {*
-Nitpick.register_frac_type @{type_name real}
-    [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
-     (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
-     (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
-     (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
-     (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
-     (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
-     (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
-     (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
+  Nitpick.register_frac_type @{type_name real}
+   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),
+    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),
+    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),
+    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),
+    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),
+    (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}),
+    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),
+    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]
 *}
 
 lemmas [nitpick_def] = inverse_real_inst.inverse_real
--- a/src/HOL/Relation.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Relation.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -607,6 +607,9 @@
 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   by (auto simp:inv_image_def)
 
+lemma converse_inv_image[simp]: "(inv_image R f)^-1 = inv_image (R^-1) f"
+unfolding inv_image_def converse_def by auto
+
 
 subsection {* Finiteness *}
 
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -271,7 +271,7 @@
                     Markup.markup Markup.sendback "apply metis")
                 | ERROR msg => (false, "Error: " ^ msg);
             val _ = unregister result (Thread.self ());
-          in () end handle Exn.Interrupt => ())
+          in () end)
       in () end);
 
 
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -432,7 +432,7 @@
     if auto orelse blocking then
       go ()
     else
-      (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
+      (SimpleThread.fork true (fn () => (go (); ()));
        state)
   end
 
--- a/src/HOL/Wellfounded.thy	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Oct 27 12:16:26 2009 +0100
@@ -14,19 +14,12 @@
 
 subsection {* Basic Definitions *}
 
-constdefs
-  wf         :: "('a * 'a)set => bool"
+definition wf :: "('a * 'a) set => bool" where
   "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x. P(x)))"
 
-  wfP :: "('a => 'a => bool) => bool"
+definition wfP :: "('a => 'a => bool) => bool" where
   "wfP r == wf {(x, y). r x y}"
 
-  acyclic :: "('a*'a)set => bool"
-  "acyclic r == !x. (x,x) ~: r^+"
-
-abbreviation acyclicP :: "('a => 'a => bool) => bool" where
-  "acyclicP r == acyclic {(x, y). r x y}"
-
 lemma wfP_wf_eq [pred_set_conv]: "wfP (\<lambda>x y. (x, y) \<in> r) = wf r"
   by (simp add: wfP_def)
 
@@ -59,14 +52,16 @@
 lemma wf_not_sym: "wf r ==> (a, x) : r ==> (x, a) ~: r"
   by (induct a arbitrary: x set: wf) blast
 
-(* [| wf r;  ~Z ==> (a,x) : r;  (x,a) ~: r ==> Z |] ==> Z *)
-lemmas wf_asym = wf_not_sym [elim_format]
+lemma wf_asym:
+  assumes "wf r" "(a, x) \<in> r"
+  obtains "(x, a) \<notin> r"
+  by (drule wf_not_sym[OF assms])
 
 lemma wf_not_refl [simp]: "wf r ==> (a, a) ~: r"
   by (blast elim: wf_asym)
 
-(* [| wf r;  (a,a) ~: r ==> PROP W |] ==> PROP W *)
-lemmas wf_irrefl = wf_not_refl [elim_format]
+lemma wf_irrefl: assumes "wf r" obtains "(a, a) \<notin> r"
+by (drule wf_not_refl[OF assms])
 
 lemma wf_wellorderI:
   assumes wf: "wf {(x::'a::ord, y). x < y}"
@@ -82,7 +77,62 @@
 
 subsection {* Basic Results *}
 
-text{*transitive closure of a well-founded relation is well-founded! *}
+text {* Point-free characterization of well-foundedness *}
+
+lemma wfE_pf:
+  assumes wf: "wf R"
+  assumes a: "A \<subseteq> R `` A"
+  shows "A = {}"
+proof -
+  { fix x
+    from wf have "x \<notin> A"
+    proof induct
+      fix x assume "\<And>y. (y, x) \<in> R \<Longrightarrow> y \<notin> A"
+      then have "x \<notin> R `` A" by blast
+      with a show "x \<notin> A" by blast
+    qed
+  } thus ?thesis by auto
+qed
+
+lemma wfI_pf:
+  assumes a: "\<And>A. A \<subseteq> R `` A \<Longrightarrow> A = {}"
+  shows "wf R"
+proof (rule wfUNIVI)
+  fix P :: "'a \<Rightarrow> bool" and x
+  let ?A = "{x. \<not> P x}"
+  assume "\<forall>x. (\<forall>y. (y, x) \<in> R \<longrightarrow> P y) \<longrightarrow> P x"
+  then have "?A \<subseteq> R `` ?A" by blast
+  with a show "P x" by blast
+qed
+
+text{*Minimal-element characterization of well-foundedness*}
+
+lemma wfE_min:
+  assumes wf: "wf R" and Q: "x \<in> Q"
+  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
+  using Q wfE_pf[OF wf, of Q] by blast
+
+lemma wfI_min:
+  assumes a: "\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q"
+  shows "wf R"
+proof (rule wfI_pf)
+  fix A assume b: "A \<subseteq> R `` A"
+  { fix x assume "x \<in> A"
+    from a[OF this] b have "False" by blast
+  }
+  thus "A = {}" by blast
+qed
+
+lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
+apply auto
+apply (erule wfE_min, assumption, blast)
+apply (rule wfI_min, auto)
+done
+
+lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
+
+text{* Well-foundedness of transitive closure *}
+
 lemma wf_trancl:
   assumes "wf r"
   shows "wf (r^+)"
@@ -122,43 +172,8 @@
   apply (erule wf_trancl)
   done
 
+text {* Well-foundedness of subsets *}
 
-text{*Minimal-element characterization of well-foundedness*}
-lemma wf_eq_minimal: "wf r = (\<forall>Q x. x\<in>Q --> (\<exists>z\<in>Q. \<forall>y. (y,z)\<in>r --> y\<notin>Q))"
-proof (intro iffI strip)
-  fix Q :: "'a set" and x
-  assume "wf r" and "x \<in> Q"
-  then show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q"
-    unfolding wf_def
-    by (blast dest: spec [of _ "%x. x\<in>Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y,z) \<in> r \<longrightarrow> y\<notin>Q)"]) 
-next
-  assume 1: "\<forall>Q x. x \<in> Q \<longrightarrow> (\<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q)"
-  show "wf r"
-  proof (rule wfUNIVI)
-    fix P :: "'a \<Rightarrow> bool" and x
-    assume 2: "\<forall>x. (\<forall>y. (y, x) \<in> r \<longrightarrow> P y) \<longrightarrow> P x"
-    let ?Q = "{x. \<not> P x}"
-    have "x \<in> ?Q \<longrightarrow> (\<exists>z \<in> ?Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> ?Q)"
-      by (rule 1 [THEN spec, THEN spec])
-    then have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> (\<forall>y. (y, z) \<in> r \<longrightarrow> P y))" by simp
-    with 2 have "\<not> P x \<longrightarrow> (\<exists>z. \<not> P z \<and> P z)" by fast
-    then show "P x" by simp
-  qed
-qed
-
-lemma wfE_min: 
-  assumes "wf R" "x \<in> Q"
-  obtains z where "z \<in> Q" "\<And>y. (y, z) \<in> R \<Longrightarrow> y \<notin> Q"
-  using assms unfolding wf_eq_minimal by blast
-
-lemma wfI_min:
-  "(\<And>x Q. x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> R \<longrightarrow> y \<notin> Q)
-  \<Longrightarrow> wf R"
-  unfolding wf_eq_minimal by blast
-
-lemmas wfP_eq_minimal = wf_eq_minimal [to_pred]
-
-text {* Well-foundedness of subsets *}
 lemma wf_subset: "[| wf(r);  p<=r |] ==> wf(p)"
   apply (simp (no_asm_use) add: wf_eq_minimal)
   apply fast
@@ -167,7 +182,8 @@
 lemmas wfP_subset = wf_subset [to_pred]
 
 text {* Well-foundedness of the empty relation *}
-lemma wf_empty [iff]: "wf({})"
+
+lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
 lemma wfP_empty [iff]:
@@ -187,7 +203,20 @@
   apply (rule Int_lower2)
   done  
 
-text{*Well-foundedness of insert*}
+text {* Exponentiation *}
+
+lemma wf_exp:
+  assumes "wf (R ^^ n)"
+  shows "wf R"
+proof (rule wfI_pf)
+  fix A assume "A \<subseteq> R `` A"
+  then have "A \<subseteq> (R ^^ n) `` A" by (induct n) force+
+  with `wf (R ^^ n)`
+  show "A = {}" by (rule wfE_pf)
+qed
+
+text {* Well-foundedness of insert *}
+
 lemma wf_insert [iff]: "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"
 apply (rule iffI)
  apply (blast elim: wf_trancl [THEN wf_irrefl]
@@ -210,6 +239,7 @@
 done
 
 text{*Well-foundedness of image*}
+
 lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
 apply (simp only: wf_eq_minimal, clarify)
 apply (case_tac "EX p. f p : Q")
@@ -351,7 +381,13 @@
   by (rule wf_union_merge [where S = "{}", simplified])
 
 
-subsubsection {* acyclic *}
+subsection {* Acyclic relations *}
+
+definition acyclic :: "('a * 'a) set => bool" where
+  "acyclic r == !x. (x,x) ~: r^+"
+
+abbreviation acyclicP :: "('a => 'a => bool) => bool" where
+  "acyclicP r == acyclic {(x, y). r x y}"
 
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)
--- a/src/Pure/Concurrent/simple_thread.ML	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -15,7 +15,7 @@
 struct
 
 fun fork interrupts body =
-  Thread.fork (fn () => exception_trace (fn () => body ()),
+  Thread.fork (fn () => exception_trace (fn () => body () handle Exn.Interrupt => ()),
     if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
 
 fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
--- a/src/Pure/ML-Systems/multithreading_polyml.ML	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -33,14 +33,9 @@
 
 val max_threads = Unsynchronized.ref 0;
 
-val tested_platform =
-  let val ml_platform = getenv "ML_PLATFORM"
-  in String.isSuffix "linux" ml_platform orelse String.isSuffix "darwin" ml_platform end;
-
 fun max_threads_value () =
   let val m = ! max_threads in
     if m > 0 then m
-    else if not tested_platform then 1
     else Int.min (Int.max (Thread.numProcessors (), 1), 4)
   end;
 
--- a/src/Pure/ML-Systems/polyml_common.ML	Mon Oct 26 18:52:29 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Oct 27 12:16:26 2009 +0100
@@ -18,6 +18,9 @@
 
 val forget_structure = PolyML.Compiler.forgetStructure;
 
+val _ = PolyML.Compiler.forgetValue "isSome";
+val _ = PolyML.Compiler.forgetValue "getOpt";
+val _ = PolyML.Compiler.forgetValue "valOf";
 val _ = PolyML.Compiler.forgetValue "foldl";
 val _ = PolyML.Compiler.forgetValue "foldr";
 val _ = PolyML.Compiler.forgetValue "print";