author  kleing 
Sun, 09 Dec 2001 14:34:18 +0100  
changeset 12428  f3033eed309a 
parent 11327  cd2c27a23df1 
child 12566  fe20540bcf93 
permissions  rwrr 
10213  1 
(* Title: HOL/Transitive_Closure.thy 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1992 University of Cambridge 

5 

6 
Relfexive and Transitive closure of a relation 

7 

8 
rtrancl is reflexive/transitive closure; 

9 
trancl is transitive closure 

10 
reflcl is reflexive closure 

11 

10331  12 
These postfix operators have MAXIMUM PRIORITY, forcing their operands 
13 
to be atomic. 

10213  14 
*) 
15 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

16 
theory Transitive_Closure = Inductive 
10980  17 
files ("Transitive_Closure_lemmas.ML"): 
10213  18 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

19 
consts 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

20 
rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999) 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

21 

cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

22 
inductive "r^*" 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

23 
intros 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

24 
rtrancl_refl [intro!, simp]: "(a, a) : r^*" 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

25 
rtrancl_into_rtrancl: "[ (a,b) : r^*; (b,c) : r ] ==> (a,c) : r^*" 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

26 

10213  27 
constdefs 
10331  28 
trancl :: "('a * 'a) set => ('a * 'a) set" ("(_^+)" [1000] 999) 
29 
"r^+ == r O rtrancl r" 

10213  30 

31 
syntax 

10331  32 
"_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_^=)" [1000] 999) 
10213  33 
translations 
34 
"r^=" == "r Un Id" 

35 

10827  36 
syntax (xsymbols) 
10331  37 
rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) 
38 
trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) 

39 
"_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) 

40 

10980  41 
use "Transitive_Closure_lemmas.ML" 
42 

10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

43 

11090  44 
lemma reflcl_trancl [simp]: "(r^+)^= = r^*" 
11084  45 
apply safe 
46 
apply (erule trancl_into_rtrancl) 

47 
apply (blast elim: rtranclE dest: rtrancl_into_trancl1) 

48 
done 

10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

49 

11090  50 
lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" 
11084  51 
apply safe 
52 
apply (drule trancl_into_rtrancl) 

53 
apply simp 

54 
apply (erule rtranclE) 

55 
apply safe 

56 
apply (rule r_into_trancl) 

57 
apply simp 

58 
apply (rule rtrancl_into_trancl1) 

59 
apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD]) 

60 
apply fast 

61 
done 

10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

62 

11090  63 
lemma trancl_empty [simp]: "{}^+ = {}" 
11084  64 
by (auto elim: trancl_induct) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

65 

11090  66 
lemma rtrancl_empty [simp]: "{}^* = Id" 
11084  67 
by (rule subst [OF reflcl_trancl]) simp 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

68 

11090  69 
lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+" 
11084  70 
by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) 
71 

10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

72 

74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

73 
(* should be merged with the main body of lemmas: *) 
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

74 

11090  75 
lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" 
11084  76 
by blast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

77 

11090  78 
lemma Range_rtrancl [simp]: "Range (R^*) = UNIV" 
11084  79 
by blast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

80 

11090  81 
lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*" 
11084  82 
by (rule rtrancl_Un_rtrancl [THEN subst]) fast 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

83 

11090  84 
lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*" 
11084  85 
by (blast intro: subsetD [OF rtrancl_Un_subset]) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

86 

11090  87 
lemma trancl_domain [simp]: "Domain (r^+) = Domain r" 
11084  88 
by (unfold Domain_def) (blast dest: tranclD) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

89 

11090  90 
lemma trancl_range [simp]: "Range (r^+) = Range r" 
11084  91 
by (simp add: Range_def trancl_converse [symmetric]) 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

92 

11115  93 
lemma Not_Domain_rtrancl: 
94 
"x ~: Domain R ==> ((x, y) : R^*) = (x = y)" 

95 
apply (auto) 

96 
by (erule rev_mp, erule rtrancl_induct, auto) 

11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

97 

12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

98 
(* more about converse rtrancl and trancl, should be merged with main body *) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

99 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

100 
lemma converse_rtrancl_into_rtrancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R^* \<Longrightarrow> (a,c) \<in> R^*" 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

101 
by (erule rtrancl_induct) (fast intro: rtrancl_into_rtrancl)+ 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

102 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

103 
lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+" 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

104 
by (fast intro: trancl_trans) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

105 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

106 
lemma trancl_into_trancl [rule_format]: 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

107 
"(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+" 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

108 
apply (erule trancl_induct) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

109 
apply (fast intro: r_r_into_trancl) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

110 
apply (fast intro: r_r_into_trancl trancl_trans) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

111 
done 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

112 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

113 
lemma trancl_rtrancl_trancl: 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

114 
"(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+" 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

115 
apply (drule tranclD) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

116 
apply (erule exE, erule conjE) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

117 
apply (drule rtrancl_trans, assumption) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

118 
apply (drule rtrancl_into_trancl2, assumption) 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

119 
apply assumption 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

120 
done 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

121 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

122 
lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

123 
trancl_into_trancl trancl_into_trancl2 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

124 
rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

125 
rtrancl_trancl_trancl trancl_rtrancl_trancl 
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

126 

f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

127 
declare trancl_into_rtrancl [elim] 
11327
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

128 

cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

129 
declare rtrancl_induct [induct set: rtrancl] 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

130 
declare rtranclE [cases set: rtrancl] 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

131 
declare trancl_induct [induct set: trancl] 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

132 
declare tranclE [cases set: trancl] 
cd2c27a23df1
Transitive closure is now defined via "inductive".
berghofe
parents:
11115
diff
changeset

133 

10213  134 
end 