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