author  berghofe 
Wed, 11 Jul 2007 11:10:37 +0200  
changeset 23743  52fbc991039f 
parent 22422  ee19cdb07528 
child 25295  12985023be5e 
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 

12691  7 
header {* Reflexive and Transitive closure of a relation *} 
8 

15131  9 
theory Transitive_Closure 
22262  10 
imports Predicate 
21589  11 
uses "~~/src/Provers/trancl.ML" 
15131  12 
begin 
12691  13 

14 
text {* 

15 
@{text rtrancl} is reflexive/transitive closure, 

16 
@{text trancl} is transitive closure, 

17 
@{text reflcl} is reflexive closure. 

18 

19 
These postfix operators have \emph{maximum priority}, forcing their 

20 
operands to be atomic. 

21 
*} 

10213  22 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

23 
inductive_set 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

24 
rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_^*)" [1000] 999) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

25 
for r :: "('a \<times> 'a) set" 
22262  26 
where 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

27 
rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

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

29 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

30 
inductive_set 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

31 
trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" ("(_^+)" [1000] 999) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

32 
for r :: "('a \<times> 'a) set" 
22262  33 
where 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

34 
r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

35 
 trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+" 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

36 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

37 
notation 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

38 
rtranclp ("(_^**)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

39 
tranclp ("(_^++)" [1000] 1000) 
10213  40 

19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19623
diff
changeset

41 
abbreviation 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

42 
reflclp :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where 
22422
ee19cdb07528
stepping towards uniform lattice theory development in HOL
haftmann
parents:
22262
diff
changeset

43 
"r^== == sup r op =" 
22262  44 

45 
abbreviation 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

46 
reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where 
19656
09be06943252
tuned concrete syntax  abbreviation/const_syntax;
wenzelm
parents:
19623
diff
changeset

47 
"r^= == r \<union> Id" 
10213  48 

21210  49 
notation (xsymbols) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

50 
rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

51 
tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

52 
reflclp ("(_\<^sup>=\<^sup>=)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

53 
rtrancl ("(_\<^sup>*)" [1000] 999) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

54 
trancl ("(_\<^sup>+)" [1000] 999) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

55 
reflcl ("(_\<^sup>=)" [1000] 999) 
12691  56 

21210  57 
notation (HTML output) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

58 
rtranclp ("(_\<^sup>*\<^sup>*)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

59 
tranclp ("(_\<^sup>+\<^sup>+)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

60 
reflclp ("(_\<^sup>=\<^sup>=)" [1000] 1000) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

61 
rtrancl ("(_\<^sup>*)" [1000] 999) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

62 
trancl ("(_\<^sup>+)" [1000] 999) and 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

63 
reflcl ("(_\<^sup>=)" [1000] 999) 
14565  64 

12691  65 

66 
subsection {* Reflexivetransitive closure *} 

67 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

68 
lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r Un Id)" 
22262  69 
by (simp add: expand_fun_eq) 
70 

12691  71 
lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" 
72 
 {* @{text rtrancl} of @{text r} contains @{text r} *} 

73 
apply (simp only: split_tupled_all) 

74 
apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) 

75 
done 

76 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

77 
lemma r_into_rtranclp [intro]: "r x y ==> r^** x y" 
22262  78 
 {* @{text rtrancl} of @{text r} contains @{text r} *} 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

79 
by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) 
22262  80 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

81 
lemma rtranclp_mono: "r \<le> s ==> r^** \<le> s^**" 
12691  82 
 {* monotonicity of @{text rtrancl} *} 
22262  83 
apply (rule predicate2I) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

84 
apply (erule rtranclp.induct) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

85 
apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) 
12691  86 
done 
87 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

88 
lemmas rtrancl_mono = rtranclp_mono [to_set] 
22262  89 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

90 
theorem rtranclp_induct [consumes 1, induct set: rtranclp]: 
22262  91 
assumes a: "r^** a b" 
92 
and cases: "P a" "!!y z. [ r^** a y; r y z; P y ] ==> P z" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12823
diff
changeset

93 
shows "P b" 
12691  94 
proof  
95 
from a have "a = a > P b" 

17589  96 
by (induct "%x y. x = a > P y" a b) (iprover intro: cases)+ 
97 
thus ?thesis by iprover 

12691  98 
qed 
99 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

100 
lemmas rtrancl_induct [consumes 1, induct set: rtrancl] = rtranclp_induct [to_set] 
22262  101 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

102 
lemmas rtranclp_induct2 = 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

103 
rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, 
22262  104 
consumes 1, case_names refl step] 
105 

14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

106 
lemmas rtrancl_induct2 = 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

107 
rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

108 
consumes 1, case_names refl step] 
18372  109 

19228  110 
lemma reflexive_rtrancl: "reflexive (r^*)" 
111 
by (unfold refl_def) fast 

112 

12691  113 
lemma trans_rtrancl: "trans(r^*)" 
114 
 {* transitivity of transitive closure!!  by induction *} 

12823  115 
proof (rule transI) 
116 
fix x y z 

117 
assume "(x, y) \<in> r\<^sup>*" 

118 
assume "(y, z) \<in> r\<^sup>*" 

17589  119 
thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+ 
12823  120 
qed 
12691  121 

122 
lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard] 

123 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

124 
lemma rtranclp_trans: 
22262  125 
assumes xy: "r^** x y" 
126 
and yz: "r^** y z" 

127 
shows "r^** x z" using yz xy 

128 
by induct iprover+ 

129 

12691  130 
lemma rtranclE: 
18372  131 
assumes major: "(a::'a,b) : r^*" 
132 
and cases: "(a = b) ==> P" 

133 
"!!y. [ (a,y) : r^*; (y,b) : r ] ==> P" 

134 
shows P 

12691  135 
 {* elimination of @{text rtrancl}  by induction on a special formula *} 
18372  136 
apply (subgoal_tac "(a::'a) = b  (EX y. (a,y) : r^* & (y,b) : r)") 
137 
apply (rule_tac [2] major [THEN rtrancl_induct]) 

138 
prefer 2 apply blast 

139 
prefer 2 apply blast 

140 
apply (erule asm_rl exE disjE conjE cases)+ 

141 
done 

12691  142 

22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

143 
lemma rtrancl_Int_subset: "[ Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s] ==> r^* \<subseteq> s" 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

144 
apply (rule subsetI) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

145 
apply (rule_tac p="x" in PairE, clarify) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

146 
apply (erule rtrancl_induct, auto) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

147 
done 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

148 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

149 
lemma converse_rtranclp_into_rtranclp: 
22262  150 
"r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

151 
by (rule rtranclp_trans) iprover+ 
22262  152 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

153 
lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] 
12691  154 

155 
text {* 

156 
\medskip More @{term "r^*"} equations and inclusions. 

157 
*} 

158 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

159 
lemma rtranclp_idemp [simp]: "(r^**)^** = r^**" 
22262  160 
apply (auto intro!: order_antisym) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

161 
apply (erule rtranclp_induct) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

162 
apply (rule rtranclp.rtrancl_refl) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

163 
apply (blast intro: rtranclp_trans) 
12691  164 
done 
165 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

166 
lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] 
22262  167 

12691  168 
lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" 
169 
apply (rule set_ext) 

170 
apply (simp only: split_tupled_all) 

171 
apply (blast intro: rtrancl_trans) 

172 
done 

173 

174 
lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" 

14208  175 
by (drule rtrancl_mono, simp) 
12691  176 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

177 
lemma rtranclp_subset: "R \<le> S ==> S \<le> R^** ==> S^** = R^**" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

178 
apply (drule rtranclp_mono) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

179 
apply (drule rtranclp_mono, simp) 
12691  180 
done 
181 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

182 
lemmas rtrancl_subset = rtranclp_subset [to_set] 
22262  183 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

184 
lemma rtranclp_sup_rtranclp: "(sup (R^**) (S^**))^** = (sup R S)^**" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

185 
by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) 
12691  186 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

187 
lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] 
22262  188 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

189 
lemma rtranclp_reflcl [simp]: "(R^==)^** = R^**" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

190 
by (blast intro!: rtranclp_subset) 
22262  191 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

192 
lemmas rtrancl_reflcl [simp] = rtranclp_reflcl [to_set] 
12691  193 

194 
lemma rtrancl_r_diff_Id: "(r  Id)^* = r^*" 

195 
apply (rule sym) 

14208  196 
apply (rule rtrancl_subset, blast, clarify) 
12691  197 
apply (rename_tac a b) 
14208  198 
apply (case_tac "a = b", blast) 
12691  199 
apply (blast intro!: r_into_rtrancl) 
200 
done 

201 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

202 
lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**" 
22262  203 
apply (rule sym) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

204 
apply (rule rtranclp_subset) 
22262  205 
apply blast+ 
206 
done 

207 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

208 
theorem rtranclp_converseD: 
22262  209 
assumes r: "(r^1)^** x y" 
210 
shows "r^** y x" 

12823  211 
proof  
212 
from r show ?thesis 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

213 
by induct (iprover intro: rtranclp_trans dest!: conversepD)+ 
12823  214 
qed 
12691  215 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

216 
lemmas rtrancl_converseD = rtranclp_converseD [to_set] 
22262  217 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

218 
theorem rtranclp_converseI: 
22262  219 
assumes r: "r^** y x" 
220 
shows "(r^1)^** x y" 

12823  221 
proof  
222 
from r show ?thesis 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

223 
by induct (iprover intro: rtranclp_trans conversepI)+ 
12823  224 
qed 
12691  225 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

226 
lemmas rtrancl_converseI = rtranclp_converseI [to_set] 
22262  227 

12691  228 
lemma rtrancl_converse: "(r^1)^* = (r^*)^1" 
229 
by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) 

230 

19228  231 
lemma sym_rtrancl: "sym r ==> sym (r^*)" 
232 
by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) 

233 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

234 
theorem converse_rtranclp_induct[consumes 1]: 
22262  235 
assumes major: "r^** a b" 
236 
and cases: "P b" "!!y z. [ r y z; r^** z b; P z ] ==> P y" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12823
diff
changeset

237 
shows "P a" 
12691  238 
proof  
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

239 
from rtranclp_converseI [OF major] 
12691  240 
show ?thesis 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

241 
by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ 
12691  242 
qed 
243 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

244 
lemmas converse_rtrancl_induct[consumes 1] = converse_rtranclp_induct [to_set] 
22262  245 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

246 
lemmas converse_rtranclp_induct2 = 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

247 
converse_rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, 
22262  248 
consumes 1, case_names refl step] 
249 

14404
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

250 
lemmas converse_rtrancl_induct2 = 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

251 
converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 
4952c5a92e04
Transitive_Closure: added consumes and case_names attributes
nipkow
parents:
14398
diff
changeset

252 
consumes 1, case_names refl step] 
12691  253 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

254 
lemma converse_rtranclpE: 
22262  255 
assumes major: "r^** x z" 
18372  256 
and cases: "x=z ==> P" 
22262  257 
"!!y. [ r x y; r^** y z ] ==> P" 
18372  258 
shows P 
22262  259 
apply (subgoal_tac "x = z  (EX y. r x y & r^** y z)") 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

260 
apply (rule_tac [2] major [THEN converse_rtranclp_induct]) 
18372  261 
prefer 2 apply iprover 
262 
prefer 2 apply iprover 

263 
apply (erule asm_rl exE disjE conjE cases)+ 

264 
done 

12691  265 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

266 
lemmas converse_rtranclE = converse_rtranclpE [to_set] 
22262  267 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

268 
lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] 
22262  269 

270 
lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] 

12691  271 

272 
lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" 

273 
by (blast elim: rtranclE converse_rtranclE 

274 
intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) 

275 

20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
19656
diff
changeset

276 
lemma rtrancl_unfold: "r^* = Id Un r O r^*" 
15551  277 
by (auto intro: rtrancl_into_rtrancl elim: rtranclE) 
278 

12691  279 

280 
subsection {* Transitive closure *} 

10331  281 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

282 
lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

283 
apply (simp add: split_tupled_all) 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

284 
apply (erule trancl.induct) 
17589  285 
apply (iprover dest: subsetD)+ 
12691  286 
done 
287 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

288 
lemma r_into_trancl': "!!p. p : r ==> p : r^+" 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

289 
by (simp only: split_tupled_all) (erule r_into_trancl) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

290 

12691  291 
text {* 
292 
\medskip Conversions between @{text trancl} and @{text rtrancl}. 

293 
*} 

294 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

295 
lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

296 
by (erule tranclp.induct) iprover+ 
12691  297 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

298 
lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] 
22262  299 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

300 
lemma rtranclp_into_tranclp1: assumes r: "r^** a b" 
22262  301 
shows "!!c. r b c ==> r^++ a c" using r 
17589  302 
by induct iprover+ 
12691  303 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

304 
lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] 
22262  305 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

306 
lemma rtranclp_into_tranclp2: "[ r a b; r^** b c ] ==> r^++ a c" 
12691  307 
 {* intro rule from @{text r} and @{text rtrancl} *} 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

308 
apply (erule rtranclp.cases, iprover) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

309 
apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

310 
apply (simp  rule r_into_rtranclp)+ 
12691  311 
done 
312 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

313 
lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] 
22262  314 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

315 
lemma tranclp_induct [consumes 1, induct set: tranclp]: 
22262  316 
assumes a: "r^++ a b" 
317 
and cases: "!!y. r a y ==> P y" 

318 
"!!y z. r^++ a y ==> r y z ==> P y ==> P z" 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

319 
shows "P b" 
12691  320 
 {* Nice induction rule for @{text trancl} *} 
321 
proof  

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

322 
from a have "a = a > P b" 
17589  323 
by (induct "%x y. x = a > P y" a b) (iprover intro: cases)+ 
324 
thus ?thesis by iprover 

12691  325 
qed 
326 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

327 
lemmas trancl_induct [consumes 1, induct set: trancl] = tranclp_induct [to_set] 
22262  328 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

329 
lemmas tranclp_induct2 = 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

330 
tranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, 
22262  331 
consumes 1, case_names base step] 
332 

22172  333 
lemmas trancl_induct2 = 
334 
trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), 

335 
consumes 1, case_names base step] 

336 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

337 
lemma tranclp_trans_induct: 
22262  338 
assumes major: "r^++ x y" 
339 
and cases: "!!x y. r x y ==> P x y" 

340 
"!!x y z. [ r^++ x y; P x y; r^++ y z; P y z ] ==> P x z" 

18372  341 
shows "P x y" 
12691  342 
 {* Another induction rule for trancl, incorporating transitivity *} 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

343 
by (iprover intro: major [THEN tranclp_induct] cases) 
12691  344 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

345 
lemmas trancl_trans_induct = tranclp_trans_induct [to_set] 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

346 

52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

347 
inductive_cases tranclE: "(a, b) : r^+" 
10980  348 

22080
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

349 
lemma trancl_Int_subset: "[ r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s] ==> r^+ \<subseteq> s" 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

350 
apply (rule subsetI) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

351 
apply (rule_tac p="x" in PairE, clarify) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

352 
apply (erule trancl_induct, auto) 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

353 
done 
7bf8868ab3e4
induction rules for trancl/rtrancl expressed using subsets
paulson
parents:
21589
diff
changeset

354 

20716
a6686a8e1b68
Changed precedence of "op O" (relation composition) from 60 to 75.
krauss
parents:
19656
diff
changeset

355 
lemma trancl_unfold: "r^+ = r Un r O r^+" 
15551  356 
by (auto intro: trancl_into_trancl elim: tranclE) 
357 

19623  358 
lemma trans_trancl[simp]: "trans(r^+)" 
12691  359 
 {* Transitivity of @{term "r^+"} *} 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

360 
proof (rule transI) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

361 
fix x y z 
18372  362 
assume xy: "(x, y) \<in> r^+" 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

363 
assume "(y, z) \<in> r^+" 
18372  364 
thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+ 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

365 
qed 
12691  366 

367 
lemmas trancl_trans = trans_trancl [THEN transD, standard] 

368 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

369 
lemma tranclp_trans: 
22262  370 
assumes xy: "r^++ x y" 
371 
and yz: "r^++ y z" 

372 
shows "r^++ x z" using yz xy 

373 
by induct iprover+ 

374 

19623  375 
lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r" 
376 
apply(auto) 

377 
apply(erule trancl_induct) 

378 
apply assumption 

379 
apply(unfold trans_def) 

380 
apply(blast) 

381 
done 

382 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

383 
lemma rtranclp_tranclp_tranclp: assumes r: "r^** x y" 
22262  384 
shows "!!z. r^++ y z ==> r^++ x z" using r 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

385 
by induct (iprover intro: tranclp_trans)+ 
12691  386 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

387 
lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] 
22262  388 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

389 
lemma tranclp_into_tranclp2: "r a b ==> r^++ b c ==> r^++ a c" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

390 
by (erule tranclp_trans [OF tranclp.r_into_trancl]) 
22262  391 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

392 
lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] 
12691  393 

394 
lemma trancl_insert: 

395 
"(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" 

396 
 {* primitive recursion for @{text trancl} over finite relations *} 

397 
apply (rule equalityI) 

398 
apply (rule subsetI) 

399 
apply (simp only: split_tupled_all) 

14208  400 
apply (erule trancl_induct, blast) 
12691  401 
apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans) 
402 
apply (rule subsetI) 

403 
apply (blast intro: trancl_mono rtrancl_mono 

404 
[THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) 

405 
done 

406 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

407 
lemma tranclp_converseI: "(r^++)^1 x y ==> (r^1)^++ x y" 
22262  408 
apply (drule conversepD) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

409 
apply (erule tranclp_induct) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

410 
apply (iprover intro: conversepI tranclp_trans)+ 
12691  411 
done 
412 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

413 
lemmas trancl_converseI = tranclp_converseI [to_set] 
22262  414 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

415 
lemma tranclp_converseD: "(r^1)^++ x y ==> (r^++)^1 x y" 
22262  416 
apply (rule conversepI) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

417 
apply (erule tranclp_induct) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

418 
apply (iprover dest: conversepD intro: tranclp_trans)+ 
13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

419 
done 
12691  420 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

421 
lemmas trancl_converseD = tranclp_converseD [to_set] 
22262  422 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

423 
lemma tranclp_converse: "(r^1)^++ = (r^++)^1" 
22262  424 
by (fastsimp simp add: expand_fun_eq 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

425 
intro!: tranclp_converseI dest!: tranclp_converseD) 
22262  426 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

427 
lemmas trancl_converse = tranclp_converse [to_set] 
12691  428 

19228  429 
lemma sym_trancl: "sym r ==> sym (r^+)" 
430 
by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) 

431 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

432 
lemma converse_tranclp_induct: 
22262  433 
assumes major: "r^++ a b" 
434 
and cases: "!!y. r y b ==> P(y)" 

435 
"!!y z.[ r y z; r^++ z b; P(z) ] ==> P(y)" 

18372  436 
shows "P a" 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

437 
apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) 
18372  438 
apply (rule cases) 
22262  439 
apply (erule conversepD) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

440 
apply (blast intro: prems dest!: tranclp_converseD conversepD) 
18372  441 
done 
12691  442 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

443 
lemmas converse_trancl_induct = converse_tranclp_induct [to_set] 
22262  444 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

445 
lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

446 
apply (erule converse_tranclp_induct, auto) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

447 
apply (blast intro: rtranclp_trans) 
12691  448 
done 
449 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

450 
lemmas tranclD = tranclpD [to_set] 
22262  451 

13867  452 
lemma irrefl_tranclI: "r^1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" 
18372  453 
by (blast elim: tranclE dest: trancl_into_rtrancl) 
12691  454 

455 
lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y" 

456 
by (blast dest: r_into_trancl) 

457 

458 
lemma trancl_subset_Sigma_aux: 

459 
"(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A" 

18372  460 
by (induct rule: rtrancl_induct) auto 
12691  461 

462 
lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A" 

13704
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

463 
apply (rule subsetI) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

464 
apply (simp only: split_tupled_all) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

465 
apply (erule tranclE) 
854501b1e957
Transitive closure is now defined inductively as well.
berghofe
parents:
12937
diff
changeset

466 
apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ 
12691  467 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

468 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

469 
lemma reflcl_tranclp [simp]: "(r^++)^== = r^**" 
22262  470 
apply (safe intro!: order_antisym) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

471 
apply (erule tranclp_into_rtranclp) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

472 
apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) 
11084  473 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

474 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

475 
lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set] 
22262  476 

11090  477 
lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" 
11084  478 
apply safe 
14208  479 
apply (drule trancl_into_rtrancl, simp) 
480 
apply (erule rtranclE, safe) 

481 
apply (rule r_into_trancl, simp) 

11084  482 
apply (rule rtrancl_into_trancl1) 
14208  483 
apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) 
11084  484 
done 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

485 

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

488 

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

491 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

492 
lemma rtranclpD: "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b" 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

493 
by (force simp add: reflcl_tranclp [symmetric] simp del: reflcl_tranclp) 
22262  494 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

495 
lemmas rtranclD = rtranclpD [to_set] 
11084  496 

16514  497 
lemma rtrancl_eq_or_trancl: 
498 
"(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)" 

499 
by (fast elim: trancl_into_rtrancl dest: rtranclD) 

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

500 

12691  501 
text {* @{text Domain} and @{text Range} *} 
10996
74e970389def
Moved some thms from Transitive_ClosureTr.ML to Transitive_Closure.thy
nipkow
parents:
10980
diff
changeset

502 

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

505 

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

508 

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

511 

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

514 

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

517 

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

520 

11115  521 
lemma Not_Domain_rtrancl: 
12691  522 
"x ~: Domain R ==> ((x, y) : R^*) = (x = y)" 
523 
apply auto 

524 
by (erule rev_mp, erule rtrancl_induct, auto) 

525 

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

526 

12691  527 
text {* More about converse @{text rtrancl} and @{text trancl}, should 
528 
be merged with main body. *} 

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

529 

14337
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

530 
lemma single_valued_confluent: 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

531 
"\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk> 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

532 
\<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*" 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

533 
apply(erule rtrancl_induct) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

534 
apply simp 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

535 
apply(erule disjE) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

536 
apply(blast elim:converse_rtranclE dest:single_valuedD) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

537 
apply(blast intro:rtrancl_trans) 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

538 
done 
e13731554e50
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
nipkow
parents:
14208
diff
changeset

539 

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

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

542 

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

543 
lemma trancl_into_trancl [rule_format]: 
12691  544 
"(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r > (a,c) \<in> r\<^sup>+" 
545 
apply (erule trancl_induct) 

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

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

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

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

549 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

550 
lemma tranclp_rtranclp_tranclp: 
22262  551 
"r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c" 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

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

553 
apply (erule exE, erule conjE) 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

554 
apply (drule rtranclp_trans, assumption) 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

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

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

557 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

558 
lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set] 
22262  559 

12691  560 
lemmas transitive_closure_trans [trans] = 
561 
r_r_into_trancl trancl_trans rtrancl_trans 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

562 
trancl.trancl_into_trancl trancl_into_trancl2 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

563 
rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl 
12691  564 
rtrancl_trancl_trancl trancl_rtrancl_trancl 
12428
f3033eed309a
setup [trans] rules for calculational Isar reasoning
kleing
parents:
11327
diff
changeset

565 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

566 
lemmas transitive_closurep_trans' [trans] = 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

567 
tranclp_trans rtranclp_trans 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

568 
tranclp.trancl_into_trancl tranclp_into_tranclp2 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

569 
rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

570 
rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp 
22262  571 

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

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

573 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

574 
declare rtranclE [cases set: rtrancl] 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

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

576 

15551  577 

578 

579 

580 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

581 
subsection {* Setup of transitivity reasoner *} 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

582 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

583 
ML_setup {* 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

584 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

585 
structure Trancl_Tac = Trancl_Tac_Fun ( 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

586 
struct 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

587 
val r_into_trancl = thm "trancl.r_into_trancl"; 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

588 
val trancl_trans = thm "trancl_trans"; 
23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

589 
val rtrancl_refl = thm "rtrancl.rtrancl_refl"; 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

590 
val r_into_rtrancl = thm "r_into_rtrancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

591 
val trancl_into_rtrancl = thm "trancl_into_rtrancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

592 
val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

593 
val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl"; 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

594 
val rtrancl_trans = thm "rtrancl_trans"; 
15096  595 

18372  596 
fun decomp (Trueprop $ t) = 
597 
let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

598 
let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

599 
 decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") 
18372  600 
 decr r = (r,"r"); 
601 
val (rel,r) = decr rel; 

602 
in SOME (a,b,rel,r) end 

603 
 dec _ = NONE 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

604 
in dec t end; 
18372  605 

21589  606 
end); 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

607 

22262  608 
structure Tranclp_Tac = Trancl_Tac_Fun ( 
609 
struct 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

610 
val r_into_trancl = thm "tranclp.r_into_trancl"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

611 
val trancl_trans = thm "tranclp_trans"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

612 
val rtrancl_refl = thm "rtranclp.rtrancl_refl"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

613 
val r_into_rtrancl = thm "r_into_rtranclp"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

614 
val trancl_into_rtrancl = thm "tranclp_into_rtranclp"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

615 
val rtrancl_trancl_trancl = thm "rtranclp_tranclp_tranclp"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

616 
val trancl_rtrancl_trancl = thm "tranclp_rtranclp_tranclp"; 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

617 
val rtrancl_trans = thm "rtranclp_trans"; 
22262  618 

619 
fun decomp (Trueprop $ t) = 

620 
let fun dec (rel $ a $ b) = 

23743
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

621 
let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*") 
52fbc991039f
rtrancl and trancl are now defined using inductive_set.
berghofe
parents:
22422
diff
changeset

622 
 decr (Const ("Transitive_Closure.tranclp", _ ) $ r) = (r,"r+") 
22262  623 
 decr r = (r,"r"); 
624 
val (rel,r) = decr rel; 

625 
in SOME (a, b, Envir.beta_eta_contract rel, r) end 

626 
 dec _ = NONE 

627 
in dec t end; 

628 

629 
end); 

630 

17876  631 
change_simpset (fn ss => ss 
632 
addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) 

22262  633 
addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)) 
634 
addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac)) 

635 
addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac))); 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

636 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

637 
*} 
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

638 

21589  639 
(* Optional methods *) 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

640 

4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

641 
method_setup trancl = 
21589  642 
{* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} 
18372  643 
{* simple transitivity reasoner *} 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

644 
method_setup rtrancl = 
21589  645 
{* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} 
15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

646 
{* simple transitivity reasoner *} 
22262  647 
method_setup tranclp = 
648 
{* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} 

649 
{* simple transitivity reasoner (predicate version) *} 

650 
method_setup rtranclp = 

651 
{* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} 

652 
{* simple transitivity reasoner (predicate version) *} 

15076
4b3d280ef06a
New prover for transitive and reflexivetransitive closure of relations.
ballarin
parents:
14565
diff
changeset

653 

10213  654 
end 