1.1 --- a/Admin/isatest/isatest-makeall Wed Nov 21 16:32:34 2012 +0100
1.2 +++ b/Admin/isatest/isatest-makeall Wed Nov 21 16:43:14 2012 +0100
1.3 @@ -47,7 +47,7 @@
1.4 [ -d $DISTPREFIX ] || fail "$DISTPREFIX is not a directory."
1.5
1.6 # build args and nice setup for different target platforms
1.7 -BUILD_ARGS="-v -o timeout=3600"
1.8 +BUILD_ARGS="-v"
1.9 NICE="nice"
1.10 case $HOSTNAME in
1.11 macbroy2 | macbroy6 | macbroy30)
1.12 @@ -85,6 +85,15 @@
1.13
1.14 [ -r $SETTINGS ] || fail "Cannot read $SETTINGS."
1.15
1.16 + case "$SETTINGS" in
1.17 + *sml*)
1.18 + BUILD_ARGS="-o timeout=36000 $BUILD_ARGS"
1.19 + ;;
1.20 + *)
1.21 + BUILD_ARGS="-o timeout=3600 $BUILD_ARGS"
1.22 + ;;
1.23 + esac
1.24 +
1.25 # logfile setup
1.26
1.27 DATE=$(date "+%Y-%m-%d")
2.1 --- a/src/HOL/Library/Countable_Set.thy Wed Nov 21 16:32:34 2012 +0100
2.2 +++ b/src/HOL/Library/Countable_Set.thy Wed Nov 21 16:43:14 2012 +0100
2.3 @@ -89,7 +89,7 @@
2.4 using countableE_infinite unfolding to_nat_on_def
2.5 by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
2.6
2.7 -lemma from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
2.8 +lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
2.9 unfolding from_nat_into_def[abs_def]
2.10 using to_nat_on_finite[of S]
2.11 apply (subst bij_betw_cong)
2.12 @@ -99,7 +99,7 @@
2.13 intro: bij_betw_inv_into to_nat_on_finite)
2.14 done
2.15
2.16 -lemma from_nat_into_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
2.17 +lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
2.18 unfolding from_nat_into_def[abs_def]
2.19 using to_nat_on_infinite[of S, unfolded bij_betw_def]
2.20 by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
2.21 @@ -124,7 +124,7 @@
2.22 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
2.23 using from_nat_into[of A] by auto
2.24
2.25 -lemma from_nat_into_image[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> from_nat_into A ` UNIV = A"
2.26 +lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
2.27 by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
2.28
2.29 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
2.30 @@ -136,32 +136,32 @@
2.31 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"
2.32 by (simp add: f_inv_into_f from_nat_into_def)
2.33
2.34 -lemma infinite_to_nat_on_from_nat_into[simp]:
2.35 +lemma to_nat_on_from_nat_into_infinite[simp]:
2.36 "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
2.37 by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
2.38
2.39 lemma from_nat_into_inj:
2.40 - assumes c: "countable A" and i: "infinite A"
2.41 - shows "from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
2.42 -proof-
2.43 - have "?L = ?R \<longleftrightarrow> to_nat_on A ?L = to_nat_on A ?R"
2.44 - unfolding to_nat_on_inj[OF c from_nat_into[OF infinite_imp_nonempty[OF i]]
2.45 - from_nat_into[OF infinite_imp_nonempty[OF i]]] ..
2.46 - also have "... \<longleftrightarrow> ?K" using c i by simp
2.47 - finally show ?thesis .
2.48 -qed
2.49 + "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
2.50 + from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
2.51 + by (subst to_nat_on_inj[symmetric, of A]) auto
2.52 +
2.53 +lemma from_nat_into_inj_infinite[simp]:
2.54 + "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
2.55 + using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
2.56 +
2.57 +lemma eq_from_nat_into_iff:
2.58 + "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"
2.59 + by auto
2.60
2.61 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
2.62 by (rule exI[of _ "to_nat_on A a"]) simp
2.63
2.64 lemma from_nat_into_inject[simp]:
2.65 -assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
2.66 -shows "from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
2.67 -by (metis assms from_nat_into_image)
2.68 + "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
2.69 + by (metis range_from_nat_into)
2.70
2.71 -lemma inj_on_from_nat_into:
2.72 -"inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
2.73 -unfolding inj_on_def by auto
2.74 +lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
2.75 + unfolding inj_on_def by auto
2.76
2.77 subsection {* Closure properties of countability *}
2.78
3.1 --- a/src/HOL/ROOT Wed Nov 21 16:32:34 2012 +0100
3.2 +++ b/src/HOL/ROOT Wed Nov 21 16:43:14 2012 +0100
3.3 @@ -793,7 +793,7 @@
3.4 theories MutabelleExtra
3.5
3.6 session "HOL-Quickcheck_Examples" in Quickcheck_Examples = HOL +
3.7 - options [timeout = 3600, document = false]
3.8 + options [timeout = 5400, document = false]
3.9 theories
3.10 Quickcheck_Examples
3.11 (* FIXME