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