author | kleing |
Sun, 09 Dec 2001 14:34:18 +0100 | |
changeset 12428 | f3033eed309a |
parent 11327 | cd2c27a23df1 |
child 12566 | fe20540bcf93 |
permissions | -rw-r--r-- |
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 |