1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/Abs_Int0.thy Wed Sep 28 09:55:11 2011 +0200
1.3 @@ -0,0 +1,101 @@
1.4 +(* Author: Tobias Nipkow *)
1.5 +
1.6 +theory Abs_Int0
1.7 +imports Abs_State
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 st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
1.17 +assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
1.18 +and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
1.19 +begin
1.20 +
1.21 +fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
1.22 +"aval' (N n) _ = num' n" |
1.23 +"aval' (V x) S = lookup S x" |
1.24 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
1.25 +
1.26 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
1.27 +"step S (SKIP {P}) = (SKIP {S})" |
1.28 +"step S (x ::= e {P}) =
1.29 + x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" |
1.30 +"step S (c1; c2) = step S c1; step (post c1) c2" |
1.31 +"step S (IF b THEN c1 ELSE c2 {P}) =
1.32 + (let c1' = step S c1; c2' = step S c2
1.33 + in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
1.34 +"step S ({Inv} WHILE b DO c {P}) =
1.35 + {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
1.36 +
1.37 +lemma strip_step[simp]: "strip(step S c) = strip c"
1.38 +by(induct c arbitrary: S) (simp_all add: Let_def)
1.39 +
1.40 +definition AI :: "com \<Rightarrow> 'a st up acom" where
1.41 +"AI c = pfp (step Top) (bot_acom c)"
1.42 +
1.43 +
1.44 +subsubsection "Monotonicity"
1.45 +
1.46 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
1.47 +by(induction e) (auto simp: le_st_def lookup_def mono_plus')
1.48 +
1.49 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
1.50 +by(auto simp add: le_st_def lookup_def update_def)
1.51 +
1.52 +lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
1.53 +apply(induction c arbitrary: S S')
1.54 +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
1.55 +done
1.56 +
1.57 +subsubsection "Soundness"
1.58 +
1.59 +lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
1.60 +by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
1.61 +
1.62 +lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
1.63 +by(simp add: rep_st_def lookup_update)
1.64 +
1.65 +lemma step_sound:
1.66 + "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
1.67 +proof(induction c arbitrary: S s t)
1.68 + case SKIP thus ?case
1.69 + by simp (metis skipE up_fun_in_rep_le)
1.70 +next
1.71 + case Assign thus ?case
1.72 + apply (auto simp del: fun_upd_apply simp: split: up.splits)
1.73 + by (metis aval'_sound fun_in_rep_le in_rep_update)
1.74 +next
1.75 + case Semi thus ?case by simp blast
1.76 +next
1.77 + case (If b c1 c2 S0) thus ?case
1.78 + apply(auto simp: Let_def)
1.79 + apply (metis up_fun_in_rep_le)+
1.80 + done
1.81 +next
1.82 + case (While Inv b c P)
1.83 + from While.prems have inv: "step Inv c \<sqsubseteq> c"
1.84 + and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
1.85 + { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
1.86 + proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
1.87 + case WhileFalse thus ?case by simp
1.88 + next
1.89 + case (WhileTrue s1 s2 s3)
1.90 + from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
1.91 + show ?case .
1.92 + qed
1.93 + }
1.94 + thus ?case using While.prems(2)
1.95 + by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
1.96 +qed
1.97 +
1.98 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
1.99 +by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
1.100 +
1.101 +end
1.102 +
1.103 +
1.104 +end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/IMP/Abs_Int0_const.thy Wed Sep 28 09:55:11 2011 +0200
2.3 @@ -0,0 +1,150 @@
2.4 +(* Author: Tobias Nipkow *)
2.5 +
2.6 +theory Abs_Int0_const
2.7 +imports Abs_Int0
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 +lemma plus_cval_cases: "plus_cval a1 a2 =
2.23 + (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
2.24 +by(auto split: prod.split cval.split)
2.25 +
2.26 +instantiation cval :: SL_top
2.27 +begin
2.28 +
2.29 +fun le_cval where
2.30 +"_ \<sqsubseteq> Any = True" |
2.31 +"Const n \<sqsubseteq> Const m = (n=m)" |
2.32 +"Any \<sqsubseteq> Const _ = False"
2.33 +
2.34 +fun join_cval where
2.35 +"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
2.36 +"_ \<squnion> _ = Any"
2.37 +
2.38 +definition "\<top> = Any"
2.39 +
2.40 +instance
2.41 +proof
2.42 + case goal1 thus ?case by (cases x) simp_all
2.43 +next
2.44 + case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
2.45 +next
2.46 + case goal3 thus ?case by(cases x, cases y, simp_all)
2.47 +next
2.48 + case goal4 thus ?case by(cases y, cases x, simp_all)
2.49 +next
2.50 + case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
2.51 +next
2.52 + case goal6 thus ?case by(simp add: Top_cval_def)
2.53 +qed
2.54 +
2.55 +end
2.56 +
2.57 +interpretation Rep rep_cval
2.58 +proof
2.59 + case goal1 thus ?case
2.60 + by(cases a, cases b, simp, simp, cases b, simp, simp)
2.61 +next
2.62 + case goal2 show ?case by(simp add: Top_cval_def)
2.63 +qed
2.64 +
2.65 +interpretation Val_abs rep_cval Const plus_cval
2.66 +proof
2.67 + case goal1 show ?case by simp
2.68 +next
2.69 + case goal2 thus ?case
2.70 + by(auto simp: plus_cval_cases split: cval.split)
2.71 +next
2.72 + case goal3 thus ?case
2.73 + by(auto simp: plus_cval_cases split: cval.split)
2.74 +qed
2.75 +
2.76 +text{* Could set the limit of the number of iterations to an arbitrarily
2.77 +large number because all ascending chains in this semilattice are finite. *}
2.78 +
2.79 +interpretation Abs_Int rep_cval Const plus_cval "(iter 15)"
2.80 +defines AI_const is AI
2.81 +and aval'_const is aval'
2.82 +and step_const is step
2.83 +proof qed (auto simp: iter_pfp strip_iter)
2.84 +
2.85 +text{* Straight line code: *}
2.86 +definition "test1_const =
2.87 + ''y'' ::= N 7;
2.88 + ''z'' ::= Plus (V ''y'') (N 2);
2.89 + ''y'' ::= Plus (V ''x'') (N 0)"
2.90 +
2.91 +text{* Conditional: *}
2.92 +definition "test2_const =
2.93 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
2.94 +
2.95 +text{* Conditional, test is ignored: *}
2.96 +definition "test3_const =
2.97 + ''x'' ::= N 42;
2.98 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
2.99 +
2.100 +text{* While: *}
2.101 +definition "test4_const =
2.102 + ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
2.103 +
2.104 +text{* While, test is ignored: *}
2.105 +definition "test5_const =
2.106 + ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
2.107 +
2.108 +text{* Iteration is needed: *}
2.109 +definition "test6_const =
2.110 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
2.111 + WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
2.112 +
2.113 +text{* More iteration would be needed: *}
2.114 +definition "test7_const =
2.115 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
2.116 + WHILE Less (V ''x'') (N 1)
2.117 + DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
2.118 +
2.119 +text{* For readability: *}
2.120 +translations "x" <= "CONST V x"
2.121 +translations "x" <= "CONST N x"
2.122 +translations "x" <= "CONST Const x"
2.123 +translations "x < y" <= "CONST Less x y"
2.124 +translations "x" <= "CONST B x"
2.125 +translations "x" <= "CONST Up x"
2.126 +
2.127 +value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
2.128 +value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
2.129 +value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
2.130 +value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
2.131 +value [code] "show_acom (AI_const test1_const)"
2.132 +
2.133 +value [code] "show_acom (AI_const test2_const)"
2.134 +value [code] "show_acom (AI_const test3_const)"
2.135 +
2.136 +value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
2.137 +value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
2.138 +value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
2.139 +value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
2.140 +value [code] "show_acom (AI_const test4_const)"
2.141 +
2.142 +value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
2.143 +value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
2.144 +value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
2.145 +value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
2.146 +value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
2.147 +value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
2.148 +value [code] "show_acom (AI_const test5_const)"
2.149 +
2.150 +value [code] "show_acom (AI_const test6_const)"
2.151 +value [code] "show_acom (AI_const test7_const)"
2.152 +
2.153 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/IMP/Abs_Int0_fun.thy Wed Sep 28 09:55:11 2011 +0200
3.3 @@ -0,0 +1,423 @@
3.4 +(* Author: Tobias Nipkow *)
3.5 +
3.6 +header "Abstract Interpretation"
3.7 +
3.8 +theory Abs_Int0_fun
3.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
3.10 +begin
3.11 +
3.12 +subsection "Annotated Commands"
3.13 +
3.14 +datatype 'a acom =
3.15 + SKIP 'a ("SKIP {_}") |
3.16 + Assign name aexp 'a ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
3.17 + Semi "'a acom" "'a acom" ("_;// _" [60, 61] 60) |
3.18 + If bexp "'a acom" "'a acom" 'a
3.19 + ("((IF _/ THEN _/ ELSE _)/ {_})" [0, 0, 61, 0] 61) |
3.20 + While 'a bexp "'a acom" 'a
3.21 + ("({_}// WHILE _/ DO (_)// {_})" [0, 0, 61, 0] 61)
3.22 +
3.23 +fun post :: "'a acom \<Rightarrow>'a" where
3.24 +"post (SKIP {P}) = P" |
3.25 +"post (x ::= e {P}) = P" |
3.26 +"post (c1; c2) = post c2" |
3.27 +"post (IF b THEN c1 ELSE c2 {P}) = P" |
3.28 +"post ({Inv} WHILE b DO c {P}) = P"
3.29 +
3.30 +fun strip :: "'a acom \<Rightarrow> com" where
3.31 +"strip (SKIP {a}) = com.SKIP" |
3.32 +"strip (x ::= e {a}) = (x ::= e)" |
3.33 +"strip (c1;c2) = (strip c1; strip c2)" |
3.34 +"strip (IF b THEN c1 ELSE c2 {a}) = (IF b THEN strip c1 ELSE strip c2)" |
3.35 +"strip ({a1} WHILE b DO c {a2}) = (WHILE b DO strip c)"
3.36 +
3.37 +fun anno :: "'a \<Rightarrow> com \<Rightarrow> 'a acom" where
3.38 +"anno a com.SKIP = SKIP {a}" |
3.39 +"anno a (x ::= e) = (x ::= e {a})" |
3.40 +"anno a (c1;c2) = (anno a c1; anno a c2)" |
3.41 +"anno a (IF b THEN c1 ELSE c2) =
3.42 + (IF b THEN anno a c1 ELSE anno a c2 {a})" |
3.43 +"anno a (WHILE b DO c) =
3.44 + ({a} WHILE b DO anno a c {a})"
3.45 +
3.46 +lemma strip_anno[simp]: "strip (anno a c) = c"
3.47 +by(induct c) simp_all
3.48 +
3.49 +fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
3.50 +"map_acom f (SKIP {a}) = SKIP {f a}" |
3.51 +"map_acom f (x ::= e {a}) = (x ::= e {f a})" |
3.52 +"map_acom f (c1;c2) = (map_acom f c1; map_acom f c2)" |
3.53 +"map_acom f (IF b THEN c1 ELSE c2 {a}) =
3.54 + (IF b THEN map_acom f c1 ELSE map_acom f c2 {f a})" |
3.55 +"map_acom f ({a1} WHILE b DO c {a2}) =
3.56 + ({f a1} WHILE b DO map_acom f c {f a2})"
3.57 +
3.58 +
3.59 +subsection "Orderings"
3.60 +
3.61 +class preord =
3.62 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
3.63 +assumes le_refl[simp]: "x \<sqsubseteq> x"
3.64 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
3.65 +begin
3.66 +
3.67 +definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
3.68 +
3.69 +lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
3.70 +
3.71 +lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
3.72 +by(simp add: mono_def)
3.73 +
3.74 +declare le_trans[trans]
3.75 +
3.76 +end
3.77 +
3.78 +text{* Note: no antisymmetry. Allows implementations where some abstract
3.79 +element is implemented by two different values @{prop "x \<noteq> y"}
3.80 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
3.81 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
3.82 +*}
3.83 +
3.84 +class SL_top = preord +
3.85 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
3.86 +fixes Top :: "'a" ("\<top>")
3.87 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
3.88 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
3.89 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
3.90 +and top[simp]: "x \<sqsubseteq> \<top>"
3.91 +begin
3.92 +
3.93 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
3.94 +by (metis join_ge1 join_ge2 join_least le_trans)
3.95 +
3.96 +lemma le_join_disj: "x \<sqsubseteq> y \<or> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<squnion> z"
3.97 +by (metis join_ge1 join_ge2 le_trans)
3.98 +
3.99 +end
3.100 +
3.101 +instantiation "fun" :: (type, SL_top) SL_top
3.102 +begin
3.103 +
3.104 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
3.105 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
3.106 +definition "\<top> = (\<lambda>x. \<top>)"
3.107 +
3.108 +lemma join_apply[simp]: "(f \<squnion> g) x = f x \<squnion> g x"
3.109 +by (simp add: join_fun_def)
3.110 +
3.111 +instance
3.112 +proof
3.113 + case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
3.114 +qed (simp_all add: le_fun_def Top_fun_def)
3.115 +
3.116 +end
3.117 +
3.118 +
3.119 +instantiation acom :: (preord) preord
3.120 +begin
3.121 +
3.122 +fun le_acom :: "('a::preord)acom \<Rightarrow> 'a acom \<Rightarrow> bool" where
3.123 +"le_acom (SKIP {S}) (SKIP {S'}) = (S \<sqsubseteq> S')" |
3.124 +"le_acom (x ::= e {S}) (x' ::= e' {S'}) = (x=x' \<and> e=e' \<and> S \<sqsubseteq> S')" |
3.125 +"le_acom (c1;c2) (c1';c2') = (le_acom c1 c1' \<and> le_acom c2 c2')" |
3.126 +"le_acom (IF b THEN c1 ELSE c2 {S}) (IF b' THEN c1' ELSE c2' {S'}) =
3.127 + (b=b' \<and> le_acom c1 c1' \<and> le_acom c2 c2' \<and> S \<sqsubseteq> S')" |
3.128 +"le_acom ({Inv} WHILE b DO c {P}) ({Inv'} WHILE b' DO c' {P'}) =
3.129 + (b=b' \<and> le_acom c c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')" |
3.130 +"le_acom _ _ = False"
3.131 +
3.132 +lemma [simp]: "SKIP {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = SKIP {S'} \<and> S \<sqsubseteq> S')"
3.133 +by (cases c) auto
3.134 +
3.135 +lemma [simp]: "x ::= e {S} \<sqsubseteq> c \<longleftrightarrow> (\<exists>S'. c = x ::= e {S'} \<and> S \<sqsubseteq> S')"
3.136 +by (cases c) auto
3.137 +
3.138 +lemma [simp]: "c1;c2 \<sqsubseteq> c \<longleftrightarrow> (\<exists>c1' c2'. c = c1';c2' \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2')"
3.139 +by (cases c) auto
3.140 +
3.141 +lemma [simp]: "IF b THEN c1 ELSE c2 {S} \<sqsubseteq> c \<longleftrightarrow>
3.142 + (\<exists>c1' c2' S'. c = IF b THEN c1' ELSE c2' {S'} \<and> c1 \<sqsubseteq> c1' \<and> c2 \<sqsubseteq> c2' \<and> S \<sqsubseteq> S')"
3.143 +by (cases c) auto
3.144 +
3.145 +lemma [simp]: "{Inv} WHILE b DO c {P} \<sqsubseteq> w \<longleftrightarrow>
3.146 + (\<exists>Inv' c' P'. w = {Inv'} WHILE b DO c' {P'} \<and> c \<sqsubseteq> c' \<and> Inv \<sqsubseteq> Inv' \<and> P \<sqsubseteq> P')"
3.147 +by (cases w) auto
3.148 +
3.149 +instance
3.150 +proof
3.151 + case goal1 thus ?case by (induct x) auto
3.152 +next
3.153 + case goal2 thus ?case
3.154 + apply(induct x y arbitrary: z rule: le_acom.induct)
3.155 + apply (auto intro: le_trans)
3.156 + done
3.157 +qed
3.158 +
3.159 +end
3.160 +
3.161 +definition Top_acom :: "com \<Rightarrow> ('a::SL_top) acom" ("\<top>\<^sub>c") where
3.162 +"\<top>\<^sub>c = anno \<top>"
3.163 +
3.164 +lemma strip_Top_acom[simp]: "strip (\<top>\<^sub>c c) = c"
3.165 +by(simp add: Top_acom_def)
3.166 +
3.167 +lemma le_Top_acomp[simp]: "strip c' = c \<Longrightarrow> c' \<sqsubseteq> \<top>\<^sub>c c"
3.168 +by(induct c' arbitrary: c) (auto simp: Top_acom_def)
3.169 +
3.170 +
3.171 +subsubsection "Lifting"
3.172 +
3.173 +datatype 'a up = Bot | Up 'a
3.174 +
3.175 +instantiation up :: (SL_top)SL_top
3.176 +begin
3.177 +
3.178 +fun le_up where
3.179 +"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
3.180 +"Bot \<sqsubseteq> y = True" |
3.181 +"Up _ \<sqsubseteq> Bot = False"
3.182 +
3.183 +lemma [simp]: "(x \<sqsubseteq> Bot) = (x = Bot)"
3.184 +by (cases x) simp_all
3.185 +
3.186 +lemma [simp]: "(Up x \<sqsubseteq> u) = (\<exists>y. u = Up y & x \<sqsubseteq> y)"
3.187 +by (cases u) auto
3.188 +
3.189 +fun join_up where
3.190 +"Up x \<squnion> Up y = Up(x \<squnion> y)" |
3.191 +"Bot \<squnion> y = y" |
3.192 +"x \<squnion> Bot = x"
3.193 +
3.194 +lemma [simp]: "x \<squnion> Bot = x"
3.195 +by (cases x) simp_all
3.196 +
3.197 +definition "\<top> = Up \<top>"
3.198 +
3.199 +instance proof
3.200 + case goal1 show ?case by(cases x, simp_all)
3.201 +next
3.202 + case goal2 thus ?case
3.203 + by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
3.204 +next
3.205 + case goal3 thus ?case by(cases x, simp, cases y, simp_all)
3.206 +next
3.207 + case goal4 thus ?case by(cases y, simp, cases x, simp_all)
3.208 +next
3.209 + case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
3.210 +next
3.211 + case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
3.212 +qed
3.213 +
3.214 +end
3.215 +
3.216 +definition bot_acom :: "com \<Rightarrow> ('a::SL_top)up acom" ("\<bottom>\<^sub>c") where
3.217 +"\<bottom>\<^sub>c = anno Bot"
3.218 +
3.219 +lemma strip_bot_acom[simp]: "strip(\<bottom>\<^sub>c c) = c"
3.220 +by(simp add: bot_acom_def)
3.221 +
3.222 +
3.223 +subsection "Absract Interpretation"
3.224 +
3.225 +text{* The representation of abstract by a set of concrete values: *}
3.226 +
3.227 +locale Rep =
3.228 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
3.229 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
3.230 +and rep_Top: "rep \<top> = UNIV"
3.231 +begin
3.232 +
3.233 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
3.234 +
3.235 +lemma in_rep_Top[simp]: "x <: \<top>"
3.236 +by(simp add: rep_Top)
3.237 +
3.238 +end
3.239 +
3.240 +definition rep_fun :: "('a \<Rightarrow> 'b set) \<Rightarrow> ('c \<Rightarrow> 'a) \<Rightarrow> ('c \<Rightarrow> 'b)set" where
3.241 +"rep_fun rep F = {f. \<forall>x. f x \<in> rep(F x)}"
3.242 +
3.243 +fun rep_up :: "('a \<Rightarrow> 'b set) \<Rightarrow> 'a up \<Rightarrow> 'b set" where
3.244 +"rep_up rep Bot = {}" |
3.245 +"rep_up rep (Up a) = rep a"
3.246 +
3.247 +text{* The interface for abstract values: *}
3.248 +
3.249 +(* FIXME: separate Rep interface needed? *)
3.250 +locale Val_abs = Rep rep for rep :: "'a::SL_top \<Rightarrow> val set" +
3.251 +fixes num' :: "val \<Rightarrow> 'a"
3.252 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
3.253 +assumes rep_num': "n <: num' n"
3.254 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
3.255 +and mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
3.256 +
3.257 +
3.258 +subsubsection "Post-fixed point iteration"
3.259 +
3.260 +fun iter :: "nat \<Rightarrow> (('a::SL_top) acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
3.261 +"iter 0 f c = \<top>\<^sub>c (strip c)" |
3.262 +"iter (Suc n) f c = (let fc = f c in if fc \<sqsubseteq> c then c else iter n f fc)"
3.263 +(* code lemma?? *)
3.264 +
3.265 +lemma strip_iter: assumes "\<forall>c. strip(f c) = strip c"
3.266 +shows "strip(iter n f c) = strip c"
3.267 +apply (induction n arbitrary: c)
3.268 + apply (metis iter.simps(1) strip_Top_acom)
3.269 +apply (simp add:Let_def)
3.270 +by (metis assms)
3.271 +
3.272 +lemma iter_pfp: assumes "\<forall>c. strip(f c) = strip c"
3.273 +shows "f(iter n f c) \<sqsubseteq> iter n f c"
3.274 +apply (induction n arbitrary: c)
3.275 + apply(simp add: assms)
3.276 +apply (simp add:Let_def)
3.277 +done
3.278 +
3.279 +lemma iter_funpow: assumes "\<forall>c. strip(f c) = strip c"
3.280 +shows "iter n f x \<noteq> \<top>\<^sub>c (strip x) \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
3.281 +apply(induction n arbitrary: x)
3.282 + apply simp
3.283 +apply (auto simp: Let_def assms)
3.284 + apply(metis funpow.simps(1) id_def)
3.285 +by (metis assms funpow.simps(2) funpow_swap1 o_apply)
3.286 +
3.287 +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
3.288 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
3.289 +
3.290 +lemma iter_least_pfp:
3.291 +assumes strip: "\<forall>c. strip(f c) = strip c"
3.292 +and mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
3.293 +and not_top: "iter n f x0 \<noteq> \<top>\<^sub>c (strip x0)"
3.294 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
3.295 +proof-
3.296 + obtain k where "iter n f x0 = (f^^k) x0"
3.297 + using iter_funpow[OF strip not_top] by blast
3.298 + moreover
3.299 + { fix n have "(f^^n) x0 \<sqsubseteq> p"
3.300 + proof(induction n)
3.301 + case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
3.302 + next
3.303 + case (Suc n) thus ?case
3.304 + by (simp add: `x0 \<sqsubseteq> p`)(metis Suc `f p \<sqsubseteq> p` le_trans mono)
3.305 + qed
3.306 + } ultimately show ?thesis by simp
3.307 +qed
3.308 +
3.309 +type_synonym 'a st = "(name \<Rightarrow> 'a)"
3.310 +
3.311 +locale Abs_Int_Fun = Val_abs +
3.312 +fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
3.313 +assumes pfp: "f(pfp f c) \<sqsubseteq> pfp f c"
3.314 +and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
3.315 +begin
3.316 +
3.317 +fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
3.318 +"aval' (N n) _ = num' n" |
3.319 +"aval' (V x) S = S x" |
3.320 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
3.321 +
3.322 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
3.323 +"step S (SKIP {P}) = (SKIP {S})" |
3.324 +"step S (x ::= e {P}) =
3.325 + x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(S(x := aval' e S))}" |
3.326 +"step S (c1; c2) = step S c1; step (post c1) c2" |
3.327 +"step S (IF b THEN c1 ELSE c2 {P}) =
3.328 + (let c1' = step S c1; c2' = step S c2
3.329 + in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
3.330 +"step S ({Inv} WHILE b DO c {P}) =
3.331 + {S \<squnion> post c} WHILE b DO (step Inv c) {Inv}"
3.332 +
3.333 +lemma strip_step[simp]: "strip(step S c) = strip c"
3.334 +by(induct c arbitrary: S) (simp_all add: Let_def)
3.335 +
3.336 +
3.337 +definition AI :: "com \<Rightarrow> 'a st up acom" where
3.338 +"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
3.339 +
3.340 +
3.341 +abbreviation fun_in_rep :: "state \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
3.342 +"s <:f S == s \<in> rep_fun rep S"
3.343 +
3.344 +notation fun_in_rep (infix "<:\<^sub>f" 50)
3.345 +
3.346 +lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
3.347 +by(auto simp add: rep_fun_def le_fun_def dest: le_rep)
3.348 +
3.349 +abbreviation up_in_rep :: "state \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50) where
3.350 +"s <:up S == s : rep_up (rep_fun rep) S"
3.351 +
3.352 +notation (output) up_in_rep (infix "<:\<^sub>u\<^sub>p" 50)
3.353 +
3.354 +lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
3.355 +by (cases S) (auto intro:fun_in_rep_le)
3.356 +
3.357 +lemma in_rep_Top_fun: "s <:f Top"
3.358 +by(simp add: Top_fun_def rep_fun_def)
3.359 +
3.360 +lemma in_rep_Top_up: "s <:up Top"
3.361 +by(simp add: Top_up_def in_rep_Top_fun)
3.362 +
3.363 +
3.364 +subsubsection "Monotonicity"
3.365 +
3.366 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
3.367 +by(induction e)(auto simp: le_fun_def mono_plus')
3.368 +
3.369 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> S(x := a) \<sqsubseteq> S'(x := a')"
3.370 +by(simp add: le_fun_def)
3.371 +
3.372 +lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
3.373 +apply(induction c arbitrary: S S')
3.374 +apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
3.375 +done
3.376 +
3.377 +subsubsection "Soundness"
3.378 +
3.379 +lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
3.380 +by (induct a) (auto simp: rep_num' rep_plus' rep_fun_def)
3.381 +
3.382 +lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f S(x := a)"
3.383 +by(simp add: rep_fun_def)
3.384 +
3.385 +lemma step_sound:
3.386 + "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
3.387 +proof(induction c arbitrary: S s t)
3.388 + case SKIP thus ?case
3.389 + by simp (metis skipE up_fun_in_rep_le)
3.390 +next
3.391 + case Assign thus ?case
3.392 + apply (auto simp del: fun_upd_apply split: up.splits)
3.393 + by (metis aval'_sound fun_in_rep_le in_rep_update)
3.394 +next
3.395 + case Semi thus ?case by simp blast
3.396 +next
3.397 + case (If b c1 c2 S0) thus ?case
3.398 + apply(auto simp: Let_def)
3.399 + apply (metis up_fun_in_rep_le)+
3.400 + done
3.401 +next
3.402 + case (While Inv b c P)
3.403 + from While.prems have inv: "step Inv c \<sqsubseteq> c"
3.404 + and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
3.405 + { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
3.406 + proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
3.407 + case WhileFalse thus ?case by simp
3.408 + next
3.409 + case (WhileTrue s1 s2 s3)
3.410 + from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]]
3.411 + show ?case .
3.412 + qed
3.413 + }
3.414 + thus ?case using While.prems(2)
3.415 + by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
3.416 +qed
3.417 +
3.418 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
3.419 +by(auto simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp)
3.420 +
3.421 +end
3.422 +
3.423 +text{* Problem: not executable because of the comparison of abstract states,
3.424 +i.e. functions, in the post-fixedpoint computation. *}
3.425 +
3.426 +end
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/IMP/Abs_Int1.thy Wed Sep 28 09:55:11 2011 +0200
4.3 @@ -0,0 +1,266 @@
4.4 +(* Author: Tobias Nipkow *)
4.5 +
4.6 +theory Abs_Int1
4.7 +imports Abs_Int0_const
4.8 +begin
4.9 +
4.10 +instantiation prod :: (preord,preord) preord
4.11 +begin
4.12 +
4.13 +definition "le_prod p1 p2 = (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
4.14 +
4.15 +instance
4.16 +proof
4.17 + case goal1 show ?case by(simp add: le_prod_def)
4.18 +next
4.19 + case goal2 thus ?case unfolding le_prod_def by(metis le_trans)
4.20 +qed
4.21 +
4.22 +end
4.23 +
4.24 +
4.25 +subsection "Backward Analysis of Expressions"
4.26 +
4.27 +hide_const bot
4.28 +
4.29 +class L_top_bot = SL_top +
4.30 +fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
4.31 +and bot :: "'a" ("\<bottom>")
4.32 +assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
4.33 +and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
4.34 +and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
4.35 +assumes bot[simp]: "\<bottom> \<sqsubseteq> x"
4.36 +
4.37 +locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
4.38 +assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
4.39 + -- "this means the meet is precise"
4.40 +and rep_Bot: "rep \<bottom> = {}"
4.41 +begin
4.42 +
4.43 +lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
4.44 +by (metis IntI inter_rep_subset_rep_meet set_mp)
4.45 +
4.46 +lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
4.47 +by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
4.48 +
4.49 +lemma mono_meet: "x \<sqsubseteq> x' \<Longrightarrow> y \<sqsubseteq> y' \<Longrightarrow> x \<sqinter> y \<sqsubseteq> x' \<sqinter> y'"
4.50 +by (metis meet_greatest meet_le1 meet_le2 le_trans)
4.51 +
4.52 +end
4.53 +
4.54 +
4.55 +locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
4.56 + for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
4.57 +fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
4.58 +and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
4.59 +assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
4.60 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
4.61 +and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
4.62 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
4.63 +and mono_filter_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> r \<sqsubseteq> r' \<Longrightarrow>
4.64 + filter_plus' r a1 a2 \<sqsubseteq> filter_plus' r' b1 b2"
4.65 +and mono_filter_less': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow>
4.66 + filter_less' bv a1 a2 \<sqsubseteq> filter_less' bv b1 b2"
4.67 +
4.68 +locale Abs_Int1 = Val_abs1 +
4.69 +fixes pfp :: "('a st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom"
4.70 +assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> mono f \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c"
4.71 +and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c"
4.72 +begin
4.73 +
4.74 +lemma in_rep_join_UpI: "s <:up S1 | s <:up S2 \<Longrightarrow> s <:up S1 \<squnion> S2"
4.75 +by (metis join_ge1 join_ge2 up_fun_in_rep_le)
4.76 +
4.77 +fun aval' :: "aexp \<Rightarrow> 'a st up \<Rightarrow> 'a" where
4.78 +"aval' _ Bot = \<bottom>" |
4.79 +"aval' (N n) _ = num' n" |
4.80 +"aval' (V x) (Up S) = lookup S x" |
4.81 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
4.82 +
4.83 +lemma aval'_sound: "s <:up S \<Longrightarrow> aval a s <: aval' a S"
4.84 +by (induct a)(auto simp: rep_num' rep_plus' in_rep_up_iff lookup_def rep_st_def)
4.85 +
4.86 +fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
4.87 +"afilter (N n) a S = (if n <: a then S else Bot)" |
4.88 +"afilter (V x) a S = (case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow>
4.89 + let a' = lookup S x \<sqinter> a in
4.90 + if a' \<sqsubseteq> \<bottom> then Bot else Up(update S x a'))" |
4.91 +"afilter (Plus e1 e2) a S =
4.92 + (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
4.93 + in afilter e1 a1 (afilter e2 a2 S))"
4.94 +
4.95 +text{* The test for @{const Bot} in the @{const V}-case is important: @{const
4.96 +Bot} indicates that a variable has no possible values, i.e.\ that the current
4.97 +program point is unreachable. But then the abstract state should collapse to
4.98 +@{const bot}. Put differently, we maintain the invariant that in an abstract
4.99 +state all variables are mapped to non-@{const Bot} values. Otherwise the
4.100 +(pointwise) join of two abstract states, one of which contains @{const Bot}
4.101 +values, may produce too large a result, thus making the analysis less
4.102 +precise. *}
4.103 +
4.104 +
4.105 +fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a st up \<Rightarrow> 'a st up" where
4.106 +"bfilter (B bv) res S = (if bv=res then S else Bot)" |
4.107 +"bfilter (Not b) res S = bfilter b (\<not> res) S" |
4.108 +"bfilter (And b1 b2) res S =
4.109 + (if res then bfilter b1 True (bfilter b2 True S)
4.110 + else bfilter b1 False S \<squnion> bfilter b2 False S)" |
4.111 +"bfilter (Less e1 e2) res S =
4.112 + (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
4.113 + in afilter e1 res1 (afilter e2 res2 S))"
4.114 +
4.115 +lemma afilter_sound: "s <:up S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:up afilter e a S"
4.116 +proof(induction e arbitrary: a S)
4.117 + case N thus ?case by simp
4.118 +next
4.119 + case (V x)
4.120 + obtain S' where "S = Up S'" and "s <:f S'" using `s <:up S`
4.121 + by(auto simp: in_rep_up_iff)
4.122 + moreover hence "s x <: lookup S' x" by(simp add: rep_st_def)
4.123 + moreover have "s x <: a" using V by simp
4.124 + ultimately show ?case using V(1)
4.125 + by(simp add: lookup_update Let_def rep_st_def)
4.126 + (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
4.127 +next
4.128 + case (Plus e1 e2) thus ?case
4.129 + using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
4.130 + by (auto split: prod.split)
4.131 +qed
4.132 +
4.133 +lemma bfilter_sound: "s <:up S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:up bfilter b bv S"
4.134 +proof(induction b arbitrary: S bv)
4.135 + case B thus ?case by simp
4.136 +next
4.137 + case (Not b) thus ?case by simp
4.138 +next
4.139 + case (And b1 b2) thus ?case by(fastforce simp: in_rep_join_UpI)
4.140 +next
4.141 + case (Less e1 e2) thus ?case
4.142 + by (auto split: prod.split)
4.143 + (metis afilter_sound filter_less' aval'_sound Less)
4.144 +qed
4.145 +
4.146 +
4.147 +fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
4.148 +"step S (SKIP {P}) = (SKIP {S})" |
4.149 +"step S (x ::= e {P}) =
4.150 + x ::= e {case S of Bot \<Rightarrow> Bot
4.151 + | Up S \<Rightarrow> Up(update S x (aval' e (Up S)))}" |
4.152 +"step S (c1; c2) = step S c1; step (post c1) c2" |
4.153 +"step S (IF b THEN c1 ELSE c2 {P}) =
4.154 + (let c1' = step (bfilter b True S) c1; c2' = step (bfilter b False S) c2
4.155 + in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
4.156 +"step S ({Inv} WHILE b DO c {P}) =
4.157 + {S \<squnion> post c}
4.158 + WHILE b DO step (bfilter b True Inv) c
4.159 + {bfilter b False Inv}"
4.160 +
4.161 +lemma strip_step[simp]: "strip(step S c) = strip c"
4.162 +by(induct c arbitrary: S) (simp_all add: Let_def)
4.163 +
4.164 +
4.165 +definition AI :: "com \<Rightarrow> 'a st up acom" where
4.166 +"AI c = pfp (step \<top>) (\<bottom>\<^sub>c c)"
4.167 +
4.168 +
4.169 +subsubsection "Monotonicity"
4.170 +
4.171 +lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
4.172 +apply(cases S)
4.173 + apply simp
4.174 +apply(cases S')
4.175 + apply simp
4.176 +apply simp
4.177 +by(induction e) (auto simp: le_st_def lookup_def mono_plus')
4.178 +
4.179 +lemma mono_afilter: "r \<sqsubseteq> r' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> afilter e r S \<sqsubseteq> afilter e r' S'"
4.180 +apply(induction e arbitrary: r r' S S')
4.181 +apply(auto simp: Let_def split: up.splits prod.splits)
4.182 +apply (metis le_rep subsetD)
4.183 +apply(drule_tac x = "list" in mono_lookup)
4.184 +apply (metis mono_meet le_trans)
4.185 +apply (metis mono_meet mono_lookup mono_update le_trans)
4.186 +apply(metis mono_aval' mono_filter_plus'[simplified le_prod_def] fst_conv snd_conv)
4.187 +done
4.188 +
4.189 +lemma mono_bfilter: "S \<sqsubseteq> S' \<Longrightarrow> bfilter b r S \<sqsubseteq> bfilter b r S'"
4.190 +apply(induction b arbitrary: r S S')
4.191 +apply(auto simp: le_trans[OF _ join_ge1] le_trans[OF _ join_ge2] split: prod.splits)
4.192 +apply(metis mono_aval' mono_afilter mono_filter_less'[simplified le_prod_def] fst_conv snd_conv)
4.193 +done
4.194 +
4.195 +
4.196 +lemma post_le_post: "c \<sqsubseteq> c' \<Longrightarrow> post c \<sqsubseteq> post c'"
4.197 +by (induction c c' rule: le_acom.induct) simp_all
4.198 +
4.199 +lemma mono_step: "S \<sqsubseteq> S' \<Longrightarrow> c \<sqsubseteq> c' \<Longrightarrow> step S c \<sqsubseteq> step S' c'"
4.200 +apply(induction c c' arbitrary: S S' rule: le_acom.induct)
4.201 +apply (auto simp: post_le_post Let_def mono_bfilter mono_update mono_aval' le_join_disj
4.202 + split: up.split)
4.203 +done
4.204 +
4.205 +
4.206 +subsubsection "Soundness"
4.207 +
4.208 +lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
4.209 +by(simp add: rep_st_def lookup_update)
4.210 +
4.211 +lemma While_final_False: "(WHILE b DO c, s) \<Rightarrow> t \<Longrightarrow> \<not> bval b t"
4.212 +by(induct "WHILE b DO c" s t rule: big_step_induct) simp_all
4.213 +
4.214 +lemma step_sound:
4.215 + "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
4.216 +proof(induction c arbitrary: S s t)
4.217 + case SKIP thus ?case
4.218 + by simp (metis skipE up_fun_in_rep_le)
4.219 +next
4.220 + case Assign thus ?case
4.221 + apply (auto simp del: fun_upd_apply split: up.splits)
4.222 + by (metis aval'_sound fun_in_rep_le in_rep_update rep_up.simps(2))
4.223 +next
4.224 + case Semi thus ?case by simp blast
4.225 +next
4.226 + case (If b c1 c2 S0)
4.227 + show ?case
4.228 + proof cases
4.229 + assume "bval b s"
4.230 + with If.prems have 1: "step (bfilter b True S) c1 \<sqsubseteq> c1"
4.231 + and 2: "(strip c1, s) \<Rightarrow> t" and 3: "post c1 \<sqsubseteq> S0" by(auto simp: Let_def)
4.232 + from If.IH(1)[OF 1 2 bfilter_sound[OF `s <:up S`]] `bval b s` 3
4.233 + show ?thesis by simp (metis up_fun_in_rep_le)
4.234 + next
4.235 + assume "\<not> bval b s"
4.236 + with If.prems have 1: "step (bfilter b False S) c2 \<sqsubseteq> c2"
4.237 + and 2: "(strip c2, s) \<Rightarrow> t" and 3: "post c2 \<sqsubseteq> S0" by(auto simp: Let_def)
4.238 + from If.IH(2)[OF 1 2 bfilter_sound[OF `s <:up S`]] `\<not> bval b s` 3
4.239 + show ?thesis by simp (metis up_fun_in_rep_le)
4.240 + qed
4.241 +next
4.242 + case (While Inv b c P)
4.243 + from While.prems have inv: "step (bfilter b True Inv) c \<sqsubseteq> c"
4.244 + and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "bfilter b False Inv \<sqsubseteq> P"
4.245 + by(auto simp: Let_def)
4.246 + { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
4.247 + proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
4.248 + case WhileFalse thus ?case by simp
4.249 + next
4.250 + case (WhileTrue s1 s2 s3)
4.251 + from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` bfilter_sound[OF `s1 <:up Inv`]] `post c \<sqsubseteq> Inv`]] `bval b s1`
4.252 + show ?case by simp
4.253 + qed
4.254 + } note Inv = this
4.255 + from While.prems(2) have "(WHILE b DO strip c, s) \<Rightarrow> t" and "\<not> bval b t"
4.256 + by(auto dest: While_final_False)
4.257 + from Inv[OF this(1) up_fun_in_rep_le[OF `s <:up S` `S \<sqsubseteq> Inv`]]
4.258 + have "t <:up Inv" .
4.259 + from up_fun_in_rep_le[OF bfilter_sound[OF this] `bfilter b False Inv \<sqsubseteq> P`]
4.260 + show ?case using `\<not> bval b t` by simp
4.261 +qed
4.262 +
4.263 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)"
4.264 +by(fastforce simp: AI_def strip_pfp mono_def in_rep_Top_up
4.265 + intro: step_sound pfp mono_step[OF le_refl])
4.266 +
4.267 +end
4.268 +
4.269 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/IMP/Abs_Int1_ivl.thy Wed Sep 28 09:55:11 2011 +0200
5.3 @@ -0,0 +1,276 @@
5.4 +(* Author: Tobias Nipkow *)
5.5 +
5.6 +theory Abs_Int1_ivl
5.7 +imports Abs_Int1
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 +definition "rep_ivl i = (case i of
5.15 + I (Some l) (Some h) \<Rightarrow> {l..h} |
5.16 + I (Some l) None \<Rightarrow> {l..} |
5.17 + I None (Some h) \<Rightarrow> {..h} |
5.18 + I None None \<Rightarrow> UNIV)"
5.19 +
5.20 +definition "num_ivl n = I (Some n) (Some n)"
5.21 +
5.22 +instantiation option :: (plus)plus
5.23 +begin
5.24 +
5.25 +fun plus_option where
5.26 +"Some x + Some y = Some(x+y)" |
5.27 +"_ + _ = None"
5.28 +
5.29 +instance proof qed
5.30 +
5.31 +end
5.32 +
5.33 +definition empty where "empty = I (Some 1) (Some 0)"
5.34 +
5.35 +fun is_empty where
5.36 +"is_empty(I (Some l) (Some h)) = (h<l)" |
5.37 +"is_empty _ = False"
5.38 +
5.39 +lemma [simp]: "is_empty(I l h) =
5.40 + (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
5.41 +by(auto split:option.split)
5.42 +
5.43 +lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
5.44 +by(auto simp add: rep_ivl_def split: ivl.split option.split)
5.45 +
5.46 +definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
5.47 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
5.48 +
5.49 +instantiation ivl :: SL_top
5.50 +begin
5.51 +
5.52 +definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
5.53 +"le_option pos x y =
5.54 + (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
5.55 + | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
5.56 +
5.57 +fun le_aux where
5.58 +"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
5.59 +
5.60 +definition le_ivl where
5.61 +"i1 \<sqsubseteq> i2 =
5.62 + (if is_empty i1 then True else
5.63 + if is_empty i2 then False else le_aux i1 i2)"
5.64 +
5.65 +definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
5.66 +"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
5.67 +
5.68 +definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
5.69 +"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
5.70 +
5.71 +definition "i1 \<squnion> i2 =
5.72 + (if is_empty i1 then i2 else if is_empty i2 then i1
5.73 + else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
5.74 + I (min_option False l1 l2) (max_option True h1 h2))"
5.75 +
5.76 +definition "\<top> = I None None"
5.77 +
5.78 +instance
5.79 +proof
5.80 + case goal1 thus ?case
5.81 + by(cases x, simp add: le_ivl_def le_option_def split: option.split)
5.82 +next
5.83 + case goal2 thus ?case
5.84 + by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
5.85 +next
5.86 + case goal3 thus ?case
5.87 + 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.88 +next
5.89 + case goal4 thus ?case
5.90 + 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.91 +next
5.92 + case goal5 thus ?case
5.93 + 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.94 +next
5.95 + case goal6 thus ?case
5.96 + by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
5.97 +qed
5.98 +
5.99 +end
5.100 +
5.101 +
5.102 +instantiation ivl :: L_top_bot
5.103 +begin
5.104 +
5.105 +definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
5.106 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
5.107 + I (max_option False l1 l2) (min_option True h1 h2))"
5.108 +
5.109 +definition "\<bottom> = empty"
5.110 +
5.111 +instance
5.112 +proof
5.113 + case goal1 thus ?case
5.114 + 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.115 +next
5.116 + case goal2 thus ?case
5.117 + 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.118 +next
5.119 + case goal3 thus ?case
5.120 + 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.121 +next
5.122 + case goal4 show ?case by(cases x, simp add: bot_ivl_def empty_def le_ivl_def)
5.123 +qed
5.124 +
5.125 +end
5.126 +
5.127 +instantiation option :: (minus)minus
5.128 +begin
5.129 +
5.130 +fun minus_option where
5.131 +"Some x - Some y = Some(x-y)" |
5.132 +"_ - _ = None"
5.133 +
5.134 +instance proof qed
5.135 +
5.136 +end
5.137 +
5.138 +definition "minus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty else
5.139 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
5.140 +
5.141 +lemma rep_minus_ivl:
5.142 + "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
5.143 +by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
5.144 +
5.145 +
5.146 +definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
5.147 + i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
5.148 +
5.149 +fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
5.150 +"filter_less_ivl res (I l1 h1) (I l2 h2) =
5.151 + (if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else
5.152 + if res
5.153 + then (I l1 (min_option True h1 (h2 - Some 1)),
5.154 + I (max_option False (l1 + Some 1) l2) h2)
5.155 + else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
5.156 +
5.157 +interpretation Rep rep_ivl
5.158 +proof
5.159 + case goal1 thus ?case
5.160 + by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
5.161 +next
5.162 + case goal2 show ?case by(simp add: rep_ivl_def Top_ivl_def)
5.163 +qed
5.164 +
5.165 +interpretation Val_abs rep_ivl num_ivl plus_ivl
5.166 +proof
5.167 + case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
5.168 +next
5.169 + case goal2 thus ?case
5.170 + by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
5.171 +next
5.172 + case goal3 thus ?case
5.173 + by(auto simp: plus_ivl_def le_ivl_def le_option_def empty_def split: if_splits ivl.splits 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 +lemma mono_minus_ivl:
5.185 + "i1 \<sqsubseteq> i1' \<Longrightarrow> i2 \<sqsubseteq> i2' \<Longrightarrow> minus_ivl i1 i2 \<sqsubseteq> minus_ivl i1' i2'"
5.186 +apply(auto simp add: minus_ivl_def empty_def le_ivl_def le_option_def split: ivl.splits)
5.187 + apply(simp split: option.splits)
5.188 + apply(simp split: option.splits)
5.189 +apply(simp split: option.splits)
5.190 +done
5.191 +
5.192 +
5.193 +interpretation
5.194 + Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
5.195 +proof
5.196 + case goal1 thus ?case
5.197 + by(auto simp add: filter_plus_ivl_def)
5.198 + (metis rep_minus_ivl add_diff_cancel add_commute)+
5.199 +next
5.200 + case goal2 thus ?case
5.201 + by(cases a1, cases a2,
5.202 + auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
5.203 +next
5.204 + case goal3 thus ?case
5.205 + by(auto simp: filter_plus_ivl_def le_prod_def mono_meet mono_minus_ivl)
5.206 +next
5.207 + case goal4 thus ?case
5.208 + apply(cases a1, cases b1, cases a2, cases b2, auto simp: le_prod_def)
5.209 + by(auto simp add: empty_def le_ivl_def le_option_def min_option_def max_option_def split: option.splits)
5.210 +qed
5.211 +
5.212 +interpretation
5.213 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter 20)"
5.214 +defines afilter_ivl is afilter
5.215 +and bfilter_ivl is bfilter
5.216 +and step_ivl is step
5.217 +and AI_ivl is AI
5.218 +and aval_ivl is aval'
5.219 +proof qed (auto simp: iter_pfp strip_iter)
5.220 +
5.221 +definition "test1_ivl =
5.222 + ''y'' ::= N 7;
5.223 + IF Less (V ''x'') (V ''y'')
5.224 + THEN ''y'' ::= Plus (V ''y'') (V ''x'')
5.225 + ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
5.226 +
5.227 +translations
5.228 +"{i..j}" <= "CONST I (CONST Some i) (CONST Some j)"
5.229 +"{..j}" <= "CONST I (CONST None) (CONST Some j)"
5.230 +"{i..}" <= "CONST I (CONST Some i) (CONST None)"
5.231 +"CONST UNIV" <= "CONST I (CONST None) (CONST None)"
5.232 +
5.233 +value [code] "show_acom (AI_ivl test1_ivl)"
5.234 +
5.235 +value [code] "show_acom (AI_const test3_const)"
5.236 +value [code] "show_acom (AI_ivl test3_const)"
5.237 +
5.238 +value [code] "show_acom (AI_const test4_const)"
5.239 +value [code] "show_acom (AI_ivl test4_const)"
5.240 +
5.241 +value [code] "show_acom (AI_ivl test6_const)"
5.242 +
5.243 +definition "test2_ivl =
5.244 + WHILE Less (V ''x'') (N 100)
5.245 + DO ''x'' ::= Plus (V ''x'') (N 1)"
5.246 +
5.247 +value [code] "show_acom (AI_ivl test2_ivl)"
5.248 +
5.249 +definition "test3_ivl =
5.250 + ''x'' ::= N 7;
5.251 + WHILE Less (V ''x'') (N 100)
5.252 + DO ''x'' ::= Plus (V ''x'') (N 1)"
5.253 +
5.254 +value [code] "show_acom (AI_ivl test3_ivl)"
5.255 +value [code] "show_acom (((step_ivl \<top>)^^0) (\<bottom>\<^sub>c test3_ivl))"
5.256 +value [code] "show_acom (((step_ivl \<top>)^^1) (\<bottom>\<^sub>c test3_ivl))"
5.257 +value [code] "show_acom (((step_ivl \<top>)^^2) (\<bottom>\<^sub>c test3_ivl))"
5.258 +value [code] "show_acom (((step_ivl \<top>)^^3) (\<bottom>\<^sub>c test3_ivl))"
5.259 +value [code] "show_acom (((step_ivl \<top>)^^4) (\<bottom>\<^sub>c test3_ivl))"
5.260 +
5.261 +definition "test4_ivl =
5.262 + ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
5.263 + WHILE Less (V ''x'') (N 11)
5.264 + DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
5.265 +value [code] "show_acom(AI_ivl test4_ivl)"
5.266 +
5.267 +definition "test5_ivl =
5.268 + ''x'' ::= N 0; ''y'' ::= N 0;
5.269 + WHILE Less (V ''x'') (N 1001)
5.270 + DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
5.271 +value [code] "show_acom(AI_ivl test5_ivl)"
5.272 +
5.273 +text{* Nontermination not detected: *}
5.274 +definition "test6_ivl =
5.275 + ''x'' ::= N 0;
5.276 + WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
5.277 +value [code] "show_acom(AI_ivl test6_ivl)"
5.278 +
5.279 +end
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/IMP/Abs_Int2.thy Wed Sep 28 09:55:11 2011 +0200
6.3 @@ -0,0 +1,216 @@
6.4 +(* Author: Tobias Nipkow *)
6.5 +
6.6 +theory Abs_Int2
6.7 +imports Abs_Int1_ivl
6.8 +begin
6.9 +
6.10 +
6.11 +subsection "Widening and Narrowing"
6.12 +
6.13 +class WN = SL_top +
6.14 +fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
6.15 +assumes widen: "y \<sqsubseteq> x \<nabla> y"
6.16 +fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
6.17 +assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
6.18 +assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
6.19 +
6.20 +
6.21 +instantiation ivl :: WN
6.22 +begin
6.23 +
6.24 +definition "widen_ivl ivl1 ivl2 =
6.25 + ((*if is_empty ivl1 then ivl2 else
6.26 + if is_empty ivl2 then ivl1 else*)
6.27 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
6.28 + I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l1)
6.29 + (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h1))"
6.30 +
6.31 +definition "narrow_ivl ivl1 ivl2 =
6.32 + ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
6.33 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
6.34 + I (if l1 = None then l2 else l1)
6.35 + (if h1 = None then h2 else h1))"
6.36 +
6.37 +instance
6.38 +proof qed
6.39 + (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.40 +
6.41 +end
6.42 +
6.43 +instantiation st :: (WN)WN
6.44 +begin
6.45 +
6.46 +definition "widen_st F1 F2 =
6.47 + FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
6.48 +
6.49 +definition "narrow_st F1 F2 =
6.50 + FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
6.51 +
6.52 +instance
6.53 +proof
6.54 + case goal1 thus ?case
6.55 + by(simp add: widen_st_def le_st_def lookup_def widen)
6.56 +next
6.57 + case goal2 thus ?case
6.58 + by(auto simp: narrow_st_def le_st_def lookup_def narrow1)
6.59 +next
6.60 + case goal3 thus ?case
6.61 + by(auto simp: narrow_st_def le_st_def lookup_def narrow2)
6.62 +qed
6.63 +
6.64 +end
6.65 +
6.66 +instantiation up :: (WN)WN
6.67 +begin
6.68 +
6.69 +fun widen_up where
6.70 +"widen_up Bot x = x" |
6.71 +"widen_up x Bot = x" |
6.72 +"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
6.73 +
6.74 +fun narrow_up where
6.75 +"narrow_up Bot x = Bot" |
6.76 +"narrow_up x Bot = Bot" |
6.77 +"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
6.78 +
6.79 +instance
6.80 +proof
6.81 + case goal1 show ?case
6.82 + by(induct x y rule: widen_up.induct) (simp_all add: widen)
6.83 +next
6.84 + case goal2 thus ?case
6.85 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
6.86 +next
6.87 + case goal3 thus ?case
6.88 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
6.89 +qed
6.90 +
6.91 +end
6.92 +
6.93 +fun map2_acom :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
6.94 +"map2_acom f (SKIP {a1}) (SKIP {a2}) = (SKIP {f a1 a2})" |
6.95 +"map2_acom f (x ::= e {a1}) (x' ::= e' {a2}) = (x ::= e {f a1 a2})" |
6.96 +"map2_acom f (c1;c2) (c1';c2') = (map2_acom f c1 c1'; map2_acom f c2 c2')" |
6.97 +"map2_acom f (IF b THEN c1 ELSE c2 {a1}) (IF b' THEN c1' ELSE c2' {a2}) =
6.98 + (IF b THEN map2_acom f c1 c1' ELSE map2_acom f c2 c2' {f a1 a2})" |
6.99 +"map2_acom f ({a1} WHILE b DO c {a2}) ({a3} WHILE b' DO c' {a4}) =
6.100 + ({f a1 a3} WHILE b DO map2_acom f c c' {f a2 a4})"
6.101 +
6.102 +abbreviation widen_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<nabla>\<^sub>c" 65)
6.103 +where "widen_acom == map2_acom (op \<nabla>)"
6.104 +
6.105 +abbreviation narrow_acom :: "('a::WN)acom \<Rightarrow> 'a acom \<Rightarrow> 'a acom" (infix "\<triangle>\<^sub>c" 65)
6.106 +where "narrow_acom == map2_acom (op \<triangle>)"
6.107 +
6.108 +lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
6.109 +by(induct y x rule: le_acom.induct) (simp_all add: narrow1)
6.110 +
6.111 +lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
6.112 +by(induct y x rule: le_acom.induct) (simp_all add: narrow2)
6.113 +
6.114 +fun iter_up :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
6.115 +"iter_up f 0 x = \<top>\<^sub>c (strip x)" |
6.116 +"iter_up f (Suc n) x =
6.117 + (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla>\<^sub>c fx))"
6.118 +
6.119 +abbreviation
6.120 + iter_down :: "(('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> nat \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
6.121 +"iter_down f n x == ((\<lambda>x. x \<triangle>\<^sub>c f x)^^n) x"
6.122 +
6.123 +definition
6.124 + iter' :: "nat \<Rightarrow> nat \<Rightarrow> (('a::WN)acom \<Rightarrow> 'a acom) \<Rightarrow> 'a acom \<Rightarrow> 'a acom" where
6.125 +"iter' m n f x = iter_down f n (iter_up f m x)"
6.126 +
6.127 +lemma strip_map2_acom:
6.128 + "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
6.129 +by(induct f c1 c2 rule: map2_acom.induct) simp_all
6.130 +
6.131 +lemma strip_iter_up: assumes "\<forall>c. strip(f c) = strip c"
6.132 +shows "strip(iter_up f n c) = strip c"
6.133 +apply (induction n arbitrary: c)
6.134 + apply (metis iter_up.simps(1) strip_Top_acom snd_conv)
6.135 +apply (simp add:Let_def)
6.136 +by (metis assms strip_map2_acom)
6.137 +
6.138 +lemma iter_up_pfp: assumes "\<forall>c. strip(f c) = strip c"
6.139 +shows "f(iter_up f n c) \<sqsubseteq> iter_up f n c"
6.140 +apply (induction n arbitrary: c)
6.141 + apply(simp add: assms)
6.142 +apply (simp add:Let_def)
6.143 +done
6.144 +
6.145 +lemma strip_iter_down: assumes "\<forall>c. strip(f c) = strip c"
6.146 +shows "strip(iter_down f n c) = strip c"
6.147 +apply (induction n arbitrary: c)
6.148 + apply(simp)
6.149 +apply (simp add: strip_map2_acom assms)
6.150 +done
6.151 +
6.152 +lemma iter_down_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
6.153 +defines "x n == iter_down f n x0"
6.154 +shows "f(x n) \<sqsubseteq> x n"
6.155 +proof (induction n)
6.156 + case 0 show ?case by (simp add: x_def assms(2))
6.157 +next
6.158 + case (Suc n)
6.159 + have "f (x (Suc n)) = f(x n \<triangle>\<^sub>c f(x n))" by(simp add: x_def)
6.160 + also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2_acom[OF Suc]])
6.161 + also have "\<dots> \<sqsubseteq> x n \<triangle>\<^sub>c f(x n)" by(rule narrow1_acom[OF Suc])
6.162 + also have "\<dots> = x(Suc n)" by(simp add: x_def)
6.163 + finally show ?case .
6.164 +qed
6.165 +
6.166 +lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
6.167 +defines "x n == iter_down f n x0"
6.168 +shows "x n \<sqsubseteq> x0"
6.169 +proof (induction n)
6.170 + case 0 show ?case by(simp add: x_def)
6.171 +next
6.172 + case (Suc n)
6.173 + have "x(Suc n) = x n \<triangle>\<^sub>c f(x n)" by(simp add: x_def)
6.174 + also have "\<dots> \<sqsubseteq> x n" unfolding x_def
6.175 + by(rule narrow2_acom[OF iter_down_pfp[OF assms(1), OF assms(2)]])
6.176 + also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
6.177 + finally show ?case .
6.178 +qed
6.179 +
6.180 +
6.181 +lemma iter'_pfp: assumes "\<forall>c. strip (f c) = strip c" and "mono f"
6.182 +shows "f (iter' m n f c) \<sqsubseteq> iter' m n f c"
6.183 +using iter_up_pfp[of f] iter_down_pfp[of f]
6.184 +by(auto simp add: iter'_def Let_def assms)
6.185 +
6.186 +lemma strip_iter': assumes "\<forall>c. strip(f c) = strip c"
6.187 +shows "strip(iter' m n f c) = strip c"
6.188 +by(simp add: iter'_def strip_iter_down strip_iter_up assms)
6.189 +
6.190 +
6.191 +interpretation
6.192 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 20 5)"
6.193 +defines afilter_ivl' is afilter
6.194 +and bfilter_ivl' is bfilter
6.195 +and step_ivl' is step
6.196 +and AI_ivl' is AI
6.197 +and aval_ivl' is aval'
6.198 +proof qed (auto simp: iter'_pfp strip_iter')
6.199 +
6.200 +value [code] "show_acom (AI_ivl test3_ivl)"
6.201 +value [code] "show_acom (AI_ivl' test3_ivl)"
6.202 +
6.203 +definition "step_up n = ((\<lambda>c. c \<nabla>\<^sub>c step_ivl \<top> c)^^n)"
6.204 +definition "step_down n = ((\<lambda>c. c \<triangle>\<^sub>c step_ivl \<top> c)^^n)"
6.205 +
6.206 +value [code] "show_acom (step_up 1 (\<bottom>\<^sub>c test3_ivl))"
6.207 +value [code] "show_acom (step_up 2 (\<bottom>\<^sub>c test3_ivl))"
6.208 +value [code] "show_acom (step_up 3 (\<bottom>\<^sub>c test3_ivl))"
6.209 +value [code] "show_acom (step_up 4 (\<bottom>\<^sub>c test3_ivl))"
6.210 +value [code] "show_acom (step_up 5 (\<bottom>\<^sub>c test3_ivl))"
6.211 +value [code] "show_acom (step_down 1 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
6.212 +value [code] "show_acom (step_down 2 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
6.213 +value [code] "show_acom (step_down 3 (step_up 5 (\<bottom>\<^sub>c test3_ivl)))"
6.214 +
6.215 +value [code] "show_acom (AI_ivl' test4_ivl)"
6.216 +value [code] "show_acom (AI_ivl' test5_ivl)"
6.217 +value [code] "show_acom (AI_ivl' test6_ivl)"
6.218 +
6.219 +end
7.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy Wed Sep 28 08:51:55 2011 +0200
7.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
7.3 @@ -1,67 +0,0 @@
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 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy Wed Sep 28 08:51:55 2011 +0200
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,111 +0,0 @@
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 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy Wed Sep 28 08:51:55 2011 +0200
9.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
9.3 @@ -1,187 +0,0 @@
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 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy Wed Sep 28 08:51:55 2011 +0200
10.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
10.3 @@ -1,214 +0,0 @@
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 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy Wed Sep 28 08:51:55 2011 +0200
11.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
11.3 @@ -1,260 +0,0 @@
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 --- a/src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy Wed Sep 28 08:51:55 2011 +0200
12.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
12.3 @@ -1,207 +0,0 @@
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_Int_den0.thy Wed Sep 28 09:55:11 2011 +0200
13.3 @@ -0,0 +1,67 @@
13.4 +(* Author: Tobias Nipkow *)
13.5 +
13.6 +theory Abs_Int_den0
13.7 +imports Abs_State_den
13.8 +begin
13.9 +
13.10 +subsection "Computable Abstract Interpretation"
13.11 +
13.12 +text{* Abstract interpretation over type @{text astate} instead of
13.13 +functions. *}
13.14 +
13.15 +locale Abs_Int = Val_abs +
13.16 +fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate"
13.17 +assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
13.18 +assumes above: "x0 \<sqsubseteq> pfp f x0"
13.19 +begin
13.20 +
13.21 +fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where
13.22 +"aval' (N n) _ = num' n" |
13.23 +"aval' (V x) S = lookup S x" |
13.24 +"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
13.25 +
13.26 +abbreviation astate_in_rep (infix "<:" 50) where
13.27 +"s <: S == ALL x. s x <: lookup S x"
13.28 +
13.29 +lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
13.30 +by (metis in_mono le_astate_def le_rep lookup_def top)
13.31 +
13.32 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
13.33 +by (induct a) (auto simp: rep_num' rep_plus')
13.34 +
13.35 +
13.36 +fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
13.37 +"AI SKIP S = S" |
13.38 +"AI (x ::= a) S = update S x (aval' a S)" |
13.39 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
13.40 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
13.41 +"AI (WHILE b DO c) S = pfp (AI c) S"
13.42 +
13.43 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
13.44 +proof(induction c arbitrary: s t S0)
13.45 + case SKIP thus ?case by fastforce
13.46 +next
13.47 + case Assign thus ?case
13.48 + by (auto simp: lookup_update aval'_sound)
13.49 +next
13.50 + case Semi thus ?case by auto
13.51 +next
13.52 + case If thus ?case
13.53 + by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
13.54 +next
13.55 + case (While b c)
13.56 + let ?P = "pfp (AI c) S0"
13.57 + { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
13.58 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
13.59 + case WhileFalse thus ?case by simp
13.60 + next
13.61 + case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
13.62 + qed
13.63 + }
13.64 + with astate_in_rep_le[OF `s <: S0` above]
13.65 + show ?case by (metis While(2) AI.simps(5))
13.66 +qed
13.67 +
13.68 +end
13.69 +
13.70 +end
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy Wed Sep 28 09:55:11 2011 +0200
14.3 @@ -0,0 +1,111 @@
14.4 +(* Author: Tobias Nipkow *)
14.5 +
14.6 +theory Abs_Int_den0_const
14.7 +imports Abs_Int_den0
14.8 +begin
14.9 +
14.10 +subsection "Constant Propagation"
14.11 +
14.12 +datatype cval = Const val | Any
14.13 +
14.14 +fun rep_cval where
14.15 +"rep_cval (Const n) = {n}" |
14.16 +"rep_cval (Any) = UNIV"
14.17 +
14.18 +fun plus_cval where
14.19 +"plus_cval (Const m) (Const n) = Const(m+n)" |
14.20 +"plus_cval _ _ = Any"
14.21 +
14.22 +instantiation cval :: SL_top
14.23 +begin
14.24 +
14.25 +fun le_cval where
14.26 +"_ \<sqsubseteq> Any = True" |
14.27 +"Const n \<sqsubseteq> Const m = (n=m)" |
14.28 +"Any \<sqsubseteq> Const _ = False"
14.29 +
14.30 +fun join_cval where
14.31 +"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
14.32 +"_ \<squnion> _ = Any"
14.33 +
14.34 +definition "Top = Any"
14.35 +
14.36 +instance
14.37 +proof
14.38 + case goal1 thus ?case by (cases x) simp_all
14.39 +next
14.40 + case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
14.41 +next
14.42 + case goal3 thus ?case by(cases x, cases y, simp_all)
14.43 +next
14.44 + case goal4 thus ?case by(cases y, cases x, simp_all)
14.45 +next
14.46 + case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
14.47 +next
14.48 + case goal6 thus ?case by(simp add: Top_cval_def)
14.49 +qed
14.50 +
14.51 +end
14.52 +
14.53 +interpretation Rep rep_cval
14.54 +proof
14.55 + case goal1 thus ?case
14.56 + by(cases a, cases b, simp, simp, cases b, simp, simp)
14.57 +qed
14.58 +
14.59 +interpretation Val_abs rep_cval Const plus_cval
14.60 +proof
14.61 + case goal1 show ?case by simp
14.62 +next
14.63 + case goal2 thus ?case
14.64 + by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
14.65 +qed
14.66 +
14.67 +interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
14.68 +defines AI_const is AI
14.69 +and aval'_const is aval'
14.70 +proof qed (auto simp: iter'_pfp_above)
14.71 +
14.72 +text{* Straight line code: *}
14.73 +definition "test1_const =
14.74 + ''y'' ::= N 7;
14.75 + ''z'' ::= Plus (V ''y'') (N 2);
14.76 + ''y'' ::= Plus (V ''x'') (N 0)"
14.77 +
14.78 +text{* Conditional: *}
14.79 +definition "test2_const =
14.80 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
14.81 +
14.82 +text{* Conditional, test is ignored: *}
14.83 +definition "test3_const =
14.84 + ''x'' ::= N 42;
14.85 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
14.86 +
14.87 +text{* While: *}
14.88 +definition "test4_const =
14.89 + ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
14.90 +
14.91 +text{* While, test is ignored: *}
14.92 +definition "test5_const =
14.93 + ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
14.94 +
14.95 +text{* Iteration is needed: *}
14.96 +definition "test6_const =
14.97 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
14.98 + WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
14.99 +
14.100 +text{* More iteration would be needed: *}
14.101 +definition "test7_const =
14.102 + ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
14.103 + WHILE Less (V ''x'') (N 1)
14.104 + DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
14.105 +
14.106 +value [code] "list (AI_const test1_const Top)"
14.107 +value [code] "list (AI_const test2_const Top)"
14.108 +value [code] "list (AI_const test3_const Top)"
14.109 +value [code] "list (AI_const test4_const Top)"
14.110 +value [code] "list (AI_const test5_const Top)"
14.111 +value [code] "list (AI_const test6_const Top)"
14.112 +value [code] "list (AI_const test7_const Top)"
14.113 +
14.114 +end
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Wed Sep 28 09:55:11 2011 +0200
15.3 @@ -0,0 +1,187 @@
15.4 +(* Author: Tobias Nipkow *)
15.5 +
15.6 +header "Denotational Abstract Interpretation"
15.7 +
15.8 +theory Abs_Int_den0_fun
15.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
15.10 +begin
15.11 +
15.12 +subsection "Orderings"
15.13 +
15.14 +class preord =
15.15 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
15.16 +assumes le_refl[simp]: "x \<sqsubseteq> x"
15.17 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
15.18 +
15.19 +text{* Note: no antisymmetry. Allows implementations where some abstract
15.20 +element is implemented by two different values @{prop "x \<noteq> y"}
15.21 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
15.22 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
15.23 +*}
15.24 +
15.25 +class SL_top = preord +
15.26 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
15.27 +fixes Top :: "'a"
15.28 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
15.29 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
15.30 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
15.31 +and top[simp]: "x \<sqsubseteq> Top"
15.32 +begin
15.33 +
15.34 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
15.35 +by (metis join_ge1 join_ge2 join_least le_trans)
15.36 +
15.37 +fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
15.38 +"iter 0 f _ = Top" |
15.39 +"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
15.40 +
15.41 +lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
15.42 +apply (induction n arbitrary: x)
15.43 + apply (simp)
15.44 +apply (simp)
15.45 +done
15.46 +
15.47 +abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
15.48 +"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
15.49 +
15.50 +lemma iter'_pfp_above:
15.51 + "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
15.52 +using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
15.53 +
15.54 +text{* So much for soundness. But how good an approximation of the post-fixed
15.55 +point does @{const iter} yield? *}
15.56 +
15.57 +lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
15.58 +apply(induction n arbitrary: x)
15.59 + apply simp
15.60 +apply (auto)
15.61 + apply(metis funpow.simps(1) id_def)
15.62 +by (metis funpow.simps(2) funpow_swap1 o_apply)
15.63 +
15.64 +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
15.65 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
15.66 +
15.67 +lemma iter_least_pfp:
15.68 +assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
15.69 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
15.70 +proof-
15.71 + obtain k where "iter n f x0 = (f^^k) x0"
15.72 + using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
15.73 + moreover
15.74 + { fix n have "(f^^n) x0 \<sqsubseteq> p"
15.75 + proof(induction n)
15.76 + case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
15.77 + next
15.78 + case (Suc n) thus ?case
15.79 + by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
15.80 + qed
15.81 + } ultimately show ?thesis by simp
15.82 +qed
15.83 +
15.84 +end
15.85 +
15.86 +text{* The interface of abstract values: *}
15.87 +
15.88 +locale Rep =
15.89 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
15.90 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
15.91 +begin
15.92 +
15.93 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
15.94 +
15.95 +lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
15.96 +by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
15.97 +
15.98 +end
15.99 +
15.100 +locale Val_abs = Rep rep
15.101 + for rep :: "'a::SL_top \<Rightarrow> val set" +
15.102 +fixes num' :: "val \<Rightarrow> 'a"
15.103 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
15.104 +assumes rep_num': "rep(num' n) = {n}"
15.105 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
15.106 +
15.107 +
15.108 +instantiation "fun" :: (type, SL_top) SL_top
15.109 +begin
15.110 +
15.111 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
15.112 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
15.113 +definition "Top = (\<lambda>x. Top)"
15.114 +
15.115 +lemma join_apply[simp]:
15.116 + "(f \<squnion> g) x = f x \<squnion> g x"
15.117 +by (simp add: join_fun_def)
15.118 +
15.119 +instance
15.120 +proof
15.121 + case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
15.122 +qed (simp_all add: le_fun_def Top_fun_def)
15.123 +
15.124 +end
15.125 +
15.126 +subsection "Abstract Interpretation Abstractly"
15.127 +
15.128 +text{* Abstract interpretation over abstract values. Abstract states are
15.129 +simply functions. The post-fixed point finder is parameterized over. *}
15.130 +
15.131 +type_synonym 'a st = "name \<Rightarrow> 'a"
15.132 +
15.133 +locale Abs_Int_Fun = Val_abs +
15.134 +fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
15.135 +assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
15.136 +assumes above: "x \<sqsubseteq> pfp f x"
15.137 +begin
15.138 +
15.139 +fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
15.140 +"aval' (N n) _ = num' n" |
15.141 +"aval' (V x) S = S x" |
15.142 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
15.143 +
15.144 +abbreviation fun_in_rep (infix "<:" 50) where
15.145 +"f <: F == \<forall>x. f x <: F x"
15.146 +
15.147 +lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
15.148 +by (metis le_fun_def le_rep subsetD)
15.149 +
15.150 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
15.151 +by (induct a) (auto simp: rep_num' rep_plus')
15.152 +
15.153 +fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
15.154 +"AI SKIP S = S" |
15.155 +"AI (x ::= a) S = S(x := aval' a S)" |
15.156 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
15.157 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
15.158 +"AI (WHILE b DO c) S = pfp (AI c) S"
15.159 +
15.160 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
15.161 +proof(induction c arbitrary: s t S0)
15.162 + case SKIP thus ?case by fastforce
15.163 +next
15.164 + case Assign thus ?case by (auto simp: aval'_sound)
15.165 +next
15.166 + case Semi thus ?case by auto
15.167 +next
15.168 + case If thus ?case by(auto simp: in_rep_join)
15.169 +next
15.170 + case (While b c)
15.171 + let ?P = "pfp (AI c) S0"
15.172 + { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
15.173 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
15.174 + case WhileFalse thus ?case by simp
15.175 + next
15.176 + case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
15.177 + qed
15.178 + }
15.179 + with fun_in_rep_le[OF `s <: S0` above]
15.180 + show ?case by (metis While(2) AI.simps(5))
15.181 +qed
15.182 +
15.183 +end
15.184 +
15.185 +
15.186 +text{* Problem: not executable because of the comparison of abstract states,
15.187 +i.e. functions, in the post-fixedpoint computation. Need to implement
15.188 +abstract states concretely. *}
15.189 +
15.190 +end
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy Wed Sep 28 09:55:11 2011 +0200
16.3 @@ -0,0 +1,214 @@
16.4 +(* Author: Tobias Nipkow *)
16.5 +
16.6 +theory Abs_Int_den1
16.7 +imports Abs_Int_den0_const
16.8 +begin
16.9 +
16.10 +subsection "Backward Analysis of Expressions"
16.11 +
16.12 +class L_top_bot = SL_top +
16.13 +fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
16.14 +and Bot :: "'a"
16.15 +assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
16.16 +and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
16.17 +and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
16.18 +assumes bot[simp]: "Bot \<sqsubseteq> x"
16.19 +
16.20 +locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
16.21 +assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
16.22 +and rep_Bot: "rep Bot = {}"
16.23 +begin
16.24 +
16.25 +lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
16.26 +by (metis IntI inter_rep_subset_rep_meet set_mp)
16.27 +
16.28 +lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
16.29 +by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
16.30 +
16.31 +end
16.32 +
16.33 +
16.34 +locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
16.35 + for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
16.36 +fixes filter_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
16.37 +and filter_less' :: "bool \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
16.38 +assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') \<Longrightarrow>
16.39 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
16.40 +and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') \<Longrightarrow>
16.41 + n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
16.42 +
16.43 +datatype 'a up = bot | Up 'a
16.44 +
16.45 +instantiation up :: (SL_top)SL_top
16.46 +begin
16.47 +
16.48 +fun le_up where
16.49 +"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
16.50 +"bot \<sqsubseteq> y = True" |
16.51 +"Up _ \<sqsubseteq> bot = False"
16.52 +
16.53 +lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
16.54 +by (cases x) simp_all
16.55 +
16.56 +lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
16.57 +by (cases u) auto
16.58 +
16.59 +fun join_up where
16.60 +"Up x \<squnion> Up y = Up(x \<squnion> y)" |
16.61 +"bot \<squnion> y = y" |
16.62 +"x \<squnion> bot = x"
16.63 +
16.64 +lemma [simp]: "x \<squnion> bot = x"
16.65 +by (cases x) simp_all
16.66 +
16.67 +
16.68 +definition "Top = Up Top"
16.69 +
16.70 +instance proof
16.71 + case goal1 show ?case by(cases x, simp_all)
16.72 +next
16.73 + case goal2 thus ?case
16.74 + by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
16.75 +next
16.76 + case goal3 thus ?case by(cases x, simp, cases y, simp_all)
16.77 +next
16.78 + case goal4 thus ?case by(cases y, simp, cases x, simp_all)
16.79 +next
16.80 + case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
16.81 +next
16.82 + case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
16.83 +qed
16.84 +
16.85 +end
16.86 +
16.87 +
16.88 +locale Abs_Int1 = Val_abs1 +
16.89 +fixes pfp :: "('a astate up \<Rightarrow> 'a astate up) \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up"
16.90 +assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0"
16.91 +assumes above: "x0 \<sqsubseteq> pfp f x0"
16.92 +begin
16.93 +
16.94 +(* FIXME avoid duplicating this defn *)
16.95 +abbreviation astate_in_rep (infix "<:" 50) where
16.96 +"s <: S == ALL x. s x <: lookup S x"
16.97 +
16.98 +abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool" (infix "<::" 50) where
16.99 +"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
16.100 +
16.101 +lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
16.102 +apply auto
16.103 +by (metis in_mono le_astate_def le_rep lookup_def top)
16.104 +
16.105 +lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
16.106 +by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
16.107 +
16.108 +fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
16.109 +"aval' _ bot = Bot" |
16.110 +"aval' (N n) _ = num' n" |
16.111 +"aval' (V x) (Up S) = lookup S x" |
16.112 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
16.113 +
16.114 +lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
16.115 +by (induct a) (auto simp: rep_num' rep_plus')
16.116 +
16.117 +fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
16.118 +"afilter (N n) a S = (if n <: a then S else bot)" |
16.119 +"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
16.120 + let a' = lookup S x \<sqinter> a in
16.121 + if a' \<sqsubseteq> Bot then bot else Up(update S x a'))" |
16.122 +"afilter (Plus e1 e2) a S =
16.123 + (let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
16.124 + in afilter e1 a1 (afilter e2 a2 S))"
16.125 +
16.126 +text{* The test for @{const Bot} in the @{const V}-case is important: @{const
16.127 +Bot} indicates that a variable has no possible values, i.e.\ that the current
16.128 +program point is unreachable. But then the abstract state should collapse to
16.129 +@{const bot}. Put differently, we maintain the invariant that in an abstract
16.130 +state all variables are mapped to non-@{const Bot} values. Otherwise the
16.131 +(pointwise) join of two abstract states, one of which contains @{const Bot}
16.132 +values, may produce too large a result, thus making the analysis less
16.133 +precise. *}
16.134 +
16.135 +
16.136 +fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
16.137 +"bfilter (B bv) res S = (if bv=res then S else bot)" |
16.138 +"bfilter (Not b) res S = bfilter b (\<not> res) S" |
16.139 +"bfilter (And b1 b2) res S =
16.140 + (if res then bfilter b1 True (bfilter b2 True S)
16.141 + else bfilter b1 False S \<squnion> bfilter b2 False S)" |
16.142 +"bfilter (Less e1 e2) res S =
16.143 + (let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
16.144 + in afilter e1 res1 (afilter e2 res2 S))"
16.145 +
16.146 +lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
16.147 +proof(induction e arbitrary: a S)
16.148 + case N thus ?case by simp
16.149 +next
16.150 + case (V x)
16.151 + obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
16.152 + moreover hence "s x <: lookup S' x" by(simp)
16.153 + moreover have "s x <: a" using V by simp
16.154 + ultimately show ?case using V(1)
16.155 + by(simp add: lookup_update Let_def)
16.156 + (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
16.157 +next
16.158 + case (Plus e1 e2) thus ?case
16.159 + using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
16.160 + by (auto split: prod.split)
16.161 +qed
16.162 +
16.163 +lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
16.164 +proof(induction b arbitrary: S bv)
16.165 + case B thus ?case by simp
16.166 +next
16.167 + case (Not b) thus ?case by simp
16.168 +next
16.169 + case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
16.170 +next
16.171 + case (Less e1 e2) thus ?case
16.172 + by (auto split: prod.split)
16.173 + (metis afilter_sound filter_less' aval'_sound Less)
16.174 +qed
16.175 +
16.176 +fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
16.177 +"AI SKIP S = S" |
16.178 +"AI (x ::= a) S =
16.179 + (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
16.180 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
16.181 +"AI (IF b THEN c1 ELSE c2) S =
16.182 + AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
16.183 +"AI (WHILE b DO c) S =
16.184 + bfilter b False (pfp (\<lambda>S. AI c (bfilter b True S)) S)"
16.185 +
16.186 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
16.187 +proof(induction c arbitrary: s t S)
16.188 + case SKIP thus ?case by fastforce
16.189 +next
16.190 + case Assign thus ?case
16.191 + by (auto simp: lookup_update aval'_sound)
16.192 +next
16.193 + case Semi thus ?case by fastforce
16.194 +next
16.195 + case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
16.196 +next
16.197 + case (While b c)
16.198 + let ?P = "pfp (\<lambda>S. AI c (bfilter b True S)) S"
16.199 + { fix s t
16.200 + have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
16.201 + t <:: bfilter b False ?P"
16.202 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
16.203 + case WhileFalse thus ?case by(metis bfilter_sound)
16.204 + next
16.205 + case WhileTrue show ?case
16.206 + by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
16.207 + rule While.IH[OF WhileTrue(2)],
16.208 + rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
16.209 + qed
16.210 + }
16.211 + with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
16.212 + show ?case by simp
16.213 +qed
16.214 +
16.215 +end
16.216 +
16.217 +end
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy Wed Sep 28 09:55:11 2011 +0200
17.3 @@ -0,0 +1,260 @@
17.4 +(* Author: Tobias Nipkow *)
17.5 +
17.6 +theory Abs_Int_den1_ivl
17.7 +imports Abs_Int_den1
17.8 +begin
17.9 +
17.10 +subsection "Interval Analysis"
17.11 +
17.12 +datatype ivl = I "int option" "int option"
17.13 +
17.14 +text{* We assume an important invariant: arithmetic operations are never
17.15 +applied to empty intervals @{term"I (Some i) (Some j)"} with @{term"j <
17.16 +i"}. This avoids special cases. Why can we assume this? Because an empty
17.17 +interval of values for a variable means that the current program point is
17.18 +unreachable. But this should actually translate into the bottom state, not a
17.19 +state where some variables have empty intervals. *}
17.20 +
17.21 +definition "rep_ivl i =
17.22 + (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
17.23 + | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
17.24 +
17.25 +definition "num_ivl n = I (Some n) (Some n)"
17.26 +
17.27 +instantiation option :: (plus)plus
17.28 +begin
17.29 +
17.30 +fun plus_option where
17.31 +"Some x + Some y = Some(x+y)" |
17.32 +"_ + _ = None"
17.33 +
17.34 +instance proof qed
17.35 +
17.36 +end
17.37 +
17.38 +definition empty where "empty = I (Some 1) (Some 0)"
17.39 +
17.40 +fun is_empty where
17.41 +"is_empty(I (Some l) (Some h)) = (h<l)" |
17.42 +"is_empty _ = False"
17.43 +
17.44 +lemma [simp]: "is_empty(I l h) =
17.45 + (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
17.46 +by(auto split:option.split)
17.47 +
17.48 +lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
17.49 +by(auto simp add: rep_ivl_def split: ivl.split option.split)
17.50 +
17.51 +definition "plus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
17.52 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
17.53 +
17.54 +instantiation ivl :: SL_top
17.55 +begin
17.56 +
17.57 +definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
17.58 +"le_option pos x y =
17.59 + (case x of (Some i) \<Rightarrow> (case y of Some j \<Rightarrow> i\<le>j | None \<Rightarrow> pos)
17.60 + | None \<Rightarrow> (case y of Some j \<Rightarrow> \<not>pos | None \<Rightarrow> True))"
17.61 +
17.62 +fun le_aux where
17.63 +"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
17.64 +
17.65 +definition le_ivl where
17.66 +"i1 \<sqsubseteq> i2 =
17.67 + (if is_empty i1 then True else
17.68 + if is_empty i2 then False else le_aux i1 i2)"
17.69 +
17.70 +definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
17.71 +"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
17.72 +
17.73 +definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
17.74 +"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
17.75 +
17.76 +definition "i1 \<squnion> i2 =
17.77 + (if is_empty i1 then i2 else if is_empty i2 then i1
17.78 + else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
17.79 + I (min_option False l1 l2) (max_option True h1 h2))"
17.80 +
17.81 +definition "Top = I None None"
17.82 +
17.83 +instance
17.84 +proof
17.85 + case goal1 thus ?case
17.86 + by(cases x, simp add: le_ivl_def le_option_def split: option.split)
17.87 +next
17.88 + case goal2 thus ?case
17.89 + by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
17.90 +next
17.91 + case goal3 thus ?case
17.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)
17.93 +next
17.94 + case goal4 thus ?case
17.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)
17.96 +next
17.97 + case goal5 thus ?case
17.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)
17.99 +next
17.100 + case goal6 thus ?case
17.101 + by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
17.102 +qed
17.103 +
17.104 +end
17.105 +
17.106 +
17.107 +instantiation ivl :: L_top_bot
17.108 +begin
17.109 +
17.110 +definition "i1 \<sqinter> i2 = (if is_empty i1 \<or> is_empty i2 then empty else
17.111 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
17.112 + I (max_option False l1 l2) (min_option True h1 h2))"
17.113 +
17.114 +definition "Bot = empty"
17.115 +
17.116 +instance
17.117 +proof
17.118 + case goal1 thus ?case
17.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)
17.120 +next
17.121 + case goal2 thus ?case
17.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)
17.123 +next
17.124 + case goal3 thus ?case
17.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)
17.126 +next
17.127 + case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
17.128 +qed
17.129 +
17.130 +end
17.131 +
17.132 +instantiation option :: (minus)minus
17.133 +begin
17.134 +
17.135 +fun minus_option where
17.136 +"Some x - Some y = Some(x-y)" |
17.137 +"_ - _ = None"
17.138 +
17.139 +instance proof qed
17.140 +
17.141 +end
17.142 +
17.143 +definition "minus_ivl i1 i2 = ((*if is_empty i1 | is_empty i2 then empty else*)
17.144 + case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
17.145 +
17.146 +lemma rep_minus_ivl:
17.147 + "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
17.148 +by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
17.149 +
17.150 +
17.151 +definition "filter_plus_ivl i i1 i2 = ((*if is_empty i then empty else*)
17.152 + i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
17.153 +
17.154 +fun filter_less_ivl :: "bool \<Rightarrow> ivl \<Rightarrow> ivl \<Rightarrow> ivl * ivl" where
17.155 +"filter_less_ivl res (I l1 h1) (I l2 h2) =
17.156 + ((*if is_empty(I l1 h1) \<or> is_empty(I l2 h2) then (empty, empty) else*)
17.157 + if res
17.158 + then (I l1 (min_option True h1 (h2 - Some 1)),
17.159 + I (max_option False (l1 + Some 1) l2) h2)
17.160 + else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
17.161 +
17.162 +interpretation Rep rep_ivl
17.163 +proof
17.164 + case goal1 thus ?case
17.165 + by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
17.166 +qed
17.167 +
17.168 +interpretation Val_abs rep_ivl num_ivl plus_ivl
17.169 +proof
17.170 + case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
17.171 +next
17.172 + case goal2 thus ?case
17.173 + by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
17.174 +qed
17.175 +
17.176 +interpretation Rep1 rep_ivl
17.177 +proof
17.178 + case goal1 thus ?case
17.179 + by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
17.180 +next
17.181 + case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
17.182 +qed
17.183 +
17.184 +interpretation
17.185 + Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
17.186 +proof
17.187 + case goal1 thus ?case
17.188 + by(auto simp add: filter_plus_ivl_def)
17.189 + (metis rep_minus_ivl add_diff_cancel add_commute)+
17.190 +next
17.191 + case goal2 thus ?case
17.192 + by(cases a1, cases a2,
17.193 + auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
17.194 +qed
17.195 +
17.196 +interpretation
17.197 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
17.198 +defines afilter_ivl is afilter
17.199 +and bfilter_ivl is bfilter
17.200 +and AI_ivl is AI
17.201 +and aval_ivl is aval'
17.202 +proof qed (auto simp: iter'_pfp_above)
17.203 +
17.204 +
17.205 +fun list_up where
17.206 +"list_up bot = bot" |
17.207 +"list_up (Up x) = Up(list x)"
17.208 +
17.209 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
17.210 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
17.211 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
17.212 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
17.213 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
17.214 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
17.215 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
17.216 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
17.217 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
17.218 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
17.219 +
17.220 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
17.221 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
17.222 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
17.223 + (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
17.224 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
17.225 + (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
17.226 +
17.227 +definition "test_ivl1 =
17.228 + ''y'' ::= N 7;
17.229 + IF Less (V ''x'') (V ''y'')
17.230 + THEN ''y'' ::= Plus (V ''y'') (V ''x'')
17.231 + ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
17.232 +value [code] "list_up(AI_ivl test_ivl1 Top)"
17.233 +
17.234 +value "list_up (AI_ivl test3_const Top)"
17.235 +
17.236 +value "list_up (AI_ivl test5_const Top)"
17.237 +
17.238 +value "list_up (AI_ivl test6_const Top)"
17.239 +
17.240 +definition "test2_ivl =
17.241 + ''y'' ::= N 7;
17.242 + WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
17.243 +value [code] "list_up(AI_ivl test2_ivl Top)"
17.244 +
17.245 +definition "test3_ivl =
17.246 + ''x'' ::= N 0; ''y'' ::= N 100; ''z'' ::= Plus (V ''x'') (V ''y'');
17.247 + WHILE Less (V ''x'') (N 11)
17.248 + DO (''x'' ::= Plus (V ''x'') (N 1); ''y'' ::= Plus (V ''y'') (N -1))"
17.249 +value [code] "list_up(AI_ivl test3_ivl Top)"
17.250 +
17.251 +definition "test4_ivl =
17.252 + ''x'' ::= N 0; ''y'' ::= N 0;
17.253 + WHILE Less (V ''x'') (N 1001)
17.254 + DO (''y'' ::= V ''x''; ''x'' ::= Plus (V ''x'') (N 1))"
17.255 +value [code] "list_up(AI_ivl test4_ivl Top)"
17.256 +
17.257 +text{* Nontermination not detected: *}
17.258 +definition "test5_ivl =
17.259 + ''x'' ::= N 0;
17.260 + WHILE Less (V ''x'') (N 1) DO ''x'' ::= Plus (V ''x'') (N -1)"
17.261 +value [code] "list_up(AI_ivl test5_ivl Top)"
17.262 +
17.263 +end
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy Wed Sep 28 09:55:11 2011 +0200
18.3 @@ -0,0 +1,207 @@
18.4 +(* Author: Tobias Nipkow *)
18.5 +
18.6 +theory Abs_Int_den2
18.7 +imports Abs_Int_den1_ivl
18.8 +begin
18.9 +
18.10 +context preord
18.11 +begin
18.12 +
18.13 +definition mono where "mono f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
18.14 +
18.15 +lemma monoD: "mono f \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" by(simp add: mono_def)
18.16 +
18.17 +lemma mono_comp: "mono f \<Longrightarrow> mono g \<Longrightarrow> mono (g o f)"
18.18 +by(simp add: mono_def)
18.19 +
18.20 +declare le_trans[trans]
18.21 +
18.22 +end
18.23 +
18.24 +
18.25 +subsection "Widening and Narrowing"
18.26 +
18.27 +text{* Jumping to the trivial post-fixed point @{const Top} in case @{text k}
18.28 +rounds of iteration did not reach a post-fixed point (as in @{const iter}) is
18.29 +a trivial widening step. We generalise this idea and complement it with
18.30 +narrowing, a process to regain precision.
18.31 +
18.32 +Class @{text WN} makes some assumptions about the widening and narrowing
18.33 +operators. The assumptions serve two purposes. Together with a further
18.34 +assumption that certain chains become stationary, they permit to prove
18.35 +termination of the fixed point iteration, which we do not --- we limit the
18.36 +number of iterations as before. The second purpose of the narrowing
18.37 +assumptions is to prove that the narrowing iteration keeps on producing
18.38 +post-fixed points and that it goes down. However, this requires the function
18.39 +being iterated to be monotone. Unfortunately, abstract interpretation with
18.40 +widening is not monotone. Hence the (recursive) abstract interpretation of a
18.41 +loop body that again contains a loop may result in a non-monotone
18.42 +function. Therefore our narrowing iteration needs to check at every step
18.43 +that a post-fixed point is maintained, and we cannot prove that the precision
18.44 +increases. *}
18.45 +
18.46 +class WN = SL_top +
18.47 +fixes widen :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<nabla>" 65)
18.48 +assumes widen: "y \<sqsubseteq> x \<nabla> y"
18.49 +fixes narrow :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infix "\<triangle>" 65)
18.50 +assumes narrow1: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle> y"
18.51 +assumes narrow2: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle> y \<sqsubseteq> x"
18.52 +begin
18.53 +
18.54 +fun iter_up :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
18.55 +"iter_up f 0 x = Top" |
18.56 +"iter_up f (Suc n) x =
18.57 + (let fx = f x in if fx \<sqsubseteq> x then x else iter_up f n (x \<nabla> fx))"
18.58 +
18.59 +lemma iter_up_pfp: "f(iter_up f n x) \<sqsubseteq> iter_up f n x"
18.60 +apply (induction n arbitrary: x)
18.61 + apply (simp)
18.62 +apply (simp add: Let_def)
18.63 +done
18.64 +
18.65 +fun iter_down :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
18.66 +"iter_down f 0 x = x" |
18.67 +"iter_down f (Suc n) x =
18.68 + (let y = x \<triangle> f x in if f y \<sqsubseteq> y then iter_down f n y else x)"
18.69 +
18.70 +lemma iter_down_pfp: "f x \<sqsubseteq> x \<Longrightarrow> f(iter_down f n x) \<sqsubseteq> iter_down f n x"
18.71 +apply (induction n arbitrary: x)
18.72 + apply (simp)
18.73 +apply (simp add: Let_def)
18.74 +done
18.75 +
18.76 +definition iter' :: "nat \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
18.77 +"iter' m n f x =
18.78 + (let f' = (\<lambda>y. x \<squnion> f y) in iter_down f' n (iter_up f' m x))"
18.79 +
18.80 +lemma iter'_pfp_above:
18.81 +shows "f(iter' m n f x0) \<sqsubseteq> iter' m n f x0"
18.82 +and "x0 \<sqsubseteq> iter' m n f x0"
18.83 +using iter_up_pfp[of "\<lambda>x. x0 \<squnion> f x"] iter_down_pfp[of "\<lambda>x. x0 \<squnion> f x"]
18.84 +by(auto simp add: iter'_def Let_def)
18.85 +
18.86 +text{* This is how narrowing works on monotone functions: you just iterate. *}
18.87 +
18.88 +abbreviation iter_down_mono :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
18.89 +"iter_down_mono f n x == ((\<lambda>x. x \<triangle> f x)^^n) x"
18.90 +
18.91 +text{* Narrowing always yields a post-fixed point: *}
18.92 +
18.93 +lemma iter_down_mono_pfp: assumes "mono f" and "f x0 \<sqsubseteq> x0"
18.94 +defines "x n == iter_down_mono f n x0"
18.95 +shows "f(x n) \<sqsubseteq> x n"
18.96 +proof (induction n)
18.97 + case 0 show ?case by (simp add: x_def assms(2))
18.98 +next
18.99 + case (Suc n)
18.100 + have "f (x (Suc n)) = f(x n \<triangle> f(x n))" by(simp add: x_def)
18.101 + also have "\<dots> \<sqsubseteq> f(x n)" by(rule monoD[OF `mono f` narrow2[OF Suc]])
18.102 + also have "\<dots> \<sqsubseteq> x n \<triangle> f(x n)" by(rule narrow1[OF Suc])
18.103 + also have "\<dots> = x(Suc n)" by(simp add: x_def)
18.104 + finally show ?case .
18.105 +qed
18.106 +
18.107 +text{* Narrowing can only increase precision: *}
18.108 +
18.109 +lemma iter_down_down: assumes "mono f" and "f x0 \<sqsubseteq> x0"
18.110 +defines "x n == iter_down_mono f n x0"
18.111 +shows "x n \<sqsubseteq> x0"
18.112 +proof (induction n)
18.113 + case 0 show ?case by(simp add: x_def)
18.114 +next
18.115 + case (Suc n)
18.116 + have "x(Suc n) = x n \<triangle> f(x n)" by(simp add: x_def)
18.117 + also have "\<dots> \<sqsubseteq> x n" unfolding x_def
18.118 + by(rule narrow2[OF iter_down_mono_pfp[OF assms(1), OF assms(2)]])
18.119 + also have "\<dots> \<sqsubseteq> x0" by(rule Suc)
18.120 + finally show ?case .
18.121 +qed
18.122 +
18.123 +
18.124 +end
18.125 +
18.126 +
18.127 +instantiation ivl :: WN
18.128 +begin
18.129 +
18.130 +definition "widen_ivl ivl1 ivl2 =
18.131 + ((*if is_empty ivl1 then ivl2 else if is_empty ivl2 then ivl1 else*)
18.132 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
18.133 + I (if le_option False l2 l1 \<and> l2 \<noteq> l1 then None else l2)
18.134 + (if le_option True h1 h2 \<and> h1 \<noteq> h2 then None else h2))"
18.135 +
18.136 +definition "narrow_ivl ivl1 ivl2 =
18.137 + ((*if is_empty ivl1 \<or> is_empty ivl2 then empty else*)
18.138 + case (ivl1,ivl2) of (I l1 h1, I l2 h2) \<Rightarrow>
18.139 + I (if l1 = None then l2 else l1)
18.140 + (if h1 = None then h2 else h1))"
18.141 +
18.142 +instance
18.143 +proof qed
18.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)
18.145 +
18.146 +end
18.147 +
18.148 +instantiation astate :: (WN) WN
18.149 +begin
18.150 +
18.151 +definition "widen_astate F1 F2 =
18.152 + FunDom (\<lambda>x. fun F1 x \<nabla> fun F2 x) (inter_list (dom F1) (dom F2))"
18.153 +
18.154 +definition "narrow_astate F1 F2 =
18.155 + FunDom (\<lambda>x. fun F1 x \<triangle> fun F2 x) (inter_list (dom F1) (dom F2))"
18.156 +
18.157 +instance
18.158 +proof
18.159 + case goal1 thus ?case
18.160 + by(simp add: widen_astate_def le_astate_def lookup_def widen)
18.161 +next
18.162 + case goal2 thus ?case
18.163 + by(auto simp: narrow_astate_def le_astate_def lookup_def narrow1)
18.164 +next
18.165 + case goal3 thus ?case
18.166 + by(auto simp: narrow_astate_def le_astate_def lookup_def narrow2)
18.167 +qed
18.168 +
18.169 +end
18.170 +
18.171 +instantiation up :: (WN) WN
18.172 +begin
18.173 +
18.174 +fun widen_up where
18.175 +"widen_up bot x = x" |
18.176 +"widen_up x bot = x" |
18.177 +"widen_up (Up x) (Up y) = Up(x \<nabla> y)"
18.178 +
18.179 +fun narrow_up where
18.180 +"narrow_up bot x = bot" |
18.181 +"narrow_up x bot = bot" |
18.182 +"narrow_up (Up x) (Up y) = Up(x \<triangle> y)"
18.183 +
18.184 +instance
18.185 +proof
18.186 + case goal1 show ?case
18.187 + by(induct x y rule: widen_up.induct) (simp_all add: widen)
18.188 +next
18.189 + case goal2 thus ?case
18.190 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow1)
18.191 +next
18.192 + case goal3 thus ?case
18.193 + by(induct x y rule: narrow_up.induct) (simp_all add: narrow2)
18.194 +qed
18.195 +
18.196 +end
18.197 +
18.198 +interpretation
18.199 + Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
18.200 +defines afilter_ivl' is afilter
18.201 +and bfilter_ivl' is bfilter
18.202 +and AI_ivl' is AI
18.203 +and aval_ivl' is aval'
18.204 +proof qed (auto simp: iter'_pfp_above)
18.205 +
18.206 +value [code] "list_up(AI_ivl' test3_ivl Top)"
18.207 +value [code] "list_up(AI_ivl' test4_ivl Top)"
18.208 +value [code] "list_up(AI_ivl' test5_ivl Top)"
18.209 +
18.210 +end
19.1 --- a/src/HOL/IMP/Abs_Int_Den/Abs_State.thy Wed Sep 28 08:51:55 2011 +0200
19.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
19.3 @@ -1,50 +0,0 @@
19.4 -(* Author: Tobias Nipkow *)
19.5 -
19.6 -theory Abs_State
19.7 -imports Abs_Int0_fun
19.8 - "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
19.9 - (* Library import merely to allow string lists to be sorted for output *)
19.10 -begin
19.11 -
19.12 -subsection "Abstract State with Computable Ordering"
19.13 -
19.14 -text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
19.15 -
19.16 -datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
19.17 -
19.18 -fun "fun" where "fun (FunDom f _) = f"
19.19 -fun dom where "dom (FunDom _ A) = A"
19.20 -
19.21 -definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
19.22 -
19.23 -definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
19.24 -
19.25 -definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
19.26 -
19.27 -definition "update F x y =
19.28 - FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
19.29 -
19.30 -lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
19.31 -by(rule ext)(auto simp: lookup_def update_def)
19.32 -
19.33 -instantiation astate :: (SL_top) SL_top
19.34 -begin
19.35 -
19.36 -definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
19.37 -
19.38 -definition
19.39 -"join_astate F G =
19.40 - FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
19.41 -
19.42 -definition "Top = FunDom (\<lambda>x. Top) []"
19.43 -
19.44 -instance
19.45 -proof
19.46 - case goal2 thus ?case
19.47 - apply(auto simp: le_astate_def)
19.48 - by (metis lookup_def preord_class.le_trans top)
19.49 -qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
19.50 -
19.51 -end
19.52 -
19.53 -end
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy Wed Sep 28 09:55:11 2011 +0200
20.3 @@ -0,0 +1,50 @@
20.4 +(* Author: Tobias Nipkow *)
20.5 +
20.6 +theory Abs_State_den
20.7 +imports Abs_Int_den0_fun
20.8 + "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
20.9 + (* Library import merely to allow string lists to be sorted for output *)
20.10 +begin
20.11 +
20.12 +subsection "Abstract State with Computable Ordering"
20.13 +
20.14 +text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
20.15 +
20.16 +datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
20.17 +
20.18 +fun "fun" where "fun (FunDom f _) = f"
20.19 +fun dom where "dom (FunDom _ A) = A"
20.20 +
20.21 +definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
20.22 +
20.23 +definition "list S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
20.24 +
20.25 +definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
20.26 +
20.27 +definition "update F x y =
20.28 + FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
20.29 +
20.30 +lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
20.31 +by(rule ext)(auto simp: lookup_def update_def)
20.32 +
20.33 +instantiation astate :: (SL_top) SL_top
20.34 +begin
20.35 +
20.36 +definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
20.37 +
20.38 +definition
20.39 +"join_astate F G =
20.40 + FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
20.41 +
20.42 +definition "Top = FunDom (\<lambda>x. Top) []"
20.43 +
20.44 +instance
20.45 +proof
20.46 + case goal2 thus ?case
20.47 + apply(auto simp: le_astate_def)
20.48 + by (metis lookup_def preord_class.le_trans top)
20.49 +qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
20.50 +
20.51 +end
20.52 +
20.53 +end
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/IMP/Abs_State.thy Wed Sep 28 09:55:11 2011 +0200
21.3 @@ -0,0 +1,95 @@
21.4 +(* Author: Tobias Nipkow *)
21.5 +
21.6 +theory Abs_State
21.7 +imports Abs_Int0_fun
21.8 + "~~/src/HOL/Library/Char_ord" "~~/src/HOL/Library/List_lexord"
21.9 + (* Library import merely to allow string lists to be sorted for output *)
21.10 +begin
21.11 +
21.12 +subsection "Abstract State with Computable Ordering"
21.13 +
21.14 +text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
21.15 +
21.16 +datatype 'a st = FunDom "name \<Rightarrow> 'a" "name list"
21.17 +
21.18 +fun "fun" where "fun (FunDom f _) = f"
21.19 +fun dom where "dom (FunDom _ A) = A"
21.20 +
21.21 +definition [simp]: "inter_list xs ys = [x\<leftarrow>xs. x \<in> set ys]"
21.22 +
21.23 +definition "show_st S = [(x,fun S x). x \<leftarrow> sort(dom S)]"
21.24 +
21.25 +fun show_st_up where
21.26 +"show_st_up Bot = Bot" |
21.27 +"show_st_up (Up S) = Up(show_st S)"
21.28 +
21.29 +definition "show_acom = map_acom show_st_up"
21.30 +
21.31 +definition "lookup F x = (if x : set(dom F) then fun F x else \<top>)"
21.32 +
21.33 +definition "update F x y =
21.34 + FunDom ((fun F)(x:=y)) (if x \<in> set(dom F) then dom F else x # dom F)"
21.35 +
21.36 +lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
21.37 +by(rule ext)(auto simp: lookup_def update_def)
21.38 +
21.39 +definition "rep_st rep F = {f. \<forall>x. f x \<in> rep(lookup F x)}"
21.40 +
21.41 +instantiation st :: (SL_top) SL_top
21.42 +begin
21.43 +
21.44 +definition "le_st F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
21.45 +
21.46 +definition
21.47 +"join_st F G =
21.48 + FunDom (\<lambda>x. fun F x \<squnion> fun G x) (inter_list (dom F) (dom G))"
21.49 +
21.50 +definition "\<top> = FunDom (\<lambda>x. \<top>) []"
21.51 +
21.52 +instance
21.53 +proof
21.54 + case goal2 thus ?case
21.55 + apply(auto simp: le_st_def)
21.56 + by (metis lookup_def preord_class.le_trans top)
21.57 +qed (auto simp: le_st_def lookup_def join_st_def Top_st_def)
21.58 +
21.59 +end
21.60 +
21.61 +lemma mono_lookup: "F \<sqsubseteq> F' \<Longrightarrow> lookup F x \<sqsubseteq> lookup F' x"
21.62 +by(auto simp add: lookup_def le_st_def)
21.63 +
21.64 +lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
21.65 +by(auto simp add: le_st_def lookup_def update_def)
21.66 +
21.67 +context Rep
21.68 +begin
21.69 +
21.70 +abbreviation fun_in_rep :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st \<Rightarrow> bool" (infix "<:f" 50) where
21.71 +"s <:f S == s \<in> rep_st rep S"
21.72 +
21.73 +notation fun_in_rep (infix "<:\<^sub>f" 50)
21.74 +
21.75 +lemma fun_in_rep_le: "s <:f S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:f T"
21.76 +apply(auto simp add: rep_st_def le_st_def dest: le_rep)
21.77 +by (metis in_rep_Top le_rep lookup_def subsetD)
21.78 +
21.79 +abbreviation in_rep_up :: "(name \<Rightarrow> 'b) \<Rightarrow> 'a st up \<Rightarrow> bool" (infix "<:up" 50)
21.80 +where "s <:up S == s : rep_up (rep_st rep) S"
21.81 +
21.82 +notation (output) in_rep_up (infix "<:\<^sub>u\<^sub>p" 50)
21.83 +
21.84 +lemma up_fun_in_rep_le: "s <:up S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:up T"
21.85 +by (cases S) (auto intro:fun_in_rep_le)
21.86 +
21.87 +lemma in_rep_up_iff: "x <:up u \<longleftrightarrow> (\<exists>u'. u = Up u' \<and> x <:f u')"
21.88 +by (cases u) auto
21.89 +
21.90 +lemma in_rep_Top_fun: "s <:f \<top>"
21.91 +by(simp add: rep_st_def lookup_def Top_st_def)
21.92 +
21.93 +lemma in_rep_Top_up: "s <:up \<top>"
21.94 +by(simp add: Top_up_def in_rep_Top_fun)
21.95 +
21.96 +end
21.97 +
21.98 +end
22.1 --- a/src/HOL/IMP/ROOT.ML Wed Sep 28 08:51:55 2011 +0200
22.2 +++ b/src/HOL/IMP/ROOT.ML Wed Sep 28 09:55:11 2011 +0200
22.3 @@ -18,7 +18,8 @@
22.4 "Hoare_Examples",
22.5 "VC",
22.6 "HoareT",
22.7 - "Abs_Int_Den/Abs_Int2",
22.8 + "Abs_Int2",
22.9 + "Abs_Int_Den/Abs_Int_den2",
22.10 "Procs_Dyn_Vars_Dyn",
22.11 "Procs_Stat_Vars_Dyn",
22.12 "Procs_Stat_Vars_Stat",
23.1 --- a/src/HOL/IsaMakefile Wed Sep 28 08:51:55 2011 +0200
23.2 +++ b/src/HOL/IsaMakefile Wed Sep 28 09:55:11 2011 +0200
23.3 @@ -515,10 +515,10 @@
23.4
23.5 HOL-IMP: HOL $(OUT)/HOL-IMP
23.6
23.7 -$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int0_fun.thy \
23.8 - IMP/Abs_Int_Den/Abs_State.thy IMP/Abs_Int_Den/Abs_Int0.thy \
23.9 - IMP/Abs_Int_Den/Abs_Int0_const.thy IMP/Abs_Int_Den/Abs_Int1.thy \
23.10 - IMP/Abs_Int_Den/Abs_Int1_ivl.thy IMP/Abs_Int_Den/Abs_Int2.thy \
23.11 +$(OUT)/HOL-IMP: $(OUT)/HOL IMP/Abs_Int_Den/Abs_Int_den0_fun.thy \
23.12 + IMP/Abs_Int_Den/Abs_State_den.thy IMP/Abs_Int_Den/Abs_Int_den0.thy \
23.13 + IMP/Abs_Int_Den/Abs_Int_den0_const.thy IMP/Abs_Int_Den/Abs_Int_den1.thy \
23.14 + IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy IMP/Abs_Int_Den/Abs_Int_den2.thy \
23.15 IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy \
23.16 IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
23.17 IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \