Theory Acc
section ‹The accessible part of a relation›
theory Acc imports ZF 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