author  paulson 
Wed, 14 Feb 2001 12:16:32 +0100  
changeset 11115  285b31e9e026 
parent 11090  3041d0347d26 
child 11327  cd2c27a23df1 
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 

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 

11090  39 
lemma reflcl_trancl [simp]: "(r^+)^= = r^*" 
11084  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 

11090  45 
lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" 
11084  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 

11090  58 
lemma trancl_empty [simp]: "{}^+ = {}" 
11084  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 

11090  61 
lemma rtrancl_empty [simp]: "{}^* = Id" 
11084  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 

11090  64 
lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+" 
11084  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 

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

72 

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

75 

11090  76 
lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*" 
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 

11090  79 
lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*" 
11084  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 

11090  82 
lemma trancl_domain [simp]: "Domain (r^+) = 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 

11090  85 
lemma trancl_range [simp]: "Range (r^+) = 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 

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

90 
apply (auto) 

91 
by (erule rev_mp, erule rtrancl_induct, auto) 

92 

10213  93 
end 