Theory Acyclicity

theory Acyclicity
  imports Main
begin


section ‹Acyclicity›

text ‹ Two of the discussed bounding algorithms ("top-down" and "bottom-up") exploit acyclicity
of the system under projection on sets of state variables closed under mutual variable dependency. 
[Abdulaziz et al., p.11] 

This specific notion of acyclicity is formalised using topologically sorted dependency graphs 
induced by the variable dependency relation. [Abdulaziz et al., p.14]›


subsection "Topological Sorting of Dependency Graphs"

― ‹NOTE name shortened.›
― ‹NOTE using 'fun' because of multiple defining equations.› 
fun top_sorted_abs where
  "top_sorted_abs R [] = True"
| "top_sorted_abs R (h # l) = (list_all (λx. ¬R x h) l ∧ top_sorted_abs R l)"


lemma top_sorted_abs_mem: 
  assumes "(top_sorted_abs R (h # l))" "(ListMem x l)"
  shows "(¬ R x h)"
  using assms
  by (auto simp add: ListMem_iff list.pred_set)


lemma top_sorted_cons: 
  assumes "top_sorted_abs R (h # l)"
  shows "(top_sorted_abs R l)"
  using assms
  by simp


subsection ‹The Weightiest Path Function (wlp)›

text ‹ The weightiest path function is a generalization of an algorithm which computes the
longest path in a DAG starting at a given vertex `v`. Its arguments are the relation `R` which
induces the graph, a weighing function `w` assigning weights to vertices, an accumulating functions
`f` and `g` which aggregate vertex weights into a path weight and the weights of different paths
respectively, the considered vertex and the graph represented as a topological sorted list. 
[Abdulaziz et al., p.18] 

Typical weight combining functions have the properties defined by `geq\_arg` and `increasing`. 
[Abdulaziz et al., p.18] ›

― ‹NOTE name shortened.›
fun wlp where
  "wlp R w g f x [] = w x"
| "wlp R w g f x (h # l) = (if R x h
    then g (f (w x) (wlp R w g f h l)) (wlp R w g f x l)
    else wlp R w g f x l
  )"


― ‹NOTE name shortened.›
definition geq_arg where 
  "geq_arg f ≡ (∀x y. (x ≤ f x y) ∧ (y ≤ f x y))"


lemma individual_weight_less_eq_lp: 
  fixes w :: "'a ⇒ nat"
  assumes "geq_arg g"
  shows "(w x ≤ wlp R w g f x l)"
  using assms
  unfolding geq_arg_def
proof (induction l arbitrary: R w g f x)
  case (Cons a l)
  then show ?case
    using Cons.IH Cons.prems
  proof (cases "R x a")
    case True
    then show ?thesis 
      using Cons le_trans wlp.simps(2)
      by smt
  next
    case False
    then show ?thesis 
      using Cons
      by simp
  qed
qed simp


― ‹NOTE Types of 'f' and 'g' had to be fixed to be able to use transitivity rule of the less-equal
relation.›
lemma lp_geq_lp_from_successor:
  fixes vtx1 and f g :: "nat ⇒ nat ⇒ nat"
  assumes "geq_arg f" "geq_arg g" "(∀vtx. ListMem vtx G ⟶ ¬R vtx vtx)" "R vtx2 vtx1" 
    "ListMem vtx1 G" "top_sorted_abs R G" 
  shows "(f (w vtx2) (wlp R w g f vtx1 G) ≤ (wlp R w g f vtx2 G))" 
  using assms
  unfolding geq_arg_def
proof (induction G arbitrary: vtx1 f g R vtx2)
  case Nil
  then show ?case 
    using ListMem_iff
    by fastforce
next
  case (Cons a G)
  show ?case 
  proof (auto)
    assume P1: "R vtx1 a" "R vtx2 a"
    then show "
        f (w vtx2) (g (f (w vtx1) (wlp R w g f a G)) (wlp R w g f vtx1 G))
        ≤ g (f (w vtx2) (wlp R w g f a G)) (wlp R w g f vtx2 G)"
      using Cons.prems(3, 5, 6)
      by (metis ListMem_iff set_ConsD top_sorted_abs_mem)
  next 
    assume P2: "R vtx1 a" "¬ R vtx2 a" 
    then show "
        f (w vtx2) (g (f (w vtx1) (wlp R w g f a G)) (wlp R w g f vtx1 G)) 
        ≤ wlp R w g f vtx2 G"
      using Cons.prems(4, 5, 6)
      by (metis ListMem_iff set_ConsD top_sorted_abs_mem) 
  next 
    assume P3: "¬ R vtx1 a" "R vtx2 a" 
    then show "
        f (w vtx2) (wlp R w g f vtx1 G) 
        ≤ g (f (w vtx2) (wlp R w g f a G)) (wlp R w g f vtx2 G)"
    proof -
      have f1: "∀n na. n ≤ g n na ∧ na ≤ g n na"
        using Cons.prems(2) by blast
      have f2: "vtx1 = a ∨ vtx1 ∈ set G"
        by (meson Cons.prems(5) ListMem_iff set_ConsD)
      obtain aa :: "('a ⇒ 'a ⇒ bool) ⇒ 'a" where
        "∀x2. (∃v5. ListMem v5 G ∧ x2 v5 v5) = (ListMem (aa x2) G ∧ x2 (aa x2) (aa x2))"
        by moura
      then have "
          ListMem (aa R) G ∧ R (aa R) (aa R) 
          ∨ ¬ ListMem vtx1 G ∨ f (w vtx2) (wlp R w g f vtx1 G) ≤ wlp R w g f vtx2 G"
        using f1 by (metis (no_types) Cons.IH Cons.prems(1, 4, 6) top_sorted_cons)
      then show ?thesis
        using f2 f1 by (meson Cons.prems(3) ListMem_iff insert le_trans)
    qed
  next 
    assume P4: "¬ R vtx1 a" "¬ R vtx2 a"
    then show "f (w vtx2) (wlp R w g f vtx1 G) ≤ wlp R w g f vtx2 G"
    proof -
      have f1: "top_sorted_abs R G"
        using Cons.prems(6) by fastforce
      have "ListMem vtx1 G"
        by (metis Cons.prems(4) Cons.prems(5) ListMem_iff P4(2) set_ConsD)
      then show ?thesis
        using f1 by (simp add: Cons.IH Cons.prems(1, 2, 3, 4) insert)
    qed 
  qed
qed


definition increasing where
  "increasing f ≡ (∀e b c d. (e ≤ c) ∧ (b ≤ d) ⟶ (f e b ≤ f c d))"


lemma weight_fun_leq_imp_lp_leq: "⋀x.
  (increasing f)
  ⟹ (increasing g)
  ⟹ (∀y. ListMem y l ⟶ w1 y ≤ w2 y) 
  ⟹ (w1 x ≤ w2 x)
  ⟹ (wlp R w1 g f x l ≤ wlp R w2 g f x l)
"
  unfolding increasing_def
  by (induction l) (auto simp add: elem insert)


― ‹NOTE generalizing `f2`, `x1`, `x2` seems to break the prover.›
lemma wlp_congruence_rule: 
  fixes l1 l2 R1 R2 w1 w2 g1 g2 f1 f2 x1 x2 
  assumes "(l1 = l2)" "(∀y. ListMem y l2 ⟶ (R1 x1 y = R2 x2 y))"
    "(∀y. ListMem y l2 ⟶ (R1 y x1 = R2 y x2))" "(w1 x1 = w2 x2)" 
    "(∀y1 y2. (y1 = y2) ⟶ (f1 (w1 x1) y1 = f2 (w2 x2) y2))" 
    "(∀y1 y2 z1 z2. (y1 = y2) ∧ (z1 = z2) ⟶ ((g1 (f1 (w1 x1) y1) z1) = (g2 (f2 (w2 x2) y2) z2)))"
    "(∀x y. ListMem x l2 ∧ ListMem y l2 ⟶ (R1 x y = R2 x y))"
    "(∀x. ListMem x l2 ⟶ (w1 x = w2 x))"
    "(∀x y z. ListMem x l2 ⟶ (g1 (f1 (w1 x) y) z = g2 (f2 (w2 x) y) z))"
    "(∀x y. ListMem x l2 ⟶ (f1 (w1 x) y = f2 (w1 x) y))"
  shows "((wlp R1 w1 g1 f1 x1 l1) = (wlp R2 w2 g2 f2 x2 l2))"
  using assms
proof (induction l2 arbitrary: l1 x1 x2)
  case (Cons a l2)
  then have "(wlp R1 w1 g1 f1 x1 l2) = (wlp R2 w2 g2 f2 x2 l2)"
    using Cons
    by (simp add: insert)
  moreover have "(wlp R1 w1 g1 f1 a l2) = (wlp R2 w2 g2 f2 a l2)"
    using Cons
    by (simp add: elem insert)
  ultimately show ?case
    by (simp add: Cons.prems(1,2, 6) elem)
qed auto


lemma wlp_ite_weights: 
  fixes x
  assumes "∀y. ListMem y l1 ⟶ P y" "P x"
  shows "((wlp R (λy. if P y then w1 y else w2 y) g f x l1) = (wlp R w1 g f x l1))"
  using assms 

proof (induction l1 arbitrary: R P w1 w2 f g)
  case (Cons a l1)
  let ?w1="(λy. if P y then w1 y else w2 y)"
  let ?w2="w1"
  {
    have "∀y. ListMem y l1 ⟶ P y" 
      using Cons.prems(1) insert
      by fast
    then have "((wlp R (λy. if P y then w1 y else w2 y) g f x l1) = (wlp R w1 g f x l1))" 
      using Cons.prems(2) Cons.IH
      by blast
  }
  note 1 = this
  { 
    have "(if P x then w1 x else w2 x) = w1 x" 
      "∀y1 y2. y1 = y2 ⟶ f (if P x then w1 x else w2 x) y1 = f (w1 x) y2"
      "∀y1 y2 z1 z2. 
        y1 = y2 ∧ z1 = z2 
        ⟶ g (f (if P x then w1 x else w2 x) y1) z1 = g (f (w1 x) y2) z2"
      "∀x. ListMem x (a # l1) ⟶ (if P x then w1 x else w2 x) = w1 x"
      "∀x y z. 
        ListMem x (a # l1) 
        ⟶ g (f (if P x then w1 x else w2 x) y) z = g (f (w1 x) y) z"
      "∀x y.
        ListMem x (a # l1) ⟶ f (if P x then w1 x else w2 x) y = f (if P x then w1 x else w2 x) y"
      using Cons.prems(1, 2)
      by simp+
    then have "wlp R (λy. if P y then w1 y else w2 y) g f x (a # l1) = wlp R w1 g f x (a # l1)"
      using Cons wlp_congruence_rule[of "a # l1" "a # l1" R x R x "?w1" "?w2" f f g g] 
      by blast
  }
  then show ?case
    by blast
qed auto


lemma map_wlp_ite_weights: "
  (∀x. ListMem x l1 ⟶ P x) 
  ⟹ (∀x. ListMem x l2 ⟶ P x) 
  ⟹ (
    map (λx. wlp R (λy. if P y then w1 y else w2 y) g f x l1) l2 
    = map (λx. wlp R w1 g f x l1) l2
  )
"
  apply(induction l2)
   apply(auto)
  subgoal by (simp add: elem wlp_congruence_rule)
  subgoal by (simp add: insert)
  done


lemma wlp_weight_lamda_exp: "⋀x. wlp R w g f x l = wlp R (λy. w y) g f x l"
proof -
  fix x
  show "wlp R w g f x l = wlp R (λy. w y) g f x l" 
    by(induction l) auto
qed


lemma img_wlp_ite_weights: "
  (∀x. ListMem x l ⟶ P x) 
  ⟹ (∀x. x ∈ s ⟶ P x) 
  ⟹ (
    (λx. wlp R (λy. if P y then w1 y else w2 y) g f x l) ` s 
    = (λx. wlp R w1 g f x l) ` s
  )
"
proof -
  assume P1: "∀x. ListMem x l ⟶ P x"
  assume P2: "∀x. x ∈ s ⟶ P x"
  show "(
    (λx. wlp R (λy. if P y then w1 y else w2 y) g f x l) ` s 
    = (λx. wlp R w1 g f x l) ` s
  )" 
    by (auto simp add:  P1 P2 image_iff wlp_ite_weights)
qed


end