Theory Foundation_Principles

theory Foundation_Principles
  imports Dependency_Structures
begin

section ‹Competing Binary Principles›

text ‹
  The same immediate relation supports several non-equivalent readings of a
  regress argument.  We keep them as separate predicates.  In particular,
  acyclicity is only a prohibition on nonempty cycles, while
  well-foundedness is a global condition on all predecessor chains.
›

definition acyclic_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
where
  "acyclic_on C D ⟷
     (∀x ∈ C. ¬ (dependency_on C D)⇧+⇧+ x x)"

definition well_founded_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
where
  "well_founded_on C D ⟷ wfp_on C (dependency_on C D)"

definition chain_terminating_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool"
where
  "chain_terminating_on C D ⟷
     (∄f. ∀n. dependency_on C D (f (Suc n)) (f n))"

definition local_foundation_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
  "local_foundation_on C D R ⟷
     (∀a ∈ R. grounded_in C D a ⟶
       (∃f. first_member_in C D f a))"

definition global_foundation_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
  "global_foundation_on C D R ⟷
     (∃F. foundation_set_for C D R F)"

lemma global_foundation_onI:
  assumes "foundation_set_for C D R F"
  shows "global_foundation_on C D R"
  using assms by (auto simp: global_foundation_on_def)

lemma global_foundation_onD:
  assumes "global_foundation_on C D R"
  obtains F where "foundation_set_for C D R F"
  using assms by (auto simp: global_foundation_on_def)

section ‹Plural Grounding›

text ‹
  A full ground may be a set rather than a single member.  The carrier
  restriction is part of the interface.  This makes the later comparison with
  binary dependence explicit instead of silently identifying singleton and
  plural grounding.
›

definition full_grounding_on ::
  "'a set ⇒ ('a set ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a ⇒ bool"
where
  "full_grounding_on C G S x ⟷
     S ⊆ C ∧ x ∈ C ∧ G S x"

definition partial_grounding_on ::
  "'a set ⇒ ('a set ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"
where
  "partial_grounding_on C G x y ⟷
     x ∈ C ∧ y ∈ C ∧
     (∃S. full_grounding_on C G S y ∧ x ∈ S)"

definition full_foundation_for ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a set ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ 'a set ⇒ bool"
where
  "full_foundation_for C D G R F ⟷
     F ⊆ C ∧ R ⊆ C ∧
     (∀f ∈ F. independent_in C D f) ∧
     (∀a ∈ R.
       grounded_in C (partial_grounding_on C G) a ⟶
       (∃S. full_grounding_on C G S a ∧ S ⊆ F))"

definition full_foundation_on ::
  "'a set ⇒ ('a ⇒ 'a ⇒ bool) ⇒
   ('a set ⇒ 'a ⇒ bool) ⇒ 'a set ⇒ bool"
where
  "full_foundation_on C D G R ⟷
     (∃F. full_foundation_for C D G R F)"

lemma full_grounding_onD:
  assumes "full_grounding_on C G S x"
  shows "S ⊆ C" "x ∈ C" "G S x"
  using assms by (auto simp: full_grounding_on_def)

lemma full_grounding_onI:
  assumes "S ⊆ C" and "x ∈ C" and "G S x"
  shows "full_grounding_on C G S x"
  using assms by (auto simp: full_grounding_on_def)

lemma partial_grounding_onI:
  assumes "full_grounding_on C G S y" and "x ∈ S"
  shows "partial_grounding_on C G x y"
  using assms
  by (auto simp: partial_grounding_on_def full_grounding_on_def)

lemma partial_grounding_onD:
  assumes "partial_grounding_on C G x y"
  shows "x ∈ C" "y ∈ C"
    and "∃S. full_grounding_on C G S y ∧ x ∈ S"
  using assms by (auto simp: partial_grounding_on_def)

lemma full_foundation_forD:
  assumes "full_foundation_for C D G R F"
  shows "F ⊆ C" "R ⊆ C"
    and "∀f ∈ F. independent_in C D f"
    and "∀a ∈ R.
      grounded_in C (partial_grounding_on C G) a ⟶
      (∃S. full_grounding_on C G S a ∧ S ⊆ F)"
  using assms by (auto simp: full_foundation_for_def)

lemma full_foundation_onI:
  assumes "full_foundation_for C D G R F"
  shows "full_foundation_on C D G R"
  using assms by (auto simp: full_foundation_on_def)

lemma full_foundation_onD:
  assumes "full_foundation_on C D G R"
  obtains F where "full_foundation_for C D G R F"
  using assms by (auto simp: full_foundation_on_def)

end