# HG changeset patch
# User wenzelm
# Date 1258399382 -3600
# Node ID d15212c7501c94acdcfd1c63ba63638bdbcbb079
# Parent  474ebcc348e6c35a378afc8f2c602ac7038801d8# Parent  5249bbca5fab28d58959f66f6750a667dba5ba1a
merged

diff -r 5249bbca5fab -r d15212c7501c src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -152,78 +152,66 @@
   thus ?thesis by auto
 qed
 
-lemma hassize_insert: "a \<notin> F \<Longrightarrow> insert a F hassize n \<Longrightarrow> F hassize (n - 1)"
-  by (auto simp add: hassize_def)
-
-lemma hassize_permutations: assumes Sn: "S hassize n"
-  shows "{p. p permutes S} hassize (fact n)"
-proof-
-  from Sn have fS:"finite S" by (simp add: hassize_def)
-
-  have "\<forall>n. (S hassize n) \<longrightarrow> ({p. p permutes S} hassize (fact n))"
-  proof(rule finite_induct[where F = S])
-    from fS show "finite S" .
-  next
-    show "\<forall>n. ({} hassize n) \<longrightarrow> ({p. p permutes {}} hassize fact n)"
-      by (simp add: hassize_def permutes_empty)
-  next
-    fix x F
-    assume fF: "finite F" and xF: "x \<notin> F"
-      and H: "\<forall>n. (F hassize n) \<longrightarrow> ({p. p permutes F} hassize fact n)"
-    {fix n assume H0: "insert x F hassize n"
-      let ?xF = "{p. p permutes insert x F}"
-      let ?pF = "{p. p permutes F}"
-      let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
-      let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
-      from permutes_insert[of x F]
-      have xfgpF': "?xF = ?g ` ?pF'" .
-      from hassize_insert[OF xF H0] have Fs: "F hassize (n - 1)" .
-      from H Fs have pFs: "?pF hassize fact (n - 1)" by blast
-      hence pF'f: "finite ?pF'" using H0 unfolding hassize_def
-        apply (simp only: Collect_split Collect_mem_eq)
-        apply (rule finite_cartesian_product)
-        apply simp_all
-        done
+lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
+  shows "card {p. p permutes S} = fact n"
+using fS Sn proof (induct arbitrary: n)
+  case empty thus ?case by (simp add: permutes_empty)
+next
+  case (insert x F)
+  { fix n assume H0: "card (insert x F) = n"
+    let ?xF = "{p. p permutes insert x F}"
+    let ?pF = "{p. p permutes F}"
+    let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
+    let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
+    from permutes_insert[of x F]
+    have xfgpF': "?xF = ?g ` ?pF'" .
+    have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
+    from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
+    moreover hence "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
+    ultimately have pF'f: "finite ?pF'" using H0 `finite F`
+      apply (simp only: Collect_split Collect_mem_eq)
+      apply (rule finite_cartesian_product)
+      apply simp_all
+      done
 
-      have ginj: "inj_on ?g ?pF'"
-      proof-
-        {
-          fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
-            and eq: "?g (b,p) = ?g (c,q)"
-          from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
-          from ths(4) xF eq have "b = ?g (b,p) x" unfolding permutes_def
-            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
-          also have "\<dots> = ?g (c,q) x" using ths(5) xF eq
-            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
-          also have "\<dots> = c"using ths(5) xF unfolding permutes_def
-            by (auto simp add: swap_def fun_upd_def expand_fun_eq)
-          finally have bc: "b = c" .
-          hence "Fun.swap x b id = Fun.swap x c id" by simp
-          with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
-          hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
-          hence "p = q" by (simp add: o_assoc)
-          with bc have "(b,p) = (c,q)" by simp }
-        thus ?thesis  unfolding inj_on_def by blast
-      qed
-      from xF H0 have n0: "n \<noteq> 0 " by (auto simp add: hassize_def)
-      hence "\<exists>m. n = Suc m" by arith
-      then obtain m where n[simp]: "n = Suc m" by blast
-      from pFs H0 have xFc: "card ?xF = fact n"
-        unfolding xfgpF' card_image[OF ginj] hassize_def
-        apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
-        by simp
-      from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
-      have "?xF hassize fact n"
-        using xFf xFc
-        unfolding hassize_def  xFf by blast }
-    thus "\<forall>n. (insert x F hassize n) \<longrightarrow> ({p. p permutes insert x F} hassize fact n)"
-      by blast
-  qed
-  with Sn show ?thesis by blast
+    have ginj: "inj_on ?g ?pF'"
+    proof-
+      {
+        fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
+          and eq: "?g (b,p) = ?g (c,q)"
+        from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
+        from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
+          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
+        also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
+          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
+        also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
+          by (auto simp add: swap_def fun_upd_def expand_fun_eq)
+        finally have bc: "b = c" .
+        hence "Fun.swap x b id = Fun.swap x c id" by simp
+        with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
+        hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
+        hence "p = q" by (simp add: o_assoc)
+        with bc have "(b,p) = (c,q)" by simp
+      }
+      thus ?thesis  unfolding inj_on_def by blast
+    qed
+    from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
+    hence "\<exists>m. n = Suc m" by arith
+    then obtain m where n[simp]: "n = Suc m" by blast
+    from pFs H0 have xFc: "card ?xF = fact n"
+      unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
+      apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
+      by simp
+    from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
+    have "card ?xF = fact n"
+      using xFf xFc unfolding xFf by blast
+  }
+  thus ?case using insert by simp
 qed
 
-lemma finite_permutations: "finite S ==> finite {p. p permutes S}"
-  using hassize_permutations[of S] unfolding hassize_def by blast
+lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}"
+  using card_permutations[OF refl fS] fact_gt_zero_nat
+  by (auto intro: card_ge_0_finite)
 
 (* ------------------------------------------------------------------------- *)
 (* Permutations of index set for iterated operations.                        *)
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Log.thy
--- a/src/HOL/Log.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Log.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -87,6 +87,17 @@
 lemma log_ln: "ln x = log (exp(1)) x"
 by (simp add: log_def)
 
+lemma DERIV_log: "x > 0 ==> DERIV (%y. log b y) x :> 1 / (ln b * x)"
+  apply (subst log_def)
+  apply (subgoal_tac "(%y. ln y / ln b) = (%y. (1 / ln b) * ln y)")
+  apply (erule ssubst)
+  apply (subgoal_tac "1 / (ln b * x) = (1 / ln b) * (1 / x)")
+  apply (erule ssubst)
+  apply (rule DERIV_cmult)
+  apply (erule DERIV_ln_divide)
+  apply auto
+done
+
 lemma powr_log_cancel [simp]:
      "[| 0 < a; a \<noteq> 1; 0 < x |] ==> a powr (log a x) = x"
 by (simp add: powr_def log_def)
@@ -152,9 +163,20 @@
   apply (rule powr_realpow [THEN sym], simp)
 done
 
-lemma ln_pwr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
+lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
 by (unfold powr_def, simp)
 
+lemma log_powr: "0 < x ==> 0 \<le> y ==> log b (x powr y) = y * log b x"
+  apply (case_tac "y = 0")
+  apply force
+  apply (auto simp add: log_def ln_powr field_simps)
+done
+
+lemma log_nat_power: "0 < x ==> log b (x^n) = real n * log b x"
+  apply (subst powr_realpow [symmetric])
+  apply (auto simp add: log_powr)
+done
+
 lemma ln_bound: "1 <= x ==> ln x <= x"
   apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
   apply simp
@@ -207,7 +229,7 @@
   apply (rule mult_imp_le_div_pos)
   apply (assumption)
   apply (subst mult_commute)
-  apply (subst ln_pwr [THEN sym])
+  apply (subst ln_powr [THEN sym])
   apply auto
   apply (rule ln_bound)
   apply (erule ge_one_powr_ge_zero)
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -379,6 +379,9 @@
   shows "((1 - u) *\<^sub>R a + u *\<^sub>R b) \<in> s"
   using assms unfolding convex_alt by auto
 
+lemma convex_vec1:"convex (vec1 ` s) = convex (s::real set)"
+  unfolding convex_def Ball_def forall_vec1 unfolding vec1_dest_vec1_simps image_iff by auto
+
 lemma convex_empty[intro]: "convex {}"
   unfolding convex_def by simp
 
@@ -1952,16 +1955,17 @@
 subsection {* Helly's theorem. *}
 
 lemma helly_induct: fixes f::"(real^'n::finite) set set"
-  assumes "f hassize n" "n \<ge> CARD('n) + 1"
+  assumes "card f = n" "n \<ge> CARD('n) + 1"
   "\<forall>s\<in>f. convex s" "\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   shows "\<Inter> f \<noteq> {}"
-  using assms unfolding hassize_def apply(erule_tac conjE) proof(induct n arbitrary: f)
+using assms proof(induct n arbitrary: f)
 case (Suc n)
-show "\<Inter> f \<noteq> {}" apply(cases "n = CARD('n)") apply(rule Suc(4)[rule_format])
-  unfolding card_Diff_singleton_if[OF Suc(5)] and Suc(6) proof-
+have "finite f" using `card f = Suc n` by (auto intro: card_ge_0_finite)
+show "\<Inter> f \<noteq> {}" apply(cases "n = CARD('n)") apply(rule Suc(5)[rule_format])
+  unfolding `card f = Suc n` proof-
   assume ng:"n \<noteq> CARD('n)" hence "\<exists>X. \<forall>s\<in>f. X s \<in> \<Inter>(f - {s})" apply(rule_tac bchoice) unfolding ex_in_conv
-    apply(rule, rule Suc(1)[rule_format])  unfolding card_Diff_singleton_if[OF Suc(5)] and Suc(6)
-    defer apply(rule Suc(3)[rule_format]) defer apply(rule Suc(4)[rule_format]) using Suc(2,5) by auto
+    apply(rule, rule Suc(1)[rule_format]) unfolding card_Diff_singleton_if[OF `finite f`] `card f = Suc n`
+    defer defer apply(rule Suc(4)[rule_format]) defer apply(rule Suc(5)[rule_format]) using Suc(3) `finite f` by auto
   then obtain X where X:"\<forall>s\<in>f. X s \<in> \<Inter>(f - {s})" by auto
   show ?thesis proof(cases "inj_on X f")
     case False then obtain s t where st:"s\<noteq>t" "s\<in>f" "t\<in>f" "X s = X t" unfolding inj_on_def by auto
@@ -1970,7 +1974,7 @@
       apply(rule, rule X[rule_format]) using X st by auto
   next case True then obtain m p where mp:"m \<inter> p = {}" "m \<union> p = X ` f" "convex hull m \<inter> convex hull p \<noteq> {}"
       using radon_partition[of "X ` f"] and affine_dependent_biggerset[of "X ` f"]
-      unfolding card_image[OF True] and Suc(6) using Suc(2,5) and ng by auto
+      unfolding card_image[OF True] and `card f = Suc n` using Suc(3) `finite f` and ng by auto
     have "m \<subseteq> X ` f" "p \<subseteq> X ` f" using mp(2) by auto
     then obtain g h where gh:"m = X ` g" "p = X ` h" "g \<subseteq> f" "h \<subseteq> f" unfolding subset_image_iff by auto 
     hence "f \<union> (g \<union> h) = f" by auto
@@ -1978,7 +1982,7 @@
       unfolding mp(2)[unfolded image_Un[THEN sym] gh] by auto
     have *:"g \<inter> h = {}" using mp(1) unfolding gh using inj_on_image_Int[OF True gh(3,4)] by auto
     have "convex hull (X ` h) \<subseteq> \<Inter> g" "convex hull (X ` g) \<subseteq> \<Inter> h"
-      apply(rule_tac [!] hull_minimal) using Suc(3) gh(3-4)  unfolding mem_def unfolding subset_eq
+      apply(rule_tac [!] hull_minimal) using Suc gh(3-4)  unfolding mem_def unfolding subset_eq
       apply(rule_tac [2] convex_Inter, rule_tac [4] convex_Inter) apply rule prefer 3 apply rule proof-
       fix x assume "x\<in>X ` g" then guess y unfolding image_iff ..
       thus "x\<in>\<Inter>h" using X[THEN bspec[where x=y]] using * f by auto next
@@ -1989,10 +1993,10 @@
 qed(insert dimindex_ge_1, auto) qed(auto)
 
 lemma helly: fixes f::"(real^'n::finite) set set"
-  assumes "finite f" "card f \<ge> CARD('n) + 1" "\<forall>s\<in>f. convex s"
+  assumes "card f \<ge> CARD('n) + 1" "\<forall>s\<in>f. convex s"
           "\<forall>t\<subseteq>f. card t = CARD('n) + 1 \<longrightarrow> \<Inter> t \<noteq> {}"
   shows "\<Inter> f \<noteq>{}"
-  apply(rule helly_induct) unfolding hassize_def using assms by auto
+  apply(rule helly_induct) using assms by auto
 
 subsection {* Convex hull is "preserved" by a linear function. *}
 
@@ -3379,6 +3383,4 @@
 lemma connected_sphere: "2 \<le> CARD('n) \<Longrightarrow> connected {x::real^'n::finite. norm(x - a) = r}"
   using path_connected_sphere path_connected_imp_connected by auto
  
-(** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
-
 end
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -1642,6 +1642,9 @@
 
 definition "linear f \<longleftrightarrow> (\<forall>x y. f(x + y) = f x + f y) \<and> (\<forall>c x. f(c *s x) = c *s f x)"
 
+lemma linearI: assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *s x) = c *s f x"
+  shows "linear f" using assms unfolding linear_def by auto
+
 lemma linear_compose_cmul: "linear f ==> linear (\<lambda>x. (c::'a::comm_semiring) *s f x)"
   by (vector linear_def Cart_eq ring_simps)
 
@@ -1812,6 +1815,11 @@
     by (simp add: f.add f.scaleR)
 qed
 
+lemma bounded_linearI': fixes f::"real^'n::finite \<Rightarrow> real^'m::finite"
+  assumes "\<And>x y. f (x + y) = f x + f y" "\<And>c x. f (c *s x) = c *s f x"
+  shows "bounded_linear f" unfolding linear_conv_bounded_linear[THEN sym]
+  by(rule linearI[OF assms])
+
 subsection{* Bilinear functions. *}
 
 definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
@@ -2470,6 +2478,11 @@
 lemma vec1_cmul: "vec1(c* x) = c *s vec1 x " by (vector vec1_def)
 lemma vec1_neg: "vec1(- x) = - vec1 x " by (vector vec1_def)
 
+lemma vec1_0[simp]:"vec1 0 = 0" unfolding vec1_def Cart_eq by auto
+
+lemma range_vec1[simp]:"range vec1 = UNIV" apply(rule set_ext,rule) unfolding image_iff defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
 lemma vec1_setsum: assumes fS: "finite S"
   shows "vec1(setsum f S) = setsum (vec1 o f) S"
   apply (induct rule: finite_induct[OF fS])
@@ -2512,6 +2525,14 @@
 lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
   by (metis vec1_dest_vec1 norm_vec1)
 
+lemmas vec1_dest_vec1_simps = forall_vec1 vec1_add[THEN sym] dist_vec1 vec1_sub[THEN sym] vec1_dest_vec1 norm_vec1 dest_vec1_cmul
+   vec1_eq vec1_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def
+
+lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
+  unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
+  unfolding smult_conv_scaleR[THEN sym] unfolding vec1_dest_vec1_simps
+  apply(rule conjI) defer apply(rule conjI) defer apply(rule_tac x=1 in exI) by auto
+
 lemma linear_vmul_dest_vec1:
   fixes f:: "'a::semiring_1^'n \<Rightarrow> 'a^1"
   shows "linear f \<Longrightarrow> linear (\<lambda>x. dest_vec1(f x) *s v)"
@@ -3415,21 +3436,18 @@
 apply (auto simp add: Collect_def mem_def)
 done
 
-lemma has_size_stdbasis: "{basis i ::real ^'n::finite | i. i \<in> (UNIV :: 'n set)} hassize CARD('n)" (is "?S hassize ?n")
+lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
 proof-
   have eq: "?S = basis ` UNIV" by blast
-  show ?thesis unfolding eq
-    apply (rule hassize_image_inj[OF basis_inj])
-    by (simp add: hassize_def)
+  show ?thesis unfolding eq by auto
 qed
 
-lemma finite_stdbasis: "finite {basis i ::real^'n::finite |i. i\<in> (UNIV:: 'n set)}"
-  using has_size_stdbasis[unfolded hassize_def]
-  ..
-
-lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)} = CARD('n)"
-  using has_size_stdbasis[unfolded hassize_def]
-  ..
+lemma card_stdbasis: "card {basis i ::real^'n::finite |i. i\<in> (UNIV :: 'n set)} = CARD('n)" (is "card ?S = _")
+proof-
+  have eq: "?S = basis ` UNIV" by blast
+  show ?thesis unfolding eq using card_image[OF basis_inj] by simp
+qed
+
 
 lemma independent_stdbasis_lemma:
   assumes x: "(x::'a::semiring_1 ^ 'n) \<in> span (basis ` S)"
@@ -3550,7 +3568,7 @@
 lemma exchange_lemma:
   assumes f:"finite (t:: ('a::field^'n) set)" and i: "independent s"
   and sp:"s \<subseteq> span t"
-  shows "\<exists>t'. (t' hassize card t) \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
+  shows "\<exists>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
 using f i sp
 proof(induct c\<equiv>"card(t - s)" arbitrary: s t rule: nat_less_induct)
   fix n:: nat and s t :: "('a ^'n) set"
@@ -3559,21 +3577,21 @@
                 independent x \<longrightarrow>
                 x \<subseteq> span xa \<longrightarrow>
                 m = card (xa - x) \<longrightarrow>
-                (\<exists>t'. (t' hassize card xa) \<and>
+                (\<exists>t'. (card t' = card xa) \<and> finite t' \<and>
                       x \<subseteq> t' \<and> t' \<subseteq> x \<union> xa \<and> x \<subseteq> span t')"
     and ft: "finite t" and s: "independent s" and sp: "s \<subseteq> span t"
     and n: "n = card (t - s)"
-  let ?P = "\<lambda>t'. (t' hassize card t) \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
+  let ?P = "\<lambda>t'. (card t' = card t) \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
   let ?ths = "\<exists>t'. ?P t'"
   {assume st: "s \<subseteq> t"
     from st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
-      by (auto simp add: hassize_def intro: span_superset)}
+      by (auto intro: span_superset)}
   moreover
   {assume st: "t \<subseteq> s"
 
     from spanning_subset_independent[OF st s sp]
       st ft span_mono[OF st] have ?ths apply - apply (rule exI[where x=t])
-      by (auto simp add: hassize_def intro: span_superset)}
+      by (auto intro: span_superset)}
   moreover
   {assume st: "\<not> s \<subseteq> t" "\<not> t \<subseteq> s"
     from st(2) obtain b where b: "b \<in> t" "b \<notin> s" by blast
@@ -3584,20 +3602,20 @@
     {assume stb: "s \<subseteq> span(t -{b})"
       from ft have ftb: "finite (t -{b})" by auto
       from H[rule_format, OF cardlt ftb s stb]
-      obtain u where u: "u hassize card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" by blast
+      obtain u where u: "card u = card (t-{b})" "s \<subseteq> u" "u \<subseteq> s \<union> (t - {b})" "s \<subseteq> span u" and fu: "finite u" by blast
       let ?w = "insert b u"
       have th0: "s \<subseteq> insert b u" using u by blast
       from u(3) b have "u \<subseteq> s \<union> t" by blast
       then have th1: "insert b u \<subseteq> s \<union> t" using u b by blast
       have bu: "b \<notin> u" using b u by blast
-      from u(1) have fu: "finite u" by (simp add: hassize_def)
-      from u(1) ft b have "u hassize (card t - 1)" by auto
+      from u(1) ft b have "card u = (card t - 1)" by auto
       then
-      have th2: "insert b u hassize card t"
-        using  card_insert_disjoint[OF fu bu] ct0 by (auto simp add: hassize_def)
+      have th2: "card (insert b u) = card t"
+        using card_insert_disjoint[OF fu bu] ct0 by auto
       from u(4) have "s \<subseteq> span u" .
       also have "\<dots> \<subseteq> span (insert b u)" apply (rule span_mono) by blast
-      finally have th3: "s \<subseteq> span (insert b u)" .      from th0 th1 th2 th3 have th: "?P ?w"  by blast
+      finally have th3: "s \<subseteq> span (insert b u)" .
+      from th0 th1 th2 th3 fu have th: "?P ?w"  by blast
       from th have ?ths by blast}
     moreover
     {assume stb: "\<not> s \<subseteq> span(t -{b})"
@@ -3619,9 +3637,9 @@
       then have sp': "s \<subseteq> span (insert a (t - {b}))" by blast
 
       from H[rule_format, OF mlt ft' s sp' refl] obtain u where
-        u: "u hassize card (insert a (t -{b}))" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
+        u: "card u = card (insert a (t -{b}))" "finite u" "s \<subseteq> u" "u \<subseteq> s \<union> insert a (t -{b})"
         "s \<subseteq> span u" by blast
-      from u a b ft at ct0 have "?P u" by (auto simp add: hassize_def)
+      from u a b ft at ct0 have "?P u" by auto
       then have ?ths by blast }
     ultimately have ?ths by blast
   }
@@ -3634,7 +3652,7 @@
 lemma independent_span_bound:
   assumes f: "finite t" and i: "independent (s::('a::field^'n) set)" and sp:"s \<subseteq> span t"
   shows "finite s \<and> card s \<le> card t"
-  by (metis exchange_lemma[OF f i sp] hassize_def finite_subset card_mono)
+  by (metis exchange_lemma[OF f i sp] finite_subset card_mono)
 
 
 lemma finite_Atleast_Atmost_nat[simp]: "finite {f x |x. x\<in> (UNIV::'a::finite set)}"
@@ -3702,39 +3720,44 @@
 
 (* Notion of dimension.                                                      *)
 
-definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n))"
-
-lemma basis_exists:  "\<exists>B. (B :: (real ^'n::finite) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize dim V)"
-unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (B hassize n)"]
-unfolding hassize_def
+definition "dim V = (SOME n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n))"
+
+lemma basis_exists:  "\<exists>B. (B :: (real ^'n::finite) set) \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = dim V)"
+unfolding dim_def some_eq_ex[of "\<lambda>n. \<exists>B. B \<subseteq> V \<and> independent B \<and> V \<subseteq> span B \<and> (card B = n)"]
 using maximal_independent_subset[of V] independent_bound
 by auto
 
 (* Consequences of independence or spanning for cardinality.                 *)
 
-lemma independent_card_le_dim: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B \<le> dim V"
-by (metis basis_exists[of V] independent_span_bound[where ?'a=real] hassize_def subset_trans)
+lemma independent_card_le_dim: 
+  assumes "(B::(real ^'n::finite) set) \<subseteq> V" and "independent B" shows "card B \<le> dim V"
+proof -
+  from basis_exists[of V] `B \<subseteq> V`
+  obtain B' where "independent B'" and "B \<subseteq> span B'" and "card B' = dim V" by blast
+  with independent_span_bound[OF _ `independent B` `B \<subseteq> span B'`] independent_bound[of B']
+  show ?thesis by auto
+qed
 
 lemma span_card_ge_dim:  "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> finite B \<Longrightarrow> dim V \<le> card B"
-  by (metis basis_exists[of V] independent_span_bound hassize_def subset_trans)
+  by (metis basis_exists[of V] independent_span_bound subset_trans)
 
 lemma basis_card_eq_dim:
   "B \<subseteq> (V:: (real ^'n::finite) set) \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> finite B \<and> card B = dim V"
-  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono)
-
-lemma dim_unique: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> B hassize n \<Longrightarrow> dim V = n"
-  by (metis basis_card_eq_dim hassize_def)
+  by (metis order_eq_iff independent_card_le_dim span_card_ge_dim independent_mono independent_bound)
+
+lemma dim_unique: "(B::(real ^'n::finite) set) \<subseteq> V \<Longrightarrow> V \<subseteq> span B \<Longrightarrow> independent B \<Longrightarrow> card B = n \<Longrightarrow> dim V = n"
+  by (metis basis_card_eq_dim)
 
 (* More lemmas about dimension.                                              *)
 
 lemma dim_univ: "dim (UNIV :: (real^'n::finite) set) = CARD('n)"
   apply (rule dim_unique[of "{basis i |i. i\<in> (UNIV :: 'n set)}"])
-  by (auto simp only: span_stdbasis has_size_stdbasis independent_stdbasis)
+  by (auto simp only: span_stdbasis card_stdbasis finite_stdbasis independent_stdbasis)
 
 lemma dim_subset:
   "(S:: (real ^'n::finite) set) \<subseteq> T \<Longrightarrow> dim S \<le> dim T"
   using basis_exists[of T] basis_exists[of S]
-  by (metis independent_span_bound[where ?'a = real and ?'n = 'n] subset_eq hassize_def)
+  by (metis independent_card_le_dim subset_trans)
 
 lemma dim_subset_univ: "dim (S:: (real^'n::finite) set) \<le> CARD('n)"
   by (metis dim_subset subset_UNIV dim_univ)
@@ -3750,7 +3773,7 @@
       then have iaB: "independent (insert a B)" using iB aV  BV by (simp add: independent_insert)
       from aV BV have th0: "insert a B \<subseteq> V" by blast
       from aB have "a \<notin>B" by (auto simp add: span_superset)
-      with independent_card_le_dim[OF th0 iaB] dVB  have False by auto}
+      with independent_card_le_dim[OF th0 iaB] dVB independent_bound[OF iB] have False by auto }
     then have "a \<in> span B"  by blast}
   then show ?thesis by blast
 qed
@@ -3777,8 +3800,8 @@
   then show ?thesis unfolding dependent_def by blast
 qed
 
-lemma card_eq_dim: "(B:: (real ^'n::finite) set) \<subseteq> V \<Longrightarrow> B hassize dim V \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
-  by (metis hassize_def order_eq_iff card_le_dim_spanning
+lemma card_eq_dim: "(B:: (real ^'n::finite) set) \<subseteq> V \<Longrightarrow> card B = dim V \<Longrightarrow> finite B \<Longrightarrow> independent B \<longleftrightarrow> V \<subseteq> span B"
+  by (metis order_eq_iff card_le_dim_spanning
     card_ge_dim_independent)
 
 (* ------------------------------------------------------------------------- *)
@@ -3797,8 +3820,8 @@
   have th0: "dim S \<le> dim (span S)"
     by (auto simp add: subset_eq intro: dim_subset span_superset)
   from basis_exists[of S]
-  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast
-  from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+
+  obtain B where B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
+  from B have fB: "finite B" "card B = dim S" using independent_bound by blast+
   have bSS: "B \<subseteq> span S" using B(1) by (metis subset_eq span_inc)
   have sssB: "span S \<subseteq> span B" using span_mono[OF B(3)] by (simp add: span_span)
   from span_card_ge_dim[OF bSS sssB fB(1)] th0 show ?thesis
@@ -3822,8 +3845,8 @@
   assumes lf: "linear f" shows "dim (f ` S) \<le> dim (S:: (real ^'n::finite) set)"
 proof-
   from basis_exists[of S] obtain B where
-    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast
-  from B have fB: "finite B" "card B = dim S" unfolding hassize_def by blast+
+    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" by blast
+  from B have fB: "finite B" "card B = dim S" using independent_bound by blast+
   have "dim (f ` S) \<le> card (f ` B)"
     apply (rule span_card_ge_dim)
     using lf B fB by (auto simp add: span_linear_image spans_image subset_image_iff)
@@ -3947,10 +3970,10 @@
 
 lemma orthogonal_basis_exists:
   fixes V :: "(real ^'n::finite) set"
-  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (B hassize dim V) \<and> pairwise orthogonal B"
+  shows "\<exists>B. independent B \<and> B \<subseteq> span V \<and> V \<subseteq> span B \<and> (card B = dim V) \<and> pairwise orthogonal B"
 proof-
-  from basis_exists[of V] obtain B where B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "B hassize dim V" by blast
-  from B have fB: "finite B" "card B = dim V" by (simp_all add: hassize_def)
+  from basis_exists[of V] obtain B where B: "B \<subseteq> V" "independent B" "V \<subseteq> span B" "card B = dim V" by blast
+  from B have fB: "finite B" "card B = dim V" using independent_bound by auto
   from basis_orthogonal[OF fB(1)] obtain C where
     C: "finite C" "card C \<le> card B" "span C = span B" "pairwise orthogonal C" by blast
   from C B
@@ -3961,7 +3984,7 @@
   from C fB have "card C \<le> dim V" by simp
   moreover have "dim V \<le> card C" using span_card_ge_dim[OF CSV SVC C(1)]
     by (simp add: dim_span)
-  ultimately have CdV: "C hassize dim V" unfolding hassize_def using C(1) by simp
+  ultimately have CdV: "card C = dim V" using C(1) by simp
   from C B CSV CdV iC show ?thesis by auto
 qed
 
@@ -3978,9 +4001,9 @@
 proof-
   from sU obtain a where a: "a \<notin> span S" by blast
   from orthogonal_basis_exists obtain B where
-    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "B hassize dim S" "pairwise orthogonal B"
+    B: "independent B" "B \<subseteq> span S" "S \<subseteq> span B" "card B = dim S" "pairwise orthogonal B"
     by blast
-  from B have fB: "finite B" "card B = dim S" by (simp_all add: hassize_def)
+  from B have fB: "finite B" "card B = dim S" using independent_bound by auto
   from span_mono[OF B(2)] span_mono[OF B(3)]
   have sSB: "span S = span B" by (simp add: span_span)
   let ?a = "a - setsum (\<lambda>b. (a\<bullet>b / (b\<bullet>b)) *s b) B"
@@ -4228,20 +4251,18 @@
   and d: "dim S = dim T"
   shows "\<exists>f. linear f \<and> f ` S = T \<and> inj_on f S"
 proof-
-  from basis_exists[of S] obtain B where
-    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "B hassize dim S" by blast
-  from basis_exists[of T] obtain C where
-    C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "C hassize dim T" by blast
+  from basis_exists[of S] independent_bound obtain B where
+    B: "B \<subseteq> S" "independent B" "S \<subseteq> span B" "card B = dim S" and fB: "finite B" by blast
+  from basis_exists[of T] independent_bound obtain C where
+    C: "C \<subseteq> T" "independent C" "T \<subseteq> span C" "card C = dim T" and fC: "finite C" by blast
   from B(4) C(4) card_le_inj[of B C] d obtain f where
-    f: "f ` B \<subseteq> C" "inj_on f B" unfolding hassize_def by auto
+    f: "f ` B \<subseteq> C" "inj_on f B" using `finite B` `finite C` by auto
   from linear_independent_extend[OF B(2)] obtain g where
     g: "linear g" "\<forall>x\<in> B. g x = f x" by blast
-  from B(4) have fB: "finite B" by (simp add: hassize_def)
-  from C(4) have fC: "finite C" by (simp add: hassize_def)
   from inj_on_iff_eq_card[OF fB, of f] f(2)
   have "card (f ` B) = card B" by simp
   with B(4) C(4) have ceq: "card (f ` B) = card C" using d
-    by (simp add: hassize_def)
+    by simp
   have "g ` B = f ` B" using g(2)
     by (auto simp add: image_iff)
   also have "\<dots> = C" using card_subset_eq[OF fC f(1) ceq] .
@@ -4557,9 +4578,9 @@
 proof-
   let ?U = "UNIV :: (real ^'n) set"
   from basis_exists[of ?U] obtain B
-    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"
+    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "card B = dim ?U"
     by blast
-  from B(4) have d: "dim ?U = card B" by (simp add: hassize_def)
+  from B(4) have d: "dim ?U = card B" by simp
   have th: "?U \<subseteq> span (f ` B)"
     apply (rule card_ge_dim_independent)
     apply blast
@@ -4619,11 +4640,10 @@
 proof-
   let ?U = "UNIV :: (real ^'n) set"
   from basis_exists[of ?U] obtain B
-    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" "B hassize dim ?U"
+    where B: "B \<subseteq> ?U" "independent B" "?U \<subseteq> span B" and d: "card B = dim ?U"
     by blast
   {fix x assume x: "x \<in> span B" and fx: "f x = 0"
-    from B(4) have fB: "finite B" by (simp add: hassize_def)
-    from B(4) have d: "dim ?U = card B" by (simp add: hassize_def)
+    from B(2) have fB: "finite B" using independent_bound by auto
     have fBi: "independent (f ` B)"
       apply (rule card_le_dim_spanning[of "f ` B" ?U])
       apply blast
@@ -4631,7 +4651,7 @@
       unfolding span_linear_image[OF lf] surj_def subset_eq image_iff
       apply blast
       using fB apply (blast intro: finite_imageI)
-      unfolding d
+      unfolding d[symmetric]
       apply (rule card_image_le)
       apply (rule fB)
       done
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -8,15 +8,6 @@
 imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
 begin
 
-definition hassize (infixr "hassize" 12) where
-  "(S hassize n) = (finite S \<and> card S = n)"
-
-lemma hassize_image_inj: assumes f: "inj_on f S" and S: "S hassize n"
-  shows "f ` S hassize n"
-  using f S card_image[OF f]
-    by (simp add: hassize_def inj_on_def)
-
-
 subsection {* Finite Cartesian products, with indexing and lambdas. *}
 
 typedef (open Cart)
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Library/Topology_Euclidian_Space.thy
+(*  title:      HOL/Library/Topology_Euclidian_Space.thy
     Author:     Amine Chaieb, University of Cambridge
     Author:     Robert Himmelmann, TU Muenchen
 *)
@@ -275,6 +275,11 @@
 lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
   unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
 
+lemma openE[elim?]:
+  assumes "open S" "x\<in>S" 
+  obtains e where "e>0" "ball x e \<subseteq> S"
+  using assms unfolding open_contains_ball by auto
+
 lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
   by (metis open_contains_ball subset_eq centre_in_ball)
 
@@ -4011,6 +4016,9 @@
   shows "bounded_linear f ==> continuous_on s f"
   using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
 
+lemma continuous_on_vec1:"continuous_on A (vec1::real\<Rightarrow>real^1)"
+  by(rule linear_continuous_on[OF bounded_linear_vec1])
+
 text{* Also bilinear functions, in composition form.                             *}
 
 lemma bilinear_continuous_at_compose:
@@ -4195,6 +4203,8 @@
   shows "(c ---> d) net ==> ((\<lambda>x. c(x) *\<^sub>R v) ---> d *\<^sub>R v) net"
   by (intro tendsto_intros)
 
+lemmas Lim_intros = Lim_add Lim_const Lim_sub Lim_cmul Lim_vmul Lim_within_id
+
 lemma continuous_vmul:
   fixes c :: "'a::metric_space \<Rightarrow> real" and v :: "'b::real_normed_vector"
   shows "continuous net c ==> continuous net (\<lambda>x. c(x) *\<^sub>R v)"
@@ -4621,6 +4631,15 @@
  "(x \<in> {a<..<b} \<longleftrightarrow> dest_vec1 a < dest_vec1 x \<and> dest_vec1 x < dest_vec1 b)"
 by(simp_all add: Cart_eq vector_less_def vector_less_eq_def dest_vec1_def forall_1)
 
+lemma vec1_interval:fixes a::"real" shows
+  "vec1 ` {a .. b} = {vec1 a .. vec1 b}"
+  "vec1 ` {a<..<b} = {vec1 a<..<vec1 b}"
+  apply(rule_tac[!] set_ext) unfolding image_iff vector_less_def unfolding mem_interval
+  unfolding forall_1  unfolding dest_vec1_def[THEN sym, of] unfolding vec1_dest_vec1_simps
+  apply rule defer apply(rule_tac x="dest_vec1 x" in bexI) prefer 3 apply rule defer
+  apply(rule_tac x="dest_vec1 x" in bexI) by auto
+
+
 lemma interval_eq_empty: fixes a :: "real^'n::finite" shows
  "({a <..< b} = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) and
  "({a  ..  b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2)
@@ -4802,6 +4821,12 @@
   thus ?thesis unfolding open_dist using open_interval_lemma by auto
 qed
 
+lemma open_interval_real: fixes a :: "real" shows "open {a<..<b}"
+  using open_interval[of "vec1 a" "vec1 b"] unfolding open_contains_ball
+  apply-apply(rule,erule_tac x="vec1 x" in ballE) apply(erule exE,rule_tac x=e in exI)
+  unfolding subset_eq mem_ball apply(rule) defer apply(rule,erule conjE,erule_tac x="vec1 xa" in ballE)
+  by(auto simp add: vec1_dest_vec1_simps vector_less_def forall_1) 
+
 lemma closed_interval: fixes a :: "real^'n::finite" shows "closed {a .. b}"
 proof-
   { fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)
@@ -5604,7 +5629,7 @@
   moreover
   have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
   hence *:"inj_on (basis::'n\<Rightarrow>real^'n) d" using subset_inj_on[OF basis_inj, of "d"] by auto
-  have "?B hassize (card d)" unfolding hassize_def and card_image[OF *] by auto
+  have "card ?B = card d" unfolding card_image[OF *] by auto
 
   ultimately show ?thesis using dim_unique[of "basis ` d" ?A] by auto
 qed
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -20,7 +20,7 @@
 
 The original theory, "IntPrimes", by Thomas M. Rasmussen, defined and
 developed the congruence relations on the integers. The notion was
-extended to the natural numbers by Chiaeb. Jeremy Avigad combined
+extended to the natural numbers by Chaieb. Jeremy Avigad combined
 these, revised and tidied them, made the development uniform for the
 natural numbers and the integers, and added a number of new theorems.
 
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Number_Theory/Primes.thy	Mon Nov 16 20:23:02 2009 +0100
@@ -16,7 +16,7 @@
 another extension of the notions to the integers, and added a number
 of results to "Primes" and "GCD". IntPrimes also defined and developed
 the congruence relations on the integers. The notion was extended to
-the natural numbers by Chiaeb.
+the natural numbers by Chaieb.
 
 Jeremy Avigad combined all of these, made everything uniform for the
 natural numbers and the integers, and added a number of new theorems.
diff -r 5249bbca5fab -r d15212c7501c src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Nov 16 13:53:31 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Nov 16 20:23:02 2009 +0100
@@ -459,7 +459,7 @@
       in
         SOME [(HOLogic.natT :: Ts, subgoal1), (Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) mod (number_of ?k)) =
+    (* ?P ((?n::nat) mod (number_of ?k)) =
          ((number_of ?k = 0 --> ?P ?n) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P j))) *)
     | (Const ("Divides.div_class.mod", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
@@ -491,7 +491,7 @@
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::nat) div (number_of ?k)) =
+    (* ?P ((?n::nat) div (number_of ?k)) =
          ((number_of ?k = 0 --> ?P 0) & (~ (number_of ?k = 0) -->
            (ALL i j. j < number_of ?k --> ?n = number_of ?k * i + j --> ?P i))) *)
     | (Const ("Divides.div_class.div", Type ("fun", [Type ("nat", []), _])), [t1, t2]) =>
@@ -523,7 +523,7 @@
       in
         SOME [(Ts, subgoal1), (split_type :: split_type :: Ts, subgoal2)]
       end
-    (* "?P ((?n::int) mod (number_of ?k)) =
+    (* ?P ((?n::int) mod (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P ?n) &
           (neg (number_of (uminus ?k)) -->
             (ALL i j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j --> ?P j)) &
@@ -575,7 +575,7 @@
       in
         SOME [(Ts, subgoal1), (Ts', subgoal2), (Ts', subgoal3)]
       end
-    (* "?P ((?n::int) div (number_of ?k)) =
+    (* ?P ((?n::int) div (number_of ?k)) =
          ((iszero (number_of ?k) --> ?P 0) &
           (neg (number_of (uminus ?k)) -->
             (ALL i. (EX j. 0 <= j & j < number_of ?k & ?n = number_of ?k * i + j) --> ?P i)) &