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