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