Theory Edrel

theory Edrel
  imports
    Transitive_Models.ZF_Miscellanea
    Transitive_Models.Recursion_Thms

begin

subsection‹The well-founded relation \<^term>‹ed››

lemma eclose_sing : "x ∈ eclose(a) ⟹ x ∈ eclose({a})"
  using subsetD[OF mem_eclose_subset]
  by simp

lemma ecloseE :
  assumes  "x ∈ eclose(A)"
  shows  "x ∈ A ∨ (∃ B ∈ A . x ∈ eclose(B))"
  using assms
proof (induct rule:eclose_induct_down)
  case (1 y)
  then
  show ?case
    using arg_into_eclose by auto
next
  case (2 y z)
  from ‹y ∈ A ∨ (∃B∈A. y ∈ eclose(B))›
  consider (inA) "y ∈ A" | (exB) "(∃B∈A. y ∈ eclose(B))"
    by auto
  then show ?case
  proof (cases)
    case inA
    then
    show ?thesis using 2 arg_into_eclose by auto
  next
    case exB
    then obtain B where "y ∈ eclose(B)" "B∈A"
      by auto
    then
    show ?thesis using 2 ecloseD[of y B z] by auto
  qed
qed

lemma eclose_singE : "x ∈ eclose({a}) ⟹ x = a ∨ x ∈ eclose(a)"
  by(blast dest: ecloseE)

lemma in_eclose_sing :
  assumes "x ∈ eclose({a})" "a ∈ eclose(z)"
  shows "x ∈ eclose({z})"
proof -
  from ‹x∈eclose({a})›
  consider "x=a" | "x∈eclose(a)"
    using eclose_singE by auto
  then
  show ?thesis
    using eclose_sing mem_eclose_trans assms
    by (cases, auto)
qed

lemma in_dom_in_eclose :
  assumes "x ∈ domain(z)"
  shows "x ∈ eclose(z)"
proof -
  from assms
  obtain y where "⟨x,y⟩ ∈ z"
    unfolding domain_def by auto
  then
  show ?thesis
    unfolding Pair_def
    using ecloseD[of "{x,x}"] ecloseD[of "{{x,x},{x,y}}"] arg_into_eclose
    by auto
qed

text‹term‹ed› is the well-founded relation on which \<^term>‹val› is defined.›
definition ed :: "[i,i] ⇒ o" where
  "ed(x,y) ≡ x ∈ domain(y)"

definition edrel :: "i ⇒ i" where
  "edrel(A) ≡ Rrel(ed,A)"

lemma edI[intro!]: "t∈domain(x) ⟹ ed(t,x)"
  unfolding ed_def .

lemma edD[dest!]: "ed(t,x) ⟹ t∈domain(x)"
  unfolding ed_def .

lemma rank_ed:
  assumes "ed(y,x)"
  shows "succ(rank(y)) ≤ rank(x)"
proof
  from assms
  obtain p where "⟨y,p⟩∈x" by auto
  moreover
  obtain s where "y∈s" "s∈⟨y,p⟩" unfolding Pair_def by auto
  ultimately
  have "rank(y) < rank(s)" "rank(s) < rank(⟨y,p⟩)" "rank(⟨y,p⟩) < rank(x)"
    using rank_lt by blast+
  then
  show "rank(y) < rank(x)"
    using lt_trans by blast
qed

lemma edrel_dest [dest]: "x ∈ edrel(A) ⟹ ∃ a ∈ A. ∃ b ∈ A. x =⟨a,b⟩"
  by(auto simp add:ed_def edrel_def Rrel_def)

lemma edrelD : "x ∈ edrel(A) ⟹ ∃ a∈ A. ∃ b ∈ A. x =⟨a,b⟩ ∧ a ∈ domain(b)"
  by(auto simp add:ed_def edrel_def Rrel_def)

lemma edrelI [intro!]: "x∈A ⟹ y∈A ⟹ x ∈ domain(y) ⟹ ⟨x,y⟩∈edrel(A)"
  by (simp add:ed_def edrel_def Rrel_def)

lemma edrel_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ ⟨x,y⟩∈edrel(A)"
  by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)

lemma domain_trans: "Transset(A) ⟹ y∈A ⟹ x ∈ domain(y) ⟹ x∈A"
  by (auto simp add: Transset_def domain_def Pair_def)

lemma relation_edrel : "relation(edrel(A))"
  by(auto simp add: relation_def)

lemma field_edrel : "field(edrel(A))⊆A"
  by blast

lemma edrel_sub_memrel: "edrel(A) ⊆ trancl(Memrel(eclose(A)))"
proof
  let
    ?r="trancl(Memrel(eclose(A)))"
  fix z
  assume "z∈edrel(A)"
  then
  obtain x y where "x∈A" "y∈A" "z=⟨x,y⟩" "x∈domain(y)"
    using edrelD
    by blast
  moreover from this
  obtain u v where "x∈u" "u∈v" "v∈y"
    unfolding domain_def Pair_def by auto
  moreover from calculation
  have "x∈eclose(A)" "y∈eclose(A)" "y⊆eclose(A)"
    using arg_into_eclose Transset_eclose[unfolded Transset_def]
    by simp_all
  moreover from calculation
  have "v∈eclose(A)"
    by auto
  moreover from calculation
  have "u∈eclose(A)"
    using Transset_eclose[unfolded Transset_def]
    by auto
  moreover from calculation
  have"⟨x,u⟩∈?r" "⟨u,v⟩∈?r" "⟨v,y⟩∈?r"
    by (auto simp add: r_into_trancl)
  moreover from this
  have "⟨x,y⟩∈?r"
    using trancl_trans[OF _ trancl_trans[of _ v _ y]]
    by simp
  ultimately
  show "z∈?r"
    by simp
qed

lemma wf_edrel : "wf(edrel(A))"
  using wf_subset[of "trancl(Memrel(eclose(A)))"] edrel_sub_memrel
    wf_trancl wf_Memrel
  by auto

lemma ed_induction:
  assumes "⋀x. ⟦⋀y.  ed(y,x) ⟹ Q(y) ⟧ ⟹ Q(x)"
  shows "Q(a)"
proof(induct rule: wf_induct2[OF wf_edrel[of "eclose({a})"] ,of a "eclose({a})"])
  case 1
  then show ?case using arg_into_eclose by simp
next
  case 2
  then show ?case using field_edrel .
next
  case (3 x)
  then
  show ?case
    using assms[of x] edrelI domain_trans[OF Transset_eclose 3(1)] by blast
qed

lemma dom_under_edrel_eclose: "edrel(eclose({x})) -`` {x} = domain(x)"
proof(intro equalityI)
  show "edrel(eclose({x})) -`` {x} ⊆ domain(x)"
    unfolding edrel_def Rrel_def ed_def
    by auto
next
  show "domain(x) ⊆ edrel(eclose({x})) -`` {x}"
    unfolding edrel_def Rrel_def
    using in_dom_in_eclose eclose_sing arg_into_eclose
    by blast
qed

lemma ed_eclose : "⟨y,z⟩ ∈ edrel(A) ⟹ y ∈ eclose(z)"
  by(drule edrelD,auto simp add:domain_def in_dom_in_eclose)

lemma tr_edrel_eclose : "⟨y,z⟩ ∈ edrel(eclose({x}))^+ ⟹ y ∈ eclose(z)"
  by(rule trancl_induct,(simp add: ed_eclose mem_eclose_trans)+)

lemma restrict_edrel_eq :
  assumes "z ∈ domain(x)"
  shows "edrel(eclose({x})) ∩ eclose({z})×eclose({z}) = edrel(eclose({z}))"
proof(intro equalityI subsetI)
  let ?ec="λ y . edrel(eclose({y}))"
  let ?ez="eclose({z})"
  let ?rr="?ec(x) ∩ ?ez × ?ez"
  fix y
  assume "y ∈ ?rr"
  then
  obtain a b where "⟨a,b⟩ ∈ ?rr" "a ∈ ?ez" "b ∈ ?ez" "⟨a,b⟩ ∈ ?ec(x)" "y=⟨a,b⟩"
    by blast
  moreover from this
  have "a ∈ domain(b)"
    using edrelD by blast
  ultimately
  show "y ∈ edrel(eclose({z}))"
    by blast
next
  let ?ec="λ y . edrel(eclose({y}))"
  let ?ez="eclose({z})"
  let ?rr="?ec(x) ∩ ?ez × ?ez"
  fix y
  assume "y ∈ edrel(?ez)"
  then
  obtain a b where "a ∈ ?ez" "b ∈ ?ez" "y=⟨a,b⟩" "a ∈ domain(b)"
    using edrelD by blast
  moreover
  from this assms
  have "z ∈ eclose(x)"
    using in_dom_in_eclose by simp
  moreover
  from assms calculation
  have "a ∈ eclose({x})" "b ∈ eclose({x})"
    using in_eclose_sing by simp_all
  moreover from calculation
  have "⟨a,b⟩ ∈ edrel(eclose({x}))"
    by blast
  ultimately
  show "y ∈ ?rr"
    by simp
qed

lemma tr_edrel_subset :
  assumes "z ∈ domain(x)"
  shows   "tr_down(edrel(eclose({x})),z) ⊆ eclose({z})"
proof(intro subsetI)
  let ?r="λ x . edrel(eclose({x}))"
  fix y
  assume "y ∈ tr_down(?r(x),z)"
  then
  have "⟨y,z⟩ ∈ ?r(x)^+"
    using tr_downD by simp
  with assms
  show "y ∈ eclose({z})"
    using tr_edrel_eclose eclose_sing by simp
qed

end