src/HOL/Transitive_Closure.thy
changeset 12691 d21db58bcdc2
parent 12566 fe20540bcf93
child 12823 9d3f5056296b
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 09 17:42:49 2002 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 09 17:48:40 2002 +0100
     1.3 @@ -2,48 +2,394 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8 -Relfexive and Transitive closure of a relation
     1.9 -
    1.10 -rtrancl is reflexive/transitive closure;
    1.11 -trancl  is transitive closure
    1.12 -reflcl  is reflexive closure
    1.13 -
    1.14 -These postfix operators have MAXIMUM PRIORITY, forcing their operands
    1.15 -to be atomic.
    1.16  *)
    1.17  
    1.18 -theory Transitive_Closure = Inductive
    1.19 -files ("Transitive_Closure_lemmas.ML"):
    1.20 +header {* Reflexive and Transitive closure of a relation *}
    1.21 +
    1.22 +theory Transitive_Closure = Inductive:
    1.23 +
    1.24 +text {*
    1.25 +  @{text rtrancl} is reflexive/transitive closure,
    1.26 +  @{text trancl} is transitive closure,
    1.27 +  @{text reflcl} is reflexive closure.
    1.28 +
    1.29 +  These postfix operators have \emph{maximum priority}, forcing their
    1.30 +  operands to be atomic.
    1.31 +*}
    1.32  
    1.33  consts
    1.34 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^*)" [1000] 999)
    1.35 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
    1.36  
    1.37  inductive "r^*"
    1.38 -intros
    1.39 -  rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    1.40 -  rtrancl_into_rtrancl:        "[| (a,b) : r^*; (b,c) : r |] ==> (a,c) : r^*"
    1.41 +  intros
    1.42 +    rtrancl_refl [intro!, simp]: "(a, a) : r^*"
    1.43 +    rtrancl_into_rtrancl: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
    1.44  
    1.45  constdefs
    1.46 -  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_^+)" [1000] 999)
    1.47 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    1.48    "r^+ ==  r O rtrancl r"
    1.49  
    1.50  syntax
    1.51 -  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_^=)" [1000] 999)
    1.52 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^=)" [1000] 999)
    1.53  translations
    1.54 -  "r^=" == "r Un Id"
    1.55 +  "r^=" == "r \<union> Id"
    1.56  
    1.57  syntax (xsymbols)
    1.58 -  rtrancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    1.59 -  trancl :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    1.60 -  "_reflcl" :: "('a * 'a) set => ('a * 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    1.61 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>*)" [1000] 999)
    1.62 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>+)" [1000] 999)
    1.63 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    1.64 +
    1.65 +
    1.66 +subsection {* Reflexive-transitive closure *}
    1.67 +
    1.68 +lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    1.69 +  -- {* @{text rtrancl} of @{text r} contains @{text r} *}
    1.70 +  apply (simp only: split_tupled_all)
    1.71 +  apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
    1.72 +  done
    1.73 +
    1.74 +lemma rtrancl_mono: "r \<subseteq> s ==> r^* \<subseteq> s^*"
    1.75 +  -- {* monotonicity of @{text rtrancl} *}
    1.76 +  apply (rule subsetI)
    1.77 +  apply (simp only: split_tupled_all)
    1.78 +  apply (erule rtrancl.induct)
    1.79 +   apply (rule_tac [2] rtrancl_into_rtrancl)
    1.80 +    apply blast+
    1.81 +  done
    1.82 +
    1.83 +theorem rtrancl_induct [consumes 1]:
    1.84 +  (assumes a: "(a, b) : r^*"
    1.85 +    and cases: "P a" "!!y z. [| (a, y) : r^*; (y, z) : r; P y |] ==> P z")
    1.86 +  "P b"
    1.87 +proof -
    1.88 +  from a have "a = a --> P b"
    1.89 +    by (induct "%x y. x = a --> P y" a b rule: rtrancl.induct)
    1.90 +      (rules intro: cases)+
    1.91 +  thus ?thesis by rules
    1.92 +qed
    1.93 +
    1.94 +ML_setup {*
    1.95 +  bind_thm ("rtrancl_induct2", split_rule
    1.96 +    (read_instantiate [("a","(ax,ay)"), ("b","(bx,by)")] (thm "rtrancl_induct")));
    1.97 +*}
    1.98 +
    1.99 +lemma trans_rtrancl: "trans(r^*)"
   1.100 +  -- {* transitivity of transitive closure!! -- by induction *}
   1.101 +  apply (unfold trans_def)
   1.102 +  apply safe
   1.103 +  apply (erule_tac b = z in rtrancl_induct)
   1.104 +   apply (blast intro: rtrancl_into_rtrancl)+
   1.105 +  done
   1.106 +
   1.107 +lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   1.108 +
   1.109 +lemma rtranclE:
   1.110 +  "[| (a::'a,b) : r^*;  (a = b) ==> P;
   1.111 +      !!y.[| (a,y) : r^*; (y,b) : r |] ==> P
   1.112 +   |] ==> P"
   1.113 +  -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
   1.114 +proof -
   1.115 +  assume major: "(a::'a,b) : r^*"
   1.116 +  case rule_context
   1.117 +  show ?thesis
   1.118 +    apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
   1.119 +     apply (rule_tac [2] major [THEN rtrancl_induct])
   1.120 +      prefer 2 apply (blast!)
   1.121 +      prefer 2 apply (blast!)
   1.122 +    apply (erule asm_rl exE disjE conjE prems)+
   1.123 +    done
   1.124 +qed
   1.125 +
   1.126 +lemmas converse_rtrancl_into_rtrancl = r_into_rtrancl [THEN rtrancl_trans, standard]
   1.127 +
   1.128 +text {*
   1.129 +  \medskip More @{term "r^*"} equations and inclusions.
   1.130 +*}
   1.131 +
   1.132 +lemma rtrancl_idemp [simp]: "(r^*)^* = r^*"
   1.133 +  apply auto
   1.134 +  apply (erule rtrancl_induct)
   1.135 +   apply (rule rtrancl_refl)
   1.136 +  apply (blast intro: rtrancl_trans)
   1.137 +  done
   1.138 +
   1.139 +lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
   1.140 +  apply (rule set_ext)
   1.141 +  apply (simp only: split_tupled_all)
   1.142 +  apply (blast intro: rtrancl_trans)
   1.143 +  done
   1.144 +
   1.145 +lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
   1.146 +  apply (drule rtrancl_mono)
   1.147 +  apply simp
   1.148 +  done
   1.149 +
   1.150 +lemma rtrancl_subset: "R \<subseteq> S ==> S \<subseteq> R^* ==> S^* = R^*"
   1.151 +  apply (drule rtrancl_mono)
   1.152 +  apply (drule rtrancl_mono)
   1.153 +  apply simp
   1.154 +  apply blast
   1.155 +  done
   1.156 +
   1.157 +lemma rtrancl_Un_rtrancl: "(R^* \<union> S^*)^* = (R \<union> S)^*"
   1.158 +  by (blast intro!: rtrancl_subset intro: r_into_rtrancl rtrancl_mono [THEN subsetD])
   1.159 +
   1.160 +lemma rtrancl_reflcl [simp]: "(R^=)^* = R^*"
   1.161 +  by (blast intro!: rtrancl_subset intro: r_into_rtrancl)
   1.162 +
   1.163 +lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   1.164 +  apply (rule sym)
   1.165 +  apply (rule rtrancl_subset)
   1.166 +   apply blast
   1.167 +  apply clarify
   1.168 +  apply (rename_tac a b)
   1.169 +  apply (case_tac "a = b")
   1.170 +   apply blast
   1.171 +  apply (blast intro!: r_into_rtrancl)
   1.172 +  done
   1.173 +
   1.174 +lemma rtrancl_converseD: "(x, y) \<in> (r^-1)^* ==> (y, x) \<in> r^*"
   1.175 +  apply (erule rtrancl_induct)
   1.176 +   apply (rule rtrancl_refl)
   1.177 +  apply (blast intro: rtrancl_trans)
   1.178 +  done
   1.179 +
   1.180 +lemma rtrancl_converseI: "(y, x) \<in> r^* ==> (x, y) \<in> (r^-1)^*"
   1.181 +  apply (erule rtrancl_induct)
   1.182 +   apply (rule rtrancl_refl)
   1.183 +  apply (blast intro: rtrancl_trans)
   1.184 +  done
   1.185 +
   1.186 +lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   1.187 +  by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
   1.188 +
   1.189 +lemma converse_rtrancl_induct:
   1.190 +  "[| (a,b) : r^*; P(b);
   1.191 +      !!y z.[| (y,z) : r;  (z,b) : r^*;  P(z) |] ==> P(y) |]
   1.192 +    ==> P(a)"
   1.193 +proof -
   1.194 +  assume major: "(a,b) : r^*"
   1.195 +  case rule_context
   1.196 +  show ?thesis
   1.197 +    apply (rule major [THEN rtrancl_converseI, THEN rtrancl_induct])
   1.198 +     apply assumption
   1.199 +    apply (blast! dest!: rtrancl_converseD)
   1.200 +  done
   1.201 +qed
   1.202 +
   1.203 +ML_setup {*
   1.204 +  bind_thm ("converse_rtrancl_induct2", split_rule
   1.205 +    (read_instantiate [("a","(ax,ay)"),("b","(bx,by)")] (thm "converse_rtrancl_induct")));
   1.206 +*}
   1.207 +
   1.208 +lemma converse_rtranclE:
   1.209 +  "[| (x,z):r^*;
   1.210 +      x=z ==> P;
   1.211 +      !!y. [| (x,y):r; (y,z):r^* |] ==> P
   1.212 +   |] ==> P"
   1.213 +proof -
   1.214 +  assume major: "(x,z):r^*"
   1.215 +  case rule_context
   1.216 +  show ?thesis
   1.217 +    apply (subgoal_tac "x = z | (EX y. (x,y) : r & (y,z) : r^*)")
   1.218 +     apply (rule_tac [2] major [THEN converse_rtrancl_induct])
   1.219 +      prefer 2 apply (blast!)
   1.220 +     prefer 2 apply (blast!)
   1.221 +    apply (erule asm_rl exE disjE conjE prems)+
   1.222 +    done
   1.223 +qed
   1.224 +
   1.225 +ML_setup {*
   1.226 +  bind_thm ("converse_rtranclE2", split_rule
   1.227 +    (read_instantiate [("x","(xa,xb)"), ("z","(za,zb)")] (thm "converse_rtranclE")));
   1.228 +*}
   1.229 +
   1.230 +lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"
   1.231 +  by (blast elim: rtranclE converse_rtranclE
   1.232 +    intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
   1.233 +
   1.234 +
   1.235 +subsection {* Transitive closure *}
   1.236  
   1.237 -use "Transitive_Closure_lemmas.ML"
   1.238 +lemma trancl_mono: "p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   1.239 +  apply (unfold trancl_def)
   1.240 +  apply (blast intro: rtrancl_mono [THEN subsetD])
   1.241 +  done
   1.242 +
   1.243 +text {*
   1.244 +  \medskip Conversions between @{text trancl} and @{text rtrancl}.
   1.245 +*}
   1.246 +
   1.247 +lemma trancl_into_rtrancl: "!!p. p \<in> r^+ ==> p \<in> r^*"
   1.248 +  apply (unfold trancl_def)
   1.249 +  apply (simp only: split_tupled_all)
   1.250 +  apply (erule rel_compEpair)
   1.251 +  apply (assumption | rule rtrancl_into_rtrancl)+
   1.252 +  done
   1.253 +
   1.254 +lemma r_into_trancl [intro]: "!!p. p \<in> r ==> p \<in> r^+"
   1.255 +  -- {* @{text "r^+"} contains @{text r} *}
   1.256 +  apply (unfold trancl_def)
   1.257 +  apply (simp only: split_tupled_all)
   1.258 +  apply (assumption | rule rel_compI rtrancl_refl)+
   1.259 +  done
   1.260 +
   1.261 +lemma rtrancl_into_trancl1: "(a, b) \<in> r^* ==> (b, c) \<in> r ==> (a, c) \<in> r^+"
   1.262 +  -- {* intro rule by definition: from @{text rtrancl} and @{text r} *}
   1.263 +  by (auto simp add: trancl_def)
   1.264 +
   1.265 +lemma rtrancl_into_trancl2: "[| (a,b) : r;  (b,c) : r^* |]   ==>  (a,c) : r^+"
   1.266 +  -- {* intro rule from @{text r} and @{text rtrancl} *}
   1.267 +  apply (erule rtranclE)
   1.268 +   apply (blast intro: r_into_trancl)
   1.269 +  apply (rule rtrancl_trans [THEN rtrancl_into_trancl1])
   1.270 +   apply (assumption | rule r_into_rtrancl)+
   1.271 +  done
   1.272 +
   1.273 +lemma trancl_induct:
   1.274 +  "[| (a,b) : r^+;
   1.275 +      !!y.  [| (a,y) : r |] ==> P(y);
   1.276 +      !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)
   1.277 +   |] ==> P(b)"
   1.278 +  -- {* Nice induction rule for @{text trancl} *}
   1.279 +proof -
   1.280 +  assume major: "(a, b) : r^+"
   1.281 +  case rule_context
   1.282 +  show ?thesis
   1.283 +    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   1.284 +    txt {* by induction on this formula *}
   1.285 +    apply (subgoal_tac "ALL z. (y,z) : r --> P (z)")
   1.286 +     txt {* now solve first subgoal: this formula is sufficient *}
   1.287 +     apply blast
   1.288 +    apply (erule rtrancl_induct)
   1.289 +    apply (blast intro: rtrancl_into_trancl1 prems)+
   1.290 +    done
   1.291 +qed
   1.292 +
   1.293 +lemma trancl_trans_induct:
   1.294 +  "[| (x,y) : r^+;
   1.295 +      !!x y. (x,y) : r ==> P x y;
   1.296 +      !!x y z. [| (x,y) : r^+; P x y; (y,z) : r^+; P y z |] ==> P x z
   1.297 +   |] ==> P x y"
   1.298 +  -- {* Another induction rule for trancl, incorporating transitivity *}
   1.299 +proof -
   1.300 +  assume major: "(x,y) : r^+"
   1.301 +  case rule_context
   1.302 +  show ?thesis
   1.303 +    by (blast intro: r_into_trancl major [THEN trancl_induct] prems)
   1.304 +qed
   1.305 +
   1.306 +lemma tranclE:
   1.307 +  "[| (a::'a,b) : r^+;
   1.308 +      (a,b) : r ==> P;
   1.309 +      !!y.[| (a,y) : r^+;  (y,b) : r |] ==> P
   1.310 +   |] ==> P"
   1.311 +  -- {* elimination of @{text "r^+"} -- \emph{not} an induction rule *}
   1.312 +proof -
   1.313 +  assume major: "(a::'a,b) : r^+"
   1.314 +  case rule_context
   1.315 +  show ?thesis
   1.316 +    apply (subgoal_tac "(a::'a, b) : r | (EX y. (a,y) : r^+ & (y,b) : r)")
   1.317 +     apply (erule asm_rl disjE exE conjE prems)+
   1.318 +    apply (rule major [unfolded trancl_def, THEN rel_compEpair])
   1.319 +    apply (erule rtranclE)
   1.320 +     apply blast
   1.321 +    apply (blast intro!: rtrancl_into_trancl1)
   1.322 +    done
   1.323 +qed
   1.324  
   1.325 +lemma trans_trancl: "trans(r^+)"
   1.326 +  -- {* Transitivity of @{term "r^+"} *}
   1.327 +  -- {* Proved by unfolding since it uses transitivity of @{text rtrancl} *}
   1.328 +  apply (unfold trancl_def)
   1.329 +  apply (rule transI)
   1.330 +  apply (erule rel_compEpair)+
   1.331 +  apply (rule rtrancl_into_rtrancl [THEN rtrancl_trans [THEN rel_compI]])
   1.332 +  apply assumption+
   1.333 +  done
   1.334 +
   1.335 +lemmas trancl_trans = trans_trancl [THEN transD, standard]
   1.336 +
   1.337 +lemma rtrancl_trancl_trancl: "(x, y) \<in> r^* ==> (y, z) \<in> r^+ ==> (x, z) \<in> r^+"
   1.338 +  apply (unfold trancl_def)
   1.339 +  apply (blast intro: rtrancl_trans)
   1.340 +  done
   1.341 +
   1.342 +lemma trancl_into_trancl2: "(a, b) \<in> r ==> (b, c) \<in> r^+ ==> (a, c) \<in> r^+"
   1.343 +  by (erule transD [OF trans_trancl r_into_trancl])
   1.344 +
   1.345 +lemma trancl_insert:
   1.346 +  "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
   1.347 +  -- {* primitive recursion for @{text trancl} over finite relations *}
   1.348 +  apply (rule equalityI)
   1.349 +   apply (rule subsetI)
   1.350 +   apply (simp only: split_tupled_all)
   1.351 +   apply (erule trancl_induct)
   1.352 +    apply blast
   1.353 +   apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
   1.354 +  apply (rule subsetI)
   1.355 +  apply (blast intro: trancl_mono rtrancl_mono
   1.356 +    [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   1.357 +  done
   1.358 +
   1.359 +lemma trancl_converse: "(r^-1)^+ = (r^+)^-1"
   1.360 +  apply (unfold trancl_def)
   1.361 +  apply (simp add: rtrancl_converse converse_rel_comp)
   1.362 +  apply (simp add: rtrancl_converse [symmetric] r_comp_rtrancl_eq)
   1.363 +  done
   1.364 +
   1.365 +lemma trancl_converseI: "(x, y) \<in> (r^+)^-1 ==> (x,y) \<in> (r^-1)^+"
   1.366 +  by (simp add: trancl_converse)
   1.367 +
   1.368 +lemma trancl_converseD: "(x, y) \<in> (r^-1)^+ ==> (x, y) \<in> (r^+)^-1"
   1.369 +  by (simp add: trancl_converse)
   1.370 +
   1.371 +lemma converse_trancl_induct:
   1.372 +  "[| (a,b) : r^+; !!y. (y,b) : r ==> P(y);
   1.373 +      !!y z.[| (y,z) : r;  (z,b) : r^+;  P(z) |] ==> P(y) |]
   1.374 +    ==> P(a)"
   1.375 +proof -
   1.376 +  assume major: "(a,b) : r^+"
   1.377 +  case rule_context
   1.378 +  show ?thesis
   1.379 +    apply (rule major [THEN converseI, THEN trancl_converseI [THEN trancl_induct]])
   1.380 +     apply (rule prems)
   1.381 +     apply (erule converseD)
   1.382 +    apply (blast intro: prems dest!: trancl_converseD)
   1.383 +    done
   1.384 +qed
   1.385 +
   1.386 +lemma tranclD: "(x, y) \<in> R^+ ==> EX z. (x, z) \<in> R \<and> (z, y) \<in> R^*"
   1.387 +  apply (erule converse_trancl_induct)
   1.388 +   apply auto
   1.389 +  apply (blast intro: rtrancl_trans)
   1.390 +  done
   1.391 +
   1.392 +lemma irrefl_tranclI: "r^-1 \<inter> r^+ = {} ==> (x, x) \<notin> r^+"
   1.393 +  apply (subgoal_tac "ALL y. (x, y) : r^+ --> x \<noteq> y")
   1.394 +   apply fast
   1.395 +  apply (intro strip)
   1.396 +  apply (erule trancl_induct)
   1.397 +   apply (auto intro: r_into_trancl)
   1.398 +  done
   1.399 +
   1.400 +lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
   1.401 +  by (blast dest: r_into_trancl)
   1.402 +
   1.403 +lemma trancl_subset_Sigma_aux:
   1.404 +    "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
   1.405 +  apply (erule rtrancl_induct)
   1.406 +   apply auto
   1.407 +  done
   1.408 +
   1.409 +lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   1.410 +  apply (unfold trancl_def)
   1.411 +  apply (blast dest!: trancl_subset_Sigma_aux)
   1.412 +  done
   1.413  
   1.414  lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
   1.415    apply safe
   1.416 -  apply (erule trancl_into_rtrancl)
   1.417 +   apply (erule trancl_into_rtrancl)
   1.418    apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
   1.419    done
   1.420  
   1.421 @@ -70,7 +416,7 @@
   1.422    by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
   1.423  
   1.424  
   1.425 -(* should be merged with the main body of lemmas: *)
   1.426 +text {* @{text Domain} and @{text Range} *}
   1.427  
   1.428  lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
   1.429    by blast
   1.430 @@ -91,24 +437,26 @@
   1.431    by (simp add: Range_def trancl_converse [symmetric])
   1.432  
   1.433  lemma Not_Domain_rtrancl:
   1.434 -	"x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   1.435 - apply (auto)
   1.436 - by (erule rev_mp, erule rtrancl_induct, auto)
   1.437 +    "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   1.438 +  apply auto
   1.439 +  by (erule rev_mp, erule rtrancl_induct, auto)
   1.440 +
   1.441  
   1.442 -(* more about converse rtrancl and trancl, should be merged with main body *)
   1.443 +text {* More about converse @{text rtrancl} and @{text trancl}, should
   1.444 +  be merged with main body. *}
   1.445  
   1.446 -lemma r_r_into_trancl: "(a,b) \<in> R \<Longrightarrow> (b,c) \<in> R \<Longrightarrow> (a,c) \<in> R^+"
   1.447 +lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
   1.448    by (fast intro: trancl_trans)
   1.449  
   1.450  lemma trancl_into_trancl [rule_format]:
   1.451 -  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r \<longrightarrow> (a,c) \<in> r\<^sup>+"
   1.452 -  apply (erule trancl_induct)   
   1.453 +    "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+"
   1.454 +  apply (erule trancl_induct)
   1.455     apply (fast intro: r_r_into_trancl)
   1.456    apply (fast intro: r_r_into_trancl trancl_trans)
   1.457    done
   1.458  
   1.459  lemma trancl_rtrancl_trancl:
   1.460 -  "(a,b) \<in> r\<^sup>+ \<Longrightarrow> (b,c) \<in> r\<^sup>* \<Longrightarrow> (a,c) \<in> r\<^sup>+"
   1.461 +    "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r\<^sup>* ==> (a, c) \<in> r\<^sup>+"
   1.462    apply (drule tranclD)
   1.463    apply (erule exE, erule conjE)
   1.464    apply (drule rtrancl_trans, assumption)
   1.465 @@ -116,10 +464,11 @@
   1.466    apply assumption
   1.467    done
   1.468  
   1.469 -lemmas [trans] = r_r_into_trancl trancl_trans rtrancl_trans 
   1.470 -                 trancl_into_trancl trancl_into_trancl2
   1.471 -                 rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   1.472 -                 rtrancl_trancl_trancl trancl_rtrancl_trancl
   1.473 +lemmas transitive_closure_trans [trans] =
   1.474 +  r_r_into_trancl trancl_trans rtrancl_trans
   1.475 +  trancl_into_trancl trancl_into_trancl2
   1.476 +  rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   1.477 +  rtrancl_trancl_trancl trancl_rtrancl_trancl
   1.478  
   1.479  declare trancl_into_rtrancl [elim]
   1.480