|
1 (* Title: HOL/Library/Accessible_Part.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 *) |
|
6 |
|
7 header {* |
|
8 \title{The accessible part of a relation} |
|
9 \author{Lawrence C Paulson} |
|
10 *} |
|
11 |
|
12 theory Accessible_Part = Main: |
|
13 |
|
14 |
|
15 subsection {* Inductive definition *} |
|
16 |
|
17 text {* |
|
18 Inductive definition of the accessible part @{term "acc r"} of a |
|
19 relation; see also \cite{paulin-tlca}. |
|
20 *} |
|
21 |
|
22 consts |
|
23 acc :: "('a \<times> 'a) set => 'a set" |
|
24 inductive "acc r" |
|
25 intros |
|
26 accI [rule_format]: "\<forall>y. (y, x) \<in> r --> y \<in> acc r ==> x \<in> acc r" |
|
27 |
|
28 syntax |
|
29 termi :: "('a \<times> 'a) set => 'a set" |
|
30 translations |
|
31 "termi r" == "acc (r^-1)" |
|
32 |
|
33 |
|
34 subsection {* Induction rules *} |
|
35 |
|
36 theorem acc_induct [induct set: acc]: |
|
37 "a \<in> acc r ==> |
|
38 (!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x) ==> P a" |
|
39 proof - |
|
40 assume major: "a \<in> acc r" |
|
41 assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r --> P y ==> P x" |
|
42 show ?thesis |
|
43 apply (rule major [THEN acc.induct]) |
|
44 apply (rule hyp) |
|
45 apply (rule accI) |
|
46 apply fast |
|
47 apply fast |
|
48 done |
|
49 qed |
|
50 |
|
51 theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r" |
|
52 apply (erule acc.elims) |
|
53 apply fast |
|
54 done |
|
55 |
|
56 lemma acc_downwards_aux: "(b, a) \<in> r^* ==> a \<in> acc r --> b \<in> acc r" |
|
57 apply (erule rtrancl_induct) |
|
58 apply blast |
|
59 apply (blast dest: acc_downward) |
|
60 done |
|
61 |
|
62 theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r^* ==> b \<in> acc r" |
|
63 apply (blast dest: acc_downwards_aux) |
|
64 done |
|
65 |
|
66 theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r" |
|
67 apply (rule wfUNIVI) |
|
68 apply (induct_tac P x rule: acc_induct) |
|
69 apply blast |
|
70 apply blast |
|
71 done |
|
72 |
|
73 theorem acc_wfD: "wf r ==> x \<in> acc r" |
|
74 apply (erule wf_induct) |
|
75 apply (rule accI) |
|
76 apply blast |
|
77 done |
|
78 |
|
79 theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)" |
|
80 apply (blast intro: acc_wfI dest: acc_wfD) |
|
81 done |
|
82 |
|
83 end |