summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Real/RealDef.thy

changeset 15013 | 34264f5e4691 |

parent 15003 | 6145dd7538d7 |

child 15077 | 89840837108e |

--- a/src/HOL/Real/RealDef.thy Wed Jun 30 14:04:58 2004 +0200 +++ b/src/HOL/Real/RealDef.thy Thu Jul 01 12:29:53 2004 +0200 @@ -732,25 +732,12 @@ instance real :: number .. -primrec (*the type constraint is essential!*) - number_of_Pls: "number_of bin.Pls = 0" - number_of_Min: "number_of bin.Min = - (1::real)" - number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) + - (number_of w) + (number_of w)" - -declare number_of_Pls [simp del] - number_of_Min [simp del] - number_of_BIT [simp del] +defs (overloaded) + real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)" + --{*the type constraint is essential!*} instance real :: number_ring -proof - show "Numeral0 = (0::real)" by (rule number_of_Pls) - show "-1 = - (1::real)" by (rule number_of_Min) - fix w :: bin and x :: bool - show "(number_of (w BIT x) :: real) = - (if x then 1 else 0) + number_of w + number_of w" - by (rule number_of_BIT) -qed +by (intro_classes, simp add: real_number_of_def) text{*Collapse applications of @{term real} to @{term number_of}*}