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