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