Theory Dependency_Structures

theory Dependency_Structures
  imports Preliminaries
begin

section ‹Carrier-Restricted Dependency›

text ‹
  A dependency structure consists of a carrier and an immediate relation.  The
  orientation is fixed throughout this development: @{term "D x y"} means that
  @{term x} is prior to, grounds, or immediately supports @{term y}.  The
  carrier restriction is explicit so that unrelated elements cannot become
  accidental first causes.
›

definition dependency_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "dependency_on C D x y ⟷ x ∈ C ∧ y ∈ C ∧ D x y"

lemma dependency_onI:
  assumes "x ∈ C" and "y ∈ C" and "D x y"
  shows "dependency_on C D x y"
  using assms by (simp add: dependency_on_def)

lemma dependency_onD:
  assumes "dependency_on C D x y"
  shows "x ∈ C" "y ∈ C" "D x y"
  using assms by (auto simp: dependency_on_def)

definition dependency_ancestor ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "dependency_ancestor C D x y ⟷
     x ∈ C ∧ y ∈ C ∧ (dependency_on C D)⇧*⇧* x y"

lemma dependency_ancestor_refl:
  assumes "x ∈ C"
  shows "dependency_ancestor C D x x"
  using assms by (simp add: dependency_ancestor_def)

lemma dependency_ancestor_direct:
  assumes "x ∈ C" and "y ∈ C" and "D x y"
  shows "dependency_ancestor C D x y"
proof -
  have "dependency_on C D x y"
    using assms by (simp add: dependency_on_def)
  then have "(dependency_on C D)⇧*⇧* x y"
    by (rule r_into_rtranclp)
  then show ?thesis
    using assms by (simp add: dependency_ancestor_def)
qed

lemma dependency_ancestor_trans:
  assumes "dependency_ancestor C D x y"
    and "dependency_ancestor C D y z"
  shows "dependency_ancestor C D x z"
proof -
  from assms obtain
      "x ∈ C" "y ∈ C" "(dependency_on C D)⇧*⇧* x y"
      "z ∈ C" "(dependency_on C D)⇧*⇧* y z"
    by (auto simp: dependency_ancestor_def)
  then show ?thesis
    by (auto simp: dependency_ancestor_def intro: rtranclp_trans)
qed

section ‹Compatibility with the Existing Ancestry Predicate›

lemma ancestor_iff_rtranclp:
  "ancestor D x y ⟷ D⇧*⇧* x y"
proof
  assume "ancestor D x y"
  then show "D⇧*⇧* x y"
  proof (induction rule: ancestor.induct)
    case refl
    show ?case by (rule rtranclp.rtrancl_refl)
  next
    case (step x y z)
    have "D⇧*⇧* x y"
      using step.hyps(1) by (rule r_into_rtranclp)
    with step.IH show ?case
      by (blast intro: rtranclp_trans)
  qed
next
  assume "D⇧*⇧* x y"
  then show "ancestor D x y"
  proof (induction rule: rtranclp_induct)
    case base
    show ?case by (rule ancestor.refl)
  next
    case (step y z)
    have "ancestor D y z"
      using step.hyps(2) by (rule ancestor_direct)
    then show ?case
      using step.IH by (blast intro: ancestor_trans)
  qed
qed

lemma legacy_ancestor_iff_dependency_ancestor:
  "ancestor D x y ⟷ dependency_ancestor UNIV D x y"
proof -
  have relation_eq: "dependency_on UNIV D = D"
    by (rule ext, rule ext) (simp add: dependency_on_def)
  then show ?thesis
    by (simp add: ancestor_iff_rtranclp dependency_ancestor_def)
qed

section ‹Grounded and Independent Members›

definition grounded_in ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool"
where
  "grounded_in C D x ⟷ x ∈ C ∧ (∃y ∈ C. D y x)"

definition independent_in ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool"
where
  "independent_in C D x ⟷ x ∈ C ∧
     (¬ (∃y ∈ C. D y x))"

lemma grounded_inD:
  assumes "grounded_in C D x"
  shows "x ∈ C" "∃y ∈ C. D y x"
  using assms by (auto simp: grounded_in_def)

lemma independent_inD:
  assumes "independent_in C D x"
  shows "x ∈ C" "¬ (∃y ∈ C. D y x)"
  using assms by (auto simp: independent_in_def)

lemma grounded_not_independent:
  assumes "grounded_in C D x"
  shows "¬ independent_in C D x"
  using assms by (auto simp: grounded_in_def independent_in_def)

definition first_member_in ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "first_member_in C D x a ⟷
     dependency_ancestor C D x a ∧ independent_in C D x"

definition first_cause_in ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "first_cause_in C D x a ⟷
     first_member_in C D x a ∧ x ≠ a"

lemma first_member_inD:
  assumes "first_member_in C D x a"
  shows "dependency_ancestor C D x a" "independent_in C D x"
  using assms by (auto simp: first_member_in_def)

lemma first_cause_inD:
  assumes "first_cause_in C D x a"
  shows "first_member_in C D x a" "x ≠ a"
  using assms by (auto simp: first_cause_in_def)

definition foundation_set_for ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a set ⇒ bool"
where
  "foundation_set_for C D R F ⟷
     F ⊆ C ∧ R ⊆ C ∧
     (∀f ∈ F. independent_in C D f) ∧
     (∀a ∈ R. grounded_in C D a ⟶
       (∃f ∈ F. dependency_ancestor C D f a))"

lemma foundation_set_forD:
  assumes "foundation_set_for C D R F"
  shows "F ⊆ C" "R ⊆ C"
    and "∀f ∈ F. independent_in C D f"
    and "∀a ∈ R. grounded_in C D a ⟶
      (∃f ∈ F. dependency_ancestor C D f a)"
  using assms by (auto simp: foundation_set_for_def)

end