Quelle  Acc.thy

(*  Title:      ZF/Induct/Acc.thy
  Author: Lawrence C Paulson, Cambridge University Computer Laboratory
  Copyright 1994 University of Cambridge
*)

section ‹The accessible part of a relation›

theory Acc imports ZF begin

text ‹
  Inductive definition of ‹acc(r)›; see 🍋‹"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 🍋‹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