src/HOL/IMP/Abs_Int2.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 61179 16775cad1a5c
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
     1 (* Author: Tobias Nipkow *)
     2 
     3 theory Abs_Int2
     4 imports Abs_Int1
     5 begin
     6 
     7 instantiation prod :: (order,order) order
     8 begin
     9 
    10 definition "less_eq_prod p1 p2 = (fst p1 \<le> fst p2 \<and> snd p1 \<le> snd p2)"
    11 definition "less_prod p1 p2 = (p1 \<le> p2 \<and> \<not> p2 \<le> (p1::'a*'b))"
    12 
    13 instance
    14 proof (standard, goal_cases)
    15   case 1 show ?case by(rule less_prod_def)
    16 next
    17   case 2 show ?case by(simp add: less_eq_prod_def)
    18 next
    19   case 3 thus ?case unfolding less_eq_prod_def by(metis order_trans)
    20 next
    21   case 4 thus ?case by(simp add: less_eq_prod_def)(metis eq_iff surjective_pairing)
    22 qed
    23 
    24 end
    25 
    26 
    27 subsection "Backward Analysis of Expressions"
    28 
    29 subclass (in bounded_lattice) semilattice_sup_top ..
    30 
    31 locale Val_lattice_gamma = Gamma_semilattice where \<gamma> = \<gamma>
    32   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
    33 assumes inter_gamma_subset_gamma_inf:
    34   "\<gamma> a1 \<inter> \<gamma> a2 \<subseteq> \<gamma>(a1 \<sqinter> a2)"
    35 and gamma_bot[simp]: "\<gamma> \<bottom> = {}"
    36 begin
    37 
    38 lemma in_gamma_inf: "x : \<gamma> a1 \<Longrightarrow> x : \<gamma> a2 \<Longrightarrow> x : \<gamma>(a1 \<sqinter> a2)"
    39 by (metis IntI inter_gamma_subset_gamma_inf set_mp)
    40 
    41 lemma gamma_inf: "\<gamma>(a1 \<sqinter> a2) = \<gamma> a1 \<inter> \<gamma> a2"
    42 by(rule equalityI[OF _ inter_gamma_subset_gamma_inf])
    43   (metis inf_le1 inf_le2 le_inf_iff mono_gamma)
    44 
    45 end
    46 
    47 
    48 locale Val_inv = Val_lattice_gamma where \<gamma> = \<gamma>
    49    for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set" +
    50 fixes test_num' :: "val \<Rightarrow> 'av \<Rightarrow> bool"
    51 and inv_plus' :: "'av \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
    52 and inv_less' :: "bool \<Rightarrow> 'av \<Rightarrow> 'av \<Rightarrow> 'av * 'av"
    53 assumes test_num': "test_num' i a = (i : \<gamma> a)"
    54 and inv_plus': "inv_plus' a a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
    55   i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1+i2 : \<gamma> a \<Longrightarrow> i1 : \<gamma> a\<^sub>1' \<and> i2 : \<gamma> a\<^sub>2'"
    56 and inv_less': "inv_less' (i1<i2) a1 a2 = (a\<^sub>1',a\<^sub>2') \<Longrightarrow>
    57   i1 : \<gamma> a1 \<Longrightarrow> i2 : \<gamma> a2 \<Longrightarrow> i1 : \<gamma> a\<^sub>1' \<and> i2 : \<gamma> a\<^sub>2'"
    58 
    59 
    60 locale Abs_Int_inv = Val_inv where \<gamma> = \<gamma>
    61   for \<gamma> :: "'av::bounded_lattice \<Rightarrow> val set"
    62 begin
    63 
    64 lemma in_gamma_sup_UpI:
    65   "s : \<gamma>\<^sub>o S1 \<or> s : \<gamma>\<^sub>o S2 \<Longrightarrow> s : \<gamma>\<^sub>o(S1 \<squnion> S2)"
    66 by (metis (hide_lams, no_types) sup_ge1 sup_ge2 mono_gamma_o subsetD)
    67 
    68 fun aval'' :: "aexp \<Rightarrow> 'av st option \<Rightarrow> 'av" where
    69 "aval'' e None = \<bottom>" |
    70 "aval'' e (Some S) = aval' e S"
    71 
    72 lemma aval''_correct: "s : \<gamma>\<^sub>o S \<Longrightarrow> aval a s : \<gamma>(aval'' a S)"
    73 by(cases S)(auto simp add: aval'_correct split: option.splits)
    74 
    75 subsubsection "Backward analysis"
    76 
    77 fun inv_aval' :: "aexp \<Rightarrow> 'av \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    78 "inv_aval' (N n) a S = (if test_num' n a then S else None)" |
    79 "inv_aval' (V x) a S = (case S of None \<Rightarrow> None | Some S \<Rightarrow>
    80   let a' = fun S x \<sqinter> a in
    81   if a' = \<bottom> then None else Some(update S x a'))" |
    82 "inv_aval' (Plus e1 e2) a S =
    83  (let (a1,a2) = inv_plus' a (aval'' e1 S) (aval'' e2 S)
    84   in inv_aval' e1 a1 (inv_aval' e2 a2 S))"
    85 
    86 text{* The test for @{const bot} in the @{const V}-case is important: @{const
    87 bot} indicates that a variable has no possible values, i.e.\ that the current
    88 program point is unreachable. But then the abstract state should collapse to
    89 @{const None}. Put differently, we maintain the invariant that in an abstract
    90 state of the form @{term"Some s"}, all variables are mapped to non-@{const
    91 bot} values. Otherwise the (pointwise) sup of two abstract states, one of
    92 which contains @{const bot} values, may produce too large a result, thus
    93 making the analysis less precise. *}
    94 
    95 
    96 fun inv_bval' :: "bexp \<Rightarrow> bool \<Rightarrow> 'av st option \<Rightarrow> 'av st option" where
    97 "inv_bval' (Bc v) res S = (if v=res then S else None)" |
    98 "inv_bval' (Not b) res S = inv_bval' b (\<not> res) S" |
    99 "inv_bval' (And b1 b2) res S =
   100   (if res then inv_bval' b1 True (inv_bval' b2 True S)
   101    else inv_bval' b1 False S \<squnion> inv_bval' b2 False S)" |
   102 "inv_bval' (Less e1 e2) res S =
   103   (let (a1,a2) = inv_less' res (aval'' e1 S) (aval'' e2 S)
   104    in inv_aval' e1 a1 (inv_aval' e2 a2 S))"
   105 
   106 lemma inv_aval'_correct: "s : \<gamma>\<^sub>o S \<Longrightarrow> aval e s : \<gamma> a \<Longrightarrow> s : \<gamma>\<^sub>o (inv_aval' e a S)"
   107 proof(induction e arbitrary: a S)
   108   case N thus ?case by simp (metis test_num')
   109 next
   110   case (V x)
   111   obtain S' where "S = Some S'" and "s : \<gamma>\<^sub>s S'" using `s : \<gamma>\<^sub>o S`
   112     by(auto simp: in_gamma_option_iff)
   113   moreover hence "s x : \<gamma> (fun S' x)"
   114     by(simp add: \<gamma>_st_def)
   115   moreover have "s x : \<gamma> a" using V(2) by simp
   116   ultimately show ?case
   117     by(simp add: Let_def \<gamma>_st_def)
   118       (metis mono_gamma emptyE in_gamma_inf gamma_bot subset_empty)
   119 next
   120   case (Plus e1 e2) thus ?case
   121     using inv_plus'[OF _ aval''_correct aval''_correct]
   122     by (auto split: prod.split)
   123 qed
   124 
   125 lemma inv_bval'_correct: "s : \<gamma>\<^sub>o S \<Longrightarrow> bv = bval b s \<Longrightarrow> s : \<gamma>\<^sub>o(inv_bval' b bv S)"
   126 proof(induction b arbitrary: S bv)
   127   case Bc thus ?case by simp
   128 next
   129   case (Not b) thus ?case by simp
   130 next
   131   case (And b1 b2) thus ?case
   132     by simp (metis And(1) And(2) in_gamma_sup_UpI)
   133 next
   134   case (Less e1 e2) thus ?case
   135     apply hypsubst_thin
   136     apply (auto split: prod.split)
   137     apply (metis (lifting) inv_aval'_correct aval''_correct inv_less')
   138     done
   139 qed
   140 
   141 definition "step' = Step
   142   (\<lambda>x e S. case S of None \<Rightarrow> None | Some S \<Rightarrow> Some(update S x (aval' e S)))
   143   (\<lambda>b S. inv_bval' b True S)"
   144 
   145 definition AI :: "com \<Rightarrow> 'av st option acom option" where
   146 "AI c = pfp (step' \<top>) (bot c)"
   147 
   148 lemma strip_step'[simp]: "strip(step' S c) = strip c"
   149 by(simp add: step'_def)
   150 
   151 lemma top_on_inv_aval': "\<lbrakk> top_on_opt S X;  vars e \<subseteq> -X \<rbrakk> \<Longrightarrow> top_on_opt (inv_aval' e a S) X"
   152 by(induction e arbitrary: a S) (auto simp: Let_def split: option.splits prod.split)
   153 
   154 lemma top_on_inv_bval': "\<lbrakk>top_on_opt S X; vars b \<subseteq> -X\<rbrakk> \<Longrightarrow> top_on_opt (inv_bval' b r S) X"
   155 by(induction b arbitrary: r S) (auto simp: top_on_inv_aval' top_on_sup split: prod.split)
   156 
   157 lemma top_on_step': "top_on_acom C (- vars C) \<Longrightarrow> top_on_acom (step' \<top> C) (- vars C)"
   158 unfolding step'_def
   159 by(rule top_on_Step)
   160   (auto simp add: top_on_top top_on_inv_bval' split: option.split)
   161 
   162 subsubsection "Correctness"
   163 
   164 lemma step_step': "step (\<gamma>\<^sub>o S) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' S C)"
   165 unfolding step_def step'_def
   166 by(rule gamma_Step_subcomm)
   167   (auto simp: intro!: aval'_correct inv_bval'_correct in_gamma_update split: option.splits)
   168 
   169 lemma AI_correct: "AI c = Some C \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c C"
   170 proof(simp add: CS_def AI_def)
   171   assume 1: "pfp (step' \<top>) (bot c) = Some C"
   172   have pfp': "step' \<top> C \<le> C" by(rule pfp_pfp[OF 1])
   173   have 2: "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c C"  --"transfer the pfp'"
   174   proof(rule order_trans)
   175     show "step (\<gamma>\<^sub>o \<top>) (\<gamma>\<^sub>c C) \<le> \<gamma>\<^sub>c (step' \<top> C)" by(rule step_step')
   176     show "... \<le> \<gamma>\<^sub>c C" by (metis mono_gamma_c[OF pfp'])
   177   qed
   178   have 3: "strip (\<gamma>\<^sub>c C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
   179   have "lfp c (step (\<gamma>\<^sub>o \<top>)) \<le> \<gamma>\<^sub>c C"
   180     by(rule lfp_lowerbound[simplified,where f="step (\<gamma>\<^sub>o \<top>)", OF 3 2])
   181   thus "lfp c (step UNIV) \<le> \<gamma>\<^sub>c C" by simp
   182 qed
   183 
   184 end
   185 
   186 
   187 subsubsection "Monotonicity"
   188 
   189 locale Abs_Int_inv_mono = Abs_Int_inv +
   190 assumes mono_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> plus' a1 a2 \<le> plus' b1 b2"
   191 and mono_inv_plus': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow> r \<le> r' \<Longrightarrow>
   192   inv_plus' r a1 a2 \<le> inv_plus' r' b1 b2"
   193 and mono_inv_less': "a1 \<le> b1 \<Longrightarrow> a2 \<le> b2 \<Longrightarrow>
   194   inv_less' bv a1 a2 \<le> inv_less' bv b1 b2"
   195 begin
   196 
   197 lemma mono_aval':
   198   "S1 \<le> S2 \<Longrightarrow> aval' e S1 \<le> aval' e S2"
   199 by(induction e) (auto simp: mono_plus' mono_fun)
   200 
   201 lemma mono_aval'':
   202   "S1 \<le> S2 \<Longrightarrow> aval'' e S1 \<le> aval'' e S2"
   203 apply(cases S1)
   204  apply simp
   205 apply(cases S2)
   206  apply simp
   207 by (simp add: mono_aval')
   208 
   209 lemma mono_inv_aval': "r1 \<le> r2 \<Longrightarrow> S1 \<le> S2 \<Longrightarrow> inv_aval' e r1 S1 \<le> inv_aval' e r2 S2"
   210 apply(induction e arbitrary: r1 r2 S1 S2)
   211    apply(auto simp: test_num' Let_def inf_mono split: option.splits prod.splits)
   212    apply (metis mono_gamma subsetD)
   213   apply (metis le_bot inf_mono le_st_iff)
   214  apply (metis inf_mono mono_update le_st_iff)
   215 apply(metis mono_aval'' mono_inv_plus'[simplified less_eq_prod_def] fst_conv snd_conv)
   216 done
   217 
   218 lemma mono_inv_bval': "S1 \<le> S2 \<Longrightarrow> inv_bval' b bv S1 \<le> inv_bval' b bv S2"
   219 apply(induction b arbitrary: bv S1 S2)
   220    apply(simp)
   221   apply(simp)
   222  apply simp
   223  apply(metis order_trans[OF _ sup_ge1] order_trans[OF _ sup_ge2])
   224 apply (simp split: prod.splits)
   225 apply(metis mono_aval'' mono_inv_aval' mono_inv_less'[simplified less_eq_prod_def] fst_conv snd_conv)
   226 done
   227 
   228 theorem mono_step': "S1 \<le> S2 \<Longrightarrow> C1 \<le> C2 \<Longrightarrow> step' S1 C1 \<le> step' S2 C2"
   229 unfolding step'_def
   230 by(rule mono2_Step) (auto simp: mono_aval' mono_inv_bval' split: option.split)
   231 
   232 lemma mono_step'_top: "C1 \<le> C2 \<Longrightarrow> step' \<top> C1 \<le> step' \<top> C2"
   233 by (metis mono_step' order_refl)
   234 
   235 end
   236 
   237 end