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


― ‹NOTE added lemma.› 
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

― ‹NOTE added lemma.› 
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]
    by (simp add: TC_equiv_tranclp)
      ― ‹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 (atomize_elim, (subst choice_iff[symmetric])+, blast)
  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