Theory Abs_Int_den0

theory Abs_Int_den0
imports Abs_State_den
(* Author: Tobias Nipkow *)

theory Abs_Int_den0
imports Abs_State_den

subsection "Computable Abstract Interpretation"

text{* Abstract interpretation over type @{text astate} instead of
functions. *}

locale Abs_Int = Val_abs +
fixes pfp :: "('a astate ⇒ 'a astate) ⇒ 'a astate ⇒ 'a astate"
assumes pfp: "f(pfp f x0) ⊑ pfp f x0"
assumes above: "x0 ⊑ pfp f x0"

fun aval' :: "aexp ⇒ 'a astate ⇒ 'a" where
"aval' (N n) _ = num' n" |
"aval' (V x) S = lookup S x" |
"aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)"

abbreviation astate_in_rep (infix "<:" 50) where
"s <: S == ALL x. s x <: lookup S x"

lemma astate_in_rep_le: "(s::state) <: S ⟹ S ⊑ T ⟹ s <: T"
by (metis in_mono le_astate_def le_rep lookup_def top)

lemma aval'_sound: "s <: S ⟹ aval a s <: aval' a S"
by (induct a) (auto simp: rep_num' rep_plus')

fun AI :: "com ⇒ 'a astate ⇒ 'a astate" where
"AI SKIP S = S" |
"AI (x ::= a) S = update S x (aval' a S)" |
"AI (c1;;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S = (AI c1 S) ⊔ (AI c2 S)" |
"AI (WHILE b DO c) S = pfp (AI c) S"

lemma AI_sound: "(c,s) ⇒ t ⟹ s <: S0 ⟹ t <: AI c S0"
proof(induction c arbitrary: s t S0)
  case SKIP thus ?case by fastforce
  case Assign thus ?case
    by (auto simp: lookup_update aval'_sound)
  case Seq thus ?case by auto
  case If thus ?case
    by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2)
  case (While b c)
  let ?P = "pfp (AI c) S0"
  { fix s t have "(WHILE b DO c,s) ⇒ t ⟹ s <: ?P ⟹ t <: ?P"
    proof(induction "WHILE b DO c" s t rule: big_step_induct)
      case WhileFalse thus ?case by simp
      case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis
  with astate_in_rep_le[OF `s <: S0` above]
  show ?case by (metis While(2) AI.simps(5))