src/HOL/Real/RealDef.thy
changeset 15013 34264f5e4691
parent 15003 6145dd7538d7
child 15077 89840837108e
equal deleted inserted replaced
15012:28fa57b57209 15013:34264f5e4691
   730 
   730 
   731 subsection{*Numerals and Arithmetic*}
   731 subsection{*Numerals and Arithmetic*}
   732 
   732 
   733 instance real :: number ..
   733 instance real :: number ..
   734 
   734 
   735 primrec (*the type constraint is essential!*)
   735 defs (overloaded)
   736   number_of_Pls: "number_of bin.Pls = 0"
   736   real_number_of_def: "(number_of w :: real) == of_int (Rep_Bin w)"
   737   number_of_Min: "number_of bin.Min = - (1::real)"
   737     --{*the type constraint is essential!*}
   738   number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
       
   739 	                               (number_of w) + (number_of w)"
       
   740 
       
   741 declare number_of_Pls [simp del]
       
   742         number_of_Min [simp del]
       
   743         number_of_BIT [simp del]
       
   744 
   738 
   745 instance real :: number_ring
   739 instance real :: number_ring
   746 proof
   740 by (intro_classes, simp add: real_number_of_def) 
   747   show "Numeral0 = (0::real)" by (rule number_of_Pls)
       
   748   show "-1 = - (1::real)" by (rule number_of_Min)
       
   749   fix w :: bin and x :: bool
       
   750   show "(number_of (w BIT x) :: real) =
       
   751         (if x then 1 else 0) + number_of w + number_of w"
       
   752     by (rule number_of_BIT)
       
   753 qed
       
   754 
   741 
   755 
   742 
   756 text{*Collapse applications of @{term real} to @{term number_of}*}
   743 text{*Collapse applications of @{term real} to @{term number_of}*}
   757 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   744 lemma real_number_of [simp]: "real (number_of v :: int) = number_of v"
   758 by (simp add:  real_of_int_def of_int_number_of_eq)
   745 by (simp add:  real_of_int_def of_int_number_of_eq)