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```