# Theory Abs_Int_den1

theory Abs_Int_den1
imports Abs_Int_den0_const
```(* Author: Tobias Nipkow *)

theory Abs_Int_den1
imports Abs_Int_den0_const
begin

subsection "Backward Analysis of Expressions"

class L_top_bot = SL_top +
fixes meet :: "'a ⇒ 'a ⇒ 'a" (infixl "⊓" 65)
and Bot :: "'a"
assumes meet_le1 [simp]: "x ⊓ y ⊑ x"
and meet_le2 [simp]: "x ⊓ y ⊑ y"
and meet_greatest: "x ⊑ y ⟹ x ⊑ z ⟹ x ⊑ y ⊓ z"
assumes bot[simp]: "Bot ⊑ x"

locale Rep1 = Rep rep for rep :: "'a::L_top_bot ⇒ 'b set" +
assumes inter_rep_subset_rep_meet: "rep a1 ∩ rep a2 ⊆ rep(a1 ⊓ a2)"
and rep_Bot: "rep Bot = {}"
begin

lemma in_rep_meet: "x <: a1 ⟹ x <: a2 ⟹ x <: a1 ⊓ a2"
by (metis IntI inter_rep_subset_rep_meet set_mp)

lemma rep_meet[simp]: "rep(a1 ⊓ a2) = rep a1 ∩ rep a2"
by (metis equalityI inter_rep_subset_rep_meet le_inf_iff le_rep meet_le1 meet_le2)

end

locale Val_abs1 = Val_abs rep num' plus' + Rep1 rep
for rep :: "'a::L_top_bot ⇒ int set" and num' plus' +
fixes filter_plus' :: "'a ⇒ 'a ⇒ 'a ⇒ 'a * 'a"
and filter_less' :: "bool ⇒ 'a ⇒ 'a ⇒ 'a * 'a"
assumes filter_plus': "filter_plus' a a1 a2 = (a1',a2') ⟹
n1 <: a1 ⟹ n2 <: a2 ⟹ n1+n2 <: a ⟹ n1 <: a1' ∧ n2 <: a2'"
and filter_less': "filter_less' (n1<n2) a1 a2 = (a1',a2') ⟹
n1 <: a1 ⟹ n2 <: a2 ⟹ n1 <: a1' ∧ n2 <: a2'"

datatype 'a up = bot | Up 'a

instantiation up :: (SL_top)SL_top
begin

fun le_up where
"Up x ⊑ Up y = (x ⊑ y)" |
"bot ⊑ y = True" |
"Up _ ⊑ bot = False"

lemma [simp]: "(x ⊑ bot) = (x = bot)"
by (cases x) simp_all

lemma [simp]: "(Up x ⊑ u) = (EX y. u = Up y & x ⊑ y)"
by (cases u) auto

fun join_up where
"Up x ⊔ Up y = Up(x ⊔ y)" |
"bot ⊔ y = y" |
"x ⊔ bot = x"

lemma [simp]: "x ⊔ bot = x"
by (cases x) simp_all

definition "Top = Up Top"

instance proof
case goal1 show ?case by(cases x, simp_all)
next
case goal2 thus ?case
by(cases z, simp, cases y, simp, cases x, auto intro: le_trans)
next
case goal3 thus ?case by(cases x, simp, cases y, simp_all)
next
case goal4 thus ?case by(cases y, simp, cases x, simp_all)
next
case goal5 thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
next
case goal6 thus ?case by(cases x, simp_all add: Top_up_def)
qed

end

locale Abs_Int1 = Val_abs1 +
fixes pfp :: "('a astate up ⇒ 'a astate up) ⇒ 'a astate up ⇒ 'a astate up"
assumes pfp: "f(pfp f x0) ⊑ pfp f x0"
assumes above: "x0 ⊑ pfp f x0"
begin

(* FIXME avoid duplicating this defn *)
abbreviation astate_in_rep (infix "<:" 50) where
"s <: S == ALL x. s x <: lookup S x"

abbreviation in_rep_up :: "state ⇒ 'a astate up ⇒ bool"  (infix "<::" 50) where
"s <:: S == EX S0. S = Up S0 ∧ s <: S0"

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

lemma in_rep_join_UpI: "s <:: S1 | s <:: S2 ⟹ s <:: S1 ⊔ S2"
by (metis in_rep_up_trans SL_top_class.join_ge1 SL_top_class.join_ge2)

fun aval' :: "aexp ⇒ 'a astate up ⇒ 'a" ("aval⇧#") where
"aval' _ bot = Bot" |
"aval' (N n) _ = num' n" |
"aval' (V x) (Up S) = lookup S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"

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

fun afilter :: "aexp ⇒ 'a ⇒ 'a astate up ⇒ 'a astate up" where
"afilter (N n) a S = (if n <: a then S else bot)" |
"afilter (V x) a S = (case S of bot ⇒ bot | Up S ⇒
let a' = lookup S x ⊓ a in
if a' ⊑ Bot then bot else Up(update S x a'))" |
"afilter (Plus e1 e2) a S =
(let (a1,a2) = filter_plus' a (aval' e1 S) (aval' e2 S)
in afilter e1 a1 (afilter e2 a2 S))"

text{* The test for @{const Bot} in the @{const V}-case is important: @{const
Bot} indicates that a variable has no possible values, i.e.\ that the current
program point is unreachable. But then the abstract state should collapse to
@{const bot}. Put differently, we maintain the invariant that in an abstract
state all variables are mapped to non-@{const Bot} values. Otherwise the
(pointwise) join of two abstract states, one of which contains @{const Bot}
values, may produce too large a result, thus making the analysis less
precise. *}

fun bfilter :: "bexp ⇒ bool ⇒ 'a astate up ⇒ 'a astate up" where
"bfilter (Bc v) res S = (if v=res then S else bot)" |
"bfilter (Not b) res S = bfilter b (¬ res) S" |
"bfilter (And b1 b2) res S =
(if res then bfilter b1 True (bfilter b2 True S)
else bfilter b1 False S ⊔ bfilter b2 False S)" |
"bfilter (Less e1 e2) res S =
(let (res1,res2) = filter_less' res (aval' e1 S) (aval' e2 S)
in afilter e1 res1 (afilter e2 res2 S))"

lemma afilter_sound: "s <:: S ⟹ aval e s <: a ⟹ s <:: afilter e a S"
proof(induction e arbitrary: a S)
case N thus ?case by simp
next
case (V x)
obtain S' where "S = Up S'" and "s <: S'" using `s <:: S` by auto
moreover hence "s x <: lookup S' x" by(simp)
moreover have "s x <: a" using V by simp
ultimately show ?case using V(1)
(metis le_rep emptyE in_rep_meet rep_Bot subset_empty)
next
case (Plus e1 e2) thus ?case
using filter_plus'[OF _ aval'_sound[OF Plus(3)] aval'_sound[OF Plus(3)]]
by (auto split: prod.split)
qed

lemma bfilter_sound: "s <:: S ⟹ bv = bval b s ⟹ s <:: bfilter b bv S"
proof(induction b arbitrary: S bv)
case Bc thus ?case by simp
next
case (Not b) thus ?case by simp
next
case (And b1 b2) thus ?case by (auto simp: in_rep_join_UpI)
next
case (Less e1 e2) thus ?case
apply hypsubst_thin
apply (auto split: prod.split)
apply (metis afilter_sound filter_less' aval'_sound Less)
done
qed

fun AI :: "com ⇒ 'a astate up ⇒ 'a astate up" where
"AI SKIP S = S" |
"AI (x ::= a) S =
(case S of bot ⇒ bot | Up S ⇒ Up(update S x (aval' a (Up S))))" |
"AI (c1;;c2) S = AI c2 (AI c1 S)" |
"AI (IF b THEN c1 ELSE c2) S =
AI c1 (bfilter b True S) ⊔ AI c2 (bfilter b False S)" |
"AI (WHILE b DO c) S =
bfilter b False (pfp (λS. AI c (bfilter b True S)) S)"

lemma AI_sound: "(c,s) ⇒ t ⟹ s <:: S ⟹ t <:: AI c S"
proof(induction c arbitrary: s t S)
case SKIP thus ?case by fastforce
next
case Assign thus ?case
by (auto simp: lookup_update aval'_sound)
next
case Seq thus ?case by fastforce
next
case If thus ?case by (auto simp: in_rep_join_UpI bfilter_sound)
next
case (While b c)
let ?P = "pfp (λS. AI c (bfilter b True S)) S"
{ fix s t
have "(WHILE b DO c,s) ⇒ t ⟹ s <:: ?P ⟹
t <:: bfilter b False ?P"
proof(induction "WHILE b DO c" s t rule: big_step_induct)
case WhileFalse thus ?case by(metis bfilter_sound)
next
case WhileTrue show ?case
by(rule WhileTrue, rule in_rep_up_trans[OF _ pfp],
rule While.IH[OF WhileTrue(2)],
rule bfilter_sound[OF WhileTrue.prems], simp add: WhileTrue(1))
qed
}
with in_rep_up_trans[OF `s <:: S` above] While(2,3) AI.simps(5)
show ?case by simp
qed

end

end
```