1(*  Title:      ZF/Induct/Acc.thy
2    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
3    Copyright   1994  University of Cambridge
4*)
5
6section \<open>The accessible part of a relation\<close>
7
8theory Acc imports ZF begin
9
10text \<open>
11  Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
12\<close>
13
14consts
15  acc :: "i => i"
16
17inductive
18  domains "acc(r)" \<subseteq> "field(r)"
19  intros
20    vimage:  "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
21  monos      Pow_mono
22
23text \<open>
24  The introduction rule must require \<^prop>\<open>a \<in> field(r)\<close>,
25  otherwise \<open>acc(r)\<close> would be a proper class!
26
27  \medskip
28  The intended introduction rule:
29\<close>
30
31lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r);  a \<in> field(r) |] ==> a \<in> acc(r)"
32  by (blast intro: acc.intros)
33
34lemma acc_downward: "[| b \<in> acc(r);  <a,b>: r |] ==> a \<in> acc(r)"
35  by (erule acc.cases) blast
36
37lemma acc_induct [consumes 1, case_names vimage, induct set: acc]:
38    "[| a \<in> acc(r);
39        !!x. [| x \<in> acc(r);  \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x)
40     |] ==> P(a)"
41  by (erule acc.induct) (blast intro: acc.intros)
42
43lemma wf_on_acc: "wf[acc(r)](r)"
44  apply (rule wf_onI2)
45  apply (erule acc_induct)
46  apply fast
47  done
48
49lemma acc_wfI: "field(r) \<subseteq> acc(r) \<Longrightarrow> wf(r)"
50  by (erule wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf])
51
52lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)"
53  apply (rule subsetI)
54  apply (erule wf_induct2, assumption)
55   apply (blast intro: accI)+
56  done
57
58lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)"
59  by (rule iffI, erule acc_wfD, erule acc_wfI)
60
61end
62