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