# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1474464007 -3600
# Node ID 0efb482beb84e427fdfa37efb3df6fc3bf23fcbb
# Parent  70973a1b4ec0af5c183a4a287c2f0ad6efc57894
vector_add_divide_simps now a "named theorems" bundle

diff -r 70973a1b4ec0 -r 0efb482beb84 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 20 22:31:50 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Sep 21 14:20:07 2016 +0100
@@ -220,7 +220,9 @@
   for y :: "'a::real_vector"
   by (induct A rule: infinite_finite_induct) (simp_all add: algebra_simps)
 
-lemma vector_add_divide_simps:
+named_theorems vector_add_divide_simps "to simplify sums of scaled vectors"
+
+lemma [vector_add_divide_simps]:
   "v + (b / z) *\<^sub>R w = (if z = 0 then v else (z *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
   "a *\<^sub>R v + (b / z) *\<^sub>R w = (if z = 0 then a *\<^sub>R v else ((a * z) *\<^sub>R v + b *\<^sub>R w) /\<^sub>R z)"
   "(a / z) *\<^sub>R v + w = (if z = 0 then w else (a *\<^sub>R v + z *\<^sub>R w) /\<^sub>R z)"
@@ -232,6 +234,17 @@
   for v :: "'a :: real_vector"
   by (simp_all add: divide_inverse_commute scaleR_add_right real_vector.scale_right_diff_distrib)
 
+
+lemma eq_vector_fraction_iff [vector_add_divide_simps]:
+  fixes x :: "'a :: real_vector"
+  shows "(x = (u / v) *\<^sub>R a) \<longleftrightarrow> (if v=0 then x = 0 else v *\<^sub>R x = u *\<^sub>R a)"
+by auto (metis (no_types) divide_eq_1_iff divide_inverse_commute scaleR_one scaleR_scaleR)
+
+lemma vector_fraction_eq_iff [vector_add_divide_simps]:
+  fixes x :: "'a :: real_vector"
+  shows "((u / v) *\<^sub>R a = x) \<longleftrightarrow> (if v=0 then x = 0 else u *\<^sub>R a = v *\<^sub>R x)"
+by (metis eq_vector_fraction_iff)
+
 lemma real_vector_affinity_eq:
   fixes x :: "'a :: real_vector"
   assumes m0: "m \<noteq> 0"