add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image

--- a/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:53 2013 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Nov 12 19:28:54 2013 +0100
@@ -518,7 +518,6 @@
   then show ?thesis by simp
 qed
 
-
 subsection {* Class @{text finite}  *}
 
 class finite =
@@ -1333,6 +1332,58 @@
 lemma card_psubset: "finite B ==> A \<subseteq> B ==> card A < card B ==> A < B"
 by (erule psubsetI, blast)
 
+lemma card_le_inj:
+  assumes fA: "finite A"
+    and fB: "finite B"
+    and c: "card A \<le> card B"
+  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
+  using fA fB c
+proof (induct arbitrary: B rule: finite_induct)
+  case empty
+  then show ?case by simp
+next
+  case (insert x s t)
+  then show ?case
+  proof (induct rule: finite_induct[OF "insert.prems"(1)])
+    case 1
+    then show ?case by simp
+  next
+    case (2 y t)
+    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
+      by simp
+    from "2.prems"(3) [OF "2.hyps"(1) cst]
+    obtain f where "f ` s \<subseteq> t" "inj_on f s"
+      by blast
+    with "2.prems"(2) "2.hyps"(2) show ?case
+      apply -
+      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
+      apply (auto simp add: inj_on_def)
+      done
+  qed
+qed
+
+lemma card_subset_eq:
+  assumes fB: "finite B"
+    and AB: "A \<subseteq> B"
+    and c: "card A = card B"
+  shows "A = B"
+proof -
+  from fB AB have fA: "finite A"
+    by (auto intro: finite_subset)
+  from fA fB have fBA: "finite (B - A)"
+    by auto
+  have e: "A \<inter> (B - A) = {}"
+    by blast
+  have eq: "A \<union> (B - A) = B"
+    using AB by blast
+  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
+    by arith
+  then have "B - A = {}"
+    unfolding card_eq_0_iff using fA fB by simp
+  with AB show "A = B"
+    by blast
+qed
+
 lemma insert_partition:
   "\<lbrakk> x \<notin> F; \<forall>c1 \<in> insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 \<longrightarrow> c1 \<inter> c2 = {} \<rbrakk>
   \<Longrightarrow> x \<inter> \<Union> F = {}"
@@ -1359,6 +1410,32 @@
   with fin show "P A" using major by blast
 qed
 
+lemma finite_induct_select[consumes 1, case_names empty select]:
+  assumes "finite S"
+  assumes "P {}"
+  assumes select: "\<And>T. T \<subset> S \<Longrightarrow> P T \<Longrightarrow> \<exists>s\<in>S - T. P (insert s T)"
+  shows "P S"
+proof -
+  have "0 \<le> card S" by simp
+  then have "\<exists>T \<subseteq> S. card T = card S \<and> P T"
+  proof (induct rule: dec_induct)
+    case base with `P {}` show ?case
+      by (intro exI[of _ "{}"]) auto
+  next
+    case (step n)
+    then obtain T where T: "T \<subseteq> S" "card T = n" "P T"
+      by auto
+    with `n < card S` have "T \<subset> S" "P T"
+      by auto
+    with select[of T] obtain s where "s \<in> S" "s \<notin> T" "P (insert s T)"
+      by auto
+    with step(2) T `finite S` show ?case
+      by (intro exI[of _ "insert s T"]) (auto dest: finite_subset)
+  qed
+  with `finite S` show "P S"
+    by (auto dest: card_subset_eq)
+qed
+
 text{* main cardinality theorem *}
 lemma card_partition [rule_format]:
   "finite C ==>

--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:53 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Nov 12 19:28:54 2013 +0100
@@ -36,34 +36,6 @@
   apply auto
   done
 
-lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
-  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
-
-lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
-  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
-
-lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
-  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
-
-lemma sqrt_even_pow2:
-  assumes n: "even n"
-  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
-proof -
-  from n obtain m where m: "n = 2 * m"
-    unfolding even_mult_two_ex ..
-  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
-    by (simp only: power_mult[symmetric] mult_commute)
-  then show ?thesis
-    using m by simp
-qed
-
-lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
-  apply (cases "x = 0")
-  apply simp_all
-  using sqrt_divide_self_eq[of x]
-  apply (simp add: inverse_eq_divide field_simps)
-  done
-
 text{* Hence derive more interesting properties of the norm. *}
 
 lemma norm_eq_0_dot: "norm x = 0 \<longleftrightarrow> x \<bullet> x = (0::real)"
@@ -2406,58 +2378,6 @@
 
 text {* Can construct an isomorphism between spaces of same dimension. *}
 
-lemma card_le_inj:
-  assumes fA: "finite A"
-    and fB: "finite B"
-    and c: "card A \<le> card B"
-  shows "\<exists>f. f ` A \<subseteq> B \<and> inj_on f A"
-  using fA fB c
-proof (induct arbitrary: B rule: finite_induct)
-  case empty
-  then show ?case by simp
-next
-  case (insert x s t)
-  then show ?case
-  proof (induct rule: finite_induct[OF "insert.prems"(1)])
-    case 1
-    then show ?case by simp
-  next
-    case (2 y t)
-    from "2.prems"(1,2,5) "2.hyps"(1,2) have cst: "card s \<le> card t"
-      by simp
-    from "2.prems"(3) [OF "2.hyps"(1) cst]
-    obtain f where "f ` s \<subseteq> t" "inj_on f s"
-      by blast
-    with "2.prems"(2) "2.hyps"(2) show ?case
-      apply -
-      apply (rule exI[where x = "\<lambda>z. if z = x then y else f z"])
-      apply (auto simp add: inj_on_def)
-      done
-  qed
-qed
-
-lemma card_subset_eq:
-  assumes fB: "finite B"
-    and AB: "A \<subseteq> B"
-    and c: "card A = card B"
-  shows "A = B"
-proof -
-  from fB AB have fA: "finite A"
-    by (auto intro: finite_subset)
-  from fA fB have fBA: "finite (B - A)"
-    by auto
-  have e: "A \<inter> (B - A) = {}"
-    by blast
-  have eq: "A \<union> (B - A) = B"
-    using AB by blast
-  from card_Un_disjoint[OF fA fBA e, unfolded eq c] have "card (B - A) = 0"
-    by arith
-  then have "B - A = {}"
-    unfolding card_eq_0_iff using fA fB by simp
-  with AB show "A = B"
-    by blast
-qed
-
 lemma subspace_isomorphism:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"

--- a/src/HOL/NthRoot.thy	Tue Nov 12 19:28:53 2013 +0100
+++ b/src/HOL/NthRoot.thy	Tue Nov 12 19:28:54 2013 +0100
@@ -410,6 +410,27 @@
 lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
 unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
 
+lemma real_le_lsqrt: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> x \<le> y\<^sup>2 \<Longrightarrow> sqrt x \<le> y"
+  using real_sqrt_le_iff[of x "y\<^sup>2"] by simp
+
+lemma real_le_rsqrt: "x\<^sup>2 \<le> y \<Longrightarrow> x \<le> sqrt y"
+  using real_sqrt_le_mono[of "x\<^sup>2" y] by simp
+
+lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
+  using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
+
+lemma sqrt_even_pow2:
+  assumes n: "even n"
+  shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
+proof -
+  from n obtain m where m: "n = 2 * m"
+    unfolding even_mult_two_ex ..
+  from m have "sqrt (2 ^ n) = sqrt ((2 ^ m)\<^sup>2)"
+    by (simp only: power_mult[symmetric] mult_commute)
+  then show ?thesis
+    using m by simp
+qed
+
 lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, unfolded real_sqrt_zero]
 lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, unfolded real_sqrt_zero]
 lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, unfolded real_sqrt_zero]
@@ -490,6 +511,13 @@
   qed
 qed
 
+lemma real_div_sqrt: "0 \<le> x \<Longrightarrow> x / sqrt x = sqrt x"
+  apply (cases "x = 0")
+  apply simp_all
+  using sqrt_divide_self_eq[of x]
+  apply (simp add: inverse_eq_divide field_simps)
+  done
+
 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
 apply (simp add: divide_inverse)
 apply (case_tac "r=0")