src/HOL/IMP/Abs_Int2_ivl.thy
changeset 51870 a331fbefcdb1
parent 51826 054a40461449
child 51871 f16bd7d2359c
equal deleted inserted replaced
51869:d58cd7673b04 51870:a331fbefcdb1
   183    if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
   183    if [l2\<dots>h2] = \<bottom> then [l1\<dots>h1] else [min l1 l2\<dots>max h1 h2])"
   184 unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty)
   184 unfolding bot_ivl_def by transfer (simp add: sup_rep_def eq_ivl_empty)
   185 
   185 
   186 lemma inf_ivl_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
   186 lemma inf_ivl_nice: "[l1\<dots>h1] \<sqinter> [l2\<dots>h2] = [max l1 l2\<dots>min h1 h2]"
   187 by transfer (simp add: inf_rep_def)
   187 by transfer (simp add: inf_rep_def)
       
   188 
       
   189 lemma top_ivl_nice: "\<top> = [-\<infinity>\<dots>\<infinity>]"
       
   190 by (simp add: top_ivl_def)
   188 
   191 
   189 
   192 
   190 instantiation ivl :: plus
   193 instantiation ivl :: plus
   191 begin
   194 begin
   192 
   195