1721 |
1721 |
1722 lemma Infinitesimal_square_cancel [simp]: |
1722 lemma Infinitesimal_square_cancel [simp]: |
1723 "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1723 "(x::hypreal)*x + y*y \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1724 apply (rule Infinitesimal_interval2) |
1724 apply (rule Infinitesimal_interval2) |
1725 apply (rule_tac [3] zero_le_square, assumption) |
1725 apply (rule_tac [3] zero_le_square, assumption) |
1726 apply (auto simp add: zero_le_square) |
1726 apply (auto) |
1727 done |
1727 done |
1728 |
1728 |
1729 lemma HFinite_square_cancel [simp]: |
1729 lemma HFinite_square_cancel [simp]: |
1730 "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite" |
1730 "(x::hypreal)*x + y*y \<in> HFinite ==> x*x \<in> HFinite" |
1731 apply (rule HFinite_bounded, assumption) |
1731 apply (rule HFinite_bounded, assumption) |
1732 apply (auto simp add: zero_le_square) |
1732 apply (auto) |
1733 done |
1733 done |
1734 |
1734 |
1735 lemma Infinitesimal_square_cancel2 [simp]: |
1735 lemma Infinitesimal_square_cancel2 [simp]: |
1736 "(x::hypreal)*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal" |
1736 "(x::hypreal)*x + y*y \<in> Infinitesimal ==> y*y \<in> Infinitesimal" |
1737 apply (rule Infinitesimal_square_cancel) |
1737 apply (rule Infinitesimal_square_cancel) |
1749 lemma Infinitesimal_sum_square_cancel [simp]: |
1749 lemma Infinitesimal_sum_square_cancel [simp]: |
1750 "(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1750 "(x::hypreal)*x + y*y + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1751 apply (rule Infinitesimal_interval2, assumption) |
1751 apply (rule Infinitesimal_interval2, assumption) |
1752 apply (rule_tac [2] zero_le_square, simp) |
1752 apply (rule_tac [2] zero_le_square, simp) |
1753 apply (insert zero_le_square [of y]) |
1753 apply (insert zero_le_square [of y]) |
1754 apply (insert zero_le_square [of z], simp) |
1754 apply (insert zero_le_square [of z], simp del:zero_le_square) |
1755 done |
1755 done |
1756 |
1756 |
1757 lemma HFinite_sum_square_cancel [simp]: |
1757 lemma HFinite_sum_square_cancel [simp]: |
1758 "(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite" |
1758 "(x::hypreal)*x + y*y + z*z \<in> HFinite ==> x*x \<in> HFinite" |
1759 apply (rule HFinite_bounded, assumption) |
1759 apply (rule HFinite_bounded, assumption) |
1760 apply (rule_tac [2] zero_le_square) |
1760 apply (rule_tac [2] zero_le_square) |
1761 apply (insert zero_le_square [of y]) |
1761 apply (insert zero_le_square [of y]) |
1762 apply (insert zero_le_square [of z], simp) |
1762 apply (insert zero_le_square [of z], simp del:zero_le_square) |
1763 done |
1763 done |
1764 |
1764 |
1765 lemma Infinitesimal_sum_square_cancel2 [simp]: |
1765 lemma Infinitesimal_sum_square_cancel2 [simp]: |
1766 "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1766 "(y::hypreal)*y + x*x + z*z \<in> Infinitesimal ==> x*x \<in> Infinitesimal" |
1767 apply (rule Infinitesimal_sum_square_cancel) |
1767 apply (rule Infinitesimal_sum_square_cancel) |