src/HOL/Transitive_Closure.thy
 author wenzelm Fri Mar 13 19:58:26 2009 +0100 (2009-03-13) changeset 30510 4120fc59dd85 parent 30242 aea5d7fa7ef5 child 30549 d2d7874648bd permissions -rw-r--r--
unified type Proof.method and pervasive METHOD combinators;
     1 (*  Title:      HOL/Transitive_Closure.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1992  University of Cambridge

     4 *)

     5

     6 header {* Reflexive and Transitive closure of a relation *}

     7

     8 theory Transitive_Closure

     9 imports Predicate

    10 uses "~~/src/Provers/trancl.ML"

    11 begin

    12

    13 text {*

    14   @{text rtrancl} is reflexive/transitive closure,

    15   @{text trancl} is transitive closure,

    16   @{text reflcl} is reflexive closure.

    17

    18   These postfix operators have \emph{maximum priority}, forcing their

    19   operands to be atomic.

    20 *}

    21

    22 inductive_set

    23   rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"   ("(_^*)" [1000] 999)

    24   for r :: "('a \<times> 'a) set"

    25 where

    26     rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"

    27   | rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"

    28

    29 inductive_set

    30   trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_^+)" [1000] 999)

    31   for r :: "('a \<times> 'a) set"

    32 where

    33     r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"

    34   | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"

    35

    36 notation

    37   rtranclp  ("(_^**)" [1000] 1000) and

    38   tranclp  ("(_^++)" [1000] 1000)

    39

    40 abbreviation

    41   reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where

    42   "r^== == sup r op ="

    43

    44 abbreviation

    45   reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where

    46   "r^= == r \<union> Id"

    47

    48 notation (xsymbols)

    49   rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and

    50   tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and

    51   reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and

    52   rtrancl  ("(_\<^sup>*)" [1000] 999) and

    53   trancl  ("(_\<^sup>+)" [1000] 999) and

    54   reflcl  ("(_\<^sup>=)" [1000] 999)

    55

    56 notation (HTML output)

    57   rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and

    58   tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and

    59   reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and

    60   rtrancl  ("(_\<^sup>*)" [1000] 999) and

    61   trancl  ("(_\<^sup>+)" [1000] 999) and

    62   reflcl  ("(_\<^sup>=)" [1000] 999)

    63

    64

    65 subsection {* Reflexive closure *}

    66

    67 lemma refl_reflcl[simp]: "refl(r^=)"

    68 by(simp add:refl_on_def)

    69

    70 lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"

    71 by(simp add:antisym_def)

    72

    73 lemma trans_reflclI[simp]: "trans r \<Longrightarrow> trans(r^=)"

    74 unfolding trans_def by blast

    75

    76

    77 subsection {* Reflexive-transitive closure *}

    78

    79 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)"

    80   by (simp add: expand_fun_eq)

    81

    82 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"

    83   -- {* @{text rtrancl} of @{text r} contains @{text r} *}

    84   apply (simp only: split_tupled_all)

    85   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])

    86   done

    87

    88 lemma r_into_rtranclp [intro]: "r x y ==> r^** x y"

    89   -- {* @{text rtrancl} of @{text r} contains @{text r} *}

    90   by (erule rtranclp.rtrancl_refl [THEN rtranclp.rtrancl_into_rtrancl])

    91

    92 lemma rtranclp_mono: "r \<le> s ==> r^** \<le> s^**"

    93   -- {* monotonicity of @{text rtrancl} *}

    94   apply (rule predicate2I)

    95   apply (erule rtranclp.induct)

    96    apply (rule_tac [2] rtranclp.rtrancl_into_rtrancl, blast+)

    97   done

    98

    99 lemmas rtrancl_mono = rtranclp_mono [to_set]

   100

   101 theorem rtranclp_induct [consumes 1, case_names base step, induct set: rtranclp]:

   102   assumes a: "r^** a b"

   103     and cases: "P a" "!!y z. [| r^** a y; r y z; P y |] ==> P z"

   104   shows "P b"

   105 proof -

   106   from a have "a = a --> P b"

   107     by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+

   108   then show ?thesis by iprover

   109 qed

   110

   111 lemmas rtrancl_induct [induct set: rtrancl] = rtranclp_induct [to_set]

   112

   113 lemmas rtranclp_induct2 =

   114   rtranclp_induct[of _ "(ax,ay)" "(bx,by)", split_rule,

   115                  consumes 1, case_names refl step]

   116

   117 lemmas rtrancl_induct2 =

   118   rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),

   119                  consumes 1, case_names refl step]

   120

   121 lemma refl_rtrancl: "refl (r^*)"

   122 by (unfold refl_on_def) fast

   123

   124 text {* Transitivity of transitive closure. *}

   125 lemma trans_rtrancl: "trans (r^*)"

   126 proof (rule transI)

   127   fix x y z

   128   assume "(x, y) \<in> r\<^sup>*"

   129   assume "(y, z) \<in> r\<^sup>*"

   130   then show "(x, z) \<in> r\<^sup>*"

   131   proof induct

   132     case base

   133     show "(x, y) \<in> r\<^sup>*" by fact

   134   next

   135     case (step u v)

   136     from (x, u) \<in> r\<^sup>* and (u, v) \<in> r

   137     show "(x, v) \<in> r\<^sup>*" ..

   138   qed

   139 qed

   140

   141 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]

   142

   143 lemma rtranclp_trans:

   144   assumes xy: "r^** x y"

   145   and yz: "r^** y z"

   146   shows "r^** x z" using yz xy

   147   by induct iprover+

   148

   149 lemma rtranclE [cases set: rtrancl]:

   150   assumes major: "(a::'a, b) : r^*"

   151   obtains

   152     (base) "a = b"

   153   | (step) y where "(a, y) : r^*" and "(y, b) : r"

   154   -- {* elimination of @{text rtrancl} -- by induction on a special formula *}

   155   apply (subgoal_tac "(a::'a) = b | (EX y. (a,y) : r^* & (y,b) : r)")

   156    apply (rule_tac [2] major [THEN rtrancl_induct])

   157     prefer 2 apply blast

   158    prefer 2 apply blast

   159   apply (erule asm_rl exE disjE conjE base step)+

   160   done

   161

   162 lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"

   163   apply (rule subsetI)

   164   apply (rule_tac p="x" in PairE, clarify)

   165   apply (erule rtrancl_induct, auto)

   166   done

   167

   168 lemma converse_rtranclp_into_rtranclp:

   169   "r a b \<Longrightarrow> r\<^sup>*\<^sup>* b c \<Longrightarrow> r\<^sup>*\<^sup>* a c"

   170   by (rule rtranclp_trans) iprover+

   171

   172 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]

   173

   174 text {*

   175   \medskip More @{term "r^*"} equations and inclusions.

   176 *}

   177

   178 lemma rtranclp_idemp [simp]: "(r^**)^** = r^**"

   179   apply (auto intro!: order_antisym)

   180   apply (erule rtranclp_induct)

   181    apply (rule rtranclp.rtrancl_refl)

   182   apply (blast intro: rtranclp_trans)

   183   done

   184

   185 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]

   186

   187 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"

   188   apply (rule set_ext)

   189   apply (simp only: split_tupled_all)

   190   apply (blast intro: rtrancl_trans)

   191   done

   192

   193 lemma rtrancl_subset_rtrancl: "r \<subseteq> s^* ==> r^* \<subseteq> s^*"

   194   apply (drule rtrancl_mono)

   195   apply simp

   196   done

   197

   198 lemma rtranclp_subset: "R \<le> S ==> S \<le> R^** ==> S^** = R^**"

   199   apply (drule rtranclp_mono)

   200   apply (drule rtranclp_mono)

   201   apply simp

   202   done

   203

   204 lemmas rtrancl_subset = rtranclp_subset [to_set]

   205

   206 lemma rtranclp_sup_rtranclp: "(sup (R^**) (S^**))^** = (sup R S)^**"

   207   by (blast intro!: rtranclp_subset intro: rtranclp_mono [THEN predicate2D])

   208

   209 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]

   210

   211 lemma rtranclp_reflcl [simp]: "(R^==)^** = R^**"

   212   by (blast intro!: rtranclp_subset)

   213

   214 lemmas rtrancl_reflcl [simp] = rtranclp_reflcl [to_set]

   215

   216 lemma rtrancl_r_diff_Id: "(r - Id)^* = r^*"

   217   apply (rule sym)

   218   apply (rule rtrancl_subset, blast, clarify)

   219   apply (rename_tac a b)

   220   apply (case_tac "a = b")

   221    apply blast

   222   apply (blast intro!: r_into_rtrancl)

   223   done

   224

   225 lemma rtranclp_r_diff_Id: "(inf r op ~=)^** = r^**"

   226   apply (rule sym)

   227   apply (rule rtranclp_subset)

   228    apply blast+

   229   done

   230

   231 theorem rtranclp_converseD:

   232   assumes r: "(r^--1)^** x y"

   233   shows "r^** y x"

   234 proof -

   235   from r show ?thesis

   236     by induct (iprover intro: rtranclp_trans dest!: conversepD)+

   237 qed

   238

   239 lemmas rtrancl_converseD = rtranclp_converseD [to_set]

   240

   241 theorem rtranclp_converseI:

   242   assumes "r^** y x"

   243   shows "(r^--1)^** x y"

   244   using assms

   245   by induct (iprover intro: rtranclp_trans conversepI)+

   246

   247 lemmas rtrancl_converseI = rtranclp_converseI [to_set]

   248

   249 lemma rtrancl_converse: "(r^-1)^* = (r^*)^-1"

   250   by (fast dest!: rtrancl_converseD intro!: rtrancl_converseI)

   251

   252 lemma sym_rtrancl: "sym r ==> sym (r^*)"

   253   by (simp only: sym_conv_converse_eq rtrancl_converse [symmetric])

   254

   255 theorem converse_rtranclp_induct[consumes 1]:

   256   assumes major: "r^** a b"

   257     and cases: "P b" "!!y z. [| r y z; r^** z b; P z |] ==> P y"

   258   shows "P a"

   259   using rtranclp_converseI [OF major]

   260   by induct (iprover intro: cases dest!: conversepD rtranclp_converseD)+

   261

   262 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]

   263

   264 lemmas converse_rtranclp_induct2 =

   265   converse_rtranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,

   266                  consumes 1, case_names refl step]

   267

   268 lemmas converse_rtrancl_induct2 =

   269   converse_rtrancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),

   270                  consumes 1, case_names refl step]

   271

   272 lemma converse_rtranclpE:

   273   assumes major: "r^** x z"

   274     and cases: "x=z ==> P"

   275       "!!y. [| r x y; r^** y z |] ==> P"

   276   shows P

   277   apply (subgoal_tac "x = z | (EX y. r x y & r^** y z)")

   278    apply (rule_tac [2] major [THEN converse_rtranclp_induct])

   279     prefer 2 apply iprover

   280    prefer 2 apply iprover

   281   apply (erule asm_rl exE disjE conjE cases)+

   282   done

   283

   284 lemmas converse_rtranclE = converse_rtranclpE [to_set]

   285

   286 lemmas converse_rtranclpE2 = converse_rtranclpE [of _ "(xa,xb)" "(za,zb)", split_rule]

   287

   288 lemmas converse_rtranclE2 = converse_rtranclE [of "(xa,xb)" "(za,zb)", split_rule]

   289

   290 lemma r_comp_rtrancl_eq: "r O r^* = r^* O r"

   291   by (blast elim: rtranclE converse_rtranclE

   292     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)

   293

   294 lemma rtrancl_unfold: "r^* = Id Un r O r^*"

   295   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)

   296

   297

   298 subsection {* Transitive closure *}

   299

   300 lemma trancl_mono: "!!p. p \<in> r^+ ==> r \<subseteq> s ==> p \<in> s^+"

   301   apply (simp add: split_tupled_all)

   302   apply (erule trancl.induct)

   303    apply (iprover dest: subsetD)+

   304   done

   305

   306 lemma r_into_trancl': "!!p. p : r ==> p : r^+"

   307   by (simp only: split_tupled_all) (erule r_into_trancl)

   308

   309 text {*

   310   \medskip Conversions between @{text trancl} and @{text rtrancl}.

   311 *}

   312

   313 lemma tranclp_into_rtranclp: "r^++ a b ==> r^** a b"

   314   by (erule tranclp.induct) iprover+

   315

   316 lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set]

   317

   318 lemma rtranclp_into_tranclp1: assumes r: "r^** a b"

   319   shows "!!c. r b c ==> r^++ a c" using r

   320   by induct iprover+

   321

   322 lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]

   323

   324 lemma rtranclp_into_tranclp2: "[| r a b; r^** b c |] ==> r^++ a c"

   325   -- {* intro rule from @{text r} and @{text rtrancl} *}

   326   apply (erule rtranclp.cases)

   327    apply iprover

   328   apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])

   329     apply (simp | rule r_into_rtranclp)+

   330   done

   331

   332 lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]

   333

   334 text {* Nice induction rule for @{text trancl} *}

   335 lemma tranclp_induct [consumes 1, case_names base step, induct pred: tranclp]:

   336   assumes "r^++ a b"

   337   and cases: "!!y. r a y ==> P y"

   338     "!!y z. r^++ a y ==> r y z ==> P y ==> P z"

   339   shows "P b"

   340 proof -

   341   from r^++ a b have "a = a --> P b"

   342     by (induct "%x y. x = a --> P y" a b) (iprover intro: cases)+

   343   then show ?thesis by iprover

   344 qed

   345

   346 lemmas trancl_induct [induct set: trancl] = tranclp_induct [to_set]

   347

   348 lemmas tranclp_induct2 =

   349   tranclp_induct [of _ "(ax,ay)" "(bx,by)", split_rule,

   350     consumes 1, case_names base step]

   351

   352 lemmas trancl_induct2 =

   353   trancl_induct [of "(ax,ay)" "(bx,by)", split_format (complete),

   354     consumes 1, case_names base step]

   355

   356 lemma tranclp_trans_induct:

   357   assumes major: "r^++ x y"

   358     and cases: "!!x y. r x y ==> P x y"

   359       "!!x y z. [| r^++ x y; P x y; r^++ y z; P y z |] ==> P x z"

   360   shows "P x y"

   361   -- {* Another induction rule for trancl, incorporating transitivity *}

   362   by (iprover intro: major [THEN tranclp_induct] cases)

   363

   364 lemmas trancl_trans_induct = tranclp_trans_induct [to_set]

   365

   366 lemma tranclE [cases set: trancl]:

   367   assumes "(a, b) : r^+"

   368   obtains

   369     (base) "(a, b) : r"

   370   | (step) c where "(a, c) : r^+" and "(c, b) : r"

   371   using assms by cases simp_all

   372

   373 lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"

   374   apply (rule subsetI)

   375   apply (rule_tac p = x in PairE)

   376   apply clarify

   377   apply (erule trancl_induct)

   378    apply auto

   379   done

   380

   381 lemma trancl_unfold: "r^+ = r Un r O r^+"

   382   by (auto intro: trancl_into_trancl elim: tranclE)

   383

   384 text {* Transitivity of @{term "r^+"} *}

   385 lemma trans_trancl [simp]: "trans (r^+)"

   386 proof (rule transI)

   387   fix x y z

   388   assume "(x, y) \<in> r^+"

   389   assume "(y, z) \<in> r^+"

   390   then show "(x, z) \<in> r^+"

   391   proof induct

   392     case (base u)

   393     from (x, y) \<in> r^+ and (y, u) \<in> r

   394     show "(x, u) \<in> r^+" ..

   395   next

   396     case (step u v)

   397     from (x, u) \<in> r^+ and (u, v) \<in> r

   398     show "(x, v) \<in> r^+" ..

   399   qed

   400 qed

   401

   402 lemmas trancl_trans = trans_trancl [THEN transD, standard]

   403

   404 lemma tranclp_trans:

   405   assumes xy: "r^++ x y"

   406   and yz: "r^++ y z"

   407   shows "r^++ x z" using yz xy

   408   by induct iprover+

   409

   410 lemma trancl_id [simp]: "trans r \<Longrightarrow> r^+ = r"

   411   apply auto

   412   apply (erule trancl_induct)

   413    apply assumption

   414   apply (unfold trans_def)

   415   apply blast

   416   done

   417

   418 lemma rtranclp_tranclp_tranclp:

   419   assumes "r^** x y"

   420   shows "!!z. r^++ y z ==> r^++ x z" using assms

   421   by induct (iprover intro: tranclp_trans)+

   422

   423 lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set]

   424

   425 lemma tranclp_into_tranclp2: "r a b ==> r^++ b c ==> r^++ a c"

   426   by (erule tranclp_trans [OF tranclp.r_into_trancl])

   427

   428 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]

   429

   430 lemma trancl_insert:

   431   "(insert (y, x) r)^+ = r^+ \<union> {(a, b). (a, y) \<in> r^* \<and> (x, b) \<in> r^*}"

   432   -- {* primitive recursion for @{text trancl} over finite relations *}

   433   apply (rule equalityI)

   434    apply (rule subsetI)

   435    apply (simp only: split_tupled_all)

   436    apply (erule trancl_induct, blast)

   437    apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)

   438   apply (rule subsetI)

   439   apply (blast intro: trancl_mono rtrancl_mono

   440     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)

   441   done

   442

   443 lemma tranclp_converseI: "(r^++)^--1 x y ==> (r^--1)^++ x y"

   444   apply (drule conversepD)

   445   apply (erule tranclp_induct)

   446   apply (iprover intro: conversepI tranclp_trans)+

   447   done

   448

   449 lemmas trancl_converseI = tranclp_converseI [to_set]

   450

   451 lemma tranclp_converseD: "(r^--1)^++ x y ==> (r^++)^--1 x y"

   452   apply (rule conversepI)

   453   apply (erule tranclp_induct)

   454   apply (iprover dest: conversepD intro: tranclp_trans)+

   455   done

   456

   457 lemmas trancl_converseD = tranclp_converseD [to_set]

   458

   459 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"

   460   by (fastsimp simp add: expand_fun_eq

   461     intro!: tranclp_converseI dest!: tranclp_converseD)

   462

   463 lemmas trancl_converse = tranclp_converse [to_set]

   464

   465 lemma sym_trancl: "sym r ==> sym (r^+)"

   466   by (simp only: sym_conv_converse_eq trancl_converse [symmetric])

   467

   468 lemma converse_tranclp_induct:

   469   assumes major: "r^++ a b"

   470     and cases: "!!y. r y b ==> P(y)"

   471       "!!y z.[| r y z;  r^++ z b;  P(z) |] ==> P(y)"

   472   shows "P a"

   473   apply (rule tranclp_induct [OF tranclp_converseI, OF conversepI, OF major])

   474    apply (rule cases)

   475    apply (erule conversepD)

   476   apply (blast intro: prems dest!: tranclp_converseD conversepD)

   477   done

   478

   479 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]

   480

   481 lemma tranclpD: "R^++ x y ==> EX z. R x z \<and> R^** z y"

   482   apply (erule converse_tranclp_induct)

   483    apply auto

   484   apply (blast intro: rtranclp_trans)

   485   done

   486

   487 lemmas tranclD = tranclpD [to_set]

   488

   489 lemma tranclD2:

   490   "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R"

   491   by (blast elim: tranclE intro: trancl_into_rtrancl)

   492

   493 lemma irrefl_tranclI: "r^-1 \<inter> r^* = {} ==> (x, x) \<notin> r^+"

   494   by (blast elim: tranclE dest: trancl_into_rtrancl)

   495

   496 lemma irrefl_trancl_rD: "!!X. ALL x. (x, x) \<notin> r^+ ==> (x, y) \<in> r ==> x \<noteq> y"

   497   by (blast dest: r_into_trancl)

   498

   499 lemma trancl_subset_Sigma_aux:

   500     "(a, b) \<in> r^* ==> r \<subseteq> A \<times> A ==> a = b \<or> a \<in> A"

   501   by (induct rule: rtrancl_induct) auto

   502

   503 lemma trancl_subset_Sigma: "r \<subseteq> A \<times> A ==> r^+ \<subseteq> A \<times> A"

   504   apply (rule subsetI)

   505   apply (simp only: split_tupled_all)

   506   apply (erule tranclE)

   507    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+

   508   done

   509

   510 lemma reflcl_tranclp [simp]: "(r^++)^== = r^**"

   511   apply (safe intro!: order_antisym)

   512    apply (erule tranclp_into_rtranclp)

   513   apply (blast elim: rtranclp.cases dest: rtranclp_into_tranclp1)

   514   done

   515

   516 lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set]

   517

   518 lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"

   519   apply safe

   520    apply (drule trancl_into_rtrancl, simp)

   521   apply (erule rtranclE, safe)

   522    apply (rule r_into_trancl, simp)

   523   apply (rule rtrancl_into_trancl1)

   524    apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)

   525   done

   526

   527 lemma trancl_empty [simp]: "{}^+ = {}"

   528   by (auto elim: trancl_induct)

   529

   530 lemma rtrancl_empty [simp]: "{}^* = Id"

   531   by (rule subst [OF reflcl_trancl]) simp

   532

   533 lemma rtranclpD: "R^** a b ==> a = b \<or> a \<noteq> b \<and> R^++ a b"

   534   by (force simp add: reflcl_tranclp [symmetric] simp del: reflcl_tranclp)

   535

   536 lemmas rtranclD = rtranclpD [to_set]

   537

   538 lemma rtrancl_eq_or_trancl:

   539   "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"

   540   by (fast elim: trancl_into_rtrancl dest: rtranclD)

   541

   542 text {* @{text Domain} and @{text Range} *}

   543

   544 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"

   545   by blast

   546

   547 lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"

   548   by blast

   549

   550 lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"

   551   by (rule rtrancl_Un_rtrancl [THEN subst]) fast

   552

   553 lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"

   554   by (blast intro: subsetD [OF rtrancl_Un_subset])

   555

   556 lemma trancl_domain [simp]: "Domain (r^+) = Domain r"

   557   by (unfold Domain_def) (blast dest: tranclD)

   558

   559 lemma trancl_range [simp]: "Range (r^+) = Range r"

   560 unfolding Range_def by(simp add: trancl_converse [symmetric])

   561

   562 lemma Not_Domain_rtrancl:

   563     "x ~: Domain R ==> ((x, y) : R^*) = (x = y)"

   564   apply auto

   565   apply (erule rev_mp)

   566   apply (erule rtrancl_induct)

   567    apply auto

   568   done

   569

   570 lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"

   571   apply clarify

   572   apply (erule trancl_induct)

   573    apply (auto simp add: Field_def)

   574   done

   575

   576 lemma finite_trancl: "finite (r^+) = finite r"

   577   apply auto

   578    prefer 2

   579    apply (rule trancl_subset_Field2 [THEN finite_subset])

   580    apply (rule finite_SigmaI)

   581     prefer 3

   582     apply (blast intro: r_into_trancl' finite_subset)

   583    apply (auto simp add: finite_Field)

   584   done

   585

   586 text {* More about converse @{text rtrancl} and @{text trancl}, should

   587   be merged with main body. *}

   588

   589 lemma single_valued_confluent:

   590   "\<lbrakk> single_valued r; (x,y) \<in> r^*; (x,z) \<in> r^* \<rbrakk>

   591   \<Longrightarrow> (y,z) \<in> r^* \<or> (z,y) \<in> r^*"

   592   apply (erule rtrancl_induct)

   593   apply simp

   594   apply (erule disjE)

   595    apply (blast elim:converse_rtranclE dest:single_valuedD)

   596   apply(blast intro:rtrancl_trans)

   597   done

   598

   599 lemma r_r_into_trancl: "(a, b) \<in> R ==> (b, c) \<in> R ==> (a, c) \<in> R^+"

   600   by (fast intro: trancl_trans)

   601

   602 lemma trancl_into_trancl [rule_format]:

   603     "(a, b) \<in> r\<^sup>+ ==> (b, c) \<in> r --> (a,c) \<in> r\<^sup>+"

   604   apply (erule trancl_induct)

   605    apply (fast intro: r_r_into_trancl)

   606   apply (fast intro: r_r_into_trancl trancl_trans)

   607   done

   608

   609 lemma tranclp_rtranclp_tranclp:

   610     "r\<^sup>+\<^sup>+ a b ==> r\<^sup>*\<^sup>* b c ==> r\<^sup>+\<^sup>+ a c"

   611   apply (drule tranclpD)

   612   apply (elim exE conjE)

   613   apply (drule rtranclp_trans, assumption)

   614   apply (drule rtranclp_into_tranclp2, assumption, assumption)

   615   done

   616

   617 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]

   618

   619 lemmas transitive_closure_trans [trans] =

   620   r_r_into_trancl trancl_trans rtrancl_trans

   621   trancl.trancl_into_trancl trancl_into_trancl2

   622   rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl

   623   rtrancl_trancl_trancl trancl_rtrancl_trancl

   624

   625 lemmas transitive_closurep_trans' [trans] =

   626   tranclp_trans rtranclp_trans

   627   tranclp.trancl_into_trancl tranclp_into_tranclp2

   628   rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp

   629   rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp

   630

   631 declare trancl_into_rtrancl [elim]

   632

   633

   634 subsection {* Setup of transitivity reasoner *}

   635

   636 ML {*

   637

   638 structure Trancl_Tac = Trancl_Tac_Fun (

   639   struct

   640     val r_into_trancl = @{thm trancl.r_into_trancl};

   641     val trancl_trans  = @{thm trancl_trans};

   642     val rtrancl_refl = @{thm rtrancl.rtrancl_refl};

   643     val r_into_rtrancl = @{thm r_into_rtrancl};

   644     val trancl_into_rtrancl = @{thm trancl_into_rtrancl};

   645     val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};

   646     val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};

   647     val rtrancl_trans = @{thm rtrancl_trans};

   648

   649   fun decomp (@{const Trueprop} $t) =   650 let fun dec (Const ("op :", _)$ (Const ("Pair", _) $a$ b) $rel ) =   651 let fun decr (Const ("Transitive_Closure.rtrancl", _ )$ r) = (r,"r*")

   652               | decr (Const ("Transitive_Closure.trancl", _ ) $r) = (r,"r+")   653 | decr r = (r,"r");   654 val (rel,r) = decr (Envir.beta_eta_contract rel);   655 in SOME (a,b,rel,r) end   656 | dec _ = NONE   657 in dec t end   658 | decomp _ = NONE;   659   660 end);   661   662 structure Tranclp_Tac = Trancl_Tac_Fun (   663 struct   664 val r_into_trancl = @{thm tranclp.r_into_trancl};   665 val trancl_trans = @{thm tranclp_trans};   666 val rtrancl_refl = @{thm rtranclp.rtrancl_refl};   667 val r_into_rtrancl = @{thm r_into_rtranclp};   668 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};   669 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};   670 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};   671 val rtrancl_trans = @{thm rtranclp_trans};   672   673 fun decomp (@{const Trueprop}$ t) =

   674     let fun dec (rel $a$ b) =

   675         let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $r) = (r,"r*")   676 | decr (Const ("Transitive_Closure.tranclp", _ )$ r)  = (r,"r+")

   677               | decr r = (r,"r");

   678             val (rel,r) = decr rel;

   679         in SOME (a, b, rel, r) end

   680       | dec _ =  NONE

   681     in dec t end

   682     | decomp _ = NONE;

   683

   684   end);

   685 *}

   686

   687 declaration {* fn _ =>

   688   Simplifier.map_ss (fn ss => ss

   689     addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))

   690     addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac))

   691     addSolver (mk_solver "Tranclp" (fn _ => Tranclp_Tac.trancl_tac))

   692     addSolver (mk_solver "Rtranclp" (fn _ => Tranclp_Tac.rtrancl_tac)))

   693 *}

   694

   695 (* Optional methods *)

   696

   697 method_setup trancl =

   698   {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *}

   699   {* simple transitivity reasoner *}

   700 method_setup rtrancl =

   701   {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *}

   702   {* simple transitivity reasoner *}

   703 method_setup tranclp =

   704   {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *}

   705   {* simple transitivity reasoner (predicate version) *}

   706 method_setup rtranclp =

   707   {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *}

   708   {* simple transitivity reasoner (predicate version) *}

   709

   710 end