Theory Recursion_Thms

theory Recursion_Thms imports ZF.WF begin

(* 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> ∈ r∩A*A" "x ∈ r∩A*A" 
      using assms xr 
      by force
    then have "x∈ r ∩ A*A" by simp
  }
  then show "x ∈ r ⟹ x∈ r∩A*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} = (r∩B*B)-``{a}"
proof 
  { fix x 
    assume "x ∈ r-``{a}"
    then have "x ∈ B" using assms by (simp add: subsetD)
    from ‹x∈ r-``{a}› underD have "<x,a> ∈ r" by simp
    then have "x ∈ (r∩B*B)-``{a}" using ‹x ∈ B› ‹a∈B› underI by simp
  }
  then show "r -`` {a} ⊆ (r∩B*B)-`` {a}" by auto
next
  from vimage_mono assms
  show "(r∩B*B) -`` {a} ⊆ r -`` {a}" 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)
  from wf_subset wfr wf_on_def Int_lower1 have wfRa : "wf[A](r)" by simp
  from pred_down rr have "r -`` {a} ⊆ tr_down(r, a)"  .
  then have "r-``{a} ⊆ A" using 1 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
    then have "tr_down(r,x) ⊆ A" using 1 subset_trans by force
    have "<x,a> ∈ r" using x_a  underD by simp
    then have "wfrec(r,x,H) = wfrec[A](r,x,H)" 
      using 1 ‹tr_down(r,x) ⊆ A› ‹x ∈ A› 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 have "... = H(a,λ x ∈ (r∩A*A)-``{a} . wfrec[A](r,x,H))"
    using 1 assms rest_eq ‹r-``{a} ⊆ A› by simp
  also have "... = H(a,λ x ∈ (r-``{a})∩A . wfrec[A](r,x,H))"
    using ‹a∈A› fld_restrict_eq by simp
  also have "... = wfrec[A](r,a,H)" using ‹wf[A](r)› ‹a∈A› 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)  

end