# HG changeset patch
# User haftmann
# Date 1410027152 -7200
# Node ID 1fee63e0377df048932a4d517642f86a95187813
# Parent  3d90a96fd6a96c669170dc4caf60691888807ccb
added various facts

diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Finite_Set.thy
--- 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 =
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Fun.thy
--- 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
 
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Groups_Big.thy
--- 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)
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/List.thy
--- 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
 
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Product_Type.thy
--- 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
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Relation.thy
--- 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
 
diff -r 3d90a96fd6a9 -r 1fee63e0377d src/HOL/Rings.thy
--- 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