src/HOL/Library/Extended.thy
changeset 51358 0c376ef98559
parent 51357 ac4c1cf1b001
child 53427 415354b68f0c
equal deleted inserted replaced
51357:ac4c1cf1b001 51358:0c376ef98559
   180   apply (induct w rule: num_induct)
   180   apply (induct w rule: num_induct)
   181   apply (simp only: numeral_One one_extended_def)
   181   apply (simp only: numeral_One one_extended_def)
   182   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   182   apply (simp only: numeral_inc one_extended_def plus_extended.simps(1)[symmetric])
   183   done
   183   done
   184 
   184 
       
   185 lemma Fin_neg_numeral: "Fin(neg_numeral w) = - numeral w"
       
   186 by (simp only: Fin_numeral minus_numeral[symmetric] uminus_extended.simps[symmetric])
       
   187 
   185 
   188 
   186 instantiation extended :: (lattice)bounded_lattice
   189 instantiation extended :: (lattice)bounded_lattice
   187 begin
   190 begin
   188 
   191 
   189 definition "bot = Minf"
   192 definition "bot = Minf"