Theory Abs_Int1

(* Author: Tobias Nipkow *)

theory Abs_Int1
imports Abs_State
begin

lemma le_iff_le_annos_zip: "C1 \<sqsubseteq> C2 <->
 (∀ (a1,a2) ∈ set(zip (annos C1) (annos C2)). a1 \<sqsubseteq> a2) ∧ strip C1 = strip C2"
by(induct C1 C2 rule: le_acom.induct) (auto simp: size_annos_same2)

lemma le_iff_le_annos: "C1 \<sqsubseteq> C2 <->
  strip C1 = strip C2 ∧ (∀ i<size(annos C1). annos C1 ! i \<sqsubseteq> annos C2 ! i)"
by(auto simp add: le_iff_le_annos_zip set_zip) (metis size_annos_same2)


lemma mono_fun_L[simp]: "F ∈ L X ==> F \<sqsubseteq> G ==> x : X ==> fun F x \<sqsubseteq> fun G x"
by(simp add: mono_fun L_st_def)

lemma bot_in_L[simp]: "bot c ∈ L(vars c)"
by(simp add: L_acom_def bot_def)

lemma L_acom_simps[simp]: "SKIP {P} ∈ L X <-> P ∈ L X"
  "(x ::= e {P}) ∈ L X <-> x : X ∧ vars e ⊆ X ∧ P ∈ L X"
  "(C1;C2) ∈ L X <-> C1 ∈ L X ∧ C2 ∈ L X"
  "(IF b THEN {P1} C1 ELSE {P2} C2 {Q}) ∈ L X <->
   vars b ⊆ X ∧ C1 ∈ L X ∧ C2 ∈ L X ∧ P1 ∈ L X ∧ P2 ∈ L X ∧ Q ∈ L X"
  "({I} WHILE b DO {P} C {Q}) ∈ L X <->
   I ∈ L X ∧ vars b ⊆ X ∧ P ∈ L X ∧ C ∈ L X ∧ Q ∈ L X"
by(auto simp add: L_acom_def)

lemma post_in_annos: "post C : set(annos C)"
by(induction C) auto

lemma post_in_L[simp]: "C ∈ L X ==> post C ∈ L X"
by(simp add: L_acom_def post_in_annos)


subsection "Computable Abstract Interpretation"

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

context Gamma
begin

fun aval' :: "aexp => 'av st => 'av" where
"aval' (N i) S = num' i" |
"aval' (V x) S = fun S x" |
"aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)"

lemma aval'_sound: "s : γ⇣s S ==> vars a ⊆ dom S ==> aval a s : γ(aval' a S)"
by (induction a) (auto simp: gamma_num' gamma_plus' γ_st_def)

end

text{* The for-clause (here and elsewhere) only serves the purpose of fixing
the name of the type parameter @{typ 'av} which would otherwise be renamed to
@{typ 'a}. *}

locale Abs_Int = Gamma where γ=γ for γ :: "'av::semilattice => val set"
begin

fun step' :: "'av st option => 'av st option acom => 'av st option acom" where
"step' S (SKIP {P}) = (SKIP {S})" |
"step' S (x ::= e {P}) =
  x ::= e {case S of None => None | Some S => Some(update S x (aval' e S))}" |
"step' S (C1; C2) = step' S C1; step' (post C1) C2" |
"step' S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
  (IF b THEN {S} step' P1 C1 ELSE {S} step' P2 C2 {post C1 \<squnion> post C2})" |
"step' S ({I} WHILE b DO {P} C {Q}) =
   {S \<squnion> post C} WHILE b DO {I} step' P C {I}"

definition AI :: "com => 'av st option acom option" where
"AI c = pfp (step' (top c)) (bot c)"


lemma strip_step'[simp]: "strip(step' S C) = strip C"
by(induct C arbitrary: S) (simp_all add: Let_def)


text{* Soundness: *}

lemma in_gamma_update:
  "[| s : γ⇣s S; i : γ a |] ==> s(x := i) : γ⇣s(update S x a)"
by(simp add: γ_st_def)

lemma step_step': "C ∈ L X ==> S ∈ L X ==> step (γ⇣o S) (γ⇣c C) ≤ γ⇣c (step' S C)"
proof(induction C arbitrary: S)
  case SKIP thus ?case by auto
next
  case Assign thus ?case
    by (fastforce simp: L_st_def intro: aval'_sound in_gamma_update split: option.splits)
next
  case Seq thus ?case by auto
next
  case (If b p1 C1 p2 C2 P)
  hence "post C1 \<sqsubseteq> post C1 \<squnion> post C2 ∧ post C2 \<sqsubseteq> post C1 \<squnion> post C2"
    by(simp, metis post_in_L join_ge1 join_ge2)
  thus ?case using If by (auto simp: mono_gamma_o)
next
  case While thus ?case by (auto simp: mono_gamma_o)
qed

lemma step'_in_L[simp]:
  "[| C ∈ L X; S ∈ L X |] ==> (step' S C) ∈ L X"
proof(induction C arbitrary: S)
  case Assign thus ?case
    by(auto simp: L_st_def update_def split: option.splits)
qed auto

lemma AI_sound: "AI c = Some C ==> CS c ≤ γ⇣c C"
proof(simp add: CS_def AI_def)
  assume 1: "pfp (step' (top c)) (bot c) = Some C"
  have "C ∈ L(vars c)"
    by(rule pfp_inv[where P = "%C. C ∈ L(vars c)", OF 1 _ bot_in_L])
      (erule step'_in_L[OF _ top_in_L])
  have pfp': "step' (top c) C \<sqsubseteq> C" by(rule pfp_pfp[OF 1])
  have 2: "step (γ⇣o(top c)) (γ⇣c C) ≤ γ⇣c C"
  proof(rule order_trans)
    show "step (γ⇣o (top c)) (γ⇣c C) ≤  γ⇣c (step' (top c) C)"
      by(rule step_step'[OF `C ∈ L(vars c)` top_in_L])
    show "γ⇣c (step' (top c) C) ≤ γ⇣c C"
      by(rule mono_gamma_c[OF pfp'])
  qed
  have 3: "strip (γ⇣c C) = c" by(simp add: strip_pfp[OF _ 1])
  have "lfp c (step (γ⇣o(top c))) ≤ γ⇣c C"
    by(rule lfp_lowerbound[simplified,where f="step (γ⇣o(top c))", OF 3 2])
  thus "lfp c (step UNIV) ≤ γ⇣c C" by simp
qed

end


subsubsection "Monotonicity"

lemma le_join_disj: "y ∈ L X ==> (z::_::semilatticeL) ∈ L X ==>
  x \<sqsubseteq> y ∨ x \<sqsubseteq> z ==> x \<sqsubseteq> y \<squnion> z"
by (metis join_ge1 join_ge2 preord_class.le_trans)

locale Abs_Int_mono = Abs_Int +
assumes mono_plus': "a1 \<sqsubseteq> b1 ==> a2 \<sqsubseteq> b2 ==> plus' a1 a2 \<sqsubseteq> plus' b1 b2"
begin

lemma mono_aval':
  "S1 \<sqsubseteq> S2 ==> S1 ∈ L X ==> S2 ∈ L X ==> vars e ⊆ X ==> aval' e S1 \<sqsubseteq> aval' e S2"
by(induction e) (auto simp: le_st_def mono_plus' L_st_def)

theorem mono_step': "S1 ∈ L X ==> S2 ∈ L X ==> C1 ∈ L X ==> C2 ∈ L X ==>
  S1 \<sqsubseteq> S2 ==> C1 \<sqsubseteq> C2 ==> step' S1 C1 \<sqsubseteq> step' S2 C2"
apply(induction C1 C2 arbitrary: S1 S2 rule: le_acom.induct)
apply (auto simp: Let_def mono_aval' mono_post
  le_join_disj le_join_disj[OF  post_in_L post_in_L]
            split: option.split)
done

lemma mono_step'_top: "C ∈ L(vars c) ==> C' ∈ L(vars c) ==>
  C \<sqsubseteq> C' ==> step' (top c) C \<sqsubseteq> step' (top c) C'"
by (metis top_in_L mono_step' preord_class.le_refl)

lemma pfp_bot_least:
assumes "∀x∈L(vars c)∩{C. strip C = c}.∀y∈L(vars c)∩{C. strip C = c}.
  x \<sqsubseteq> y --> f x \<sqsubseteq> f y"
and "∀C. C ∈ L(vars c)∩{C. strip C = c} --> f C ∈ L(vars c)∩{C. strip C = c}"
and "f C' \<sqsubseteq> C'" "strip C' = c" "C' ∈ L(vars c)" "pfp f (bot c) = Some C"
shows "C \<sqsubseteq> C'"
apply(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(6)[unfolded pfp_def]])
by (simp_all add: assms(4,5) bot_least)

lemma AI_least_pfp: assumes "AI c = Some C"
and "step' (top c) C' \<sqsubseteq> C'" "strip C' = c" "C' ∈ L(vars c)"
shows "C \<sqsubseteq> C'"
apply(rule pfp_bot_least[OF _ _ assms(2-4) assms(1)[unfolded AI_def]])
by (simp_all add: mono_step'_top)

end


subsubsection "Termination"

abbreviation sqless (infix "\<sqsubset>" 50) where
"x \<sqsubset> y == x \<sqsubseteq> y ∧ ¬ y \<sqsubseteq> x"

lemma pfp_termination:
fixes x0 :: "'a::preord" and m :: "'a => nat"
assumes mono: "!!x y. I x ==> I y ==> x \<sqsubseteq> y ==> f x \<sqsubseteq> f y"
and m: "!!x y. I x ==> I y ==> x \<sqsubset> y ==> m x > m y"
and I: "!!x y. I x ==> I(f x)" and "I x0" and "x0 \<sqsubseteq> f x0"
shows "∃x. pfp f x0 = Some x"
proof(simp add: pfp_def, rule wf_while_option_Some[where P = "%x. I x & x \<sqsubseteq> f x"])
  show "wf {(y,x). ((I x ∧ x \<sqsubseteq> f x) ∧ ¬ f x \<sqsubseteq> x) ∧ y = f x}"
    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
next
  show "I x0 ∧ x0 \<sqsubseteq> f x0" using `I x0` `x0 \<sqsubseteq> f x0` by blast
next
  fix x assume "I x ∧ x \<sqsubseteq> f x" thus "I(f x) ∧ f x \<sqsubseteq> f(f x)"
    by (blast intro: I mono)
qed


locale Measure1 =
fixes m :: "'av::preord => nat"
fixes h :: "nat"
assumes m1: "x \<sqsubseteq> y ==> m x ≥ m y"
assumes h: "m x ≤ h"
begin

definition m_s :: "'av st => nat" ("m⇣s") where
"m_s S = (∑ x ∈ dom S. m(fun S x))"

lemma m_s_h: "x ∈ L X ==> finite X ==> m_s x ≤ h * card X"
by(simp add: L_st_def m_s_def)
  (metis nat_mult_commute of_nat_id setsum_bounded[OF h])

lemma m_s1: "S1 \<sqsubseteq> S2 ==> m_s S1 ≥ m_s S2"
proof(auto simp add: le_st_def m_s_def)
  assume "∀x∈dom S2. fun S1 x \<sqsubseteq> fun S2 x"
  hence "∀x∈dom S2. m(fun S1 x) ≥ m(fun S2 x)" by (metis m1)
  thus "(∑x∈dom S2. m (fun S2 x)) ≤ (∑x∈dom S2. m (fun S1 x))"
    by (metis setsum_mono)
qed

definition m_o :: "nat => 'av st option => nat" ("m⇣o") where
"m_o d opt = (case opt of None => h*d+1 | Some S => m_s S)"

lemma m_o_h: "ost ∈ L X ==> finite X ==> m_o (card X) ost ≤ (h*card X + 1)"
by(auto simp add: m_o_def m_s_h split: option.split dest!:m_s_h)

lemma m_o1: "finite X ==> o1 ∈ L X ==> o2 ∈ L X ==>
  o1 \<sqsubseteq> o2 ==> m_o (card X) o1 ≥ m_o (card X) o2"
proof(induction o1 o2 rule: le_option.induct)
  case 1 thus ?case by (simp add: m_o_def)(metis m_s1)
next
  case 2 thus ?case
    by(simp add: L_option_def m_o_def le_SucI m_s_h split: option.splits)
next
  case 3 thus ?case by simp
qed

definition m_c :: "'av st option acom => nat" ("m⇣c") where
"m_c C = (∑i<size(annos C). m_o (card(vars(strip C))) (annos C ! i))"

lemma m_c_h: assumes "C ∈ L(vars(strip C))"
shows "m_c C ≤ size(annos C) * (h * card(vars(strip C)) + 1)"
proof-
  let ?X = "vars(strip C)" let ?n = "card ?X" let ?a = "size(annos C)"
  { fix i assume "i < ?a"
    hence "annos C ! i ∈ L ?X" using assms by(simp add: L_acom_def)
    note m_o_h[OF this finite_cvars]
  } note 1 = this
  have "m_c C = (∑i<?a. m_o ?n (annos C ! i))" by(simp add: m_c_def)
  also have "… ≤ (∑i<?a. h * ?n + 1)"
    apply(rule setsum_mono) using 1 by simp
  also have "… = ?a * (h * ?n + 1)" by simp
  finally show ?thesis .
qed

end

locale Measure = Measure1 +
assumes m2: "x \<sqsubset> y ==> m x > m y"
begin

lemma m_s2: "finite(dom S1) ==> S1 \<sqsubset> S2 ==> m_s S1 > m_s S2"
proof(auto simp add: le_st_def m_s_def)
  assume "finite(dom S2)" and 0: "∀x∈dom S2. fun S1 x \<sqsubseteq> fun S2 x"
  hence 1: "∀x∈dom S2. m(fun S1 x) ≥ m(fun S2 x)" by (metis m1)
  fix x assume "x ∈ dom S2" "¬ fun S2 x \<sqsubseteq> fun S1 x"
  hence 2: "∃x∈dom S2. m(fun S1 x) > m(fun S2 x)" using 0 m2 by blast
  from setsum_strict_mono_ex1[OF `finite(dom S2)` 1 2]
  show "(∑x∈dom S2. m (fun S2 x)) < (∑x∈dom S2. m (fun S1 x))" .
qed

lemma m_o2: "finite X ==> o1 ∈ L X ==> o2 ∈ L X ==>
  o1 \<sqsubset> o2 ==> m_o (card X) o1 > m_o (card X) o2"
proof(induction o1 o2 rule: le_option.induct)
  case 1 thus ?case by (simp add: m_o_def L_st_def m_s2)
next
  case 2 thus ?case
    by(auto simp add: m_o_def le_imp_less_Suc m_s_h)
next
  case 3 thus ?case by simp
qed


lemma m_c2: "C1 ∈ L(vars(strip C1)) ==> C2 ∈ L(vars(strip C2)) ==>
  C1 \<sqsubset> C2 ==> m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos m_c_def size_annos_same[of C1 C2] L_acom_def)
  let ?X = "vars(strip C2)"
  let ?n = "card ?X"
  assume V1: "∀a∈set(annos C1). a ∈ L ?X"
    and V2: "∀a∈set(annos C2). a ∈ L ?X"
    and strip_eq: "strip C1 = strip C2"
    and 0: "∀i<size(annos C2). annos C1 ! i \<sqsubseteq> annos C2 ! i"
  hence 1: "∀i<size(annos C2). m_o ?n (annos C1 ! i) ≥ m_o ?n (annos C2 ! i)"
    by (auto simp: all_set_conv_all_nth)
       (metis finite_cvars m_o1 size_annos_same2)
  fix i assume "i < size(annos C2)" "¬ annos C2 ! i \<sqsubseteq> annos C1 ! i"
  hence "m_o ?n (annos C1 ! i) > m_o ?n (annos C2 ! i)" (is "?P i")
    by(metis m_o2[OF finite_cvars] V1 V2 nth_mem size_annos_same[OF strip_eq] 0)
  hence 2: "∃i < size(annos C2). ?P i" using `i < size(annos C2)` by blast
  show "(∑i<size(annos C2). m_o ?n (annos C2 ! i))
         < (∑i<size(annos C2). m_o ?n (annos C1 ! i))"
    apply(rule setsum_strict_mono_ex1) using 1 2 by (auto)
qed

end

locale Abs_Int_measure =
  Abs_Int_mono where γ=γ + Measure where m=m
  for γ :: "'av::semilattice => val set" and m :: "'av => nat"
begin

lemma AI_Some_measure: "∃C. AI c = Some C"
unfolding AI_def
apply(rule pfp_termination[where I = "%C. strip C = c ∧ C ∈ L(vars c)"
  and m="m_c"])
apply(simp_all add: m_c2 mono_step'_top bot_least)
done

end

end