src/HOL/Library/Transitive_Closure_Table.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 37589 9c33d02656bc
child 43973 a907e541b127
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
bulwahn@33649
     1
(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
bulwahn@33649
     2
bulwahn@33649
     3
header {* A tabled implementation of the reflexive transitive closure *}
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
bulwahn@33649
    15
lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
bulwahn@33649
    16
proof
bulwahn@33649
    17
  assume "r\<^sup>*\<^sup>* x y"
bulwahn@33649
    18
  then show "\<exists>xs. rtrancl_path r x xs y"
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)
bulwahn@33649
    25
    from `\<exists>xs. rtrancl_path r z xs y`
bulwahn@33649
    26
    obtain xs where "rtrancl_path r z xs y" ..
bulwahn@33649
    27
    with `r x z` 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
bulwahn@33649
    31
next
bulwahn@33649
    32
  assume "\<exists>xs. rtrancl_path r x xs y"
bulwahn@33649
    33
  then obtain xs where "rtrancl_path r x xs y" ..
bulwahn@33649
    34
  then show "r\<^sup>*\<^sup>* x y"
bulwahn@33649
    35
  proof induct
bulwahn@33649
    36
    case (base x)
bulwahn@33649
    37
    show ?case by (rule rtranclp.rtrancl_refl)
bulwahn@33649
    38
  next
bulwahn@33649
    39
    case (step x y ys z)
bulwahn@33649
    40
    from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
bulwahn@33649
    41
      by (rule converse_rtranclp_into_rtranclp)
bulwahn@33649
    42
  qed
bulwahn@33649
    43
qed
bulwahn@33649
    44
bulwahn@33649
    45
lemma rtrancl_path_trans:
bulwahn@33649
    46
  assumes xy: "rtrancl_path r x xs y"
bulwahn@33649
    47
  and yz: "rtrancl_path r y ys z"
bulwahn@33649
    48
  shows "rtrancl_path r x (xs @ ys) z" using xy yz
bulwahn@33649
    49
proof (induct arbitrary: z)
bulwahn@33649
    50
  case (base x)
bulwahn@33649
    51
  then show ?case by simp
bulwahn@33649
    52
next
bulwahn@33649
    53
  case (step x y xs)
bulwahn@33649
    54
  then have "rtrancl_path r y (xs @ ys) z"
bulwahn@33649
    55
    by simp
bulwahn@33649
    56
  with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
bulwahn@33649
    57
    by (rule rtrancl_path.step)
bulwahn@33649
    58
  then show ?case by simp
bulwahn@33649
    59
qed
bulwahn@33649
    60
bulwahn@33649
    61
lemma rtrancl_path_appendE:
bulwahn@33649
    62
  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
bulwahn@33649
    63
  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
bulwahn@33649
    64
proof (induct xs arbitrary: x)
bulwahn@33649
    65
  case Nil
bulwahn@33649
    66
  then have "rtrancl_path r x (y # ys) z" by simp
bulwahn@33649
    67
  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
bulwahn@33649
    68
    by cases auto
bulwahn@33649
    69
  from xy have "rtrancl_path r x [y] y"
bulwahn@33649
    70
    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
bulwahn@33649
    71
  then have "rtrancl_path r x ([] @ [y]) y" by simp
bulwahn@33649
    72
  then show ?thesis using yz by (rule Nil)
bulwahn@33649
    73
next
bulwahn@33649
    74
  case (Cons a as)
bulwahn@33649
    75
  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
bulwahn@33649
    76
  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
bulwahn@33649
    77
    by cases auto
bulwahn@33649
    78
  show ?thesis
bulwahn@33649
    79
  proof (rule Cons(1) [OF _ az])
bulwahn@33649
    80
    assume "rtrancl_path r y ys z"
bulwahn@33649
    81
    assume "rtrancl_path r a (as @ [y]) y"
bulwahn@33649
    82
    with xa have "rtrancl_path r x (a # (as @ [y])) y"
bulwahn@33649
    83
      by (rule rtrancl_path.step)
bulwahn@33649
    84
    then have "rtrancl_path r x ((a # as) @ [y]) y"
bulwahn@33649
    85
      by simp
bulwahn@33649
    86
    then show ?thesis using `rtrancl_path r y ys z`
bulwahn@33649
    87
      by (rule Cons(2))
bulwahn@33649
    88
  qed
bulwahn@33649
    89
qed
bulwahn@33649
    90
bulwahn@33649
    91
lemma rtrancl_path_distinct:
bulwahn@33649
    92
  assumes xy: "rtrancl_path r x xs y"
bulwahn@33649
    93
  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
bulwahn@33649
    94
proof (induct xs rule: measure_induct_rule [of length])
bulwahn@33649
    95
  case (less xs)
bulwahn@33649
    96
  show ?case
bulwahn@33649
    97
  proof (cases "distinct (x # xs)")
bulwahn@33649
    98
    case True
bulwahn@33649
    99
    with `rtrancl_path r x xs y` show ?thesis by (rule less)
bulwahn@33649
   100
  next
bulwahn@33649
   101
    case False
bulwahn@33649
   102
    then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649
   103
      by (rule not_distinct_decomp)
bulwahn@33649
   104
    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
bulwahn@33649
   105
      by iprover
bulwahn@33649
   106
    show ?thesis
bulwahn@33649
   107
    proof (cases as)
bulwahn@33649
   108
      case Nil
bulwahn@33649
   109
      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
wenzelm@35423
   110
        by auto
bulwahn@33649
   111
      from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
wenzelm@35423
   112
        by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   113
      from xs have "length cs < length xs" by simp
bulwahn@33649
   114
      then show ?thesis
wenzelm@35423
   115
        by (rule less(1)) (iprover intro: cs less(2))+
bulwahn@33649
   116
    next
bulwahn@33649
   117
      case (Cons d ds)
bulwahn@33649
   118
      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
wenzelm@35423
   119
        by auto
bulwahn@33649
   120
      with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
bulwahn@33649
   121
        and ay: "rtrancl_path r a (bs @ a # cs) y"
wenzelm@35423
   122
        by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   123
      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
bulwahn@33649
   124
      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
wenzelm@35423
   125
        by (rule rtrancl_path_trans)
bulwahn@33649
   126
      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
bulwahn@33649
   127
      then show ?thesis
wenzelm@35423
   128
        by (rule less(1)) (iprover intro: xy less(2))+
bulwahn@33649
   129
    qed
bulwahn@33649
   130
  qed
bulwahn@33649
   131
qed
bulwahn@33649
   132
bulwahn@33649
   133
inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
   134
  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@33649
   135
where
bulwahn@33649
   136
  base: "rtrancl_tab r xs x x"
bulwahn@33649
   137
| 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
   138
bulwahn@33649
   139
lemma rtrancl_path_imp_rtrancl_tab:
bulwahn@33649
   140
  assumes path: "rtrancl_path r x xs y"
bulwahn@33649
   141
  and x: "distinct (x # xs)"
bulwahn@33649
   142
  and ys: "({x} \<union> set xs) \<inter> set ys = {}"
bulwahn@33649
   143
  shows "rtrancl_tab r ys x y" using path x ys
bulwahn@33649
   144
proof (induct arbitrary: ys)
bulwahn@33649
   145
  case base
bulwahn@33649
   146
  show ?case by (rule rtrancl_tab.base)
bulwahn@33649
   147
next
bulwahn@33649
   148
  case (step x y zs z)
bulwahn@33649
   149
  then have "x \<notin> set ys" by auto
bulwahn@33649
   150
  from step have "distinct (y # zs)" by simp
bulwahn@33649
   151
  moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
bulwahn@33649
   152
    by auto
bulwahn@33649
   153
  ultimately have "rtrancl_tab r (x # ys) y z"
bulwahn@33649
   154
    by (rule step)
bulwahn@33649
   155
  with `x \<notin> set ys` `r x y`
bulwahn@33649
   156
  show ?case by (rule rtrancl_tab.step)
bulwahn@33649
   157
qed
bulwahn@33649
   158
bulwahn@33649
   159
lemma rtrancl_tab_imp_rtrancl_path:
bulwahn@33649
   160
  assumes tab: "rtrancl_tab r ys x y"
bulwahn@33649
   161
  obtains xs where "rtrancl_path r x xs y" using tab
bulwahn@33649
   162
proof induct
bulwahn@33649
   163
  case base
bulwahn@33649
   164
  from rtrancl_path.base show ?case by (rule base)
bulwahn@33649
   165
next
bulwahn@33649
   166
  case step show ?case by (iprover intro: step rtrancl_path.step)
bulwahn@33649
   167
qed
bulwahn@33649
   168
bulwahn@33649
   169
lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
bulwahn@33649
   170
proof
bulwahn@33649
   171
  assume "r\<^sup>*\<^sup>* x y"
bulwahn@33649
   172
  then obtain xs where "rtrancl_path r x xs y"
bulwahn@33649
   173
    by (auto simp add: rtranclp_eq_rtrancl_path)
bulwahn@33649
   174
  then obtain xs' where xs': "rtrancl_path r x xs' y"
bulwahn@33649
   175
    and distinct: "distinct (x # xs')"
bulwahn@33649
   176
    by (rule rtrancl_path_distinct)
bulwahn@33649
   177
  have "({x} \<union> set xs') \<inter> set [] = {}" by simp
bulwahn@33649
   178
  with xs' distinct show "rtrancl_tab r [] x y"
bulwahn@33649
   179
    by (rule rtrancl_path_imp_rtrancl_tab)
bulwahn@33649
   180
next
bulwahn@33649
   181
  assume "rtrancl_tab r [] x y"
bulwahn@33649
   182
  then obtain xs where "rtrancl_path r x xs y"
bulwahn@33649
   183
    by (rule rtrancl_tab_imp_rtrancl_path)
bulwahn@33649
   184
  then show "r\<^sup>*\<^sup>* x y"
bulwahn@33649
   185
    by (auto simp add: rtranclp_eq_rtrancl_path)
bulwahn@33649
   186
qed
bulwahn@33649
   187
bulwahn@33870
   188
declare rtranclp_eq_rtrancl_tab_nil [code_unfold, code_inline del]
bulwahn@33649
   189
bulwahn@33649
   190
declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
bulwahn@33649
   191
haftmann@37589
   192
code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastsimp
bulwahn@33649
   193
bulwahn@33649
   194
subsection {* A simple example *}
bulwahn@33649
   195
bulwahn@33649
   196
datatype ty = A | B | C
bulwahn@33649
   197
bulwahn@33649
   198
inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
bulwahn@33649
   199
where
bulwahn@33649
   200
  "test A B"
bulwahn@33649
   201
| "test B A"
bulwahn@33649
   202
| "test B C"
bulwahn@33649
   203
bulwahn@33649
   204
subsubsection {* Invoking with the SML code generator *}
bulwahn@33649
   205
bulwahn@33649
   206
code_module Test
bulwahn@33649
   207
contains
bulwahn@33649
   208
test1 = "test\<^sup>*\<^sup>* A C"
bulwahn@33649
   209
test2 = "test\<^sup>*\<^sup>* C A"
bulwahn@33649
   210
test3 = "test\<^sup>*\<^sup>* A _"
bulwahn@33649
   211
test4 = "test\<^sup>*\<^sup>* _ C"
bulwahn@33649
   212
bulwahn@33649
   213
ML "Test.test1"
bulwahn@33649
   214
ML "Test.test2"
bulwahn@33649
   215
ML "DSeq.list_of Test.test3"
bulwahn@33649
   216
ML "DSeq.list_of Test.test4"
bulwahn@33649
   217
bulwahn@33649
   218
subsubsection {* Invoking with the predicate compiler and the generic code generator *}
bulwahn@33649
   219
bulwahn@33649
   220
code_pred test .
bulwahn@33649
   221
bulwahn@33649
   222
values "{x. test\<^sup>*\<^sup>* A C}"
bulwahn@33649
   223
values "{x. test\<^sup>*\<^sup>* C A}"
bulwahn@33649
   224
values "{x. test\<^sup>*\<^sup>* A x}"
bulwahn@33649
   225
values "{x. test\<^sup>*\<^sup>* x C}"
bulwahn@33649
   226
bulwahn@33870
   227
value "test\<^sup>*\<^sup>* A C"
bulwahn@33870
   228
value "test\<^sup>*\<^sup>* C A"
bulwahn@33870
   229
wenzelm@36176
   230
hide_type ty
wenzelm@36176
   231
hide_const test A B C
bulwahn@33649
   232
bulwahn@33649
   233
end
bulwahn@33649
   234