Quelle  Abs_Int0.thy

(* Author: Tobias Nipkow *)

subsection "Abstract Interpretation"

theory Abs_Int0
imports Abs_Int_init
begin

subsubsection "Orderings"

text‹The basic type classes 🚫‹order›, 🚫‹semilattice_sup› and 🚫‹order_top› are
  in 🚫‹Main›, more precisely in theories 🚫‹HOL.Orderings› and 🚫‹HOL.Lattices›.
  you view this theory with jedit, just click on the names to get there.›

class semilattice_sup_top = semilattice_sup + order_top


instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..

instantiation option :: (order)order
begin

fun less_eq_option where
"Some x ≤ Some y = (x ≤ y)" |
"None ≤ y = True" |
"Some _ ≤ None = False"

definition less_option where "x < (y::'a option) = (x ≤ y ∧ ¬ y ≤ x)"

lemma le_None[simp]: "(x ≤ None) = (x = None)"
by (cases x) simp_all

lemma Some_le[simp]: "(Some x ≤ u) = (∃y. u = Some y ∧ x ≤ y)"
by (cases u) auto

instance
proof (standard, goal_cases)
  case 1 show ?case by(rule less_option_def)
next
  case (2 x) show ?case by(cases x, simp_all)
next
  case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, auto)
next
  case (4 x y) thus ?case by(cases y, simp, cases x, auto)
qed

end

instantiation option :: (sup)sup
begin

fun sup_option where
"Some x ⊔ Some y = Some(x ⊔ y)" |
"None ⊔ y = y" |
"x ⊔ None = x"

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

instance ..

end

instantiation option :: (semilattice_sup_top)semilattice_sup_top
begin

definition top_option where "⊤ = Some ⊤"

instance
proof (standard, goal_cases)
  case (4 a) show ?case by(cases a, simp_all add: top_option_def)
next
  case (1 x y) thus ?case by(cases x, simp, cases y, simp_all)
next
  case (2 x y) thus ?case by(cases y, simp, cases x, simp_all)
next
  case (3 x y z) thus ?case by(cases z, simp, cases y, simp, cases x, simp_all)
qed

end

lemma [simp]: "(Some x < Some y) = (x < y)"
by(auto simp: less_le)

instantiation option :: (order)order_bot
begin

definition bot_option :: "'a option" where
"⊥ = None"

instance
proof (standard, goal_cases)
  case 1 thus ?case by(auto simp: bot_option_def)
qed

end


definition bot :: "com → 'a option acom" where
"bot c = annotate (λp. None) c"

lemma bot_least: "strip C = c ==> bot c ≤ C"
by(auto simp: bot_def less_eq_acom_def)

lemma strip_bot[simp]: "strip(bot c) = c"
by(simp add: bot_def)


subsubsection "Pre-fixpoint iteration"

definition pfp :: "(('a::order) → 'a) → 'a → 'a option" where
"pfp f = while_option (λx. ¬ f x ≤ x) f"

lemma pfp_pfp: assumes "pfp f x0 = Some x" shows "f x ≤ x"
using while_option_stop[OF assms[simplified pfp_def]] by simp

lemma while_least:
fixes q :: "'a::order"
assumes "∀x∈L.∀y∈L. x ≤ y ⟶ f x ≤ f y" and "∀x. x ∈ L ⟶ f x ∈ L"
and "∀x ∈ L. b ≤ x" and "b ∈ L" and "f q ≤ q" and "q ∈ L"
and "while_option P f b = Some p"
shows "p ≤ q"
using while_option_rule[OF _  assms(7)[unfolded pfp_def],
                        where P = "%x. x ∈ L ∧ x ≤ q"]
by (metis assms(1-6) order_trans)

lemma pfp_bot_least:
assumes "∀x∈{C. strip C = c}.∀y∈{C. strip C = c}. x ≤ y ⟶ f x ≤ f y"
and "∀C. C ∈ {C. strip C = c} ⟶ f C ∈ {C. strip C = c}"
and "f C' ≤ C'" "strip C' = c" "pfp f (bot c) = Some C"
shows "C ≤ C'"
by(rule while_least[OF assms(1,2) _ _ assms(3) _ assms(5)[unfolded pfp_def]])
  (simp_all add: assms(4) bot_least)

lemma pfp_inv:
  "pfp f x = Some y ==> (∧x. P x ==> P(f x)) ==> P x ==> P y"
unfolding pfp_def by (blast intro: while_option_rule)

lemma strip_pfp:
assumes "∧x. g(f x) = g x" and "pfp f x0 = Some x" shows "g x = g x0"
using pfp_inv[OF assms(2), where P = "%x. g x = g x0"] assms(1) by simp


subsubsection "Abstract Interpretation"

definition γ_fun :: "('a → 'b set) → ('c → 'a) → ('c → 'b)set" where
"γ_fun γ F = {f. ∀x. f x ∈ γ(F x)}"

fun γ_option :: "('a → 'b set) → 'a option → 'b set" where
"γ_option γ None = {}" |
"γ_option γ (Some a) = γ a"

text‹The interface for abstract values:›

locale Val_semilattice =
fixes γ :: "'av::semilattice_sup_top → val set"
  assumes mono_gamma: "a ≤ b ==> γ a ≤ γ b"
  and gamma_Top[simp]: "γ ⊤ = UNIV"
fixes num' :: "val → 'av"
and plus' :: "'av → 'av → 'av"
  assumes gamma_num': "i ∈ γ(num' i)"
  and gamma_plus': "i1 ∈ γ a1 ==> i2 ∈ γ a2 ==> i1+i2 ∈ γ(plus' a1 a2)"

type_synonym 'av st = "(vname → 'av)"

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

locale Abs_Int_fun = Val_semilattice where γ=γ
  for γ :: "'av::semilattice_sup_top → val set"
begin

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

definition "asem x e S = (case S of None → None | Some S → Some(S(x := aval' e S)))"

definition "step' = Step asem (λb S. S)"

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

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


abbreviation γ_s :: "'av st → state set"
where "γ_s == γ_fun γ"

abbreviation γ_o :: "'av st option → state set"
where "γ_o == γ_option γ_s"

abbreviation γ_c :: "'av st option acom → state set acom"
where "γ_c == map_acom γ_o"

lemma gamma_s_Top[simp]: "γ_s ⊤ = UNIV"
by(simp add: top_fun_def γ_fun_def)

lemma gamma_o_Top[simp]: "γ_o ⊤ = UNIV"
by (simp add: top_option_def)

lemma mono_gamma_s: "f1 ≤ f2 ==> γ_s f1 ⊆ γ_s f2"
by(auto simp: le_fun_def γ_fun_def dest: mono_gamma)

lemma mono_gamma_o:
  "S1 ≤ S2 ==> γ_o S1 ⊆ γ_o S2"
by(induction S1 S2 rule: less_eq_option.induct)(simp_all add: mono_gamma_s)

lemma mono_gamma_c: "C1 ≤ C2 ==> γ_c C1 ≤ γ_c C2"
by (simp add: less_eq_acom_def mono_gamma_o size_annos anno_map_acom size_annos_same[of C1 C2])

text‹Correctness:›

lemma aval'_correct: "s ∈ γ_s S ==> aval a s ∈ γ(aval' a S)"
by (induct a) (auto simp: gamma_num' gamma_plus' γ_fun_def)

lemma in_gamma_update: "[ s ∈ γ_s S; i ∈ γ a ] ==> s(x := i) ∈ γ_s(S(x := a))"
by(simp add: γ_fun_def)

lemma gamma_Step_subcomm:
  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)"
by (induction C arbitrary: S) (auto simp: mono_gamma_o assms)

lemma step_step': "step (γ_o S) (γ_c C) ≤ γ_c (step' S C)"
unfolding step_def step'_def
by(rule gamma_Step_subcomm)
  (auto simp: aval'_correct in_gamma_update asem_def 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'])
  qed
  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
qed

end


subsubsection "Monotonicity"

locale Abs_Int_fun_mono = Abs_Int_fun +
assumes mono_plus': "a1 ≤ b1 ==> a2 ≤ b2 ==> plus' a1 a2 ≤ plus' b1 b2"
begin

lemma mono_aval': "S ≤ S' ==> aval' e S ≤ aval' e S'"
by(induction e)(auto simp: le_fun_def mono_plus')

lemma mono_update: "a ≤ a' ==> S ≤ S' ==> S(x := a) ≤ S'(x := a')"
by(simp add: le_fun_def)

lemma mono_step': "S1 ≤ S2 ==> C1 ≤ C2 ==> step' S1 C1 ≤ step' S2 C2"
unfolding step'_def
by(rule mono2_Step)
  (auto simp: mono_update mono_aval' asem_def 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)

end


instantiation acom :: (type) vars
begin

definition "vars_acom = vars o strip"

instance ..

end

lemma finite_Cvars: "finite(vars(C::'a acom))"
by(simp add: vars_acom_def)


subsubsection "Termination"

lemma pfp_termination:
fixes x0 :: "'a::order" and m :: "'a → nat"
assumes mono: "∧x y. I x ==> I y ==> x ≤ y ==> f x ≤ f y"
and m: "∧x y. I x ==> I y ==> x < y ==> m x > m y"
and I: "∧x y. I x ==> I(f x)" and "I x0" and "x0 ≤ 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 ≤ f x"])
  show "wf {(y,x). ((I x ∧ x ≤ f x) ∧ ¬ f x ≤ x) ∧ y = f x}"
    by(rule wf_subset[OF wf_measure[of m]]) (auto simp: m I)
next
  show "I x0 ∧ x0 ≤ f x0" using ‹I x0› ‹x0 ≤ f x0› by blast
next
  fix x assume "I x ∧ x ≤ f x" thus "I(f x) ∧ f x ≤ f(f x)"
    by (blast intro: I mono)
qed

lemma le_iff_le_annos: "C1 ≤ C2 ⟷
  strip C1 = strip C2 ∧ (∀ i<size(annos C1). annos C1 ! i ≤ annos C2 ! i)"
by(simp add: less_eq_acom_def anno_def)

locale Measure1_fun =
fixes m :: "'av::top → nat"
fixes h :: "nat"
assumes h: "m x ≤ h"
begin

definition m_s :: "'av st → vname set → nat" (‹m_s›) where
"m_s S X = (∑ x ∈ X. m(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])

fun m_o :: "'av st option → vname set → nat" (‹m_o›) where
"m_o (Some S) X = m_s S X" |
"m_o None X = h * card X + 1"

lemma m_o_h: "finite X ==> m_o opt X ≤ (h*card X + 1)"
by(cases opt)(auto simp add: m_s_h le_SucI dest: m_s_h)

definition m_c :: "'av st option acom → nat" (‹m_c›) 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)"
proof-
  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 .
qed

end


locale Measure_fun = Measure1_fun where m=m
  for m :: "'av::semilattice_sup_top → nat" +
assumes m2: "x < y ==> m x > m y"
begin

text‹The predicates ‹top_on_ty a X› that follow describe that any abstract
  in ‹a› maps all variables in ‹X› to term‹⊤›.
  is an important invariant for the termination proof where we argue that only
  finitely many variables in the program change. That the others do not change
  because they remain term‹⊤›.›

fun top_on_st :: "'av st → vname set → bool" (‹top'_on_s›) where
"top_on_st S X = (∀x∈X. S x = ⊤)"

fun top_on_opt :: "'av st option → vname set → bool" (‹top'_on_o›) where
"top_on_opt (Some S) X = top_on_st S X" |
"top_on_opt None X = True"

definition top_on_acom :: "'av st option acom → vname set → bool" (‹top'_on_c›) where
"top_on_acom C X = (∀a ∈ set(annos C). top_on_opt a X)"

lemma top_on_top: "top_on_opt ⊤ X"
by(auto simp: top_option_def)

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) X"
apply(induction o1 o2 rule: sup_option.induct)
apply(auto)
done

lemma top_on_Step: fixes C :: "'av 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)

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 "(∑x∈X. m (S2 x)) < (∑x∈X. m (S1 x))"
proof-
  from assms(3) have 1: "∀x∈X. m(S1 x) ≥ m(S2 x)" by (simp add: m1)
  from assms(2,3,4) have "∃x∈X. S1 x < S2 x"
    by(simp add: fun_eq_iff) (metis Compl_iff le_neq_trans)
  hence 2: "∃x∈X. m(S1 x) > m(S2 x)" by (metis m2)
  from sum_strict_mono_ex1[OF ‹finite X› 1 2]
  show "(∑x∈X. m (S2 x)) < (∑x∈X. m (S1 x))" .
qed

lemma m_s2: "finite(X) ==> S1 = S2 on -X ==> S1 < S2 ==> m_s S1 X > m_s S2 X"
apply(auto simp add: less_fun_def m_s_def)
apply(simp add: m_s2_rep le_fun_def)
done

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_s2 less_option_def)
next
  case 2 thus ?case by(auto simp: less_option_def le_imp_less_Suc m_s_h)
next
  case 3 thus ?case by (auto simp: less_option_def)
qed

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 (lifting, no_types) 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])
qed

end


locale Abs_Int_fun_measure =
  Abs_Int_fun_mono where γ=γ + Measure_fun where m=m
  for γ :: "'av::semilattice_sup_top → val set" and m :: "'av → nat"
begin

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 asem_def 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)
done

end

text‹Problem: not executable because of the comparison of abstract states,
 .e. functions, in the pre-fixpoint computation.›

end