src/HOL/Transitive_Closure.thy
author wenzelm
Fri Feb 09 23:48:50 2001 +0100 (2001-02-09)
changeset 11090 3041d0347d26
parent 11084 32c1deea5bcd
child 11115 285b31e9e026
permissions -rw-r--r--
tuned;
     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^+)^= = r^*"
    40   apply safe
    41   apply (erule trancl_into_rtrancl)
    42   apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    43   done
    44 
    45 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
    46   apply safe
    47    apply (drule trancl_into_rtrancl)
    48    apply simp
    49   apply (erule rtranclE)
    50    apply safe
    51    apply (rule r_into_trancl)
    52    apply simp
    53   apply (rule rtrancl_into_trancl1)
    54    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
    55   apply fast
    56   done
    57 
    58 lemma trancl_empty [simp]: "{}^+ = {}"
    59   by (auto elim: trancl_induct)
    60 
    61 lemma rtrancl_empty [simp]: "{}^* = Id"
    62   by (rule subst [OF reflcl_trancl]) simp
    63 
    64 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
    65   by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
    66 
    67 
    68 (* should be merged with the main body of lemmas: *)
    69 
    70 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
    71   by blast
    72 
    73 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
    74   by blast
    75 
    76 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
    77   by (rule rtrancl_Un_rtrancl [THEN subst]) fast
    78 
    79 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
    80   by (blast intro: subsetD [OF rtrancl_Un_subset])
    81 
    82 lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
    83   by (unfold Domain_def) (blast dest: tranclD)
    84 
    85 lemma trancl_range [simp]: "Range (r^+) = Range r"
    86   by (simp add: Range_def trancl_converse [symmetric])
    87 
    88 end