author | nipkow |
Sun, 04 Nov 2018 12:07:24 +0100 | |
changeset 69232 | 2b913054a9cf |
parent 65449 | c82e63b11b8b |
child 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
12560 | 1 |
(* Title: ZF/Induct/Acc.thy |
12088 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1994 University of Cambridge |
|
12610 | 4 |
*) |
12088 | 5 |
|
60770 | 6 |
section \<open>The accessible part of a relation\<close> |
12088 | 7 |
|
65449
c82e63b11b8b
clarified main ZF.thy / ZFC.thy, and avoid name clash with global HOL/Main.thy;
wenzelm
parents:
61798
diff
changeset
|
8 |
theory Acc imports ZF begin |
12088 | 9 |
|
60770 | 10 |
text \<open> |
61798 | 11 |
Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}. |
60770 | 12 |
\<close> |
12610 | 13 |
|
12088 | 14 |
consts |
12610 | 15 |
acc :: "i => i" |
12088 | 16 |
|
17 |
inductive |
|
12610 | 18 |
domains "acc(r)" \<subseteq> "field(r)" |
12560 | 19 |
intros |
20 |
vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)" |
|
12088 | 21 |
monos Pow_mono |
22 |
||
60770 | 23 |
text \<open> |
12610 | 24 |
The introduction rule must require @{prop "a \<in> field(r)"}, |
61798 | 25 |
otherwise \<open>acc(r)\<close> would be a proper class! |
12560 | 26 |
|
12610 | 27 |
\medskip |
28 |
The intended introduction rule: |
|
60770 | 29 |
\<close> |
12610 | 30 |
|
12560 | 31 |
lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r); a \<in> field(r) |] ==> a \<in> acc(r)" |
12610 | 32 |
by (blast intro: acc.intros) |
12560 | 33 |
|
34 |
lemma acc_downward: "[| b \<in> acc(r); <a,b>: r |] ==> a \<in> acc(r)" |
|
12610 | 35 |
by (erule acc.cases) blast |
12560 | 36 |
|
18414 | 37 |
lemma acc_induct [consumes 1, case_names vimage, induct set: acc]: |
12610 | 38 |
"[| a \<in> acc(r); |
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
35762
diff
changeset
|
39 |
!!x. [| x \<in> acc(r); \<forall>y. <y,x>:r \<longrightarrow> P(y) |] ==> P(x) |
12560 | 40 |
|] ==> P(a)" |
12610 | 41 |
by (erule acc.induct) (blast intro: acc.intros) |
12560 | 42 |
|
43 |
lemma wf_on_acc: "wf[acc(r)](r)" |
|
12610 | 44 |
apply (rule wf_onI2) |
45 |
apply (erule acc_induct) |
|
46 |
apply fast |
|
47 |
done |
|
12560 | 48 |
|
12610 | 49 |
lemma 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]) |
|
12560 | 51 |
|
52 |
lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)" |
|
12610 | 53 |
apply (rule subsetI) |
54 |
apply (erule wf_induct2, assumption) |
|
55 |
apply (blast intro: accI)+ |
|
56 |
done |
|
12560 | 57 |
|
46822
95f1e700b712
mathematical symbols for Isabelle/ZF example theories
paulson
parents:
35762
diff
changeset
|
58 |
lemma wf_acc_iff: "wf(r) \<longleftrightarrow> field(r) \<subseteq> acc(r)" |
12610 | 59 |
by (rule iffI, erule acc_wfD, erule acc_wfI) |
12560 | 60 |
|
12088 | 61 |
end |