# Theory Acc

theory Acc
imports Main
(*  Title:      ZF/Induct/Acc.thy
Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
*)

section ‹The accessible part of a relation›

theory Acc imports Main begin

text ‹
Inductive definition of ‹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 ‹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