author | oheimb |
Thu, 01 Feb 2001 20:51:48 +0100 | |
changeset 11025 | a70b796d9af8 |
parent 10996 | 74e970389def |
child 11084 | 32c1deea5bcd |
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 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
39 |
lemma reflcl_trancl[simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
40 |
apply safe; |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
41 |
apply (erule trancl_into_rtrancl); |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
42 |
by (blast elim:rtranclE dest:rtrancl_into_trancl1) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
43 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
44 |
lemma trancl_reflcl[simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
45 |
apply safe |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
46 |
apply (drule trancl_into_rtrancl) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
47 |
apply simp; |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
48 |
apply (erule rtranclE) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
49 |
apply safe |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
50 |
apply(rule r_into_trancl) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
51 |
apply simp |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
52 |
apply(rule rtrancl_into_trancl1) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
53 |
apply(erule rtrancl_reflcl[THEN equalityD2, THEN subsetD]) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
54 |
apply fast |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
55 |
done |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
56 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
57 |
lemma trancl_empty[simp]: "{}\<^sup>+ = {}" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
58 |
by (auto elim:trancl_induct) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
59 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
60 |
lemma rtrancl_empty[simp]: "{}\<^sup>* = Id" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
61 |
by(rule subst[OF reflcl_trancl], simp) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
62 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
63 |
lemma rtranclD: "(a,b) \<in> R\<^sup>* \<Longrightarrow> a=b \<or> a\<noteq>b \<and> (a,b) \<in> R\<^sup>+" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
64 |
by(force simp add: reflcl_trancl[THEN sym] simp del: reflcl_trancl) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
65 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
66 |
(* 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
|
67 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
68 |
lemma Domain_rtrancl[simp]: "Domain(R\<^sup>*) = UNIV" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
69 |
by blast |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
70 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
71 |
lemma Range_rtrancl[simp]: "Range(R\<^sup>*) = UNIV" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
72 |
by blast |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
73 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
74 |
lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
75 |
by(rule rtrancl_Un_rtrancl[THEN subst], fast) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
76 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
77 |
lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
78 |
by (blast intro: subsetD[OF rtrancl_Un_subset]) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
79 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
80 |
lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
81 |
by (unfold Domain_def, blast dest:tranclD) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
82 |
|
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
83 |
lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
84 |
by (simp add:Range_def trancl_converse[THEN sym]) |
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset
|
85 |
|
10213 | 86 |
end |