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