src/HOL/Transitive_Closure.thy
 author bulwahn Thu Jun 11 22:17:13 2009 +0200 (2009-06-11) changeset 31576 525073f7aff6 parent 31351 b8d856545a02 child 31577 ce3721fa1e17 permissions -rw-r--r--
     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 converse_tranclpE:

   482   assumes "tranclp r x z "

   483   assumes "r x z ==> P"

   484   assumes "\<And> y. [| r x y; tranclp r y z |] ==> P"

   485   shows P

   486 proof -

   487   from tranclpD[OF assms(1)]

   488   obtain y where "r x y" and "rtranclp r y z" by iprover

   489   with assms(2-3) rtranclpD[OF this(2)] this(1)

   490   show P by iprover

   491 qed

   492

   493 lemmas converse_tranclE = converse_tranclpE [to_set]

   494

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

   496   apply (erule converse_tranclp_induct)

   497    apply auto

   498   apply (blast intro: rtranclp_trans)

   499   done

   500

   501 lemmas tranclD = tranclpD [to_set]

   502

   503 lemma tranclD2:

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

   505   by (blast elim: tranclE intro: trancl_into_rtrancl)

   506

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

   508   by (blast elim: tranclE dest: trancl_into_rtrancl)

   509

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

   511   by (blast dest: r_into_trancl)

   512

   513 lemma trancl_subset_Sigma_aux:

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

   515   by (induct rule: rtrancl_induct) auto

   516

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

   518   apply (rule subsetI)

   519   apply (simp only: split_tupled_all)

   520   apply (erule tranclE)

   521    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+

   522   done

   523

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

   525   apply (safe intro!: order_antisym)

   526    apply (erule tranclp_into_rtranclp)

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

   528   done

   529

   530 lemmas reflcl_trancl [simp] = reflcl_tranclp [to_set]

   531

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

   533   apply safe

   534    apply (drule trancl_into_rtrancl, simp)

   535   apply (erule rtranclE, safe)

   536    apply (rule r_into_trancl, simp)

   537   apply (rule rtrancl_into_trancl1)

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

   539   done

   540

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

   542   by (auto elim: trancl_induct)

   543

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

   545   by (rule subst [OF reflcl_trancl]) simp

   546

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

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

   549

   550 lemmas rtranclD = rtranclpD [to_set]

   551

   552 lemma rtrancl_eq_or_trancl:

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

   554   by (fast elim: trancl_into_rtrancl dest: rtranclD)

   555

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

   557

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

   559   by blast

   560

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

   562   by blast

   563

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

   565   by (rule rtrancl_Un_rtrancl [THEN subst]) fast

   566

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

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

   569

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

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

   572

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

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

   575

   576 lemma Not_Domain_rtrancl:

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

   578   apply auto

   579   apply (erule rev_mp)

   580   apply (erule rtrancl_induct)

   581    apply auto

   582   done

   583

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

   585   apply clarify

   586   apply (erule trancl_induct)

   587    apply (auto simp add: Field_def)

   588   done

   589

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

   591   apply auto

   592    prefer 2

   593    apply (rule trancl_subset_Field2 [THEN finite_subset])

   594    apply (rule finite_SigmaI)

   595     prefer 3

   596     apply (blast intro: r_into_trancl' finite_subset)

   597    apply (auto simp add: finite_Field)

   598   done

   599

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

   601   be merged with main body. *}

   602

   603 lemma single_valued_confluent:

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

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

   606   apply (erule rtrancl_induct)

   607   apply simp

   608   apply (erule disjE)

   609    apply (blast elim:converse_rtranclE dest:single_valuedD)

   610   apply(blast intro:rtrancl_trans)

   611   done

   612

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

   614   by (fast intro: trancl_trans)

   615

   616 lemma trancl_into_trancl [rule_format]:

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

   618   apply (erule trancl_induct)

   619    apply (fast intro: r_r_into_trancl)

   620   apply (fast intro: r_r_into_trancl trancl_trans)

   621   done

   622

   623 lemma tranclp_rtranclp_tranclp:

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

   625   apply (drule tranclpD)

   626   apply (elim exE conjE)

   627   apply (drule rtranclp_trans, assumption)

   628   apply (drule rtranclp_into_tranclp2, assumption, assumption)

   629   done

   630

   631 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]

   632

   633 lemmas transitive_closure_trans [trans] =

   634   r_r_into_trancl trancl_trans rtrancl_trans

   635   trancl.trancl_into_trancl trancl_into_trancl2

   636   rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl

   637   rtrancl_trancl_trancl trancl_rtrancl_trancl

   638

   639 lemmas transitive_closurep_trans' [trans] =

   640   tranclp_trans rtranclp_trans

   641   tranclp.trancl_into_trancl tranclp_into_tranclp2

   642   rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp

   643   rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp

   644

   645 declare trancl_into_rtrancl [elim]

   646

   647 subsection {* The power operation on relations *}

   648

   649 text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}

   650

   651 overloading

   652   relpow == "compow :: nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"

   653 begin

   654

   655 primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where

   656     "relpow 0 R = Id"

   657   | "relpow (Suc n) R = R O (R ^^ n)"

   658

   659 end

   660

   661 lemma rel_pow_1 [simp]:

   662   fixes R :: "('a \<times> 'a) set"

   663   shows "R ^^ 1 = R"

   664   by simp

   665

   666 lemma rel_pow_0_I:

   667   "(x, x) \<in> R ^^ 0"

   668   by simp

   669

   670 lemma rel_pow_Suc_I:

   671   "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"

   672   by auto

   673

   674 lemma rel_pow_Suc_I2:

   675   "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"

   676   by (induct n arbitrary: z) (simp, fastsimp)

   677

   678 lemma rel_pow_0_E:

   679   "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"

   680   by simp

   681

   682 lemma rel_pow_Suc_E:

   683   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"

   684   by auto

   685

   686 lemma rel_pow_E:

   687   "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)

   688    \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)

   689    \<Longrightarrow> P"

   690   by (cases n) auto

   691

   692 lemma rel_pow_Suc_D2:

   693   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"

   694   apply (induct n arbitrary: x z)

   695    apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)

   696   apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)

   697   done

   698

   699 lemma rel_pow_Suc_E2:

   700   "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P"

   701   by (blast dest: rel_pow_Suc_D2)

   702

   703 lemma rel_pow_Suc_D2':

   704   "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)"

   705   by (induct n) (simp_all, blast)

   706

   707 lemma rel_pow_E2:

   708   "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)

   709      \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)

   710    \<Longrightarrow> P"

   711   apply (cases n, simp)

   712   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)

   713   done

   714

   715 lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"

   716 by(induct n) auto

   717

   718 lemma rtrancl_imp_UN_rel_pow:

   719   assumes "p \<in> R^*"

   720   shows "p \<in> (\<Union>n. R ^^ n)"

   721 proof (cases p)

   722   case (Pair x y)

   723   with assms have "(x, y) \<in> R^*" by simp

   724   then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct

   725     case base show ?case by (blast intro: rel_pow_0_I)

   726   next

   727     case step then show ?case by (blast intro: rel_pow_Suc_I)

   728   qed

   729   with Pair show ?thesis by simp

   730 qed

   731

   732 lemma rel_pow_imp_rtrancl:

   733   assumes "p \<in> R ^^ n"

   734   shows "p \<in> R^*"

   735 proof (cases p)

   736   case (Pair x y)

   737   with assms have "(x, y) \<in> R ^^ n" by simp

   738   then have "(x, y) \<in> R^*" proof (induct n arbitrary: x y)

   739     case 0 then show ?case by simp

   740   next

   741     case Suc then show ?case

   742       by (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)

   743   qed

   744   with Pair show ?thesis by simp

   745 qed

   746

   747 lemma rtrancl_is_UN_rel_pow:

   748   "R^* = (\<Union>n. R ^^ n)"

   749   by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)

   750

   751 lemma rtrancl_power:

   752   "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)"

   753   by (simp add: rtrancl_is_UN_rel_pow)

   754

   755 lemma trancl_power:

   756   "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)"

   757   apply (cases p)

   758   apply simp

   759   apply (rule iffI)

   760    apply (drule tranclD2)

   761    apply (clarsimp simp: rtrancl_is_UN_rel_pow)

   762    apply (rule_tac x="Suc n" in exI)

   763    apply (clarsimp simp: rel_comp_def)

   764    apply fastsimp

   765   apply clarsimp

   766   apply (case_tac n, simp)

   767   apply clarsimp

   768   apply (drule rel_pow_imp_rtrancl)

   769   apply (drule rtrancl_into_trancl1) apply auto

   770   done

   771

   772 lemma rtrancl_imp_rel_pow:

   773   "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n"

   774   by (auto dest: rtrancl_imp_UN_rel_pow)

   775

   776 lemma single_valued_rel_pow:

   777   fixes R :: "('a * 'a) set"

   778   shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"

   779   apply (induct n arbitrary: R)

   780   apply simp_all

   781   apply (rule single_valuedI)

   782   apply (fast dest: single_valuedD elim: rel_pow_Suc_E)

   783   done

   784

   785 subsection {* Setup of transitivity reasoner *}

   786

   787 ML {*

   788

   789 structure Trancl_Tac = Trancl_Tac_Fun (

   790   struct

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

   792     val trancl_trans  = @{thm trancl_trans};

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

   794     val r_into_rtrancl = @{thm r_into_rtrancl};

   795     val trancl_into_rtrancl = @{thm trancl_into_rtrancl};

   796     val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};

   797     val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};

   798     val rtrancl_trans = @{thm rtrancl_trans};

   799

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

   803               | decr (Const ("Transitive_Closure.trancl", _ ) $r) = (r,"r+")   804 | decr r = (r,"r");   805 val (rel,r) = decr (Envir.beta_eta_contract rel);   806 in SOME (a,b,rel,r) end   807 | dec _ = NONE   808 in dec t end   809 | decomp _ = NONE;   810   811 end);   812   813 structure Tranclp_Tac = Trancl_Tac_Fun (   814 struct   815 val r_into_trancl = @{thm tranclp.r_into_trancl};   816 val trancl_trans = @{thm tranclp_trans};   817 val rtrancl_refl = @{thm rtranclp.rtrancl_refl};   818 val r_into_rtrancl = @{thm r_into_rtranclp};   819 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};   820 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};   821 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};   822 val rtrancl_trans = @{thm rtranclp_trans};   823   824 fun decomp (@{const Trueprop}$ t) =

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

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

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

   829             val (rel,r) = decr rel;

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

   831       | dec _ =  NONE

   832     in dec t end

   833     | decomp _ = NONE;

   834

   835   end);

   836 *}

   837

   838 declaration {* fn _ =>

   839   Simplifier.map_ss (fn ss => ss

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

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

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

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

   844 *}

   845

   846 (* Optional methods *)

   847

   848 method_setup trancl =

   849   {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.trancl_tac)) *}

   850   {* simple transitivity reasoner *}

   851 method_setup rtrancl =

   852   {* Scan.succeed (K (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac)) *}

   853   {* simple transitivity reasoner *}

   854 method_setup tranclp =

   855   {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.trancl_tac)) *}

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

   857 method_setup rtranclp =

   858   {* Scan.succeed (K (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac)) *}

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

   860

   861 end