Theory Acc_tools (Isabelle2008: June 2008)

theory Acc_tools imports Main
begin

section{*Definition of some results about the accesible part of a relation.*}

term acc
thm accp.intros

lemma wf_imp_subset_accP[rule_format]: "wf {(y,x) . Q y ∧ Q x ∧ r y x} ==> (∀ y x. Q x --> r y x --> Q y) ==> Q x --> accp r x"
  apply (erule wf_induct)
  apply clarify
  apply (rule accp.intros)
  apply (simp (no_asm_use))
  apply blast
  done

lemma subset_accP_imp_wf:
  assumes Q_subset: "∀ x. Q x --> accp r x"
  shows "wf ({(a,b). Q b ∧ r a b})"
proof -
  let ?s = "λ y x. Q x ∧ r y x"
  have "!! y x. ?s y x ==> r y x" by simp
  then have Q_sub_accP_s: "!! x. Q x ==> accp ?s x"
    apply (rule accp_subset[simplified le_fun_def le_bool_def, rule_format])
    apply (auto simp add: Q_subset)
    done
  {
    fix x
    have "¬ (Q x) ==> accp ?s x"
      apply (rule accp.intros)
      apply auto
      done
    with Q_sub_accP_s have "accp ?s x" by auto
  }
  note accP_univ = this
  show ?thesis
    apply (rule accp_wfPI[simplified wfP_def])
    apply (simp add: accP_univ)
    done
qed

lemma downchain_contra_imp_subset_accP:
  assumes downchain:"!! f. (!! i. Q (f i)) ==> (!! i. r (f (Suc i)) (f i)) ==> False"
  and downclosed: "!! y x. [|Q x; r y x|] ==> Q y"
  shows "Q x ==> accp r x"
  apply (rule wf_imp_subset_accP[where Q=Q])
  prefer 3
  apply simp
  prefer 2
  apply (rule_tac y=y and x=xa in downclosed)
  apply simp_all
  apply (simp add: wf_iff_no_infinite_down_chain)
  apply (insert downchain)
  apply blast
  done

lemma accP_subset_induct: 
  assumes Q_subset: "∀ x. Q x --> accp r x"
  assumes Q_downward: "∀ x y. Q x --> r y x --> Q y"
  assumes Q_a: "Q a"
  assumes Q_induct: "!! x. Q x ==> ∀ y. r y x --> P y ==> P x"
  shows "P a"
proof -
  show ?thesis
    apply (rule_tac accp_subset_induct[where x=a and D=Q and R=r])
    apply (simp add: le_fun_def Q_subset le_bool_def)
    apply (auto simp add: Q_a Q_subset)
    apply (erule Q_downward[rule_format])
    apply simp
    apply (erule Q_induct[rule_format])
    apply simp
    done
qed

end

Definition of some results about the accesible part of a relation.

lemma wf_imp_subset_accP:

  [| wf {(y, x). Q y ∧ Q x ∧ r y x}; !!y x. [| Q x; r y x |] ==> Q y; Q x |]
  ==> accp r x

lemma subset_accP_imp_wf:

  ∀x. Q x --> accp r x ==> wf {(a, b). Q b ∧ r a b}

lemma downchain_contra_imp_subset_accP:

  [| !!f. [| !!i. Q (f i); !!i. r (f (Suc i)) (f i) |] ==> False;
     !!y x. [| Q x; r y x |] ==> Q y; Q x |]
  ==> accp r x

lemma accP_subset_induct:

  [| ∀x. Q x --> accp r x; ∀x y. Q x --> r y x --> Q y; Q a;
     !!x. [| Q x; ∀y. r y x --> P y |] ==> P x |]
  ==> P a