# HG changeset patch
# User nipkow
# Date 1316583068 -7200
# Node ID 76abd26e2e2d1f729983f282c4d443f6f76eff50
# Parent  3c888c58e10b19ee55272af94a17c5246e59939c
renamed inv -> filter

diff -r 3c888c58e10b -r 76abd26e2e2d src/HOL/IMP/AbsInt1.thy
--- a/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 07:04:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy	Wed Sep 21 07:31:08 2011 +0200
@@ -30,11 +30,11 @@
 
 locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
   for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
-fixes inv_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
-and inv_less' :: "'a \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> 'a * 'a"
-assumes inv_plus': "inv_plus' a1 a2 a = (a1',a2') \<Longrightarrow>
+fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
+assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
   n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
-and inv_less': "inv_less' a1 a2 (n1<n2) = (a1',a2') \<Longrightarrow>
+and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
   n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
 
 datatype 'a up = bot | Up 'a
@@ -117,7 +117,7 @@
   let a' = lookup S x \<sqinter> a in
   if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
 "afilter (Plus e1 e2) a S =
- (let (a1,a2) = inv_plus' (aval' e1 S) (aval' e2 S) a
+ (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
   in afilter e1 a1 (afilter e2 a2 S))"
 
 text{* The test for @{const Bot} in the @{const V}-case is important: @{const
@@ -137,7 +137,7 @@
   (if res then bfilter b1 True (bfilter b2 True S)
    else bfilter b1 False S \<squnion> bfilter b2 False S)" |
 "bfilter (Less e1 e2) res S =
-  (let (res1,res2) = inv_less' (aval' e1 S) (aval' e2 S) res
+  (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
    in afilter e1 res1 (afilter e2 res2 S))"
 
 lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
@@ -153,7 +153,7 @@
        (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
 next
   case (Plus e1 e2) thus ?case
-    using inv_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
+    using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
     by (auto split: prod.split)
 qed
 
@@ -167,7 +167,7 @@
 next
   case (Less e1 e2) thus ?case
     by (auto split: prod.split)
-       (metis afilter_sound inv_less' aval'_sound Less)
+       (metis afilter_sound filter_less' aval'_sound Less)
 qed
 
 fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
diff -r 3c888c58e10b -r 76abd26e2e2d src/HOL/IMP/AbsInt1_ivl.thy
--- 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
diff -r 3c888c58e10b -r 76abd26e2e2d src/HOL/IMP/AbsInt2.thy
--- a/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 07:04:04 2011 +0200
+++ b/src/HOL/IMP/AbsInt2.thy	Wed Sep 21 07:31:08 2011 +0200
@@ -142,7 +142,7 @@
 
 end
 
-instantiation astate :: (WN)WN
+instantiation astate :: (WN) WN
 begin
 
 definition "widen_astate F1 F2 =
@@ -165,7 +165,7 @@
 
 end
 
-instantiation up :: (WN)WN
+instantiation up :: (WN) WN
 begin
 
 fun widen_up where
@@ -193,7 +193,7 @@
 end
 
 interpretation
-  Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter' 3 2)"
+  Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
 defines afilter_ivl' is afilter
 and bfilter_ivl' is bfilter
 and AI_ivl' is AI