18 |
18 |
19 These postfix operators have \emph{maximum priority}, forcing their |
19 These postfix operators have \emph{maximum priority}, forcing their |
20 operands to be atomic. |
20 operands to be atomic. |
21 *} |
21 *} |
22 |
22 |
23 consts |
23 inductive2 |
24 rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^*)" [1000] 999) |
24 rtrancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_^**)" [1000] 1000) |
25 |
25 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
26 inductive "r^*" |
26 where |
27 intros |
27 rtrancl_refl [intro!, Pure.intro!, simp]: "r^** a a" |
28 rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*" |
28 | rtrancl_into_rtrancl [Pure.intro]: "r^** a b ==> r b c ==> r^** a c" |
29 rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*" |
29 |
30 |
30 inductive2 |
31 consts |
31 trancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" ("(_^++)" [1000] 1000) |
32 trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^+)" [1000] 999) |
32 for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
33 |
33 where |
34 inductive "r^+" |
34 r_into_trancl [intro, Pure.intro]: "r a b ==> r^++ a b" |
35 intros |
35 | trancl_into_trancl [Pure.intro]: "r^++ a b ==> r b c ==> r^++ a c" |
36 r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+" |
36 |
37 trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a,c) : r^+" |
37 constdefs |
|
38 rtrancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^*)" [1000] 999) |
|
39 "r^* == Collect2 (member2 r)^**" |
|
40 |
|
41 trancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^+)" [1000] 999) |
|
42 "r^+ == Collect2 (member2 r)^++" |
38 |
43 |
39 abbreviation |
44 abbreviation |
40 reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where |
45 reflcl :: "('a => 'a => bool) => 'a => 'a => bool" ("(_^==)" [1000] 1000) where |
|
46 "r^== == join r op =" |
|
47 |
|
48 abbreviation |
|
49 reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set" ("(_^=)" [1000] 999) where |
41 "r^= == r \<union> Id" |
50 "r^= == r \<union> Id" |
42 |
51 |
43 notation (xsymbols) |
52 notation (xsymbols) |
44 rtrancl ("(_\<^sup>*)" [1000] 999) and |
53 rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and |
45 trancl ("(_\<^sup>+)" [1000] 999) and |
54 trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and |
46 reflcl ("(_\<^sup>=)" [1000] 999) |
55 reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and |
|
56 rtrancl_set ("(_\<^sup>*)" [1000] 999) and |
|
57 trancl_set ("(_\<^sup>+)" [1000] 999) and |
|
58 reflcl_set ("(_\<^sup>=)" [1000] 999) |
47 |
59 |
48 notation (HTML output) |
60 notation (HTML output) |
49 rtrancl ("(_\<^sup>*)" [1000] 999) and |
61 rtrancl ("(_\<^sup>*\<^sup>*)" [1000] 1000) and |
50 trancl ("(_\<^sup>+)" [1000] 999) and |
62 trancl ("(_\<^sup>+\<^sup>+)" [1000] 1000) and |
51 reflcl ("(_\<^sup>=)" [1000] 999) |
63 reflcl ("(_\<^sup>=\<^sup>=)" [1000] 1000) and |
|
64 rtrancl_set ("(_\<^sup>*)" [1000] 999) and |
|
65 trancl_set ("(_\<^sup>+)" [1000] 999) and |
|
66 reflcl_set ("(_\<^sup>=)" [1000] 999) |
52 |
67 |
53 |
68 |
54 subsection {* Reflexive-transitive closure *} |
69 subsection {* Reflexive-transitive closure *} |
|
70 |
|
71 lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)" |
|
72 by (simp add: rtrancl_set_def) |
|
73 |
|
74 lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)" |
|
75 by (simp add: expand_fun_eq) |
|
76 |
|
77 lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set] |
|
78 lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set] |
55 |
79 |
56 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
80 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*" |
57 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
81 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
58 apply (simp only: split_tupled_all) |
82 apply (simp only: split_tupled_all) |
59 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
83 apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl]) |
60 done |
84 done |
61 |
85 |
62 lemma rtrancl_mono: "r \<subseteq> s ==> r^* \<subseteq> s^*" |
86 lemma r_into_rtrancl' [intro]: "r x y ==> r^** x y" |
|
87 -- {* @{text rtrancl} of @{text r} contains @{text r} *} |
|
88 by (erule rtrancl.rtrancl_refl [THEN rtrancl.rtrancl_into_rtrancl]) |
|
89 |
|
90 lemma rtrancl_mono': "r \<le> s ==> r^** \<le> s^**" |
63 -- {* monotonicity of @{text rtrancl} *} |
91 -- {* monotonicity of @{text rtrancl} *} |
64 apply (rule subsetI) |
92 apply (rule predicate2I) |
65 apply (simp only: split_tupled_all) |
|
66 apply (erule rtrancl.induct) |
93 apply (erule rtrancl.induct) |
67 apply (rule_tac [2] rtrancl_into_rtrancl, blast+) |
94 apply (rule_tac [2] rtrancl.rtrancl_into_rtrancl, blast+) |
68 done |
95 done |
69 |
96 |
70 theorem rtrancl_induct [consumes 1, induct set: rtrancl]: |
97 lemmas rtrancl_mono = rtrancl_mono' [to_set] |
71 assumes a: "(a, b) : r^*" |
98 |
72 and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z" |
99 theorem rtrancl_induct' [consumes 1, induct set: rtrancl]: |
|
100 assumes a: "r^** a b" |
|
101 and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z" |
73 shows "P b" |
102 shows "P b" |
74 proof - |
103 proof - |
75 from a have "a = a --> P b" |
104 from a have "a = a --> P b" |
76 by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ |
105 by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ |
77 thus ?thesis by iprover |
106 thus ?thesis by iprover |
78 qed |
107 qed |
|
108 |
|
109 lemmas rtrancl_induct [consumes 1, induct set: rtrancl_set] = rtrancl_induct' [to_set] |
|
110 |
|
111 lemmas rtrancl_induct2' = |
|
112 rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, |
|
113 consumes 1, case_names refl step] |
79 |
114 |
80 lemmas rtrancl_induct2 = |
115 lemmas rtrancl_induct2 = |
81 rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
116 rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
82 consumes 1, case_names refl step] |
117 consumes 1, case_names refl step] |
83 |
118 |
112 apply (rule subsetI) |
153 apply (rule subsetI) |
113 apply (rule_tac p="x" in PairE, clarify) |
154 apply (rule_tac p="x" in PairE, clarify) |
114 apply (erule rtrancl_induct, auto) |
155 apply (erule rtrancl_induct, auto) |
115 done |
156 done |
116 |
157 |
117 lemma converse_rtrancl_into_rtrancl: |
158 lemma converse_rtrancl_into_rtrancl': |
118 "(a, b) \<in> r \<Longrightarrow> (b, c) \<in> r\<^sup>* \<Longrightarrow> (a, c) \<in> r\<^sup>*" |
159 "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c" |
119 by (rule rtrancl_trans) iprover+ |
160 by (rule rtrancl_trans') iprover+ |
|
161 |
|
162 lemmas converse_rtrancl_into_rtrancl = converse_rtrancl_into_rtrancl' [to_set] |
120 |
163 |
121 text {* |
164 text {* |
122 \medskip More @{term "r^*"} equations and inclusions. |
165 \medskip More @{term "r^*"} equations and inclusions. |
123 *} |
166 *} |
124 |
167 |
125 lemma rtrancl_idemp [simp]: "(r^*)^* = r^*" |
168 lemma rtrancl_idemp' [simp]: "(r^**)^** = r^**" |
126 apply auto |
169 apply (auto intro!: order_antisym) |
127 apply (erule rtrancl_induct) |
170 apply (erule rtrancl_induct') |
128 apply (rule rtrancl_refl) |
171 apply (rule rtrancl.rtrancl_refl) |
129 apply (blast intro: rtrancl_trans) |
172 apply (blast intro: rtrancl_trans') |
130 done |
173 done |
|
174 |
|
175 lemmas rtrancl_idemp [simp] = rtrancl_idemp' [to_set] |
131 |
176 |
132 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" |
177 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*" |
133 apply (rule set_ext) |
178 apply (rule set_ext) |
134 apply (simp only: split_tupled_all) |
179 apply (simp only: split_tupled_all) |
135 apply (blast intro: rtrancl_trans) |
180 apply (blast intro: rtrancl_trans) |
136 done |
181 done |
137 |
182 |
138 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
183 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*" |
139 by (drule rtrancl_mono, simp) |
184 by (drule rtrancl_mono, simp) |
140 |
185 |
141 lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*" |
186 lemma rtrancl_subset': "R \<le> S ==> S \<le> R^** ==> S^** = R^**" |
142 apply (drule rtrancl_mono) |
187 apply (drule rtrancl_mono') |
143 apply (drule rtrancl_mono, simp) |
188 apply (drule rtrancl_mono', simp) |
144 done |
189 done |
145 |
190 |
146 lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*" |
191 lemmas rtrancl_subset = rtrancl_subset' [to_set] |
147 by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD]) |
192 |
148 |
193 lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**" |
149 lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*" |
194 by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D]) |
150 by (blast intro!: rtrancl_subset intro: r_into_rtrancl) |
195 |
|
196 lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set] |
|
197 |
|
198 lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**" |
|
199 by (blast intro!: rtrancl_subset') |
|
200 |
|
201 lemmas rtrancl_reflcl [simp] = rtrancl_reflcl' [to_set] |
151 |
202 |
152 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" |
203 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*" |
153 apply (rule sym) |
204 apply (rule sym) |
154 apply (rule rtrancl_subset, blast, clarify) |
205 apply (rule rtrancl_subset, blast, clarify) |
155 apply (rename_tac a b) |
206 apply (rename_tac a b) |
156 apply (case_tac "a = b", blast) |
207 apply (case_tac "a = b", blast) |
157 apply (blast intro!: r_into_rtrancl) |
208 apply (blast intro!: r_into_rtrancl) |
158 done |
209 done |
159 |
210 |
160 theorem rtrancl_converseD: |
211 lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**" |
161 assumes r: "(x, y) \<in> (r^-1)^*" |
212 apply (rule sym) |
162 shows "(y, x) \<in> r^*" |
213 apply (rule rtrancl_subset') |
|
214 apply blast+ |
|
215 done |
|
216 |
|
217 theorem rtrancl_converseD': |
|
218 assumes r: "(r^--1)^** x y" |
|
219 shows "r^** y x" |
163 proof - |
220 proof - |
164 from r show ?thesis |
221 from r show ?thesis |
165 by induct (iprover intro: rtrancl_trans dest!: converseD)+ |
222 by induct (iprover intro: rtrancl_trans' dest!: conversepD)+ |
166 qed |
223 qed |
167 |
224 |
168 theorem rtrancl_converseI: |
225 lemmas rtrancl_converseD = rtrancl_converseD' [to_set] |
169 assumes r: "(y, x) \<in> r^*" |
226 |
170 shows "(x, y) \<in> (r^-1)^*" |
227 theorem rtrancl_converseI': |
|
228 assumes r: "r^** y x" |
|
229 shows "(r^--1)^** x y" |
171 proof - |
230 proof - |
172 from r show ?thesis |
231 from r show ?thesis |
173 by induct (iprover intro: rtrancl_trans converseI)+ |
232 by induct (iprover intro: rtrancl_trans' conversepI)+ |
174 qed |
233 qed |
|
234 |
|
235 lemmas rtrancl_converseI = rtrancl_converseI' [to_set] |
175 |
236 |
176 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" |
237 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1" |
177 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
238 by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI) |
178 |
239 |
179 lemma sym_rtrancl: "sym r ==> sym (r^*)" |
240 lemma sym_rtrancl: "sym r ==> sym (r^*)" |
180 by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) |
241 by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric]) |
181 |
242 |
182 theorem converse_rtrancl_induct[consumes 1]: |
243 theorem converse_rtrancl_induct'[consumes 1]: |
183 assumes major: "(a, b) : r^*" |
244 assumes major: "r^** a b" |
184 and cases: "P b" "!!y z. [| (y, z) : r; (z, b) : r^*; P z |] ==> P y" |
245 and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y" |
185 shows "P a" |
246 shows "P a" |
186 proof - |
247 proof - |
187 from rtrancl_converseI [OF major] |
248 from rtrancl_converseI' [OF major] |
188 show ?thesis |
249 show ?thesis |
189 by induct (iprover intro: cases dest!: converseD rtrancl_converseD)+ |
250 by induct (iprover intro: cases dest!: conversepD rtrancl_converseD')+ |
190 qed |
251 qed |
|
252 |
|
253 lemmas converse_rtrancl_induct[consumes 1] = converse_rtrancl_induct' [to_set] |
|
254 |
|
255 lemmas converse_rtrancl_induct2' = |
|
256 converse_rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, |
|
257 consumes 1, case_names refl step] |
191 |
258 |
192 lemmas converse_rtrancl_induct2 = |
259 lemmas converse_rtrancl_induct2 = |
193 converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
260 converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
194 consumes 1, case_names refl step] |
261 consumes 1, case_names refl step] |
195 |
262 |
196 lemma converse_rtranclE: |
263 lemma converse_rtranclE': |
197 assumes major: "(x,z):r^*" |
264 assumes major: "r^** x z" |
198 and cases: "x=z ==> P" |
265 and cases: "x=z ==> P" |
199 "!!y. [| (x,y):r; (y,z):r^* |] ==> P" |
266 "!!y. [| r x y; r^** y z |] ==> P" |
200 shows P |
267 shows P |
201 apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)") |
268 apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)") |
202 apply (rule_tac [2] major [THEN converse_rtrancl_induct]) |
269 apply (rule_tac [2] major [THEN converse_rtrancl_induct']) |
203 prefer 2 apply iprover |
270 prefer 2 apply iprover |
204 prefer 2 apply iprover |
271 prefer 2 apply iprover |
205 apply (erule asm_rl exE disjE conjE cases)+ |
272 apply (erule asm_rl exE disjE conjE cases)+ |
206 done |
273 done |
207 |
274 |
208 ML_setup {* |
275 lemmas converse_rtranclE = converse_rtranclE' [to_set] |
209 bind_thm ("converse_rtranclE2", split_rule |
276 |
210 (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE"))); |
277 lemmas converse_rtranclE2' = converse_rtranclE' [of _ "(xa,xb)" "(za,zb)", split_rule] |
211 *} |
278 |
|
279 lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule] |
212 |
280 |
213 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" |
281 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r" |
214 by (blast elim: rtranclE converse_rtranclE |
282 by (blast elim: rtranclE converse_rtranclE |
215 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
283 intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl) |
216 |
284 |
231 |
305 |
232 text {* |
306 text {* |
233 \medskip Conversions between @{text trancl} and @{text rtrancl}. |
307 \medskip Conversions between @{text trancl} and @{text rtrancl}. |
234 *} |
308 *} |
235 |
309 |
236 lemma trancl_into_rtrancl: "(a, b) \<in> r^+ ==> (a, b) \<in> r^*" |
310 lemma trancl_into_rtrancl': "r^++ a b ==> r^** a b" |
237 by (erule trancl.induct) iprover+ |
311 by (erule trancl.induct) iprover+ |
238 |
312 |
239 lemma rtrancl_into_trancl1: assumes r: "(a, b) \<in> r^*" |
313 lemmas trancl_into_rtrancl = trancl_into_rtrancl' [to_set] |
240 shows "!!c. (b, c) \<in> r ==> (a, c) \<in> r^+" using r |
314 |
|
315 lemma rtrancl_into_trancl1': assumes r: "r^** a b" |
|
316 shows "!!c. r b c ==> r^++ a c" using r |
241 by induct iprover+ |
317 by induct iprover+ |
242 |
318 |
243 lemma rtrancl_into_trancl2: "[| (a,b) : r; (b,c) : r^* |] ==> (a,c) : r^+" |
319 lemmas rtrancl_into_trancl1 = rtrancl_into_trancl1' [to_set] |
|
320 |
|
321 lemma rtrancl_into_trancl2': "[| r a b; r^** b c |] ==> r^++ a c" |
244 -- {* intro rule from @{text r} and @{text rtrancl} *} |
322 -- {* intro rule from @{text r} and @{text rtrancl} *} |
245 apply (erule rtranclE, iprover) |
323 apply (erule rtrancl.cases, iprover) |
246 apply (rule rtrancl_trans [THEN rtrancl_into_trancl1]) |
324 apply (rule rtrancl_trans' [THEN rtrancl_into_trancl1']) |
247 apply (assumption | rule r_into_rtrancl)+ |
325 apply (simp | rule r_into_rtrancl')+ |
248 done |
326 done |
249 |
327 |
250 lemma trancl_induct [consumes 1, induct set: trancl]: |
328 lemmas rtrancl_into_trancl2 = rtrancl_into_trancl2' [to_set] |
251 assumes a: "(a,b) : r^+" |
329 |
252 and cases: "!!y. (a, y) : r ==> P y" |
330 lemma trancl_induct' [consumes 1, induct set: trancl]: |
253 "!!y z. (a,y) : r^+ ==> (y, z) : r ==> P y ==> P z" |
331 assumes a: "r^++ a b" |
|
332 and cases: "!!y. r a y ==> P y" |
|
333 "!!y z. r^++ a y ==> r y z ==> P y ==> P z" |
254 shows "P b" |
334 shows "P b" |
255 -- {* Nice induction rule for @{text trancl} *} |
335 -- {* Nice induction rule for @{text trancl} *} |
256 proof - |
336 proof - |
257 from a have "a = a --> P b" |
337 from a have "a = a --> P b" |
258 by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ |
338 by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+ |
259 thus ?thesis by iprover |
339 thus ?thesis by iprover |
260 qed |
340 qed |
261 |
341 |
|
342 lemmas trancl_induct [consumes 1, induct set: trancl_set] = trancl_induct' [to_set] |
|
343 |
|
344 lemmas trancl_induct2' = |
|
345 trancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule, |
|
346 consumes 1, case_names base step] |
|
347 |
262 lemmas trancl_induct2 = |
348 lemmas trancl_induct2 = |
263 trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
349 trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete), |
264 consumes 1, case_names base step] |
350 consumes 1, case_names base step] |
265 |
351 |
266 lemma trancl_trans_induct: |
352 lemma trancl_trans_induct': |
267 assumes major: "(x,y) : r^+" |
353 assumes major: "r^++ x y" |
268 and cases: "!!x y. (x,y) : r ==> P x y" |
354 and cases: "!!x y. r x y ==> P x y" |
269 "!!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z" |
355 "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z" |
270 shows "P x y" |
356 shows "P x y" |
271 -- {* Another induction rule for trancl, incorporating transitivity *} |
357 -- {* Another induction rule for trancl, incorporating transitivity *} |
272 by (iprover intro: r_into_trancl major [THEN trancl_induct] cases) |
358 by (iprover intro: major [THEN trancl_induct'] cases) |
273 |
359 |
274 inductive_cases tranclE: "(a, b) : r^+" |
360 lemmas trancl_trans_induct = trancl_trans_induct' [to_set] |
|
361 |
|
362 lemma tranclE: |
|
363 assumes H: "(a, b) : r^+" |
|
364 and cases: "(a, b) : r ==> P" "\<And>c. (a, c) : r^+ ==> (c, b) : r ==> P" |
|
365 shows P |
|
366 using H [simplified trancl_set_def, simplified] |
|
367 by cases (auto intro: cases [simplified trancl_set_def, simplified]) |
275 |
368 |
276 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s" |
369 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s" |
277 apply (rule subsetI) |
370 apply (rule subsetI) |
278 apply (rule_tac p="x" in PairE, clarify) |
371 apply (rule_tac p="x" in PairE, clarify) |
279 apply (erule trancl_induct, auto) |
372 apply (erule trancl_induct, auto) |
291 thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+ |
384 thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+ |
292 qed |
385 qed |
293 |
386 |
294 lemmas trancl_trans = trans_trancl [THEN transD, standard] |
387 lemmas trancl_trans = trans_trancl [THEN transD, standard] |
295 |
388 |
|
389 lemma trancl_trans': |
|
390 assumes xy: "r^++ x y" |
|
391 and yz: "r^++ y z" |
|
392 shows "r^++ x z" using yz xy |
|
393 by induct iprover+ |
|
394 |
296 lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r" |
395 lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r" |
297 apply(auto) |
396 apply(auto) |
298 apply(erule trancl_induct) |
397 apply(erule trancl_induct) |
299 apply assumption |
398 apply assumption |
300 apply(unfold trans_def) |
399 apply(unfold trans_def) |
301 apply(blast) |
400 apply(blast) |
302 done |
401 done |
303 |
402 |
304 lemma rtrancl_trancl_trancl: assumes r: "(x, y) \<in> r^*" |
403 lemma rtrancl_trancl_trancl': assumes r: "r^** x y" |
305 shows "!!z. (y, z) \<in> r^+ ==> (x, z) \<in> r^+" using r |
404 shows "!!z. r^++ y z ==> r^++ x z" using r |
306 by induct (iprover intro: trancl_trans)+ |
405 by induct (iprover intro: trancl_trans')+ |
307 |
406 |
308 lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+" |
407 lemmas rtrancl_trancl_trancl = rtrancl_trancl_trancl' [to_set] |
309 by (erule transD [OF trans_trancl r_into_trancl]) |
408 |
|
409 lemma trancl_into_trancl2': "r a b ==> r^++ b c ==> r^++ a c" |
|
410 by (erule trancl_trans' [OF trancl.r_into_trancl]) |
|
411 |
|
412 lemmas trancl_into_trancl2 = trancl_into_trancl2' [to_set] |
310 |
413 |
311 lemma trancl_insert: |
414 lemma trancl_insert: |
312 "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" |
415 "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}" |
313 -- {* primitive recursion for @{text trancl} over finite relations *} |
416 -- {* primitive recursion for @{text trancl} over finite relations *} |
314 apply (rule equalityI) |
417 apply (rule equalityI) |
319 apply (rule subsetI) |
422 apply (rule subsetI) |
320 apply (blast intro: trancl_mono rtrancl_mono |
423 apply (blast intro: trancl_mono rtrancl_mono |
321 [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
424 [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2) |
322 done |
425 done |
323 |
426 |
324 lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x, y) \<in> (r^-1)^+" |
427 lemma trancl_converseI': "(r^++)^--1 x y ==> (r^--1)^++ x y" |
325 apply (drule converseD) |
428 apply (drule conversepD) |
326 apply (erule trancl.induct) |
429 apply (erule trancl_induct') |
327 apply (iprover intro: converseI trancl_trans)+ |
430 apply (iprover intro: conversepI trancl_trans')+ |
328 done |
431 done |
329 |
432 |
330 lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1" |
433 lemmas trancl_converseI = trancl_converseI' [to_set] |
331 apply (rule converseI) |
434 |
332 apply (erule trancl.induct) |
435 lemma trancl_converseD': "(r^--1)^++ x y ==> (r^++)^--1 x y" |
333 apply (iprover dest: converseD intro: trancl_trans)+ |
436 apply (rule conversepI) |
334 done |
437 apply (erule trancl_induct') |
335 |
438 apply (iprover dest: conversepD intro: trancl_trans')+ |
336 lemma trancl_converse: "(r^-1)^+ = (r^+)^-1" |
439 done |
337 by (fastsimp simp add: split_tupled_all |
440 |
338 intro!: trancl_converseI trancl_converseD) |
441 lemmas trancl_converseD = trancl_converseD' [to_set] |
|
442 |
|
443 lemma trancl_converse': "(r^--1)^++ = (r^++)^--1" |
|
444 by (fastsimp simp add: expand_fun_eq |
|
445 intro!: trancl_converseI' dest!: trancl_converseD') |
|
446 |
|
447 lemmas trancl_converse = trancl_converse' [to_set] |
339 |
448 |
340 lemma sym_trancl: "sym r ==> sym (r^+)" |
449 lemma sym_trancl: "sym r ==> sym (r^+)" |
341 by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) |
450 by (simp only: sym_conv_converse_eq trancl_converse [symmetric]) |
342 |
451 |
343 lemma converse_trancl_induct: |
452 lemma converse_trancl_induct': |
344 assumes major: "(a,b) : r^+" |
453 assumes major: "r^++ a b" |
345 and cases: "!!y. (y,b) : r ==> P(y)" |
454 and cases: "!!y. r y b ==> P(y)" |
346 "!!y z.[| (y,z) : r; (z,b) : r^+; P(z) |] ==> P(y)" |
455 "!!y z.[| r y z; r^++ z b; P(z) |] ==> P(y)" |
347 shows "P a" |
456 shows "P a" |
348 apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]]) |
457 apply (rule trancl_induct' [OF trancl_converseI', OF conversepI, OF major]) |
349 apply (rule cases) |
458 apply (rule cases) |
350 apply (erule converseD) |
459 apply (erule conversepD) |
351 apply (blast intro: prems dest!: trancl_converseD) |
460 apply (blast intro: prems dest!: trancl_converseD' conversepD) |
352 done |
461 done |
353 |
462 |
354 lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*" |
463 lemmas converse_trancl_induct = converse_trancl_induct' [to_set] |
355 apply (erule converse_trancl_induct, auto) |
464 |
356 apply (blast intro: rtrancl_trans) |
465 lemma tranclD': "R^++ x y ==> EX z. R x z \<and> R^** z y" |
357 done |
466 apply (erule converse_trancl_induct', auto) |
|
467 apply (blast intro: rtrancl_trans') |
|
468 done |
|
469 |
|
470 lemmas tranclD = tranclD' [to_set] |
358 |
471 |
359 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" |
472 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+" |
360 by (blast elim: tranclE dest: trancl_into_rtrancl) |
473 by (blast elim: tranclE dest: trancl_into_rtrancl) |
361 |
474 |
362 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y" |
475 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y" |
448 apply (erule trancl_induct) |
565 apply (erule trancl_induct) |
449 apply (fast intro: r_r_into_trancl) |
566 apply (fast intro: r_r_into_trancl) |
450 apply (fast intro: r_r_into_trancl trancl_trans) |
567 apply (fast intro: r_r_into_trancl trancl_trans) |
451 done |
568 done |
452 |
569 |
453 lemma trancl_rtrancl_trancl: |
570 lemma trancl_rtrancl_trancl': |
454 "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r\<^sup>* ==> (a, c) \<in> r\<^sup>+" |
571 "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c" |
455 apply (drule tranclD) |
572 apply (drule tranclD') |
456 apply (erule exE, erule conjE) |
573 apply (erule exE, erule conjE) |
457 apply (drule rtrancl_trans, assumption) |
574 apply (drule rtrancl_trans', assumption) |
458 apply (drule rtrancl_into_trancl2, assumption, assumption) |
575 apply (drule rtrancl_into_trancl2', assumption, assumption) |
459 done |
576 done |
|
577 |
|
578 lemmas trancl_rtrancl_trancl = trancl_rtrancl_trancl' [to_set] |
460 |
579 |
461 lemmas transitive_closure_trans [trans] = |
580 lemmas transitive_closure_trans [trans] = |
462 r_r_into_trancl trancl_trans rtrancl_trans |
581 r_r_into_trancl trancl_trans rtrancl_trans |
463 trancl_into_trancl trancl_into_trancl2 |
582 trancl_into_trancl trancl_into_trancl2 |
464 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
583 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl |
465 rtrancl_trancl_trancl trancl_rtrancl_trancl |
584 rtrancl_trancl_trancl trancl_rtrancl_trancl |
466 |
585 |
|
586 lemmas transitive_closure_trans' [trans] = |
|
587 trancl_trans' rtrancl_trans' |
|
588 trancl.trancl_into_trancl trancl_into_trancl2' |
|
589 rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl' |
|
590 rtrancl_trancl_trancl' trancl_rtrancl_trancl' |
|
591 |
467 declare trancl_into_rtrancl [elim] |
592 declare trancl_into_rtrancl [elim] |
468 |
593 |
469 declare rtranclE [cases set: rtrancl] |
594 declare rtranclE [cases set: rtrancl_set] |
470 declare tranclE [cases set: trancl] |
595 declare tranclE [cases set: trancl_set] |
471 |
596 |
472 |
597 |
473 |
598 |
474 |
599 |
475 |
600 |
488 val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl"; |
613 val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl"; |
489 val rtrancl_trans = thm "rtrancl_trans"; |
614 val rtrancl_trans = thm "rtrancl_trans"; |
490 |
615 |
491 fun decomp (Trueprop $ t) = |
616 fun decomp (Trueprop $ t) = |
492 let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = |
617 let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) = |
493 let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") |
618 let fun decr (Const ("Transitive_Closure.rtrancl_set", _ ) $ r) = (r,"r*") |
494 | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") |
619 | decr (Const ("Transitive_Closure.trancl_set", _ ) $ r) = (r,"r+") |
495 | decr r = (r,"r"); |
620 | decr r = (r,"r"); |
496 val (rel,r) = decr rel; |
621 val (rel,r) = decr rel; |
497 in SOME (a,b,rel,r) end |
622 in SOME (a,b,rel,r) end |
498 | dec _ = NONE |
623 | dec _ = NONE |
499 in dec t end; |
624 in dec t end; |
500 |
625 |
501 end); |
626 end); |
502 |
627 |
|
628 structure Tranclp_Tac = Trancl_Tac_Fun ( |
|
629 struct |
|
630 val r_into_trancl = thm "trancl.r_into_trancl"; |
|
631 val trancl_trans = thm "trancl_trans'"; |
|
632 val rtrancl_refl = thm "rtrancl.rtrancl_refl"; |
|
633 val r_into_rtrancl = thm "r_into_rtrancl'"; |
|
634 val trancl_into_rtrancl = thm "trancl_into_rtrancl'"; |
|
635 val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl'"; |
|
636 val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl'"; |
|
637 val rtrancl_trans = thm "rtrancl_trans'"; |
|
638 |
|
639 fun decomp (Trueprop $ t) = |
|
640 let fun dec (rel $ a $ b) = |
|
641 let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*") |
|
642 | decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+") |
|
643 | decr r = (r,"r"); |
|
644 val (rel,r) = decr rel; |
|
645 in SOME (a, b, Envir.beta_eta_contract rel, r) end |
|
646 | dec _ = NONE |
|
647 in dec t end; |
|
648 |
|
649 end); |
|
650 |
503 change_simpset (fn ss => ss |
651 change_simpset (fn ss => ss |
504 addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) |
652 addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac)) |
505 addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))); |
653 addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)) |
|
654 addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac)) |
|
655 addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac))); |
506 |
656 |
507 *} |
657 *} |
508 |
658 |
509 (* Optional methods *) |
659 (* Optional methods *) |
510 |
660 |