Added Hoare-like Abstract Interpretation
authornipkow
Wed Sep 28 09:55:11 2011 +0200 (2011-09-28 ago)
changeset 45111054a9ac0d7ef
parent 45110 305f83b6da54
child 45112 32c90199df2e
Added Hoare-like Abstract Interpretation
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int0_const.thy
src/HOL/IMP/Abs_Int0_fun.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/IMP/Abs_Int1_ivl.thy
src/HOL/IMP/Abs_Int2.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int0.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int0_fun.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int1.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int2.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_fun.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
src/HOL/IMP/Abs_Int_Den/Abs_State.thy
src/HOL/IMP/Abs_Int_Den/Abs_State_den.thy
src/HOL/IMP/Abs_State.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/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 \