Theory TD_invariant_lemmas

theory TD_invariant_lemmas
  imports Basics Destabilization
begin

(* Lemmas copied from TD.thy to avoid importing state record type for theories still not using
   state based definitions *)

declare fun_upd_apply[simp del]

lemma stabl_infl_empty:
  assumes "x ∉ s"
    and "fset (fmdom i) ⊆ s"
  shows "slookup i x = {}"
proof (rule ccontr, goal_cases)
  case 1
  then have "x ∈ fset (fmdom i)"
    unfolding fmlookup_default_def by force
  then show ?case using assms by blast
qed

lemma dep_subset_stable:
  assumes "fset (fmdom i) ⊆ s"
    and "(∀y∈s - c. ∀x ∈ dep T sigma y. y ∈ slookup i x)"
  shows "(∀ξ∈s - c. dep T sigma ξ ⊆ s)"
  using assms stabl_infl_empty[of _ s]
  by (metis DiffD2 Diff_empty subsetI)

lemma new_lookup_to_infl_not_stabl:
  assumes "∀ξ. (slookup i1 ξ - slookup i ξ) ∩ s = {}"
    and "x ∉ s"
    and "fset (fmdom i) ⊆ s"
  shows "influenced_by i1 x ∩ s = {}"
proof -
  have "u ∉ s" if "u ∈ influenced_by i1 x" for u
    using that
  proof (induction rule: influenced_by.induct)
    case (base ys y)
    have "slookup i x = {}" using stabl_infl_empty[OF assms(2,3)] by auto
    then have "y ∈ slookup i1 x - slookup i x"
      using base.hyps(1,2) by auto
    then show ?case using base.hyps(1) assms(1,3) by force
  next
    case (step y zs z)
    have "slookup i y = {}"
      by (meson assms(3) stabl_infl_empty step.IH)
    then have "z ∈ slookup i1 y - slookup i y"
      by (simp add: step.hyps(2,3))
    then show ?case using assms(1) stabl_infl_empty[OF _ assms(3)] by fastforce
  qed
  then show ?thesis by auto
qed

lemma infl_upd_diff:
  assumes "∀ξ. (slookup i' ξ - slookup i ξ) ∩ s = {}"
  shows "∀ξ. (slookup (fminsert i' x y) ξ - slookup i ξ) ∩ (s - {y}) = {}"
proof(intro allI, goal_cases)
  case (1 ξ)
  show ?case
    using assms
    unfolding fminsert_def fmlookup_default_def
    by (cases "x = ξ") auto
qed


lemma infl_diff_eval_step:
  assumes "s ⊆ s1"
    and "∀ξ. (slookup i' ξ - slookup i1 ξ) ∩ (s1 - {x}) = {}"
    and "∀ξ. (slookup i1 ξ - slookup i ξ) ∩ (s - {x}) = {}"
  shows "∀ξ. (slookup i' ξ - slookup i ξ) ∩ (s - {x}) = {}"
proof(intro allI, goal_cases)
  case (1 ξ)
  have "((slookup i' ξ - slookup i1 ξ) ∪ (slookup i1 ξ - slookup i ξ)) ∩ (s - {x}) = {}"
    using assms by auto
  then show ?case by blast
qed

end