Theory Abs_Int_den0_fun

theory Abs_Int_den0_fun
imports Big_Step
(* Author: Tobias Nipkow *)

section "Denotational Abstract Interpretation"

theory Abs_Int_den0_fun
imports "../Big_Step"

subsection "Orderings"

class preord =
fixes le :: "'a ⇒ 'a ⇒ bool" (infix "⊑" 50)
assumes le_refl[simp]: "x ⊑ x"
and le_trans: "x ⊑ y ⟹ y ⊑ z ⟹ x ⊑ z"

text{* Note: no antisymmetry. Allows implementations where some abstract
element is implemented by two different values @{prop "x ≠ y"}
such that @{prop"x ⊑ y"} and @{prop"y ⊑ x"}. Antisymmetry is not
needed because we never compare elements for equality but only for @{text"⊑"}.

class SL_top = preord +
fixes join :: "'a ⇒ 'a ⇒ 'a" (infixl "⊔" 65)
fixes Top :: "'a"
assumes join_ge1 [simp]: "x ⊑ x ⊔ y"
and join_ge2 [simp]: "y ⊑ x ⊔ y"
and join_least: "x ⊑ z ⟹ y ⊑ z ⟹ x ⊔ y ⊑ z"
and top[simp]: "x ⊑ Top"

lemma join_le_iff[simp]: "x ⊔ y ⊑ z ⟷ x ⊑ z ∧ y ⊑ z"
by (metis join_ge1 join_ge2 join_least le_trans)

fun iter :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" where
"iter 0 f _ = Top" |
"iter (Suc n) f x = (if f x ⊑ x then x else iter n f (f x))"

lemma iter_pfp: "f(iter n f x) ⊑ iter n f x"
apply (induction n arbitrary: x)
 apply (simp)
apply (simp)

abbreviation iter' :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a" where
"iter' n f x0 == iter n (λx. x0 ⊔ f x) x0"

lemma iter'_pfp_above:
  "f(iter' n f x0) ⊑ iter' n f x0"  "x0 ⊑ iter' n f x0"
using iter_pfp[of "λx. x0 ⊔ f x"] by auto

text{* So much for soundness. But how good an approximation of the post-fixed
point does @{const iter} yield? *}

lemma iter_funpow: "iter n f x ≠ Top ⟹ ∃k. iter n f x = (f^^k) x"
apply(induction n arbitrary: x)
 apply simp
apply (auto)
 apply(metis funpow.simps(1) id_def)
by (metis funpow.simps(2) funpow_swap1 o_apply)

text{* For monotone @{text f}, @{term "iter f n x0"} yields the least
post-fixed point above @{text x0}, unless it yields @{text Top}. *}

lemma iter_least_pfp:
assumes mono: "⋀x y. x ⊑ y ⟹ f x ⊑ f y" and "iter n f x0 ≠ Top"
and "f p ⊑ p" and "x0 ⊑ p" shows "iter n f x0 ⊑ p"
  obtain k where "iter n f x0 = (f^^k) x0"
    using iter_funpow[OF `iter n f x0 ≠ Top`] by blast
  { fix n have "(f^^n) x0 ⊑ p"
    proof(induction n)
      case 0 show ?case by(simp add: `x0 ⊑ p`)
      case (Suc n) thus ?case
        by (simp add: `x0 ⊑ p`)(metis Suc assms(3) le_trans mono)
  } ultimately show ?thesis by simp


text{* The interface of abstract values: *}

locale Rep =
fixes rep :: "'a::SL_top ⇒ 'b set"
assumes le_rep: "a ⊑ b ⟹ rep a ⊆ rep b"

abbreviation in_rep (infix "<:" 50) where "x <: a == x : rep a"

lemma in_rep_join: "x <: a1 ∨ x <: a2 ⟹ x <: a1 ⊔ a2"
by (metis SL_top_class.join_ge1 SL_top_class.join_ge2 le_rep subsetD)


locale Val_abs = Rep rep
  for rep :: "'a::SL_top ⇒ val set" +
fixes num' :: "val ⇒ 'a"
and plus' :: "'a ⇒ 'a ⇒ 'a"
assumes rep_num': "rep(num' n) = {n}"
and rep_plus': "n1 <: a1 ⟹ n2 <: a2 ⟹ n1+n2 <: plus' a1 a2"

instantiation "fun" :: (type, SL_top) SL_top

definition "f ⊑ g = (ALL x. f x ⊑ g x)"
definition "f ⊔ g = (λx. f x ⊔ g x)"
definition "Top = (λx. Top)"

lemma join_apply[simp]:
  "(f ⊔ g) x = f x ⊔ g x"
by (simp add: join_fun_def)

  case goal2 thus ?case by (metis le_fun_def preord_class.le_trans)
qed (simp_all add: le_fun_def Top_fun_def)


subsection "Abstract Interpretation Abstractly"

text{* Abstract interpretation over abstract values. Abstract states are
simply functions. The post-fixed point finder is parameterized over. *}

type_synonym 'a st = "vname ⇒ 'a"

locale Abs_Int_Fun = Val_abs +
fixes pfp :: "('a st ⇒ 'a st) ⇒ 'a st ⇒ 'a st"
assumes pfp: "f(pfp f x) ⊑ pfp f x"
assumes above: "x ⊑ pfp f x"

fun aval' :: "aexp ⇒ 'a st ⇒ 'a" where
"aval' (N n) _ = num' n" |
"aval' (V x) S = S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"

abbreviation fun_in_rep (infix "<:" 50) where
"f <: F == ∀x. f x <: F x"

lemma fun_in_rep_le: "(s::state) <: S ⟹ S ⊑ T ⟹ s <: T"
by (metis le_fun_def le_rep subsetD)

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

fun AI :: "com ⇒ 'a st ⇒ 'a st" where
"AI SKIP S = S" |
"AI (x ::= a) S = 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: aval'_sound)
  case Seq thus ?case by auto
  case If thus ?case by(auto simp: in_rep_join)
  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 by(metis While.IH pfp fun_in_rep_le)
  with fun_in_rep_le[OF `s <: S0` above]
  show ?case by (metis While(2) AI.simps(5))


text{* Problem: not executable because of the comparison of abstract states,
i.e. functions, in the post-fixedpoint computation. Need to implement
abstract states concretely. *}