equal
deleted
inserted
replaced
762 assume "finite A" then show ?thesis |
762 assume "finite A" then show ?thesis |
763 by induct (auto simp: one_ereal_def) |
763 by induct (auto simp: one_ereal_def) |
764 qed (simp add: one_ereal_def) |
764 qed (simp add: one_ereal_def) |
765 |
765 |
766 subsubsection {* Power *} |
766 subsubsection {* Power *} |
767 |
|
768 instantiation ereal :: power |
|
769 begin |
|
770 primrec power_ereal where |
|
771 "power_ereal x 0 = 1" | |
|
772 "power_ereal x (Suc n) = x * x ^ n" |
|
773 instance .. |
|
774 end |
|
775 |
767 |
776 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)" |
768 lemma ereal_power[simp]: "(ereal x) ^ n = ereal (x^n)" |
777 by (induct n) (auto simp: one_ereal_def) |
769 by (induct n) (auto simp: one_ereal_def) |
778 |
770 |
779 lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)" |
771 lemma ereal_power_PInf[simp]: "(\<infinity>::ereal) ^ n = (if n = 0 then 1 else \<infinity>)" |