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 [consumes 1, case_names vimage, 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