nipkow@10213: (*  Title:      HOL/Transitive_Closure.thy
nipkow@10213:     ID:         $Id$
nipkow@10213:     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
nipkow@10213:     Copyright   1992  University of Cambridge
nipkow@10213: 
nipkow@10213: Relfexive and Transitive closure of a relation
nipkow@10213: 
nipkow@10213: rtrancl is reflexive/transitive closure;
nipkow@10213: trancl  is transitive closure
nipkow@10213: reflcl  is reflexive closure
nipkow@10213: 
wenzelm@10331: These postfix operators have MAXIMUM PRIORITY, forcing their operands
wenzelm@10331: to be atomic.
nipkow@10213: *)
nipkow@10213: 
wenzelm@10980: theory Transitive_Closure = Lfp + Relation
wenzelm@10980: files ("Transitive_Closure_lemmas.ML"):
nipkow@10213: 
nipkow@10213: constdefs
wenzelm@10331:   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
wenzelm@10331:   "r^* == lfp (%s. Id Un (r O s))"
nipkow@10213: 
wenzelm@10331:   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
wenzelm@10331:   "r^+ ==  r O rtrancl r"
nipkow@10213: 
nipkow@10213: syntax
wenzelm@10331:   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
nipkow@10213: translations
nipkow@10213:   "r^=" == "r Un Id"
nipkow@10213: 
wenzelm@10827: syntax (xsymbols)
wenzelm@10331:   rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
wenzelm@10331:   trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
wenzelm@10331:   "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
wenzelm@10331: 
wenzelm@10980: use "Transitive_Closure_lemmas.ML"
wenzelm@10980: 
nipkow@10996: 
wenzelm@11090: lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
wenzelm@11084:   apply safe
wenzelm@11084:   apply (erule trancl_into_rtrancl)
wenzelm@11084:   apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
wenzelm@11084:   done
nipkow@10996: 
wenzelm@11090: lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
wenzelm@11084:   apply safe
wenzelm@11084:    apply (drule trancl_into_rtrancl)
wenzelm@11084:    apply simp
wenzelm@11084:   apply (erule rtranclE)
wenzelm@11084:    apply safe
wenzelm@11084:    apply (rule r_into_trancl)
wenzelm@11084:    apply simp
wenzelm@11084:   apply (rule rtrancl_into_trancl1)
wenzelm@11084:    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
wenzelm@11084:   apply fast
wenzelm@11084:   done
nipkow@10996: 
wenzelm@11090: lemma trancl_empty [simp]: "{}^+ = {}"
wenzelm@11084:   by (auto elim: trancl_induct)
nipkow@10996: 
wenzelm@11090: lemma rtrancl_empty [simp]: "{}^* = Id"
wenzelm@11084:   by (rule subst [OF reflcl_trancl]) simp
nipkow@10996: 
wenzelm@11090: lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
wenzelm@11084:   by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
wenzelm@11084: 
nipkow@10996: 
nipkow@10996: (* should be merged with the main body of lemmas: *)
nipkow@10996: 
wenzelm@11090: lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
wenzelm@11084:   by blast
nipkow@10996: 
wenzelm@11090: lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
wenzelm@11084:   by blast
nipkow@10996: 
wenzelm@11090: lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
wenzelm@11084:   by (rule rtrancl_Un_rtrancl [THEN subst]) fast
nipkow@10996: 
wenzelm@11090: lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
wenzelm@11084:   by (blast intro: subsetD [OF rtrancl_Un_subset])
nipkow@10996: 
wenzelm@11090: lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
wenzelm@11084:   by (unfold Domain_def) (blast dest: tranclD)
nipkow@10996: 
wenzelm@11090: lemma trancl_range [simp]: "Range (r^+) = Range r"
wenzelm@11084:   by (simp add: Range_def trancl_converse [symmetric])
nipkow@10996: 
nipkow@10213: end