src/HOL/Transitive_Closure.thy
author nipkow
Thu Dec 20 18:22:44 2001 +0100 (2001-12-20)
changeset 12566 fe20540bcf93
parent 12428 f3033eed309a
child 12691 d21db58bcdc2
permissions -rw-r--r--
renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
     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 = Inductive
    17 files ("Transitive_Closure_lemmas.ML"):
    18 
    19 consts
    20   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    21 
    22 inductive "r^*"
    23 intros
    24   rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    25   rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
    26 
    27 constdefs
    28   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    29   "r^+ ==  r O rtrancl r"
    30 
    31 syntax
    32   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    33 translations
    34   "r^=" == "r Un Id"
    35 
    36 syntax (xsymbols)
    37   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    38   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    39   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    40 
    41 use "Transitive_Closure_lemmas.ML"
    42 
    43 
    44 lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
    45   apply safe
    46   apply (erule trancl_into_rtrancl)
    47   apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    48   done
    49 
    50 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
    51   apply safe
    52    apply (drule trancl_into_rtrancl)
    53    apply simp
    54   apply (erule rtranclE)
    55    apply safe
    56    apply (rule r_into_trancl)
    57    apply simp
    58   apply (rule rtrancl_into_trancl1)
    59    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
    60   apply fast
    61   done
    62 
    63 lemma trancl_empty [simp]: "{}^+ = {}"
    64   by (auto elim: trancl_induct)
    65 
    66 lemma rtrancl_empty [simp]: "{}^* = Id"
    67   by (rule subst [OF reflcl_trancl]) simp
    68 
    69 lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
    70   by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
    71 
    72 
    73 (* should be merged with the main body of lemmas: *)
    74 
    75 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
    76   by blast
    77 
    78 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
    79   by blast
    80 
    81 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
    82   by (rule rtrancl_Un_rtrancl [THEN subst]) fast
    83 
    84 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
    85   by (blast intro: subsetD [OF rtrancl_Un_subset])
    86 
    87 lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
    88   by (unfold Domain_def) (blast dest: tranclD)
    89 
    90 lemma trancl_range [simp]: "Range (r^+) = Range r"
    91   by (simp add: Range_def trancl_converse [symmetric])
    92 
    93 lemma Not_Domain_rtrancl:
    94 	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
    95  apply (auto)
    96  by (erule rev_mp, erule rtrancl_induct, auto)
    97 
    98 (* more about converse rtrancl and trancl, should be merged with main body *)
    99 
   100 lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
   101   by (fast intro: trancl_trans)
   102 
   103 lemma trancl_into_trancl [rule_format]:
   104   "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+"
   105   apply (erule trancl_induct)   
   106    apply (fast intro: r_r_into_trancl)
   107   apply (fast intro: r_r_into_trancl trancl_trans)
   108   done
   109 
   110 lemma trancl_rtrancl_trancl:
   111   "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+"
   112   apply (drule tranclD)
   113   apply (erule exE, erule conjE)
   114   apply (drule rtrancl_trans, assumption)
   115   apply (drule rtrancl_into_trancl2, assumption)
   116   apply assumption
   117   done
   118 
   119 lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
   120                  trancl_into_trancl trancl_into_trancl2
   121                  rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   122                  rtrancl_trancl_trancl trancl_rtrancl_trancl
   123 
   124 declare trancl_into_rtrancl [elim]
   125 
   126 declare rtrancl_induct [induct set: rtrancl]
   127 declare rtranclE [cases set: rtrancl]
   128 declare trancl_induct [induct set: trancl]
   129 declare tranclE [cases set: trancl]
   130 
   131 end