author wenzelm Fri, 07 Sep 2012 15:15:07 +0200 changeset 49197 e5224d887e12 parent 49196 1d63ceb0d177 child 49198 38af9102ee75
tuned proofs;
```--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 07 15:00:03 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 07 15:15:07 2012 +0200
@@ -57,23 +57,39 @@

text{* The ordering on one-dimensional vectors is linear. *}

-class cart_one = assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
+class cart_one =
+  assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0"
begin
-  subclass finite
-  proof from UNIV_one show "finite (UNIV :: 'a set)"
-      by (auto intro!: card_ge_0_finite) qed
+
+subclass finite
+proof
+  from UNIV_one show "finite (UNIV :: 'a set)"
+    by (auto intro!: card_ge_0_finite)
+qed
+
end

-instantiation vec :: (linorder,cart_one) linorder begin
-instance proof
-  guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+
-  hence *:"UNIV = {a}" by auto
-  have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P a" unfolding * by auto hence all:"\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" by auto
-  fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff
-  show "x\<le>x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x\<le>y \<or> y\<le>x" unfolding * by(auto simp only:field_simps)
-  { assume "x\<le>y" "y\<le>z" thus "x\<le>z" unfolding * by(auto simp only:field_simps) }
-  { assume "x\<le>y" "y\<le>x" thus "x=y" unfolding * by(auto simp only:field_simps) }
-qed end
+instantiation vec :: (linorder, cart_one) linorder
+begin
+
+instance
+proof
+  obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a"
+  proof -
+    have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one)
+    then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq)
+    then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto
+    then show thesis by (auto intro: that)
+  qed
+
+  note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps
+  fix x y z :: "'a^'b::cart_one"
+  show "x \<le> x" "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" "x \<le> y \<or> y \<le> x" by auto
+  { assume "x\<le>y" "y\<le>z" then show "x\<le>z" by auto }
+  { assume "x\<le>y" "y\<le>x" then show "x=y" by auto }
+qed
+
+end

text{* Constant Vectors *}

@@ -1986,12 +2002,21 @@
unfolding simps unfolding *(1)[of "\<lambda>i x. b\$i - x"] *(1)[of "\<lambda>i x. x - a\$i"] *(2) by(auto)
qed*)

-lemma has_integral_vec1: assumes "(f has_integral k) {a..b}"
+lemma has_integral_vec1:
+  assumes "(f has_integral k) {a..b}"
shows "((\<lambda>x. vec1 (f x)) has_integral (vec1 k)) {a..b}"
-proof- have *:"\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
-    unfolding vec_sub vec_eq_iff by(auto simp add: split_beta)
-  show ?thesis using assms unfolding has_integral apply safe
-    apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe)
-    apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed
+proof -
+  have *: "\<And>p. (\<Sum>(x, k)\<in>p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f x) - k)"
+    unfolding vec_sub vec_eq_iff by (auto simp add: split_beta)
+  show ?thesis
+    using assms unfolding has_integral
+    apply safe
+    apply(erule_tac x=e in allE,safe)
+    apply(rule_tac x=d in exI,safe)
+    apply(erule_tac x=p in allE,safe)
+    unfolding * norm_vector_1
+    apply auto
+    done
+qed

end```
```--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 15:00:03 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Sep 07 15:15:07 2012 +0200
@@ -1771,31 +1771,33 @@
lemma forall_option: "(\<forall>x. P x) \<longleftrightarrow> P None \<and> (\<forall>x. P(Some x))"
by (metis option.nchotomy)

-lemma exists_option:
- "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
+lemma exists_option: "(\<exists>x. P x) \<longleftrightarrow> P None \<or> (\<exists>x. P(Some x))"
by (metis option.nchotomy)

-fun lifted where
-  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some(opp x y)" |
-  "lifted opp None _ = (None::'b option)" |
-  "lifted opp _ None = None"
+fun lifted
+where
+  "lifted (opp::'a\<Rightarrow>'a\<Rightarrow>'b) (Some x) (Some y) = Some (opp x y)"
+| "lifted opp None _ = (None::'b option)"
+| "lifted opp _ None = None"

lemma lifted_simp_1[simp]: "lifted opp v None = None"
-  apply(induct v) by auto
+  by (induct v) auto

definition "monoidal opp \<equiv>  (\<forall>x y. opp x y = opp y x) \<and>
(\<forall>x y z. opp x (opp y z) = opp (opp x y) z) \<and>
(\<forall>x. opp (neutral opp) x = x)"

-lemma monoidalI: assumes "\<And>x y. opp x y = opp y x"
+lemma monoidalI:
+  assumes "\<And>x y. opp x y = opp y x"
"\<And>x y z. opp x (opp y z) = opp (opp x y) z"
"\<And>x. opp (neutral opp) x = x" shows "monoidal opp"
unfolding monoidal_def using assms by fastforce

-lemma monoidal_ac: assumes "monoidal opp"
+lemma monoidal_ac:
+  assumes "monoidal opp"
shows "opp (neutral opp) a = a" "opp a (neutral opp) = a" "opp a b = opp b a"
"opp (opp a b) c = opp a (opp b c)"  "opp a (opp b c) = opp b (opp a c)"
-  using assms unfolding monoidal_def apply- by metis+
+  using assms unfolding monoidal_def by metis+

lemma monoidal_simps[simp]: assumes "monoidal opp"
shows "opp (neutral opp) a = a" "opp a (neutral opp) = a"
@@ -1804,10 +1806,14 @@
lemma neutral_lifted[cong]: assumes "monoidal opp"
shows "neutral (lifted opp) = Some(neutral opp)"
apply(subst neutral_def) apply(rule some_equality) apply(rule,induct_tac y) prefer 3
-proof- fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
-  thus "x = Some (neutral opp)" apply(induct x) defer
+proof -
+  fix x assume "\<forall>y. lifted opp x y = y \<and> lifted opp y x = y"
+  thus "x = Some (neutral opp)"
+    apply(induct x) defer
apply rule apply(subst neutral_def) apply(subst eq_commute,rule some_equality)
-    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE) by auto
+    apply(rule,erule_tac x="Some y" in allE) defer apply(erule_tac x="Some x" in allE)
+    apply auto
+    done