src/HOL/IMP/Abs_Int0.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45127 d2eb07a1e01b
child 45623 f682f3f7b726
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@45111
     1
(* Author: Tobias Nipkow *)
nipkow@45111
     2
nipkow@45111
     3
theory Abs_Int0
nipkow@45111
     4
imports Abs_State
nipkow@45111
     5
begin
nipkow@45111
     6
nipkow@45111
     7
subsection "Computable Abstract Interpretation"
nipkow@45111
     8
nipkow@45111
     9
text{* Abstract interpretation over type @{text astate} instead of
nipkow@45111
    10
functions. *}
nipkow@45111
    11
nipkow@45127
    12
locale Abs_Int = Val_abs
nipkow@45111
    13
begin
nipkow@45111
    14
nipkow@45111
    15
fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where
nipkow@45111
    16
"aval' (N n) _ = num' n" |
nipkow@45111
    17
"aval' (V x) S = lookup S x" |
nipkow@45111
    18
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"
nipkow@45111
    19
nipkow@45111
    20
fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where
nipkow@45111
    21
"step S (SKIP {P}) = (SKIP {S})" |
nipkow@45111
    22
"step S (x ::= e {P}) =
nipkow@45111
    23
  x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" |
nipkow@45111
    24
"step S (c1; c2) = step S c1; step (post c1) c2" |
nipkow@45111
    25
"step S (IF b THEN c1 ELSE c2 {P}) =
nipkow@45111
    26
  (let c1' = step S c1; c2' = step S c2
nipkow@45111
    27
   in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" |
nipkow@45111
    28
"step S ({Inv} WHILE b DO c {P}) =
nipkow@45111
    29
   {S \<squnion> post c} WHILE b DO step Inv c {Inv}"
nipkow@45111
    30
nipkow@45127
    31
definition AI :: "com \<Rightarrow> 'a st up acom option" where
nipkow@45127
    32
"AI = lpfp\<^isub>c (step \<top>)"
nipkow@45127
    33
nipkow@45127
    34
nipkow@45111
    35
lemma strip_step[simp]: "strip(step S c) = strip c"
nipkow@45111
    36
by(induct c arbitrary: S) (simp_all add: Let_def)
nipkow@45111
    37
nipkow@45111
    38
nipkow@45127
    39
text{* Soundness: *}
nipkow@45111
    40
nipkow@45111
    41
lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S"
nipkow@45111
    42
by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def)
nipkow@45111
    43
nipkow@45111
    44
lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a"
nipkow@45111
    45
by(simp add: rep_st_def lookup_update)
nipkow@45111
    46
nipkow@45111
    47
lemma step_sound:
nipkow@45111
    48
  "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c"
nipkow@45111
    49
proof(induction c arbitrary: S s t)
nipkow@45111
    50
  case SKIP thus ?case
nipkow@45111
    51
    by simp (metis skipE up_fun_in_rep_le)
nipkow@45111
    52
next
nipkow@45111
    53
  case Assign thus ?case
nipkow@45111
    54
    apply (auto simp del: fun_upd_apply simp: split: up.splits)
nipkow@45111
    55
    by (metis aval'_sound fun_in_rep_le in_rep_update)
nipkow@45111
    56
next
nipkow@45111
    57
  case Semi thus ?case by simp blast
nipkow@45111
    58
next
nipkow@45111
    59
  case (If b c1 c2 S0) thus ?case
nipkow@45111
    60
    apply(auto simp: Let_def)
nipkow@45111
    61
    apply (metis up_fun_in_rep_le)+
nipkow@45111
    62
    done
nipkow@45111
    63
next
nipkow@45111
    64
  case (While Inv b c P)
nipkow@45111
    65
  from While.prems have inv: "step Inv c \<sqsubseteq> c"
nipkow@45111
    66
    and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def)
nipkow@45111
    67
  { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv"
nipkow@45111
    68
    proof(induction "WHILE b DO strip c" s t rule: big_step_induct)
nipkow@45111
    69
      case WhileFalse thus ?case by simp
nipkow@45111
    70
    next
nipkow@45111
    71
      case (WhileTrue s1 s2 s3)
nipkow@45111
    72
      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`]]
nipkow@45111
    73
      show ?case .
nipkow@45111
    74
    qed
nipkow@45111
    75
  }
nipkow@45111
    76
  thus ?case using While.prems(2)
nipkow@45111
    77
    by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le)
nipkow@45111
    78
qed
nipkow@45111
    79
nipkow@45127
    80
lemma AI_sound: "\<lbrakk> AI c = Some c';  (c,s) \<Rightarrow> t \<rbrakk> \<Longrightarrow> t <:up post c'"
nipkow@45127
    81
by (metis AI_def in_rep_Top_up lpfpc_pfp step_sound strip_lpfpc strip_step)
nipkow@45111
    82
nipkow@45111
    83
end
nipkow@45111
    84
nipkow@45111
    85
nipkow@45127
    86
subsubsection "Monotonicity"
nipkow@45127
    87
nipkow@45127
    88
locale Abs_Int_mono = Abs_Int +
nipkow@45127
    89
assumes mono_plus': "a1 \<sqsubseteq> b1 \<Longrightarrow> a2 \<sqsubseteq> b2 \<Longrightarrow> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
nipkow@45127
    90
begin
nipkow@45127
    91
nipkow@45127
    92
lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'"
nipkow@45127
    93
by(induction e) (auto simp: le_st_def lookup_def mono_plus')
nipkow@45127
    94
nipkow@45127
    95
lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'"
nipkow@45127
    96
by(auto simp add: le_st_def lookup_def update_def)
nipkow@45127
    97
nipkow@45127
    98
lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c"
nipkow@45127
    99
apply(induction c arbitrary: S S')
nipkow@45127
   100
apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split)
nipkow@45127
   101
done
nipkow@45127
   102
nipkow@45111
   103
end
nipkow@45127
   104
nipkow@45127
   105
end