author | wenzelm |
Fri, 09 Feb 2001 11:40:10 +0100 | |
changeset 11084 | 32c1deea5bcd |
parent 10996 | 74e970389def |
child 11090 | 3041d0347d26 |
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 |
||
10980 | 16 |
theory Transitive_Closure = Lfp + Relation |
17 |
files ("Transitive_Closure_lemmas.ML"): |
|
10213 | 18 |
|
19 |
constdefs |
|
10331 | 20 |
rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_^*)" [1000] 999) |
21 |
"r^* == lfp (%s. Id Un (r O s))" |
|
10213 | 22 |
|
10331 | 23 |
trancl :: "('a * 'a) set => ('a * 'a) set" ("(_^+)" [1000] 999) |
24 |
"r^+ == r O rtrancl r" |
|
10213 | 25 |
|
26 |
syntax |
|
10331 | 27 |
"_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_^=)" [1000] 999) |
10213 | 28 |
translations |
29 |
"r^=" == "r Un Id" |
|
30 |
||
10827 | 31 |
syntax (xsymbols) |
10331 | 32 |
rtrancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>*)" [1000] 999) |
33 |
trancl :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>+)" [1000] 999) |
|
34 |
"_reflcl" :: "('a * 'a) set => ('a * 'a) set" ("(_\\<^sup>=)" [1000] 999) |
|
35 |
||
10980 | 36 |
use "Transitive_Closure_lemmas.ML" |
37 |
||
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
38 |
|
11084 | 39 |
lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*" |
40 |
apply safe |
|
41 |
apply (erule trancl_into_rtrancl) |
|
42 |
apply (blast elim: rtranclE dest: rtrancl_into_trancl1) |
|
43 |
done |
|
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
44 |
|
11084 | 45 |
lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" |
46 |
apply safe |
|
47 |
apply (drule trancl_into_rtrancl) |
|
48 |
apply simp |
|
49 |
apply (erule rtranclE) |
|
50 |
apply safe |
|
51 |
apply (rule r_into_trancl) |
|
52 |
apply simp |
|
53 |
apply (rule rtrancl_into_trancl1) |
|
54 |
apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD]) |
|
55 |
apply fast |
|
56 |
done |
|
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
57 |
|
11084 | 58 |
lemma trancl_empty [simp]: "{}\<^sup>+ = {}" |
59 |
by (auto elim: trancl_induct) |
|
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
60 |
|
11084 | 61 |
lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" |
62 |
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
|
63 |
|
11084 | 64 |
lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+" |
65 |
by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl) |
|
66 |
||
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
67 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
68 |
(* 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
|
69 |
|
11084 | 70 |
lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" |
71 |
by blast |
|
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
72 |
|
11084 | 73 |
lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" |
74 |
by blast |
|
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
75 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
76 |
lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*" |
11084 | 77 |
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
|
78 |
|
11084 | 79 |
lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*" |
80 |
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
|
81 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
82 |
lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" |
11084 | 83 |
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
|
84 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
85 |
lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" |
11084 | 86 |
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
|
87 |
|
10213 | 88 |
end |