Theory Abs_Int1

(* Author: Tobias Nipkow *)

subsection "Computable Abstract Interpretation"

theory Abs_Int1
imports Abs_State

text‹Abstract interpretation over type st› instead of functions.›

context Gamma_semilattice

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'_correct: "s  γs S  aval a s  γ(aval' a S)"
by (induction a) (auto simp: gamma_num' gamma_plus' γ_st_def)

lemma gamma_Step_subcomm: fixes C1 C2 :: "'a::semilattice_sup acom"
  assumes "!!x e S. f1 x e (γo S)  γo (f2 x e S)"
          "!!b S. g1 b (γo S)  γo (g2 b S)"
  shows "Step f1 g1 (γo S) (γc C)  γc (Step f2 g2 S C)"
proof(induction C arbitrary: S)
qed (auto simp: assms intro!: mono_gamma_o sup_ge1 sup_ge2)

lemma in_gamma_update: " s  γs S; i  γ a   s(x := i)  γs(update S x a)"
by(simp add: γ_st_def)


locale Abs_Int = Gamma_semilattice where γ=γ
  for γ :: "'av::semilattice_sup_top  val set"

definition "step' = Step
  (λx e S. case S of None  None | Some S  Some(update S x (aval' e S)))
  (λb S. S)"

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

lemma strip_step'[simp]: "strip(step' S C) = strip C"
by(simp add: step'_def)


lemma step_step': "step (γo S) (γc C)  γc (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
  (auto simp: intro!: aval'_correct in_gamma_update split: option.splits)

lemma AI_correct: "AI c = Some C  CS c  γc C"
proof(simp add: CS_def AI_def)
  assume 1: "pfp (step' ) (bot c) = Some C"
  have pfp': "step'  C  C" by(rule pfp_pfp[OF 1])
  have 2: "step (γo ) (γc C)  γc C"  ― ‹transfer the pfp'›
  proof(rule order_trans)
    show "step (γo ) (γc C)  γc (step'  C)" by(rule step_step')
    show "...  γc C" by (metis mono_gamma_c[OF pfp'])
  have 3: "strip (γc C) = c" by(simp add: strip_pfp[OF _ 1] step'_def)
  have "lfp c (step (γo ))  γc C"
    by(rule lfp_lowerbound[simplified,where f="step (γo )", OF 3 2])
  thus "lfp c (step UNIV)  γc C" by simp


subsubsection "Monotonicity"

locale Abs_Int_mono = Abs_Int +
assumes mono_plus': "a1  b1  a2  b2  plus' a1 a2  plus' b1 b2"

lemma mono_aval': "S1  S2  aval' e S1  aval' e S2"
by(induction e) (auto simp: mono_plus' mono_fun)

theorem mono_step': "S1  S2  C1  C2  step' S1 C1  step' S2 C2"
unfolding step'_def
by(rule mono2_Step) (auto simp: mono_aval' split: option.split)

lemma mono_step'_top: "C  C'  step'  C  step'  C'"
by (metis mono_step' order_refl)

lemma AI_least_pfp: assumes "AI c = Some C" "step'  C'  C'" "strip C' = c"
shows "C  C'"
by(rule pfp_bot_least[OF _ _ assms(2,3) assms(1)[unfolded AI_def]])
  (simp_all add: mono_step'_top)


subsubsection "Termination"

locale Measure1 =
fixes m :: "'av::order_top  nat"
fixes h :: "nat"
assumes h: "m x  h"

definition m_s :: "'av st  vname set  nat" ("ms") where
"m_s S X = ( x  X. m(fun S x))"

lemma m_s_h: "finite X  m_s S X  h * card X"
by(simp add: m_s_def) (metis mult.commute of_nat_id sum_bounded_above[OF h])

definition m_o :: "'av st option  vname set  nat" ("mo") where
"m_o opt X = (case opt of None  h * card X + 1 | Some S  m_s S X)"

lemma m_o_h: "finite X  m_o opt X  (h*card X + 1)"
by(auto simp add: m_o_def m_s_h le_SucI split: option.split dest:m_s_h)

definition m_c :: "'av st option acom  nat" ("mc") where
"m_c C = sum_list (map (λa. m_o a (vars C)) (annos C))"

text‹Upper complexity bound:›
lemma m_c_h: "m_c C  size(annos C) * (h * card(vars C) + 1)"
  let ?X = "vars C" let ?n = "card ?X" let ?a = "size(annos C)"
  have "m_c C = (i<?a. m_o (annos C ! i) ?X)"
    by(simp add: m_c_def sum_list_sum_nth atLeast0LessThan)
  also have "  (i<?a. h * ?n + 1)"
    apply(rule sum_mono) using m_o_h[OF finite_Cvars] by simp
  also have " = ?a * (h * ?n + 1)" by simp
  finally show ?thesis .


fun top_on_st :: "'a::order_top st  vname set  bool" ("top'_ons") where
"top_on_st S X = (xX. fun S x = )"

fun top_on_opt :: "'a::order_top st option  vname set  bool" ("top'_ono") where
"top_on_opt (Some S)  X = top_on_st S X" |
"top_on_opt None X = True"

definition top_on_acom :: "'a::order_top st option acom  vname set  bool" ("top'_onc") where
"top_on_acom C X = (a  set(annos C). top_on_opt a X)"

lemma top_on_top: "top_on_opt (::_ st option) X"
by(auto simp: top_option_def fun_top)

lemma top_on_bot: "top_on_acom (bot c) X"
by(auto simp add: top_on_acom_def bot_def)

lemma top_on_post: "top_on_acom C X  top_on_opt (post C) X"
by(simp add: top_on_acom_def post_in_annos)

lemma top_on_acom_simps:
  "top_on_acom (SKIP {Q}) X = top_on_opt Q X"
  "top_on_acom (x ::= e {Q}) X = top_on_opt Q X"
  "top_on_acom (C1;;C2) X = (top_on_acom C1 X  top_on_acom C2 X)"
  "top_on_acom (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) X =
   (top_on_opt P1 X  top_on_acom C1 X  top_on_opt P2 X  top_on_acom C2 X  top_on_opt Q X)"
  "top_on_acom ({I} WHILE b DO {P} C {Q}) X =
   (top_on_opt I X  top_on_acom C X  top_on_opt P X  top_on_opt Q X)"
by(auto simp add: top_on_acom_def)

lemma top_on_sup:
  "top_on_opt o1 X  top_on_opt o2 X  top_on_opt (o1  o2 :: _ st option) X"
apply(induction o1 o2 rule: sup_option.induct)
by transfer simp

lemma top_on_Step: fixes C :: "('a::semilattice_sup_top)st option acom"
assumes "!!x e S. top_on_opt S X; x  X; vars e  -X  top_on_opt (f x e S) X"
        "!!b S. top_on_opt S X  vars b  -X  top_on_opt (g b S) X"
shows " vars C  -X; top_on_opt S X; top_on_acom C X   top_on_acom (Step f g S C) X"
proof(induction C arbitrary: S)
qed (auto simp: top_on_acom_simps vars_acom_def top_on_post top_on_sup assms)

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

lemma m1: "x  y  m x  m y"
by(auto simp: le_less m2)

lemma m_s2_rep: assumes "finite(X)" and "S1 = S2 on -X" and "x. S1 x  S2 x" and "S1  S2"
shows "(xX. m (S2 x)) < (xX. m (S1 x))"
  from assms(3) have 1: "xX. m(S1 x)  m(S2 x)" by (simp add: m1)
  from assms(2,3,4) have "xX. S1 x < S2 x"
    by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
  hence 2: "xX. m(S1 x) > m(S2 x)" by (metis m2)
  from sum_strict_mono_ex1[OF finite X 1 2]
  show "(xX. m (S2 x)) < (xX. m (S1 x))" .

lemma m_s2: "finite(X)  fun S1 = fun S2 on -X
   S1 < S2  m_s S1 X > m_s S2 X"
apply(auto simp add: less_st_def m_s_def)
apply (transfer fixing: m)
apply(simp add: less_eq_st_rep_iff eq_st_def m_s2_rep)

lemma m_o2: "finite X  top_on_opt o1 (-X)  top_on_opt o2 (-X) 
  o1 < o2  m_o o1 X > m_o o2 X"
proof(induction o1 o2 rule: less_eq_option.induct)
  case 1 thus ?case by (auto simp: m_o_def m_s2 less_option_def)
  case 2 thus ?case by(auto simp: m_o_def less_option_def le_imp_less_Suc m_s_h)
  case 3 thus ?case by (auto simp: less_option_def)

lemma m_o1: "finite X  top_on_opt o1 (-X)  top_on_opt o2 (-X) 
  o1  o2  m_o o1 X  m_o o2 X"
by(auto simp: le_less m_o2)

lemma m_c2: "top_on_acom C1 (-vars C1)  top_on_acom C2 (-vars C2) 
  C1 < C2  m_c C1 > m_c C2"
proof(auto simp add: le_iff_le_annos size_annos_same[of C1 C2] vars_acom_def less_acom_def)
  let ?X = "vars(strip C2)"
  assume top: "top_on_acom C1 (- vars(strip C2))"  "top_on_acom C2 (- vars(strip C2))"
  and strip_eq: "strip C1 = strip C2"
  and 0: "i<size(annos C2). annos C1 ! i  annos C2 ! i"
  hence 1: "i<size(annos C2). m_o (annos C1 ! i) ?X  m_o (annos C2 ! i) ?X"
    apply (auto simp: all_set_conv_all_nth vars_acom_def top_on_acom_def)
    by (metis finite_cvars m_o1 size_annos_same2)
  fix i assume i: "i < size(annos C2)" "¬ annos C2 ! i  annos C1 ! i"
  have topo1: "top_on_opt (annos C1 ! i) (- ?X)"
    using i(1) top(1) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
  have topo2: "top_on_opt (annos C2 ! i) (- ?X)"
    using i(1) top(2) by(simp add: top_on_acom_def size_annos_same[OF strip_eq])
  from i have "m_o (annos C1 ! i) ?X > m_o (annos C2 ! i) ?X" (is "?P i")
    by (metis 0 less_option_def m_o2[OF finite_cvars topo1] topo2)
  hence 2: "i < size(annos C2). ?P i" using i < size(annos C2) by blast
  have "(i<size(annos C2). m_o (annos C2 ! i) ?X)
         < (i<size(annos C2). m_o (annos C1 ! i) ?X)"
    apply(rule sum_strict_mono_ex1) using 1 2 by (auto)
  thus ?thesis
    by(simp add: m_c_def vars_acom_def strip_eq sum_list_sum_nth atLeast0LessThan size_annos_same[OF strip_eq])


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

lemma top_on_step': " top_on_acom C (-vars C)   top_on_acom (step'  C) (-vars C)"
unfolding step'_def
by(rule top_on_Step)
  (auto simp add: top_option_def fun_top split: option.splits)

lemma AI_Some_measure: "C. AI c = Some C"
unfolding AI_def
apply(rule pfp_termination[where I = "λC. top_on_acom C (- vars C)" and m="m_c"])
apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
using top_on_step' apply(auto simp add: vars_acom_def)