author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 18241  afdba6b3e383 
permissions  rwrr 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Library/Accessible_Part.thy 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

5 
*) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

6 

14706  7 
header {* The accessible part of a relation *} 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

8 

15131  9 
theory Accessible_Part 
15140  10 
imports Main 
15131  11 
begin 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

12 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

13 
subsection {* Inductive definition *} 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

14 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

15 
text {* 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

16 
Inductive definition of the accessible part @{term "acc r"} of a 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

17 
relation; see also \cite{paulintlca}. 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

18 
*} 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

19 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

20 
consts 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

21 
acc :: "('a \<times> 'a) set => 'a set" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

22 
inductive "acc r" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

23 
intros 
10734  24 
accI: "(!!y. (y, x) \<in> r ==> y \<in> acc r) ==> x \<in> acc r" 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

25 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

26 
syntax 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

27 
termi :: "('a \<times> 'a) set => 'a set" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

28 
translations 
10388  29 
"termi r" == "acc (r\<inverse>)" 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

30 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

31 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

32 
subsection {* Induction rules *} 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

33 

10734  34 
theorem acc_induct: 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

35 
"a \<in> acc r ==> 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

36 
(!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r > P y ==> P x) ==> P a" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

37 
proof  
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

38 
assume major: "a \<in> acc r" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

39 
assume hyp: "!!x. x \<in> acc r ==> \<forall>y. (y, x) \<in> r > P y ==> P x" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

40 
show ?thesis 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

41 
apply (rule major [THEN acc.induct]) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

42 
apply (rule hyp) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

43 
apply (rule accI) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

44 
apply fast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

45 
apply fast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

46 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

47 
qed 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

48 

10734  49 
theorems acc_induct_rule = acc_induct [rule_format, induct set: acc] 
50 

10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

51 
theorem acc_downward: "b \<in> acc r ==> (a, b) \<in> r ==> a \<in> acc r" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

52 
apply (erule acc.elims) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

53 
apply fast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

54 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

55 

10388  56 
lemma acc_downwards_aux: "(b, a) \<in> r\<^sup>* ==> a \<in> acc r > b \<in> acc r" 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

57 
apply (erule rtrancl_induct) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

58 
apply blast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

59 
apply (blast dest: acc_downward) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

60 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

61 

10388  62 
theorem acc_downwards: "a \<in> acc r ==> (b, a) \<in> r\<^sup>* ==> b \<in> acc r" 
10248
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

63 
apply (blast dest: acc_downwards_aux) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

64 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

65 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

66 
theorem acc_wfI: "\<forall>x. x \<in> acc r ==> wf r" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

67 
apply (rule wfUNIVI) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

68 
apply (induct_tac P x rule: acc_induct) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

69 
apply blast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

70 
apply blast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

71 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

72 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

73 
theorem acc_wfD: "wf r ==> x \<in> acc r" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

74 
apply (erule wf_induct) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

75 
apply (rule accI) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

76 
apply blast 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

77 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

78 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

79 
theorem wf_acc_iff: "wf r = (\<forall>x. x \<in> acc r)" 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

80 
apply (blast intro: acc_wfI dest: acc_wfD) 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

81 
done 
d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

82 

d99e5eeb16f4
The accessible part of a relation (from HOL/Induct/Acc);
wenzelm
parents:
diff
changeset

83 
end 