src/HOL/Library/Transitive_Closure_Table.thy
author haftmann
Mon Jun 05 15:59:41 2017 +0200 (2017-06-05)
changeset 66010 2f7d39285a1a
parent 64632 9df24b8b6c0a
permissions -rw-r--r--
executable domain membership checks
wenzelm@60519
     1
(*  Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen  *)
bulwahn@33649
     2
wenzelm@60500
     3
section \<open>A table-based implementation of the reflexive transitive closure\<close>
bulwahn@33649
     4
bulwahn@33649
     5
theory Transitive_Closure_Table
bulwahn@33649
     6
imports Main
bulwahn@33649
     7
begin
bulwahn@33649
     8
bulwahn@33649
     9
inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
    10
  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
    11
where
bulwahn@33649
    12
  base: "rtrancl_path r x [] x"
bulwahn@33649
    13
| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
bulwahn@33649
    14
wenzelm@60519
    15
lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)"
bulwahn@33649
    16
proof
wenzelm@60519
    17
  show "\<exists>xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y"
wenzelm@60519
    18
    using that
bulwahn@33649
    19
  proof (induct rule: converse_rtranclp_induct)
berghofe@34912
    20
    case base
bulwahn@33649
    21
    have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
bulwahn@33649
    22
    then show ?case ..
bulwahn@33649
    23
  next
berghofe@34912
    24
    case (step x z)
wenzelm@60500
    25
    from \<open>\<exists>xs. rtrancl_path r z xs y\<close>
bulwahn@33649
    26
    obtain xs where "rtrancl_path r z xs y" ..
wenzelm@60500
    27
    with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y"
bulwahn@33649
    28
      by (rule rtrancl_path.step)
bulwahn@33649
    29
    then show ?case ..
bulwahn@33649
    30
  qed
wenzelm@60519
    31
  show "r\<^sup>*\<^sup>* x y" if "\<exists>xs. rtrancl_path r x xs y"
wenzelm@60519
    32
  proof -
wenzelm@60519
    33
    from that obtain xs where "rtrancl_path r x xs y" ..
wenzelm@60519
    34
    then show ?thesis
wenzelm@60519
    35
    proof induct
wenzelm@60519
    36
      case (base x)
wenzelm@60519
    37
      show ?case
wenzelm@60519
    38
        by (rule rtranclp.rtrancl_refl)
wenzelm@60519
    39
    next
wenzelm@60519
    40
      case (step x y ys z)
wenzelm@60519
    41
      from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case
wenzelm@60519
    42
        by (rule converse_rtranclp_into_rtranclp)
wenzelm@60519
    43
    qed
bulwahn@33649
    44
  qed
bulwahn@33649
    45
qed
bulwahn@33649
    46
bulwahn@33649
    47
lemma rtrancl_path_trans:
bulwahn@33649
    48
  assumes xy: "rtrancl_path r x xs y"
wenzelm@60519
    49
    and yz: "rtrancl_path r y ys z"
bulwahn@33649
    50
  shows "rtrancl_path r x (xs @ ys) z" using xy yz
bulwahn@33649
    51
proof (induct arbitrary: z)
bulwahn@33649
    52
  case (base x)
bulwahn@33649
    53
  then show ?case by simp
bulwahn@33649
    54
next
bulwahn@33649
    55
  case (step x y xs)
bulwahn@33649
    56
  then have "rtrancl_path r y (xs @ ys) z"
bulwahn@33649
    57
    by simp
wenzelm@60500
    58
  with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z"
bulwahn@33649
    59
    by (rule rtrancl_path.step)
bulwahn@33649
    60
  then show ?case by simp
bulwahn@33649
    61
qed
bulwahn@33649
    62
bulwahn@33649
    63
lemma rtrancl_path_appendE:
bulwahn@33649
    64
  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
wenzelm@60519
    65
  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z"
wenzelm@60519
    66
  using xz
bulwahn@33649
    67
proof (induct xs arbitrary: x)
bulwahn@33649
    68
  case Nil
bulwahn@33649
    69
  then have "rtrancl_path r x (y # ys) z" by simp
bulwahn@33649
    70
  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
bulwahn@33649
    71
    by cases auto
bulwahn@33649
    72
  from xy have "rtrancl_path r x [y] y"
bulwahn@33649
    73
    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
bulwahn@33649
    74
  then have "rtrancl_path r x ([] @ [y]) y" by simp
wenzelm@60519
    75
  then show thesis using yz by (rule Nil)
bulwahn@33649
    76
next
bulwahn@33649
    77
  case (Cons a as)
bulwahn@33649
    78
  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
bulwahn@33649
    79
  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
bulwahn@33649
    80
    by cases auto
wenzelm@60519
    81
  show thesis
bulwahn@33649
    82
  proof (rule Cons(1) [OF _ az])
bulwahn@33649
    83
    assume "rtrancl_path r y ys z"
bulwahn@33649
    84
    assume "rtrancl_path r a (as @ [y]) y"
bulwahn@33649
    85
    with xa have "rtrancl_path r x (a # (as @ [y])) y"
bulwahn@33649
    86
      by (rule rtrancl_path.step)
bulwahn@33649
    87
    then have "rtrancl_path r x ((a # as) @ [y]) y"
bulwahn@33649
    88
      by simp
wenzelm@60519
    89
    then show thesis using \<open>rtrancl_path r y ys z\<close>
bulwahn@33649
    90
      by (rule Cons(2))
bulwahn@33649
    91
  qed
bulwahn@33649
    92
qed
bulwahn@33649
    93
bulwahn@33649
    94
lemma rtrancl_path_distinct:
bulwahn@33649
    95
  assumes xy: "rtrancl_path r x xs y"
Andreas@61764
    96
  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs"
wenzelm@60519
    97
  using xy
bulwahn@33649
    98
proof (induct xs rule: measure_induct_rule [of length])
bulwahn@33649
    99
  case (less xs)
bulwahn@33649
   100
  show ?case
bulwahn@33649
   101
  proof (cases "distinct (x # xs)")
bulwahn@33649
   102
    case True
Andreas@61764
   103
    with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp
bulwahn@33649
   104
  next
bulwahn@33649
   105
    case False
bulwahn@33649
   106
    then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649
   107
      by (rule not_distinct_decomp)
bulwahn@33649
   108
    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649
   109
      by iprover
bulwahn@33649
   110
    show ?thesis
bulwahn@33649
   111
    proof (cases as)
bulwahn@33649
   112
      case Nil
bulwahn@33649
   113
      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
wenzelm@35423
   114
        by auto
Andreas@61764
   115
      from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs"
wenzelm@35423
   116
        by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   117
      from xs have "length cs < length xs" by simp
bulwahn@33649
   118
      then show ?thesis
Andreas@61764
   119
        by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+
bulwahn@33649
   120
    next
bulwahn@33649
   121
      case (Cons d ds)
bulwahn@33649
   122
      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
wenzelm@35423
   123
        by auto
wenzelm@60500
   124
      with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a"
bulwahn@33649
   125
        and ay: "rtrancl_path r a (bs @ a # cs) y"
wenzelm@35423
   126
        by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   127
      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   128
      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
wenzelm@35423
   129
        by (rule rtrancl_path_trans)
Andreas@61764
   130
      from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto
bulwahn@33649
   131
      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
bulwahn@33649
   132
      then show ?thesis
Andreas@61764
   133
        by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+
bulwahn@33649
   134
    qed
bulwahn@33649
   135
  qed
bulwahn@33649
   136
qed
bulwahn@33649
   137
bulwahn@33649
   138
inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
   139
  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
   140
where
bulwahn@33649
   141
  base: "rtrancl_tab r xs x x"
bulwahn@33649
   142
| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
bulwahn@33649
   143
bulwahn@33649
   144
lemma rtrancl_path_imp_rtrancl_tab:
bulwahn@33649
   145
  assumes path: "rtrancl_path r x xs y"
wenzelm@60519
   146
    and x: "distinct (x # xs)"
wenzelm@60519
   147
    and ys: "({x} \<union> set xs) \<inter> set ys = {}"
wenzelm@60519
   148
  shows "rtrancl_tab r ys x y"
wenzelm@60519
   149
  using path x ys
bulwahn@33649
   150
proof (induct arbitrary: ys)
bulwahn@33649
   151
  case base
wenzelm@60519
   152
  show ?case
wenzelm@60519
   153
    by (rule rtrancl_tab.base)
bulwahn@33649
   154
next
bulwahn@33649
   155
  case (step x y zs z)
wenzelm@60519
   156
  then have "x \<notin> set ys"
wenzelm@60519
   157
    by auto
wenzelm@60519
   158
  from step have "distinct (y # zs)"
wenzelm@60519
   159
    by simp
bulwahn@33649
   160
  moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
bulwahn@33649
   161
    by auto
bulwahn@33649
   162
  ultimately have "rtrancl_tab r (x # ys) y z"
bulwahn@33649
   163
    by (rule step)
wenzelm@60519
   164
  with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case
wenzelm@60519
   165
    by (rule rtrancl_tab.step)
bulwahn@33649
   166
qed
bulwahn@33649
   167
bulwahn@33649
   168
lemma rtrancl_tab_imp_rtrancl_path:
bulwahn@33649
   169
  assumes tab: "rtrancl_tab r ys x y"
wenzelm@60519
   170
  obtains xs where "rtrancl_path r x xs y"
wenzelm@60519
   171
  using tab
bulwahn@33649
   172
proof induct
bulwahn@33649
   173
  case base
wenzelm@60519
   174
  from rtrancl_path.base show ?case
wenzelm@60519
   175
    by (rule base)
bulwahn@33649
   176
next
wenzelm@60519
   177
  case step
wenzelm@60519
   178
  show ?case
wenzelm@60519
   179
    by (iprover intro: step rtrancl_path.step)
bulwahn@33649
   180
qed
bulwahn@33649
   181
wenzelm@60519
   182
lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y"
bulwahn@33649
   183
proof
wenzelm@60519
   184
  show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y"
wenzelm@60519
   185
  proof -
wenzelm@60519
   186
    from that obtain xs where "rtrancl_path r x xs y"
wenzelm@60519
   187
      by (auto simp add: rtranclp_eq_rtrancl_path)
wenzelm@60519
   188
    then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')"
wenzelm@60519
   189
      by (rule rtrancl_path_distinct)
wenzelm@60519
   190
    have "({x} \<union> set xs') \<inter> set [] = {}"
wenzelm@60519
   191
      by simp
wenzelm@60519
   192
    with xs' distinct show ?thesis
wenzelm@60519
   193
      by (rule rtrancl_path_imp_rtrancl_tab)
wenzelm@60519
   194
  qed
wenzelm@60519
   195
  show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y"
wenzelm@60519
   196
  proof -
wenzelm@60519
   197
    from that obtain xs where "rtrancl_path r x xs y"
wenzelm@60519
   198
      by (rule rtrancl_tab_imp_rtrancl_path)
wenzelm@60519
   199
    then show ?thesis
wenzelm@60519
   200
      by (auto simp add: rtranclp_eq_rtrancl_path)
wenzelm@60519
   201
  qed
bulwahn@33649
   202
qed
bulwahn@33649
   203
wenzelm@60519
   204
declare rtranclp_rtrancl_eq [code del]
wenzelm@60519
   205
declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]
bulwahn@33649
   206
wenzelm@60519
   207
code_pred rtranclp
wenzelm@60519
   208
  using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
bulwahn@33649
   209
haftmann@64632
   210
lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> Rangep R z"
Andreas@61765
   211
by(induction rule: rtrancl_path.induct) auto
Andreas@61765
   212
haftmann@64632
   213
lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> Rangep R y"
Andreas@61765
   214
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
Andreas@61765
   215
Andreas@61765
   216
lemma rtrancl_path_nth:
Andreas@61765
   217
  "\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)"
Andreas@61765
   218
proof(induction arbitrary: i rule: rtrancl_path.induct)
Andreas@61765
   219
  case step thus ?case by(cases i) simp_all
Andreas@61765
   220
qed simp
Andreas@61765
   221
Andreas@61765
   222
lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y"
Andreas@61765
   223
by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases)
Andreas@61765
   224
Andreas@61765
   225
lemma rtrancl_path_mono:
Andreas@61765
   226
  "\<lbrakk> rtrancl_path R x p y; \<And>x y. R x y \<Longrightarrow> S x y \<rbrakk> \<Longrightarrow> rtrancl_path S x p y"
Andreas@61765
   227
by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros)
Andreas@61765
   228
nipkow@62390
   229
end