# Theory Acc

Up to index of Isabelle/ZF/UNITY

theory Acc
imports Main
begin

    (*  Title:      ZF/Induct/Acc.thy
        ID:         $Id: Acc.thy,v 1.4 2005/06/17 14:15:11 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header {* The accessible part of a relation *}

    theory Acc imports Main begin

    text {*
      Inductive definition of @{text "acc(r)"}; see \cite{paulin-tlca}.
    *}

    consts
      acc :: "i => i"

    inductive
      domains "acc(r)" ⊆ "field(r)"
      intros
        vimage:  "[| r-``{a}: Pow(acc(r)); a ∈ field(r) |] ==> a ∈ acc(r)"
      monos      Pow_mono

    text {*
      The introduction rule must require @{prop "a ∈ field(r)"},
      otherwise @{text "acc(r)"} would be a proper class!

      \medskip
      The intended introduction rule:
    *}

    lemma accI: "[| !!b. <b,a>:r ==> b ∈ acc(r);  a ∈ field(r) |] ==> a ∈ acc(r)"
      by (blast intro: acc.intros)

    lemma acc_downward: "[| b ∈ acc(r);  <a,b>: r |] ==> a ∈ acc(r)"
      by (erule acc.cases) blast

    lemma acc_induct [induct set: acc]:
        "[| a ∈ acc(r);
            !!x. [| x ∈ acc(r);  ∀y. <y,x>:r --> P(y) |] ==> P(x)
         |] ==> P(a)"
      by (erule acc.induct) (blast intro: acc.intros)

    lemma wf_on_acc: "wf[acc(r)](r)"
      apply (rule wf_onI2)
      apply (erule acc_induct)
      apply fast
      done

    lemma acc_wfI: "field(r) ⊆ acc(r) ==> wf(r)"
      by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf])

    lemma acc_wfD: "wf(r) ==> field(r) ⊆ acc(r)"
      apply (rule subsetI)
      apply (erule wf_induct2, assumption)
       apply (blast intro: accI)+
      done

    lemma wf_acc_iff: "wf(r) <-> field(r) ⊆ acc(r)"
      by (rule iffI, erule acc_wfD, erule acc_wfI)

    end

lemma accI:

      [| !!b. ⟨b, a⟩ ∈ r ==> b ∈ acc(r); a ∈ field(r) |] ==> a ∈ acc(r)

lemma acc_downward:

      [| b ∈ acc(r); ⟨a, b⟩ ∈ r |] ==> a ∈ acc(r)

lemma acc_induct:

      [| a ∈ acc(r); !!x. [| x ∈ acc(r); ∀y. ⟨y, x⟩ ∈ r --> P(y) |] ==> P(x) |]
      ==> P(a)

lemma wf_on_acc:

      wf[acc(r)](r)

lemma acc_wfI:

      field(r) ⊆ acc(r) ==> wf(r)

lemma acc_wfD:

      wf(r) ==> field(r) ⊆ acc(r)

lemma wf_acc_iff:

      wf(r) <-> field(r) ⊆ acc(r)