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