equal
deleted
inserted
replaced
2566 unfolding as[unfolded dist_def] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i] |
2566 unfolding as[unfolded dist_def] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i] |
2567 by(auto simp add:field_simps vector_component_simps) |
2567 by(auto simp add:field_simps vector_component_simps) |
2568 finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto |
2568 finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto |
2569 qed(insert Fal2, auto) qed qed |
2569 qed(insert Fal2, auto) qed qed |
2570 |
2570 |
2571 lemma between_midpoint: |
2571 lemma between_midpoint: fixes a::"real^'n::finite" shows |
2572 "between (a,b) (midpoint a b)" (is ?t1) |
2572 "between (a,b) (midpoint a b)" (is ?t1) |
2573 "between (b,a) (midpoint a b)" (is ?t2) |
2573 "between (b,a) (midpoint a b)" (is ?t2) |
2574 proof- have *:"\<And>x y z. x = (1/2::real) *s z \<Longrightarrow> y = (1/2) *s z \<Longrightarrow> norm z = norm x + norm y" by auto |
2574 proof- have *:"\<And>x y z. x = (1/2::real) *s z \<Longrightarrow> y = (1/2) *s z \<Longrightarrow> norm z = norm x + norm y" by auto |
2575 show ?t1 ?t2 unfolding between midpoint_def dist_def apply(rule_tac[!] *) |
2575 show ?t1 ?t2 unfolding between midpoint_def dist_def apply(rule_tac[!] *) |
2576 by(auto simp add:field_simps Cart_eq vector_component_simps) qed |
2576 by(auto simp add:field_simps Cart_eq vector_component_simps) qed |