add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
authorhoelzl
Tue Nov 12 19:28:54 2013 +0100 (2013-11-12)
changeset 5441388a036a95967
parent 54412 900c6d724250
child 54414 72949fae4f81
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
src/HOL/Finite_Set.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/NthRoot.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:53 2013 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:54 2013 +0100
     1.3 @@ -518,7 +518,6 @@
     1.4    then show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -
     1.8  subsection {* Class @{text finite}  *}
     1.9  
    1.10  class finite =
    1.11 @@ -1333,6 +1332,58 @@
    1.12  lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
    1.13  by (erule psubsetI, blast)
    1.14  
    1.15 +lemma card_le_inj:
    1.16 +  assumes fA: "finite A"
    1.17 +    and fB: "finite B"
    1.18 +    and c: "card A \<le> card B"
    1.19 +  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
    1.20 +  using fA fB c
    1.21 +proof (induct arbitrary: B rule: finite_induct)
    1.22 +  case empty
    1.23 +  then show ?case by simp
    1.24 +next
    1.25 +  case (insert x s t)
    1.26 +  then show ?case
    1.27 +  proof (induct rule: finite_induct[OF "insert.prems"(1)])
    1.28 +    case 1
    1.29 +    then show ?case by simp
    1.30 +  next
    1.31 +    case (2 y t)
    1.32 +    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
    1.33 +      by simp
    1.34 +    from "2.prems"(3) [OF "2.hyps"(1) cst]
    1.35 +    obtain f where "f ` s \<subseteq> t" "inj_on f s"
    1.36 +      by blast
    1.37 +    with "2.prems"(2) "2.hyps"(2) show ?case
    1.38 +      apply -
    1.39 +      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
    1.40 +      apply (auto simp add: inj_on_def)
    1.41 +      done
    1.42 +  qed
    1.43 +qed
    1.44 +
    1.45 +lemma card_subset_eq:
    1.46 +  assumes fB: "finite B"
    1.47 +    and AB: "A \<subseteq> B"
    1.48 +    and c: "card A = card B"
    1.49 +  shows "A = B"
    1.50 +proof -
    1.51 +  from fB AB have fA: "finite A"
    1.52 +    by (auto intro: finite_subset)
    1.53 +  from fA fB have fBA: "finite (B - A)"
    1.54 +    by auto
    1.55 +  have e: "A \<inter> (B - A) = {}"
    1.56 +    by blast
    1.57 +  have eq: "A \<union> (B - A) = B"
    1.58 +    using AB by blast
    1.59 +  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
    1.60 +    by arith
    1.61 +  then have "B - A = {}"
    1.62 +    unfolding card_eq_0_iff using fA fB by simp
    1.63 +  with AB show "A = B"
    1.64 +    by blast
    1.65 +qed
    1.66 +
    1.67  lemma insert_partition:
    1.68    "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
    1.69    \<Longrightarrow> x \<inter> \<Union> F = {}"
    1.70 @@ -1359,6 +1410,32 @@
    1.71    with fin show "P A" using major by blast
    1.72  qed
    1.73  
    1.74 +lemma finite_induct_select[consumes 1, case_names empty select]:
    1.75 +  assumes "finite S"
    1.76 +  assumes "P {}"
    1.77 +  assumes select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
    1.78 +  shows "P S"
    1.79 +proof -
    1.80 +  have "0 \<le> card S" by simp
    1.81 +  then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
    1.82 +  proof (induct rule: dec_induct)
    1.83 +    case base with `P {}` show ?case
    1.84 +      by (intro exI[of _ "{}"]) auto
    1.85 +  next
    1.86 +    case (step n)
    1.87 +    then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
    1.88 +      by auto
    1.89 +    with `n < card S` have "T \<subset> S" "P T"
    1.90 +      by auto
    1.91 +    with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
    1.92 +      by auto
    1.93 +    with step(2) T `finite S` show ?case
    1.94 +      by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
    1.95 +  qed
    1.96 +  with `finite S` show "P S"
    1.97 +    by (auto dest: card_subset_eq)
    1.98 +qed
    1.99 +
   1.100  text{* main cardinality theorem *}
   1.101  lemma card_partition [rule_format]:
   1.102    "finite C ==>
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:53 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:54 2013 +0100
     2.3 @@ -36,34 +36,6 @@
     2.4    apply auto
     2.5    done
     2.6  
     2.7 -lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
     2.8 -  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
     2.9 -
    2.10 -lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
    2.11 -  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
    2.12 -
    2.13 -lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
    2.14 -  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
    2.15 -
    2.16 -lemma sqrt_even_pow2:
    2.17 -  assumes n: "even n"
    2.18 -  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
    2.19 -proof -
    2.20 -  from n obtain m where m: "n = 2 * m"
    2.21 -    unfolding even_mult_two_ex ..
    2.22 -  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    2.23 -    by (simp only: power_mult[symmetric] mult_commute)
    2.24 -  then show ?thesis
    2.25 -    using m by simp
    2.26 -qed
    2.27 -
    2.28 -lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
    2.29 -  apply (cases "x = 0")
    2.30 -  apply simp_all
    2.31 -  using sqrt_divide_self_eq[of x]
    2.32 -  apply (simp add: inverse_eq_divide field_simps)
    2.33 -  done
    2.34 -
    2.35  text{* Hence derive more interesting properties of the norm. *}
    2.36  
    2.37  lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
    2.38 @@ -2406,58 +2378,6 @@
    2.39  
    2.40  text {* Can construct an isomorphism between spaces of same dimension. *}
    2.41  
    2.42 -lemma card_le_inj:
    2.43 -  assumes fA: "finite A"
    2.44 -    and fB: "finite B"
    2.45 -    and c: "card A \<le> card B"
    2.46 -  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
    2.47 -  using fA fB c
    2.48 -proof (induct arbitrary: B rule: finite_induct)
    2.49 -  case empty
    2.50 -  then show ?case by simp
    2.51 -next
    2.52 -  case (insert x s t)
    2.53 -  then show ?case
    2.54 -  proof (induct rule: finite_induct[OF "insert.prems"(1)])
    2.55 -    case 1
    2.56 -    then show ?case by simp
    2.57 -  next
    2.58 -    case (2 y t)
    2.59 -    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
    2.60 -      by simp
    2.61 -    from "2.prems"(3) [OF "2.hyps"(1) cst]
    2.62 -    obtain f where "f ` s \<subseteq> t" "inj_on f s"
    2.63 -      by blast
    2.64 -    with "2.prems"(2) "2.hyps"(2) show ?case
    2.65 -      apply -
    2.66 -      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
    2.67 -      apply (auto simp add: inj_on_def)
    2.68 -      done
    2.69 -  qed
    2.70 -qed
    2.71 -
    2.72 -lemma card_subset_eq:
    2.73 -  assumes fB: "finite B"
    2.74 -    and AB: "A \<subseteq> B"
    2.75 -    and c: "card A = card B"
    2.76 -  shows "A = B"
    2.77 -proof -
    2.78 -  from fB AB have fA: "finite A"
    2.79 -    by (auto intro: finite_subset)
    2.80 -  from fA fB have fBA: "finite (B - A)"
    2.81 -    by auto
    2.82 -  have e: "A \<inter> (B - A) = {}"
    2.83 -    by blast
    2.84 -  have eq: "A \<union> (B - A) = B"
    2.85 -    using AB by blast
    2.86 -  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
    2.87 -    by arith
    2.88 -  then have "B - A = {}"
    2.89 -    unfolding card_eq_0_iff using fA fB by simp
    2.90 -  with AB show "A = B"
    2.91 -    by blast
    2.92 -qed
    2.93 -
    2.94  lemma subspace_isomorphism:
    2.95    fixes S :: "'a::euclidean_space set"
    2.96      and T :: "'b::euclidean_space set"
     3.1 --- a/src/HOL/NthRoot.thy	Tue Nov 12 19:28:53 2013 +0100
     3.2 +++ b/src/HOL/NthRoot.thy	Tue Nov 12 19:28:54 2013 +0100
     3.3 @@ -410,6 +410,27 @@
     3.4  lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
     3.5  unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
     3.6  
     3.7 +lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
     3.8 +  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
     3.9 +
    3.10 +lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
    3.11 +  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
    3.12 +
    3.13 +lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
    3.14 +  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
    3.15 +
    3.16 +lemma sqrt_even_pow2:
    3.17 +  assumes n: "even n"
    3.18 +  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
    3.19 +proof -
    3.20 +  from n obtain m where m: "n = 2 * m"
    3.21 +    unfolding even_mult_two_ex ..
    3.22 +  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
    3.23 +    by (simp only: power_mult[symmetric] mult_commute)
    3.24 +  then show ?thesis
    3.25 +    using m by simp
    3.26 +qed
    3.27 +
    3.28  lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
    3.29  lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
    3.30  lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
    3.31 @@ -490,6 +511,13 @@
    3.32    qed
    3.33  qed
    3.34  
    3.35 +lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
    3.36 +  apply (cases "x = 0")
    3.37 +  apply simp_all
    3.38 +  using sqrt_divide_self_eq[of x]
    3.39 +  apply (simp add: inverse_eq_divide field_simps)
    3.40 +  done
    3.41 +
    3.42  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
    3.43  apply (simp add: divide_inverse)
    3.44  apply (case_tac "r=0")