src/HOL/Transitive_Closure.thy
 author wenzelm Mon Dec 28 21:47:32 2015 +0100 (2015-12-28) changeset 61955 e96292f32c3c parent 61799 4cf66f21b764 child 62093 bd73a2279fcd permissions -rw-r--r--
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
     1 (*  Title:      HOL/Transitive_Closure.thy

     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory

     3     Copyright   1992  University of Cambridge

     4 *)

     5

     6 section \<open>Reflexive and Transitive closure of a relation\<close>

     7

     8 theory Transitive_Closure

     9 imports Relation

    10 begin

    11

    12 ML_file "~~/src/Provers/trancl.ML"

    13

    14 text \<open>

    15   \<open>rtrancl\<close> is reflexive/transitive closure,

    16   \<open>trancl\<close> is transitive closure,

    17   \<open>reflcl\<close> is reflexive closure.

    18

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

    20   operands to be atomic.

    21 \<close>

    22

    23 context

    24   notes [[inductive_defs]]

    25 begin

    26

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

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

    29 where

    30   rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"

    31 | rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"

    32

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

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

    35 where

    36   r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"

    37 | trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"

    38

    39 notation

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

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

    42

    43 declare

    44   rtrancl_def [nitpick_unfold del]

    45   rtranclp_def [nitpick_unfold del]

    46   trancl_def [nitpick_unfold del]

    47   tranclp_def [nitpick_unfold del]

    48

    49 end

    50

    51 abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>=)" [1000] 999)

    52   where "r\<^sup>= \<equiv> r \<union> Id"

    53

    54 abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(_\<^sup>=\<^sup>=)" [1000] 1000)

    55   where "r\<^sup>=\<^sup>= \<equiv> sup r op ="

    56

    57 notation (ASCII)

    58   rtrancl  ("(_^*)" [1000] 999) and

    59   trancl  ("(_^+)" [1000] 999) and

    60   reflcl  ("(_^=)" [1000] 999) and

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

    62   tranclp  ("(_^++)" [1000] 1000) and

    63   reflclp  ("(_^==)" [1000] 1000)

    64

    65

    66 subsection \<open>Reflexive closure\<close>

    67

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

    69 by(simp add:refl_on_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 lemma reflclp_idemp [simp]: "(P^==)^==  =  P^=="

    78 by blast

    79

    80 subsection \<open>Reflexive-transitive closure\<close>

    81

    82 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"

    83   by (auto simp add: fun_eq_iff)

    84

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

    86   \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>

    87   apply (simp only: split_tupled_all)

    88   apply (erule rtrancl_refl [THEN rtrancl_into_rtrancl])

    89   done

    90

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

    92   \<comment> \<open>\<open>rtrancl\<close> of \<open>r\<close> contains \<open>r\<close>\<close>

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

    94

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

    96   \<comment> \<open>monotonicity of \<open>rtrancl\<close>\<close>

    97   apply (rule predicate2I)

    98   apply (erule rtranclp.induct)

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

   100   done

   101

   102 lemma mono_rtranclp[mono]:

   103    "(\<And>a b. x a b \<longrightarrow> y a b) \<Longrightarrow> x^** a b \<longrightarrow> y^** a b"

   104    using rtranclp_mono[of x y] by auto

   105

   106 lemmas rtrancl_mono = rtranclp_mono [to_set]

   107

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

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

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

   111   shows "P b" using a

   112   by (induct x\<equiv>a b) (rule cases)+

   113

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

   115

   116 lemmas rtranclp_induct2 =

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

   118                  consumes 1, case_names refl step]

   119

   120 lemmas rtrancl_induct2 =

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

   122                  consumes 1, case_names refl step]

   123

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

   125 by (unfold refl_on_def) fast

   126

   127 text \<open>Transitivity of transitive closure.\<close>

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

   129 proof (rule transI)

   130   fix x y z

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

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

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

   134   proof induct

   135     case base

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

   137   next

   138     case (step u v)

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

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

   141   qed

   142 qed

   143

   144 lemmas rtrancl_trans = trans_rtrancl [THEN transD]

   145

   146 lemma rtranclp_trans:

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

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

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

   150   by induct iprover+

   151

   152 lemma rtranclE [cases set: rtrancl]:

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

   154   obtains

   155     (base) "a = b"

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

   157   \<comment> \<open>elimination of \<open>rtrancl\<close> -- by induction on a special formula\<close>

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

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

   160     prefer 2 apply blast

   161    prefer 2 apply blast

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

   163   done

   164

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

   166   apply (rule subsetI)

   167   apply auto

   168   apply (erule rtrancl_induct)

   169   apply auto

   170   done

   171

   172 lemma converse_rtranclp_into_rtranclp:

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

   174   by (rule rtranclp_trans) iprover+

   175

   176 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]

   177

   178 text \<open>

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

   180 \<close>

   181

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

   183   apply (auto intro!: order_antisym)

   184   apply (erule rtranclp_induct)

   185    apply (rule rtranclp.rtrancl_refl)

   186   apply (blast intro: rtranclp_trans)

   187   done

   188

   189 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]

   190

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

   192   apply (rule set_eqI)

   193   apply (simp only: split_tupled_all)

   194   apply (blast intro: rtrancl_trans)

   195   done

   196

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

   198   apply (drule rtrancl_mono)

   199   apply simp

   200   done

   201

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

   203   apply (drule rtranclp_mono)

   204   apply (drule rtranclp_mono)

   205   apply simp

   206   done

   207

   208 lemmas rtrancl_subset = rtranclp_subset [to_set]

   209

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

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

   212

   213 lemmas rtrancl_Un_rtrancl = rtranclp_sup_rtranclp [to_set]

   214

   215 lemma rtranclp_reflclp [simp]: "(R^==)^** = R^**"

   216 by (blast intro!: rtranclp_subset)

   217

   218 lemmas rtrancl_reflcl [simp] = rtranclp_reflclp [to_set]

   219

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

   221   apply (rule sym)

   222   apply (rule rtrancl_subset, blast, clarify)

   223   apply (rename_tac a b)

   224   apply (case_tac "a = b")

   225    apply blast

   226   apply blast

   227   done

   228

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

   230   apply (rule sym)

   231   apply (rule rtranclp_subset)

   232    apply blast+

   233   done

   234

   235 theorem rtranclp_converseD:

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

   237   shows "r^** y x"

   238 proof -

   239   from r show ?thesis

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

   241 qed

   242

   243 lemmas rtrancl_converseD = rtranclp_converseD [to_set]

   244

   245 theorem rtranclp_converseI:

   246   assumes "r^** y x"

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

   248   using assms

   249   by induct (iprover intro: rtranclp_trans conversepI)+

   250

   251 lemmas rtrancl_converseI = rtranclp_converseI [to_set]

   252

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

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

   255

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

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

   258

   259 theorem converse_rtranclp_induct [consumes 1, case_names base step]:

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

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

   262   shows "P a"

   263   using rtranclp_converseI [OF major]

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

   265

   266 lemmas converse_rtrancl_induct = converse_rtranclp_induct [to_set]

   267

   268 lemmas converse_rtranclp_induct2 =

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

   270                  consumes 1, case_names refl step]

   271

   272 lemmas converse_rtrancl_induct2 =

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

   274                  consumes 1, case_names refl step]

   275

   276 lemma converse_rtranclpE [consumes 1, case_names base step]:

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

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

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

   280   shows P

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

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

   283     prefer 2 apply iprover

   284    prefer 2 apply iprover

   285   apply (erule asm_rl exE disjE conjE cases)+

   286   done

   287

   288 lemmas converse_rtranclE = converse_rtranclpE [to_set]

   289

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

   291

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

   293

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

   295   by (blast elim: rtranclE converse_rtranclE

   296     intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)

   297

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

   299   by (auto intro: rtrancl_into_rtrancl elim: rtranclE)

   300

   301 lemma rtrancl_Un_separatorE:

   302   "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (a,x) : P^* \<longrightarrow> (x,y) : Q \<longrightarrow> x=y \<Longrightarrow> (a,b) : P^*"

   303 apply (induct rule:rtrancl.induct)

   304  apply blast

   305 apply (blast intro:rtrancl_trans)

   306 done

   307

   308 lemma rtrancl_Un_separator_converseE:

   309   "(a,b) : (P \<union> Q)^* \<Longrightarrow> \<forall>x y. (x,b) : P^* \<longrightarrow> (y,x) : Q \<longrightarrow> y=x \<Longrightarrow> (a,b) : P^*"

   310 apply (induct rule:converse_rtrancl_induct)

   311  apply blast

   312 apply (blast intro:rtrancl_trans)

   313 done

   314

   315 lemma Image_closed_trancl:

   316   assumes "r  X \<subseteq> X" shows "r\<^sup>*  X = X"

   317 proof -

   318   from assms have **: "{y. \<exists>x\<in>X. (x, y) \<in> r} \<subseteq> X" by auto

   319   have "\<And>x y. (y, x) \<in> r\<^sup>* \<Longrightarrow> y \<in> X \<Longrightarrow> x \<in> X"

   320   proof -

   321     fix x y

   322     assume *: "y \<in> X"

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

   324     then show "x \<in> X"

   325     proof induct

   326       case base show ?case by (fact *)

   327     next

   328       case step with ** show ?case by auto

   329     qed

   330   qed

   331   then show ?thesis by auto

   332 qed

   333

   334

   335 subsection \<open>Transitive closure\<close>

   336

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

   338   apply (simp add: split_tupled_all)

   339   apply (erule trancl.induct)

   340    apply (iprover dest: subsetD)+

   341   done

   342

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

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

   345

   346 text \<open>

   347   \medskip Conversions between \<open>trancl\<close> and \<open>rtrancl\<close>.

   348 \<close>

   349

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

   351   by (erule tranclp.induct) iprover+

   352

   353 lemmas trancl_into_rtrancl = tranclp_into_rtranclp [to_set]

   354

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

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

   357   by induct iprover+

   358

   359 lemmas rtrancl_into_trancl1 = rtranclp_into_tranclp1 [to_set]

   360

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

   362   \<comment> \<open>intro rule from \<open>r\<close> and \<open>rtrancl\<close>\<close>

   363   apply (erule rtranclp.cases)

   364    apply iprover

   365   apply (rule rtranclp_trans [THEN rtranclp_into_tranclp1])

   366     apply (simp | rule r_into_rtranclp)+

   367   done

   368

   369 lemmas rtrancl_into_trancl2 = rtranclp_into_tranclp2 [to_set]

   370

   371 text \<open>Nice induction rule for \<open>trancl\<close>\<close>

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

   373   assumes a: "r^++ a b"

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

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

   376   shows "P b" using a

   377   by (induct x\<equiv>a b) (iprover intro: cases)+

   378

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

   380

   381 lemmas tranclp_induct2 =

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

   383     consumes 1, case_names base step]

   384

   385 lemmas trancl_induct2 =

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

   387     consumes 1, case_names base step]

   388

   389 lemma tranclp_trans_induct:

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

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

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

   393   shows "P x y"

   394   \<comment> \<open>Another induction rule for trancl, incorporating transitivity\<close>

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

   396

   397 lemmas trancl_trans_induct = tranclp_trans_induct [to_set]

   398

   399 lemma tranclE [cases set: trancl]:

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

   401   obtains

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

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

   404   using assms by cases simp_all

   405

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

   407   apply (rule subsetI)

   408   apply auto

   409   apply (erule trancl_induct)

   410   apply auto

   411   done

   412

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

   414   by (auto intro: trancl_into_trancl elim: tranclE)

   415

   416 text \<open>Transitivity of @{term "r^+"}\<close>

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

   418 proof (rule transI)

   419   fix x y z

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

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

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

   423   proof induct

   424     case (base u)

   425     from \<open>(x, y) \<in> r^+\<close> and \<open>(y, u) \<in> r\<close>

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

   427   next

   428     case (step u v)

   429     from \<open>(x, u) \<in> r^+\<close> and \<open>(u, v) \<in> r\<close>

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

   431   qed

   432 qed

   433

   434 lemmas trancl_trans = trans_trancl [THEN transD]

   435

   436 lemma tranclp_trans:

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

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

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

   440   by induct iprover+

   441

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

   443   apply auto

   444   apply (erule trancl_induct)

   445    apply assumption

   446   apply (unfold trans_def)

   447   apply blast

   448   done

   449

   450 lemma rtranclp_tranclp_tranclp:

   451   assumes "r^** x y"

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

   453   by induct (iprover intro: tranclp_trans)+

   454

   455 lemmas rtrancl_trancl_trancl = rtranclp_tranclp_tranclp [to_set]

   456

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

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

   459

   460 lemmas trancl_into_trancl2 = tranclp_into_tranclp2 [to_set]

   461

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

   463   apply (drule conversepD)

   464   apply (erule tranclp_induct)

   465   apply (iprover intro: conversepI tranclp_trans)+

   466   done

   467

   468 lemmas trancl_converseI = tranclp_converseI [to_set]

   469

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

   471   apply (rule conversepI)

   472   apply (erule tranclp_induct)

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

   474   done

   475

   476 lemmas trancl_converseD = tranclp_converseD [to_set]

   477

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

   479   by (fastforce simp add: fun_eq_iff

   480     intro!: tranclp_converseI dest!: tranclp_converseD)

   481

   482 lemmas trancl_converse = tranclp_converse [to_set]

   483

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

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

   486

   487 lemma converse_tranclp_induct [consumes 1, case_names base step]:

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

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

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

   491   shows "P a"

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

   493    apply (rule cases)

   494    apply (erule conversepD)

   495   apply (blast intro: assms dest!: tranclp_converseD)

   496   done

   497

   498 lemmas converse_trancl_induct = converse_tranclp_induct [to_set]

   499

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

   501   apply (erule converse_tranclp_induct)

   502    apply auto

   503   apply (blast intro: rtranclp_trans)

   504   done

   505

   506 lemmas tranclD = tranclpD [to_set]

   507

   508 lemma converse_tranclpE:

   509   assumes major: "tranclp r x z"

   510   assumes base: "r x z ==> P"

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

   512   shows P

   513 proof -

   514   from tranclpD[OF major]

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

   516   from this(2) show P

   517   proof (cases rule: rtranclp.cases)

   518     case rtrancl_refl

   519     with \<open>r x y\<close> base show P by iprover

   520   next

   521     case rtrancl_into_rtrancl

   522     from this have "tranclp r y z"

   523       by (iprover intro: rtranclp_into_tranclp1)

   524     with \<open>r x y\<close> step show P by iprover

   525   qed

   526 qed

   527

   528 lemmas converse_tranclE = converse_tranclpE [to_set]

   529

   530 lemma tranclD2:

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

   532   by (blast elim: tranclE intro: trancl_into_rtrancl)

   533

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

   535   by (blast elim: tranclE dest: trancl_into_rtrancl)

   536

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

   538   by (blast dest: r_into_trancl)

   539

   540 lemma trancl_subset_Sigma_aux:

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

   542   by (induct rule: rtrancl_induct) auto

   543

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

   545   apply (rule subsetI)

   546   apply (simp only: split_tupled_all)

   547   apply (erule tranclE)

   548    apply (blast dest!: trancl_into_rtrancl trancl_subset_Sigma_aux)+

   549   done

   550

   551 lemma reflclp_tranclp [simp]: "(r^++)^== = r^**"

   552   apply (safe intro!: order_antisym)

   553    apply (erule tranclp_into_rtranclp)

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

   555   done

   556

   557 lemmas reflcl_trancl [simp] = reflclp_tranclp [to_set]

   558

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

   560   apply safe

   561    apply (drule trancl_into_rtrancl, simp)

   562   apply (erule rtranclE, safe)

   563    apply (rule r_into_trancl, simp)

   564   apply (rule rtrancl_into_trancl1)

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

   566   done

   567

   568 lemma rtrancl_trancl_reflcl [code]: "r^* = (r^+)^="

   569   by simp

   570

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

   572   by (auto elim: trancl_induct)

   573

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

   575   by (rule subst [OF reflcl_trancl]) simp

   576

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

   578 by (force simp add: reflclp_tranclp [symmetric] simp del: reflclp_tranclp)

   579

   580 lemmas rtranclD = rtranclpD [to_set]

   581

   582 lemma rtrancl_eq_or_trancl:

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

   584   by (fast elim: trancl_into_rtrancl dest: rtranclD)

   585

   586 lemma trancl_unfold_right: "r^+ = r^* O r"

   587 by (auto dest: tranclD2 intro: rtrancl_into_trancl1)

   588

   589 lemma trancl_unfold_left: "r^+ = r O r^*"

   590 by (auto dest: tranclD intro: rtrancl_into_trancl2)

   591

   592 lemma trancl_insert:

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

   594   \<comment> \<open>primitive recursion for \<open>trancl\<close> over finite relations\<close>

   595   apply (rule equalityI)

   596    apply (rule subsetI)

   597    apply (simp only: split_tupled_all)

   598    apply (erule trancl_induct, blast)

   599    apply (blast intro: rtrancl_into_trancl1 trancl_into_rtrancl trancl_trans)

   600   apply (rule subsetI)

   601   apply (blast intro: trancl_mono rtrancl_mono

   602     [THEN [2] rev_subsetD] rtrancl_trancl_trancl rtrancl_into_trancl2)

   603   done

   604

   605 lemma trancl_insert2:

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

   607 by(auto simp add: trancl_insert rtrancl_eq_or_trancl)

   608

   609 lemma rtrancl_insert:

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

   611 using trancl_insert[of a b r]

   612 by(simp add: rtrancl_trancl_reflcl del: reflcl_trancl) blast

   613

   614

   615 text \<open>Simplifying nested closures\<close>

   616

   617 lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"

   618 by (simp add: trans_rtrancl)

   619

   620 lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*"

   621 by (subst reflcl_trancl[symmetric]) simp

   622

   623 lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*"

   624 by auto

   625

   626

   627 text \<open>\<open>Domain\<close> and \<open>Range\<close>\<close>

   628

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

   630   by blast

   631

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

   633   by blast

   634

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

   636   by (rule rtrancl_Un_rtrancl [THEN subst]) fast

   637

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

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

   640

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

   642   by (unfold Domain_unfold) (blast dest: tranclD)

   643

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

   645   unfolding Domain_converse [symmetric] by (simp add: trancl_converse [symmetric])

   646

   647 lemma Not_Domain_rtrancl:

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

   649   apply auto

   650   apply (erule rev_mp)

   651   apply (erule rtrancl_induct)

   652    apply auto

   653   done

   654

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

   656   apply clarify

   657   apply (erule trancl_induct)

   658    apply (auto simp add: Field_def)

   659   done

   660

   661 lemma finite_trancl[simp]: "finite (r^+) = finite r"

   662   apply auto

   663    prefer 2

   664    apply (rule trancl_subset_Field2 [THEN finite_subset])

   665    apply (rule finite_SigmaI)

   666     prefer 3

   667     apply (blast intro: r_into_trancl' finite_subset)

   668    apply (auto simp add: finite_Field)

   669   done

   670

   671 text \<open>More about converse \<open>rtrancl\<close> and \<open>trancl\<close>, should

   672   be merged with main body.\<close>

   673

   674 lemma single_valued_confluent:

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

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

   677   apply (erule rtrancl_induct)

   678   apply simp

   679   apply (erule disjE)

   680    apply (blast elim:converse_rtranclE dest:single_valuedD)

   681   apply(blast intro:rtrancl_trans)

   682   done

   683

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

   685   by (fast intro: trancl_trans)

   686

   687 lemma trancl_into_trancl [rule_format]:

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

   689   apply (erule trancl_induct)

   690    apply (fast intro: r_r_into_trancl)

   691   apply (fast intro: r_r_into_trancl trancl_trans)

   692   done

   693

   694 lemma tranclp_rtranclp_tranclp:

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

   696   apply (drule tranclpD)

   697   apply (elim exE conjE)

   698   apply (drule rtranclp_trans, assumption)

   699   apply (drule rtranclp_into_tranclp2, assumption, assumption)

   700   done

   701

   702 lemmas trancl_rtrancl_trancl = tranclp_rtranclp_tranclp [to_set]

   703

   704 lemmas transitive_closure_trans [trans] =

   705   r_r_into_trancl trancl_trans rtrancl_trans

   706   trancl.trancl_into_trancl trancl_into_trancl2

   707   rtrancl.rtrancl_into_rtrancl converse_rtrancl_into_rtrancl

   708   rtrancl_trancl_trancl trancl_rtrancl_trancl

   709

   710 lemmas transitive_closurep_trans' [trans] =

   711   tranclp_trans rtranclp_trans

   712   tranclp.trancl_into_trancl tranclp_into_tranclp2

   713   rtranclp.rtrancl_into_rtrancl converse_rtranclp_into_rtranclp

   714   rtranclp_tranclp_tranclp tranclp_rtranclp_tranclp

   715

   716 declare trancl_into_rtrancl [elim]

   717

   718 subsection \<open>The power operation on relations\<close>

   719

   720 text \<open>\<open>R ^^ n = R O ... O R\<close>, the n-fold composition of \<open>R\<close>\<close>

   721

   722 overloading

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

   724   relpowp == "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)"

   725 begin

   726

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

   728     "relpow 0 R = Id"

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

   730

   731 primrec relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where

   732     "relpowp 0 R = HOL.eq"

   733   | "relpowp (Suc n) R = (R ^^ n) OO R"

   734

   735 end

   736

   737 lemma relpowp_relpow_eq [pred_set_conv]:

   738   fixes R :: "'a rel"

   739   shows "(\<lambda>x y. (x, y) \<in> R) ^^ n = (\<lambda>x y. (x, y) \<in> R ^^ n)"

   740   by (induct n) (simp_all add: relcompp_relcomp_eq)

   741

   742 text \<open>for code generation\<close>

   743

   744 definition relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where

   745   relpow_code_def [code_abbrev]: "relpow = compow"

   746

   747 definition relpowp :: "nat \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool)" where

   748   relpowp_code_def [code_abbrev]: "relpowp = compow"

   749

   750 lemma [code]:

   751   "relpow (Suc n) R = (relpow n R) O R"

   752   "relpow 0 R = Id"

   753   by (simp_all add: relpow_code_def)

   754

   755 lemma [code]:

   756   "relpowp (Suc n) R = (R ^^ n) OO R"

   757   "relpowp 0 R = HOL.eq"

   758   by (simp_all add: relpowp_code_def)

   759

   760 hide_const (open) relpow

   761 hide_const (open) relpowp

   762

   763 lemma relpow_1 [simp]:

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

   765   shows "R ^^ 1 = R"

   766   by simp

   767

   768 lemma relpowp_1 [simp]:

   769   fixes P :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

   770   shows "P ^^ 1 = P"

   771   by (fact relpow_1 [to_pred])

   772

   773 lemma relpow_0_I:

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

   775   by simp

   776

   777 lemma relpowp_0_I:

   778   "(P ^^ 0) x x"

   779   by (fact relpow_0_I [to_pred])

   780

   781 lemma relpow_Suc_I:

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

   783   by auto

   784

   785 lemma relpowp_Suc_I:

   786   "(P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> (P ^^ Suc n) x z"

   787   by (fact relpow_Suc_I [to_pred])

   788

   789 lemma relpow_Suc_I2:

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

   791   by (induct n arbitrary: z) (simp, fastforce)

   792

   793 lemma relpowp_Suc_I2:

   794   "P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> (P ^^ Suc n) x z"

   795   by (fact relpow_Suc_I2 [to_pred])

   796

   797 lemma relpow_0_E:

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

   799   by simp

   800

   801 lemma relpowp_0_E:

   802   "(P ^^ 0) x y \<Longrightarrow> (x = y \<Longrightarrow> Q) \<Longrightarrow> Q"

   803   by (fact relpow_0_E [to_pred])

   804

   805 lemma relpow_Suc_E:

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

   807   by auto

   808

   809 lemma relpowp_Suc_E:

   810   "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. (P ^^ n) x y \<Longrightarrow> P y z \<Longrightarrow> Q) \<Longrightarrow> Q"

   811   by (fact relpow_Suc_E [to_pred])

   812

   813 lemma relpow_E:

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

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

   816    \<Longrightarrow> P"

   817   by (cases n) auto

   818

   819 lemma relpowp_E:

   820   "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)

   821   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (P ^^ m) x y \<Longrightarrow> P y z \<Longrightarrow> Q)

   822   \<Longrightarrow> Q"

   823   by (fact relpow_E [to_pred])

   824

   825 lemma relpow_Suc_D2:

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

   827   apply (induct n arbitrary: x z)

   828    apply (blast intro: relpow_0_I elim: relpow_0_E relpow_Suc_E)

   829   apply (blast intro: relpow_Suc_I elim: relpow_0_E relpow_Suc_E)

   830   done

   831

   832 lemma relpowp_Suc_D2:

   833   "(P ^^ Suc n) x z \<Longrightarrow> \<exists>y. P x y \<and> (P ^^ n) y z"

   834   by (fact relpow_Suc_D2 [to_pred])

   835

   836 lemma relpow_Suc_E2:

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

   838   by (blast dest: relpow_Suc_D2)

   839

   840 lemma relpowp_Suc_E2:

   841   "(P ^^ Suc n) x z \<Longrightarrow> (\<And>y. P x y \<Longrightarrow> (P ^^ n) y z \<Longrightarrow> Q) \<Longrightarrow> Q"

   842   by (fact relpow_Suc_E2 [to_pred])

   843

   844 lemma relpow_Suc_D2':

   845   "\<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)"

   846   by (induct n) (simp_all, blast)

   847

   848 lemma relpowp_Suc_D2':

   849   "\<forall>x y z. (P ^^ n) x y \<and> P y z \<longrightarrow> (\<exists>w. P x w \<and> (P ^^ n) w z)"

   850   by (fact relpow_Suc_D2' [to_pred])

   851

   852 lemma relpow_E2:

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

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

   855    \<Longrightarrow> P"

   856   apply (cases n, simp)

   857   apply (rename_tac nat)

   858   apply (cut_tac n=nat and R=R in relpow_Suc_D2', simp, blast)

   859   done

   860

   861 lemma relpowp_E2:

   862   "(P ^^ n) x z \<Longrightarrow> (n = 0 \<Longrightarrow> x = z \<Longrightarrow> Q)

   863     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> P x y \<Longrightarrow> (P ^^ m) y z \<Longrightarrow> Q)

   864   \<Longrightarrow> Q"

   865   by (fact relpow_E2 [to_pred])

   866

   867 lemma relpow_add: "R ^^ (m+n) = R^^m O R^^n"

   868   by (induct n) auto

   869

   870 lemma relpowp_add: "P ^^ (m + n) = P ^^ m OO P ^^ n"

   871   by (fact relpow_add [to_pred])

   872

   873 lemma relpow_commute: "R O R ^^ n = R ^^ n O R"

   874   by (induct n) (simp, simp add: O_assoc [symmetric])

   875

   876 lemma relpowp_commute: "P OO P ^^ n = P ^^ n OO P"

   877   by (fact relpow_commute [to_pred])

   878

   879 lemma relpow_empty:

   880   "0 < n \<Longrightarrow> ({} :: ('a \<times> 'a) set) ^^ n = {}"

   881   by (cases n) auto

   882

   883 lemma relpowp_bot:

   884   "0 < n \<Longrightarrow> (\<bottom> :: 'a \<Rightarrow> 'a \<Rightarrow> bool) ^^ n = \<bottom>"

   885   by (fact relpow_empty [to_pred])

   886

   887 lemma rtrancl_imp_UN_relpow:

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

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

   890 proof (cases p)

   891   case (Pair x y)

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

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

   894     case base show ?case by (blast intro: relpow_0_I)

   895   next

   896     case step then show ?case by (blast intro: relpow_Suc_I)

   897   qed

   898   with Pair show ?thesis by simp

   899 qed

   900

   901 lemma rtranclp_imp_Sup_relpowp:

   902   assumes "(P^**) x y"

   903   shows "(\<Squnion>n. P ^^ n) x y"

   904   using assms and rtrancl_imp_UN_relpow [of "(x, y)", to_pred] by simp

   905

   906 lemma relpow_imp_rtrancl:

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

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

   909 proof (cases p)

   910   case (Pair x y)

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

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

   913     case 0 then show ?case by simp

   914   next

   915     case Suc then show ?case

   916       by (blast elim: relpow_Suc_E intro: rtrancl_into_rtrancl)

   917   qed

   918   with Pair show ?thesis by simp

   919 qed

   920

   921 lemma relpowp_imp_rtranclp:

   922   assumes "(P ^^ n) x y"

   923   shows "(P^**) x y"

   924   using assms and relpow_imp_rtrancl [of "(x, y)", to_pred] by simp

   925

   926 lemma rtrancl_is_UN_relpow:

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

   928   by (blast intro: rtrancl_imp_UN_relpow relpow_imp_rtrancl)

   929

   930 lemma rtranclp_is_Sup_relpowp:

   931   "P^** = (\<Squnion>n. P ^^ n)"

   932   using rtrancl_is_UN_relpow [to_pred, of P] by auto

   933

   934 lemma rtrancl_power:

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

   936   by (simp add: rtrancl_is_UN_relpow)

   937

   938 lemma rtranclp_power:

   939   "(P^**) x y \<longleftrightarrow> (\<exists>n. (P ^^ n) x y)"

   940   by (simp add: rtranclp_is_Sup_relpowp)

   941

   942 lemma trancl_power:

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

   944   apply (cases p)

   945   apply simp

   946   apply (rule iffI)

   947    apply (drule tranclD2)

   948    apply (clarsimp simp: rtrancl_is_UN_relpow)

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

   950    apply (clarsimp simp: relcomp_unfold)

   951    apply fastforce

   952   apply clarsimp

   953   apply (case_tac n, simp)

   954   apply clarsimp

   955   apply (drule relpow_imp_rtrancl)

   956   apply (drule rtrancl_into_trancl1) apply auto

   957   done

   958

   959 lemma tranclp_power:

   960   "(P^++) x y \<longleftrightarrow> (\<exists>n > 0. (P ^^ n) x y)"

   961   using trancl_power [to_pred, of P "(x, y)"] by simp

   962

   963 lemma rtrancl_imp_relpow:

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

   965   by (auto dest: rtrancl_imp_UN_relpow)

   966

   967 lemma rtranclp_imp_relpowp:

   968   "(P^**) x y \<Longrightarrow> \<exists>n. (P ^^ n) x y"

   969   by (auto dest: rtranclp_imp_Sup_relpowp)

   970

   971 text\<open>By Sternagel/Thiemann:\<close>

   972 lemma relpow_fun_conv:

   973   "((a,b) \<in> R ^^ n) = (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f(Suc i)) \<in> R))"

   974 proof (induct n arbitrary: b)

   975   case 0 show ?case by auto

   976 next

   977   case (Suc n)

   978   show ?case

   979   proof (simp add: relcomp_unfold Suc)

   980     show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R)

   981      = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"

   982     (is "?l = ?r")

   983     proof

   984       assume ?l

   985       then obtain c f where 1: "f 0 = a"  "f n = c"  "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R"  "(c,b) \<in> R" by auto

   986       let ?g = "\<lambda> m. if m = Suc n then b else f m"

   987       show ?r by (rule exI[of _ ?g], simp add: 1)

   988     next

   989       assume ?r

   990       then obtain f where 1: "f 0 = a"  "b = f (Suc n)"  "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto

   991       show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto)

   992     qed

   993   qed

   994 qed

   995

   996 lemma relpowp_fun_conv:

   997   "(P ^^ n) x y \<longleftrightarrow> (\<exists>f. f 0 = x \<and> f n = y \<and> (\<forall>i<n. P (f i) (f (Suc i))))"

   998   by (fact relpow_fun_conv [to_pred])

   999

  1000 lemma relpow_finite_bounded1:

  1001 assumes "finite(R :: ('a*'a)set)" and "k>0"

  1002 shows "R^^k \<subseteq> (UN n:{n. 0<n & n <= card R}. R^^n)" (is "_ \<subseteq> ?r")

  1003 proof-

  1004   { fix a b k

  1005     have "(a,b) : R^^(Suc k) \<Longrightarrow> EX n. 0<n & n <= card R & (a,b) : R^^n"

  1006     proof(induct k arbitrary: b)

  1007       case 0

  1008       hence "R \<noteq> {}" by auto

  1009       with card_0_eq[OF \<open>finite R\<close>] have "card R >= Suc 0" by auto

  1010       thus ?case using 0 by force

  1011     next

  1012       case (Suc k)

  1013       then obtain a' where "(a,a') : R^^(Suc k)" and "(a',b) : R" by auto

  1014       from Suc(1)[OF \<open>(a,a') : R^^(Suc k)\<close>]

  1015       obtain n where "n \<le> card R" and "(a,a') \<in> R ^^ n" by auto

  1016       have "(a,b) : R^^(Suc n)" using \<open>(a,a') \<in> R^^n\<close> and \<open>(a',b)\<in> R\<close> by auto

  1017       { assume "n < card R"

  1018         hence ?case using \<open>(a,b): R^^(Suc n)\<close> Suc_leI[OF \<open>n < card R\<close>] by blast

  1019       } moreover

  1020       { assume "n = card R"

  1021         from \<open>(a,b) \<in> R ^^ (Suc n)\<close>[unfolded relpow_fun_conv]

  1022         obtain f where "f 0 = a" and "f(Suc n) = b"

  1023           and steps: "\<And>i. i <= n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto

  1024         let ?p = "%i. (f i, f(Suc i))"

  1025         let ?N = "{i. i \<le> n}"

  1026         have "?p  ?N <= R" using steps by auto

  1027         from card_mono[OF assms(1) this]

  1028         have "card(?p  ?N) <= card R" .

  1029         also have "\<dots> < card ?N" using \<open>n = card R\<close> by simp

  1030         finally have "~ inj_on ?p ?N" by(rule pigeonhole)

  1031         then obtain i j where i: "i <= n" and j: "j <= n" and ij: "i \<noteq> j" and

  1032           pij: "?p i = ?p j" by(auto simp: inj_on_def)

  1033         let ?i = "min i j" let ?j = "max i j"

  1034         have i: "?i <= n" and j: "?j <= n" and pij: "?p ?i = ?p ?j"

  1035           and ij: "?i < ?j"

  1036           using i j ij pij unfolding min_def max_def by auto

  1037         from i j pij ij obtain i j where i: "i<=n" and j: "j<=n" and ij: "i<j"

  1038           and pij: "?p i = ?p j" by blast

  1039         let ?g = "\<lambda> l. if l \<le> i then f l else f (l + (j - i))"

  1040         let ?n = "Suc(n - (j - i))"

  1041         have abl: "(a,b) \<in> R ^^ ?n" unfolding relpow_fun_conv

  1042         proof (rule exI[of _ ?g], intro conjI impI allI)

  1043           show "?g ?n = b" using \<open>f(Suc n) = b\<close> j ij by auto

  1044         next

  1045           fix k assume "k < ?n"

  1046           show "(?g k, ?g (Suc k)) \<in> R"

  1047           proof (cases "k < i")

  1048             case True

  1049             with i have "k <= n" by auto

  1050             from steps[OF this] show ?thesis using True by simp

  1051           next

  1052             case False

  1053             hence "i \<le> k" by auto

  1054             show ?thesis

  1055             proof (cases "k = i")

  1056               case True

  1057               thus ?thesis using ij pij steps[OF i] by simp

  1058             next

  1059               case False

  1060               with \<open>i \<le> k\<close> have "i < k" by auto

  1061               hence small: "k + (j - i) <= n" using \<open>k<?n\<close> by arith

  1062               show ?thesis using steps[OF small] \<open>i<k\<close> by auto

  1063             qed

  1064           qed

  1065         qed (simp add: \<open>f 0 = a\<close>)

  1066         moreover have "?n <= n" using i j ij by arith

  1067         ultimately have ?case using \<open>n = card R\<close> by blast

  1068       }

  1069       ultimately show ?case using \<open>n \<le> card R\<close> by force

  1070     qed

  1071   }

  1072   thus ?thesis using gr0_implies_Suc[OF \<open>k>0\<close>] by auto

  1073 qed

  1074

  1075 lemma relpow_finite_bounded:

  1076 assumes "finite(R :: ('a*'a)set)"

  1077 shows "R^^k \<subseteq> (UN n:{n. n <= card R}. R^^n)"

  1078 apply(cases k)

  1079  apply force

  1080 using relpow_finite_bounded1[OF assms, of k] by auto

  1081

  1082 lemma rtrancl_finite_eq_relpow:

  1083   "finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)"

  1084 by(fastforce simp: rtrancl_power dest: relpow_finite_bounded)

  1085

  1086 lemma trancl_finite_eq_relpow:

  1087   "finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"

  1088 apply(auto simp add: trancl_power)

  1089 apply(auto dest: relpow_finite_bounded1)

  1090 done

  1091

  1092 lemma finite_relcomp[simp,intro]:

  1093 assumes "finite R" and "finite S"

  1094 shows "finite(R O S)"

  1095 proof-

  1096   have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {})  S))"

  1097     by(force simp add: split_def)

  1098   thus ?thesis using assms by(clarsimp)

  1099 qed

  1100

  1101 lemma finite_relpow[simp,intro]:

  1102   assumes "finite(R :: ('a*'a)set)" shows "n>0 \<Longrightarrow> finite(R^^n)"

  1103 apply(induct n)

  1104  apply simp

  1105 apply(case_tac n)

  1106  apply(simp_all add: assms)

  1107 done

  1108

  1109 lemma single_valued_relpow:

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

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

  1112 apply (induct n arbitrary: R)

  1113 apply simp_all

  1114 apply (rule single_valuedI)

  1115 apply (fast dest: single_valuedD elim: relpow_Suc_E)

  1116 done

  1117

  1118

  1119 subsection \<open>Bounded transitive closure\<close>

  1120

  1121 definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"

  1122 where

  1123   "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)"

  1124

  1125 lemma ntrancl_Zero [simp, code]:

  1126   "ntrancl 0 R = R"

  1127 proof

  1128   show "R \<subseteq> ntrancl 0 R"

  1129     unfolding ntrancl_def by fastforce

  1130 next

  1131   {

  1132     fix i have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" by auto

  1133   }

  1134   from this show "ntrancl 0 R \<le> R"

  1135     unfolding ntrancl_def by auto

  1136 qed

  1137

  1138 lemma ntrancl_Suc [simp]:

  1139   "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"

  1140 proof

  1141   {

  1142     fix a b

  1143     assume "(a, b) \<in> ntrancl (Suc n) R"

  1144     from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"

  1145       unfolding ntrancl_def by auto

  1146     have "(a, b) \<in> ntrancl n R O (Id \<union> R)"

  1147     proof (cases "i = 1")

  1148       case True

  1149       from this \<open>(a, b) \<in> R ^^ i\<close> show ?thesis

  1150         unfolding ntrancl_def by auto

  1151     next

  1152       case False

  1153       from this \<open>0 < i\<close> obtain j where j: "i = Suc j" "0 < j"

  1154         by (cases i) auto

  1155       from this \<open>(a, b) \<in> R ^^ i\<close> obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"

  1156         by auto

  1157       from c1 j \<open>i \<le> Suc (Suc n)\<close> have "(a, c) \<in> ntrancl n R"

  1158         unfolding ntrancl_def by fastforce

  1159       from this c2 show ?thesis by fastforce

  1160     qed

  1161   }

  1162   from this show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)"

  1163     by auto

  1164 next

  1165   show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R"

  1166     unfolding ntrancl_def by fastforce

  1167 qed

  1168

  1169 lemma [code]:

  1170   "ntrancl (Suc n) r = (let r' = ntrancl n r in r' Un r' O r)"

  1171 unfolding Let_def by auto

  1172

  1173 lemma finite_trancl_ntranl:

  1174   "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"

  1175   by (cases "card R") (auto simp add: trancl_finite_eq_relpow relpow_empty ntrancl_def)

  1176

  1177

  1178 subsection \<open>Acyclic relations\<close>

  1179

  1180 definition acyclic :: "('a * 'a) set => bool" where

  1181   "acyclic r \<longleftrightarrow> (!x. (x,x) ~: r^+)"

  1182

  1183 abbreviation acyclicP :: "('a => 'a => bool) => bool" where

  1184   "acyclicP r \<equiv> acyclic {(x, y). r x y}"

  1185

  1186 lemma acyclic_irrefl [code]:

  1187   "acyclic r \<longleftrightarrow> irrefl (r^+)"

  1188   by (simp add: acyclic_def irrefl_def)

  1189

  1190 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"

  1191   by (simp add: acyclic_def)

  1192

  1193 lemma (in order) acyclicI_order:

  1194   assumes *: "\<And>a b. (a, b) \<in> r \<Longrightarrow> f b < f a"

  1195   shows "acyclic r"

  1196 proof -

  1197   { fix a b assume "(a, b) \<in> r\<^sup>+"

  1198     then have "f b < f a"

  1199       by induct (auto intro: * less_trans) }

  1200   then show ?thesis

  1201     by (auto intro!: acyclicI)

  1202 qed

  1203

  1204 lemma acyclic_insert [iff]:

  1205      "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"

  1206 apply (simp add: acyclic_def trancl_insert)

  1207 apply (blast intro: rtrancl_trans)

  1208 done

  1209

  1210 lemma acyclic_converse [iff]: "acyclic(r^-1) = acyclic r"

  1211 by (simp add: acyclic_def trancl_converse)

  1212

  1213 lemmas acyclicP_converse [iff] = acyclic_converse [to_pred]

  1214

  1215 lemma acyclic_impl_antisym_rtrancl: "acyclic r ==> antisym(r^*)"

  1216 apply (simp add: acyclic_def antisym_def)

  1217 apply (blast elim: rtranclE intro: rtrancl_into_trancl1 rtrancl_trancl_trancl)

  1218 done

  1219

  1220 (* Other direction:

  1221 acyclic = no loops

  1222 antisym = only self loops

  1223 Goalw [acyclic_def,antisym_def] "antisym( r^* ) ==> acyclic(r - Id)

  1224 ==> antisym( r^* ) = acyclic(r - Id)";

  1225 *)

  1226

  1227 lemma acyclic_subset: "[| acyclic s; r <= s |] ==> acyclic r"

  1228 apply (simp add: acyclic_def)

  1229 apply (blast intro: trancl_mono)

  1230 done

  1231

  1232

  1233 subsection \<open>Setup of transitivity reasoner\<close>

  1234

  1235 ML \<open>

  1236

  1237 structure Trancl_Tac = Trancl_Tac

  1238 (

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

  1240   val trancl_trans  = @{thm trancl_trans};

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

  1242   val r_into_rtrancl = @{thm r_into_rtrancl};

  1243   val trancl_into_rtrancl = @{thm trancl_into_rtrancl};

  1244   val rtrancl_trancl_trancl = @{thm rtrancl_trancl_trancl};

  1245   val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};

  1246   val rtrancl_trans = @{thm rtrancl_trans};

  1247

  1248   fun decomp (@{const Trueprop} $t) =   1249 let fun dec (Const (@{const_name Set.member}, _)$ (Const (@{const_name Pair}, _) $a$ b) $rel ) =   1250 let fun decr (Const (@{const_name rtrancl}, _ )$ r) = (r,"r*")

  1251               | decr (Const (@{const_name trancl}, _ ) $r) = (r,"r+")   1252 | decr r = (r,"r");   1253 val (rel,r) = decr (Envir.beta_eta_contract rel);   1254 in SOME (a,b,rel,r) end   1255 | dec _ = NONE   1256 in dec t end   1257 | decomp _ = NONE;   1258 );   1259   1260 structure Tranclp_Tac = Trancl_Tac   1261 (   1262 val r_into_trancl = @{thm tranclp.r_into_trancl};   1263 val trancl_trans = @{thm tranclp_trans};   1264 val rtrancl_refl = @{thm rtranclp.rtrancl_refl};   1265 val r_into_rtrancl = @{thm r_into_rtranclp};   1266 val trancl_into_rtrancl = @{thm tranclp_into_rtranclp};   1267 val rtrancl_trancl_trancl = @{thm rtranclp_tranclp_tranclp};   1268 val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};   1269 val rtrancl_trans = @{thm rtranclp_trans};   1270   1271 fun decomp (@{const Trueprop}$ t) =

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

  1273         let fun decr (Const (@{const_name rtranclp}, _ ) $r) = (r,"r*")   1274 | decr (Const (@{const_name tranclp}, _ )$ r)  = (r,"r+")

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

  1276             val (rel,r) = decr rel;

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

  1278       | dec _ =  NONE

  1279     in dec t end

  1280     | decomp _ = NONE;

  1281 );

  1282 \<close>

  1283

  1284 setup \<open>

  1285   map_theory_simpset (fn ctxt => ctxt

  1286     addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac)

  1287     addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)

  1288     addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)

  1289     addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))

  1290 \<close>

  1291

  1292

  1293 text \<open>Optional methods.\<close>

  1294

  1295 method_setup trancl =

  1296   \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.trancl_tac)\<close>

  1297   \<open>simple transitivity reasoner\<close>

  1298 method_setup rtrancl =

  1299   \<open>Scan.succeed (SIMPLE_METHOD' o Trancl_Tac.rtrancl_tac)\<close>

  1300   \<open>simple transitivity reasoner\<close>

  1301 method_setup tranclp =

  1302   \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.trancl_tac)\<close>

  1303   \<open>simple transitivity reasoner (predicate version)\<close>

  1304 method_setup rtranclp =

  1305   \<open>Scan.succeed (SIMPLE_METHOD' o Tranclp_Tac.rtrancl_tac)\<close>

  1306   \<open>simple transitivity reasoner (predicate version)\<close>

  1307

  1308 end
`