src/HOL/Transitive_Closure.thy
author wenzelm
Fri Feb 09 11:40:10 2001 +0100 (2001-02-09)
changeset 11084 32c1deea5bcd
parent 10996 74e970389def
child 11090 3041d0347d26
permissions -rw-r--r--
unsymbolized;
tuned;
nipkow@10213
     1
(*  Title:      HOL/Transitive_Closure.thy
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213
     4
    Copyright   1992  University of Cambridge
nipkow@10213
     5
nipkow@10213
     6
Relfexive and Transitive closure of a relation
nipkow@10213
     7
nipkow@10213
     8
rtrancl is reflexive/transitive closure;
nipkow@10213
     9
trancl  is transitive closure
nipkow@10213
    10
reflcl  is reflexive closure
nipkow@10213
    11
wenzelm@10331
    12
These postfix operators have MAXIMUM PRIORITY, forcing their operands
wenzelm@10331
    13
to be atomic.
nipkow@10213
    14
*)
nipkow@10213
    15
wenzelm@10980
    16
theory Transitive_Closure = Lfp + Relation
wenzelm@10980
    17
files ("Transitive_Closure_lemmas.ML"):
nipkow@10213
    18
nipkow@10213
    19
constdefs
wenzelm@10331
    20
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
wenzelm@10331
    21
  "r^* == lfp (%s. Id Un (r O s))"
nipkow@10213
    22
wenzelm@10331
    23
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
wenzelm@10331
    24
  "r^+ ==  r O rtrancl r"
nipkow@10213
    25
nipkow@10213
    26
syntax
wenzelm@10331
    27
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
nipkow@10213
    28
translations
nipkow@10213
    29
  "r^=" == "r Un Id"
nipkow@10213
    30
wenzelm@10827
    31
syntax (xsymbols)
wenzelm@10331
    32
  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
wenzelm@10331
    33
  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
wenzelm@10331
    34
  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
wenzelm@10331
    35
wenzelm@10980
    36
use "Transitive_Closure_lemmas.ML"
wenzelm@10980
    37
nipkow@10996
    38
wenzelm@11084
    39
lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
wenzelm@11084
    40
  apply safe
wenzelm@11084
    41
  apply (erule trancl_into_rtrancl)
wenzelm@11084
    42
  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
wenzelm@11084
    43
  done
nipkow@10996
    44
wenzelm@11084
    45
lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
wenzelm@11084
    46
  apply safe
wenzelm@11084
    47
   apply (drule trancl_into_rtrancl)
wenzelm@11084
    48
   apply simp
wenzelm@11084
    49
  apply (erule rtranclE)
wenzelm@11084
    50
   apply safe
wenzelm@11084
    51
   apply (rule r_into_trancl)
wenzelm@11084
    52
   apply simp
wenzelm@11084
    53
  apply (rule rtrancl_into_trancl1)
wenzelm@11084
    54
   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
wenzelm@11084
    55
  apply fast
wenzelm@11084
    56
  done
nipkow@10996
    57
wenzelm@11084
    58
lemma trancl_empty [simp]: "{}\<^sup>+ = {}"
wenzelm@11084
    59
  by (auto elim: trancl_induct)
nipkow@10996
    60
wenzelm@11084
    61
lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
wenzelm@11084
    62
  by (rule subst [OF reflcl_trancl]) simp
nipkow@10996
    63
wenzelm@11084
    64
lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+"
wenzelm@11084
    65
  by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
wenzelm@11084
    66
nipkow@10996
    67
nipkow@10996
    68
(* should be merged with the main body of lemmas: *)
nipkow@10996
    69
wenzelm@11084
    70
lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV"
wenzelm@11084
    71
  by blast
nipkow@10996
    72
wenzelm@11084
    73
lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV"
wenzelm@11084
    74
  by blast
nipkow@10996
    75
nipkow@10996
    76
lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
wenzelm@11084
    77
  by (rule rtrancl_Un_rtrancl [THEN subst]) fast
nipkow@10996
    78
wenzelm@11084
    79
lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*"
wenzelm@11084
    80
  by (blast intro: subsetD [OF rtrancl_Un_subset])
nipkow@10996
    81
nipkow@10996
    82
lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
wenzelm@11084
    83
  by (unfold Domain_def) (blast dest: tranclD)
nipkow@10996
    84
nipkow@10996
    85
lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
wenzelm@11084
    86
  by (simp add: Range_def trancl_converse [symmetric])
nipkow@10996
    87
nipkow@10213
    88
end