equal
deleted
inserted
replaced
508 |
508 |
509 lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)" |
509 lemma real_of_num: "((0::real) = 0) & (!n. real (Suc n) = real n + 1)" |
510 by (simp add: real_of_nat_Suc) |
510 by (simp add: real_of_nat_Suc) |
511 |
511 |
512 lemma abs: "abs (x::real) = (if 0 <= x then x else -x)" |
512 lemma abs: "abs (x::real) = (if 0 <= x then x else -x)" |
513 by (simp add: real_abs_def) |
513 by (simp add: abs_if) |
514 |
514 |
515 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" |
515 lemma pow: "(!x::real. x ^ 0 = 1) & (!x::real. ALL n. x ^ (Suc n) = x * x ^ n)" |
516 by simp; |
516 by simp |
517 |
517 |
518 constdefs |
518 constdefs |
519 real_gt :: "real => real => bool" |
519 real_gt :: "real => real => bool" |
520 "real_gt == %x y. y < x" |
520 "real_gt == %x y. y < x" |
521 |
521 |