src/HOL/Transitive_Closure.thy
author haftmann
Fri Mar 09 08:45:50 2007 +0100 (2007-03-09)
changeset 22422 ee19cdb07528
parent 22262 96ba62dff413
child 23743 52fbc991039f
permissions -rw-r--r--
stepping towards uniform lattice theory development in HOL
     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 
     7 header {* Reflexive and Transitive closure of a relation *}
     8 
     9 theory Transitive_Closure
    10 imports Predicate
    11 uses "~~/src/Provers/trancl.ML"
    12 begin
    13 
    14 text {*
    15   @{text rtrancl} is reflexive/transitive closure,
    16   @{text trancl} is transitive closure,
    17   @{text reflcl} is reflexive closure.
    18 
    19   These postfix operators have \emph{maximum priority}, forcing their
    20   operands to be atomic.
    21 *}
    22 
    23 inductive2
    24   rtrancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"   ("(_^**)" [1000] 1000)
    25   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    26 where
    27     rtrancl_refl [intro!, Pure.intro!, simp]: "r^** a a"
    28   | rtrancl_into_rtrancl [Pure.intro]: "r^** a b ==> r b c ==> r^** a c"
    29 
    30 inductive2
    31   trancl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(_^++)" [1000] 1000)
    32   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    33 where
    34     r_into_trancl [intro, Pure.intro]: "r a b ==> r^++ a b"
    35   | trancl_into_trancl [Pure.intro]: "r^++ a b ==> r b c ==> r^++ a c"
    36 
    37 constdefs
    38   rtrancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^*)" [1000] 999)
    39   "r^* == Collect2 (member2 r)^**"
    40 
    41   trancl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_^+)" [1000] 999)
    42   "r^+ == Collect2 (member2 r)^++"
    43 
    44 abbreviation
    45   reflcl :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
    46   "r^== == sup r op ="
    47 
    48 abbreviation
    49   reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
    50   "r^= == r \<union> Id"
    51 
    52 notation (xsymbols)
    53   rtrancl  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    54   trancl  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
    55   reflcl  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
    56   rtrancl_set  ("(_\<^sup>*)" [1000] 999) and
    57   trancl_set  ("(_\<^sup>+)" [1000] 999) and
    58   reflcl_set  ("(_\<^sup>=)" [1000] 999)
    59 
    60 notation (HTML output)
    61   rtrancl  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
    62   trancl  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
    63   reflcl  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
    64   rtrancl_set  ("(_\<^sup>*)" [1000] 999) and
    65   trancl_set  ("(_\<^sup>+)" [1000] 999) and
    66   reflcl_set  ("(_\<^sup>=)" [1000] 999)
    67 
    68 
    69 subsection {* Reflexive-transitive closure *}
    70 
    71 lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
    72   by (simp add: rtrancl_set_def)
    73 
    74 lemma reflcl_set_eq [pred_set_conv]: "(sup (member2 r) op =) = member2 (r Un Id)"
    75   by (simp add: expand_fun_eq)
    76 
    77 lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
    78 lemmas rtrancl_into_rtrancl [Pure.intro] = rtrancl_into_rtrancl [to_set]
    79 
    80 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
    81   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
    82   apply (simp only: split_tupled_all)
    83   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])
    84   done
    85 
    86 lemma r_into_rtrancl' [intro]: "r x y ==> r^** x y"
    87   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
    88   by (erule rtrancl.rtrancl_refl [THEN rtrancl.rtrancl_into_rtrancl])
    89 
    90 lemma rtrancl_mono': "r \<le> s ==> r^** \<le> s^**"
    91   -- {* monotonicity of @{text rtrancl} *}
    92   apply (rule predicate2I)
    93   apply (erule rtrancl.induct)
    94    apply (rule_tac [2] rtrancl.rtrancl_into_rtrancl, blast+)
    95   done
    96 
    97 lemmas rtrancl_mono = rtrancl_mono' [to_set]
    98 
    99 theorem rtrancl_induct' [consumes 1, induct set: rtrancl]:
   100   assumes a: "r^** a b"
   101     and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"
   102   shows "P b"
   103 proof -
   104   from a have "a = a --> P b"
   105     by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
   106   thus ?thesis by iprover
   107 qed
   108 
   109 lemmas rtrancl_induct [consumes 1, induct set: rtrancl_set] = rtrancl_induct' [to_set]
   110 
   111 lemmas rtrancl_induct2' =
   112   rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   113                  consumes 1, case_names refl step]
   114 
   115 lemmas rtrancl_induct2 =
   116   rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   117                  consumes 1, case_names refl step]
   118 
   119 lemma reflexive_rtrancl: "reflexive (r^*)"
   120   by (unfold refl_def) fast
   121 
   122 lemma trans_rtrancl: "trans(r^*)"
   123   -- {* transitivity of transitive closure!! -- by induction *}
   124 proof (rule transI)
   125   fix x y z
   126   assume "(x, y) \<in> r\<^sup>*"
   127   assume "(y, z) \<in> r\<^sup>*"
   128   thus "(x, z) \<in> r\<^sup>*" by induct (iprover!)+
   129 qed
   130 
   131 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
   132 
   133 lemma rtrancl_trans':
   134   assumes xy: "r^** x y"
   135   and yz: "r^** y z"
   136   shows "r^** x z" using yz xy
   137   by induct iprover+
   138 
   139 lemma rtranclE:
   140   assumes major: "(a::'a,b) : r^*"
   141     and cases: "(a = b) ==> P"
   142       "!!y. [| (a,y) : r^*; (y,b) : r |] ==> P"
   143   shows P
   144   -- {* elimination of @{text rtrancl} -- by induction on a special formula *}
   145   apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")
   146    apply (rule_tac [2] major [THEN rtrancl_induct])
   147     prefer 2 apply blast
   148    prefer 2 apply blast
   149   apply (erule asm_rl exE disjE conjE cases)+
   150   done
   151 
   152 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
   153   apply (rule subsetI)
   154   apply (rule_tac p="x" in PairE, clarify)
   155   apply (erule rtrancl_induct, auto) 
   156   done
   157 
   158 lemma converse_rtrancl_into_rtrancl':
   159   "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c"
   160   by (rule rtrancl_trans') iprover+
   161 
   162 lemmas converse_rtrancl_into_rtrancl = converse_rtrancl_into_rtrancl' [to_set]
   163 
   164 text {*
   165   \medskip More @{term "r^*"} equations and inclusions.
   166 *}
   167 
   168 lemma rtrancl_idemp' [simp]: "(r^**)^** = r^**"
   169   apply (auto intro!: order_antisym)
   170   apply (erule rtrancl_induct')
   171    apply (rule rtrancl.rtrancl_refl)
   172   apply (blast intro: rtrancl_trans')
   173   done
   174 
   175 lemmas rtrancl_idemp [simp] = rtrancl_idemp' [to_set]
   176 
   177 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
   178   apply (rule set_ext)
   179   apply (simp only: split_tupled_all)
   180   apply (blast intro: rtrancl_trans)
   181   done
   182 
   183 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"
   184 by (drule rtrancl_mono, simp)
   185 
   186 lemma rtrancl_subset': "R \<le> S ==> S \<le> R^** ==> S^** = R^**"
   187   apply (drule rtrancl_mono')
   188   apply (drule rtrancl_mono', simp)
   189   done
   190 
   191 lemmas rtrancl_subset = rtrancl_subset' [to_set]
   192 
   193 lemma rtrancl_Un_rtrancl': "(sup (R^**) (S^**))^** = (sup R S)^**"
   194   by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
   195 
   196 lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
   197 
   198 lemma rtrancl_reflcl' [simp]: "(R^==)^** = R^**"
   199   by (blast intro!: rtrancl_subset')
   200 
   201 lemmas rtrancl_reflcl [simp] = rtrancl_reflcl' [to_set]
   202 
   203 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"
   204   apply (rule sym)
   205   apply (rule rtrancl_subset, blast, clarify)
   206   apply (rename_tac a b)
   207   apply (case_tac "a = b", blast)
   208   apply (blast intro!: r_into_rtrancl)
   209   done
   210 
   211 lemma rtrancl_r_diff_Id': "(inf r op ~=)^** = r^**"
   212   apply (rule sym)
   213   apply (rule rtrancl_subset')
   214   apply blast+
   215   done
   216 
   217 theorem rtrancl_converseD':
   218   assumes r: "(r^--1)^** x y"
   219   shows "r^** y x"
   220 proof -
   221   from r show ?thesis
   222     by induct (iprover intro: rtrancl_trans' dest!: conversepD)+
   223 qed
   224 
   225 lemmas rtrancl_converseD = rtrancl_converseD' [to_set]
   226 
   227 theorem rtrancl_converseI':
   228   assumes r: "r^** y x"
   229   shows "(r^--1)^** x y"
   230 proof -
   231   from r show ?thesis
   232     by induct (iprover intro: rtrancl_trans' conversepI)+
   233 qed
   234 
   235 lemmas rtrancl_converseI = rtrancl_converseI' [to_set]
   236 
   237 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"
   238   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)
   239 
   240 lemma sym_rtrancl: "sym r ==> sym (r^*)"
   241   by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])
   242 
   243 theorem converse_rtrancl_induct'[consumes 1]:
   244   assumes major: "r^** a b"
   245     and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"
   246   shows "P a"
   247 proof -
   248   from rtrancl_converseI' [OF major]
   249   show ?thesis
   250     by induct (iprover intro: cases dest!: conversepD rtrancl_converseD')+
   251 qed
   252 
   253 lemmas converse_rtrancl_induct[consumes 1] = converse_rtrancl_induct' [to_set]
   254 
   255 lemmas converse_rtrancl_induct2' =
   256   converse_rtrancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   257                  consumes 1, case_names refl step]
   258 
   259 lemmas converse_rtrancl_induct2 =
   260   converse_rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   261                  consumes 1, case_names refl step]
   262 
   263 lemma converse_rtranclE':
   264   assumes major: "r^** x z"
   265     and cases: "x=z ==> P"
   266       "!!y. [| r x y; r^** y z |] ==> P"
   267   shows P
   268   apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)")
   269    apply (rule_tac [2] major [THEN converse_rtrancl_induct'])
   270     prefer 2 apply iprover
   271    prefer 2 apply iprover
   272   apply (erule asm_rl exE disjE conjE cases)+
   273   done
   274 
   275 lemmas converse_rtranclE = converse_rtranclE' [to_set]
   276 
   277 lemmas converse_rtranclE2' = converse_rtranclE' [of _ "(xa,xb)" "(za,zb)", split_rule]
   278 
   279 lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule]
   280 
   281 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"
   282   by (blast elim: rtranclE converse_rtranclE
   283     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
   284 
   285 lemma rtrancl_unfold: "r^* = Id Un r O r^*"
   286   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
   287 
   288 
   289 subsection {* Transitive closure *}
   290 
   291 lemma trancl_set_eq [pred_set_conv]: "(member2 r)^++ = member2 (r^+)"
   292   by (simp add: trancl_set_def)
   293 
   294 lemmas r_into_trancl [intro, Pure.intro] = r_into_trancl [to_set]
   295 lemmas trancl_into_trancl [Pure.intro] = trancl_into_trancl [to_set]
   296 
   297 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"
   298   apply (simp add: split_tupled_all trancl_set_def)
   299   apply (erule trancl.induct)
   300   apply (iprover dest: subsetD)+
   301   done
   302 
   303 lemma r_into_trancl': "!!p. p : r ==> p : r^+"
   304   by (simp only: split_tupled_all) (erule r_into_trancl)
   305 
   306 text {*
   307   \medskip Conversions between @{text trancl} and @{text rtrancl}.
   308 *}
   309 
   310 lemma trancl_into_rtrancl': "r^++ a b ==> r^** a b"
   311   by (erule trancl.induct) iprover+
   312 
   313 lemmas trancl_into_rtrancl = trancl_into_rtrancl' [to_set]
   314 
   315 lemma rtrancl_into_trancl1': assumes r: "r^** a b"
   316   shows "!!c. r b c ==> r^++ a c" using r
   317   by induct iprover+
   318 
   319 lemmas rtrancl_into_trancl1 = rtrancl_into_trancl1' [to_set]
   320 
   321 lemma rtrancl_into_trancl2': "[| r a b; r^** b c |] ==> r^++ a c"
   322   -- {* intro rule from @{text r} and @{text rtrancl} *}
   323   apply (erule rtrancl.cases, iprover)
   324   apply (rule rtrancl_trans' [THEN rtrancl_into_trancl1'])
   325    apply (simp | rule r_into_rtrancl')+
   326   done
   327 
   328 lemmas rtrancl_into_trancl2 = rtrancl_into_trancl2' [to_set]
   329 
   330 lemma trancl_induct' [consumes 1, induct set: trancl]:
   331   assumes a: "r^++ a b"
   332   and cases: "!!y. r a y ==> P y"
   333     "!!y z. r^++ a y ==> r y z ==> P y ==> P z"
   334   shows "P b"
   335   -- {* Nice induction rule for @{text trancl} *}
   336 proof -
   337   from a have "a = a --> P b"
   338     by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+
   339   thus ?thesis by iprover
   340 qed
   341 
   342 lemmas trancl_induct [consumes 1, induct set: trancl_set] = trancl_induct' [to_set]
   343 
   344 lemmas trancl_induct2' =
   345   trancl_induct'[of _ "(ax,ay)" "(bx,by)", split_rule,
   346                  consumes 1, case_names base step]
   347 
   348 lemmas trancl_induct2 =
   349   trancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
   350                  consumes 1, case_names base step]
   351 
   352 lemma trancl_trans_induct':
   353   assumes major: "r^++ x y"
   354     and cases: "!!x y. r x y ==> P x y"
   355       "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"
   356   shows "P x y"
   357   -- {* Another induction rule for trancl, incorporating transitivity *}
   358   by (iprover intro: major [THEN trancl_induct'] cases)
   359 
   360 lemmas trancl_trans_induct = trancl_trans_induct' [to_set]
   361 
   362 lemma tranclE:
   363   assumes H: "(a, b) : r^+"
   364   and cases: "(a, b) : r ==> P" "\<And>c. (a, c) : r^+ ==> (c, b) : r ==> P"
   365   shows P
   366   using H [simplified trancl_set_def, simplified]
   367   by cases (auto intro: cases [simplified trancl_set_def, simplified])
   368 
   369 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
   370   apply (rule subsetI)
   371   apply (rule_tac p="x" in PairE, clarify)
   372   apply (erule trancl_induct, auto) 
   373   done
   374 
   375 lemma trancl_unfold: "r^+ = r Un r O r^+"
   376   by (auto intro: trancl_into_trancl elim: tranclE)
   377 
   378 lemma trans_trancl[simp]: "trans(r^+)"
   379   -- {* Transitivity of @{term "r^+"} *}
   380 proof (rule transI)
   381   fix x y z
   382   assume xy: "(x, y) \<in> r^+"
   383   assume "(y, z) \<in> r^+"
   384   thus "(x, z) \<in> r^+" by induct (insert xy, iprover)+
   385 qed
   386 
   387 lemmas trancl_trans = trans_trancl [THEN transD, standard]
   388 
   389 lemma trancl_trans':
   390   assumes xy: "r^++ x y"
   391   and yz: "r^++ y z"
   392   shows "r^++ x z" using yz xy
   393   by induct iprover+
   394 
   395 lemma trancl_id[simp]: "trans r \<Longrightarrow> r^+ = r"
   396 apply(auto)
   397 apply(erule trancl_induct)
   398 apply assumption
   399 apply(unfold trans_def)
   400 apply(blast)
   401 done
   402 
   403 lemma rtrancl_trancl_trancl': assumes r: "r^** x y"
   404   shows "!!z. r^++ y z ==> r^++ x z" using r
   405   by induct (iprover intro: trancl_trans')+
   406 
   407 lemmas rtrancl_trancl_trancl = rtrancl_trancl_trancl' [to_set]
   408 
   409 lemma trancl_into_trancl2': "r a b ==> r^++ b c ==> r^++ a c"
   410   by (erule trancl_trans' [OF trancl.r_into_trancl])
   411 
   412 lemmas trancl_into_trancl2 = trancl_into_trancl2' [to_set]
   413 
   414 lemma trancl_insert:
   415   "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"
   416   -- {* primitive recursion for @{text trancl} over finite relations *}
   417   apply (rule equalityI)
   418    apply (rule subsetI)
   419    apply (simp only: split_tupled_all)
   420    apply (erule trancl_induct, blast)
   421    apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)
   422   apply (rule subsetI)
   423   apply (blast intro: trancl_mono rtrancl_mono
   424     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)
   425   done
   426 
   427 lemma trancl_converseI': "(r^++)^--1 x y ==> (r^--1)^++ x y"
   428   apply (drule conversepD)
   429   apply (erule trancl_induct')
   430   apply (iprover intro: conversepI trancl_trans')+
   431   done
   432 
   433 lemmas trancl_converseI = trancl_converseI' [to_set]
   434 
   435 lemma trancl_converseD': "(r^--1)^++ x y ==> (r^++)^--1 x y"
   436   apply (rule conversepI)
   437   apply (erule trancl_induct')
   438   apply (iprover dest: conversepD intro: trancl_trans')+
   439   done
   440 
   441 lemmas trancl_converseD = trancl_converseD' [to_set]
   442 
   443 lemma trancl_converse': "(r^--1)^++ = (r^++)^--1"
   444   by (fastsimp simp add: expand_fun_eq
   445     intro!: trancl_converseI' dest!: trancl_converseD')
   446 
   447 lemmas trancl_converse = trancl_converse' [to_set]
   448 
   449 lemma sym_trancl: "sym r ==> sym (r^+)"
   450   by (simp only: sym_conv_converse_eq trancl_converse [symmetric])
   451 
   452 lemma converse_trancl_induct':
   453   assumes major: "r^++ a b"
   454     and cases: "!!y. r y b ==> P(y)"
   455       "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"
   456   shows "P a"
   457   apply (rule trancl_induct' [OF trancl_converseI', OF conversepI, OF major])
   458    apply (rule cases)
   459    apply (erule conversepD)
   460   apply (blast intro: prems dest!: trancl_converseD' conversepD)
   461   done
   462 
   463 lemmas converse_trancl_induct = converse_trancl_induct' [to_set]
   464 
   465 lemma tranclD': "R^++ x y ==> EX z. R x z \<and> R^** z y"
   466   apply (erule converse_trancl_induct', auto)
   467   apply (blast intro: rtrancl_trans')
   468   done
   469 
   470 lemmas tranclD = tranclD' [to_set]
   471 
   472 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"
   473   by (blast elim: tranclE dest: trancl_into_rtrancl)
   474 
   475 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"
   476   by (blast dest: r_into_trancl)
   477 
   478 lemma trancl_subset_Sigma_aux:
   479     "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"
   480   by (induct rule: rtrancl_induct) auto
   481 
   482 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"
   483   apply (rule subsetI)
   484   apply (simp only: split_tupled_all)
   485   apply (erule tranclE)
   486   apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+
   487   done
   488 
   489 lemma reflcl_trancl' [simp]: "(r^++)^== = r^**"
   490   apply (safe intro!: order_antisym)
   491    apply (erule trancl_into_rtrancl')
   492   apply (blast elim: rtrancl.cases dest: rtrancl_into_trancl1')
   493   done
   494 
   495 lemmas reflcl_trancl [simp] = reflcl_trancl' [to_set]
   496 
   497 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
   498   apply safe
   499    apply (drule trancl_into_rtrancl, simp)
   500   apply (erule rtranclE, safe)
   501    apply (rule r_into_trancl, simp)
   502   apply (rule rtrancl_into_trancl1)
   503    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
   504   done
   505 
   506 lemma trancl_empty [simp]: "{}^+ = {}"
   507   by (auto elim: trancl_induct)
   508 
   509 lemma rtrancl_empty [simp]: "{}^* = Id"
   510   by (rule subst [OF reflcl_trancl]) simp
   511 
   512 lemma rtranclD': "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b"
   513   by (force simp add: reflcl_trancl' [symmetric] simp del: reflcl_trancl')
   514 
   515 lemmas rtranclD = rtranclD' [to_set]
   516 
   517 lemma rtrancl_eq_or_trancl:
   518   "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
   519   by (fast elim: trancl_into_rtrancl dest: rtranclD)
   520 
   521 text {* @{text Domain} and @{text Range} *}
   522 
   523 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
   524   by blast
   525 
   526 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
   527   by blast
   528 
   529 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
   530   by (rule rtrancl_Un_rtrancl [THEN subst]) fast
   531 
   532 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
   533   by (blast intro: subsetD [OF rtrancl_Un_subset])
   534 
   535 lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
   536   by (unfold Domain_def) (blast dest: tranclD)
   537 
   538 lemma trancl_range [simp]: "Range (r^+) = Range r"
   539   by (simp add: Range_def trancl_converse [symmetric])
   540 
   541 lemma Not_Domain_rtrancl:
   542     "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"
   543   apply auto
   544   by (erule rev_mp, erule rtrancl_induct, auto)
   545 
   546 
   547 text {* More about converse @{text rtrancl} and @{text trancl}, should
   548   be merged with main body. *}
   549 
   550 lemma single_valued_confluent:
   551   "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>
   552   \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*"
   553 apply(erule rtrancl_induct)
   554  apply simp
   555 apply(erule disjE)
   556  apply(blast elim:converse_rtranclE dest:single_valuedD)
   557 apply(blast intro:rtrancl_trans)
   558 done
   559 
   560 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"
   561   by (fast intro: trancl_trans)
   562 
   563 lemma trancl_into_trancl [rule_format]:
   564     "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+"
   565   apply (erule trancl_induct)
   566    apply (fast intro: r_r_into_trancl)
   567   apply (fast intro: r_r_into_trancl trancl_trans)
   568   done
   569 
   570 lemma trancl_rtrancl_trancl':
   571     "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c"
   572   apply (drule tranclD')
   573   apply (erule exE, erule conjE)
   574   apply (drule rtrancl_trans', assumption)
   575   apply (drule rtrancl_into_trancl2', assumption, assumption)
   576   done
   577 
   578 lemmas trancl_rtrancl_trancl = trancl_rtrancl_trancl' [to_set]
   579 
   580 lemmas transitive_closure_trans [trans] =
   581   r_r_into_trancl trancl_trans rtrancl_trans
   582   trancl_into_trancl trancl_into_trancl2
   583   rtrancl_into_rtrancl converse_rtrancl_into_rtrancl
   584   rtrancl_trancl_trancl trancl_rtrancl_trancl
   585 
   586 lemmas transitive_closure_trans' [trans] =
   587   trancl_trans' rtrancl_trans'
   588   trancl.trancl_into_trancl trancl_into_trancl2'
   589   rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl'
   590   rtrancl_trancl_trancl' trancl_rtrancl_trancl'
   591 
   592 declare trancl_into_rtrancl [elim]
   593 
   594 declare rtranclE [cases set: rtrancl_set]
   595 declare tranclE [cases set: trancl_set]
   596 
   597 
   598 
   599 
   600 
   601 subsection {* Setup of transitivity reasoner *}
   602 
   603 ML_setup {*
   604 
   605 structure Trancl_Tac = Trancl_Tac_Fun (
   606   struct
   607     val r_into_trancl = thm "r_into_trancl";
   608     val trancl_trans  = thm "trancl_trans";
   609     val rtrancl_refl = thm "rtrancl_refl";
   610     val r_into_rtrancl = thm "r_into_rtrancl";
   611     val trancl_into_rtrancl = thm "trancl_into_rtrancl";
   612     val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl";
   613     val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl";
   614     val rtrancl_trans = thm "rtrancl_trans";
   615 
   616   fun decomp (Trueprop $ t) =
   617     let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
   618         let fun decr (Const ("Transitive_Closure.rtrancl_set", _ ) $ r) = (r,"r*")
   619               | decr (Const ("Transitive_Closure.trancl_set", _ ) $ r)  = (r,"r+")
   620               | decr r = (r,"r");
   621             val (rel,r) = decr rel;
   622         in SOME (a,b,rel,r) end
   623       | dec _ =  NONE
   624     in dec t end;
   625 
   626   end);
   627 
   628 structure Tranclp_Tac = Trancl_Tac_Fun (
   629   struct
   630     val r_into_trancl = thm "trancl.r_into_trancl";
   631     val trancl_trans  = thm "trancl_trans'";
   632     val rtrancl_refl = thm "rtrancl.rtrancl_refl";
   633     val r_into_rtrancl = thm "r_into_rtrancl'";
   634     val trancl_into_rtrancl = thm "trancl_into_rtrancl'";
   635     val rtrancl_trancl_trancl = thm "rtrancl_trancl_trancl'";
   636     val trancl_rtrancl_trancl = thm "trancl_rtrancl_trancl'";
   637     val rtrancl_trans = thm "rtrancl_trans'";
   638 
   639   fun decomp (Trueprop $ t) =
   640     let fun dec (rel $ a $ b) =
   641         let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
   642               | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
   643               | decr r = (r,"r");
   644             val (rel,r) = decr rel;
   645         in SOME (a, b, Envir.beta_eta_contract rel, r) end
   646       | dec _ =  NONE
   647     in dec t end;
   648 
   649   end);
   650 
   651 change_simpset (fn ss => ss
   652   addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
   653   addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))
   654   addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))
   655   addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)));
   656 
   657 *}
   658 
   659 (* Optional methods *)
   660 
   661 method_setup trancl =
   662   {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}
   663   {* simple transitivity reasoner *}
   664 method_setup rtrancl =
   665   {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}
   666   {* simple transitivity reasoner *}
   667 method_setup tranclp =
   668   {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}
   669   {* simple transitivity reasoner (predicate version) *}
   670 method_setup rtranclp =
   671   {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}
   672   {* simple transitivity reasoner (predicate version) *}
   673 
   674 end