src/HOL/Transitive_Closure.thy
 author wenzelm Wed Sep 17 21:27:14 2008 +0200 (2008-09-17) changeset 28263 69eaa97e7e96 parent 26801 244184661a09 child 29609 a010aab5bed0 permissions -rw-r--r--
moved global ML bindings to global place;
     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 closure *}

    67

    68 lemma reflexive_reflcl[simp]: "reflexive(r^=)"

    69 by(simp add:refl_def)

    70

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

    72 by(simp add:antisym_def)

    73

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

    75 unfolding trans_def by blast

    76

    77

    78 subsection {* Reflexive-transitive closure *}

    79

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

    81   by (simp add: expand_fun_eq)

    82

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

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

    85   apply (simp only: split_tupled_all)

    86   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])

    87   done

    88

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

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

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

    92

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

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

    95   apply (rule predicate2I)

    96   apply (erule rtranclp.induct)

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

    98   done

    99

   100 lemmas rtrancl_mono = rtranclp_mono [to_set]

   101

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

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

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

   105   shows "P b"

   106 proof -

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

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

   109   then show ?thesis by iprover

   110 qed

   111

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

   113

   114 lemmas rtranclp_induct2 =

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

   116                  consumes 1, case_names refl step]

   117

   118 lemmas rtrancl_induct2 =

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

   120                  consumes 1, case_names refl step]

   121

   122 lemma reflexive_rtrancl: "reflexive (r^*)"

   123   by (unfold refl_def) fast

   124

   125 text {* Transitivity of transitive closure. *}

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

   127 proof (rule transI)

   128   fix x y z

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

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

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

   132   proof induct

   133     case base

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

   135   next

   136     case (step u v)

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

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

   139   qed

   140 qed

   141

   142 lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]

   143

   144 lemma rtranclp_trans:

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

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

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

   148   by induct iprover+

   149

   150 lemma rtranclE [cases set: rtrancl]:

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

   152   obtains

   153     (base) "a = b"

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

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

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

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

   158     prefer 2 apply blast

   159    prefer 2 apply blast

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

   161   done

   162

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

   164   apply (rule subsetI)

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

   166   apply (erule rtrancl_induct, auto)

   167   done

   168

   169 lemma converse_rtranclp_into_rtranclp:

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

   171   by (rule rtranclp_trans) iprover+

   172

   173 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]

   174

   175 text {*

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

   177 *}

   178

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

   180   apply (auto intro!: order_antisym)

   181   apply (erule rtranclp_induct)

   182    apply (rule rtranclp.rtrancl_refl)

   183   apply (blast intro: rtranclp_trans)

   184   done

   185

   186 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]

   187

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

   189   apply (rule set_ext)

   190   apply (simp only: split_tupled_all)

   191   apply (blast intro: rtrancl_trans)

   192   done

   193

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

   195   apply (drule rtrancl_mono)

   196   apply simp

   197   done

   198

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

   200   apply (drule rtranclp_mono)

   201   apply (drule rtranclp_mono)

   202   apply simp

   203   done

   204

   205 lemmas rtrancl_subset = rtranclp_subset [to_set]

   206

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

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

   209

   210 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]

   211

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

   213   by (blast intro!: rtranclp_subset)

   214

   215 lemmas rtrancl_reflcl [simp] = rtranclp_reflcl [to_set]

   216

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

   218   apply (rule sym)

   219   apply (rule rtrancl_subset, blast, clarify)

   220   apply (rename_tac a b)

   221   apply (case_tac "a = b")

   222    apply blast

   223   apply (blast intro!: r_into_rtrancl)

   224   done

   225

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

   227   apply (rule sym)

   228   apply (rule rtranclp_subset)

   229    apply blast+

   230   done

   231

   232 theorem rtranclp_converseD:

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

   234   shows "r^** y x"

   235 proof -

   236   from r show ?thesis

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

   238 qed

   239

   240 lemmas rtrancl_converseD = rtranclp_converseD [to_set]

   241

   242 theorem rtranclp_converseI:

   243   assumes "r^** y x"

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

   245   using assms

   246   by induct (iprover intro: rtranclp_trans conversepI)+

   247

   248 lemmas rtrancl_converseI = rtranclp_converseI [to_set]

   249

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

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

   252

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

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

   255

   256 theorem converse_rtranclp_induct[consumes 1]:

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

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

   259   shows "P a"

   260   using rtranclp_converseI [OF major]

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

   262

   263 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]

   264

   265 lemmas converse_rtranclp_induct2 =

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

   267                  consumes 1, case_names refl step]

   268

   269 lemmas converse_rtrancl_induct2 =

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

   271                  consumes 1, case_names refl step]

   272

   273 lemma converse_rtranclpE:

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

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

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

   277   shows P

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

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

   280     prefer 2 apply iprover

   281    prefer 2 apply iprover

   282   apply (erule asm_rl exE disjE conjE cases)+

   283   done

   284

   285 lemmas converse_rtranclE = converse_rtranclpE [to_set]

   286

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

   288

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

   290

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

   292   by (blast elim: rtranclE converse_rtranclE

   293     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)

   294

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

   296   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)

   297

   298

   299 subsection {* Transitive closure *}

   300

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

   302   apply (simp add: split_tupled_all)

   303   apply (erule trancl.induct)

   304    apply (iprover dest: subsetD)+

   305   done

   306

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

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

   309

   310 text {*

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

   312 *}

   313

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

   315   by (erule tranclp.induct) iprover+

   316

   317 lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set]

   318

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

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

   321   by induct iprover+

   322

   323 lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]

   324

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

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

   327   apply (erule rtranclp.cases)

   328    apply iprover

   329   apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])

   330     apply (simp | rule r_into_rtranclp)+

   331   done

   332

   333 lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]

   334

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

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

   337   assumes "r^++ a b"

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

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

   340   shows "P b"

   341 proof -

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

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

   344   then show ?thesis by iprover

   345 qed

   346

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

   348

   349 lemmas tranclp_induct2 =

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

   351     consumes 1, case_names base step]

   352

   353 lemmas trancl_induct2 =

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

   355     consumes 1, case_names base step]

   356

   357 lemma tranclp_trans_induct:

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

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

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

   361   shows "P x y"

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

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

   364

   365 lemmas trancl_trans_induct = tranclp_trans_induct [to_set]

   366

   367 lemma tranclE [cases set: trancl]:

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

   369   obtains

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

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

   372   using assms by cases simp_all

   373

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

   375   apply (rule subsetI)

   376   apply (rule_tac p = x in PairE)

   377   apply clarify

   378   apply (erule trancl_induct)

   379    apply auto

   380   done

   381

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

   383   by (auto intro: trancl_into_trancl elim: tranclE)

   384

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

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

   387 proof (rule transI)

   388   fix x y z

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

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

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

   392   proof induct

   393     case (base u)

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

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

   396   next

   397     case (step u v)

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

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

   400   qed

   401 qed

   402

   403 lemmas trancl_trans = trans_trancl [THEN transD, standard]

   404

   405 lemma tranclp_trans:

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

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

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

   409   by induct iprover+

   410

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

   412   apply auto

   413   apply (erule trancl_induct)

   414    apply assumption

   415   apply (unfold trans_def)

   416   apply blast

   417   done

   418

   419 lemma rtranclp_tranclp_tranclp:

   420   assumes "r^** x y"

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

   422   by induct (iprover intro: tranclp_trans)+

   423

   424 lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set]

   425

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

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

   428

   429 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]

   430

   431 lemma trancl_insert:

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

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

   434   apply (rule equalityI)

   435    apply (rule subsetI)

   436    apply (simp only: split_tupled_all)

   437    apply (erule trancl_induct, blast)

   438    apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl r_into_trancl trancl_trans)

   439   apply (rule subsetI)

   440   apply (blast intro: trancl_mono rtrancl_mono

   441     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)

   442   done

   443

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

   445   apply (drule conversepD)

   446   apply (erule tranclp_induct)

   447   apply (iprover intro: conversepI tranclp_trans)+

   448   done

   449

   450 lemmas trancl_converseI = tranclp_converseI [to_set]

   451

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

   453   apply (rule conversepI)

   454   apply (erule tranclp_induct)

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

   456   done

   457

   458 lemmas trancl_converseD = tranclp_converseD [to_set]

   459

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

   461   by (fastsimp simp add: expand_fun_eq

   462     intro!: tranclp_converseI dest!: tranclp_converseD)

   463

   464 lemmas trancl_converse = tranclp_converse [to_set]

   465

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

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

   468

   469 lemma converse_tranclp_induct:

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

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

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

   473   shows "P a"

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

   475    apply (rule cases)

   476    apply (erule conversepD)

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

   478   done

   479

   480 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]

   481

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

   483   apply (erule converse_tranclp_induct)

   484    apply auto

   485   apply (blast intro: rtranclp_trans)

   486   done

   487

   488 lemmas tranclD = tranclpD [to_set]

   489

   490 lemma tranclD2:

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

   492   by (blast elim: tranclE intro: trancl_into_rtrancl)

   493

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

   495   by (blast elim: tranclE dest: trancl_into_rtrancl)

   496

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

   498   by (blast dest: r_into_trancl)

   499

   500 lemma trancl_subset_Sigma_aux:

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

   502   by (induct rule: rtrancl_induct) auto

   503

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

   505   apply (rule subsetI)

   506   apply (simp only: split_tupled_all)

   507   apply (erule tranclE)

   508    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+

   509   done

   510

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

   512   apply (safe intro!: order_antisym)

   513    apply (erule tranclp_into_rtranclp)

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

   515   done

   516

   517 lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set]

   518

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

   520   apply safe

   521    apply (drule trancl_into_rtrancl, simp)

   522   apply (erule rtranclE, safe)

   523    apply (rule r_into_trancl, simp)

   524   apply (rule rtrancl_into_trancl1)

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

   526   done

   527

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

   529   by (auto elim: trancl_induct)

   530

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

   532   by (rule subst [OF reflcl_trancl]) simp

   533

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

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

   536

   537 lemmas rtranclD = rtranclpD [to_set]

   538

   539 lemma rtrancl_eq_or_trancl:

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

   541   by (fast elim: trancl_into_rtrancl dest: rtranclD)

   542

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

   544

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

   546   by blast

   547

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

   549   by blast

   550

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

   552   by (rule rtrancl_Un_rtrancl [THEN subst]) fast

   553

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

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

   556

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

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

   559

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

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

   562

   563 lemma Not_Domain_rtrancl:

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

   565   apply auto

   566   apply (erule rev_mp)

   567   apply (erule rtrancl_induct)

   568    apply auto

   569   done

   570

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

   572   be merged with main body. *}

   573

   574 lemma single_valued_confluent:

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

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

   577   apply (erule rtrancl_induct)

   578   apply simp

   579   apply (erule disjE)

   580    apply (blast elim:converse_rtranclE dest:single_valuedD)

   581   apply(blast intro:rtrancl_trans)

   582   done

   583

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

   585   by (fast intro: trancl_trans)

   586

   587 lemma trancl_into_trancl [rule_format]:

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

   589   apply (erule trancl_induct)

   590    apply (fast intro: r_r_into_trancl)

   591   apply (fast intro: r_r_into_trancl trancl_trans)

   592   done

   593

   594 lemma tranclp_rtranclp_tranclp:

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

   596   apply (drule tranclpD)

   597   apply (elim exE conjE)

   598   apply (drule rtranclp_trans, assumption)

   599   apply (drule rtranclp_into_tranclp2, assumption, assumption)

   600   done

   601

   602 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]

   603

   604 lemmas transitive_closure_trans [trans] =

   605   r_r_into_trancl trancl_trans rtrancl_trans

   606   trancl.trancl_into_trancl trancl_into_trancl2

   607   rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl

   608   rtrancl_trancl_trancl trancl_rtrancl_trancl

   609

   610 lemmas transitive_closurep_trans' [trans] =

   611   tranclp_trans rtranclp_trans

   612   tranclp.trancl_into_trancl tranclp_into_tranclp2

   613   rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp

   614   rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp

   615

   616 declare trancl_into_rtrancl [elim]

   617

   618

   619 subsection {* Setup of transitivity reasoner *}

   620

   621 ML {*

   622

   623 structure Trancl_Tac = Trancl_Tac_Fun (

   624   struct

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

   626     val trancl_trans  = @{thm trancl_trans};

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

   628     val r_into_rtrancl = @{thm r_into_rtrancl};

   629     val trancl_into_rtrancl = @{thm trancl_into_rtrancl};

   630     val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};

   631     val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};

   632     val rtrancl_trans = @{thm rtrancl_trans};

   633

   634   fun decomp (Trueprop $t) =   635 let fun dec (Const ("op :", _)$ (Const ("Pair", _) $a$ b) $rel ) =   636 let fun decr (Const ("Transitive_Closure.rtrancl", _ )$ r) = (r,"r*")

   637               | decr (Const ("Transitive_Closure.trancl", _ ) $r) = (r,"r+")   638 | decr r = (r,"r");   639 val (rel,r) = decr (Envir.beta_eta_contract rel);   640 in SOME (a,b,rel,r) end   641 | dec _ = NONE   642 in dec t end;   643   644 end);   645   646 structure Tranclp_Tac = Trancl_Tac_Fun (   647 struct   648 val r_into_trancl = @{thm tranclp.r_into_trancl};   649 val trancl_trans = @{thm tranclp_trans};   650 val rtrancl_refl = @{thm rtranclp.rtrancl_refl};   651 val r_into_rtrancl = @{thm r_into_rtranclp};   652 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};   653 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};   654 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};   655 val rtrancl_trans = @{thm rtranclp_trans};   656   657 fun decomp (Trueprop$ t) =

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

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

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

   662             val (rel,r) = decr rel;

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

   664       | dec _ =  NONE

   665     in dec t end;

   666

   667   end);

   668 *}

   669

   670 declaration {* fn _ =>

   671   Simplifier.map_ss (fn ss => ss

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

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

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

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

   676 *}

   677

   678 (* Optional methods *)

   679

   680 method_setup trancl =

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

   682   {* simple transitivity reasoner *}

   683 method_setup rtrancl =

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

   685   {* simple transitivity reasoner *}

   686 method_setup tranclp =

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

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

   689 method_setup rtranclp =

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

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

   692

   693 end