merged

--- a/Admin/isatest/isatest-makeall	Wed Nov 21 16:32:34 2012 +0100
+++ b/Admin/isatest/isatest-makeall	Wed Nov 21 16:43:14 2012 +0100
@@ -47,7 +47,7 @@
 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
 
 # build args and nice setup for different target platforms
-BUILD_ARGS="-v -o timeout=3600"
+BUILD_ARGS="-v"
 NICE="nice"
 case $HOSTNAME in
     macbroy2 | macbroy6 | macbroy30)
@@ -85,6 +85,15 @@
 
     [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
 
+    case "$SETTINGS" in
+      *sml*)
+        BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
+        ;;
+      *)
+        BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
+        ;;
+    esac
+
     # logfile setup
 
     DATE=$(date "+%Y-%m-%d")

--- a/src/HOL/Library/Countable_Set.thy	Wed Nov 21 16:32:34 2012 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Wed Nov 21 16:43:14 2012 +0100
@@ -89,7 +89,7 @@
   using countableE_infinite unfolding to_nat_on_def
   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
 
-lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
+lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
   unfolding from_nat_into_def[abs_def]
   using to_nat_on_finite[of S]
   apply (subst bij_betw_cong)
@@ -99,7 +99,7 @@
               intro: bij_betw_inv_into to_nat_on_finite)
   done
 
-lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
+lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
   unfolding from_nat_into_def[abs_def]
   using to_nat_on_infinite[of S, unfolded bij_betw_def]
   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
@@ -124,7 +124,7 @@
 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
   using from_nat_into[of A] by auto
 
-lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A"
+lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
   by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
 
 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
@@ -136,32 +136,32 @@
 lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
   by (simp add: f_inv_into_f from_nat_into_def)
 
-lemma infinite_to_nat_on_from_nat_into[simp]:
+lemma to_nat_on_from_nat_into_infinite[simp]:
   "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
   by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
 
 lemma from_nat_into_inj:
-  assumes c: "countable A" and i: "infinite A"
-  shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
-proof-
-  have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R"
-  unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]]
-                               from_nat_into[OF infinite_imp_nonempty[OF i]]] ..
-  also have "... \<longleftrightarrow> ?K" using c i by simp
-  finally show ?thesis .
-qed
+  "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
+    from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
+  by (subst to_nat_on_inj[symmetric, of A]) auto
+
+lemma from_nat_into_inj_infinite[simp]:
+  "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
+  using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
+
+lemma eq_from_nat_into_iff:
+  "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x"
+  by auto
 
 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
   by (rule exI[of _ "to_nat_on A a"]) simp
 
 lemma from_nat_into_inject[simp]:
-assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
-shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
-by (metis assms from_nat_into_image)
+  "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
+  by (metis range_from_nat_into)
 
-lemma inj_on_from_nat_into:
-"inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
-unfolding inj_on_def by auto
+lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
+  unfolding inj_on_def by auto
 
 subsection {* Closure properties of countability *}
 

--- a/src/HOL/ROOT	Wed Nov 21 16:32:34 2012 +0100
+++ b/src/HOL/ROOT	Wed Nov 21 16:43:14 2012 +0100
@@ -793,7 +793,7 @@
   theories MutabelleExtra
 
 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
-  options [timeout = 3600, document = false]
+  options [timeout = 5400, document = false]
   theories
     Quickcheck_Examples
   (* FIXME