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