379 by (rule wf_union_merge [where S = "{}", simplified]) |
379 by (rule wf_union_merge [where S = "{}", simplified]) |
380 |
380 |
381 |
381 |
382 subsection {* Acyclic relations *} |
382 subsection {* Acyclic relations *} |
383 |
383 |
384 definition acyclic :: "('a * 'a) set => bool" where |
|
385 "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)" |
|
386 |
|
387 abbreviation acyclicP :: "('a => 'a => bool) => bool" where |
|
388 "acyclicP r \<equiv> acyclic {(x, y). r x y}" |
|
389 |
|
390 lemma acyclic_irrefl: |
|
391 "acyclic r \<longleftrightarrow> irrefl (r^+)" |
|
392 by (simp add: acyclic_def irrefl_def) |
|
393 |
|
394 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r" |
|
395 by (simp add: acyclic_def) |
|
396 |
|
397 lemma wf_acyclic: "wf r ==> acyclic r" |
384 lemma wf_acyclic: "wf r ==> acyclic r" |
398 apply (simp add: acyclic_def) |
385 apply (simp add: acyclic_def) |
399 apply (blast elim: wf_trancl [THEN wf_irrefl]) |
386 apply (blast elim: wf_trancl [THEN wf_irrefl]) |
400 done |
387 done |
401 |
388 |
402 lemmas wfP_acyclicP = wf_acyclic [to_pred] |
389 lemmas wfP_acyclicP = wf_acyclic [to_pred] |
403 |
|
404 lemma acyclic_insert [iff]: |
|
405 "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)" |
|
406 apply (simp add: acyclic_def trancl_insert) |
|
407 apply (blast intro: rtrancl_trans) |
|
408 done |
|
409 |
|
410 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r" |
|
411 by (simp add: acyclic_def trancl_converse) |
|
412 |
|
413 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred] |
|
414 |
|
415 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)" |
|
416 apply (simp add: acyclic_def antisym_def) |
|
417 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl) |
|
418 done |
|
419 |
|
420 (* Other direction: |
|
421 acyclic = no loops |
|
422 antisym = only self loops |
|
423 Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id) |
|
424 ==> antisym( r^* ) = acyclic(r - Id)"; |
|
425 *) |
|
426 |
|
427 lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r" |
|
428 apply (simp add: acyclic_def) |
|
429 apply (blast intro: trancl_mono) |
|
430 done |
|
431 |
390 |
432 text{* Wellfoundedness of finite acyclic relations*} |
391 text{* Wellfoundedness of finite acyclic relations*} |
433 |
392 |
434 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r" |
393 lemma finite_acyclic_wf [rule_format]: "finite r ==> acyclic r --> wf r" |
435 apply (erule finite_induct, blast) |
394 apply (erule finite_induct, blast) |