1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy Wed Sep 28 09:55:11 2011 +0200
1.3 @@ -0,0 +1,187 @@
1.4 +(* Author: Tobias Nipkow *)
1.5 +
1.6 +header "Denotational Abstract Interpretation"
1.7 +
1.8 +theory Abs_Int_den0_fun
1.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
1.10 +begin
1.11 +
1.12 +subsection "Orderings"
1.13 +
1.14 +class preord =
1.15 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
1.16 +assumes le_refl[simp]: "x \<sqsubseteq> x"
1.17 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
1.18 +
1.19 +text{* Note: no antisymmetry. Allows implementations where some abstract
1.20 +element is implemented by two different values @{prop "x \<noteq> y"}
1.21 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
1.22 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
1.23 +*}
1.24 +
1.25 +class SL_top = preord +
1.26 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
1.27 +fixes Top :: "'a"
1.28 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
1.29 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
1.30 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
1.31 +and top[simp]: "x \<sqsubseteq> Top"
1.32 +begin
1.33 +
1.34 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
1.35 +by (metis join_ge1 join_ge2 join_least le_trans)
1.36 +
1.37 +fun iter :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.38 +"iter 0 f _ = Top" |
1.39 +"iter (Suc n) f x = (if f x \<sqsubseteq> x then x else iter n f (f x))"
1.40 +
1.41 +lemma iter_pfp: "f(iter n f x) \<sqsubseteq> iter n f x"
1.42 +apply (induction n arbitrary: x)
1.43 + apply (simp)
1.44 +apply (simp)
1.45 +done
1.46 +
1.47 +abbreviation iter' :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
1.48 +"iter' n f x0 == iter n (\<lambda>x. x0 \<squnion> f x) x0"
1.49 +
1.50 +lemma iter'_pfp_above:
1.51 + "f(iter' n f x0) \<sqsubseteq> iter' n f x0" "x0 \<sqsubseteq> iter' n f x0"
1.52 +using iter_pfp[of "\<lambda>x. x0 \<squnion> f x"] by auto
1.53 +
1.54 +text{* So much for soundness. But how good an approximation of the post-fixed
1.55 +point does @{const iter} yield? *}
1.56 +
1.57 +lemma iter_funpow: "iter n f x \<noteq> Top \<Longrightarrow> \<exists>k. iter n f x = (f^^k) x"
1.58 +apply(induction n arbitrary: x)
1.59 + apply simp
1.60 +apply (auto)
1.61 + apply(metis funpow.simps(1) id_def)
1.62 +by (metis funpow.simps(2) funpow_swap1 o_apply)
1.63 +
1.64 +text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
1.65 +post-fixed point above @{text x0}, unless it yields @{text Top}. *}
1.66 +
1.67 +lemma iter_least_pfp:
1.68 +assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "iter n f x0 \<noteq> Top"
1.69 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "iter n f x0 \<sqsubseteq> p"
1.70 +proof-
1.71 + obtain k where "iter n f x0 = (f^^k) x0"
1.72 + using iter_funpow[OF `iter n f x0 \<noteq> Top`] by blast
1.73 + moreover
1.74 + { fix n have "(f^^n) x0 \<sqsubseteq> p"
1.75 + proof(induction n)
1.76 + case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
1.77 + next
1.78 + case (Suc n) thus ?case
1.79 + by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
1.80 + qed
1.81 + } ultimately show ?thesis by simp
1.82 +qed
1.83 +
1.84 +end
1.85 +
1.86 +text{* The interface of abstract values: *}
1.87 +
1.88 +locale Rep =
1.89 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
1.90 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
1.91 +begin
1.92 +
1.93 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
1.94 +
1.95 +lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
1.96 +by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
1.97 +
1.98 +end
1.99 +
1.100 +locale Val_abs = Rep rep
1.101 + for rep :: "'a::SL_top \<Rightarrow> val set" +
1.102 +fixes num' :: "val \<Rightarrow> 'a"
1.103 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.104 +assumes rep_num': "rep(num' n) = {n}"
1.105 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
1.106 +
1.107 +
1.108 +instantiation "fun" :: (type, SL_top) SL_top
1.109 +begin
1.110 +
1.111 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
1.112 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
1.113 +definition "Top = (\<lambda>x. Top)"
1.114 +
1.115 +lemma join_apply[simp]:
1.116 + "(f \<squnion> g) x = f x \<squnion> g x"
1.117 +by (simp add: join_fun_def)
1.118 +
1.119 +instance
1.120 +proof
1.121 + case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
1.122 +qed (simp_all add: le_fun_def Top_fun_def)
1.123 +
1.124 +end
1.125 +
1.126 +subsection "Abstract Interpretation Abstractly"
1.127 +
1.128 +text{* Abstract interpretation over abstract values. Abstract states are
1.129 +simply functions. The post-fixed point finder is parameterized over. *}
1.130 +
1.131 +type_synonym 'a st = "name \<Rightarrow> 'a"
1.132 +
1.133 +locale Abs_Int_Fun = Val_abs +
1.134 +fixes pfp :: "('a st \<Rightarrow> 'a st) \<Rightarrow> 'a st \<Rightarrow> 'a st"
1.135 +assumes pfp: "f(pfp f x) \<sqsubseteq> pfp f x"
1.136 +assumes above: "x \<sqsubseteq> pfp f x"
1.137 +begin
1.138 +
1.139 +fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.140 +"aval' (N n) _ = num' n" |
1.141 +"aval' (V x) S = S x" |
1.142 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
1.143 +
1.144 +abbreviation fun_in_rep (infix "<:" 50) where
1.145 +"f <: F == \<forall>x. f x <: F x"
1.146 +
1.147 +lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
1.148 +by (metis le_fun_def le_rep subsetD)
1.149 +
1.150 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
1.151 +by (induct a) (auto simp: rep_num' rep_plus')
1.152 +
1.153 +fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
1.154 +"AI SKIP S = S" |
1.155 +"AI (x ::= a) S = S(x := aval' a S)" |
1.156 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
1.157 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
1.158 +"AI (WHILE b DO c) S = pfp (AI c) S"
1.159 +
1.160 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
1.161 +proof(induction c arbitrary: s t S0)
1.162 + case SKIP thus ?case by fastforce
1.163 +next
1.164 + case Assign thus ?case by (auto simp: aval'_sound)
1.165 +next
1.166 + case Semi thus ?case by auto
1.167 +next
1.168 + case If thus ?case by(auto simp: in_rep_join)
1.169 +next
1.170 + case (While b c)
1.171 + let ?P = "pfp (AI c) S0"
1.172 + { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
1.173 + proof(induction "WHILE b DO c" s t rule: big_step_induct)
1.174 + case WhileFalse thus ?case by simp
1.175 + next
1.176 + case WhileTrue thus ?case by(metis While.IH pfp fun_in_rep_le)
1.177 + qed
1.178 + }
1.179 + with fun_in_rep_le[OF `s <: S0` above]
1.180 + show ?case by (metis While(2) AI.simps(5))
1.181 +qed
1.182 +
1.183 +end
1.184 +
1.185 +
1.186 +text{* Problem: not executable because of the comparison of abstract states,
1.187 +i.e. functions, in the post-fixedpoint computation. Need to implement
1.188 +abstract states concretely. *}
1.189 +
1.190 +end