Theory Edrel

theory Edrel
  imports
    Transitive_Models.ZF_Miscellanea
    Transitive_Models.Recursion_Thms

begin

subsection‹The well-founded relation termed

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  (BA. y  eclose(B))
  consider (inA) "y  A" | (exB) "(BA. 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)" "BA"
      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 xeclose({a})
  consider "x=a" | "xeclose(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‹termed› is the well-founded relation on which termval 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!]: "tdomain(x)  ed(t,x)"
  unfolding ed_def .

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

lemma rank_ed:
  assumes "ed(y,x)"
  shows "succ(rank(y))  rank(x)"
proof
  from assms
  obtain p where "y,px" by auto
  moreover
  obtain s where "ys" "sy,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!]: "xA  yA  x  domain(y)  x,yedrel(A)"
  by (simp add:ed_def edrel_def Rrel_def)

lemma edrel_trans: "Transset(A)  yA  x  domain(y)  x,yedrel(A)"
  by (rule edrelI, auto simp add:Transset_def domain_def Pair_def)

lemma domain_trans: "Transset(A)  yA  x  domain(y)  xA"
  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 "zedrel(A)"
  then
  obtain x y where "xA" "yA" "z=x,y" "xdomain(y)"
    using edrelD
    by blast
  moreover from this
  obtain u v where "xu" "uv" "vy"
    unfolding domain_def Pair_def by auto
  moreover from calculation
  have "xeclose(A)" "yeclose(A)" "yeclose(A)"
    using arg_into_eclose Transset_eclose[unfolded Transset_def]
    by simp_all
  moreover from calculation
  have "veclose(A)"
    by auto
  moreover from calculation
  have "ueclose(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