1.1 --- a/src/HOL/IMP/AbsInt0.thy Mon Sep 26 21:13:26 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,67 +0,0 @@
1.4 -(* Author: Tobias Nipkow *)
1.5 -
1.6 -theory AbsInt0
1.7 -imports Astate
1.8 -begin
1.9 -
1.10 -subsection "Computable Abstract Interpretation"
1.11 -
1.12 -text{* Abstract interpretation over type @{text astate} instead of
1.13 -functions. *}
1.14 -
1.15 -locale Abs_Int = Val_abs +
1.16 -fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
1.17 -assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
1.18 -assumes above: "x0 \<sqsubseteq> pfp f x0"
1.19 -begin
1.20 -
1.21 -fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
1.22 -"aval' (N n) _ = num' n" |
1.23 -"aval' (V x) S = lookup S x" |
1.24 -"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
1.25 -
1.26 -abbreviation astate_in_rep (infix "<:" 50) where
1.27 -"s <: S == ALL x. s x <: lookup S x"
1.28 -
1.29 -lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
1.30 -by (metis in_mono le_astate_def le_rep lookup_def top)
1.31 -
1.32 -lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
1.33 -by (induct a) (auto simp: rep_num' rep_plus')
1.34 -
1.35 -
1.36 -fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
1.37 -"AI SKIP S = S" |
1.38 -"AI (x ::= a) S = update S x (aval' a S)" |
1.39 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
1.40 -"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
1.41 -"AI (WHILE b DO c) S = pfp (AI c) S"
1.42 -
1.43 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
1.44 -proof(induction c arbitrary: s t S0)
1.45 - case SKIP thus ?case by fastforce
1.46 -next
1.47 - case Assign thus ?case
1.48 - by (auto simp: lookup_update aval'_sound)
1.49 -next
1.50 - case Semi thus ?case by auto
1.51 -next
1.52 - case If thus ?case
1.53 - by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
1.54 -next
1.55 - case (While b c)
1.56 - let ?P = "pfp (AI c) S0"
1.57 - { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
1.58 - proof(induction "WHILE b DO c" s t rule: big_step_induct)
1.59 - case WhileFalse thus ?case by simp
1.60 - next
1.61 - case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
1.62 - qed
1.63 - }
1.64 - with astate_in_rep_le[OF `s <: S0` above]
1.65 - show ?case by (metis While(2) AI.simps(5))
1.66 -qed
1.67 -
1.68 -end
1.69 -
1.70 -end
2.1 --- a/src/HOL/IMP/AbsInt0_const.thy Mon Sep 26 21:13:26 2011 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,111 +0,0 @@
2.4 -(* Author: Tobias Nipkow *)
2.5 -
2.6 -theory AbsInt0_const
2.7 -imports AbsInt0
2.8 -begin
2.9 -
2.10 -subsection "Constant Propagation"
2.11 -
2.12 -datatype cval = Const val | Any
2.13 -
2.14 -fun rep_cval where
2.15 -"rep_cval (Const n) = {n}" |
2.16 -"rep_cval (Any) = UNIV"
2.17 -
2.18 -fun plus_cval where
2.19 -"plus_cval (Const m) (Const n) = Const(m+n)" |
2.20 -"plus_cval _ _ = Any"
2.21 -
2.22 -instantiation cval :: SL_top
2.23 -begin
2.24 -
2.25 -fun le_cval where
2.26 -"_ \<sqsubseteq> Any = True" |
2.27 -"Const n \<sqsubseteq> Const m = (n=m)" |
2.28 -"Any \<sqsubseteq> Const _ = False"
2.29 -
2.30 -fun join_cval where
2.31 -"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
2.32 -"_ \<squnion> _ = Any"
2.33 -
2.34 -definition "Top = Any"
2.35 -
2.36 -instance
2.37 -proof
2.38 - case goal1 thus ?case by (cases x) simp_all
2.39 -next
2.40 - case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
2.41 -next
2.42 - case goal3 thus ?case by(cases x, cases y, simp_all)
2.43 -next
2.44 - case goal4 thus ?case by(cases y, cases x, simp_all)
2.45 -next
2.46 - case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
2.47 -next
2.48 - case goal6 thus ?case by(simp add: Top_cval_def)
2.49 -qed
2.50 -
2.51 -end
2.52 -
2.53 -interpretation Rep rep_cval
2.54 -proof
2.55 - case goal1 thus ?case
2.56 - by(cases a, cases b, simp, simp, cases b, simp, simp)
2.57 -qed
2.58 -
2.59 -interpretation Val_abs rep_cval Const plus_cval
2.60 -proof
2.61 - case goal1 show ?case by simp
2.62 -next
2.63 - case goal2 thus ?case
2.64 - by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
2.65 -qed
2.66 -
2.67 -interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
2.68 -defines AI_const is AI
2.69 -and aval'_const is aval'
2.70 -proof qed (auto simp: iter'_pfp_above)
2.71 -
2.72 -text{* Straight line code: *}
2.73 -definition "test1_const =
2.74 - ''y'' ::= N 7;
2.75 - ''z'' ::= Plus (V ''y'') (N 2);
2.76 - ''y'' ::= Plus (V ''x'') (N 0)"
2.77 -
2.78 -text{* Conditional: *}
2.79 -definition "test2_const =
2.80 - IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
2.81 -
2.82 -text{* Conditional, test is ignored: *}
2.83 -definition "test3_const =
2.84 - ''x'' ::= N 42;
2.85 - IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
2.86 -
2.87 -text{* While: *}
2.88 -definition "test4_const =
2.89 - ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
2.90 -
2.91 -text{* While, test is ignored: *}
2.92 -definition "test5_const =
2.93 - ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
2.94 -
2.95 -text{* Iteration is needed: *}
2.96 -definition "test6_const =
2.97 - ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
2.98 - WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
2.99 -
2.100 -text{* More iteration would be needed: *}
2.101 -definition "test7_const =
2.102 - ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
2.103 - WHILE Less (V ''x'') (N 1)
2.104 - DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
2.105 -
2.106 -value [code] "list (AI_const test1_const Top)"
2.107 -value [code] "list (AI_const test2_const Top)"
2.108 -value [code] "list (AI_const test3_const Top)"
2.109 -value [code] "list (AI_const test4_const Top)"
2.110 -value [code] "list (AI_const test5_const Top)"
2.111 -value [code] "list (AI_const test6_const Top)"
2.112 -value [code] "list (AI_const test7_const Top)"
2.113 -
2.114 -end
3.1 --- a/src/HOL/IMP/AbsInt0_fun.thy Mon Sep 26 21:13:26 2011 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,187 +0,0 @@
3.4 -(* Author: Tobias Nipkow *)
3.5 -
3.6 -header "Abstract Interpretation"
3.7 -
3.8 -theory AbsInt0_fun
3.9 -imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
3.10 -begin
3.11 -
3.12 -subsection "Orderings"
3.13 -
3.14 -class preord =
3.15 -fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
3.16 -assumes le_refl[simp]: "x \<sqsubseteq> x"
3.17 -and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
3.18 -
3.19 -text{* Note: no antisymmetry. Allows implementations where some abstract
3.20 -element is implemented by two different values @{prop "x \<noteq> y"}
3.21 -such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
3.22 -needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
3.23 -*}
3.24 -
3.25 -class SL_top = preord +
3.26 -fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
3.27 -fixes Top :: "'a"
3.28 -assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
3.29 -and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
3.30 -and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
3.31 -and top[simp]: "x \<sqsubseteq> Top"
3.32 -begin
3.33 -
3.34 -lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
3.35 -by (metis join_ge1 join_ge2 join_least le_trans)
3.36 -
3.37 -fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
3.38 -"iter 0 f _ = Top" |
3.39 -"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
3.40 -
3.41 -lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
3.42 -apply (induction n arbitrary: x)
3.43 - apply (simp)
3.44 -apply (simp)
3.45 -done
3.46 -
3.47 -abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
3.48 -"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
3.49 -
3.50 -lemma iter'_pfp_above:
3.51 - "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
3.52 -using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
3.53 -
3.54 -text{* So much for soundness. But how good an approximation of the post-fixed
3.55 -point does @{const iter} yield? *}
3.56 -
3.57 -lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
3.58 -apply(induction n arbitrary: x)
3.59 - apply simp
3.60 -apply (auto)
3.61 - apply(metis funpow.simps(1) id_def)
3.62 -by (metis funpow.simps(2) funpow_swap1 o_apply)
3.63 -
3.64 -text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
3.65 -post-fixed point above @{text x0}, unless it yields @{text Top}. *}
3.66 -
3.67 -lemma iter_least_pfp:
3.68 -assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
3.69 -and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
3.70 -proof-
3.71 - obtain k where "iter n f x0 = (f^^k) x0"
3.72 - using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
3.73 - moreover
3.74 - { fix n have "(f^^n) x0 \<sqsubseteq> p"
3.75 - proof(induction n)
3.76 - case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
3.77 - next
3.78 - case (Suc n) thus ?case
3.79 - by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
3.80 - qed
3.81 - } ultimately show ?thesis by simp
3.82 -qed
3.83 -
3.84 -end
3.85 -
3.86 -text{* The interface of abstract values: *}
3.87 -
3.88 -locale Rep =
3.89 -fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
3.90 -assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
3.91 -begin
3.92 -
3.93 -abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
3.94 -
3.95 -lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
3.96 -by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
3.97 -
3.98 -end
3.99 -
3.100 -locale Val_abs = Rep rep
3.101 - for rep :: "'a::SL_top \<Rightarrow> val set" +
3.102 -fixes num' :: "val \<Rightarrow> 'a"
3.103 -and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
3.104 -assumes rep_num': "rep(num' n) = {n}"
3.105 -and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
3.106 -
3.107 -
3.108 -instantiation "fun" :: (type, SL_top) SL_top
3.109 -begin
3.110 -
3.111 -definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
3.112 -definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
3.113 -definition "Top = (\<lambda>x. Top)"
3.114 -
3.115 -lemma join_apply[simp]:
3.116 - "(f \<squnion> g) x = f x \<squnion> g x"
3.117 -by (simp add: join_fun_def)
3.118 -
3.119 -instance
3.120 -proof
3.121 - case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
3.122 -qed (simp_all add: le_fun_def Top_fun_def)
3.123 -
3.124 -end
3.125 -
3.126 -subsection "Abstract Interpretation Abstractly"
3.127 -
3.128 -text{* Abstract interpretation over abstract values. Abstract states are
3.129 -simply functions. The post-fixed point finder is parameterized over. *}
3.130 -
3.131 -type_synonym 'a st = "name \<Rightarrow> 'a"
3.132 -
3.133 -locale Abs_Int_Fun = Val_abs +
3.134 -fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
3.135 -assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
3.136 -assumes above: "x \<sqsubseteq> pfp f x"
3.137 -begin
3.138 -
3.139 -fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
3.140 -"aval' (N n) _ = num' n" |
3.141 -"aval' (V x) S = S x" |
3.142 -"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
3.143 -
3.144 -abbreviation fun_in_rep (infix "<:" 50) where
3.145 -"f <: F == \<forall>x. f x <: F x"
3.146 -
3.147 -lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
3.148 -by (metis le_fun_def le_rep subsetD)
3.149 -
3.150 -lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
3.151 -by (induct a) (auto simp: rep_num' rep_plus')
3.152 -
3.153 -fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
3.154 -"AI SKIP S = S" |
3.155 -"AI (x ::= a) S = S(x := aval' a S)" |
3.156 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
3.157 -"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
3.158 -"AI (WHILE b DO c) S = pfp (AI c) S"
3.159 -
3.160 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
3.161 -proof(induction c arbitrary: s t S0)
3.162 - case SKIP thus ?case by fastforce
3.163 -next
3.164 - case Assign thus ?case by (auto simp: aval'_sound)
3.165 -next
3.166 - case Semi thus ?case by auto
3.167 -next
3.168 - case If thus ?case by(auto simp: in_rep_join)
3.169 -next
3.170 - case (While b c)
3.171 - let ?P = "pfp (AI c) S0"
3.172 - { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
3.173 - proof(induction "WHILE b DO c" s t rule: big_step_induct)
3.174 - case WhileFalse thus ?case by simp
3.175 - next
3.176 - case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
3.177 - qed
3.178 - }
3.179 - with fun_in_rep_le[OF `s <: S0` above]
3.180 - show ?case by (metis While(2) AI.simps(5))
3.181 -qed
3.182 -
3.183 -end
3.184 -
3.185 -
3.186 -text{* Problem: not executable because of the comparison of abstract states,
3.187 -i.e. functions, in the post-fixedpoint computation. Need to implement
3.188 -abstract states concretely. *}
3.189 -
3.190 -end
4.1 --- a/src/HOL/IMP/AbsInt1.thy Mon Sep 26 21:13:26 2011 +0200
4.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,214 +0,0 @@
4.4 -(* Author: Tobias Nipkow *)
4.5 -
4.6 -theory AbsInt1
4.7 -imports AbsInt0_const
4.8 -begin
4.9 -
4.10 -subsection "Backward Analysis of Expressions"
4.11 -
4.12 -class L_top_bot = SL_top +
4.13 -fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
4.14 -and Bot :: "'a"
4.15 -assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
4.16 -and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
4.17 -and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
4.18 -assumes bot[simp]: "Bot \<sqsubseteq> x"
4.19 -
4.20 -locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
4.21 -assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
4.22 -and rep_Bot: "rep Bot = {}"
4.23 -begin
4.24 -
4.25 -lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
4.26 -by (metis IntI inter_rep_subset_rep_meet set_mp)
4.27 -
4.28 -lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
4.29 -by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
4.30 -
4.31 -end
4.32 -
4.33 -
4.34 -locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
4.35 - for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
4.36 -fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
4.37 -and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
4.38 -assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
4.39 - n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
4.40 -and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
4.41 - n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
4.42 -
4.43 -datatype 'a up = bot | Up 'a
4.44 -
4.45 -instantiation up :: (SL_top)SL_top
4.46 -begin
4.47 -
4.48 -fun le_up where
4.49 -"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
4.50 -"bot \<sqsubseteq> y = True" |
4.51 -"Up _ \<sqsubseteq> bot = False"
4.52 -
4.53 -lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
4.54 -by (cases x) simp_all
4.55 -
4.56 -lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
4.57 -by (cases u) auto
4.58 -
4.59 -fun join_up where
4.60 -"Up x \<squnion> Up y = Up(x \<squnion> y)" |
4.61 -"bot \<squnion> y = y" |
4.62 -"x \<squnion> bot = x"
4.63 -
4.64 -lemma [simp]: "x \<squnion> bot = x"
4.65 -by (cases x) simp_all
4.66 -
4.67 -
4.68 -definition "Top = Up Top"
4.69 -
4.70 -instance proof
4.71 - case goal1 show ?case by(cases x, simp_all)
4.72 -next
4.73 - case goal2 thus ?case
4.74 - by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
4.75 -next
4.76 - case goal3 thus ?case by(cases x, simp, cases y, simp_all)
4.77 -next
4.78 - case goal4 thus ?case by(cases y, simp, cases x, simp_all)
4.79 -next
4.80 - case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
4.81 -next
4.82 - case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
4.83 -qed
4.84 -
4.85 -end
4.86 -
4.87 -
4.88 -locale Abs_Int1 = Val_abs1 +
4.89 -fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
4.90 -assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
4.91 -assumes above: "x0 \<sqsubseteq> pfp f x0"
4.92 -begin
4.93 -
4.94 -(* FIXME avoid duplicating this defn *)
4.95 -abbreviation astate_in_rep (infix "<:" 50) where
4.96 -"s <: S == ALL x. s x <: lookup S x"
4.97 -
4.98 -abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where
4.99 -"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
4.100 -
4.101 -lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
4.102 -apply auto
4.103 -by (metis in_mono le_astate_def le_rep lookup_def top)
4.104 -
4.105 -lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
4.106 -by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
4.107 -
4.108 -fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
4.109 -"aval' _ bot = Bot" |
4.110 -"aval' (N n) _ = num' n" |
4.111 -"aval' (V x) (Up S) = lookup S x" |
4.112 -"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
4.113 -
4.114 -lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
4.115 -by (induct a) (auto simp: rep_num' rep_plus')
4.116 -
4.117 -fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
4.118 -"afilter (N n) a S = (if n <: a then S else bot)" |
4.119 -"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
4.120 - let a' = lookup S x \<sqinter> a in
4.121 - if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
4.122 -"afilter (Plus e1 e2) a S =
4.123 - (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
4.124 - in afilter e1 a1 (afilter e2 a2 S))"
4.125 -
4.126 -text{* The test for @{const Bot} in the @{const V}-case is important: @{const
4.127 -Bot} indicates that a variable has no possible values, i.e.\ that the current
4.128 -program point is unreachable. But then the abstract state should collapse to
4.129 -@{const bot}. Put differently, we maintain the invariant that in an abstract
4.130 -state all variables are mapped to non-@{const Bot} values. Otherwise the
4.131 -(pointwise) join of two abstract states, one of which contains @{const Bot}
4.132 -values, may produce too large a result, thus making the analysis less
4.133 -precise. *}
4.134 -
4.135 -
4.136 -fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
4.137 -"bfilter (B bv) res S = (if bv=res then S else bot)" |
4.138 -"bfilter (Not b) res S = bfilter b (\<not> res) S" |
4.139 -"bfilter (And b1 b2) res S =
4.140 - (if res then bfilter b1 True (bfilter b2 True S)
4.141 - else bfilter b1 False S \<squnion> bfilter b2 False S)" |
4.142 -"bfilter (Less e1 e2) res S =
4.143 - (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
4.144 - in afilter e1 res1 (afilter e2 res2 S))"
4.145 -
4.146 -lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
4.147 -proof(induction e arbitrary: a S)
4.148 - case N thus ?case by simp
4.149 -next
4.150 - case (V x)
4.151 - obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
4.152 - moreover hence "s x <: lookup S' x" by(simp)
4.153 - moreover have "s x <: a" using V by simp
4.154 - ultimately show ?case using V(1)
4.155 - by(simp add: lookup_update Let_def)
4.156 - (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
4.157 -next
4.158 - case (Plus e1 e2) thus ?case
4.159 - using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
4.160 - by (auto split: prod.split)
4.161 -qed
4.162 -
4.163 -lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
4.164 -proof(induction b arbitrary: S bv)
4.165 - case B thus ?case by simp
4.166 -next
4.167 - case (Not b) thus ?case by simp
4.168 -next
4.169 - case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
4.170 -next
4.171 - case (Less e1 e2) thus ?case
4.172 - by (auto split: prod.split)
4.173 - (metis afilter_sound filter_less' aval'_sound Less)
4.174 -qed
4.175 -
4.176 -fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
4.177 -"AI SKIP S = S" |
4.178 -"AI (x ::= a) S =
4.179 - (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
4.180 -"AI (c1;c2) S = AI c2 (AI c1 S)" |
4.181 -"AI (IF b THEN c1 ELSE c2) S =
4.182 - AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
4.183 -"AI (WHILE b DO c) S =
4.184 - bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
4.185 -
4.186 -lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
4.187 -proof(induction c arbitrary: s t S)
4.188 - case SKIP thus ?case by fastforce
4.189 -next
4.190 - case Assign thus ?case
4.191 - by (auto simp: lookup_update aval'_sound)
4.192 -next
4.193 - case Semi thus ?case by fastforce
4.194 -next
4.195 - case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
4.196 -next
4.197 - case (While b c)
4.198 - let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
4.199 - { fix s t
4.200 - have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
4.201 - t <:: bfilter b False ?P"
4.202 - proof(induction "WHILE b DO c" s t rule: big_step_induct)
4.203 - case WhileFalse thus ?case by(metis bfilter_sound)
4.204 - next
4.205 - case WhileTrue show ?case
4.206 - by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
4.207 - rule While.IH[OF WhileTrue(2)],
4.208 - rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
4.209 - qed
4.210 - }
4.211 - with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
4.212 - show ?case by simp
4.213 -qed
4.214 -
4.215 -end
4.216 -
4.217 -end
5.1 --- a/src/HOL/IMP/AbsInt1_ivl.thy Mon Sep 26 21:13:26 2011 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,260 +0,0 @@
5.4 -(* Author: Tobias Nipkow *)
5.5 -
5.6 -theory AbsInt1_ivl
5.7 -imports AbsInt1
5.8 -begin
5.9 -
5.10 -subsection "Interval Analysis"
5.11 -
5.12 -datatype ivl = I "int option" "int option"
5.13 -
5.14 -text{* We assume an important invariant: arithmetic operations are never
5.15 -applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
5.16 -i"}. This avoids special cases. Why can we assume this? Because an empty
5.17 -interval of values for a variable means that the current program point is
5.18 -unreachable. But this should actually translate into the bottom state, not a
5.19 -state where some variables have empty intervals. *}
5.20 -
5.21 -definition "rep_ivl i =
5.22 - (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
5.23 - | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
5.24 -
5.25 -definition "num_ivl n = I (Some n) (Some n)"
5.26 -
5.27 -instantiation option :: (plus)plus
5.28 -begin
5.29 -
5.30 -fun plus_option where
5.31 -"Some x + Some y = Some(x+y)" |
5.32 -"_ + _ = None"
5.33 -
5.34 -instance proof qed
5.35 -
5.36 -end
5.37 -
5.38 -definition empty where "empty = I (Some 1) (Some 0)"
5.39 -
5.40 -fun is_empty where
5.41 -"is_empty(I (Some l) (Some h)) = (h<l)" |
5.42 -"is_empty _ = False"
5.43 -
5.44 -lemma [simp]: "is_empty(I l h) =
5.45 - (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
5.46 -by(auto split:option.split)
5.47 -
5.48 -lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
5.49 -by(auto simp add: rep_ivl_def split: ivl.split option.split)
5.50 -
5.51 -definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
5.52 - case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
5.53 -
5.54 -instantiation ivl :: SL_top
5.55 -begin
5.56 -
5.57 -definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
5.58 -"le_option pos x y =
5.59 - (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
5.60 - | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
5.61 -
5.62 -fun le_aux where
5.63 -"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
5.64 -
5.65 -definition le_ivl where
5.66 -"i1 \<sqsubseteq> i2 =
5.67 - (if is_empty i1 then True else
5.68 - if is_empty i2 then False else le_aux i1 i2)"
5.69 -
5.70 -definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
5.71 -"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
5.72 -
5.73 -definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
5.74 -"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
5.75 -
5.76 -definition "i1 \<squnion> i2 =
5.77 - (if is_empty i1 then i2 else if is_empty i2 then i1
5.78 - else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
5.79 - I (min_option False l1 l2) (max_option True h1 h2))"
5.80 -
5.81 -definition "Top = I None None"
5.82 -
5.83 -instance
5.84 -proof
5.85 - case goal1 thus ?case
5.86 - by(cases x, simp add: le_ivl_def le_option_def split: option.split)
5.87 -next
5.88 - case goal2 thus ?case
5.89 - by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
5.90 -next
5.91 - case goal3 thus ?case
5.92 - by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
5.93 -next
5.94 - case goal4 thus ?case
5.95 - by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
5.96 -next
5.97 - case goal5 thus ?case
5.98 - by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
5.99 -next
5.100 - case goal6 thus ?case
5.101 - by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
5.102 -qed
5.103 -
5.104 -end
5.105 -
5.106 -
5.107 -instantiation ivl :: L_top_bot
5.108 -begin
5.109 -
5.110 -definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
5.111 - case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
5.112 - I (max_option False l1 l2) (min_option True h1 h2))"
5.113 -
5.114 -definition "Bot = empty"
5.115 -
5.116 -instance
5.117 -proof
5.118 - case goal1 thus ?case
5.119 - by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
5.120 -next
5.121 - case goal2 thus ?case
5.122 - by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
5.123 -next
5.124 - case goal3 thus ?case
5.125 - by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
5.126 -next
5.127 - case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
5.128 -qed
5.129 -
5.130 -end
5.131 -
5.132 -instantiation option :: (minus)minus
5.133 -begin
5.134 -
5.135 -fun minus_option where
5.136 -"Some x - Some y = Some(x-y)" |
5.137 -"_ - _ = None"
5.138 -
5.139 -instance proof qed
5.140 -
5.141 -end
5.142 -
5.143 -definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
5.144 - case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
5.145 -
5.146 -lemma rep_minus_ivl:
5.147 - "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
5.148 -by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
5.149 -
5.150 -
5.151 -definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
5.152 - i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
5.153 -
5.154 -fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
5.155 -"filter_less_ivl res (I l1 h1) (I l2 h2) =
5.156 - ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
5.157 - if res
5.158 - then (I l1 (min_option True h1 (h2 - Some 1)),
5.159 - I (max_option False (l1 + Some 1) l2) h2)
5.160 - else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
5.161 -
5.162 -interpretation Rep rep_ivl
5.163 -proof
5.164 - case goal1 thus ?case
5.165 - by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
5.166 -qed
5.167 -
5.168 -interpretation Val_abs rep_ivl num_ivl plus_ivl
5.169 -proof
5.170 - case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
5.171 -next
5.172 - case goal2 thus ?case
5.173 - by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
5.174 -qed
5.175 -
5.176 -interpretation Rep1 rep_ivl
5.177 -proof
5.178 - case goal1 thus ?case
5.179 - by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
5.180 -next
5.181 - case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
5.182 -qed
5.183 -
5.184 -interpretation
5.185 - Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
5.186 -proof
5.187 - case goal1 thus ?case
5.188 - by(auto simp add: filter_plus_ivl_def)
5.189 - (metis rep_minus_ivl add_diff_cancel add_commute)+
5.190 -next
5.191 - case goal2 thus ?case
5.192 - by(cases a1, cases a2,
5.193 - auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
5.194 -qed
5.195 -
5.196 -interpretation
5.197 - Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
5.198 -defines afilter_ivl is afilter
5.199 -and bfilter_ivl is bfilter
5.200 -and AI_ivl is AI
5.201 -and aval_ivl is aval'
5.202 -proof qed (auto simp: iter'_pfp_above)
5.203 -
5.204 -
5.205 -fun list_up where
5.206 -"list_up bot = bot" |
5.207 -"list_up (Up x) = Up(list x)"
5.208 -
5.209 -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
5.210 -value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
5.211 -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
5.212 - (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
5.213 -value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
5.214 - (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
5.215 -value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
5.216 - (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
5.217 -value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
5.218 - (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
5.219 -
5.220 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
5.221 - (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
5.222 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
5.223 - (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
5.224 -value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
5.225 - (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
5.226 -
5.227 -definition "test_ivl1 =
5.228 - ''y'' ::= N 7;
5.229 - IF Less (V ''x'') (V ''y'')
5.230 - THEN ''y'' ::= Plus (V ''y'') (V ''x'')
5.231 - ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
5.232 -value [code] "list_up(AI_ivl test_ivl1 Top)"
5.233 -
5.234 -value "list_up (AI_ivl test3_const Top)"
5.235 -
5.236 -value "list_up (AI_ivl test5_const Top)"
5.237 -
5.238 -value "list_up (AI_ivl test6_const Top)"
5.239 -
5.240 -definition "test2_ivl =
5.241 - ''y'' ::= N 7;
5.242 - WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
5.243 -value [code] "list_up(AI_ivl test2_ivl Top)"
5.244 -
5.245 -definition "test3_ivl =
5.246 - ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
5.247 - WHILE Less (V ''x'') (N 11)
5.248 - DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
5.249 -value [code] "list_up(AI_ivl test3_ivl Top)"
5.250 -
5.251 -definition "test4_ivl =
5.252 - ''x'' ::= N 0; ''y'' ::= N 0;
5.253 - WHILE Less (V ''x'') (N 1001)
5.254 - DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
5.255 -value [code] "list_up(AI_ivl test4_ivl Top)"
5.256 -
5.257 -text{* Nontermination not detected: *}
5.258 -definition "test5_ivl =
5.259 - ''x'' ::= N 0;
5.260 - WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
5.261 -value [code] "list_up(AI_ivl test5_ivl Top)"
5.262 -
5.263 -end
6.1 --- a/src/HOL/IMP/AbsInt2.thy Mon Sep 26 21:13:26 2011 +0200
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,207 +0,0 @@
6.4 -(* Author: Tobias Nipkow *)
6.5 -
6.6 -theory AbsInt2
6.7 -imports AbsInt1_ivl
6.8 -begin
6.9 -
6.10 -context preord
6.11 -begin
6.12 -
6.13 -definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
6.14 -
6.15 -lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
6.16 -
6.17 -lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
6.18 -by(simp add: mono_def)
6.19 -
6.20 -declare le_trans[trans]
6.21 -
6.22 -end
6.23 -
6.24 -
6.25 -subsection "Widening and Narrowing"
6.26 -
6.27 -text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
6.28 -rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
6.29 -a trivial widening step. We generalise this idea and complement it with
6.30 -narrowing, a process to regain precision.
6.31 -
6.32 -Class @{text WN} makes some assumptions about the widening and narrowing
6.33 -operators. The assumptions serve two purposes. Together with a further
6.34 -assumption that certain chains become stationary, they permit to prove
6.35 -termination of the fixed point iteration, which we do not --- we limit the
6.36 -number of iterations as before. The second purpose of the narrowing
6.37 -assumptions is to prove that the narrowing iteration keeps on producing
6.38 -post-fixed points and that it goes down. However, this requires the function
6.39 -being iterated to be monotone. Unfortunately, abstract interpretation with
6.40 -widening is not monotone. Hence the (recursive) abstract interpretation of a
6.41 -loop body that again contains a loop may result in a non-monotone
6.42 -function. Therefore our narrowing iteration needs to check at every step
6.43 -that a post-fixed point is maintained, and we cannot prove that the precision
6.44 -increases. *}
6.45 -
6.46 -class WN = SL_top +
6.47 -fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
6.48 -assumes widen: "y \<sqsubseteq> x \<nabla> y"
6.49 -fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
6.50 -assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
6.51 -assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
6.52 -begin
6.53 -
6.54 -fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
6.55 -"iter_up f 0 x = Top" |
6.56 -"iter_up f (Suc n) x =
6.57 - (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
6.58 -
6.59 -lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
6.60 -apply (induction n arbitrary: x)
6.61 - apply (simp)
6.62 -apply (simp add: Let_def)
6.63 -done
6.64 -
6.65 -fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
6.66 -"iter_down f 0 x = x" |
6.67 -"iter_down f (Suc n) x =
6.68 - (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
6.69 -
6.70 -lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
6.71 -apply (induction n arbitrary: x)
6.72 - apply (simp)
6.73 -apply (simp add: Let_def)
6.74 -done
6.75 -
6.76 -definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
6.77 -"iter' m n f x =
6.78 - (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
6.79 -
6.80 -lemma iter'_pfp_above:
6.81 -shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
6.82 -and "x0 \<sqsubseteq> iter' m n f x0"
6.83 -using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
6.84 -by(auto simp add: iter'_def Let_def)
6.85 -
6.86 -text{* This is how narrowing works on monotone functions: you just iterate. *}
6.87 -
6.88 -abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
6.89 -"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
6.90 -
6.91 -text{* Narrowing always yields a post-fixed point: *}
6.92 -
6.93 -lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
6.94 -defines "x n == iter_down_mono f n x0"
6.95 -shows "f(x n) \<sqsubseteq> x n"
6.96 -proof (induction n)
6.97 - case 0 show ?case by (simp add: x_def assms(2))
6.98 -next
6.99 - case (Suc n)
6.100 - have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
6.101 - also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
6.102 - also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
6.103 - also have "\<dots> = x(Suc n)" by(simp add: x_def)
6.104 - finally show ?case .
6.105 -qed
6.106 -
6.107 -text{* Narrowing can only increase precision: *}
6.108 -
6.109 -lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
6.110 -defines "x n == iter_down_mono f n x0"
6.111 -shows "x n \<sqsubseteq> x0"
6.112 -proof (induction n)
6.113 - case 0 show ?case by(simp add: x_def)
6.114 -next
6.115 - case (Suc n)
6.116 - have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
6.117 - also have "\<dots> \<sqsubseteq> x n" unfolding x_def
6.118 - by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
6.119 - also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
6.120 - finally show ?case .
6.121 -qed
6.122 -
6.123 -
6.124 -end
6.125 -
6.126 -
6.127 -instantiation ivl :: WN
6.128 -begin
6.129 -
6.130 -definition "widen_ivl ivl1 ivl2 =
6.131 - ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
6.132 - case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
6.133 - I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
6.134 - (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
6.135 -
6.136 -definition "narrow_ivl ivl1 ivl2 =
6.137 - ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
6.138 - case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
6.139 - I (if l1 = None then l2 else l1)
6.140 - (if h1 = None then h2 else h1))"
6.141 -
6.142 -instance
6.143 -proof qed
6.144 - (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
6.145 -
6.146 -end
6.147 -
6.148 -instantiation astate :: (WN) WN
6.149 -begin
6.150 -
6.151 -definition "widen_astate F1 F2 =
6.152 - FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
6.153 -
6.154 -definition "narrow_astate F1 F2 =
6.155 - FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
6.156 -
6.157 -instance
6.158 -proof
6.159 - case goal1 thus ?case
6.160 - by(simp add: widen_astate_def le_astate_def lookup_def widen)
6.161 -next
6.162 - case goal2 thus ?case
6.163 - by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
6.164 -next
6.165 - case goal3 thus ?case
6.166 - by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
6.167 -qed
6.168 -
6.169 -end
6.170 -
6.171 -instantiation up :: (WN) WN
6.172 -begin
6.173 -
6.174 -fun widen_up where
6.175 -"widen_up bot x = x" |
6.176 -"widen_up x bot = x" |
6.177 -"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
6.178 -
6.179 -fun narrow_up where
6.180 -"narrow_up bot x = bot" |
6.181 -"narrow_up x bot = bot" |
6.182 -"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
6.183 -
6.184 -instance
6.185 -proof
6.186 - case goal1 show ?case
6.187 - by(induct x y rule: widen_up.induct) (simp_all add: widen)
6.188 -next
6.189 - case goal2 thus ?case
6.190 - by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
6.191 -next
6.192 - case goal3 thus ?case
6.193 - by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
6.194 -qed
6.195 -
6.196 -end
6.197 -
6.198 -interpretation
6.199 - Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
6.200 -defines afilter_ivl' is afilter
6.201 -and bfilter_ivl' is bfilter
6.202 -and AI_ivl' is AI
6.203 -and aval_ivl' is aval'
6.204 -proof qed (auto simp: iter'_pfp_above)
6.205 -
6.206 -value [code] "list_up(AI_ivl' test3_ivl Top)"
6.207 -value [code] "list_up(AI_ivl' test4_ivl Top)"
6.208 -value [code] "list_up(AI_ivl' test5_ivl Top)"
6.209 -
6.210 -end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy Wed Sep 28 08:51:55 2011 +0200
7.3 @@ -0,0 +1,67 @@
7.4 +(* Author: Tobias Nipkow *)
7.5 +
7.6 +theory Abs_Int0
7.7 +imports Abs_State
7.8 +begin
7.9 +
7.10 +subsection "Computable Abstract Interpretation"
7.11 +
7.12 +text{* Abstract interpretation over type @{text astate} instead of
7.13 +functions. *}
7.14 +
7.15 +locale Abs_Int = Val_abs +
7.16 +fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
7.17 +assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
7.18 +assumes above: "x0 \<sqsubseteq> pfp f x0"
7.19 +begin
7.20 +
7.21 +fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
7.22 +"aval' (N n) _ = num' n" |
7.23 +"aval' (V x) S = lookup S x" |
7.24 +"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
7.25 +
7.26 +abbreviation astate_in_rep (infix "<:" 50) where
7.27 +"s <: S == ALL x. s x <: lookup S x"
7.28 +
7.29 +lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
7.30 +by (metis in_mono le_astate_def le_rep lookup_def top)
7.31 +
7.32 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
7.33 +by (induct a) (auto simp: rep_num' rep_plus')
7.34 +
7.35 +
7.36 +fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
7.37 +"AI SKIP S = S" |
7.38 +"AI (x ::= a) S = update S x (aval' a S)" |
7.39 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
7.40 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
7.41 +"AI (WHILE b DO c) S = pfp (AI c) S"
7.42 +
7.43 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
7.44 +proof(induction c arbitrary: s t S0)
7.45 + case SKIP thus ?case by fastforce
7.46 +next
7.47 + case Assign thus ?case
7.48 + by (auto simp: lookup_update aval'_sound)
7.49 +next
7.50 + case Semi thus ?case by auto
7.51 +next
7.52 + case If thus ?case
7.53 + by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
7.54 +next
7.55 + case (While b c)
7.56 + let ?P = "pfp (AI c) S0"
7.57 + { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
7.58 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
7.59 + case WhileFalse thus ?case by simp
7.60 + next
7.61 + case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
7.62 + qed
7.63 + }
7.64 + with astate_in_rep_le[OF `s <: S0` above]
7.65 + show ?case by (metis While(2) AI.simps(5))
7.66 +qed
7.67 +
7.68 +end
7.69 +
7.70 +end
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy Wed Sep 28 08:51:55 2011 +0200
8.3 @@ -0,0 +1,111 @@
8.4 +(* Author: Tobias Nipkow *)
8.5 +
8.6 +theory Abs_Int0_const
8.7 +imports Abs_Int0
8.8 +begin
8.9 +
8.10 +subsection "Constant Propagation"
8.11 +
8.12 +datatype cval = Const val | Any
8.13 +
8.14 +fun rep_cval where
8.15 +"rep_cval (Const n) = {n}" |
8.16 +"rep_cval (Any) = UNIV"
8.17 +
8.18 +fun plus_cval where
8.19 +"plus_cval (Const m) (Const n) = Const(m+n)" |
8.20 +"plus_cval _ _ = Any"
8.21 +
8.22 +instantiation cval :: SL_top
8.23 +begin
8.24 +
8.25 +fun le_cval where
8.26 +"_ \<sqsubseteq> Any = True" |
8.27 +"Const n \<sqsubseteq> Const m = (n=m)" |
8.28 +"Any \<sqsubseteq> Const _ = False"
8.29 +
8.30 +fun join_cval where
8.31 +"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
8.32 +"_ \<squnion> _ = Any"
8.33 +
8.34 +definition "Top = Any"
8.35 +
8.36 +instance
8.37 +proof
8.38 + case goal1 thus ?case by (cases x) simp_all
8.39 +next
8.40 + case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
8.41 +next
8.42 + case goal3 thus ?case by(cases x, cases y, simp_all)
8.43 +next
8.44 + case goal4 thus ?case by(cases y, cases x, simp_all)
8.45 +next
8.46 + case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
8.47 +next
8.48 + case goal6 thus ?case by(simp add: Top_cval_def)
8.49 +qed
8.50 +
8.51 +end
8.52 +
8.53 +interpretation Rep rep_cval
8.54 +proof
8.55 + case goal1 thus ?case
8.56 + by(cases a, cases b, simp, simp, cases b, simp, simp)
8.57 +qed
8.58 +
8.59 +interpretation Val_abs rep_cval Const plus_cval
8.60 +proof
8.61 + case goal1 show ?case by simp
8.62 +next
8.63 + case goal2 thus ?case
8.64 + by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
8.65 +qed
8.66 +
8.67 +interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
8.68 +defines AI_const is AI
8.69 +and aval'_const is aval'
8.70 +proof qed (auto simp: iter'_pfp_above)
8.71 +
8.72 +text{* Straight line code: *}
8.73 +definition "test1_const =
8.74 + ''y'' ::= N 7;
8.75 + ''z'' ::= Plus (V ''y'') (N 2);
8.76 + ''y'' ::= Plus (V ''x'') (N 0)"
8.77 +
8.78 +text{* Conditional: *}
8.79 +definition "test2_const =
8.80 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
8.81 +
8.82 +text{* Conditional, test is ignored: *}
8.83 +definition "test3_const =
8.84 + ''x'' ::= N 42;
8.85 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
8.86 +
8.87 +text{* While: *}
8.88 +definition "test4_const =
8.89 + ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
8.90 +
8.91 +text{* While, test is ignored: *}
8.92 +definition "test5_const =
8.93 + ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
8.94 +
8.95 +text{* Iteration is needed: *}
8.96 +definition "test6_const =
8.97 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
8.98 + WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
8.99 +
8.100 +text{* More iteration would be needed: *}
8.101 +definition "test7_const =
8.102 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
8.103 + WHILE Less (V ''x'') (N 1)
8.104 + DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
8.105 +
8.106 +value [code] "list (AI_const test1_const Top)"
8.107 +value [code] "list (AI_const test2_const Top)"
8.108 +value [code] "list (AI_const test3_const Top)"
8.109 +value [code] "list (AI_const test4_const Top)"
8.110 +value [code] "list (AI_const test5_const Top)"
8.111 +value [code] "list (AI_const test6_const Top)"
8.112 +value [code] "list (AI_const test7_const Top)"
8.113 +
8.114 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy Wed Sep 28 08:51:55 2011 +0200
9.3 @@ -0,0 +1,187 @@
9.4 +(* Author: Tobias Nipkow *)
9.5 +
9.6 +header "Denotational Abstract Interpretation"
9.7 +
9.8 +theory Abs_Int0_fun
9.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
9.10 +begin
9.11 +
9.12 +subsection "Orderings"
9.13 +
9.14 +class preord =
9.15 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
9.16 +assumes le_refl[simp]: "x \<sqsubseteq> x"
9.17 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
9.18 +
9.19 +text{* Note: no antisymmetry. Allows implementations where some abstract
9.20 +element is implemented by two different values @{prop "x \<noteq> y"}
9.21 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
9.22 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
9.23 +*}
9.24 +
9.25 +class SL_top = preord +
9.26 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
9.27 +fixes Top :: "'a"
9.28 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
9.29 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
9.30 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
9.31 +and top[simp]: "x \<sqsubseteq> Top"
9.32 +begin
9.33 +
9.34 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
9.35 +by (metis join_ge1 join_ge2 join_least le_trans)
9.36 +
9.37 +fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
9.38 +"iter 0 f _ = Top" |
9.39 +"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
9.40 +
9.41 +lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
9.42 +apply (induction n arbitrary: x)
9.43 + apply (simp)
9.44 +apply (simp)
9.45 +done
9.46 +
9.47 +abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
9.48 +"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
9.49 +
9.50 +lemma iter'_pfp_above:
9.51 + "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
9.52 +using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
9.53 +
9.54 +text{* So much for soundness. But how good an approximation of the post-fixed
9.55 +point does @{const iter} yield? *}
9.56 +
9.57 +lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
9.58 +apply(induction n arbitrary: x)
9.59 + apply simp
9.60 +apply (auto)
9.61 + apply(metis funpow.simps(1) id_def)
9.62 +by (metis funpow.simps(2) funpow_swap1 o_apply)
9.63 +
9.64 +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
9.65 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
9.66 +
9.67 +lemma iter_least_pfp:
9.68 +assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
9.69 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
9.70 +proof-
9.71 + obtain k where "iter n f x0 = (f^^k) x0"
9.72 + using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
9.73 + moreover
9.74 + { fix n have "(f^^n) x0 \<sqsubseteq> p"
9.75 + proof(induction n)
9.76 + case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
9.77 + next
9.78 + case (Suc n) thus ?case
9.79 + by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
9.80 + qed
9.81 + } ultimately show ?thesis by simp
9.82 +qed
9.83 +
9.84 +end
9.85 +
9.86 +text{* The interface of abstract values: *}
9.87 +
9.88 +locale Rep =
9.89 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
9.90 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
9.91 +begin
9.92 +
9.93 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
9.94 +
9.95 +lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
9.96 +by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
9.97 +
9.98 +end
9.99 +
9.100 +locale Val_abs = Rep rep
9.101 + for rep :: "'a::SL_top \<Rightarrow> val set" +
9.102 +fixes num' :: "val \<Rightarrow> 'a"
9.103 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
9.104 +assumes rep_num': "rep(num' n) = {n}"
9.105 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
9.106 +
9.107 +
9.108 +instantiation "fun" :: (type, SL_top) SL_top
9.109 +begin
9.110 +
9.111 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
9.112 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
9.113 +definition "Top = (\<lambda>x. Top)"
9.114 +
9.115 +lemma join_apply[simp]:
9.116 + "(f \<squnion> g) x = f x \<squnion> g x"
9.117 +by (simp add: join_fun_def)
9.118 +
9.119 +instance
9.120 +proof
9.121 + case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
9.122 +qed (simp_all add: le_fun_def Top_fun_def)
9.123 +
9.124 +end
9.125 +
9.126 +subsection "Abstract Interpretation Abstractly"
9.127 +
9.128 +text{* Abstract interpretation over abstract values. Abstract states are
9.129 +simply functions. The post-fixed point finder is parameterized over. *}
9.130 +
9.131 +type_synonym 'a st = "name \<Rightarrow> 'a"
9.132 +
9.133 +locale Abs_Int_Fun = Val_abs +
9.134 +fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
9.135 +assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
9.136 +assumes above: "x \<sqsubseteq> pfp f x"
9.137 +begin
9.138 +
9.139 +fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
9.140 +"aval' (N n) _ = num' n" |
9.141 +"aval' (V x) S = S x" |
9.142 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
9.143 +
9.144 +abbreviation fun_in_rep (infix "<:" 50) where
9.145 +"f <: F == \<forall>x. f x <: F x"
9.146 +
9.147 +lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
9.148 +by (metis le_fun_def le_rep subsetD)
9.149 +
9.150 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
9.151 +by (induct a) (auto simp: rep_num' rep_plus')
9.152 +
9.153 +fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
9.154 +"AI SKIP S = S" |
9.155 +"AI (x ::= a) S = S(x := aval' a S)" |
9.156 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
9.157 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
9.158 +"AI (WHILE b DO c) S = pfp (AI c) S"
9.159 +
9.160 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
9.161 +proof(induction c arbitrary: s t S0)
9.162 + case SKIP thus ?case by fastforce
9.163 +next
9.164 + case Assign thus ?case by (auto simp: aval'_sound)
9.165 +next
9.166 + case Semi thus ?case by auto
9.167 +next
9.168 + case If thus ?case by(auto simp: in_rep_join)
9.169 +next
9.170 + case (While b c)
9.171 + let ?P = "pfp (AI c) S0"
9.172 + { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
9.173 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
9.174 + case WhileFalse thus ?case by simp
9.175 + next
9.176 + case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
9.177 + qed
9.178 + }
9.179 + with fun_in_rep_le[OF `s <: S0` above]
9.180 + show ?case by (metis While(2) AI.simps(5))
9.181 +qed
9.182 +
9.183 +end
9.184 +
9.185 +
9.186 +text{* Problem: not executable because of the comparison of abstract states,
9.187 +i.e. functions, in the post-fixedpoint computation. Need to implement
9.188 +abstract states concretely. *}
9.189 +
9.190 +end
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy Wed Sep 28 08:51:55 2011 +0200
10.3 @@ -0,0 +1,214 @@
10.4 +(* Author: Tobias Nipkow *)
10.5 +
10.6 +theory Abs_Int1
10.7 +imports Abs_Int0_const
10.8 +begin
10.9 +
10.10 +subsection "Backward Analysis of Expressions"
10.11 +
10.12 +class L_top_bot = SL_top +
10.13 +fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
10.14 +and Bot :: "'a"
10.15 +assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
10.16 +and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
10.17 +and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
10.18 +assumes bot[simp]: "Bot \<sqsubseteq> x"
10.19 +
10.20 +locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
10.21 +assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
10.22 +and rep_Bot: "rep Bot = {}"
10.23 +begin
10.24 +
10.25 +lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
10.26 +by (metis IntI inter_rep_subset_rep_meet set_mp)
10.27 +
10.28 +lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
10.29 +by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
10.30 +
10.31 +end
10.32 +
10.33 +
10.34 +locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
10.35 + for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
10.36 +fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
10.37 +and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
10.38 +assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
10.39 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
10.40 +and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
10.41 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
10.42 +
10.43 +datatype 'a up = bot | Up 'a
10.44 +
10.45 +instantiation up :: (SL_top)SL_top
10.46 +begin
10.47 +
10.48 +fun le_up where
10.49 +"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
10.50 +"bot \<sqsubseteq> y = True" |
10.51 +"Up _ \<sqsubseteq> bot = False"
10.52 +
10.53 +lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
10.54 +by (cases x) simp_all
10.55 +
10.56 +lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
10.57 +by (cases u) auto
10.58 +
10.59 +fun join_up where
10.60 +"Up x \<squnion> Up y = Up(x \<squnion> y)" |
10.61 +"bot \<squnion> y = y" |
10.62 +"x \<squnion> bot = x"
10.63 +
10.64 +lemma [simp]: "x \<squnion> bot = x"
10.65 +by (cases x) simp_all
10.66 +
10.67 +
10.68 +definition "Top = Up Top"
10.69 +
10.70 +instance proof
10.71 + case goal1 show ?case by(cases x, simp_all)
10.72 +next
10.73 + case goal2 thus ?case
10.74 + by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
10.75 +next
10.76 + case goal3 thus ?case by(cases x, simp, cases y, simp_all)
10.77 +next
10.78 + case goal4 thus ?case by(cases y, simp, cases x, simp_all)
10.79 +next
10.80 + case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
10.81 +next
10.82 + case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
10.83 +qed
10.84 +
10.85 +end
10.86 +
10.87 +
10.88 +locale Abs_Int1 = Val_abs1 +
10.89 +fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
10.90 +assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
10.91 +assumes above: "x0 \<sqsubseteq> pfp f x0"
10.92 +begin
10.93 +
10.94 +(* FIXME avoid duplicating this defn *)
10.95 +abbreviation astate_in_rep (infix "<:" 50) where
10.96 +"s <: S == ALL x. s x <: lookup S x"
10.97 +
10.98 +abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where
10.99 +"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
10.100 +
10.101 +lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
10.102 +apply auto
10.103 +by (metis in_mono le_astate_def le_rep lookup_def top)
10.104 +
10.105 +lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
10.106 +by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
10.107 +
10.108 +fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
10.109 +"aval' _ bot = Bot" |
10.110 +"aval' (N n) _ = num' n" |
10.111 +"aval' (V x) (Up S) = lookup S x" |
10.112 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
10.113 +
10.114 +lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
10.115 +by (induct a) (auto simp: rep_num' rep_plus')
10.116 +
10.117 +fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
10.118 +"afilter (N n) a S = (if n <: a then S else bot)" |
10.119 +"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
10.120 + let a' = lookup S x \<sqinter> a in
10.121 + if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
10.122 +"afilter (Plus e1 e2) a S =
10.123 + (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
10.124 + in afilter e1 a1 (afilter e2 a2 S))"
10.125 +
10.126 +text{* The test for @{const Bot} in the @{const V}-case is important: @{const
10.127 +Bot} indicates that a variable has no possible values, i.e.\ that the current
10.128 +program point is unreachable. But then the abstract state should collapse to
10.129 +@{const bot}. Put differently, we maintain the invariant that in an abstract
10.130 +state all variables are mapped to non-@{const Bot} values. Otherwise the
10.131 +(pointwise) join of two abstract states, one of which contains @{const Bot}
10.132 +values, may produce too large a result, thus making the analysis less
10.133 +precise. *}
10.134 +
10.135 +
10.136 +fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
10.137 +"bfilter (B bv) res S = (if bv=res then S else bot)" |
10.138 +"bfilter (Not b) res S = bfilter b (\<not> res) S" |
10.139 +"bfilter (And b1 b2) res S =
10.140 + (if res then bfilter b1 True (bfilter b2 True S)
10.141 + else bfilter b1 False S \<squnion> bfilter b2 False S)" |
10.142 +"bfilter (Less e1 e2) res S =
10.143 + (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
10.144 + in afilter e1 res1 (afilter e2 res2 S))"
10.145 +
10.146 +lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
10.147 +proof(induction e arbitrary: a S)
10.148 + case N thus ?case by simp
10.149 +next
10.150 + case (V x)
10.151 + obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
10.152 + moreover hence "s x <: lookup S' x" by(simp)
10.153 + moreover have "s x <: a" using V by simp
10.154 + ultimately show ?case using V(1)
10.155 + by(simp add: lookup_update Let_def)
10.156 + (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
10.157 +next
10.158 + case (Plus e1 e2) thus ?case
10.159 + using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
10.160 + by (auto split: prod.split)
10.161 +qed
10.162 +
10.163 +lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
10.164 +proof(induction b arbitrary: S bv)
10.165 + case B thus ?case by simp
10.166 +next
10.167 + case (Not b) thus ?case by simp
10.168 +next
10.169 + case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
10.170 +next
10.171 + case (Less e1 e2) thus ?case
10.172 + by (auto split: prod.split)
10.173 + (metis afilter_sound filter_less' aval'_sound Less)
10.174 +qed
10.175 +
10.176 +fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
10.177 +"AI SKIP S = S" |
10.178 +"AI (x ::= a) S =
10.179 + (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
10.180 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
10.181 +"AI (IF b THEN c1 ELSE c2) S =
10.182 + AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
10.183 +"AI (WHILE b DO c) S =
10.184 + bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
10.185 +
10.186 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
10.187 +proof(induction c arbitrary: s t S)
10.188 + case SKIP thus ?case by fastforce
10.189 +next
10.190 + case Assign thus ?case
10.191 + by (auto simp: lookup_update aval'_sound)
10.192 +next
10.193 + case Semi thus ?case by fastforce
10.194 +next
10.195 + case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
10.196 +next
10.197 + case (While b c)
10.198 + let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
10.199 + { fix s t
10.200 + have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
10.201 + t <:: bfilter b False ?P"
10.202 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
10.203 + case WhileFalse thus ?case by(metis bfilter_sound)
10.204 + next
10.205 + case WhileTrue show ?case
10.206 + by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
10.207 + rule While.IH[OF WhileTrue(2)],
10.208 + rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
10.209 + qed
10.210 + }
10.211 + with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
10.212 + show ?case by simp
10.213 +qed
10.214 +
10.215 +end
10.216 +
10.217 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy Wed Sep 28 08:51:55 2011 +0200
11.3 @@ -0,0 +1,260 @@
11.4 +(* Author: Tobias Nipkow *)
11.5 +
11.6 +theory Abs_Int1_ivl
11.7 +imports Abs_Int1
11.8 +begin
11.9 +
11.10 +subsection "Interval Analysis"
11.11 +
11.12 +datatype ivl = I "int option" "int option"
11.13 +
11.14 +text{* We assume an important invariant: arithmetic operations are never
11.15 +applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
11.16 +i"}. This avoids special cases. Why can we assume this? Because an empty
11.17 +interval of values for a variable means that the current program point is
11.18 +unreachable. But this should actually translate into the bottom state, not a
11.19 +state where some variables have empty intervals. *}
11.20 +
11.21 +definition "rep_ivl i =
11.22 + (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
11.23 + | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
11.24 +
11.25 +definition "num_ivl n = I (Some n) (Some n)"
11.26 +
11.27 +instantiation option :: (plus)plus
11.28 +begin
11.29 +
11.30 +fun plus_option where
11.31 +"Some x + Some y = Some(x+y)" |
11.32 +"_ + _ = None"
11.33 +
11.34 +instance proof qed
11.35 +
11.36 +end
11.37 +
11.38 +definition empty where "empty = I (Some 1) (Some 0)"
11.39 +
11.40 +fun is_empty where
11.41 +"is_empty(I (Some l) (Some h)) = (h<l)" |
11.42 +"is_empty _ = False"
11.43 +
11.44 +lemma [simp]: "is_empty(I l h) =
11.45 + (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
11.46 +by(auto split:option.split)
11.47 +
11.48 +lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
11.49 +by(auto simp add: rep_ivl_def split: ivl.split option.split)
11.50 +
11.51 +definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
11.52 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
11.53 +
11.54 +instantiation ivl :: SL_top
11.55 +begin
11.56 +
11.57 +definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
11.58 +"le_option pos x y =
11.59 + (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
11.60 + | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
11.61 +
11.62 +fun le_aux where
11.63 +"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
11.64 +
11.65 +definition le_ivl where
11.66 +"i1 \<sqsubseteq> i2 =
11.67 + (if is_empty i1 then True else
11.68 + if is_empty i2 then False else le_aux i1 i2)"
11.69 +
11.70 +definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
11.71 +"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
11.72 +
11.73 +definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
11.74 +"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
11.75 +
11.76 +definition "i1 \<squnion> i2 =
11.77 + (if is_empty i1 then i2 else if is_empty i2 then i1
11.78 + else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
11.79 + I (min_option False l1 l2) (max_option True h1 h2))"
11.80 +
11.81 +definition "Top = I None None"
11.82 +
11.83 +instance
11.84 +proof
11.85 + case goal1 thus ?case
11.86 + by(cases x, simp add: le_ivl_def le_option_def split: option.split)
11.87 +next
11.88 + case goal2 thus ?case
11.89 + by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
11.90 +next
11.91 + case goal3 thus ?case
11.92 + by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
11.93 +next
11.94 + case goal4 thus ?case
11.95 + by(cases x, cases y, simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits)
11.96 +next
11.97 + case goal5 thus ?case
11.98 + by(cases x, cases y, cases z, auto simp add: le_ivl_def join_ivl_def le_option_def min_option_def max_option_def split: option.splits if_splits)
11.99 +next
11.100 + case goal6 thus ?case
11.101 + by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
11.102 +qed
11.103 +
11.104 +end
11.105 +
11.106 +
11.107 +instantiation ivl :: L_top_bot
11.108 +begin
11.109 +
11.110 +definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
11.111 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
11.112 + I (max_option False l1 l2) (min_option True h1 h2))"
11.113 +
11.114 +definition "Bot = empty"
11.115 +
11.116 +instance
11.117 +proof
11.118 + case goal1 thus ?case
11.119 + by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
11.120 +next
11.121 + case goal2 thus ?case
11.122 + by (simp add:meet_ivl_def empty_def meet_ivl_def le_ivl_def le_option_def max_option_def min_option_def split: ivl.splits option.splits)
11.123 +next
11.124 + case goal3 thus ?case
11.125 + by (cases x, cases y, cases z, auto simp add: le_ivl_def meet_ivl_def empty_def le_option_def max_option_def min_option_def split: option.splits if_splits)
11.126 +next
11.127 + case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
11.128 +qed
11.129 +
11.130 +end
11.131 +
11.132 +instantiation option :: (minus)minus
11.133 +begin
11.134 +
11.135 +fun minus_option where
11.136 +"Some x - Some y = Some(x-y)" |
11.137 +"_ - _ = None"
11.138 +
11.139 +instance proof qed
11.140 +
11.141 +end
11.142 +
11.143 +definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
11.144 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
11.145 +
11.146 +lemma rep_minus_ivl:
11.147 + "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
11.148 +by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
11.149 +
11.150 +
11.151 +definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
11.152 + i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
11.153 +
11.154 +fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
11.155 +"filter_less_ivl res (I l1 h1) (I l2 h2) =
11.156 + ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
11.157 + if res
11.158 + then (I l1 (min_option True h1 (h2 - Some 1)),
11.159 + I (max_option False (l1 + Some 1) l2) h2)
11.160 + else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
11.161 +
11.162 +interpretation Rep rep_ivl
11.163 +proof
11.164 + case goal1 thus ?case
11.165 + by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
11.166 +qed
11.167 +
11.168 +interpretation Val_abs rep_ivl num_ivl plus_ivl
11.169 +proof
11.170 + case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
11.171 +next
11.172 + case goal2 thus ?case
11.173 + by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
11.174 +qed
11.175 +
11.176 +interpretation Rep1 rep_ivl
11.177 +proof
11.178 + case goal1 thus ?case
11.179 + by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
11.180 +next
11.181 + case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
11.182 +qed
11.183 +
11.184 +interpretation
11.185 + Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
11.186 +proof
11.187 + case goal1 thus ?case
11.188 + by(auto simp add: filter_plus_ivl_def)
11.189 + (metis rep_minus_ivl add_diff_cancel add_commute)+
11.190 +next
11.191 + case goal2 thus ?case
11.192 + by(cases a1, cases a2,
11.193 + auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
11.194 +qed
11.195 +
11.196 +interpretation
11.197 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
11.198 +defines afilter_ivl is afilter
11.199 +and bfilter_ivl is bfilter
11.200 +and AI_ivl is AI
11.201 +and aval_ivl is aval'
11.202 +proof qed (auto simp: iter'_pfp_above)
11.203 +
11.204 +
11.205 +fun list_up where
11.206 +"list_up bot = bot" |
11.207 +"list_up (Up x) = Up(list x)"
11.208 +
11.209 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
11.210 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
11.211 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
11.212 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
11.213 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
11.214 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
11.215 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
11.216 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
11.217 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
11.218 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
11.219 +
11.220 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
11.221 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
11.222 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
11.223 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
11.224 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
11.225 + (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
11.226 +
11.227 +definition "test_ivl1 =
11.228 + ''y'' ::= N 7;
11.229 + IF Less (V ''x'') (V ''y'')
11.230 + THEN ''y'' ::= Plus (V ''y'') (V ''x'')
11.231 + ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
11.232 +value [code] "list_up(AI_ivl test_ivl1 Top)"
11.233 +
11.234 +value "list_up (AI_ivl test3_const Top)"
11.235 +
11.236 +value "list_up (AI_ivl test5_const Top)"
11.237 +
11.238 +value "list_up (AI_ivl test6_const Top)"
11.239 +
11.240 +definition "test2_ivl =
11.241 + ''y'' ::= N 7;
11.242 + WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
11.243 +value [code] "list_up(AI_ivl test2_ivl Top)"
11.244 +
11.245 +definition "test3_ivl =
11.246 + ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
11.247 + WHILE Less (V ''x'') (N 11)
11.248 + DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
11.249 +value [code] "list_up(AI_ivl test3_ivl Top)"
11.250 +
11.251 +definition "test4_ivl =
11.252 + ''x'' ::= N 0; ''y'' ::= N 0;
11.253 + WHILE Less (V ''x'') (N 1001)
11.254 + DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
11.255 +value [code] "list_up(AI_ivl test4_ivl Top)"
11.256 +
11.257 +text{* Nontermination not detected: *}
11.258 +definition "test5_ivl =
11.259 + ''x'' ::= N 0;
11.260 + WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
11.261 +value [code] "list_up(AI_ivl test5_ivl Top)"
11.262 +
11.263 +end
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy Wed Sep 28 08:51:55 2011 +0200
12.3 @@ -0,0 +1,207 @@
12.4 +(* Author: Tobias Nipkow *)
12.5 +
12.6 +theory Abs_Int2
12.7 +imports Abs_Int1_ivl
12.8 +begin
12.9 +
12.10 +context preord
12.11 +begin
12.12 +
12.13 +definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
12.14 +
12.15 +lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
12.16 +
12.17 +lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
12.18 +by(simp add: mono_def)
12.19 +
12.20 +declare le_trans[trans]
12.21 +
12.22 +end
12.23 +
12.24 +
12.25 +subsection "Widening and Narrowing"
12.26 +
12.27 +text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
12.28 +rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
12.29 +a trivial widening step. We generalise this idea and complement it with
12.30 +narrowing, a process to regain precision.
12.31 +
12.32 +Class @{text WN} makes some assumptions about the widening and narrowing
12.33 +operators. The assumptions serve two purposes. Together with a further
12.34 +assumption that certain chains become stationary, they permit to prove
12.35 +termination of the fixed point iteration, which we do not --- we limit the
12.36 +number of iterations as before. The second purpose of the narrowing
12.37 +assumptions is to prove that the narrowing iteration keeps on producing
12.38 +post-fixed points and that it goes down. However, this requires the function
12.39 +being iterated to be monotone. Unfortunately, abstract interpretation with
12.40 +widening is not monotone. Hence the (recursive) abstract interpretation of a
12.41 +loop body that again contains a loop may result in a non-monotone
12.42 +function. Therefore our narrowing iteration needs to check at every step
12.43 +that a post-fixed point is maintained, and we cannot prove that the precision
12.44 +increases. *}
12.45 +
12.46 +class WN = SL_top +
12.47 +fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
12.48 +assumes widen: "y \<sqsubseteq> x \<nabla> y"
12.49 +fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
12.50 +assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
12.51 +assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
12.52 +begin
12.53 +
12.54 +fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
12.55 +"iter_up f 0 x = Top" |
12.56 +"iter_up f (Suc n) x =
12.57 + (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
12.58 +
12.59 +lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
12.60 +apply (induction n arbitrary: x)
12.61 + apply (simp)
12.62 +apply (simp add: Let_def)
12.63 +done
12.64 +
12.65 +fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
12.66 +"iter_down f 0 x = x" |
12.67 +"iter_down f (Suc n) x =
12.68 + (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
12.69 +
12.70 +lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
12.71 +apply (induction n arbitrary: x)
12.72 + apply (simp)
12.73 +apply (simp add: Let_def)
12.74 +done
12.75 +
12.76 +definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
12.77 +"iter' m n f x =
12.78 + (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
12.79 +
12.80 +lemma iter'_pfp_above:
12.81 +shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
12.82 +and "x0 \<sqsubseteq> iter' m n f x0"
12.83 +using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
12.84 +by(auto simp add: iter'_def Let_def)
12.85 +
12.86 +text{* This is how narrowing works on monotone functions: you just iterate. *}
12.87 +
12.88 +abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
12.89 +"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
12.90 +
12.91 +text{* Narrowing always yields a post-fixed point: *}
12.92 +
12.93 +lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
12.94 +defines "x n == iter_down_mono f n x0"
12.95 +shows "f(x n) \<sqsubseteq> x n"
12.96 +proof (induction n)
12.97 + case 0 show ?case by (simp add: x_def assms(2))
12.98 +next
12.99 + case (Suc n)
12.100 + have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
12.101 + also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
12.102 + also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
12.103 + also have "\<dots> = x(Suc n)" by(simp add: x_def)
12.104 + finally show ?case .
12.105 +qed
12.106 +
12.107 +text{* Narrowing can only increase precision: *}
12.108 +
12.109 +lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
12.110 +defines "x n == iter_down_mono f n x0"
12.111 +shows "x n \<sqsubseteq> x0"
12.112 +proof (induction n)
12.113 + case 0 show ?case by(simp add: x_def)
12.114 +next
12.115 + case (Suc n)
12.116 + have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
12.117 + also have "\<dots> \<sqsubseteq> x n" unfolding x_def
12.118 + by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
12.119 + also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
12.120 + finally show ?case .
12.121 +qed
12.122 +
12.123 +
12.124 +end
12.125 +
12.126 +
12.127 +instantiation ivl :: WN
12.128 +begin
12.129 +
12.130 +definition "widen_ivl ivl1 ivl2 =
12.131 + ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
12.132 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
12.133 + I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
12.134 + (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
12.135 +
12.136 +definition "narrow_ivl ivl1 ivl2 =
12.137 + ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
12.138 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
12.139 + I (if l1 = None then l2 else l1)
12.140 + (if h1 = None then h2 else h1))"
12.141 +
12.142 +instance
12.143 +proof qed
12.144 + (auto simp add: widen_ivl_def narrow_ivl_def le_option_def le_ivl_def empty_def split: ivl.split option.split if_splits)
12.145 +
12.146 +end
12.147 +
12.148 +instantiation astate :: (WN) WN
12.149 +begin
12.150 +
12.151 +definition "widen_astate F1 F2 =
12.152 + FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
12.153 +
12.154 +definition "narrow_astate F1 F2 =
12.155 + FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
12.156 +
12.157 +instance
12.158 +proof
12.159 + case goal1 thus ?case
12.160 + by(simp add: widen_astate_def le_astate_def lookup_def widen)
12.161 +next
12.162 + case goal2 thus ?case
12.163 + by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
12.164 +next
12.165 + case goal3 thus ?case
12.166 + by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
12.167 +qed
12.168 +
12.169 +end
12.170 +
12.171 +instantiation up :: (WN) WN
12.172 +begin
12.173 +
12.174 +fun widen_up where
12.175 +"widen_up bot x = x" |
12.176 +"widen_up x bot = x" |
12.177 +"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
12.178 +
12.179 +fun narrow_up where
12.180 +"narrow_up bot x = bot" |
12.181 +"narrow_up x bot = bot" |
12.182 +"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
12.183 +
12.184 +instance
12.185 +proof
12.186 + case goal1 show ?case
12.187 + by(induct x y rule: widen_up.induct) (simp_all add: widen)
12.188 +next
12.189 + case goal2 thus ?case
12.190 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
12.191 +next
12.192 + case goal3 thus ?case
12.193 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
12.194 +qed
12.195 +
12.196 +end
12.197 +
12.198 +interpretation
12.199 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
12.200 +defines afilter_ivl' is afilter
12.201 +and bfilter_ivl' is bfilter
12.202 +and AI_ivl' is AI
12.203 +and aval_ivl' is aval'
12.204 +proof qed (auto simp: iter'_pfp_above)
12.205 +
12.206 +value [code] "list_up(AI_ivl' test3_ivl Top)"
12.207 +value [code] "list_up(AI_ivl' test4_ivl Top)"
12.208 +value [code] "list_up(AI_ivl' test5_ivl Top)"
12.209 +
12.210 +end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State.thy Wed Sep 28 08:51:55 2011 +0200
13.3 @@ -0,0 +1,50 @@
13.4 +(* Author: Tobias Nipkow *)
13.5 +
13.6 +theory Abs_State
13.7 +imports Abs_Int0_fun
13.8 + "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
13.9 + (* Library import merely to allow string lists to be sorted for output *)
13.10 +begin
13.11 +
13.12 +subsection "Abstract State with Computable Ordering"
13.13 +
13.14 +text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
13.15 +
13.16 +datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
13.17 +
13.18 +fun "fun" where "fun (FunDom f _) = f"
13.19 +fun dom where "dom (FunDom _ A) = A"
13.20 +
13.21 +definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
13.22 +
13.23 +definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
13.24 +
13.25 +definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
13.26 +
13.27 +definition "update F x y =
13.28 + FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
13.29 +
13.30 +lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
13.31 +by(rule ext)(auto simp: lookup_def update_def)
13.32 +
13.33 +instantiation astate :: (SL_top) SL_top
13.34 +begin
13.35 +
13.36 +definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
13.37 +
13.38 +definition
13.39 +"join_astate F G =
13.40 + FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
13.41 +
13.42 +definition "Top = FunDom (\<lambda>x. Top) []"
13.43 +
13.44 +instance
13.45 +proof
13.46 + case goal2 thus ?case
13.47 + apply(auto simp: le_astate_def)
13.48 + by (metis lookup_def preord_class.le_trans top)
13.49 +qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
13.50 +
13.51 +end
13.52 +
13.53 +end
14.1 --- a/src/HOL/IMP/Astate.thy Mon Sep 26 21:13:26 2011 +0200
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,50 +0,0 @@
14.4 -(* Author: Tobias Nipkow *)
14.5 -
14.6 -theory Astate
14.7 -imports AbsInt0_fun
14.8 - "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
14.9 - (* Library import merely to allow string lists to be sorted for output *)
14.10 -begin
14.11 -
14.12 -subsection "Abstract State with Computable Ordering"
14.13 -
14.14 -text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
14.15 -
14.16 -datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
14.17 -
14.18 -fun "fun" where "fun (FunDom f _) = f"
14.19 -fun dom where "dom (FunDom _ A) = A"
14.20 -
14.21 -definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
14.22 -
14.23 -definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
14.24 -
14.25 -definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
14.26 -
14.27 -definition "update F x y =
14.28 - FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
14.29 -
14.30 -lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
14.31 -by(rule ext)(auto simp: lookup_def update_def)
14.32 -
14.33 -instantiation astate :: (SL_top) SL_top
14.34 -begin
14.35 -
14.36 -definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
14.37 -
14.38 -definition
14.39 -"join_astate F G =
14.40 - FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
14.41 -
14.42 -definition "Top = FunDom (\<lambda>x. Top) []"
14.43 -
14.44 -instance
14.45 -proof
14.46 - case goal2 thus ?case
14.47 - apply(auto simp: le_astate_def)
14.48 - by (metis lookup_def preord_class.le_trans top)
14.49 -qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
14.50 -
14.51 -end
14.52 -
14.53 -end
15.1 --- a/src/HOL/IMP/ROOT.ML Mon Sep 26 21:13:26 2011 +0200
15.2 +++ b/src/HOL/IMP/ROOT.ML Wed Sep 28 08:51:55 2011 +0200
15.3 @@ -15,10 +15,10 @@
15.4 "Def_Ass_Sound_Big",
15.5 "Def_Ass_Sound_Small",
15.6 "Live",
15.7 - "AbsInt2",
15.8 "Hoare_Examples",
15.9 "VC",
15.10 "HoareT",
15.11 + "Abs_Int_Den/Abs_Int2",
15.12 "Procs_Dyn_Vars_Dyn",
15.13 "Procs_Stat_Vars_Dyn",
15.14 "Procs_Stat_Vars_Stat",
16.1 --- a/src/HOL/IsaMakefile Mon Sep 26 21:13:26 2011 +0200
16.2 +++ b/src/HOL/IsaMakefile Wed Sep 28 08:51:55 2011 +0200
16.3 @@ -515,9 +515,11 @@
16.4
16.5 HOL-IMP: HOL $(OUT)/HOL-IMP
16.6
16.7 -$(OUT)/HOL-IMP: $(OUT)/HOL IMP/AbsInt0_fun.thy IMP/Astate.thy \
16.8 - IMP/AbsInt0.thy IMP/AbsInt0_const.thy IMP/AbsInt1.thy IMP/AbsInt1_ivl.thy \
16.9 - IMP/AbsInt2.thy IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
16.10 +$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int0_fun.thy \
16.11 + IMP/Abs_Int_Den/Abs_State.thy IMP/Abs_Int_Den/Abs_Int0.thy \
16.12 + IMP/Abs_Int_Den/Abs_Int0_const.thy IMP/Abs_Int_Den/Abs_Int1.thy \
16.13 + IMP/Abs_Int_Den/Abs_Int1_ivl.thy IMP/Abs_Int_Den/Abs_Int2.thy \
16.14 + IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
16.15 IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
16.16 IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
16.17 IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \