Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/AbsInt1_ivl.thy
changeset 45023 76abd26e2e2d
parent 45020 21334181f820 
--- a/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 21 07:04:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy	Wed Sep 21 07:31:08 2011 +0200
@@ -145,11 +145,11 @@
 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)),
@@ -179,10 +179,10 @@
 qed
 
 interpretation
-  Val_abs1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl
+  Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
-    by(auto simp add: inv_plus_ivl_def)
+    by(auto simp add: filter_plus_ivl_def)
       (metis rep_minus_ivl add_diff_cancel add_commute)+
 next
   case goal2 thus ?case
@@ -191,7 +191,7 @@
 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
isabelle