src/HOL/IMP/Abs_Int2.thy
changeset 50995 3371f5ee4ace
parent 50986 c54ea7f5418f
child 51036 e7b54119c436
     1.1 --- a/src/HOL/IMP/Abs_Int2.thy	Sun Jan 20 15:34:27 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Fri Jan 25 16:45:09 2013 +0100
     1.3 @@ -55,11 +55,11 @@
     1.4  fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
     1.5  and filter_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     1.6  and filter_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
     1.7 -assumes test_num': "test_num' n a = (n : \<gamma> a)"
     1.8 +assumes test_num': "test_num' i a = (i : \<gamma> a)"
     1.9  and filter_plus': "filter_plus' a a1 a2 = (b1,b2) \<Longrightarrow>
    1.10 -  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1+n2 : \<gamma> a \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    1.11 -and filter_less': "filter_less' (n1<n2) a1 a2 = (b1,b2) \<Longrightarrow>
    1.12 -  n1 : \<gamma> a1 \<Longrightarrow> n2 : \<gamma> a2 \<Longrightarrow> n1 : \<gamma> b1 \<and> n2 : \<gamma> b2"
    1.13 +  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    1.14 +and filter_less': "filter_less' (i1<i2) a1 a2 = (b1,b2) \<Longrightarrow>
    1.15 +  i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> b1 \<and> i2 : \<gamma> b2"
    1.16  
    1.17  
    1.18  locale Abs_Int1 =
    1.19 @@ -80,13 +80,13 @@
    1.20  subsubsection "Backward analysis"
    1.21  
    1.22  fun afilter :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    1.23 -"afilter (N n) a S = (if test_num' n a then S else None)" |
    1.24 +"afilter (N i) a S = (if test_num' i a then S else None)" |
    1.25  "afilter (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    1.26    let a' = fun S x \<sqinter> a in
    1.27    if a' \<sqsubseteq> \<bottom> then None else Some(update S x a'))" |
    1.28  "afilter (Plus e1 e2) a S =
    1.29 - (let (a1,a2) = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    1.30 -  in afilter e1 a1 (afilter e2 a2 S))"
    1.31 + (let (a\<^isub>1',a\<^isub>2') = filter_plus' a (aval'' e1 S) (aval'' e2 S)
    1.32 +  in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    1.33  
    1.34  text{* The test for @{const bot} in the @{const V}-case is important: @{const
    1.35  bot} indicates that a variable has no possible values, i.e.\ that the current
    1.36 @@ -105,8 +105,8 @@
    1.37    (if res then bfilter b1 True (bfilter b2 True S)
    1.38     else bfilter b1 False S \<squnion> bfilter b2 False S)" |
    1.39  "bfilter (Less e1 e2) res S =
    1.40 -  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    1.41 -   in afilter e1 res1 (afilter e2 res2 S))"
    1.42 +  (let (a\<^isub>1',a\<^isub>2') = filter_less' res (aval'' e1 S) (aval'' e2 S)
    1.43 +   in afilter e1 a\<^isub>1' (afilter e2 a\<^isub>2' S))"
    1.44  
    1.45  lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
    1.46  by(induction e arbitrary: a S)