--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Feb 21 20:54:40 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Sun Feb 21 20:55:12 2010 +0100
@@ -1,4 +1,4 @@
-(* Title: Library/Euclidean_Space
+(* Title: Library/Multivariate_Analysis/Euclidean_Space.thy
Author: Amine Chaieb, University of Cambridge
*)
@@ -66,8 +66,8 @@
instantiation cart :: (plus,finite) plus
begin
-definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))"
-instance ..
+ definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))"
+ instance ..
end
instantiation cart :: (times,finite) times
@@ -76,39 +76,42 @@
instance ..
end
-instantiation cart :: (minus,finite) minus begin
+instantiation cart :: (minus,finite) minus
+begin
definition vector_minus_def : "op - \<equiv> (\<lambda> x y. (\<chi> i. (x$i) - (y$i)))"
-instance ..
+ instance ..
end
-instantiation cart :: (uminus,finite) uminus begin
+instantiation cart :: (uminus,finite) uminus
+begin
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))"
-instance ..
+ instance ..
end
-instantiation cart :: (zero,finite) zero begin
+instantiation cart :: (zero,finite) zero
+begin
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)"
-instance ..
+ instance ..
end
-instantiation cart :: (one,finite) one begin
+instantiation cart :: (one,finite) one
+begin
definition vector_one_def : "1 \<equiv> (\<chi> i. 1)"
-instance ..
+ instance ..
end
instantiation cart :: (ord,finite) ord
- begin
-definition vector_le_def:
- "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
-definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
-
-instance by (intro_classes)
+begin
+ definition vector_le_def:
+ "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)"
+ definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)"
+ instance by (intro_classes)
end
instantiation cart :: (scaleR, finite) scaleR
begin
-definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
-instance ..
+ definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))"
+ instance ..
end
text{* Also the scalar-vector multiplication. *}
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Feb 21 20:54:40 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Sun Feb 21 20:55:12 2010 +0100
@@ -1,11 +1,11 @@
-(* Title: HOL/Library/Finite_Cartesian_Product
- Author: Amine Chaieb, University of Cambridge
+(* Title: HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
+ Author: Amine Chaieb, University of Cambridge
*)
header {* Definition of finite Cartesian product types. *}
theory Finite_Cartesian_Product
-imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
+imports Main
begin
subsection {* Finite Cartesian products, with indexing and lambdas. *}
@@ -39,10 +39,7 @@
*}
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
- apply auto
- apply (rule ext)
- apply auto
- done
+ by (auto intro: ext)
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
by (simp add: Cart_nth_inject [symmetric] expand_fun_eq)
@@ -75,7 +72,10 @@
unfolding sndcart_def by simp
lemma finite_sum_image: "(UNIV::('a + 'b) set) = range Inl \<union> range Inr"
-by (auto, case_tac x, auto)
+ apply auto
+ apply (case_tac x)
+ apply auto
+ done
lemma fstcart_pastecart[simp]: "fstcart (pastecart x y) = x"
by (simp add: Cart_eq)
@@ -90,9 +90,9 @@
using pastecart_fst_snd[of x] pastecart_fst_snd[of y] by metis
lemma forall_pastecart: "(\<forall>p. P p) \<longleftrightarrow> (\<forall>x y. P (pastecart x y))"
- by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+ by (metis pastecart_fst_snd)
-lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
- by (metis pastecart_fst_snd fstcart_pastecart sndcart_pastecart)
+lemma exists_pastecart: "(\<exists>p. P p) \<longleftrightarrow> (\<exists>x y. P (pastecart x y))"
+ by (metis pastecart_fst_snd)
end