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