--- a/src/HOL/Finite_Set.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Finite_Set.thy Sat Sep 06 20:12:32 2014 +0200
@@ -456,6 +456,15 @@
show ?thesis by(rule finite_imageD[OF 1 2])
qed
+lemma not_finite_existsD:
+ assumes "\<not> finite {a. P a}"
+ shows "\<exists>a. P a"
+proof (rule classical)
+ assume "\<not> (\<exists>a. P a)"
+ with assms show ?thesis by auto
+qed
+
+
subsubsection {* Further induction rules on finite sets *}
lemma finite_ne_induct [case_names singleton insert, consumes 2]:
@@ -523,6 +532,29 @@
then show ?thesis by simp
qed
+lemma finite_update_induct [consumes 1, case_names const update]:
+ assumes finite: "finite {a. f a \<noteq> c}"
+ assumes const: "P (\<lambda>a. c)"
+ assumes update: "\<And>a b f. finite {a. f a \<noteq> c} \<Longrightarrow> f a = c \<Longrightarrow> b \<noteq> c \<Longrightarrow> P f \<Longrightarrow> P (f(a := b))"
+ shows "P f"
+using finite proof (induct "{a. f a \<noteq> c}" arbitrary: f)
+ case empty with const show ?case by simp
+next
+ case (insert a A)
+ then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c"
+ by auto
+ with `finite A` have "finite {a'. (f(a := c)) a' \<noteq> c}"
+ by simp
+ have "(f(a := c)) a = c"
+ by simp
+ from insert `A = {a'. (f(a := c)) a' \<noteq> c}` have "P (f(a := c))"
+ by simp
+ with `finite {a'. (f(a := c)) a' \<noteq> c}` `(f(a := c)) a = c` `f a \<noteq> c` have "P ((f(a := c))(a := f a))"
+ by (rule update)
+ then show ?case by simp
+qed
+
+
subsection {* Class @{text finite} *}
class finite =
--- a/src/HOL/Fun.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Fun.thy Sat Sep 06 20:12:32 2014 +0200
@@ -422,6 +422,17 @@
using assms
by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
+lemma bij_pointE:
+ assumes "bij f"
+ obtains x where "y = f x" and "\<And>x'. y = f x' \<Longrightarrow> x' = x"
+proof -
+ from assms have "inj f" by (rule bij_is_inj)
+ moreover from assms have "surj f" by (rule bij_is_surj)
+ then have "y \<in> range f" by simp
+ ultimately have "\<exists>!x. y = f x" by (simp add: range_ex1_eq)
+ with that show thesis by blast
+qed
+
lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
by simp
--- a/src/HOL/Groups_Big.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Groups_Big.thy Sat Sep 06 20:12:32 2014 +0200
@@ -112,7 +112,7 @@
assumes "finite A"
shows "F g (A - {x. g x = z}) = F g A"
using assms by (induct A) (simp_all add: insert_Diff_if)
-
+
lemma not_neutral_contains_not_neutral:
assumes "F g A \<noteq> z"
obtains a where "a \<in> A" and "g a \<noteq> z"
@@ -424,6 +424,38 @@
by (simp add: union_disjoint reindex)
qed
+lemma same_carrier:
+ assumes "finite C"
+ assumes subset: "A \<subseteq> C" "B \<subseteq> C"
+ assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+ shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
+proof -
+ from `finite C` subset have
+ "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
+ by (auto elim: finite_subset)
+ from subset have [simp]: "A - (C - A) = A" by auto
+ from subset have [simp]: "B - (C - B) = B" by auto
+ from subset have "C = A \<union> (C - A)" by auto
+ then have "F g C = F g (A \<union> (C - A))" by simp
+ also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
+ using `finite A` `finite (C - A)` by (simp only: union_diff2)
+ finally have P: "F g C = F g A" using trivial by simp
+ from subset have "C = B \<union> (C - B)" by auto
+ then have "F h C = F h (B \<union> (C - B))" by simp
+ also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
+ using `finite B` `finite (C - B)` by (simp only: union_diff2)
+ finally have Q: "F h C = F h B" using trivial by simp
+ from P Q show ?thesis by simp
+qed
+
+lemma same_carrierI:
+ assumes "finite C"
+ assumes subset: "A \<subseteq> C" "B \<subseteq> C"
+ assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
+ assumes "F g C = F h C"
+ shows "F g A = F h B"
+ using assms same_carrier [of C A B] by simp
+
end
notation times (infixl "*" 70)
--- a/src/HOL/List.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/List.thy Sat Sep 06 20:12:32 2014 +0200
@@ -3208,6 +3208,10 @@
"distinct(map f xs) = (distinct xs & inj_on f (set xs))"
by (induct xs) auto
+lemma distinct_map_filter:
+ "distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))"
+ by (induct xs) auto
+
lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
by (induct xs) auto
--- a/src/HOL/Product_Type.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Product_Type.thy Sat Sep 06 20:12:32 2014 +0200
@@ -1029,6 +1029,14 @@
"prod.swap (x, y) = (y, x)"
by (simp add: prod.swap_def)
+lemma swap_swap [simp]:
+ "prod.swap (prod.swap p) = p"
+ by (cases p) simp
+
+lemma swap_comp_swap [simp]:
+ "prod.swap \<circ> prod.swap = id"
+ by (simp add: fun_eq_iff)
+
lemma pair_in_swap_image [simp]:
"(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
by (auto intro!: image_eqI)
@@ -1041,6 +1049,14 @@
"inj_on (\<lambda>(i, j). (j, i)) A"
by (rule inj_onI) auto
+lemma surj_swap [simp]:
+ "surj prod.swap"
+ by (rule surjI [of _ prod.swap]) simp
+
+lemma bij_swap [simp]:
+ "bij prod.swap"
+ by (simp add: bij_def)
+
lemma case_swap [simp]:
"(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
by (cases p) simp
--- a/src/HOL/Relation.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Relation.thy Sat Sep 06 20:12:32 2014 +0200
@@ -604,7 +604,6 @@
"(R O S) O T = R O (S O T)"
by blast
-
lemma relcompp_assoc:
"(r OO s) OO t = r OO (s OO t)"
by (fact O_assoc [to_pred])
@@ -665,6 +664,9 @@
"r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
by (auto simp add: set_eq_iff)
+lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)"
+ unfolding relcomp_unfold [to_pred] ..
+
lemma eq_OO: "op= OO R = R"
by blast
--- a/src/HOL/Rings.thy Fri Sep 05 16:09:03 2014 +0100
+++ b/src/HOL/Rings.thy Sat Sep 06 20:12:32 2014 +0200
@@ -30,6 +30,13 @@
assumes mult_zero_right [simp]: "a * 0 = 0"
class semiring_0 = semiring + comm_monoid_add + mult_zero
+begin
+
+lemma mult_not_zero:
+ "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
+ by auto
+
+end
class semiring_0_cancel = semiring + cancel_comm_monoid_add
begin