Theory Recursion_Thms

sectionSome enhanced theorems on recursion

theory Recursion_Thms
  imports "ZF-Constructible.Datatype_absolute"

begin

― ‹Removing arities from inherited simpset
declare arity_And [simp del] arity_Or[simp del] arity_Implies[simp del]
  arity_Exists[simp del] arity_Iff[simp del]
  arity_subset_fm [simp del] arity_ordinal_fm[simp del] arity_transset_fm[simp del]

textWe prove results concerning definitions by well-founded
recursion on some relation termR and its transitive closure
termR^*
  (* Restrict the relation r to the field A*A *)

lemma fld_restrict_eq : "a  A  (r  A×A)-``{a} = (r-``{a}  A)"
  by(force)

lemma fld_restrict_mono : "relation(r)  A  B  r  A×A  r  B×B"
  by(auto)

lemma fld_restrict_dom :
  assumes "relation(r)" "domain(r)  A" "range(r) A"
  shows "r A×A = r"
proof (rule equalityI,blast,rule subsetI)
  { fix x
    assume xr: "x  r"
    from xr assms have " a b . x = a,b" by (simp add: relation_def)
    then obtain a b where "a,b  r" "a,b  rA×A" "x  rA×A"
      using assms xr
      by force
    then have "x r  A×A" by simp
  }
  then show "x  r  x rA×A" for x .
qed

definition tr_down :: "[i,i]  i"
  where "tr_down(r,a) = (r^+)-``{a}"

lemma tr_downD : "x  tr_down(r,a)  x,a  r^+"
  by (simp add: tr_down_def vimage_singleton_iff)

lemma pred_down : "relation(r)  r-``{a}  tr_down(r,a)"
  by(simp add: tr_down_def vimage_mono r_subset_trancl)

lemma tr_down_mono : "relation(r)  x  r-``{a}  tr_down(r,x)  tr_down(r,a)"
  by(rule subsetI,simp add:tr_down_def,auto dest: underD,force simp add: underI r_into_trancl trancl_trans)

lemma rest_eq :
  assumes "relation(r)" and "r-``{a}  B" and "a  B"
  shows "r-``{a} = (rB×B)-``{a}"
proof (intro equalityI subsetI)
  fix x
  assume "x  r-``{a}"
  then
  have "x  B" using assms by (simp add: subsetD)
  from x r-``{a}
  have "x,a  r" using underD by simp
  then
  show "x  (rB×B)-``{a}" using xB aB underI by simp
next
  from assms
  show "x  r -`` {a}" if  "x  (r  B×B) -`` {a}" for x
    using vimage_mono that by auto
qed

lemma wfrec_restr_eq : "r' = r  A×A  wfrec[A](r,a,H) = wfrec(r',a,H)"
  by(simp add:wfrec_on_def)

lemma wfrec_restr :
  assumes rr: "relation(r)" and wfr:"wf(r)"
  shows  "a  A  tr_down(r,a)  A  wfrec(r,a,H) = wfrec[A](r,a,H)"
proof (induct a arbitrary:A rule:wf_induct_raw[OF wfr] )
  case (1 a)
  have wfRa : "wf[A](r)"
    using wf_subset wfr wf_on_def Int_lower1 by simp
  from pred_down rr
  have "r -`` {a}  tr_down(r, a)" .
  with 1
  have "r-``{a}  A" by (force simp add: subset_trans)
  {
    fix x
    assume x_a : "x  r-``{a}"
    with r-``{a}  A
    have "x  A" ..
    from pred_down rr
    have b : "r -``{x}  tr_down(r,x)" .
    then
    have "tr_down(r,x)  tr_down(r,a)"
      using tr_down_mono x_a rr by simp
    with 1
    have "tr_down(r,x)  A" using subset_trans by force
    have "x,a  r" using x_a  underD by simp
    with 1 tr_down(r,x)  A x  A
    have "wfrec(r,x,H) = wfrec[A](r,x,H)" by simp
  }
  then
  have "x r-``{a}  wfrec(r,x,H) =  wfrec[A](r,x,H)" for x  .
  then
  have Eq1 :"(λ x  r-``{a} . wfrec(r,x,H)) = (λ x  r-``{a} . wfrec[A](r,x,H))"
    using lam_cong by simp

  from assms
  have "wfrec(r,a,H) = H(a,λ x  r-``{a} . wfrec(r,x,H))" by (simp add:wfrec)
  also
  have "... = H(a,λ x  r-``{a} . wfrec[A](r,x,H))"
    using assms Eq1 by simp
  also from 1 r-``{a}  A
  have "... = H(a,λ x  (rA×A)-``{a} . wfrec[A](r,x,H))"
    using assms rest_eq  by simp
  also from aA
  have "... = H(a,λ x  (r-``{a})A . wfrec[A](r,x,H))"
    using fld_restrict_eq by simp
  also from aA wf[A](r)
  have "... = wfrec[A](r,a,H)" using wfrec_on by simp
  finally show ?case .
qed

lemmas wfrec_tr_down = wfrec_restr[OF _ _ _ subset_refl]

lemma wfrec_trans_restr : "relation(r)  wf(r)  trans(r)  r-``{a}A  a  A 
  wfrec(r, a, H) = wfrec[A](r, a, H)"
  by(subgoal_tac "tr_down(r,a)  A",auto simp add : wfrec_restr tr_down_def trancl_eq_r)


lemma field_trancl : "field(r^+) = field(r)"
  by (blast intro: r_into_trancl dest!: trancl_type [THEN subsetD])

definition
  Rrel :: "[iio,i]  i" where
  "Rrel(R,A)  {zA×A. x y. z = x, y  R(x,y)}"

lemma RrelI : "x  A  y  A  R(x,y)  x,y  Rrel(R,A)"
  unfolding Rrel_def by simp

lemma Rrel_mem: "Rrel(mem,x) = Memrel(x)"
  unfolding Rrel_def Memrel_def ..

lemma relation_Rrel: "relation(Rrel(R,d))"
  unfolding Rrel_def relation_def by simp

lemma field_Rrel: "field(Rrel(R,d))   d"
  unfolding Rrel_def by auto

lemma Rrel_mono : "A  B  Rrel(R,A)  Rrel(R,B)"
  unfolding Rrel_def by blast

lemma Rrel_restr_eq : "Rrel(R,A)  B×B = Rrel(R,AB)"
  unfolding Rrel_def by blast

(* now a consequence of the previous lemmas *)
lemma field_Memrel : "field(Memrel(A))  A"
  (* unfolding field_def using Ordinal.Memrel_type by blast *)
  using Rrel_mem field_Rrel by blast

lemma restrict_trancl_Rrel:
  assumes "R(w,y)"
  shows "restrict(f,Rrel(R,d)-``{y})`w
       = restrict(f,(Rrel(R,d)^+)-``{y})`w"
proof (cases "yd")
  let ?r="Rrel(R,d)" and ?s="(Rrel(R,d))^+"
  case True
  show ?thesis
  proof (cases "wd")
    case True
    with yd assms
    have "w,y?r"
      unfolding Rrel_def by blast
    then
    have "w,y?s"
      using r_subset_trancl[of ?r] relation_Rrel[of R d] by blast
    with w,y?r
    have "w?r-``{y}" "w?s-``{y}"
      using vimage_singleton_iff by simp_all
    then
    show ?thesis by simp
  next
    case False
    then
    have "wdomain(restrict(f,?r-``{y}))"
      using subsetD[OF field_Rrel[of R d]] by auto
    moreover from wd
    have "wdomain(restrict(f,?s-``{y}))"
      using subsetD[OF field_Rrel[of R d], of w] field_trancl[of ?r]
        fieldI1[of w y ?s] by auto
    ultimately
    have "restrict(f,?r-``{y})`w = 0" "restrict(f,?s-``{y})`w = 0"
      unfolding apply_def by auto
    then show ?thesis by simp
  qed
next
  let ?r="Rrel(R,d)"
  let ?s="?r^+"
  case False
  then
  have "?r-``{y}=0"
    unfolding Rrel_def by blast
  then
  have "w?r-``{y}" by simp
  with yd assms
  have "yfield(?s)"
    using field_trancl subsetD[OF field_Rrel[of R d]] by force
  then
  have "w?s-``{y}"
    using vimage_singleton_iff by blast
  with w?r-``{y}
  show ?thesis by simp
qed

lemma restrict_trans_eq:
  assumes "w  y"
  shows "restrict(f,Memrel(eclose({x}))-``{y})`w
       = restrict(f,(Memrel(eclose({x}))^+)-``{y})`w"
  using assms restrict_trancl_Rrel[of mem ] Rrel_mem by (simp)

lemma wf_eq_trancl:
  assumes " f y . H(y,restrict(f,R-``{y})) = H(y,restrict(f,R^+-``{y}))"
  shows  "wfrec(R, x, H) = wfrec(R^+, x, H)" (is "wfrec(?r,_,_) = wfrec(?r',_,_)")
proof -
  have "wfrec(R, x, H) = wftrec(?r^+, x, λy f. H(y, restrict(f,?r-``{y})))"
    unfolding wfrec_def ..
  also
  have " ... = wftrec(?r^+, x, λy f. H(y, restrict(f,(?r^+)-``{y})))"
    using assms by simp
  also
  have " ... =  wfrec(?r^+, x, H)"
    unfolding wfrec_def using trancl_eq_r[OF relation_trancl trans_trancl] by simp
  finally
  show ?thesis .
qed

lemma transrec_equal_on_Ord:
assumes
   "x f . Ord(x)  foo(x,f) = bar(x,f)"
   "Ord(α)"
shows
  "transrec(α, foo) = transrec(α, bar)"
proof -
  have "transrec(β,foo) = transrec(β,bar)" if "Ord(β)" for β
    using that
  proof (induct rule:trans_induct)
    case (step β)
    have "transrec(β, foo) = foo(β, λxβ. transrec(x, foo))"
      using def_transrec[of "λx. transrec(x, foo)" foo] by blast
    also from assms and step
    have "  = bar(β, λxβ. transrec(x, foo))"
      by simp
    also from step
    have "  = bar(β, λxβ. transrec(x, bar))"
      by (auto)
    also
    have "  = transrec(β, bar)"
      using def_transrec[of "λx. transrec(x, bar)" bar, symmetric]
      by blast
    finally
    show "transrec(β, foo) = transrec(β, bar)" .
  qed
  with assms
  show ?thesis by simp
qed

― ‹Next theorem is very similar to @{thm transrec_equal_on_Ord}
lemma (in M_eclose) transrec_equal_on_M:
assumes
   "x f . M(x)  M(f)  foo(x,f) = bar(x,f)"
   "β. M(β)  transrec_replacement(M,is_foo,β)" "relation2(M,is_foo,foo)"
   "strong_replacement(M, λx y. y = x, transrec(x, foo))"
   "x[M]. g[M]. function(g)  M(foo(x,g))"
   "M(α)" "Ord(α)"
shows
  "transrec(α, foo) = transrec(α, bar)"
proof -
  have "M(transrec(x, foo))" if "Ord(x)" and "M(x)" for x
    using that assms transrec_closed[of is_foo]
    by simp
  have "transrec(β,foo) = transrec(β,bar)" "M(transrec(β,foo))" if "Ord(β)" "M(β)" for β
    using that
  proof (induct rule:trans_induct)
    case (step β)
    moreover
    assume "M(β)"
    moreover
    note Ord(β) M(β)  M(transrec(β, foo))
    ultimately
    show "M(transrec(β, foo))" by blast
    with step M(β) x. Ord(x) M(x)  M(transrec(x, foo))
      strong_replacement(M, λx y. y = x, transrec(x, foo))
    have "M(λxβ. transrec(x, foo))"
      using Ord_in_Ord transM[of _ β]
      by (rule_tac lam_closed) auto
    have "transrec(β, foo) = foo(β, λxβ. transrec(x, foo))"
      using def_transrec[of "λx. transrec(x, foo)" foo] by blast
    also from assms and M(λxβ. transrec(x, foo)) M(β)
    have "  = bar(β, λxβ. transrec(x, foo))"
      by simp
    also from step and M(β)
    have "  = bar(β, λxβ. transrec(x, bar))"
      using transM[of _ β] by (auto)
    also
    have "  = transrec(β, bar)"
      using def_transrec[of "λx. transrec(x, bar)" bar, symmetric]
      by blast
    finally
    show "transrec(β, foo) = transrec(β, bar)" .
  qed
  with assms
  show ?thesis by simp
qed


lemma ordermap_restr_eq:
  assumes "well_ord(X,r)"
  shows "ordermap(X, r) = ordermap(X, r  X×X)"
proof -
  let ?A="λx . Order.pred(X, x, r)"
  let ?B="λx . Order.pred(X, x, r  X × X)"
  let ?F="λx f. f `` ?A(x)"
  let ?G="λx f. f `` ?B(x)"
  let ?P="λ z. zX  wfrec(r  X × X,z,λx f. f `` ?A(x)) = wfrec(r  X × X,z,λx f. f `` ?B(x))"
  have pred_eq:
    "Order.pred(X, x, r  X × X) = Order.pred(X, x, r)" if "xX" for x
    unfolding Order.pred_def using that by auto
  from assms
  have wf_onX:"wf(r  X × X)" unfolding well_ord_def wf_on_def by simp
  {
    have "?P(z)" for z
    proof(induct rule:wf_induct[where P="?P",OF wf_onX])
      case (1 x)
      {
        assume "xX"
        from 1
        have lam_eq:
            "(λw(r  X × X) -`` {x}. wfrec(r  X × X, w, ?F)) =
             (λw(r  X × X) -`` {x}. wfrec(r  X × X, w, ?G))" (is "?L=?R")
        proof -
          have "wfrec(r  X × X, w, ?F) = wfrec(r  X × X, w, ?G)" if "w(rX×X)-``{x}" for w
            using 1 that by auto
          then show ?thesis using lam_cong[OF refl] by simp
        qed
        then
        have "wfrec(r  X × X, x, ?F) = ?L `` ?A(x)"
          using wfrec[OF wf_onX,of x ?F] by simp
        also have "... =  ?R `` ?B(x)"
          using lam_eq pred_eq[OF x_] by simp
        also
        have "... = wfrec(r  X × X, x, ?G)"
          using wfrec[OF wf_onX,of x ?G] by simp
        finally
        have "wfrec(r  X × X, x, ?F) = wfrec(r  X × X, x, ?G)" by simp
      }
      then
      show ?case by simp
    qed
  }
  then
  show ?thesis
    unfolding ordermap_def wfrec_on_def using Int_ac by simp
qed

end