# 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```