--- a/src/HOL/IMP/AbsInt0.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/AbsInt0.thy Thu Sep 15 09:44:08 2011 +0200
@@ -9,10 +9,13 @@
text{* Abstract interpretation over type @{text astate} instead of
functions. *}
-locale Abs_Int = Val_abs
+locale Abs_Int = Val_abs +
+fixes pfp_above :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
begin
-fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" ("aval\<^isup>#") where
+fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
"aval' (N n) _ = num' n" |
"aval' (V x) S = lookup S x" |
"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
@@ -32,7 +35,7 @@
"AI (x ::= a) S = update S x (aval' a S)" |
"AI (c1;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
+"AI (WHILE b DO c) S = pfp_above (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
@@ -47,8 +50,7 @@
by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
next
case (While b c)
- let ?P = "iter_above (AI c) 3 S0"
- have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by(simp_all add: iter_above_pfp)
+ let ?P = "pfp_above (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
@@ -56,7 +58,7 @@
case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
qed
}
- with astate_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
+ with astate_in_rep_le[OF `s <: S0` above]
show ?case by (metis While(2) AI.simps(5))
qed
--- a/src/HOL/IMP/AbsInt0_const.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_const.thy Thu Sep 15 09:44:08 2011 +0200
@@ -61,50 +61,51 @@
by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
qed
-interpretation Abs_Int rep_cval Const plus_cval
+interpretation Abs_Int rep_cval Const plus_cval "(iter_above 3)"
defines AI_const is AI
and aval'_const is aval'
-..
+proof qed (auto simp: iter_above_pfp)
text{* Straight line code: *}
definition "test1_const =
''y'' ::= N 7;
''z'' ::= Plus (V ''y'') (N 2);
''y'' ::= Plus (V ''x'') (N 0)"
-value [code] "list (AI_const test1_const Top)"
text{* Conditional: *}
definition "test2_const =
IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
-value "list (AI_const test2_const Top)"
text{* Conditional, test is ignored: *}
definition "test3_const =
''x'' ::= N 42;
IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
-value "list (AI_const test3_const Top)"
text{* While: *}
definition "test4_const =
''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
-value [code] "list (AI_const test4_const Top)"
text{* While, test is ignored: *}
definition "test5_const =
''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
-value [code] "list (AI_const test5_const Top)"
text{* Iteration is needed: *}
definition "test6_const =
''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
-value [code] "list (AI_const test6_const Top)"
text{* More iteration would be needed: *}
definition "test7_const =
''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
- WHILE B True DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+ WHILE Less (V ''x'') (N 1)
+ DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
+
+value [code] "list (AI_const test1_const Top)"
+value [code] "list (AI_const test2_const Top)"
+value [code] "list (AI_const test3_const Top)"
+value [code] "list (AI_const test4_const Top)"
+value [code] "list (AI_const test5_const Top)"
+value [code] "list (AI_const test6_const Top)"
value [code] "list (AI_const test7_const Top)"
-
end
--- a/src/HOL/IMP/AbsInt0_fun.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/AbsInt0_fun.thy Thu Sep 15 09:44:08 2011 +0200
@@ -31,44 +31,44 @@
lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
by (metis join_ge1 join_ge2 join_least le_trans)
-fun iter where
-"iter f 0 _ = Top" |
-"iter f (Suc n) x = (if f x \<sqsubseteq> x then x else iter f n (f x))"
+fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter 0 f _ = Top" |
+"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
-lemma iter_pfp: "f(iter f n x) \<sqsubseteq> iter f n x"
+lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
apply (induct n arbitrary: x)
apply (simp)
apply (simp)
done
-definition "iter_above f n x0 = iter (\<lambda>x. x0 \<squnion> f x) n x0"
+definition iter_above :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_above n f x0 = iter n (\<lambda>x. x0 \<squnion> f x) x0"
lemma iter_above_pfp:
-shows "f(iter_above f n x0) \<sqsubseteq> iter_above f n x0" and "x0 \<sqsubseteq> iter_above f n x0"
+shows "f(iter_above n f x0) \<sqsubseteq> iter_above n f x0" and "x0 \<sqsubseteq> iter_above n f x0"
using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"]
by(auto simp add: iter_above_def)
text{* So much for soundness. But how good an approximation of the post-fixed
point does @{const iter_above} yield? *}
-lemma iter_funpow: "iter f n x \<noteq> Top \<Longrightarrow> EX k. iter f n x = (f^^k) x"
+lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
apply(induct n arbitrary: x)
apply simp
apply (auto)
-apply(rule_tac x=0 in exI)
-apply simp
+ apply(metis funpow.simps(1) id_def)
by (metis funpow.simps(2) funpow_swap1 o_apply)
text{* For monotone @{text f}, @{term "iter_above f n x0"} yields the least
post-fixed point above @{text x0}, unless it yields @{text Top}. *}
lemma iter_least_pfp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
-and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above f n x0 \<sqsubseteq> p"
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
+and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter_above n f x0 \<sqsubseteq> p"
proof-
let ?F = "\<lambda>x. x0 \<squnion> f x"
- obtain k where "iter_above f n x0 = (?F^^k) x0"
- using iter_funpow `iter_above f n x0 \<noteq> Top`
+ obtain k where "iter_above n f x0 = (?F^^k) x0"
+ using iter_funpow `iter_above n f x0 \<noteq> Top`
by(fastforce simp add: iter_above_def)
moreover
{ fix n have "(?F^^n) x0 \<sqsubseteq> p"
@@ -89,10 +89,10 @@
by (metis assms join_ge2 le_trans)
lemma iter_above_almost_fp:
-assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above f n x0 \<noteq> Top"
-shows "iter_above f n x0 \<sqsubseteq> x0 \<squnion> f(iter_above f n x0)"
+assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter_above n f x0 \<noteq> Top"
+shows "iter_above n f x0 \<sqsubseteq> x0 \<squnion> f(iter_above n f x0)"
proof-
- let ?p = "iter_above f n x0"
+ let ?p = "iter_above n f x0"
obtain k where 1: "?p = ((\<lambda>x. x0 \<squnion> f x)^^k) x0"
using iter_funpow `?p \<noteq> Top`
by(fastforce simp add: iter_above_def)
@@ -117,8 +117,8 @@
locale Val_abs = Rep rep
for rep :: "'a::SL_top \<Rightarrow> val set" +
-fixes num' :: "val \<Rightarrow> 'a" ("num\<^isup>#")
-and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" ("plus\<^isup>#")
+fixes num' :: "val \<Rightarrow> 'a"
+and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
assumes rep_num': "rep(num' n) = {n}"
and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
@@ -143,13 +143,18 @@
subsection "Abstract Interpretation Abstractly"
-text{* Abstract interpretation over abstract values.
-Abstract states are simply functions. *}
+text{* Abstract interpretation over abstract values. Abstract states are
+simply functions. The post-fixed point finder is parameterized over. *}
+
+type_synonym 'a st = "name \<Rightarrow> 'a"
-locale Abs_Int_Fun = Val_abs
+locale Abs_Int_Fun = Val_abs +
+fixes pfp_above :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
begin
-fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" ("aval\<^isup>#") where
+fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
"aval' (N n) _ = num' n" |
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
@@ -168,7 +173,7 @@
"AI (x ::= a) S = S(x := aval' a S)" |
"AI (c1;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
-"AI (WHILE b DO c) S = iter_above (AI c) 3 S"
+"AI (WHILE b DO c) S = pfp_above (AI c) S"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
proof(induct c arbitrary: s t S0)
@@ -181,8 +186,7 @@
case If thus ?case by(auto simp: in_rep_join)
next
case (While b c)
- let ?P = "iter_above (AI c) 3 S0"
- have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P" by (simp_all add: iter_above_pfp)
+ let ?P = "pfp_above (AI c) S0"
{ fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
proof(induct "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by simp
@@ -190,7 +194,7 @@
case WhileTrue thus ?case by(metis While.hyps pfp fun_in_rep_le)
qed
}
- with fun_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
+ with fun_in_rep_le[OF `s <: S0` above]
show ?case by (metis While(2) AI.simps(5))
qed
--- a/src/HOL/IMP/AbsInt1.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/AbsInt1.thy Thu Sep 15 09:44:08 2011 +0200
@@ -64,8 +64,6 @@
definition "Top = Up Top"
-(* register <= as transitive - see orderings *)
-
instance proof
case goal1 show ?case by(cases x, simp_all)
next
@@ -84,7 +82,10 @@
end
-locale Abs_Int1 = Val_abs1
+locale Abs_Int1 = Val_abs1 +
+fixes pfp_above :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
+assumes pfp: "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0"
+assumes above: "x0 \<sqsubseteq> pfp_above f x0"
begin
(* FIXME avoid duplicating this defn *)
@@ -114,11 +115,21 @@
"afilter (N n) a S = (if n <: a then S else bot)" |
"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
let a' = lookup S x \<sqinter> a in
- if a'\<sqsubseteq> Bot then bot else Up(update S x a'))" |
+ 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
in afilter e1 a1 (afilter e2 a2 S))"
+text{* The test for @{const Bot} in the @{const V}-case is important: @{const
+Bot} indicates that a variable has no possible values, i.e.\ that the current
+program point is unreachable. But then the abstract state should collaps to
+@{const bot}. Put differently, we maintain the invariant that in an abstract
+state all variables are mapped to non-@{const Bot} values. Otherwise the
+(pointwise) join of two abstract states, one of which contains @{const Bot}
+values, may produce too large a result, thus making the analysis less
+precise. *}
+
+
fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
"bfilter (B bv) res S = (if bv=res then S else bot)" |
"bfilter (Not b) res S = bfilter b (\<not> res) S" |
@@ -167,7 +178,7 @@
"AI (IF b THEN c1 ELSE c2) S =
AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
"AI (WHILE b DO c) S =
- bfilter b False (iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S)"
+ bfilter b False (pfp_above (\<lambda>S. AI c (bfilter b True S)) S)"
lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
proof(induct c arbitrary: s t S)
@@ -181,9 +192,7 @@
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next
case (While b c)
- let ?P = "iter_above (\<lambda>S. AI c (bfilter b True S)) 3 S"
- have pfp: "AI c (bfilter b True ?P) \<sqsubseteq> ?P" and "S \<sqsubseteq> ?P"
- by (rule iter_above_pfp(1), rule iter_above_pfp(2))
+ let ?P = "pfp_above (\<lambda>S. AI c (bfilter b True S)) S"
{ fix s t
have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
t <:: bfilter b False ?P"
@@ -196,7 +205,7 @@
rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
qed
}
- with in_rep_up_trans[OF `s <:: S` `S \<sqsubseteq> ?P`] While(2,3) AI.simps(5)
+ with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
show ?case by simp
qed
--- a/src/HOL/IMP/AbsInt1_ivl.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/AbsInt1_ivl.thy Thu Sep 15 09:44:08 2011 +0200
@@ -8,10 +8,19 @@
datatype ivl = I "int option" "int option"
+text{* We assume an important invariant: arithmetic operations are never
+applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
+i"}. This avoids special cases. Why can we assume this? Because an empty
+interval of values for a variable means that the current program point is
+unreachable. But this should actually translate into the bottom state, not a
+state where some variables have empty intervals. *}
+
definition "rep_ivl i =
(case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
| I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
+definition "num_ivl n = I (Some n) (Some n)"
+
instantiation option :: (plus)plus
begin
@@ -36,16 +45,16 @@
lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
by(auto simp add: rep_ivl_def split: ivl.split option.split)
-definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty
- else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
+definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
instantiation ivl :: SL_top
begin
definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
"le_option pos x y =
- (case x of (Some i) \<Rightarrow> (case y of (Some j) \<Rightarrow> (i<=j) | None \<Rightarrow> pos)
- | None \<Rightarrow> (case y of Some j \<Rightarrow> (~pos) | None \<Rightarrow> True))"
+ (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
+ | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
fun le_aux where
"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
@@ -95,8 +104,9 @@
instantiation ivl :: L_top_bot
begin
-definition "i1 \<sqinter> i2 = (if is_empty i1 | is_empty i2 then empty
- else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (max_option False l1 l2) (min_option True h1 h2))"
+definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (max_option False l1 l2) (min_option True h1 h2))"
definition "Bot = empty"
@@ -127,24 +137,22 @@
end
-definition "minus_ivl i1 i2 =
- (if is_empty i1 | is_empty i2 then empty
- else case (i1,i2) of
- (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
+definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
+ case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
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 i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
+definition "inv_plus_ivl i1 i2 i = ((*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 =
(if res
- then (I l1 (min_option True h1 (h2 - Some 1)), I (max_option False (l1 + Some 1) l2) h2)
+ 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)))"
interpretation Rep rep_ivl
@@ -153,9 +161,9 @@
by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
qed
-interpretation Val_abs rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl
+interpretation Val_abs rep_ivl num_ivl plus_ivl
proof
- case goal1 thus ?case by(simp add: rep_ivl_def)
+ case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
next
case goal2 thus ?case
by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
@@ -169,7 +177,8 @@
case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
qed
-interpretation Val_abs1 rep_ivl "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+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)
@@ -180,12 +189,13 @@
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 "\<lambda>n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
+interpretation
+ Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 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_above_pfp)
fun list_up where
@@ -228,4 +238,16 @@
WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
value [code] "list_up(AI_ivl test2_ivl Top)"
+definition "test3_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
+ WHILE Less (V ''x'') (N 11)
+ DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
+value [code] "list_up(AI_ivl test3_ivl Top)"
+
+definition "test4_ivl =
+ ''x'' ::= N 0; ''y'' ::= N 0;
+ WHILE Less (V ''x'') (N 1001)
+ DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
+value [code] "list_up(AI_ivl test4_ivl Top)"
+
end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IMP/AbsInt2.thy Thu Sep 15 09:44:08 2011 +0200
@@ -0,0 +1,139 @@
+(* Author: Tobias Nipkow *)
+
+theory AbsInt2
+imports AbsInt1_ivl
+begin
+
+subsection "Widening and Narrowing"
+
+text{* The assumptions about winden and narrow are merely sanity checks. They
+are only needed in case we want to prove termination of the fixedpoint
+iteration, which we do not --- we limit the number of iterations as before. *}
+
+class WN = SL_top +
+fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
+assumes widen: "y \<sqsubseteq> x \<nabla> y"
+fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
+assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
+assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
+begin
+
+fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_up f 0 x = Top" |
+"iter_up f (Suc n) x =
+ (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
+
+lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
+apply (induct n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_down f 0 x = x" |
+"iter_down f (Suc n) x =
+ (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
+
+lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
+apply (induct n arbitrary: x)
+ apply (simp)
+apply (simp add: Let_def)
+done
+
+definition iter_above :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+"iter_above m n f x =
+ (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
+
+lemma iter_above_pfp:
+shows "f(iter_above m n f x0) \<sqsubseteq> iter_above m n f x0"
+and "x0 \<sqsubseteq> iter_above m n f x0"
+using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
+by(auto simp add: iter_above_def Let_def)
+
+end
+
+
+instantiation ivl :: WN
+begin
+
+definition "widen_ivl ivl1 ivl2 =
+ ((*if is_empty ivl1 then ivl2 else
+ if is_empty ivl2 then ivl1 else*)
+ case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
+ (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
+
+definition "narrow_ivl ivl1 ivl2 =
+ ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
+ case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
+ I (if l1 = None then l2 else l1)
+ (if h1 = None then h2 else h1))"
+
+instance
+proof qed
+ (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
+
+end
+
+instantiation astate :: (WN)WN
+begin
+
+definition "widen_astate F1 F2 =
+ FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+definition "narrow_astate F1 F2 =
+ FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
+
+instance
+proof
+ case goal1 thus ?case
+ by(simp add: widen_astate_def le_astate_def lookup_def widen)
+next
+ case goal2 thus ?case
+ by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
+next
+ case goal3 thus ?case
+ by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
+qed
+
+end
+
+instantiation up :: (WN)WN
+begin
+
+fun widen_up where
+"widen_up bot x = x" |
+"widen_up x bot = x" |
+"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
+
+fun narrow_up where
+"narrow_up bot x = bot" |
+"narrow_up x bot = bot" |
+"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
+
+instance
+proof
+ case goal1 show ?case
+ by(induct x y rule: widen_up.induct) (simp_all add: widen)
+next
+ case goal2 thus ?case
+ by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
+next
+ case goal3 thus ?case
+ by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
+qed
+
+end
+
+interpretation
+ Abs_Int1 rep_ivl num_ivl plus_ivl inv_plus_ivl inv_less_ivl "(iter_above 3 2)"
+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_above_pfp)
+
+value [code] "list_up(AI_ivl' test3_ivl Top)"
+value [code] "list_up(AI_ivl' test4_ivl Top)"
+
+end
--- a/src/HOL/IMP/Astate.thy Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/Astate.thy Thu Sep 15 09:44:08 2011 +0200
@@ -2,6 +2,8 @@
theory Astate
imports AbsInt0_fun
+ "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
+ (* Library import merely to allow string lists to be sorted for output *)
begin
subsection "Abstract State with Computable Ordering"
@@ -13,12 +15,14 @@
fun "fun" where "fun (FunDom f _) = f"
fun dom where "dom (FunDom _ A) = A"
-definition "list S = [(x,fun S x). x \<leftarrow> dom S]"
+definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
+
+definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
definition "update F x y =
- FunDom ((fun F)(x:=y)) (if x : set(dom F) then dom F else x # dom F)"
+ FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
by(rule ext)(auto simp: lookup_def update_def)
@@ -30,7 +34,7 @@
definition
"join_astate F G =
- FunDom (\<lambda>x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
+ FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
definition "Top = FunDom (\<lambda>x. Top) []"
--- a/src/HOL/IMP/ROOT.ML Wed Sep 14 06:49:24 2011 +0200
+++ b/src/HOL/IMP/ROOT.ML Thu Sep 15 09:44:08 2011 +0200
@@ -1,4 +1,7 @@
-no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs"];
+no_document use_thys
+ ["~~/src/HOL/ex/Interpretation_with_Defs",
+ "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
+ ];
use_thys
["BExp",
@@ -12,7 +15,7 @@
"Def_Ass_Sound_Big",
"Def_Ass_Sound_Small",
"Live",
- "AbsInt1_ivl",
+ "AbsInt2",
"Hoare_Examples",
"VC",
"HoareT",