Added Abstract Interpretation theories
authornipkow
Fri Sep 02 19:25:18 2011 +0200 (2011-09-02 ago)
changeset 4465622bbd0d1b943
parent 44648 897f32a827f2
child 44657 17dbd9d9db38
Added Abstract Interpretation theories
src/HOL/IMP/AbsInt0.thy
src/HOL/IMP/AbsInt0_const.thy
src/HOL/IMP/AbsInt0_fun.thy
src/HOL/IMP/AbsInt1.thy
src/HOL/IMP/AbsInt1_ivl.thy
src/HOL/IMP/Astate.thy
src/HOL/IMP/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/IMP/AbsInt0.thy	Fri Sep 02 19:25:18 2011 +0200
     1.3 @@ -0,0 +1,66 @@
     1.4 +(* Author: Tobias Nipkow *)
     1.5 +
     1.6 +theory AbsInt0
     1.7 +imports Astate
     1.8 +begin
     1.9 +
    1.10 +subsection "Computable Abstract Interpretation"
    1.11 +
    1.12 +text{* Abstract interpretation over type @{text astate} instead of
    1.13 +functions. *}
    1.14 +
    1.15 +locale Abs_Int = Val_abs
    1.16 +begin
    1.17 +
    1.18 +fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a"  ("aval\<^isup>#") where
    1.19 +"aval' (N n) _ = num' n" |
    1.20 +"aval' (V x) S = lookup S x" |
    1.21 +"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"
    1.22 +
    1.23 +abbreviation astate_in_rep (infix "<:" 50) where
    1.24 +"s <: S == ALL x. s x <: lookup S x"
    1.25 +
    1.26 +lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
    1.27 +by (metis in_mono le_astate_def le_rep lookup_def top)
    1.28 +
    1.29 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
    1.30 +by (induct a) (auto simp: rep_num' rep_plus')
    1.31 +
    1.32 +
    1.33 +fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where
    1.34 +"AI SKIP S = S" |
    1.35 +"AI (x ::= a) S = update S x (aval' a S)" |
    1.36 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
    1.37 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
    1.38 +"AI (WHILE b DO c) S = pfp_above (AI c) S"
    1.39 +
    1.40 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
    1.41 +proof(induct c arbitrary: s t S0)
    1.42 +  case SKIP thus ?case by fastsimp
    1.43 +next
    1.44 +  case Assign thus ?case
    1.45 +    by (auto simp: lookup_update aval'_sound)
    1.46 +next
    1.47 +  case Semi thus ?case by auto
    1.48 +next
    1.49 +  case If thus ?case
    1.50 +    by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
    1.51 +next
    1.52 +  case (While b c)
    1.53 +  let ?P = "pfp_above (AI c) S0"
    1.54 +  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
    1.55 +    by(simp_all add: SL_top_class.pfp_above_pfp)
    1.56 +  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
    1.57 +    proof(induct "WHILE b DO c" s t rule: big_step_induct)
    1.58 +      case WhileFalse thus ?case by simp
    1.59 +    next
    1.60 +      case WhileTrue thus ?case using While.hyps pfp astate_in_rep_le by metis
    1.61 +    qed
    1.62 +  }
    1.63 +  with astate_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
    1.64 +  show ?case by (metis While(2) AI.simps(5))
    1.65 +qed
    1.66 +
    1.67 +end
    1.68 +
    1.69 +end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/IMP/AbsInt0_const.thy	Fri Sep 02 19:25:18 2011 +0200
     2.3 @@ -0,0 +1,110 @@
     2.4 +(* Author: Tobias Nipkow *)
     2.5 +
     2.6 +theory AbsInt0_const
     2.7 +imports AbsInt0
     2.8 +begin
     2.9 +
    2.10 +subsection "Constant Propagation"
    2.11 +
    2.12 +datatype cval = Const val | Any
    2.13 +
    2.14 +fun rep_cval where
    2.15 +"rep_cval (Const n) = {n}" |
    2.16 +"rep_cval (Any) = UNIV"
    2.17 +
    2.18 +fun plus_cval where
    2.19 +"plus_cval (Const m) (Const n) = Const(m+n)" |
    2.20 +"plus_cval _ _ = Any"
    2.21 +
    2.22 +instantiation cval :: SL_top
    2.23 +begin
    2.24 +
    2.25 +fun le_cval where
    2.26 +"_ \<sqsubseteq> Any = True" |
    2.27 +"Const n \<sqsubseteq> Const m = (n=m)" |
    2.28 +"Any \<sqsubseteq> Const _ = False"
    2.29 +
    2.30 +fun join_cval where
    2.31 +"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
    2.32 +"_ \<squnion> _ = Any"
    2.33 +
    2.34 +definition "Top = Any"
    2.35 +
    2.36 +instance
    2.37 +proof
    2.38 +  case goal1 thus ?case by (cases x) simp_all
    2.39 +next
    2.40 +  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
    2.41 +next
    2.42 +  case goal3 thus ?case by(cases x, cases y, simp_all)
    2.43 +next
    2.44 +  case goal4 thus ?case by(cases y, cases x, simp_all)
    2.45 +next
    2.46 +  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
    2.47 +next
    2.48 +  case goal6 thus ?case by(simp add: Top_cval_def)
    2.49 +qed
    2.50 +
    2.51 +end
    2.52 +
    2.53 +interpretation Rep rep_cval
    2.54 +proof
    2.55 +  case goal1 thus ?case
    2.56 +    by(cases a, cases b, simp, simp, cases b, simp, simp)
    2.57 +qed
    2.58 +
    2.59 +interpretation Val_abs rep_cval Const plus_cval
    2.60 +proof
    2.61 +  case goal1 show ?case by simp
    2.62 +next
    2.63 +  case goal2 thus ?case
    2.64 +    by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
    2.65 +qed
    2.66 +
    2.67 +interpretation Abs_Int rep_cval Const plus_cval
    2.68 +defines AI_const is AI
    2.69 +and aval'_const is aval'
    2.70 +..
    2.71 +
    2.72 +text{* Straight line code: *}
    2.73 +definition "test1_const =
    2.74 + ''y'' ::= N 7;
    2.75 + ''z'' ::= Plus (V ''y'') (N 2);
    2.76 + ''y'' ::= Plus (V ''x'') (N 0)"
    2.77 +value [code] "list (AI_const test1_const Top)"
    2.78 +
    2.79 +text{* Conditional: *}
    2.80 +definition "test2_const =
    2.81 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
    2.82 +value "list (AI_const test2_const Top)"
    2.83 +
    2.84 +text{* Conditional, test is ignored: *}
    2.85 +definition "test3_const =
    2.86 + ''x'' ::= N 42;
    2.87 + IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
    2.88 +value "list (AI_const test3_const Top)"
    2.89 +
    2.90 +text{* While: *}
    2.91 +definition "test4_const =
    2.92 + ''x'' ::= N 0; WHILE B True DO ''x'' ::= N 0"
    2.93 +value [code] "list (AI_const test4_const Top)"
    2.94 +
    2.95 +text{* While, test is ignored: *}
    2.96 +definition "test5_const =
    2.97 + ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
    2.98 +value [code] "list (AI_const test5_const Top)"
    2.99 +
   2.100 +text{* Iteration is needed: *}
   2.101 +definition "test6_const =
   2.102 +  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
   2.103 +  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
   2.104 +value [code] "list (AI_const test6_const Top)"
   2.105 +
   2.106 +text{* More iteration would be needed: *}
   2.107 +definition "test7_const =
   2.108 +  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
   2.109 +  WHILE B True DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
   2.110 +value [code] "list (AI_const test7_const Top)"
   2.111 +
   2.112 +
   2.113 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/IMP/AbsInt0_fun.thy	Fri Sep 02 19:25:18 2011 +0200
     3.3 @@ -0,0 +1,213 @@
     3.4 +(* Author: Tobias Nipkow *)
     3.5 +
     3.6 +header "Abstract Interpretation"
     3.7 +
     3.8 +theory AbsInt0_fun
     3.9 +imports "~~/src/HOL/ex/Interpretation_with_Defs" Big_Step
    3.10 +begin
    3.11 +
    3.12 +subsection "Orderings"
    3.13 +
    3.14 +class preord =
    3.15 +fixes le :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<sqsubseteq>" 50)
    3.16 +assumes le_refl[simp]: "x \<sqsubseteq> x"
    3.17 +and le_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    3.18 +
    3.19 +text{* Note: no antisymmetry. Allows implementations where some abstract
    3.20 +element is implemented by two different values @{prop "x \<noteq> y"}
    3.21 +such that @{prop"x \<sqsubseteq> y"} and @{prop"y \<sqsubseteq> x"}. Antisymmetry is not
    3.22 +needed because we never compare elements for equality but only for @{text"\<sqsubseteq>"}.
    3.23 +*}
    3.24 +
    3.25 +class SL_top = preord +
    3.26 +fixes join :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
    3.27 +fixes Top :: "'a"
    3.28 +assumes join_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
    3.29 +and join_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
    3.30 +and join_least: "x \<sqsubseteq> z \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<squnion> y \<sqsubseteq> z"
    3.31 +and top[simp]: "x \<sqsubseteq> Top"
    3.32 +begin
    3.33 +
    3.34 +lemma join_le_iff[simp]: "x \<squnion> y \<sqsubseteq> z \<longleftrightarrow> x \<sqsubseteq> z \<and> y \<sqsubseteq> z"
    3.35 +by (metis join_ge1 join_ge2 join_least le_trans)
    3.36 +
    3.37 +fun bpfp where
    3.38 +"bpfp f 0 _ = Top" |
    3.39 +"bpfp f (Suc n) x = (if f x \<sqsubseteq> x then x else bpfp f n (f x))"
    3.40 +
    3.41 +definition "pfp f = bpfp f 3"
    3.42 +
    3.43 +lemma postfixedpoint: "f(bpfp f n x) \<sqsubseteq> bpfp f n x"
    3.44 +apply (induct n arbitrary: x)
    3.45 + apply (simp)
    3.46 +apply (simp)
    3.47 +done
    3.48 +
    3.49 +lemma bpfp_funpow: "bpfp f n x \<noteq> Top \<Longrightarrow> EX k. bpfp f n x = (f^^k) x"
    3.50 +apply(induct n arbitrary: x)
    3.51 +apply simp
    3.52 +apply simp
    3.53 +apply (auto)
    3.54 +apply(rule_tac x=0 in exI)
    3.55 +apply simp
    3.56 +by (metis funpow.simps(2) funpow_swap1 o_apply)
    3.57 +
    3.58 +lemma pfp_funpow: "pfp f x \<noteq> Top \<Longrightarrow> EX k. pfp f x = (f^^k) x"
    3.59 +by(simp add: pfp_def bpfp_funpow)
    3.60 +
    3.61 +abbreviation (input) lift (infix "\<up>" 65) where "f\<up>x0 == (%x. x0 \<squnion> f x)"
    3.62 +
    3.63 +definition "pfp_above f x0 = pfp (f\<up>x0) x0"
    3.64 +
    3.65 +lemma pfp_above_pfp:
    3.66 +shows "f(pfp_above f x0) \<sqsubseteq> pfp_above f x0" and "x0 \<sqsubseteq> pfp_above f x0"
    3.67 +using postfixedpoint[of "lift f x0"]
    3.68 +by(auto simp add: pfp_above_def pfp_def)
    3.69 +
    3.70 +lemma least_pfp:
    3.71 +assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
    3.72 +and "f p \<sqsubseteq> p" and "x0 \<sqsubseteq> p" shows "pfp_above f x0 \<sqsubseteq> p"
    3.73 +proof-
    3.74 +  let ?F = "lift f x0"
    3.75 +  obtain k where "pfp_above f x0 = (?F^^k) x0"
    3.76 +    using pfp_funpow `pfp_above f x0 \<noteq> Top`
    3.77 +    by(fastsimp simp add: pfp_above_def)
    3.78 +  moreover
    3.79 +  { fix n have "(?F^^n) x0 \<sqsubseteq> p"
    3.80 +    proof(induct n)
    3.81 +      case 0 show ?case by(simp add: `x0 \<sqsubseteq> p`)
    3.82 +    next
    3.83 +      case (Suc n) thus ?case
    3.84 +        by (simp add: `x0 \<sqsubseteq> p`)(metis Suc assms(3) le_trans mono)
    3.85 +    qed
    3.86 +  } ultimately show ?thesis by simp
    3.87 +qed
    3.88 +
    3.89 +lemma chain: assumes "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
    3.90 +shows "((f\<up>x0)^^i) x0 \<sqsubseteq> ((f\<up>x0)^^(i+1)) x0"
    3.91 +apply(induct i)
    3.92 + apply simp
    3.93 +apply simp
    3.94 +by (metis assms join_ge2 le_trans)
    3.95 +
    3.96 +lemma pfp_almost_fp:
    3.97 +assumes mono: "!!x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y" and "pfp_above f x0 \<noteq> Top"
    3.98 +shows "pfp_above f x0 \<sqsubseteq> x0 \<squnion> f(pfp_above f x0)"
    3.99 +proof-
   3.100 +  let ?p = "pfp_above f x0"
   3.101 +  obtain k where 1: "?p = ((f\<up>x0)^^k) x0"
   3.102 +    using pfp_funpow `?p \<noteq> Top`
   3.103 +    by(fastsimp simp add: pfp_above_def)
   3.104 +  thus ?thesis using chain mono by simp
   3.105 +qed
   3.106 +
   3.107 +end
   3.108 +
   3.109 +text{* The interface of abstract values: *}
   3.110 +
   3.111 +locale Rep =
   3.112 +fixes rep :: "'a::SL_top \<Rightarrow> 'b set"
   3.113 +assumes le_rep: "a \<sqsubseteq> b \<Longrightarrow> rep a \<subseteq> rep b"
   3.114 +begin
   3.115 +
   3.116 +abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"
   3.117 +
   3.118 +lemma in_rep_join: "x <: a1 \<or> x <: a2 \<Longrightarrow> x <: a1 \<squnion> a2"
   3.119 +by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)
   3.120 +
   3.121 +end
   3.122 +
   3.123 +locale Val_abs = Rep rep
   3.124 +  for rep :: "'a::SL_top \<Rightarrow> val set" +
   3.125 +fixes num' :: "val \<Rightarrow> 'a"  ("num\<^isup>#")
   3.126 +and plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  ("plus\<^isup>#")
   3.127 +assumes rep_num': "rep(num' n) = {n}"
   3.128 +and rep_plus': "n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: plus' a1 a2"
   3.129 +
   3.130 +
   3.131 +instantiation "fun" :: (type, SL_top) SL_top
   3.132 +begin
   3.133 +
   3.134 +definition "f \<sqsubseteq> g = (ALL x. f x \<sqsubseteq> g x)"
   3.135 +definition "f \<squnion> g = (\<lambda>x. f x \<squnion> g x)"
   3.136 +definition "Top = (\<lambda>x. Top)"
   3.137 +
   3.138 +lemma join_apply[simp]:
   3.139 +  "(f \<squnion> g) x = f x \<squnion> g x"
   3.140 +by (simp add: join_fun_def)
   3.141 +
   3.142 +instance
   3.143 +proof
   3.144 +  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
   3.145 +qed (simp_all add: le_fun_def Top_fun_def)
   3.146 +
   3.147 +end
   3.148 +
   3.149 +subsection "Abstract Interpretation Abstractly"
   3.150 +
   3.151 +text{* Abstract interpretation over abstract values.
   3.152 +Abstract states are simply functions. *}
   3.153 +
   3.154 +locale Abs_Int_Fun = Val_abs
   3.155 +begin
   3.156 +
   3.157 +fun aval' :: "aexp \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> 'a" ("aval\<^isup>#") where
   3.158 +"aval' (N n) _ = num' n" |
   3.159 +"aval' (V x) S = S x" |
   3.160 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
   3.161 +
   3.162 +abbreviation fun_in_rep (infix "<:" 50) where
   3.163 +"f <: F == ALL x. f x <: F x"
   3.164 +
   3.165 +lemma fun_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T"
   3.166 +by (metis le_fun_def le_rep subsetD)
   3.167 +
   3.168 +lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S"
   3.169 +by (induct a) (auto simp: rep_num' rep_plus')
   3.170 +
   3.171 +fun AI :: "com \<Rightarrow> (name \<Rightarrow> 'a) \<Rightarrow> (name \<Rightarrow> 'a)" where
   3.172 +"AI SKIP S = S" |
   3.173 +"AI (x ::= a) S = S(x := aval' a S)" |
   3.174 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
   3.175 +"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" |
   3.176 +"AI (WHILE b DO c) S = pfp_above (AI c) S"
   3.177 +
   3.178 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0"
   3.179 +proof(induct c arbitrary: s t S0)
   3.180 +  case SKIP thus ?case by fastsimp
   3.181 +next
   3.182 +  case Assign thus ?case by (auto simp: aval'_sound)
   3.183 +next
   3.184 +  case Semi thus ?case by auto
   3.185 +next
   3.186 +  case If thus ?case by(auto simp: in_rep_join)
   3.187 +next
   3.188 +  case (While b c)
   3.189 +  let ?P = "pfp_above (AI c) S0"
   3.190 +  have pfp: "AI c ?P \<sqsubseteq> ?P" and "S0 \<sqsubseteq> ?P"
   3.191 +    by(simp_all add: SL_top_class.pfp_above_pfp)
   3.192 +  { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P"
   3.193 +    proof(induct "WHILE b DO c" s t rule: big_step_induct)
   3.194 +      case WhileFalse thus ?case by simp
   3.195 +    next
   3.196 +      case WhileTrue thus ?case using While.hyps pfp fun_in_rep_le by metis
   3.197 +    qed
   3.198 +  }
   3.199 +  with fun_in_rep_le[OF `s <: S0` `S0 \<sqsubseteq> ?P`]
   3.200 +  show ?case by (metis While(2) AI.simps(5))
   3.201 +qed
   3.202 +
   3.203 +end
   3.204 +
   3.205 +
   3.206 +text{* Problem: not executable because of the comparison of abstract states,
   3.207 +i.e. functions, in the post-fixedpoint computation. Need to implement
   3.208 +abstract states concretely. *}
   3.209 +
   3.210 +
   3.211 +(* Exercises: show that <= is a preorder if
   3.212 +1. v1 <= v2  =  rep v1 <= rep v2
   3.213 +2. v1 <= v2  =  ALL x. lookup v1 x <= lookup v2 x
   3.214 +*)
   3.215 +
   3.216 +end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/IMP/AbsInt1.thy	Fri Sep 02 19:25:18 2011 +0200
     4.3 @@ -0,0 +1,219 @@
     4.4 +(* Author: Tobias Nipkow *)
     4.5 +
     4.6 +theory AbsInt1
     4.7 +imports AbsInt0_const
     4.8 +begin
     4.9 +
    4.10 +subsection "Backward Analysis of Expressions"
    4.11 +
    4.12 +class L_top_bot = SL_top +
    4.13 +fixes meet :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 65)
    4.14 +and Bot :: "'a"
    4.15 +assumes meet_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
    4.16 +and meet_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
    4.17 +and meet_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
    4.18 +assumes bot[simp]: "Bot \<sqsubseteq> x"
    4.19 +
    4.20 +locale Rep1 = Rep rep for rep :: "'a::L_top_bot \<Rightarrow> 'b set" +
    4.21 +assumes inter_rep_subset_rep_meet: "rep a1 \<inter> rep a2 \<subseteq> rep(a1 \<sqinter> a2)"
    4.22 +and rep_Bot: "rep Bot = {}"
    4.23 +begin
    4.24 +
    4.25 +lemma in_rep_meet: "x <: a1 \<Longrightarrow> x <: a2 \<Longrightarrow> x <: a1 \<sqinter> a2"
    4.26 +by (metis IntI inter_rep_subset_rep_meet set_mp)
    4.27 +
    4.28 +lemma rep_meet[simp]: "rep(a1 \<sqinter> a2) = rep a1 \<inter> rep a2"
    4.29 +by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)
    4.30 +
    4.31 +end
    4.32 +
    4.33 +
    4.34 +locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
    4.35 +  for rep :: "'a::L_top_bot \<Rightarrow> int set" and num' plus' +
    4.36 +fixes inv_plus' :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a * 'a"
    4.37 +and inv_less' :: "'a \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow> 'a * 'a"
    4.38 +assumes inv_plus': "inv_plus' a1 a2 a = (a1',a2') \<Longrightarrow>
    4.39 +  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1+n2 <: a \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
    4.40 +and inv_less': "inv_less' a1 a2 (n1<n2) = (a1',a2') \<Longrightarrow>
    4.41 +  n1 <: a1 \<Longrightarrow> n2 <: a2 \<Longrightarrow> n1 <: a1' \<and> n2 <: a2'"
    4.42 +
    4.43 +datatype 'a up = bot | Up 'a
    4.44 +
    4.45 +instantiation up :: (SL_top)SL_top
    4.46 +begin
    4.47 +
    4.48 +fun le_up where
    4.49 +"Up x \<sqsubseteq> Up y = (x \<sqsubseteq> y)" |
    4.50 +"bot \<sqsubseteq> y = True" |
    4.51 +"Up _ \<sqsubseteq> bot = False"
    4.52 +
    4.53 +lemma [simp]: "(x \<sqsubseteq> bot) = (x = bot)"
    4.54 +by (cases x) simp_all
    4.55 +
    4.56 +lemma [simp]: "(Up x \<sqsubseteq> u) = (EX y. u = Up y & x \<sqsubseteq> y)"
    4.57 +by (cases u) auto
    4.58 +
    4.59 +fun join_up where
    4.60 +"Up x \<squnion> Up y = Up(x \<squnion> y)" |
    4.61 +"bot \<squnion> y = y" |
    4.62 +"x \<squnion> bot = x"
    4.63 +
    4.64 +lemma [simp]: "x \<squnion> bot = x"
    4.65 +by (cases x) simp_all
    4.66 +
    4.67 +
    4.68 +definition "Top = Up Top"
    4.69 +
    4.70 +(* register <= as transitive - see orderings *)
    4.71 +
    4.72 +instance proof
    4.73 +  case goal1 show ?case by(cases x, simp_all)
    4.74 +next
    4.75 +  case goal2 thus ?case
    4.76 +    by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
    4.77 +next
    4.78 +  case goal3 thus ?case by(cases x, simp, cases y, simp_all)
    4.79 +next
    4.80 +  case goal4 thus ?case by(cases y, simp, cases x, simp_all)
    4.81 +next
    4.82 +  case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
    4.83 +next
    4.84 +  case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
    4.85 +qed
    4.86 +
    4.87 +end
    4.88 +
    4.89 +
    4.90 +locale Abs_Int1 = Val_abs1
    4.91 +begin
    4.92 +
    4.93 +(* FIXME avoid duplicating this defn *)
    4.94 +abbreviation astate_in_rep (infix "<:" 50) where
    4.95 +"s <: S == ALL x. s x <: lookup S x"
    4.96 +
    4.97 +abbreviation in_rep_up :: "state \<Rightarrow> 'a astate up \<Rightarrow> bool"  (infix "<::" 50) where
    4.98 +"s <:: S == EX S0. S = Up S0 \<and> s <: S0"
    4.99 +
   4.100 +lemma in_rep_up_trans: "(s::state) <:: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <:: T"
   4.101 +apply auto
   4.102 +by (metis in_mono le_astate_def le_rep lookup_def top)
   4.103 +
   4.104 +lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 \<Longrightarrow> s <:: S1 \<squnion> S2"
   4.105 +by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)
   4.106 +
   4.107 +fun aval' :: "aexp \<Rightarrow> 'a astate up \<Rightarrow> 'a" ("aval\<^isup>#") where
   4.108 +"aval' _ bot = Bot" |
   4.109 +"aval' (N n) _ = num' n" |
   4.110 +"aval' (V x) (Up S) = lookup S x" |
   4.111 +"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
   4.112 +
   4.113 +lemma aval'_sound: "s <:: S \<Longrightarrow> aval a s <: aval' a S"
   4.114 +by (induct a) (auto simp: rep_num' rep_plus')
   4.115 +
   4.116 +fun afilter :: "aexp \<Rightarrow> 'a \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
   4.117 +"afilter (N n) a S = (if n <: a then S else bot)" |
   4.118 +"afilter (V x) a S = (case S of bot \<Rightarrow> bot | Up S \<Rightarrow>
   4.119 +  let a' = lookup S x \<sqinter> a in
   4.120 +  if a'\<sqsubseteq> Bot then bot else Up(update S x a'))" |
   4.121 +"afilter (Plus e1 e2) a S =
   4.122 + (let (a1,a2) = inv_plus' (aval' e1 S) (aval' e2 S) a
   4.123 +  in afilter e1 a1 (afilter e2 a2 S))"
   4.124 +
   4.125 +fun bfilter :: "bexp \<Rightarrow> bool \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
   4.126 +"bfilter (B bv) res S = (if bv=res then S else bot)" |
   4.127 +"bfilter (Not b) res S = bfilter b (\<not> res) S" |
   4.128 +"bfilter (And b1 b2) res S =
   4.129 +  (if res then bfilter b1 True (bfilter b2 True S)
   4.130 +   else bfilter b1 False S \<squnion> bfilter b2 False S)" |
   4.131 +"bfilter (Less e1 e2) res S =
   4.132 +  (let (res1,res2) = inv_less' (aval' e1 S) (aval' e2 S) res
   4.133 +   in afilter e1 res1 (afilter e2 res2 S))"
   4.134 +
   4.135 +lemma afilter_sound: "s <:: S \<Longrightarrow> aval e s <: a \<Longrightarrow> s <:: afilter e a S"
   4.136 +proof(induct e arbitrary: a S)
   4.137 +  case N thus ?case by simp
   4.138 +next
   4.139 +  case (V x)
   4.140 +  obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
   4.141 +  moreover hence "s x <: lookup S' x" by(simp)
   4.142 +  moreover have "s x <: a" using V by simp
   4.143 +  ultimately show ?case using V(1)
   4.144 +    by(simp add: lookup_update Let_def)
   4.145 +       (metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
   4.146 +next
   4.147 +  case (Plus e1 e2) thus ?case
   4.148 +    using inv_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
   4.149 +    by (auto split: prod.split)
   4.150 +qed
   4.151 +
   4.152 +lemma bfilter_sound: "s <:: S \<Longrightarrow> bv = bval b s \<Longrightarrow> s <:: bfilter b bv S"
   4.153 +proof(induct b arbitrary: S bv)
   4.154 +  case B thus ?case by simp
   4.155 +next
   4.156 +  case (Not b) thus ?case by simp
   4.157 +next
   4.158 +  case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
   4.159 +next
   4.160 +  case (Less e1 e2) thus ?case
   4.161 +    by (auto split: prod.split)
   4.162 +       (metis afilter_sound inv_less' aval'_sound Less)
   4.163 +qed
   4.164 +
   4.165 +fun AI :: "com \<Rightarrow> 'a astate up \<Rightarrow> 'a astate up" where
   4.166 +"AI SKIP S = S" |
   4.167 +"AI (x ::= a) S =
   4.168 +  (case S of bot \<Rightarrow> bot | Up S \<Rightarrow> Up(update S x (aval' a (Up S))))" |
   4.169 +"AI (c1;c2) S = AI c2 (AI c1 S)" |
   4.170 +"AI (IF b THEN c1 ELSE c2) S =
   4.171 +  AI c1 (bfilter b True S) \<squnion> AI c2 (bfilter b False S)" |
   4.172 +"AI (WHILE b DO c) S =
   4.173 +  bfilter b False (pfp_above (%S. AI c (bfilter b True S)) S)"
   4.174 +
   4.175 +lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <:: S \<Longrightarrow> t <:: AI c S"
   4.176 +proof(induct c arbitrary: s t S)
   4.177 +  case SKIP thus ?case by fastsimp
   4.178 +next
   4.179 +  case Assign thus ?case
   4.180 +    by (auto simp: lookup_update aval'_sound)
   4.181 +next
   4.182 +  case Semi thus ?case by fastsimp
   4.183 +next
   4.184 +  case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
   4.185 +next
   4.186 +  case (While b c)
   4.187 +  let ?P = "pfp_above (%S. AI c (bfilter b True S)) S"
   4.188 +  have pfp: "AI c (bfilter b True ?P) \<sqsubseteq> ?P" and "S \<sqsubseteq> ?P"
   4.189 +    by (rule pfp_above_pfp(1), rule pfp_above_pfp(2))
   4.190 +  { fix s t
   4.191 +    have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <:: ?P \<Longrightarrow>
   4.192 +          t <:: bfilter b False ?P"
   4.193 +    proof(induct "WHILE b DO c" s t rule: big_step_induct)
   4.194 +      case WhileFalse thus ?case by(metis bfilter_sound)
   4.195 +    next
   4.196 +      case WhileTrue show ?case
   4.197 +        by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
   4.198 +           rule While.hyps[OF WhileTrue(2)],
   4.199 +           rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
   4.200 +    qed
   4.201 +  }
   4.202 +  with in_rep_up_trans[OF `s <:: S` `S \<sqsubseteq> ?P`] While(2,3) AI.simps(5)
   4.203 +  show ?case by simp
   4.204 +qed
   4.205 +
   4.206 +text{* Exercise: *}
   4.207 +
   4.208 +lemma afilter_strict: "afilter e res bot = bot"
   4.209 +by (induct e arbitrary: res) simp_all
   4.210 +
   4.211 +lemma bfilter_strict: "bfilter b res bot = bot"
   4.212 +by (induct b arbitrary: res) (simp_all add: afilter_strict)
   4.213 +
   4.214 +lemma pfp_strict: "f bot = bot \<Longrightarrow> pfp_above f bot = bot"
   4.215 +by(simp add: pfp_above_def pfp_def eval_nat_numeral)
   4.216 +
   4.217 +lemma AI_strict: "AI c bot = bot"
   4.218 +by(induct c) (simp_all add: bfilter_strict pfp_strict)
   4.219 +
   4.220 +end
   4.221 +
   4.222 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/IMP/AbsInt1_ivl.thy	Fri Sep 02 19:25:18 2011 +0200
     5.3 @@ -0,0 +1,231 @@
     5.4 +(* Author: Tobias Nipkow *)
     5.5 +
     5.6 +theory AbsInt1_ivl
     5.7 +imports AbsInt1
     5.8 +begin
     5.9 +
    5.10 +subsection "Interval Analysis"
    5.11 +
    5.12 +datatype ivl = I "int option" "int option"
    5.13 +
    5.14 +definition "rep_ivl i =
    5.15 + (case i of I (Some l) (Some h) \<Rightarrow> {l..h} | I (Some l) None \<Rightarrow> {l..}
    5.16 +  | I None (Some h) \<Rightarrow> {..h} | I None None \<Rightarrow> UNIV)"
    5.17 +
    5.18 +instantiation option :: (plus)plus
    5.19 +begin
    5.20 +
    5.21 +fun plus_option where
    5.22 +"Some x + Some y = Some(x+y)" |
    5.23 +"_ + _ = None"
    5.24 +
    5.25 +instance proof qed
    5.26 +
    5.27 +end
    5.28 +
    5.29 +definition empty where "empty = I (Some 1) (Some 0)"
    5.30 +
    5.31 +fun is_empty where
    5.32 +"is_empty(I (Some l) (Some h)) = (h<l)" |
    5.33 +"is_empty _ = False"
    5.34 +
    5.35 +lemma [simp]: "is_empty(I l h) =
    5.36 +  (case l of Some l \<Rightarrow> (case h of Some h \<Rightarrow> h<l | None \<Rightarrow> False) | None \<Rightarrow> False)"
    5.37 +by(auto split:option.split)
    5.38 +
    5.39 +lemma [simp]: "is_empty i \<Longrightarrow> rep_ivl i = {}"
    5.40 +by(auto simp add: rep_ivl_def split: ivl.split option.split)
    5.41 +
    5.42 +definition "plus_ivl i1 i2 = (if is_empty i1 | is_empty i2 then empty
    5.43 +  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (l1+l2) (h1+h2))"
    5.44 +
    5.45 +instantiation ivl :: SL_top
    5.46 +begin
    5.47 +
    5.48 +definition le_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> bool" where
    5.49 +"le_option pos x y =
    5.50 + (case x of (Some i) \<Rightarrow> (case y of (Some j) \<Rightarrow> (i<=j) | None \<Rightarrow> pos)
    5.51 +  | None \<Rightarrow> (case y of Some j \<Rightarrow> (~pos) | None \<Rightarrow> True))"
    5.52 +
    5.53 +fun le_aux where
    5.54 +"le_aux (I l1 h1) (I l2 h2) = (le_option False l2 l1 & le_option True h1 h2)"
    5.55 +
    5.56 +definition le_ivl where
    5.57 +"i1 \<sqsubseteq> i2 =
    5.58 + (if is_empty i1 then True else
    5.59 +  if is_empty i2 then False else le_aux i1 i2)"
    5.60 +
    5.61 +definition min_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
    5.62 +"min_option pos o1 o2 = (if le_option pos o1 o2 then o1 else o2)"
    5.63 +
    5.64 +definition max_option :: "bool \<Rightarrow> int option \<Rightarrow> int option \<Rightarrow> int option" where
    5.65 +"max_option pos o1 o2 = (if le_option pos o1 o2 then o2 else o1)"
    5.66 +
    5.67 +definition "i1 \<squnion> i2 =
    5.68 + (if is_empty i1 then i2 else if is_empty i2 then i1
    5.69 +  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow>
    5.70 +          I (min_option False l1 l2) (max_option True h1 h2))"
    5.71 +
    5.72 +definition "Top = I None None"
    5.73 +
    5.74 +instance
    5.75 +proof
    5.76 +  case goal1 thus ?case
    5.77 +    by(cases x, simp add: le_ivl_def le_option_def split: option.split)
    5.78 +next
    5.79 +  case goal2 thus ?case
    5.80 +    by(cases x, cases y, cases z, auto simp: le_ivl_def le_option_def split: option.splits if_splits)
    5.81 +next
    5.82 +  case goal3 thus ?case
    5.83 +    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.84 +next
    5.85 +  case goal4 thus ?case
    5.86 +    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.87 +next
    5.88 +  case goal5 thus ?case
    5.89 +    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.90 +next
    5.91 +  case goal6 thus ?case
    5.92 +    by(cases x, simp add: Top_ivl_def le_ivl_def le_option_def split: option.split)
    5.93 +qed
    5.94 +
    5.95 +end
    5.96 +
    5.97 +
    5.98 +instantiation ivl :: L_top_bot
    5.99 +begin
   5.100 +
   5.101 +definition "i1 \<sqinter> i2 = (if is_empty i1 | is_empty i2 then empty
   5.102 +  else case (i1,i2) of (I l1 h1, I l2 h2) \<Rightarrow> I (max_option False l1 l2) (min_option True h1 h2))"
   5.103 +
   5.104 +definition "Bot = empty"
   5.105 +
   5.106 +instance
   5.107 +proof
   5.108 +  case goal1 thus ?case
   5.109 +    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.110 +next
   5.111 +  case goal2 thus ?case
   5.112 +    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.113 +next
   5.114 +  case goal3 thus ?case
   5.115 +    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.116 +next
   5.117 +  case goal4 show ?case by(cases x, simp add: Bot_ivl_def empty_def le_ivl_def)
   5.118 +qed
   5.119 +
   5.120 +end
   5.121 +
   5.122 +instantiation option :: (minus)minus
   5.123 +begin
   5.124 +
   5.125 +fun minus_option where
   5.126 +"Some x - Some y = Some(x-y)" |
   5.127 +"_ - _ = None"
   5.128 +
   5.129 +instance proof qed
   5.130 +
   5.131 +end
   5.132 +
   5.133 +definition "minus_ivl i1 i2 =
   5.134 + (if is_empty i1 | is_empty i2 then empty
   5.135 +  else case (i1,i2) of
   5.136 +    (I l1 h1, I l2 h2) \<Rightarrow> I (l1-h2) (h1-l2))"
   5.137 +
   5.138 +lemma rep_minus_ivl:
   5.139 +  "n1 : rep_ivl i1 \<Longrightarrow> n2 : rep_ivl i2 \<Longrightarrow> n1-n2 : rep_ivl(minus_ivl i1 i2)"
   5.140 +by(auto simp add: minus_ivl_def rep_ivl_def split: ivl.splits option.splits)
   5.141 +
   5.142 +
   5.143 +definition "inv_plus_ivl i1 i2 i =
   5.144 +  (if is_empty i then empty
   5.145 +   else i1 \<sqinter> minus_ivl i i2, i2 \<sqinter> minus_ivl i i1)"
   5.146 +
   5.147 +fun inv_less_ivl :: "ivl \<Rightarrow> ivl \<Rightarrow> bool \<Rightarrow> ivl * ivl" where
   5.148 +"inv_less_ivl (I l1 h1) (I l2 h2) res =
   5.149 +  (if res
   5.150 +   then (I l1 (min_option True h1 (h2 - Some 1)), I (max_option False (l1 + Some 1) l2) h2)
   5.151 +   else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
   5.152 +
   5.153 +interpretation Rep rep_ivl
   5.154 +proof
   5.155 +  case goal1 thus ?case
   5.156 +    by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
   5.157 +qed
   5.158 +
   5.159 +interpretation Val_abs rep_ivl "%n. I (Some n) (Some n)" plus_ivl
   5.160 +proof
   5.161 +  case goal1 thus ?case by(simp add: rep_ivl_def)
   5.162 +next
   5.163 +  case goal2 thus ?case
   5.164 +    by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
   5.165 +qed
   5.166 +
   5.167 +interpretation Rep1 rep_ivl
   5.168 +proof
   5.169 +  case goal1 thus ?case
   5.170 +    by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
   5.171 +next
   5.172 +  case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
   5.173 +qed
   5.174 +
   5.175 +interpretation Val_abs1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
   5.176 +proof
   5.177 +  case goal1 thus ?case
   5.178 +    by(auto simp add: inv_plus_ivl_def)
   5.179 +      (metis rep_minus_ivl add_diff_cancel add_commute)+
   5.180 +next
   5.181 +  case goal2 thus ?case
   5.182 +    by(cases a1, cases a2,
   5.183 +      auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
   5.184 +qed
   5.185 +
   5.186 +interpretation Abs_Int1 rep_ivl "%n. I (Some n) (Some n)" plus_ivl inv_plus_ivl inv_less_ivl
   5.187 +defines afilter_ivl is afilter
   5.188 +and bfilter_ivl is bfilter
   5.189 +and AI_ivl is AI
   5.190 +and aval_ivl is aval'
   5.191 +..
   5.192 +
   5.193 +
   5.194 +fun list_up where
   5.195 +"list_up bot = bot" |
   5.196 +"list_up (Up x) = Up(list x)"
   5.197 +
   5.198 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 5)) Top)"
   5.199 +value [code] "list_up(afilter_ivl (N 5) (I (Some 4) (Some 4)) Top)"
   5.200 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 4))
   5.201 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
   5.202 +value [code] "list_up(afilter_ivl (V ''x'') (I (Some 4) (Some 5))
   5.203 + (Up(FunDom(Top(''x'':=I (Some 5) (Some 6))) [''x''])))"
   5.204 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (V ''x'')) (I (Some 0) (Some 10))
   5.205 +  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
   5.206 +value [code] "list_up(afilter_ivl (Plus (V ''x'') (N 7)) (I (Some 0) (Some 10))
   5.207 +  (Up(FunDom(Top(''x'':= I (Some 0) (Some 100)))[''x''])))"
   5.208 +
   5.209 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
   5.210 +  (Up(FunDom(Top(''x'':= I (Some 0) (Some 0)))[''x''])))"
   5.211 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (V ''x'')) True
   5.212 +  (Up(FunDom(Top(''x'':= I (Some 0) (Some 2)))[''x''])))"
   5.213 +value [code] "list_up(bfilter_ivl (Less (V ''x'') (Plus (N 10) (V ''y''))) True
   5.214 +  (Up(FunDom(Top(''x'':= I (Some 15) (Some 20),''y'':= I (Some 5) (Some 7)))[''x'', ''y''])))"
   5.215 +
   5.216 +definition "test_ivl1 =
   5.217 + ''y'' ::= N 7;
   5.218 + IF Less (V ''x'') (V ''y'')
   5.219 + THEN ''y'' ::= Plus (V ''y'') (V ''x'')
   5.220 + ELSE ''x'' ::= Plus (V ''x'') (V ''y'')"
   5.221 +value [code] "list_up(AI_ivl test_ivl1 Top)"
   5.222 +
   5.223 +value "list_up (AI_ivl test3_const Top)"
   5.224 +
   5.225 +value "list_up (AI_ivl test5_const Top)"
   5.226 +
   5.227 +value "list_up (AI_ivl test6_const Top)"
   5.228 +
   5.229 +definition "test2_ivl =
   5.230 + ''y'' ::= N 7;
   5.231 + WHILE Less (V ''x'') (N 100) DO ''y'' ::= Plus (V ''y'') (N 1)"
   5.232 +value [code] "list_up(AI_ivl test2_ivl Top)"
   5.233 +
   5.234 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/IMP/Astate.thy	Fri Sep 02 19:25:18 2011 +0200
     6.3 @@ -0,0 +1,46 @@
     6.4 +(* Author: Tobias Nipkow *)
     6.5 +
     6.6 +theory Astate
     6.7 +imports AbsInt0_fun
     6.8 +begin
     6.9 +
    6.10 +subsection "Abstract State with Computable Ordering"
    6.11 +
    6.12 +text{* A concrete type of state with computable @{text"\<sqsubseteq>"}: *}
    6.13 +
    6.14 +datatype 'a astate = FunDom "string \<Rightarrow> 'a" "string list"
    6.15 +
    6.16 +fun "fun" where "fun (FunDom f _) = f"
    6.17 +fun dom where "dom (FunDom _ A) = A"
    6.18 +
    6.19 +definition "list S = [(x,fun S x). x \<leftarrow> dom S]"
    6.20 +
    6.21 +definition "lookup F x = (if x : set(dom F) then fun F x else Top)"
    6.22 +
    6.23 +definition "update F x y =
    6.24 +  FunDom ((fun F)(x:=y)) (if x : set(dom F) then dom F else x # dom F)"
    6.25 +
    6.26 +lemma lookup_update: "lookup (update S x y) = (lookup S)(x:=y)"
    6.27 +by(rule ext)(auto simp: lookup_def update_def)
    6.28 +
    6.29 +instantiation astate :: (SL_top) SL_top
    6.30 +begin
    6.31 +
    6.32 +definition "le_astate F G = (ALL x : set(dom G). lookup F x \<sqsubseteq> fun G x)"
    6.33 +
    6.34 +definition
    6.35 +"join_astate F G =
    6.36 + FunDom (%x. fun F x \<squnion> fun G x) ([x\<leftarrow>dom F. x : set(dom G)])"
    6.37 +
    6.38 +definition "Top = FunDom (%x. Top) []"
    6.39 +
    6.40 +instance
    6.41 +proof
    6.42 +  case goal2 thus ?case
    6.43 +    apply(auto simp: le_astate_def)
    6.44 +    by (metis lookup_def preord_class.le_trans top)
    6.45 +qed (auto simp: le_astate_def lookup_def join_astate_def Top_astate_def)
    6.46 +
    6.47 +end
    6.48 +
    6.49 +end
     7.1 --- a/src/HOL/IMP/ROOT.ML	Thu Sep 01 10:41:19 2011 -0700
     7.2 +++ b/src/HOL/IMP/ROOT.ML	Fri Sep 02 19:25:18 2011 +0200
     7.3 @@ -1,3 +1,5 @@
     7.4 +no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs"];
     7.5 +
     7.6  use_thys
     7.7  ["BExp",
     7.8   "ASM",
     7.9 @@ -10,6 +12,7 @@
    7.10   "Def_Ass_Sound_Big",
    7.11   "Def_Ass_Sound_Small",
    7.12   "Live",
    7.13 + "AbsInt1_ivl",
    7.14   "Hoare_Examples",
    7.15   "VC",
    7.16   "HoareT",
     8.1 --- a/src/HOL/IsaMakefile	Thu Sep 01 10:41:19 2011 -0700
     8.2 +++ b/src/HOL/IsaMakefile	Fri Sep 02 19:25:18 2011 +0200
     8.3 @@ -511,7 +511,9 @@
     8.4  
     8.5  HOL-IMP: HOL $(OUT)/HOL-IMP
     8.6  
     8.7 -$(OUT)/HOL-IMP: $(OUT)/HOL IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
     8.8 +$(OUT)/HOL-IMP: $(OUT)/HOL IMP/AbsInt0_fun.thy IMP/Astate.thy \
     8.9 +  IMP/AbsInt0.thy IMP/AbsInt0_const.thy IMP/AbsInt1.thy IMP/AbsInt1_ivl.thy \
    8.10 +  IMP/ASM.thy IMP/AExp.thy IMP/BExp.thy	\
    8.11    IMP/Big_Step.thy IMP/C_like.thy IMP/Com.thy IMP/Compiler.thy \
    8.12    IMP/Comp_Rev.thy IMP/Def_Ass.thy IMP/Def_Ass_Big.thy IMP/Def_Ass_Exp.thy \
    8.13    IMP/Def_Ass_Small.thy IMP/Def_Ass_Sound_Big.thy \