Quelle  Recursion_Thms.thy

sectionjava.lang.StringIndexOutOfBoundsException: Range [109, 108) out of bounds for length 121

  Recursion_Thms imports ZF.Epsilon begin

 ‹We prove results concerning definitions by well-founded
 "l_to_tree_order_wf heap_is_wellformed_{Core_DOM} parent_child_rel type_wf known_ptr known_ptrs
 term‹R^*››
 (* Restrict the relation r to the field A*A *)

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

  fld_restrict_mono : "relation(r) ==> A ⊆ B ==> r ∩ A×A ⊆ r ∩ B×B"
 by(auto)

  fld_restrict_dom :
 assumes "relation(r)" "domain(r) ⊆ A" "range(r)⊆ A"
 shows "r∩ A×A = r"
  (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 .
 

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

  tr_downD : "x ∈ tr_down(r,a) ==> ⟨x,a⟩ ∈ r^+"
 by (simp add: tr_down_def vimage_singleton_iff)

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

  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)

  rest_eq :
 assumes "relation(r)" and "r-``{a} ⊆ B" and "a ∈ B"
 shows "r-``{a} = (r∩B×B)-``{a}"
  (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 ∈ (r∩B×B)-``{a}" using ‹x∈B› ‹a∈B› underI by simp
 
 from assms
 show "x ∈ r -`` {a}" if "x ∈ (r ∩ B×B) -`` {a}" for x
 using vimage_mono that by auto
 

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

  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)"
  (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 ∈ (r∩A×A)-``{a} . wfrec[A](r,x,H))"
 using assms rest_eq by simp
 also from ‹a∈A›
 have "... = H(a,λ x ∈ (r-``{a})∩A . wfrec[A](r,x,H))"
 using fld_restrict_eq by simp
 also from ‹a∈A› ‹wf[A](r)›
 have "... = wfrec[A](r,a,H)" using wfrec_on by simp
 finally show ?case .
 

  wfrec_tr_down = wfrec_restr[OF _ _ _ subset_refl]

  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)


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

 
 Rrel :: "[i==>i==>o,i] ==> i" where
 "Rrel(R,A) ≡ {z∈A×A. ∃x y. z = ⟨x, y⟩ ∧ R(x,y)}"

  RrelI : "x ∈ A ==> y ∈ A ==> R(x,y) ==> ⟨x,y⟩ ∈ Rrel(R,A)"
 unfolding Rrel_def by simp

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

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

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

  Rrel_mono : "A ⊆ B ==> Rrel(R,A) ⊆ Rrel(R,B)"
 unfolding Rrel_def by blast

  Rrel_restr_eq : "Rrel(R,A) ∩ B×B = Rrel(R,A∩B)"
 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 "y∈d")
  let ?r="Rrel(R,d)" and ?s="(Rrel(R,d))^+"
  case True
  show ?thesis
  proof (cases "w∈d")
    case True
    with ‹y∈d› 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 "w∉domain(restrict(f,?r-``{y}))"
      using subsetD[OF field_Rrel[of R d]] by auto
    moreover from ‹w∉d›
    have "w∉domain(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 ‹y∉d› assms
  have "y∉field(?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

end