added various facts
authorhaftmann
Sat Sep 06 20:12:32 2014 +0200 (2014-09-06)
changeset 581951fee63e0377d
parent 58194 3d90a96fd6a9
child 58196 1b3fbfb85980
added various facts
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Groups_Big.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Relation.thy
src/HOL/Rings.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Fri Sep 05 16:09:03 2014 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Sat Sep 06 20:12:32 2014 +0200
     1.3 @@ -456,6 +456,15 @@
     1.4    show ?thesis by(rule finite_imageD[OF 1 2])
     1.5  qed
     1.6  
     1.7 +lemma not_finite_existsD:
     1.8 +  assumes "\<not> finite {a. P a}"
     1.9 +  shows "\<exists>a. P a"
    1.10 +proof (rule classical)
    1.11 +  assume "\<not> (\<exists>a. P a)"
    1.12 +  with assms show ?thesis by auto
    1.13 +qed
    1.14 +
    1.15 +
    1.16  subsubsection {* Further induction rules on finite sets *}
    1.17  
    1.18  lemma finite_ne_induct [case_names singleton insert, consumes 2]:
    1.19 @@ -523,6 +532,29 @@
    1.20    then show ?thesis by simp
    1.21  qed
    1.22  
    1.23 +lemma finite_update_induct [consumes 1, case_names const update]:
    1.24 +  assumes finite: "finite {a. f a \<noteq> c}"
    1.25 +  assumes const: "P (\<lambda>a. c)"
    1.26 +  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))"
    1.27 +  shows "P f"
    1.28 +using finite proof (induct "{a. f a \<noteq> c}" arbitrary: f)
    1.29 +  case empty with const show ?case by simp
    1.30 +next
    1.31 +  case (insert a A)
    1.32 +  then have "A = {a'. (f(a := c)) a' \<noteq> c}" and "f a \<noteq> c"
    1.33 +    by auto
    1.34 +  with `finite A` have "finite {a'. (f(a := c)) a' \<noteq> c}"
    1.35 +    by simp
    1.36 +  have "(f(a := c)) a = c"
    1.37 +    by simp
    1.38 +  from insert `A = {a'. (f(a := c)) a' \<noteq> c}` have "P (f(a := c))"
    1.39 +    by simp
    1.40 +  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))"
    1.41 +    by (rule update)
    1.42 +  then show ?case by simp
    1.43 +qed
    1.44 +
    1.45 +
    1.46  subsection {* Class @{text finite}  *}
    1.47  
    1.48  class finite =
     2.1 --- a/src/HOL/Fun.thy	Fri Sep 05 16:09:03 2014 +0100
     2.2 +++ b/src/HOL/Fun.thy	Sat Sep 06 20:12:32 2014 +0200
     2.3 @@ -422,6 +422,17 @@
     2.4  using assms
     2.5  by(unfold bij_betw_def inj_on_def, auto simp add: inj_on_def)
     2.6  
     2.7 +lemma bij_pointE:
     2.8 +  assumes "bij f"
     2.9 +  obtains x where "y = f x" and "\<And>x'. y = f x' \<Longrightarrow> x' = x"
    2.10 +proof -
    2.11 +  from assms have "inj f" by (rule bij_is_inj)
    2.12 +  moreover from assms have "surj f" by (rule bij_is_surj)
    2.13 +  then have "y \<in> range f" by simp
    2.14 +  ultimately have "\<exists>!x. y = f x" by (simp add: range_ex1_eq)
    2.15 +  with that show thesis by blast
    2.16 +qed
    2.17 +
    2.18  lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A"
    2.19  by simp
    2.20  
     3.1 --- a/src/HOL/Groups_Big.thy	Fri Sep 05 16:09:03 2014 +0100
     3.2 +++ b/src/HOL/Groups_Big.thy	Sat Sep 06 20:12:32 2014 +0200
     3.3 @@ -112,7 +112,7 @@
     3.4    assumes "finite A"
     3.5    shows "F g (A - {x. g x = z}) = F g A"
     3.6    using assms by (induct A) (simp_all add: insert_Diff_if) 
     3.7 -  
     3.8 +
     3.9  lemma not_neutral_contains_not_neutral:
    3.10    assumes "F g A \<noteq> z"
    3.11    obtains a where "a \<in> A" and "g a \<noteq> z"
    3.12 @@ -424,6 +424,38 @@
    3.13      by (simp add: union_disjoint reindex)
    3.14  qed
    3.15  
    3.16 +lemma same_carrier:
    3.17 +  assumes "finite C"
    3.18 +  assumes subset: "A \<subseteq> C" "B \<subseteq> C"
    3.19 +  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
    3.20 +  shows "F g A = F h B \<longleftrightarrow> F g C = F h C"
    3.21 +proof -
    3.22 +  from `finite C` subset have
    3.23 +    "finite A" and "finite B" and "finite (C - A)" and "finite (C - B)"
    3.24 +    by (auto elim: finite_subset)
    3.25 +  from subset have [simp]: "A - (C - A) = A" by auto
    3.26 +  from subset have [simp]: "B - (C - B) = B" by auto
    3.27 +  from subset have "C = A \<union> (C - A)" by auto
    3.28 +  then have "F g C = F g (A \<union> (C - A))" by simp
    3.29 +  also have "\<dots> = F g (A - (C - A)) * F g (C - A - A) * F g (A \<inter> (C - A))"
    3.30 +    using `finite A` `finite (C - A)` by (simp only: union_diff2)
    3.31 +  finally have P: "F g C = F g A" using trivial by simp
    3.32 +  from subset have "C = B \<union> (C - B)" by auto
    3.33 +  then have "F h C = F h (B \<union> (C - B))" by simp
    3.34 +  also have "\<dots> = F h (B - (C - B)) * F h (C - B - B) * F h (B \<inter> (C - B))"
    3.35 +    using `finite B` `finite (C - B)` by (simp only: union_diff2)
    3.36 +  finally have Q: "F h C = F h B" using trivial by simp
    3.37 +  from P Q show ?thesis by simp
    3.38 +qed
    3.39 +
    3.40 +lemma same_carrierI:
    3.41 +  assumes "finite C"
    3.42 +  assumes subset: "A \<subseteq> C" "B \<subseteq> C"
    3.43 +  assumes trivial: "\<And>a. a \<in> C - A \<Longrightarrow> g a = 1" "\<And>b. b \<in> C - B \<Longrightarrow> h b = 1"
    3.44 +  assumes "F g C = F h C"
    3.45 +  shows "F g A = F h B"
    3.46 +  using assms same_carrier [of C A B] by simp
    3.47 +
    3.48  end
    3.49  
    3.50  notation times (infixl "*" 70)
     4.1 --- a/src/HOL/List.thy	Fri Sep 05 16:09:03 2014 +0100
     4.2 +++ b/src/HOL/List.thy	Sat Sep 06 20:12:32 2014 +0200
     4.3 @@ -3208,6 +3208,10 @@
     4.4    "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
     4.5  by (induct xs) auto
     4.6  
     4.7 +lemma distinct_map_filter:
     4.8 +  "distinct (map f xs) \<Longrightarrow> distinct (map f (filter P xs))"
     4.9 +  by (induct xs) auto
    4.10 +
    4.11  lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
    4.12  by (induct xs) auto
    4.13  
     5.1 --- a/src/HOL/Product_Type.thy	Fri Sep 05 16:09:03 2014 +0100
     5.2 +++ b/src/HOL/Product_Type.thy	Sat Sep 06 20:12:32 2014 +0200
     5.3 @@ -1029,6 +1029,14 @@
     5.4    "prod.swap (x, y) = (y, x)"
     5.5    by (simp add: prod.swap_def)
     5.6  
     5.7 +lemma swap_swap [simp]:
     5.8 +  "prod.swap (prod.swap p) = p"
     5.9 +  by (cases p) simp
    5.10 +
    5.11 +lemma swap_comp_swap [simp]:
    5.12 +  "prod.swap \<circ> prod.swap = id"
    5.13 +  by (simp add: fun_eq_iff)
    5.14 +
    5.15  lemma pair_in_swap_image [simp]:
    5.16    "(y, x) \<in> prod.swap ` A \<longleftrightarrow> (x, y) \<in> A"
    5.17    by (auto intro!: image_eqI)
    5.18 @@ -1041,6 +1049,14 @@
    5.19    "inj_on (\<lambda>(i, j). (j, i)) A"
    5.20    by (rule inj_onI) auto
    5.21  
    5.22 +lemma surj_swap [simp]:
    5.23 +  "surj prod.swap"
    5.24 +  by (rule surjI [of _ prod.swap]) simp
    5.25 +
    5.26 +lemma bij_swap [simp]:
    5.27 +  "bij prod.swap"
    5.28 +  by (simp add: bij_def)
    5.29 +
    5.30  lemma case_swap [simp]:
    5.31    "(case prod.swap p of (y, x) \<Rightarrow> f x y) = (case p of (x, y) \<Rightarrow> f x y)"
    5.32    by (cases p) simp
     6.1 --- a/src/HOL/Relation.thy	Fri Sep 05 16:09:03 2014 +0100
     6.2 +++ b/src/HOL/Relation.thy	Sat Sep 06 20:12:32 2014 +0200
     6.3 @@ -604,7 +604,6 @@
     6.4    "(R O S) O T = R O (S O T)"
     6.5    by blast
     6.6  
     6.7 -
     6.8  lemma relcompp_assoc:
     6.9    "(r OO s) OO t = r OO (s OO t)"
    6.10    by (fact O_assoc [to_pred])
    6.11 @@ -665,6 +664,9 @@
    6.12    "r O s = {(x, z). \<exists>y. (x, y) \<in> r \<and> (y, z) \<in> s}"
    6.13    by (auto simp add: set_eq_iff)
    6.14  
    6.15 +lemma relcompp_apply: "(R OO S) a c \<longleftrightarrow> (\<exists>b. R a b \<and> S b c)"
    6.16 +  unfolding relcomp_unfold [to_pred] ..
    6.17 +
    6.18  lemma eq_OO: "op= OO R = R"
    6.19  by blast
    6.20  
     7.1 --- a/src/HOL/Rings.thy	Fri Sep 05 16:09:03 2014 +0100
     7.2 +++ b/src/HOL/Rings.thy	Sat Sep 06 20:12:32 2014 +0200
     7.3 @@ -30,6 +30,13 @@
     7.4    assumes mult_zero_right [simp]: "a * 0 = 0"
     7.5  
     7.6  class semiring_0 = semiring + comm_monoid_add + mult_zero
     7.7 +begin
     7.8 +
     7.9 +lemma mult_not_zero:
    7.10 +  "a * b \<noteq> 0 \<Longrightarrow> a \<noteq> 0 \<and> b \<noteq> 0"
    7.11 +  by auto
    7.12 +
    7.13 +end
    7.14  
    7.15  class semiring_0_cancel = semiring + cancel_comm_monoid_add
    7.16  begin