63 reflclp ("(_^==)" [1000] 1000) |
63 reflclp ("(_^==)" [1000] 1000) |
64 |
64 |
65 |
65 |
66 subsection \<open>Reflexive closure\<close> |
66 subsection \<open>Reflexive closure\<close> |
67 |
67 |
68 lemma refl_reflcl[simp]: "refl(r^=)" |
68 lemma refl_reflcl[simp]: "refl (r\<^sup>=)" |
69 by(simp add:refl_on_def) |
69 by (simp add: refl_on_def) |
70 |
70 |
71 lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r" |
71 lemma antisym_reflcl[simp]: "antisym (r\<^sup>=) = antisym r" |
72 by(simp add:antisym_def) |
72 by (simp add: antisym_def) |
73 |
73 |
74 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)" |
74 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans (r\<^sup>=)" |
75 unfolding trans_def by blast |
75 unfolding trans_def by blast |
76 |
76 |
77 lemma reflclp_idemp [simp]: "(P^==)^== = P^==" |
77 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>=" |
78 by blast |
78 by blast |
|
79 |
79 |
80 |
80 subsection \<open>Reflexive-transitive closure\<close> |
81 subsection \<open>Reflexive-transitive closure\<close> |
81 |
82 |
82 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
83 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)" |
83 by (auto simp add: fun_eq_iff) |
84 by (auto simp add: fun_eq_iff) |
84 |
85 |
85 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
86 lemma r_into_rtrancl [intro]: "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>*" |
86 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
87 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
87 apply (simp only: split_tupled_all) |
88 apply (simp only: split_tupled_all) |
88 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
89 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
89 done |
90 done |
90 |
91 |
91 lemma r_into_rtranclp [intro]: "r x y ==> r^** x y" |
92 lemma r_into_rtranclp [intro]: "r x y \<Longrightarrow> r\<^sup>*\<^sup>* x y" |
92 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
93 \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close> |
93 by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) |
94 by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl]) |
94 |
95 |
95 lemma rtranclp_mono: "r \<le> s ==> r^** \<le> s^**" |
96 lemma rtranclp_mono: "r \<le> s \<Longrightarrow> r\<^sup>*\<^sup>* \<le> s\<^sup>*\<^sup>*" |
96 \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close> |
97 \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close> |
97 apply (rule predicate2I) |
98 apply (rule predicate2I) |
98 apply (erule rtranclp.induct) |
99 apply (erule rtranclp.induct) |
99 apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) |
100 apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+) |
100 done |
101 done |
101 |
102 |
102 lemma mono_rtranclp[mono]: |
103 lemma mono_rtranclp[mono]: "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x\<^sup>*\<^sup>* a b \<longrightarrow> y\<^sup>*\<^sup>* a b" |
103 "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x^** a b \<longrightarrow> y^** a b" |
|
104 using rtranclp_mono[of x y] by auto |
104 using rtranclp_mono[of x y] by auto |
105 |
105 |
106 lemmas rtrancl_mono = rtranclp_mono [to_set] |
106 lemmas rtrancl_mono = rtranclp_mono [to_set] |
107 |
107 |
108 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: |
108 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]: |
109 assumes a: "r^** a b" |
109 assumes a: "r\<^sup>*\<^sup>* a b" |
110 and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z" |
110 and cases: "P a" "\<And>y z. r\<^sup>*\<^sup>* a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" |
111 shows "P b" using a |
111 shows "P b" |
112 by (induct x\<equiv>a b) (rule cases)+ |
112 using a by (induct x\<equiv>a b) (rule cases)+ |
113 |
113 |
114 lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] |
114 lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set] |
115 |
115 |
116 lemmas rtranclp_induct2 = |
116 lemmas rtranclp_induct2 = |
117 rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, |
117 rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] |
118 consumes 1, case_names refl step] |
|
119 |
118 |
120 lemmas rtrancl_induct2 = |
119 lemmas rtrancl_induct2 = |
121 rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
120 rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), consumes 1, case_names refl step] |
122 consumes 1, case_names refl step] |
121 |
123 |
122 lemma refl_rtrancl: "refl (r\<^sup>*)" |
124 lemma refl_rtrancl: "refl (r^*)" |
123 unfolding refl_on_def by fast |
125 by (unfold refl_on_def) fast |
|
126 |
124 |
127 text \<open>Transitivity of transitive closure.\<close> |
125 text \<open>Transitivity of transitive closure.\<close> |
128 lemma trans_rtrancl: "trans (r^*)" |
126 lemma trans_rtrancl: "trans (r\<^sup>*)" |
129 proof (rule transI) |
127 proof (rule transI) |
130 fix x y z |
128 fix x y z |
131 assume "(x, y) \<in> r\<^sup>*" |
129 assume "(x, y) \<in> r\<^sup>*" |
132 assume "(y, z) \<in> r\<^sup>*" |
130 assume "(y, z) \<in> r\<^sup>*" |
133 then show "(x, z) \<in> r\<^sup>*" |
131 then show "(x, z) \<in> r\<^sup>*" |
142 qed |
140 qed |
143 |
141 |
144 lemmas rtrancl_trans = trans_rtrancl [THEN transD] |
142 lemmas rtrancl_trans = trans_rtrancl [THEN transD] |
145 |
143 |
146 lemma rtranclp_trans: |
144 lemma rtranclp_trans: |
147 assumes xy: "r^** x y" |
145 assumes "r\<^sup>*\<^sup>* x y" |
148 and yz: "r^** y z" |
146 and "r\<^sup>*\<^sup>* y z" |
149 shows "r^** x z" using yz xy |
147 shows "r\<^sup>*\<^sup>* x z" |
150 by induct iprover+ |
148 using assms(2,1) by induct iprover+ |
151 |
149 |
152 lemma rtranclE [cases set: rtrancl]: |
150 lemma rtranclE [cases set: rtrancl]: |
153 assumes major: "(a::'a, b) : r^*" |
151 fixes a b :: 'a |
|
152 assumes major: "(a, b) \<in> r\<^sup>*" |
154 obtains |
153 obtains |
155 (base) "a = b" |
154 (base) "a = b" |
156 | (step) y where "(a, y) : r^*" and "(y, b) : r" |
155 | (step) y where "(a, y) \<in> r\<^sup>*" and "(y, b) \<in> r" |
157 \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close> |
156 \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close> |
158 apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)") |
157 apply (subgoal_tac "a = b \<or> (\<exists>y. (a, y) \<in> r\<^sup>* \<and> (y, b) \<in> r)") |
159 apply (rule_tac [2] major [THEN rtrancl_induct]) |
158 apply (rule_tac [2] major [THEN rtrancl_induct]) |
160 prefer 2 apply blast |
159 prefer 2 apply blast |
161 prefer 2 apply blast |
160 prefer 2 apply blast |
162 apply (erule asm_rl exE disjE conjE base step)+ |
161 apply (erule asm_rl exE disjE conjE base step)+ |
163 done |
162 done |
164 |
163 |
165 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s" |
164 lemma rtrancl_Int_subset: "Id \<subseteq> s \<Longrightarrow> (r\<^sup>* \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>* \<subseteq> s" |
166 apply (rule subsetI) |
165 apply (rule subsetI) |
167 apply auto |
166 apply auto |
168 apply (erule rtrancl_induct) |
167 apply (erule rtrancl_induct) |
169 apply auto |
168 apply auto |
170 done |
169 done |
171 |
170 |
172 lemma converse_rtranclp_into_rtranclp: |
171 lemma converse_rtranclp_into_rtranclp: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
173 "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
|
174 by (rule rtranclp_trans) iprover+ |
172 by (rule rtranclp_trans) iprover+ |
175 |
173 |
176 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] |
174 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set] |
177 |
175 |
178 text \<open> |
176 text \<open>\<^medskip> More @{term "r\<^sup>*"} equations and inclusions.\<close> |
179 \medskip More @{term "r^*"} equations and inclusions. |
177 |
180 \<close> |
178 lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
181 |
|
182 lemma rtranclp_idemp [simp]: "(r^**)^** = r^**" |
|
183 apply (auto intro!: order_antisym) |
179 apply (auto intro!: order_antisym) |
184 apply (erule rtranclp_induct) |
180 apply (erule rtranclp_induct) |
185 apply (rule rtranclp.rtrancl_refl) |
181 apply (rule rtranclp.rtrancl_refl) |
186 apply (blast intro: rtranclp_trans) |
182 apply (blast intro: rtranclp_trans) |
187 done |
183 done |
188 |
184 |
189 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] |
185 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set] |
190 |
186 |
191 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" |
187 lemma rtrancl_idemp_self_comp [simp]: "R\<^sup>* O R\<^sup>* = R\<^sup>*" |
192 apply (rule set_eqI) |
188 apply (rule set_eqI) |
193 apply (simp only: split_tupled_all) |
189 apply (simp only: split_tupled_all) |
194 apply (blast intro: rtrancl_trans) |
190 apply (blast intro: rtrancl_trans) |
195 done |
191 done |
196 |
192 |
197 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
193 lemma rtrancl_subset_rtrancl: "r \<subseteq> s\<^sup>* \<Longrightarrow> r\<^sup>* \<subseteq> s\<^sup>*" |
198 apply (drule rtrancl_mono) |
194 apply (drule rtrancl_mono) |
199 apply simp |
195 apply simp |
200 done |
196 done |
201 |
197 |
202 lemma rtranclp_subset: "R \<le> S ==> S \<le> R^** ==> S^** = R^**" |
198 lemma rtranclp_subset: "R \<le> S \<Longrightarrow> S \<le> R\<^sup>*\<^sup>* \<Longrightarrow> S\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" |
203 apply (drule rtranclp_mono) |
199 apply (drule rtranclp_mono) |
204 apply (drule rtranclp_mono) |
200 apply (drule rtranclp_mono) |
205 apply simp |
201 apply simp |
206 done |
202 done |
207 |
203 |
208 lemmas rtrancl_subset = rtranclp_subset [to_set] |
204 lemmas rtrancl_subset = rtranclp_subset [to_set] |
209 |
205 |
210 lemma rtranclp_sup_rtranclp: "(sup (R^**) (S^**))^** = (sup R S)^**" |
206 lemma rtranclp_sup_rtranclp: "(sup (R\<^sup>*\<^sup>*) (S\<^sup>*\<^sup>*))\<^sup>*\<^sup>* = (sup R S)\<^sup>*\<^sup>*" |
211 by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) |
207 by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D]) |
212 |
208 |
213 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] |
209 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set] |
214 |
210 |
215 lemma rtranclp_reflclp [simp]: "(R^==)^** = R^**" |
211 lemma rtranclp_reflclp [simp]: "(R\<^sup>=\<^sup>=)\<^sup>*\<^sup>* = R\<^sup>*\<^sup>*" |
216 by (blast intro!: rtranclp_subset) |
212 by (blast intro!: rtranclp_subset) |
217 |
213 |
218 lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set] |
214 lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set] |
219 |
215 |
220 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" |
216 lemma rtrancl_r_diff_Id: "(r - Id)\<^sup>* = r\<^sup>*" |
221 apply (rule sym) |
217 apply (rule sym) |
222 apply (rule rtrancl_subset, blast, clarify) |
218 apply (rule rtrancl_subset, blast, clarify) |
223 apply (rename_tac a b) |
219 apply (rename_tac a b) |
224 apply (case_tac "a = b") |
220 apply (case_tac "a = b") |
225 apply blast |
221 apply blast |
226 apply blast |
222 apply blast |
227 done |
223 done |
228 |
224 |
229 lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**" |
225 lemma rtranclp_r_diff_Id: "(inf r op \<noteq>)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*" |
230 apply (rule sym) |
226 apply (rule sym) |
231 apply (rule rtranclp_subset) |
227 apply (rule rtranclp_subset) |
232 apply blast+ |
228 apply blast+ |
233 done |
229 done |
234 |
230 |
235 theorem rtranclp_converseD: |
231 theorem rtranclp_converseD: |
236 assumes r: "(r^--1)^** x y" |
232 assumes "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" |
237 shows "r^** y x" |
233 shows "r\<^sup>*\<^sup>* y x" |
238 proof - |
234 using assms by induct (iprover intro: rtranclp_trans dest!: conversepD)+ |
239 from r show ?thesis |
|
240 by induct (iprover intro: rtranclp_trans dest!: conversepD)+ |
|
241 qed |
|
242 |
235 |
243 lemmas rtrancl_converseD = rtranclp_converseD [to_set] |
236 lemmas rtrancl_converseD = rtranclp_converseD [to_set] |
244 |
237 |
245 theorem rtranclp_converseI: |
238 theorem rtranclp_converseI: |
246 assumes "r^** y x" |
239 assumes "r\<^sup>*\<^sup>* y x" |
247 shows "(r^--1)^** x y" |
240 shows "(r\<inverse>\<inverse>)\<^sup>*\<^sup>* x y" |
248 using assms |
241 using assms by induct (iprover intro: rtranclp_trans conversepI)+ |
249 by induct (iprover intro: rtranclp_trans conversepI)+ |
|
250 |
242 |
251 lemmas rtrancl_converseI = rtranclp_converseI [to_set] |
243 lemmas rtrancl_converseI = rtranclp_converseI [to_set] |
252 |
244 |
253 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" |
245 lemma rtrancl_converse: "(r^-1)\<^sup>* = (r\<^sup>*)^-1" |
254 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
246 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
255 |
247 |
256 lemma sym_rtrancl: "sym r ==> sym (r^*)" |
248 lemma sym_rtrancl: "sym r \<Longrightarrow> sym (r\<^sup>*)" |
257 by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) |
249 by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) |
258 |
250 |
259 theorem converse_rtranclp_induct [consumes 1, case_names base step]: |
251 theorem converse_rtranclp_induct [consumes 1, case_names base step]: |
260 assumes major: "r^** a b" |
252 assumes major: "r\<^sup>*\<^sup>* a b" |
261 and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y" |
253 and cases: "P b" "\<And>y z. r y z \<Longrightarrow> r\<^sup>*\<^sup>* z b \<Longrightarrow> P z \<Longrightarrow> P y" |
262 shows "P a" |
254 shows "P a" |
263 using rtranclp_converseI [OF major] |
255 using rtranclp_converseI [OF major] |
264 by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ |
256 by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+ |
265 |
257 |
266 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] |
258 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set] |
267 |
259 |
268 lemmas converse_rtranclp_induct2 = |
260 lemmas converse_rtranclp_induct2 = |
269 converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, |
261 converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names refl step] |
270 consumes 1, case_names refl step] |
|
271 |
262 |
272 lemmas converse_rtrancl_induct2 = |
263 lemmas converse_rtrancl_induct2 = |
273 converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
264 converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
274 consumes 1, case_names refl step] |
265 consumes 1, case_names refl step] |
275 |
266 |
276 lemma converse_rtranclpE [consumes 1, case_names base step]: |
267 lemma converse_rtranclpE [consumes 1, case_names base step]: |
277 assumes major: "r^** x z" |
268 assumes major: "r\<^sup>*\<^sup>* x z" |
278 and cases: "x=z ==> P" |
269 and cases: "x = z \<Longrightarrow> P" "\<And>y. r x y \<Longrightarrow> r\<^sup>*\<^sup>* y z \<Longrightarrow> P" |
279 "!!y. [| r x y; r^** y z |] ==> P" |
|
280 shows P |
270 shows P |
281 apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)") |
271 apply (subgoal_tac "x = z \<or> (\<exists>y. r x y \<and> r\<^sup>*\<^sup>* y z)") |
282 apply (rule_tac [2] major [THEN converse_rtranclp_induct]) |
272 apply (rule_tac [2] major [THEN converse_rtranclp_induct]) |
283 prefer 2 apply iprover |
273 prefer 2 apply iprover |
284 prefer 2 apply iprover |
274 prefer 2 apply iprover |
285 apply (erule asm_rl exE disjE conjE cases)+ |
275 apply (erule asm_rl exE disjE conjE cases)+ |
286 done |
276 done |
289 |
279 |
290 lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] |
280 lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule] |
291 |
281 |
292 lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] |
282 lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] |
293 |
283 |
294 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" |
284 lemma r_comp_rtrancl_eq: "r O r\<^sup>* = r\<^sup>* O r" |
295 by (blast elim: rtranclE converse_rtranclE |
285 by (blast elim: rtranclE converse_rtranclE |
296 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
286 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
297 |
287 |
298 lemma rtrancl_unfold: "r^* = Id Un r^* O r" |
288 lemma rtrancl_unfold: "r\<^sup>* = Id \<union> r\<^sup>* O r" |
299 by (auto intro: rtrancl_into_rtrancl elim: rtranclE) |
289 by (auto intro: rtrancl_into_rtrancl elim: rtranclE) |
300 |
290 |
301 lemma rtrancl_Un_separatorE: |
291 lemma rtrancl_Un_separatorE: |
302 "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (a,x) : P^* \<longrightarrow> (x,y) : Q \<longrightarrow> x=y \<Longrightarrow> (a,b) : P^*" |
292 "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (a, x) \<in> P\<^sup>* \<longrightarrow> (x, y) \<in> Q \<longrightarrow> x = y \<Longrightarrow> (a, b) \<in> P\<^sup>*" |
303 apply (induct rule:rtrancl.induct) |
293 apply (induct rule:rtrancl.induct) |
304 apply blast |
294 apply blast |
305 apply (blast intro:rtrancl_trans) |
295 apply (blast intro:rtrancl_trans) |
306 done |
296 done |
307 |
297 |
308 lemma rtrancl_Un_separator_converseE: |
298 lemma rtrancl_Un_separator_converseE: |
309 "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*" |
299 "(a, b) \<in> (P \<union> Q)\<^sup>* \<Longrightarrow> \<forall>x y. (x, b) \<in> P\<^sup>* \<longrightarrow> (y, x) \<in> Q \<longrightarrow> y = x \<Longrightarrow> (a, b) \<in> P\<^sup>*" |
310 apply (induct rule:converse_rtrancl_induct) |
300 apply (induct rule:converse_rtrancl_induct) |
311 apply blast |
301 apply blast |
312 apply (blast intro:rtrancl_trans) |
302 apply (blast intro:rtrancl_trans) |
313 done |
303 done |
314 |
304 |
315 lemma Image_closed_trancl: |
305 lemma Image_closed_trancl: |
316 assumes "r `` X \<subseteq> X" shows "r\<^sup>* `` X = X" |
306 assumes "r `` X \<subseteq> X" |
|
307 shows "r\<^sup>* `` X = X" |
317 proof - |
308 proof - |
318 from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto |
309 from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" |
319 have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X" |
310 by auto |
|
311 have "x \<in> X" if 1: "(y, x) \<in> r\<^sup>*" and 2: "y \<in> X" for x y |
320 proof - |
312 proof - |
321 fix x y |
313 from 1 show "x \<in> X" |
322 assume *: "y \<in> X" |
|
323 assume "(y, x) \<in> r\<^sup>*" |
|
324 then show "x \<in> X" |
|
325 proof induct |
314 proof induct |
326 case base show ?case by (fact *) |
315 case base |
|
316 show ?case by (fact 2) |
327 next |
317 next |
328 case step with ** show ?case by auto |
318 case step |
|
319 with ** show ?case by auto |
329 qed |
320 qed |
330 qed |
321 qed |
331 then show ?thesis by auto |
322 then show ?thesis by auto |
332 qed |
323 qed |
333 |
324 |
334 |
325 |
335 subsection \<open>Transitive closure\<close> |
326 subsection \<open>Transitive closure\<close> |
336 |
327 |
337 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+" |
328 lemma trancl_mono: "\<And>p. p \<in> r\<^sup>+ \<Longrightarrow> r \<subseteq> s \<Longrightarrow> p \<in> s\<^sup>+" |
338 apply (simp add: split_tupled_all) |
329 apply (simp add: split_tupled_all) |
339 apply (erule trancl.induct) |
330 apply (erule trancl.induct) |
340 apply (iprover dest: subsetD)+ |
331 apply (iprover dest: subsetD)+ |
341 done |
332 done |
342 |
333 |
343 lemma r_into_trancl': "!!p. p : r ==> p : r^+" |
334 lemma r_into_trancl': "\<And>p. p \<in> r \<Longrightarrow> p \<in> r\<^sup>+" |
344 by (simp only: split_tupled_all) (erule r_into_trancl) |
335 by (simp only: split_tupled_all) (erule r_into_trancl) |
345 |
336 |
346 text \<open> |
337 text \<open>\<^medskip> Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.\<close> |
347 \medskip Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>. |
338 |
348 \<close> |
339 lemma tranclp_into_rtranclp: "r\<^sup>+\<^sup>+ a b \<Longrightarrow> r\<^sup>*\<^sup>* a b" |
349 |
|
350 lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b" |
|
351 by (erule tranclp.induct) iprover+ |
340 by (erule tranclp.induct) iprover+ |
352 |
341 |
353 lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] |
342 lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set] |
354 |
343 |
355 lemma rtranclp_into_tranclp1: assumes r: "r^** a b" |
344 lemma rtranclp_into_tranclp1: |
356 shows "!!c. r b c ==> r^++ a c" using r |
345 assumes "r\<^sup>*\<^sup>* a b" |
357 by induct iprover+ |
346 shows "r b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
|
347 using assms by (induct arbitrary: c) iprover+ |
358 |
348 |
359 lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] |
349 lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set] |
360 |
350 |
361 lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c" |
351 lemma rtranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
362 \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close> |
352 \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close> |
363 apply (erule rtranclp.cases) |
353 apply (erule rtranclp.cases) |
364 apply iprover |
354 apply iprover |
365 apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) |
355 apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1]) |
366 apply (simp | rule r_into_rtranclp)+ |
356 apply (simp | rule r_into_rtranclp)+ |
368 |
358 |
369 lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] |
359 lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set] |
370 |
360 |
371 text \<open>Nice induction rule for \<open>trancl\<close>\<close> |
361 text \<open>Nice induction rule for \<open>trancl\<close>\<close> |
372 lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: |
362 lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]: |
373 assumes a: "r^++ a b" |
363 assumes a: "r\<^sup>+\<^sup>+ a b" |
374 and cases: "!!y. r a y ==> P y" |
364 and cases: "\<And>y. r a y \<Longrightarrow> P y" "\<And>y z. r\<^sup>+\<^sup>+ a y \<Longrightarrow> r y z \<Longrightarrow> P y \<Longrightarrow> P z" |
375 "!!y z. r^++ a y ==> r y z ==> P y ==> P z" |
365 shows "P b" |
376 shows "P b" using a |
366 using a by (induct x\<equiv>a b) (iprover intro: cases)+ |
377 by (induct x\<equiv>a b) (iprover intro: cases)+ |
|
378 |
367 |
379 lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] |
368 lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set] |
380 |
369 |
381 lemmas tranclp_induct2 = |
370 lemmas tranclp_induct2 = |
382 tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, |
371 tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule, consumes 1, case_names base step] |
383 consumes 1, case_names base step] |
|
384 |
372 |
385 lemmas trancl_induct2 = |
373 lemmas trancl_induct2 = |
386 trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
374 trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete), |
387 consumes 1, case_names base step] |
375 consumes 1, case_names base step] |
388 |
376 |
389 lemma tranclp_trans_induct: |
377 lemma tranclp_trans_induct: |
390 assumes major: "r^++ x y" |
378 assumes major: "r\<^sup>+\<^sup>+ x y" |
391 and cases: "!!x y. r x y ==> P x y" |
379 and cases: "\<And>x y. r x y \<Longrightarrow> P x y" "\<And>x y z. r\<^sup>+\<^sup>+ x y \<Longrightarrow> P x y \<Longrightarrow> r\<^sup>+\<^sup>+ y z \<Longrightarrow> P y z \<Longrightarrow> P x z" |
392 "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z" |
|
393 shows "P x y" |
380 shows "P x y" |
394 \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close> |
381 \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close> |
395 by (iprover intro: major [THEN tranclp_induct] cases) |
382 by (iprover intro: major [THEN tranclp_induct] cases) |
396 |
383 |
397 lemmas trancl_trans_induct = tranclp_trans_induct [to_set] |
384 lemmas trancl_trans_induct = tranclp_trans_induct [to_set] |
398 |
385 |
399 lemma tranclE [cases set: trancl]: |
386 lemma tranclE [cases set: trancl]: |
400 assumes "(a, b) : r^+" |
387 assumes "(a, b) \<in> r\<^sup>+" |
401 obtains |
388 obtains |
402 (base) "(a, b) : r" |
389 (base) "(a, b) \<in> r" |
403 | (step) c where "(a, c) : r^+" and "(c, b) : r" |
390 | (step) c where "(a, c) \<in> r\<^sup>+" and "(c, b) \<in> r" |
404 using assms by cases simp_all |
391 using assms by cases simp_all |
405 |
392 |
406 lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s" |
393 lemma trancl_Int_subset: "r \<subseteq> s \<Longrightarrow> (r\<^sup>+ \<inter> s) O r \<subseteq> s \<Longrightarrow> r\<^sup>+ \<subseteq> s" |
407 apply (rule subsetI) |
394 apply (rule subsetI) |
408 apply auto |
395 apply auto |
409 apply (erule trancl_induct) |
396 apply (erule trancl_induct) |
410 apply auto |
397 apply auto |
411 done |
398 done |
412 |
399 |
413 lemma trancl_unfold: "r^+ = r Un r^+ O r" |
400 lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r" |
414 by (auto intro: trancl_into_trancl elim: tranclE) |
401 by (auto intro: trancl_into_trancl elim: tranclE) |
415 |
402 |
416 text \<open>Transitivity of @{term "r^+"}\<close> |
403 text \<open>Transitivity of @{term "r\<^sup>+"}\<close> |
417 lemma trans_trancl [simp]: "trans (r^+)" |
404 lemma trans_trancl [simp]: "trans (r\<^sup>+)" |
418 proof (rule transI) |
405 proof (rule transI) |
419 fix x y z |
406 fix x y z |
420 assume "(x, y) \<in> r^+" |
407 assume "(x, y) \<in> r\<^sup>+" |
421 assume "(y, z) \<in> r^+" |
408 assume "(y, z) \<in> r\<^sup>+" |
422 then show "(x, z) \<in> r^+" |
409 then show "(x, z) \<in> r\<^sup>+" |
423 proof induct |
410 proof induct |
424 case (base u) |
411 case (base u) |
425 from \<open>(x, y) \<in> r^+\<close> and \<open>(y, u) \<in> r\<close> |
412 from \<open>(x, y) \<in> r\<^sup>+\<close> and \<open>(y, u) \<in> r\<close> |
426 show "(x, u) \<in> r^+" .. |
413 show "(x, u) \<in> r\<^sup>+" .. |
427 next |
414 next |
428 case (step u v) |
415 case (step u v) |
429 from \<open>(x, u) \<in> r^+\<close> and \<open>(u, v) \<in> r\<close> |
416 from \<open>(x, u) \<in> r\<^sup>+\<close> and \<open>(u, v) \<in> r\<close> |
430 show "(x, v) \<in> r^+" .. |
417 show "(x, v) \<in> r\<^sup>+" .. |
431 qed |
418 qed |
432 qed |
419 qed |
433 |
420 |
434 lemmas trancl_trans = trans_trancl [THEN transD] |
421 lemmas trancl_trans = trans_trancl [THEN transD] |
435 |
422 |
436 lemma tranclp_trans: |
423 lemma tranclp_trans: |
437 assumes xy: "r^++ x y" |
424 assumes "r\<^sup>+\<^sup>+ x y" |
438 and yz: "r^++ y z" |
425 and "r\<^sup>+\<^sup>+ y z" |
439 shows "r^++ x z" using yz xy |
426 shows "r\<^sup>+\<^sup>+ x z" |
440 by induct iprover+ |
427 using assms(2,1) by induct iprover+ |
441 |
428 |
442 lemma trancl_id [simp]: "trans r \<Longrightarrow> r^+ = r" |
429 lemma trancl_id [simp]: "trans r \<Longrightarrow> r\<^sup>+ = r" |
443 apply auto |
430 apply auto |
444 apply (erule trancl_induct) |
431 apply (erule trancl_induct) |
445 apply assumption |
432 apply assumption |
446 apply (unfold trans_def) |
433 apply (unfold trans_def) |
447 apply blast |
434 apply blast |
448 done |
435 done |
449 |
436 |
450 lemma rtranclp_tranclp_tranclp: |
437 lemma rtranclp_tranclp_tranclp: |
451 assumes "r^** x y" |
438 assumes "r\<^sup>*\<^sup>* x y" |
452 shows "!!z. r^++ y z ==> r^++ x z" using assms |
439 shows "\<And>z. r\<^sup>+\<^sup>+ y z \<Longrightarrow> r\<^sup>+\<^sup>+ x z" |
453 by induct (iprover intro: tranclp_trans)+ |
440 using assms by induct (iprover intro: tranclp_trans)+ |
454 |
441 |
455 lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] |
442 lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set] |
456 |
443 |
457 lemma tranclp_into_tranclp2: "r a b ==> r^++ b c ==> r^++ a c" |
444 lemma tranclp_into_tranclp2: "r a b \<Longrightarrow> r\<^sup>+\<^sup>+ b c \<Longrightarrow> r\<^sup>+\<^sup>+ a c" |
458 by (erule tranclp_trans [OF tranclp.r_into_trancl]) |
445 by (erule tranclp_trans [OF tranclp.r_into_trancl]) |
459 |
446 |
460 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] |
447 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set] |
461 |
448 |
462 lemma tranclp_converseI: "(r^++)^--1 x y ==> (r^--1)^++ x y" |
449 lemma tranclp_converseI: "(r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y \<Longrightarrow> (r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y" |
463 apply (drule conversepD) |
450 apply (drule conversepD) |
464 apply (erule tranclp_induct) |
451 apply (erule tranclp_induct) |
465 apply (iprover intro: conversepI tranclp_trans)+ |
452 apply (iprover intro: conversepI tranclp_trans)+ |
466 done |
453 done |
467 |
454 |
468 lemmas trancl_converseI = tranclp_converseI [to_set] |
455 lemmas trancl_converseI = tranclp_converseI [to_set] |
469 |
456 |
470 lemma tranclp_converseD: "(r^--1)^++ x y ==> (r^++)^--1 x y" |
457 lemma tranclp_converseD: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ x y \<Longrightarrow> (r\<^sup>+\<^sup>+)\<inverse>\<inverse> x y" |
471 apply (rule conversepI) |
458 apply (rule conversepI) |
472 apply (erule tranclp_induct) |
459 apply (erule tranclp_induct) |
473 apply (iprover dest: conversepD intro: tranclp_trans)+ |
460 apply (iprover dest: conversepD intro: tranclp_trans)+ |
474 done |
461 done |
475 |
462 |
476 lemmas trancl_converseD = tranclp_converseD [to_set] |
463 lemmas trancl_converseD = tranclp_converseD [to_set] |
477 |
464 |
478 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1" |
465 lemma tranclp_converse: "(r\<inverse>\<inverse>)\<^sup>+\<^sup>+ = (r\<^sup>+\<^sup>+)\<inverse>\<inverse>" |
479 by (fastforce simp add: fun_eq_iff |
466 by (fastforce simp add: fun_eq_iff intro!: tranclp_converseI dest!: tranclp_converseD) |
480 intro!: tranclp_converseI dest!: tranclp_converseD) |
|
481 |
467 |
482 lemmas trancl_converse = tranclp_converse [to_set] |
468 lemmas trancl_converse = tranclp_converse [to_set] |
483 |
469 |
484 lemma sym_trancl: "sym r ==> sym (r^+)" |
470 lemma sym_trancl: "sym r \<Longrightarrow> sym (r\<^sup>+)" |
485 by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) |
471 by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) |
486 |
472 |
487 lemma converse_tranclp_induct [consumes 1, case_names base step]: |
473 lemma converse_tranclp_induct [consumes 1, case_names base step]: |
488 assumes major: "r^++ a b" |
474 assumes major: "r\<^sup>+\<^sup>+ a b" |
489 and cases: "!!y. r y b ==> P(y)" |
475 and cases: "\<And>y. r y b \<Longrightarrow> P y" "\<And>y z. r y z \<Longrightarrow> r\<^sup>+\<^sup>+ z b \<Longrightarrow> P z \<Longrightarrow> P y" |
490 "!!y z.[| r y z; r^++ z b; P(z) |] ==> P(y)" |
|
491 shows "P a" |
476 shows "P a" |
492 apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) |
477 apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major]) |
493 apply (rule cases) |
478 apply (rule cases) |
494 apply (erule conversepD) |
479 apply (erule conversepD) |
495 apply (blast intro: assms dest!: tranclp_converseD) |
480 apply (blast intro: assms dest!: tranclp_converseD) |
496 done |
481 done |
497 |
482 |
498 lemmas converse_trancl_induct = converse_tranclp_induct [to_set] |
483 lemmas converse_trancl_induct = converse_tranclp_induct [to_set] |
499 |
484 |
500 lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y" |
485 lemma tranclpD: "R\<^sup>+\<^sup>+ x y \<Longrightarrow> \<exists>z. R x z \<and> R\<^sup>*\<^sup>* z y" |
501 apply (erule converse_tranclp_induct) |
486 apply (erule converse_tranclp_induct) |
502 apply auto |
487 apply auto |
503 apply (blast intro: rtranclp_trans) |
488 apply (blast intro: rtranclp_trans) |
504 done |
489 done |
505 |
490 |
506 lemmas tranclD = tranclpD [to_set] |
491 lemmas tranclD = tranclpD [to_set] |
507 |
492 |
508 lemma converse_tranclpE: |
493 lemma converse_tranclpE: |
509 assumes major: "tranclp r x z" |
494 assumes major: "tranclp r x z" |
510 assumes base: "r x z ==> P" |
495 and base: "r x z \<Longrightarrow> P" |
511 assumes step: "\<And> y. [| r x y; tranclp r y z |] ==> P" |
496 and step: "\<And> y. r x y \<Longrightarrow> tranclp r y z \<Longrightarrow> P" |
512 shows P |
497 shows P |
513 proof - |
498 proof - |
514 from tranclpD[OF major] |
499 from tranclpD [OF major] obtain y where "r x y" and "rtranclp r y z" |
515 obtain y where "r x y" and "rtranclp r y z" by iprover |
500 by iprover |
516 from this(2) show P |
501 from this(2) show P |
517 proof (cases rule: rtranclp.cases) |
502 proof (cases rule: rtranclp.cases) |
518 case rtrancl_refl |
503 case rtrancl_refl |
519 with \<open>r x y\<close> base show P by iprover |
504 with \<open>r x y\<close> base show P |
|
505 by iprover |
520 next |
506 next |
521 case rtrancl_into_rtrancl |
507 case rtrancl_into_rtrancl |
522 from this have "tranclp r y z" |
508 from this have "tranclp r y z" |
523 by (iprover intro: rtranclp_into_tranclp1) |
509 by (iprover intro: rtranclp_into_tranclp1) |
524 with \<open>r x y\<close> step show P by iprover |
510 with \<open>r x y\<close> step show P |
|
511 by iprover |
525 qed |
512 qed |
526 qed |
513 qed |
527 |
514 |
528 lemmas converse_tranclE = converse_tranclpE [to_set] |
515 lemmas converse_tranclE = converse_tranclpE [to_set] |
529 |
516 |
530 lemma tranclD2: |
517 lemma tranclD2: "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" |
531 "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" |
|
532 by (blast elim: tranclE intro: trancl_into_rtrancl) |
518 by (blast elim: tranclE intro: trancl_into_rtrancl) |
533 |
519 |
534 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" |
520 lemma irrefl_tranclI: "r\<inverse> \<inter> r\<^sup>* = {} \<Longrightarrow> (x, x) \<notin> r\<^sup>+" |
535 by (blast elim: tranclE dest: trancl_into_rtrancl) |
521 by (blast elim: tranclE dest: trancl_into_rtrancl) |
536 |
522 |
537 lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r^+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y" |
523 lemma irrefl_trancl_rD: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> x \<noteq> y" |
538 by (blast dest: r_into_trancl) |
524 by (blast dest: r_into_trancl) |
539 |
525 |
540 lemma trancl_subset_Sigma_aux: |
526 lemma trancl_subset_Sigma_aux: "(a, b) \<in> r\<^sup>* \<Longrightarrow> r \<subseteq> A \<times> A \<Longrightarrow> a = b \<or> a \<in> A" |
541 "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A" |
|
542 by (induct rule: rtrancl_induct) auto |
527 by (induct rule: rtrancl_induct) auto |
543 |
528 |
544 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A" |
529 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A \<Longrightarrow> r\<^sup>+ \<subseteq> A \<times> A" |
545 apply (rule subsetI) |
530 apply (rule subsetI) |
546 apply (simp only: split_tupled_all) |
531 apply (simp only: split_tupled_all) |
547 apply (erule tranclE) |
532 apply (erule tranclE) |
548 apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ |
533 apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+ |
549 done |
534 done |
550 |
535 |
551 lemma reflclp_tranclp [simp]: "(r^++)^== = r^**" |
536 lemma reflclp_tranclp [simp]: "(r\<^sup>+\<^sup>+)\<^sup>=\<^sup>= = r\<^sup>*\<^sup>*" |
552 apply (safe intro!: order_antisym) |
537 apply (safe intro!: order_antisym) |
553 apply (erule tranclp_into_rtranclp) |
538 apply (erule tranclp_into_rtranclp) |
554 apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) |
539 apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1) |
555 done |
540 done |
556 |
541 |
557 lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set] |
542 lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set] |
558 |
543 |
559 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*" |
544 lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*" |
560 apply safe |
545 apply safe |
561 apply (drule trancl_into_rtrancl, simp) |
546 apply (drule trancl_into_rtrancl, simp) |
562 apply (erule rtranclE, safe) |
547 apply (erule rtranclE, safe) |
563 apply (rule r_into_trancl, simp) |
548 apply (rule r_into_trancl, simp) |
564 apply (rule rtrancl_into_trancl1) |
549 apply (rule rtrancl_into_trancl1) |
565 apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) |
550 apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast) |
566 done |
551 done |
567 |
552 |
568 lemma rtrancl_trancl_reflcl [code]: "r^* = (r^+)^=" |
553 lemma rtrancl_trancl_reflcl [code]: "r\<^sup>* = (r\<^sup>+)\<^sup>=" |
569 by simp |
554 by simp |
570 |
555 |
571 lemma trancl_empty [simp]: "{}^+ = {}" |
556 lemma trancl_empty [simp]: "{}\<^sup>+ = {}" |
572 by (auto elim: trancl_induct) |
557 by (auto elim: trancl_induct) |
573 |
558 |
574 lemma rtrancl_empty [simp]: "{}^* = Id" |
559 lemma rtrancl_empty [simp]: "{}\<^sup>* = Id" |
575 by (rule subst [OF reflcl_trancl]) simp |
560 by (rule subst [OF reflcl_trancl]) simp |
576 |
561 |
577 lemma rtranclpD: "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b" |
562 lemma rtranclpD: "R\<^sup>*\<^sup>* a b \<Longrightarrow> a = b \<or> a \<noteq> b \<and> R\<^sup>+\<^sup>+ a b" |
578 by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp) |
563 by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp) |
579 |
564 |
580 lemmas rtranclD = rtranclpD [to_set] |
565 lemmas rtranclD = rtranclpD [to_set] |
581 |
566 |
582 lemma rtrancl_eq_or_trancl: |
567 lemma rtrancl_eq_or_trancl: "(x,y) \<in> R\<^sup>* \<longleftrightarrow> x = y \<or> x \<noteq> y \<and> (x, y) \<in> R\<^sup>+" |
583 "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)" |
|
584 by (fast elim: trancl_into_rtrancl dest: rtranclD) |
568 by (fast elim: trancl_into_rtrancl dest: rtranclD) |
585 |
569 |
586 lemma trancl_unfold_right: "r^+ = r^* O r" |
570 lemma trancl_unfold_right: "r\<^sup>+ = r\<^sup>* O r" |
587 by (auto dest: tranclD2 intro: rtrancl_into_trancl1) |
571 by (auto dest: tranclD2 intro: rtrancl_into_trancl1) |
588 |
572 |
589 lemma trancl_unfold_left: "r^+ = r O r^*" |
573 lemma trancl_unfold_left: "r\<^sup>+ = r O r\<^sup>*" |
590 by (auto dest: tranclD intro: rtrancl_into_trancl2) |
574 by (auto dest: tranclD intro: rtrancl_into_trancl2) |
591 |
575 |
592 lemma trancl_insert: |
576 lemma trancl_insert: "(insert (y, x) r)\<^sup>+ = r\<^sup>+ \<union> {(a, b). (a, y) \<in> r\<^sup>* \<and> (x, b) \<in> r\<^sup>*}" |
593 "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" |
|
594 \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close> |
577 \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close> |
595 apply (rule equalityI) |
578 apply (rule equalityI) |
596 apply (rule subsetI) |
579 apply (rule subsetI) |
597 apply (simp only: split_tupled_all) |
580 apply (simp only: split_tupled_all) |
598 apply (erule trancl_induct, blast) |
581 apply (erule trancl_induct, blast) |
601 apply (blast intro: trancl_mono rtrancl_mono |
584 apply (blast intro: trancl_mono rtrancl_mono |
602 [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
585 [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
603 done |
586 done |
604 |
587 |
605 lemma trancl_insert2: |
588 lemma trancl_insert2: |
606 "(insert (a,b) r)^+ = r^+ \<union> {(x,y). ((x,a) : r^+ \<or> x=a) \<and> ((b,y) \<in> r^+ \<or> y=b)}" |
589 "(insert (a, b) r)\<^sup>+ = r\<^sup>+ \<union> {(x, y). ((x, a) \<in> r\<^sup>+ \<or> x = a) \<and> ((b, y) \<in> r\<^sup>+ \<or> y = b)}" |
607 by(auto simp add: trancl_insert rtrancl_eq_or_trancl) |
590 by (auto simp add: trancl_insert rtrancl_eq_or_trancl) |
608 |
591 |
609 lemma rtrancl_insert: |
592 lemma rtrancl_insert: "(insert (a,b) r)\<^sup>* = r\<^sup>* \<union> {(x, y). (x, a) \<in> r\<^sup>* \<and> (b, y) \<in> r\<^sup>*}" |
610 "(insert (a,b) r)^* = r^* \<union> {(x,y). (x,a) : r^* \<and> (b,y) \<in> r^*}" |
593 using trancl_insert[of a b r] |
611 using trancl_insert[of a b r] |
594 by (simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast |
612 by(simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast |
|
613 |
595 |
614 |
596 |
615 text \<open>Simplifying nested closures\<close> |
597 text \<open>Simplifying nested closures\<close> |
616 |
598 |
617 lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*" |
599 lemma rtrancl_trancl_absorb[simp]: "(R\<^sup>*)\<^sup>+ = R\<^sup>*" |
618 by (simp add: trans_rtrancl) |
600 by (simp add: trans_rtrancl) |
619 |
601 |
620 lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*" |
602 lemma trancl_rtrancl_absorb[simp]: "(R\<^sup>+)\<^sup>* = R\<^sup>*" |
621 by (subst reflcl_trancl[symmetric]) simp |
603 by (subst reflcl_trancl[symmetric]) simp |
622 |
604 |
623 lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*" |
605 lemma rtrancl_reflcl_absorb[simp]: "(R\<^sup>*)\<^sup>= = R\<^sup>*" |
624 by auto |
606 by auto |
625 |
607 |
626 |
608 |
627 text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close> |
609 text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close> |
628 |
610 |
629 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV" |
611 lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV" |
630 by blast |
612 by blast |
631 |
613 |
632 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV" |
614 lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV" |
633 by blast |
615 by blast |
634 |
616 |
635 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*" |
617 lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R \<union> S)\<^sup>*" |
636 by (rule rtrancl_Un_rtrancl [THEN subst]) fast |
618 by (rule rtrancl_Un_rtrancl [THEN subst]) fast |
637 |
619 |
638 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*" |
620 lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*" |
639 by (blast intro: subsetD [OF rtrancl_Un_subset]) |
621 by (blast intro: subsetD [OF rtrancl_Un_subset]) |
640 |
622 |
641 lemma trancl_domain [simp]: "Domain (r^+) = Domain r" |
623 lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r" |
642 by (unfold Domain_unfold) (blast dest: tranclD) |
624 by (unfold Domain_unfold) (blast dest: tranclD) |
643 |
625 |
644 lemma trancl_range [simp]: "Range (r^+) = Range r" |
626 lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r" |
645 unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric]) |
627 unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric]) |
646 |
628 |
647 lemma Not_Domain_rtrancl: |
629 lemma Not_Domain_rtrancl: "x \<notin> Domain R \<Longrightarrow> (x, y) \<in> R\<^sup>* \<longleftrightarrow> x = y" |
648 "x ~: Domain R ==> ((x, y) : R^*) = (x = y)" |
|
649 apply auto |
630 apply auto |
650 apply (erule rev_mp) |
631 apply (erule rev_mp) |
651 apply (erule rtrancl_induct) |
632 apply (erule rtrancl_induct) |
652 apply auto |
633 apply auto |
653 done |
634 done |
654 |
635 |
655 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r" |
636 lemma trancl_subset_Field2: "r\<^sup>+ \<subseteq> Field r \<times> Field r" |
656 apply clarify |
637 apply clarify |
657 apply (erule trancl_induct) |
638 apply (erule trancl_induct) |
658 apply (auto simp add: Field_def) |
639 apply (auto simp add: Field_def) |
659 done |
640 done |
660 |
641 |
661 lemma finite_trancl[simp]: "finite (r^+) = finite r" |
642 lemma finite_trancl[simp]: "finite (r\<^sup>+) = finite r" |
662 apply auto |
643 apply auto |
663 prefer 2 |
644 prefer 2 |
664 apply (rule trancl_subset_Field2 [THEN finite_subset]) |
645 apply (rule trancl_subset_Field2 [THEN finite_subset]) |
665 apply (rule finite_SigmaI) |
646 apply (rule finite_SigmaI) |
666 prefer 3 |
647 prefer 3 |
758 by (simp_all add: relpowp_code_def) |
738 by (simp_all add: relpowp_code_def) |
759 |
739 |
760 hide_const (open) relpow |
740 hide_const (open) relpow |
761 hide_const (open) relpowp |
741 hide_const (open) relpowp |
762 |
742 |
763 lemma relpow_1 [simp]: |
743 lemma relpow_1 [simp]: "R ^^ 1 = R" for R :: "('a \<times> 'a) set" |
764 fixes R :: "('a \<times> 'a) set" |
|
765 shows "R ^^ 1 = R" |
|
766 by simp |
744 by simp |
767 |
745 |
768 lemma relpowp_1 [simp]: |
746 lemma relpowp_1 [simp]: "P ^^ 1 = P" for P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
769 fixes P :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
770 shows "P ^^ 1 = P" |
|
771 by (fact relpow_1 [to_pred]) |
747 by (fact relpow_1 [to_pred]) |
772 |
748 |
773 lemma relpow_0_I: |
749 lemma relpow_0_I: "(x, x) \<in> R ^^ 0" |
774 "(x, x) \<in> R ^^ 0" |
|
775 by simp |
750 by simp |
776 |
751 |
777 lemma relpowp_0_I: |
752 lemma relpowp_0_I: "(P ^^ 0) x x" |
778 "(P ^^ 0) x x" |
|
779 by (fact relpow_0_I [to_pred]) |
753 by (fact relpow_0_I [to_pred]) |
780 |
754 |
781 lemma relpow_Suc_I: |
755 lemma relpow_Suc_I: "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
782 "(x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
|
783 by auto |
756 by auto |
784 |
757 |
785 lemma relpowp_Suc_I: |
758 lemma relpowp_Suc_I: "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z" |
786 "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z" |
|
787 by (fact relpow_Suc_I [to_pred]) |
759 by (fact relpow_Suc_I [to_pred]) |
788 |
760 |
789 lemma relpow_Suc_I2: |
761 lemma relpow_Suc_I2: "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
790 "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n" |
|
791 by (induct n arbitrary: z) (simp, fastforce) |
762 by (induct n arbitrary: z) (simp, fastforce) |
792 |
763 |
793 lemma relpowp_Suc_I2: |
764 lemma relpowp_Suc_I2: "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z" |
794 "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z" |
|
795 by (fact relpow_Suc_I2 [to_pred]) |
765 by (fact relpow_Suc_I2 [to_pred]) |
796 |
766 |
797 lemma relpow_0_E: |
767 lemma relpow_0_E: "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" |
798 "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P" |
|
799 by simp |
768 by simp |
800 |
769 |
801 lemma relpowp_0_E: |
770 lemma relpowp_0_E: "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q" |
802 "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q" |
|
803 by (fact relpow_0_E [to_pred]) |
771 by (fact relpow_0_E [to_pred]) |
804 |
772 |
805 lemma relpow_Suc_E: |
773 lemma relpow_Suc_E: "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" |
806 "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P" |
|
807 by auto |
774 by auto |
808 |
775 |
809 lemma relpowp_Suc_E: |
776 lemma relpowp_Suc_E: "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" |
810 "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q" |
|
811 by (fact relpow_Suc_E [to_pred]) |
777 by (fact relpow_Suc_E [to_pred]) |
812 |
778 |
813 lemma relpow_E: |
779 lemma relpow_E: |
814 "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
780 "(x, z) \<in> R ^^ n \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P) |
815 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) |
781 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) |
862 "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) |
822 "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q) |
863 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) |
823 \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q) |
864 \<Longrightarrow> Q" |
824 \<Longrightarrow> Q" |
865 by (fact relpow_E2 [to_pred]) |
825 by (fact relpow_E2 [to_pred]) |
866 |
826 |
867 lemma relpow_add: "R ^^ (m+n) = R^^m O R^^n" |
827 lemma relpow_add: "R ^^ (m + n) = R^^m O R^^n" |
868 by (induct n) auto |
828 by (induct n) auto |
869 |
829 |
870 lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" |
830 lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n" |
871 by (fact relpow_add [to_pred]) |
831 by (fact relpow_add [to_pred]) |
872 |
832 |
873 lemma relpow_commute: "R O R ^^ n = R ^^ n O R" |
833 lemma relpow_commute: "R O R ^^ n = R ^^ n O R" |
874 by (induct n) (simp, simp add: O_assoc [symmetric]) |
834 by (induct n) (simp_all add: O_assoc [symmetric]) |
875 |
835 |
876 lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" |
836 lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P" |
877 by (fact relpow_commute [to_pred]) |
837 by (fact relpow_commute [to_pred]) |
878 |
838 |
879 lemma relpow_empty: |
839 lemma relpow_empty: "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}" |
880 "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}" |
|
881 by (cases n) auto |
840 by (cases n) auto |
882 |
841 |
883 lemma relpowp_bot: |
842 lemma relpowp_bot: "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>" |
884 "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>" |
|
885 by (fact relpow_empty [to_pred]) |
843 by (fact relpow_empty [to_pred]) |
886 |
844 |
887 lemma rtrancl_imp_UN_relpow: |
845 lemma rtrancl_imp_UN_relpow: |
888 assumes "p \<in> R^*" |
846 assumes "p \<in> R\<^sup>*" |
889 shows "p \<in> (\<Union>n. R ^^ n)" |
847 shows "p \<in> (\<Union>n. R ^^ n)" |
890 proof (cases p) |
848 proof (cases p) |
891 case (Pair x y) |
849 case (Pair x y) |
892 with assms have "(x, y) \<in> R^*" by simp |
850 with assms have "(x, y) \<in> R\<^sup>*" by simp |
893 then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct |
851 then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct |
894 case base show ?case by (blast intro: relpow_0_I) |
852 case base |
|
853 show ?case by (blast intro: relpow_0_I) |
895 next |
854 next |
896 case step then show ?case by (blast intro: relpow_Suc_I) |
855 case step |
|
856 then show ?case by (blast intro: relpow_Suc_I) |
897 qed |
857 qed |
898 with Pair show ?thesis by simp |
858 with Pair show ?thesis by simp |
899 qed |
859 qed |
900 |
860 |
901 lemma rtranclp_imp_Sup_relpowp: |
861 lemma rtranclp_imp_Sup_relpowp: |
902 assumes "(P^**) x y" |
862 assumes "(P\<^sup>*\<^sup>*) x y" |
903 shows "(\<Squnion>n. P ^^ n) x y" |
863 shows "(\<Squnion>n. P ^^ n) x y" |
904 using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp |
864 using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp |
905 |
865 |
906 lemma relpow_imp_rtrancl: |
866 lemma relpow_imp_rtrancl: |
907 assumes "p \<in> R ^^ n" |
867 assumes "p \<in> R ^^ n" |
908 shows "p \<in> R^*" |
868 shows "p \<in> R\<^sup>*" |
909 proof (cases p) |
869 proof (cases p) |
910 case (Pair x y) |
870 case (Pair x y) |
911 with assms have "(x, y) \<in> R ^^ n" by simp |
871 with assms have "(x, y) \<in> R ^^ n" by simp |
912 then have "(x, y) \<in> R^*" proof (induct n arbitrary: x y) |
872 then have "(x, y) \<in> R\<^sup>*" proof (induct n arbitrary: x y) |
913 case 0 then show ?case by simp |
873 case 0 |
|
874 then show ?case by simp |
914 next |
875 next |
915 case Suc then show ?case |
876 case Suc |
|
877 then show ?case |
916 by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) |
878 by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl) |
917 qed |
879 qed |
918 with Pair show ?thesis by simp |
880 with Pair show ?thesis by simp |
919 qed |
881 qed |
920 |
882 |
921 lemma relpowp_imp_rtranclp: |
883 lemma relpowp_imp_rtranclp: "(P ^^ n) x y \<Longrightarrow> (P\<^sup>*\<^sup>*) x y" |
922 assumes "(P ^^ n) x y" |
884 using relpow_imp_rtrancl [of "(x, y)", to_pred] by simp |
923 shows "(P^**) x y" |
885 |
924 using assms and relpow_imp_rtrancl [of "(x, y)", to_pred] by simp |
886 lemma rtrancl_is_UN_relpow: "R\<^sup>* = (\<Union>n. R ^^ n)" |
925 |
|
926 lemma rtrancl_is_UN_relpow: |
|
927 "R^* = (\<Union>n. R ^^ n)" |
|
928 by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) |
887 by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl) |
929 |
888 |
930 lemma rtranclp_is_Sup_relpowp: |
889 lemma rtranclp_is_Sup_relpowp: "P\<^sup>*\<^sup>* = (\<Squnion>n. P ^^ n)" |
931 "P^** = (\<Squnion>n. P ^^ n)" |
|
932 using rtrancl_is_UN_relpow [to_pred, of P] by auto |
890 using rtrancl_is_UN_relpow [to_pred, of P] by auto |
933 |
891 |
934 lemma rtrancl_power: |
892 lemma rtrancl_power: "p \<in> R\<^sup>* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" |
935 "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)" |
|
936 by (simp add: rtrancl_is_UN_relpow) |
893 by (simp add: rtrancl_is_UN_relpow) |
937 |
894 |
938 lemma rtranclp_power: |
895 lemma rtranclp_power: "(P\<^sup>*\<^sup>*) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)" |
939 "(P^**) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)" |
|
940 by (simp add: rtranclp_is_Sup_relpowp) |
896 by (simp add: rtranclp_is_Sup_relpowp) |
941 |
897 |
942 lemma trancl_power: |
898 lemma trancl_power: "p \<in> R\<^sup>+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" |
943 "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)" |
|
944 apply (cases p) |
899 apply (cases p) |
945 apply simp |
900 apply simp |
946 apply (rule iffI) |
901 apply (rule iffI) |
947 apply (drule tranclD2) |
902 apply (drule tranclD2) |
948 apply (clarsimp simp: rtrancl_is_UN_relpow) |
903 apply (clarsimp simp: rtrancl_is_UN_relpow) |
954 apply clarsimp |
909 apply clarsimp |
955 apply (drule relpow_imp_rtrancl) |
910 apply (drule relpow_imp_rtrancl) |
956 apply (drule rtrancl_into_trancl1) apply auto |
911 apply (drule rtrancl_into_trancl1) apply auto |
957 done |
912 done |
958 |
913 |
959 lemma tranclp_power: |
914 lemma tranclp_power: "(P\<^sup>+\<^sup>+) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)" |
960 "(P^++) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)" |
|
961 using trancl_power [to_pred, of P "(x, y)"] by simp |
915 using trancl_power [to_pred, of P "(x, y)"] by simp |
962 |
916 |
963 lemma rtrancl_imp_relpow: |
917 lemma rtrancl_imp_relpow: "p \<in> R\<^sup>* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" |
964 "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n" |
|
965 by (auto dest: rtrancl_imp_UN_relpow) |
918 by (auto dest: rtrancl_imp_UN_relpow) |
966 |
919 |
967 lemma rtranclp_imp_relpowp: |
920 lemma rtranclp_imp_relpowp: "(P\<^sup>*\<^sup>*) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y" |
968 "(P^**) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y" |
|
969 by (auto dest: rtranclp_imp_Sup_relpowp) |
921 by (auto dest: rtranclp_imp_Sup_relpowp) |
970 |
922 |
971 text\<open>By Sternagel/Thiemann:\<close> |
923 text \<open>By Sternagel/Thiemann:\<close> |
972 lemma relpow_fun_conv: |
924 lemma relpow_fun_conv: "(a, b) \<in> R ^^ n \<longleftrightarrow> (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f (Suc i)) \<in> R))" |
973 "((a,b) \<in> R ^^ n) = (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f(Suc i)) \<in> R))" |
|
974 proof (induct n arbitrary: b) |
925 proof (induct n arbitrary: b) |
975 case 0 show ?case by auto |
926 case 0 |
|
927 show ?case by auto |
976 next |
928 next |
977 case (Suc n) |
929 case (Suc n) |
978 show ?case |
930 show ?case |
979 proof (simp add: relcomp_unfold Suc) |
931 proof (simp add: relcomp_unfold Suc) |
980 show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) |
932 show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R) \<longleftrightarrow> |
981 = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))" |
933 (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))" |
982 (is "?l = ?r") |
934 (is "?l = ?r") |
983 proof |
935 proof |
984 assume ?l |
936 assume ?l |
985 then obtain c f where 1: "f 0 = a" "f n = c" "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R" "(c,b) \<in> R" by auto |
937 then obtain c f |
|
938 where 1: "f 0 = a" "f n = c" "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R" "(c,b) \<in> R" |
|
939 by auto |
986 let ?g = "\<lambda> m. if m = Suc n then b else f m" |
940 let ?g = "\<lambda> m. if m = Suc n then b else f m" |
987 show ?r by (rule exI[of _ ?g], simp add: 1) |
941 show ?r by (rule exI[of _ ?g]) (simp add: 1) |
988 next |
942 next |
989 assume ?r |
943 assume ?r |
990 then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto |
944 then obtain f where 1: "f 0 = a" "b = f (Suc n)" "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" |
|
945 by auto |
991 show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) |
946 show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto) |
992 qed |
947 qed |
993 qed |
948 qed |
994 qed |
949 qed |
995 |
950 |
996 lemma relpowp_fun_conv: |
951 lemma relpowp_fun_conv: "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))" |
997 "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))" |
|
998 by (fact relpow_fun_conv [to_pred]) |
952 by (fact relpow_fun_conv [to_pred]) |
999 |
953 |
1000 lemma relpow_finite_bounded1: |
954 lemma relpow_finite_bounded1: |
1001 assumes "finite(R :: ('a*'a)set)" and "k>0" |
955 fixes R :: "('a \<times> 'a) set" |
1002 shows "R^^k \<subseteq> (UN n:{n. 0<n & n <= card R}. R^^n)" (is "_ \<subseteq> ?r") |
956 assumes "finite R" and "k > 0" |
1003 proof- |
957 shows "R^^k \<subseteq> (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" (is "_ \<subseteq> ?r") |
1004 { fix a b k |
958 proof - |
1005 have "(a,b) : R^^(Suc k) \<Longrightarrow> EX n. 0<n & n <= card R & (a,b) : R^^n" |
959 have "(a, b) \<in> R^^(Suc k) \<Longrightarrow> \<exists>n. 0 < n \<and> n \<le> card R \<and> (a, b) \<in> R^^n" for a b k |
1006 proof(induct k arbitrary: b) |
960 proof (induct k arbitrary: b) |
1007 case 0 |
961 case 0 |
1008 hence "R \<noteq> {}" by auto |
962 then have "R \<noteq> {}" by auto |
1009 with card_0_eq[OF \<open>finite R\<close>] have "card R >= Suc 0" by auto |
963 with card_0_eq[OF \<open>finite R\<close>] have "card R \<ge> Suc 0" by auto |
1010 thus ?case using 0 by force |
964 then show ?case using 0 by force |
|
965 next |
|
966 case (Suc k) |
|
967 then obtain a' where "(a, a') \<in> R^^(Suc k)" and "(a', b) \<in> R" |
|
968 by auto |
|
969 from Suc(1)[OF \<open>(a, a') \<in> R^^(Suc k)\<close>] obtain n where "n \<le> card R" and "(a, a') \<in> R ^^ n" |
|
970 by auto |
|
971 have "(a, b) \<in> R^^(Suc n)" |
|
972 using \<open>(a, a') \<in> R^^n\<close> and \<open>(a', b)\<in> R\<close> by auto |
|
973 from \<open>n \<le> card R\<close> consider "n < card R" | "n = card R" by force |
|
974 then show ?case |
|
975 proof cases |
|
976 case 1 |
|
977 then show ?thesis |
|
978 using \<open>(a, b) \<in> R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast |
1011 next |
979 next |
1012 case (Suc k) |
980 case 2 |
1013 then obtain a' where "(a,a') : R^^(Suc k)" and "(a',b) : R" by auto |
981 from \<open>(a, b) \<in> R ^^ (Suc n)\<close> [unfolded relpow_fun_conv] |
1014 from Suc(1)[OF \<open>(a,a') : R^^(Suc k)\<close>] |
982 obtain f where "f 0 = a" and "f (Suc n) = b" |
1015 obtain n where "n \<le> card R" and "(a,a') \<in> R ^^ n" by auto |
983 and steps: "\<And>i. i \<le> n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto |
1016 have "(a,b) : R^^(Suc n)" using \<open>(a,a') \<in> R^^n\<close> and \<open>(a',b)\<in> R\<close> by auto |
984 let ?p = "\<lambda>i. (f i, f(Suc i))" |
1017 { assume "n < card R" |
985 let ?N = "{i. i \<le> n}" |
1018 hence ?case using \<open>(a,b): R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast |
986 have "?p ` ?N \<subseteq> R" |
1019 } moreover |
987 using steps by auto |
1020 { assume "n = card R" |
988 from card_mono[OF assms(1) this] have "card (?p ` ?N) \<le> card R" . |
1021 from \<open>(a,b) \<in> R ^^ (Suc n)\<close>[unfolded relpow_fun_conv] |
989 also have "\<dots> < card ?N" |
1022 obtain f where "f 0 = a" and "f(Suc n) = b" |
990 using \<open>n = card R\<close> by simp |
1023 and steps: "\<And>i. i <= n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto |
991 finally have "\<not> inj_on ?p ?N" |
1024 let ?p = "%i. (f i, f(Suc i))" |
992 by (rule pigeonhole) |
1025 let ?N = "{i. i \<le> n}" |
993 then obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i \<noteq> j" and pij: "?p i = ?p j" |
1026 have "?p ` ?N <= R" using steps by auto |
994 by (auto simp: inj_on_def) |
1027 from card_mono[OF assms(1) this] |
995 let ?i = "min i j" |
1028 have "card(?p ` ?N) <= card R" . |
996 let ?j = "max i j" |
1029 also have "\<dots> < card ?N" using \<open>n = card R\<close> by simp |
997 have i: "?i \<le> n" and j: "?j \<le> n" and pij: "?p ?i = ?p ?j" and ij: "?i < ?j" |
1030 finally have "~ inj_on ?p ?N" by(rule pigeonhole) |
998 using i j ij pij unfolding min_def max_def by auto |
1031 then obtain i j where i: "i <= n" and j: "j <= n" and ij: "i \<noteq> j" and |
999 from i j pij ij obtain i j where i: "i \<le> n" and j: "j \<le> n" and ij: "i < j" |
1032 pij: "?p i = ?p j" by(auto simp: inj_on_def) |
1000 and pij: "?p i = ?p j" |
1033 let ?i = "min i j" let ?j = "max i j" |
1001 by blast |
1034 have i: "?i <= n" and j: "?j <= n" and pij: "?p ?i = ?p ?j" |
1002 let ?g = "\<lambda>l. if l \<le> i then f l else f (l + (j - i))" |
1035 and ij: "?i < ?j" |
1003 let ?n = "Suc (n - (j - i))" |
1036 using i j ij pij unfolding min_def max_def by auto |
1004 have abl: "(a, b) \<in> R ^^ ?n" |
1037 from i j pij ij obtain i j where i: "i<=n" and j: "j<=n" and ij: "i<j" |
1005 unfolding relpow_fun_conv |
1038 and pij: "?p i = ?p j" by blast |
1006 proof (rule exI[of _ ?g], intro conjI impI allI) |
1039 let ?g = "\<lambda> l. if l \<le> i then f l else f (l + (j - i))" |
1007 show "?g ?n = b" |
1040 let ?n = "Suc(n - (j - i))" |
1008 using \<open>f(Suc n) = b\<close> j ij by auto |
1041 have abl: "(a,b) \<in> R ^^ ?n" unfolding relpow_fun_conv |
1009 next |
1042 proof (rule exI[of _ ?g], intro conjI impI allI) |
1010 fix k |
1043 show "?g ?n = b" using \<open>f(Suc n) = b\<close> j ij by auto |
1011 assume "k < ?n" |
|
1012 show "(?g k, ?g (Suc k)) \<in> R" |
|
1013 proof (cases "k < i") |
|
1014 case True |
|
1015 with i have "k \<le> n" |
|
1016 by auto |
|
1017 from steps[OF this] show ?thesis |
|
1018 using True by simp |
1044 next |
1019 next |
1045 fix k assume "k < ?n" |
1020 case False |
1046 show "(?g k, ?g (Suc k)) \<in> R" |
1021 then have "i \<le> k" by auto |
1047 proof (cases "k < i") |
1022 show ?thesis |
|
1023 proof (cases "k = i") |
1048 case True |
1024 case True |
1049 with i have "k <= n" by auto |
1025 then show ?thesis |
1050 from steps[OF this] show ?thesis using True by simp |
1026 using ij pij steps[OF i] by simp |
1051 next |
1027 next |
1052 case False |
1028 case False |
1053 hence "i \<le> k" by auto |
1029 with \<open>i \<le> k\<close> have "i < k" by auto |
|
1030 then have small: "k + (j - i) \<le> n" |
|
1031 using \<open>k<?n\<close> by arith |
1054 show ?thesis |
1032 show ?thesis |
1055 proof (cases "k = i") |
1033 using steps[OF small] \<open>i<k\<close> by auto |
1056 case True |
|
1057 thus ?thesis using ij pij steps[OF i] by simp |
|
1058 next |
|
1059 case False |
|
1060 with \<open>i \<le> k\<close> have "i < k" by auto |
|
1061 hence small: "k + (j - i) <= n" using \<open>k<?n\<close> by arith |
|
1062 show ?thesis using steps[OF small] \<open>i<k\<close> by auto |
|
1063 qed |
|
1064 qed |
1034 qed |
1065 qed (simp add: \<open>f 0 = a\<close>) |
1035 qed |
1066 moreover have "?n <= n" using i j ij by arith |
1036 qed (simp add: \<open>f 0 = a\<close>) |
1067 ultimately have ?case using \<open>n = card R\<close> by blast |
1037 moreover have "?n \<le> n" |
1068 } |
1038 using i j ij by arith |
1069 ultimately show ?case using \<open>n \<le> card R\<close> by force |
1039 ultimately show ?thesis |
|
1040 using \<open>n = card R\<close> by blast |
1070 qed |
1041 qed |
1071 } |
1042 qed |
1072 thus ?thesis using gr0_implies_Suc[OF \<open>k>0\<close>] by auto |
1043 then show ?thesis |
|
1044 using gr0_implies_Suc[OF \<open>k > 0\<close>] by auto |
1073 qed |
1045 qed |
1074 |
1046 |
1075 lemma relpow_finite_bounded: |
1047 lemma relpow_finite_bounded: |
1076 assumes "finite(R :: ('a*'a)set)" |
1048 fixes R :: "('a \<times> 'a) set" |
1077 shows "R^^k \<subseteq> (UN n:{n. n <= card R}. R^^n)" |
1049 assumes "finite R" |
1078 apply(cases k) |
1050 shows "R^^k \<subseteq> (UN n:{n. n \<le> card R}. R^^n)" |
1079 apply force |
1051 apply (cases k) |
1080 using relpow_finite_bounded1[OF assms, of k] by auto |
1052 apply force |
1081 |
1053 using relpow_finite_bounded1[OF assms, of k] |
1082 lemma rtrancl_finite_eq_relpow: |
1054 apply auto |
1083 "finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)" |
1055 done |
1084 by(fastforce simp: rtrancl_power dest: relpow_finite_bounded) |
1056 |
1085 |
1057 lemma rtrancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>* = (\<Union>n\<in>{n. n \<le> card R}. R^^n)" |
1086 lemma trancl_finite_eq_relpow: |
1058 by (fastforce simp: rtrancl_power dest: relpow_finite_bounded) |
1087 "finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)" |
1059 |
1088 apply(auto simp add: trancl_power) |
1060 lemma trancl_finite_eq_relpow: "finite R \<Longrightarrow> R\<^sup>+ = (\<Union>n\<in>{n. 0 < n \<and> n \<le> card R}. R^^n)" |
1089 apply(auto dest: relpow_finite_bounded1) |
1061 apply (auto simp: trancl_power) |
1090 done |
1062 apply (auto dest: relpow_finite_bounded1) |
|
1063 done |
1091 |
1064 |
1092 lemma finite_relcomp[simp,intro]: |
1065 lemma finite_relcomp[simp,intro]: |
1093 assumes "finite R" and "finite S" |
1066 assumes "finite R" and "finite S" |
1094 shows "finite(R O S)" |
1067 shows "finite (R O S)" |
1095 proof- |
1068 proof- |
1096 have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})" |
1069 have "R O S = (\<Union>(x, y)\<in>R. \<Union>(u, v)\<in>S. if u = y then {(x, v)} else {})" |
1097 by (force simp add: split_def image_constant_conv split: if_splits) |
1070 by (force simp add: split_def image_constant_conv split: if_splits) |
1098 then show ?thesis using assms by clarsimp |
1071 then show ?thesis |
|
1072 using assms by clarsimp |
1099 qed |
1073 qed |
1100 |
1074 |
1101 lemma finite_relpow[simp,intro]: |
1075 lemma finite_relpow [simp, intro]: |
1102 assumes "finite(R :: ('a*'a)set)" shows "n>0 \<Longrightarrow> finite(R^^n)" |
1076 fixes R :: "('a \<times> 'a) set" |
1103 apply(induct n) |
1077 assumes "finite R" |
1104 apply simp |
1078 shows "n > 0 \<Longrightarrow> finite (R^^n)" |
1105 apply(case_tac n) |
1079 apply (induct n) |
1106 apply(simp_all add: assms) |
1080 apply simp |
1107 done |
1081 apply (case_tac n) |
|
1082 apply (simp_all add: assms) |
|
1083 done |
1108 |
1084 |
1109 lemma single_valued_relpow: |
1085 lemma single_valued_relpow: |
1110 fixes R :: "('a * 'a) set" |
1086 fixes R :: "('a \<times> 'a) set" |
1111 shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" |
1087 shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)" |
1112 apply (induct n arbitrary: R) |
1088 apply (induct n arbitrary: R) |
1113 apply simp_all |
1089 apply simp_all |
1114 apply (rule single_valuedI) |
1090 apply (rule single_valuedI) |
1115 apply (fast dest: single_valuedD elim: relpow_Suc_E) |
1091 apply (fast dest: single_valuedD elim: relpow_Suc_E) |
1116 done |
1092 done |
1117 |
1093 |
1118 |
1094 |
1119 subsection \<open>Bounded transitive closure\<close> |
1095 subsection \<open>Bounded transitive closure\<close> |
1120 |
1096 |
1121 definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
1097 definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" |
1122 where |
1098 where "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)" |
1123 "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)" |
1099 |
1124 |
1100 lemma ntrancl_Zero [simp, code]: "ntrancl 0 R = R" |
1125 lemma ntrancl_Zero [simp, code]: |
|
1126 "ntrancl 0 R = R" |
|
1127 proof |
1101 proof |
1128 show "R \<subseteq> ntrancl 0 R" |
1102 show "R \<subseteq> ntrancl 0 R" |
1129 unfolding ntrancl_def by fastforce |
1103 unfolding ntrancl_def by fastforce |
1130 next |
1104 next |
1131 { |
1105 have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" for i |
1132 fix i have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" by auto |
1106 by auto |
1133 } |
1107 then show "ntrancl 0 R \<le> R" |
1134 from this show "ntrancl 0 R \<le> R" |
|
1135 unfolding ntrancl_def by auto |
1108 unfolding ntrancl_def by auto |
1136 qed |
1109 qed |
1137 |
1110 |
1138 lemma ntrancl_Suc [simp]: |
1111 lemma ntrancl_Suc [simp]: "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)" |
1139 "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)" |
|
1140 proof |
1112 proof |
1141 { |
1113 { |
1142 fix a b |
1114 fix a b |
1143 assume "(a, b) \<in> ntrancl (Suc n) R" |
1115 assume "(a, b) \<in> ntrancl (Suc n) R" |
1144 from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i" |
1116 from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i" |
1157 from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R" |
1129 from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R" |
1158 unfolding ntrancl_def by fastforce |
1130 unfolding ntrancl_def by fastforce |
1159 from this c2 show ?thesis by fastforce |
1131 from this c2 show ?thesis by fastforce |
1160 qed |
1132 qed |
1161 } |
1133 } |
1162 from this show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)" |
1134 then show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)" |
1163 by auto |
1135 by auto |
1164 next |
|
1165 show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R" |
1136 show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R" |
1166 unfolding ntrancl_def by fastforce |
1137 unfolding ntrancl_def by fastforce |
1167 qed |
1138 qed |
1168 |
1139 |
1169 lemma [code]: |
1140 lemma [code]: "ntrancl (Suc n) r = (let r' = ntrancl n r in r' \<union> r' O r)" |
1170 "ntrancl (Suc n) r = (let r' = ntrancl n r in r' Un r' O r)" |
1141 by (auto simp: Let_def) |
1171 unfolding Let_def by auto |
1142 |
1172 |
1143 lemma finite_trancl_ntranl: "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R" |
1173 lemma finite_trancl_ntranl: |
|
1174 "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R" |
|
1175 by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def) |
1144 by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def) |
1176 |
1145 |
1177 |
1146 |
1178 subsection \<open>Acyclic relations\<close> |
1147 subsection \<open>Acyclic relations\<close> |
1179 |
1148 |
1180 definition acyclic :: "('a * 'a) set => bool" where |
1149 definition acyclic :: "('a \<times> 'a) set \<Rightarrow> bool" |
1181 "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)" |
1150 where "acyclic r \<longleftrightarrow> (\<forall>x. (x,x) \<notin> r\<^sup>+)" |
1182 |
1151 |
1183 abbreviation acyclicP :: "('a => 'a => bool) => bool" where |
1152 abbreviation acyclicP :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" |
1184 "acyclicP r \<equiv> acyclic {(x, y). r x y}" |
1153 where "acyclicP r \<equiv> acyclic {(x, y). r x y}" |
1185 |
1154 |
1186 lemma acyclic_irrefl [code]: |
1155 lemma acyclic_irrefl [code]: "acyclic r \<longleftrightarrow> irrefl (r\<^sup>+)" |
1187 "acyclic r \<longleftrightarrow> irrefl (r^+)" |
|
1188 by (simp add: acyclic_def irrefl_def) |
1156 by (simp add: acyclic_def irrefl_def) |
1189 |
1157 |
1190 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" |
1158 lemma acyclicI: "\<forall>x. (x, x) \<notin> r\<^sup>+ \<Longrightarrow> acyclic r" |
1191 by (simp add: acyclic_def) |
1159 by (simp add: acyclic_def) |
1192 |
1160 |
1193 lemma (in order) acyclicI_order: |
1161 lemma (in order) acyclicI_order: |
1194 assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a" |
1162 assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a" |
1195 shows "acyclic r" |
1163 shows "acyclic r" |
1196 proof - |
1164 proof - |
1197 { fix a b assume "(a, b) \<in> r\<^sup>+" |
1165 have "f b < f a" if "(a, b) \<in> r\<^sup>+" for a b |
1198 then have "f b < f a" |
1166 using that by induct (auto intro: * less_trans) |
1199 by induct (auto intro: * less_trans) } |
|
1200 then show ?thesis |
1167 then show ?thesis |
1201 by (auto intro!: acyclicI) |
1168 by (auto intro!: acyclicI) |
1202 qed |
1169 qed |
1203 |
1170 |
1204 lemma acyclic_insert [iff]: |
1171 lemma acyclic_insert [iff]: "acyclic (insert (y, x) r) \<longleftrightarrow> acyclic r \<and> (x, y) \<notin> r\<^sup>*" |
1205 "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" |
1172 apply (simp add: acyclic_def trancl_insert) |
1206 apply (simp add: acyclic_def trancl_insert) |
1173 apply (blast intro: rtrancl_trans) |
1207 apply (blast intro: rtrancl_trans) |
1174 done |
1208 done |
1175 |
1209 |
1176 lemma acyclic_converse [iff]: "acyclic (r\<inverse>) \<longleftrightarrow> acyclic r" |
1210 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r" |
1177 by (simp add: acyclic_def trancl_converse) |
1211 by (simp add: acyclic_def trancl_converse) |
|
1212 |
1178 |
1213 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] |
1179 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] |
1214 |
1180 |
1215 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" |
1181 lemma acyclic_impl_antisym_rtrancl: "acyclic r \<Longrightarrow> antisym (r\<^sup>*)" |
1216 apply (simp add: acyclic_def antisym_def) |
1182 apply (simp add: acyclic_def antisym_def) |
1217 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) |
1183 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) |
1218 done |
1184 done |
1219 |
1185 |
1220 (* Other direction: |
1186 (* Other direction: |
1221 acyclic = no loops |
1187 acyclic = no loops |
1222 antisym = only self loops |
1188 antisym = only self loops |
1223 Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id) |
1189 Goalw [acyclic_def,antisym_def] "antisym( r\<^sup>* ) \<Longrightarrow> acyclic(r - Id) |
1224 ==> antisym( r^* ) = acyclic(r - Id)"; |
1190 \<Longrightarrow> antisym( r\<^sup>* ) = acyclic(r - Id)"; |
1225 *) |
1191 *) |
1226 |
1192 |
1227 lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r" |
1193 lemma acyclic_subset: "acyclic s \<Longrightarrow> r \<subseteq> s \<Longrightarrow> acyclic r" |
1228 apply (simp add: acyclic_def) |
1194 unfolding acyclic_def by (blast intro: trancl_mono) |
1229 apply (blast intro: trancl_mono) |
|
1230 done |
|
1231 |
1195 |
1232 |
1196 |
1233 subsection \<open>Setup of transitivity reasoner\<close> |
1197 subsection \<open>Setup of transitivity reasoner\<close> |
1234 |
1198 |
1235 ML \<open> |
1199 ML \<open> |