equal
deleted
inserted
replaced
738 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
738 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
739 unfolding mem_interval_cart forall_2 vector_2 |
739 unfolding mem_interval_cart forall_2 vector_2 |
740 using ab startfin abab assms(3) |
740 using ab startfin abab assms(3) |
741 using assms(9-) |
741 using assms(9-) |
742 unfolding assms |
742 unfolding assms |
743 apply (auto simp add: field_simps box) |
743 apply (auto simp add: field_simps box_def) |
744 done |
744 done |
745 then show "path_image ?P1 \<subseteq> cbox ?a ?b" . |
745 then show "path_image ?P1 \<subseteq> cbox ?a ?b" . |
746 have "path_image ?P2 \<subseteq> cbox ?a ?b" |
746 have "path_image ?P2 \<subseteq> cbox ?a ?b" |
747 unfolding P1P2 path_image_linepath |
747 unfolding P1P2 path_image_linepath |
748 apply (rule Un_least)+ |
748 apply (rule Un_least)+ |
750 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
750 apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format]) |
751 unfolding mem_interval_cart forall_2 vector_2 |
751 unfolding mem_interval_cart forall_2 vector_2 |
752 using ab startfin abab assms(4) |
752 using ab startfin abab assms(4) |
753 using assms(9-) |
753 using assms(9-) |
754 unfolding assms |
754 unfolding assms |
755 apply (auto simp add: field_simps box) |
755 apply (auto simp add: field_simps box_def) |
756 done |
756 done |
757 then show "path_image ?P2 \<subseteq> cbox ?a ?b" . |
757 then show "path_image ?P2 \<subseteq> cbox ?a ?b" . |
758 show "a $ 1 - 2 = a $ 1 - 2" |
758 show "a $ 1 - 2 = a $ 1 - 2" |
759 and "b $ 1 + 2 = b $ 1 + 2" |
759 and "b $ 1 + 2 = b $ 1 + 2" |
760 and "pathstart g $ 2 - 3 = a $ 2 - 3" |
760 and "pathstart g $ 2 - 3 = a $ 2 - 3" |