src/HOL/IMP/AbsInt1_ivl.thy

 lemma rep_minus_ivl:
   "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
 by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
 
 
-definition "inv_plus_ivl i1 i2 i = ((*if is_empty i then empty else*)
+definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
   i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
 
-fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
-"inv_less_ivl (I l1 h1) (I l2 h2) res =
+fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
+"filter_less_ivl res (I l1 h1) (I l2 h2) =
   ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
    if res
    then (I l1 (min_option True h1 (h2 - Some 1)),
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"

 next
   case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
 qed
 
 interpretation
-  Val_abs1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl
-proof
-  case goal1 thus ?case
-    by(auto simp add: inv_plus_ivl_def)
+  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
+proof
+  case goal1 thus ?case
+    by(auto simp add: filter_plus_ivl_def)
       (metis rep_minus_ivl add_diff_cancel add_commute)+
 next
   case goal2 thus ?case
     by(cases a1, cases a2,
       auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3)"
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
 defines afilter_ivl is afilter
 and bfilter_ivl is bfilter
 and AI_ivl is AI
 and aval_ivl is aval'
 proof qed (auto simp: iter'_pfp_above)