(* 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)