# Theory Dependency

```theory Dependency
imports Main "HOL-Library.Finite_Map" FactoredSystem ActionSeqProcess RelUtils
begin

section ‹Dependency›

text ‹ State variable dependency analysis may be used to find structure in a factored system and
find useful projections, for example on variable sets which are closed under mutual dependency.
[Abdulaziz et al., p.13]

In the following the dependency predicate (`dep`) is formalized and some dependency related
propositions are proven. Dependency between variables `v1`, `v2` w.r.t to an action set @{term "δ"} is given
if one of the following holds:
(1) `v1` and `v2` are equal
(2) an action @{term "(p, e) ∈ δ"} exists where @{term "v1 ∈ 𝒟(p)"} and @{term "v2 ∈ 𝒟(e)"} (meaning that it is a
necessary condition that `p v1` is given if the action has effect `e v2`).
(3) or, an action @{term "(p, e) ∈ δ"} exists s.t. @{term "v1 v2 ∈ 𝒟(e)"}
This notion is extended to sets of variables `vs1`, `vs2` (`dep\_var\_set`): `vs1` and `vs2` are
dependent iff `vs1` and `vs2` are disjoint and if dependent `v1`, `v2` exist where @{term "v1 ∈ vs1"},
@{term "v2 ∈ vs2"}. [Abdulaziz et al., Definition 7, p.13][Abdulaziz et al., HOL4 Definition 5, p.14] ›

subsection ‹Dependent Variables and Variable Sets›

― ‹NOTE name shortened to 'dep'.›
definition dep where
"dep PROB v1 v2 ≡ (∃a.
a ∈ PROB
∧ (
((v1 ∈ fmdom' (fst a)) ∧ (v2 ∈ fmdom' (snd a)))
∨ ((v1 ∈ fmdom' (snd a) ∧ v2 ∈ fmdom' (snd a)))
)
)
∨ (v1 = v2)"

― ‹NOTE name shortened to 'dep\_var\_set'.›
definition dep_var_set where
"dep_var_set PROB vs1 vs2 ≡ (disjnt vs1 vs2) ∧
(∃ v1 v2. (v1 ∈ vs1) ∧ (v2 ∈ vs2) ∧ (dep PROB v1 v2)
)"

lemma  dep_var_set_self_empty:
fixes PROB vs
assumes "dep_var_set PROB vs vs"
shows "(vs = {})"
using assms
unfolding dep_var_set_def
proof -
obtain v1 v2 where
"v1 ∈ vs" "v2 ∈ vs" "disjnt vs vs" "dep PROB v1 v2"
using assms
unfolding dep_var_set_def
by blast
then show ?thesis
by force
qed

lemma DEP_REFL:
fixes PROB
shows "reflexive (λv v'. dep PROB v v')"
unfolding dep_def reflexive_def
by presburger

lemma NEQ_DEP_IMP_IN_DOM_i:
fixes a v
assumes "a ∈ PROB" "v ∈ fmdom' (fst a)"
shows "v ∈ prob_dom PROB"
proof -
have "v ∈ fmdom' (fst a)"
using assms(2)
by simp
moreover have "fmdom' (fst a) ⊆ prob_dom PROB"
using assms(1)
unfolding prob_dom_def action_dom_def
using case_prod_beta'
by auto
ultimately show ?thesis
by blast
qed

lemma NEQ_DEP_IMP_IN_DOM_ii:
fixes a v
assumes "a ∈ PROB" "v ∈ fmdom' (snd a)"
shows "v ∈ prob_dom PROB"
proof -
have "v ∈ fmdom' (snd a)"
using assms(2)
by simp
moreover have "fmdom' (snd a) ⊆ prob_dom PROB"
using assms(1)
unfolding prob_dom_def action_dom_def
using case_prod_beta'
by auto
ultimately show ?thesis
by blast
qed

lemma NEQ_DEP_IMP_IN_DOM:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" and  v v'
assumes "¬(v = v')" "(dep PROB v v')"
shows "(v ∈ (prob_dom PROB) ∧ v' ∈ (prob_dom PROB))"
using assms
unfolding dep_def
using FDOM_pre_subset_prob_dom_pair FDOM_eff_subset_prob_dom_pair
proof -
obtain a where 1:
"a ∈ PROB"
"(v ∈ fmdom' (fst a) ∧ v' ∈ fmdom' (snd a) ∨ v ∈ fmdom' (snd a) ∧ v' ∈ fmdom' (snd a))"
using assms
unfolding dep_def
by blast
then consider
(i) "v ∈ fmdom' (fst a) ∧ v' ∈ fmdom' (snd a)"
| (ii) "v ∈ fmdom' (snd a) ∧ v' ∈ fmdom' (snd a)"
by blast
then show ?thesis
proof (cases)
case i
then have "v ∈ fmdom' (fst a)" "v' ∈ fmdom' (snd a)"
by simp+
then have "v ∈ prob_dom PROB"  "v' ∈ prob_dom PROB"
using 1 NEQ_DEP_IMP_IN_DOM_i NEQ_DEP_IMP_IN_DOM_ii
by metis+
then show ?thesis
by simp
next
case ii
then have "v ∈ fmdom' (snd a)" "v' ∈ fmdom' (snd a)"
by simp+
then have "v ∈ prob_dom PROB"  "v' ∈ prob_dom PROB"
using 1 NEQ_DEP_IMP_IN_DOM_ii
by metis+
then show ?thesis
by simp
qed
qed

lemma dep_sos_imp_mem_dep:
fixes PROB S vs
assumes "(dep_var_set PROB (⋃ S) vs)"
shows "(∃vs'. vs' ∈ S ∧ dep_var_set PROB vs' vs)"
proof -
obtain v1 v2 where obtain_v1_v2: "v1 ∈ ⋃S" "v2 ∈ vs" "disjnt (⋃S) vs" "dep PROB v1 v2"
using assms dep_var_set_def[of PROB "⋃ S" vs]
by blast
moreover
{
fix vs'
assume "vs' ∈ S"
moreover have "vs' ⊆ (⋃S)"
using calculation Union_upper
by blast
ultimately have "disjnt vs' vs"
using obtain_v1_v2(3) disjnt_subset1
by blast
}
ultimately show ?thesis
unfolding dep_var_set_def
by blast
qed

lemma dep_union_imp_or_dep:
fixes PROB vs vs' vs''
assumes "(dep_var_set PROB vs (vs' ∪ vs''))"
shows "(dep_var_set PROB vs vs' ∨ dep_var_set PROB vs vs'')"
proof -
obtain v1 v2 where
obtain_v1_v2: "v1 ∈ vs" "v2 ∈ vs' ∪ vs''" "disjnt vs (vs' ∪ vs'')" "dep PROB v1 v2"
using assms dep_var_set_def[of PROB vs "(vs' ∪ vs'')"]
by blast
― ‹NOTE The proofs for the cases introduced here yield the goal's left and right side
respectively.›
consider (i) "v2 ∈ vs'" | (ii) "v2 ∈ vs''"
using obtain_v1_v2(2)
by blast
then show ?thesis
proof (cases)
case i
have "vs' ⊆ vs' ∪ vs''"
by auto
moreover have "disjnt (vs' ∪ vs'') vs"
using obtain_v1_v2(3) disjnt_sym
by blast
ultimately have "disjnt vs vs'"
using disjnt_subset1 disjnt_sym
by blast
then have "dep_var_set PROB vs vs'"
unfolding dep_var_set_def
using obtain_v1_v2(1, 4) i
by blast
then show ?thesis
by simp
next
case ii
then have "vs'' ⊆ vs' ∪ vs''"
by simp
moreover have "disjnt (vs' ∪ vs'') vs"
using obtain_v1_v2(3) disjnt_sym
by fast
ultimately have "disjnt vs vs''"
using disjnt_subset1 disjnt_sym
by metis
then have "dep_var_set PROB vs vs''"
unfolding dep_var_set_def
using obtain_v1_v2(1, 4) ii
by blast
then show ?thesis
by simp
qed
qed

― ‹NOTE This is symmetrical to `dep\_sos\_imp\_mem\_dep` w.r.t to `vs` and @{term "⋃ S"}.›
lemma dep_biunion_imp_or_dep:
fixes PROB vs S
assumes "(dep_var_set PROB vs (⋃S))"
shows "(∃vs'. vs' ∈ S ∧ dep_var_set PROB vs vs')"
proof -
obtain v1 v2 where obtain_v1_v2: "v1 ∈ vs" "v2 ∈ (⋃S)" "disjnt vs (⋃S)" "dep PROB v1 v2"
using assms dep_var_set_def[of PROB vs "⋃ S"]
by blast
moreover
{
fix vs'
assume "vs' ∈ S"
then have "vs' ⊆ (⋃S)"
using calculation Union_upper
by blast
moreover have "disjnt (⋃S) vs"
using obtain_v1_v2(3) disjnt_sym
by blast
ultimately have "disjnt vs vs'"
using obtain_v1_v2(3) disjnt_subset1 disjnt_sym
by metis
}
ultimately show ?thesis
unfolding dep_var_set_def
by blast
qed

subsection "Transitive Closure of Dependent Variables and Variable Sets"

definition dep_tc where
"dep_tc PROB = TC (λv1' v2'. dep PROB v1' v2')"

― ‹NOTE type of `PROB` had to be fixed for MP on `NEQ\_DEP\_IMP\_IN\_DOM`.›
lemma dep_tc_imp_in_dom:
fixes PROB :: "(('a, 'b) fmap × ('a, 'b) fmap) set" and v1 v2
assumes "¬(v1 = v2)" "(dep_tc PROB v1 v2)"
shows "(v1 ∈ prob_dom PROB)"
proof -
have "TC (dep PROB) v1 v2"
using assms(2)
unfolding dep_tc_def
by simp
then have "dep PROB v1 v2 ∨ (∃y. v1 ≠ y ∧ y ≠ v2 ∧ dep PROB v1 y ∧ TC (dep PROB) y v2)"
using TC_CASES1_NEQ[where R = "(λv1' v2'. dep PROB v1' v2')" and x = v1 and z = v2]
― ‹NOTE Split on the disjunction yielded by the previous step.›
then consider
(i) "dep PROB v1 v2"
| (ii) "(∃y. v1 ≠ y ∧ y ≠ v2 ∧ dep PROB v1 y ∧ TC (dep PROB) y v2)"
by fast
then show ?thesis
proof (cases)
case i
{
consider
(II) "(∃a.
a ∈ PROB ∧
(
v1 ∈ fmdom' (fst a) ∧ v2 ∈ fmdom' (snd a)
∨ v1 ∈ fmdom' (snd a) ∧ v2 ∈ fmdom' (snd a)))"
| (III) "v1 = v2"
using i
unfolding dep_def
by blast
then have ?thesis
proof (cases)
case II
then obtain a where 1:
"a ∈ PROB" "(v1 ∈ fmdom' (fst a) ∧ v2 ∈ fmdom' (snd a)
∨ v1 ∈ fmdom' (snd a) ∧ v2 ∈ fmdom' (snd a))"
by blast
then have "v1 ∈ fmdom' (fst a) ∪ fmdom' (snd a)"
by blast
then have 2: "v1 ∈ action_dom (fst a) (snd a)"
unfolding action_dom_def
by blast
then have "action_dom (fst a) (snd a) ⊆ prob_dom PROB"
using 1(1) exec_as_proj_valid_2
by fast
then have "v1 ∈ prob_dom PROB"
using 1 2
by fast
then show ?thesis
by simp
next
case III
then show ?thesis
using assms(1)
by simp
qed
}
then show ?thesis
by simp
next
case ii
then obtain y where "v1 ≠ y" "y ≠ v2" "dep PROB v1 y" "TC (dep PROB) y v2"
using ii
by blast
then show ?thesis
using NEQ_DEP_IMP_IN_DOM
by metis
qed
qed

lemma not_dep_disj_imp_not_dep:
fixes PROB vs_1 vs_2 vs_3
assumes "((vs_1 ∩ vs_2) = {})" "(vs_3 ⊆ vs_2)" "¬(dep_var_set PROB vs_1 vs_2)"
shows "¬(dep_var_set PROB vs_1 vs_3)"
using assms subset_eq
unfolding dep_var_set_def disjnt_def
by blast

lemma dep_slist_imp_mem_dep:
fixes PROB vs lvs
assumes "(dep_var_set PROB (⋃ (set lvs)) vs)"
shows "(∃vs'. ListMem vs' lvs ∧ dep_var_set PROB vs' vs)"
proof -
obtain v1 v2 where
obtain_v1_v2: "v1 ∈ ⋃(set lvs)" "v2 ∈ vs" "disjnt (⋃(set lvs)) vs" "dep PROB v1 v2"
using assms dep_var_set_def[of PROB "⋃ (set lvs)" vs]
by blast
then obtain vs' where obtain_vs': "vs' ∈ set lvs" "v1 ∈ vs'"
by blast
then have "ListMem vs' lvs"
using ListMem_iff
by fast
moreover {
have "disjnt vs' vs"
using obtain_v1_v2(3) obtain_vs'(1) by auto
then have "dep_var_set PROB vs' vs"
unfolding dep_var_set_def
using obtain_v1_v2(1, 2, 4) obtain_vs'(2)
by blast
}
ultimately show ?thesis
by blast
qed

lemma n_bigunion_le_sum_3:
fixes PROB vs svs
assumes "(∀ vs'. vs' ∈ svs ⟶ ¬(dep_var_set PROB vs' vs))"
shows "¬(dep_var_set PROB (⋃svs) vs)"
proof -
{
assume "(dep_var_set PROB (⋃svs) vs)"
then obtain v1 v2 where obtain_vs: "v1 ∈ ⋃svs" "v2 ∈ vs" "disjnt (⋃svs) vs" "dep PROB v1 v2"
unfolding dep_var_set_def
by blast
then obtain vs' where obtain_vs': "v1 ∈ vs'" "vs' ∈ svs"
by blast
then have a: "disjnt vs' vs"
using obtain_vs(3) obtain_vs'(2) disjnt_subset1
by blast
then have "∀v1 v2. ¬(v1 ∈ vs') ∨ ¬(v2 ∈ vs) ∨ ¬disjnt vs' vs ∨ ¬dep PROB v1 v2"
using assms obtain_vs'(2) dep_var_set_def
by fast
then have False
using a obtain_vs'(1) obtain_vs(2, 4)
by blast
}
then show ?thesis
by blast
qed

lemma disj_not_dep_vset_union_imp_or:
fixes PROB a vs vs'
assumes "(a ∈ PROB)" "(disjnt vs vs')"
"(¬(dep_var_set PROB vs' vs) ∨ ¬(dep_var_set PROB vs vs'))"
"(varset_action a (vs ∪ vs'))"
shows "(varset_action a vs ∨ varset_action a vs')"
using assms
unfolding varset_action_def dep_var_set_def dep_def
proof -
assume a1: "fmdom' (snd a) ⊆ vs ∪ vs'"
assume "disjnt vs vs'"
assume " ¬ (disjnt vs' vs ∧
(∃v1 v2. v1 ∈ vs' ∧ v2 ∈ vs ∧ ((∃a. a ∈ PROB ∧ (v1 ∈ fmdom' (fst a) ∧ v2 ∈ fmdom' (snd a) ∨ v1 ∈ fmdom' (snd a) ∧ v2 ∈ fmdom' (snd a))) ∨ v1 = v2))) ∨
¬ (disjnt vs vs' ∧
(∃v1 v2. v1 ∈ vs ∧ v2 ∈ vs' ∧ ((∃a. a ∈ PROB ∧ (v1 ∈ fmdom' (fst a) ∧ v2 ∈ fmdom' (snd a) ∨ v1 ∈ fmdom' (snd a) ∧ v2 ∈ fmdom' (snd a))) ∨ v1 = v2))) "
then have f2: "⋀aa ab. aa ∉ vs ∨ ab ∉ vs' ∨ aa ∉ fmdom' (snd a) ∨ ab ∉ fmdom' (snd a)"
using ‹a ∈ PROB› ‹disjnt vs vs'› disjnt_sym by blast
obtain aa :: "'a set ⇒ 'a set ⇒ 'a" where
f3: "⋀A Aa a Ab Ac. (A ⊆ Aa ∨ aa A Aa ∈ A) ∧ (aa A Aa ∉ Aa ∨ A ⊆ Aa)
∧ ((a::'a) ∉ Ab ∨ ¬ Ab ⊆ Ac ∨ a ∈ Ac)"
by moura
then have "⋀A. fmdom' (snd a) ⊆ A ∨ aa (fmdom' (snd a)) A ∈ vs ∨ aa (fmdom' (snd a)) A ∈ vs'"
using a1 by (meson Un_iff)
then show "fmdom' (snd a) ⊆ vs ∨ fmdom' (snd a) ⊆ vs'"
using f3 f2 by meson
qed

end```