src/HOL/Library/Transitive_Closure_Table.thy
author wenzelm
Fri Jun 19 18:41:21 2015 +0200 (2015-06-19)
changeset 60519 84b8e5c2580e
parent 60500 903bb1495239
child 61764 ac6e5de1a50b
permissions -rw-r--r--
tuned proofs;
     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')"
    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)
   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"
   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)) (iprover intro: cs less(2))+
   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 "length ((ds @ [a]) @ cs) < length xs" by simp
   131       then show ?thesis
   132         by (rule less(1)) (iprover intro: xy less(2))+
   133     qed
   134   qed
   135 qed
   136 
   137 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   138   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   139 where
   140   base: "rtrancl_tab r xs x x"
   141 | step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
   142 
   143 lemma rtrancl_path_imp_rtrancl_tab:
   144   assumes path: "rtrancl_path r x xs y"
   145     and x: "distinct (x # xs)"
   146     and ys: "({x} \<union> set xs) \<inter> set ys = {}"
   147   shows "rtrancl_tab r ys x y"
   148   using path x ys
   149 proof (induct arbitrary: ys)
   150   case base
   151   show ?case
   152     by (rule rtrancl_tab.base)
   153 next
   154   case (step x y zs z)
   155   then have "x \<notin> set ys"
   156     by auto
   157   from step have "distinct (y # zs)"
   158     by simp
   159   moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
   160     by auto
   161   ultimately have "rtrancl_tab r (x # ys) y z"
   162     by (rule step)
   163   with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case
   164     by (rule rtrancl_tab.step)
   165 qed
   166 
   167 lemma rtrancl_tab_imp_rtrancl_path:
   168   assumes tab: "rtrancl_tab r ys x y"
   169   obtains xs where "rtrancl_path r x xs y"
   170   using tab
   171 proof induct
   172   case base
   173   from rtrancl_path.base show ?case
   174     by (rule base)
   175 next
   176   case step
   177   show ?case
   178     by (iprover intro: step rtrancl_path.step)
   179 qed
   180 
   181 lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y"
   182 proof
   183   show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y"
   184   proof -
   185     from that obtain xs where "rtrancl_path r x xs y"
   186       by (auto simp add: rtranclp_eq_rtrancl_path)
   187     then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')"
   188       by (rule rtrancl_path_distinct)
   189     have "({x} \<union> set xs') \<inter> set [] = {}"
   190       by simp
   191     with xs' distinct show ?thesis
   192       by (rule rtrancl_path_imp_rtrancl_tab)
   193   qed
   194   show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y"
   195   proof -
   196     from that obtain xs where "rtrancl_path r x xs y"
   197       by (rule rtrancl_tab_imp_rtrancl_path)
   198     then show ?thesis
   199       by (auto simp add: rtranclp_eq_rtrancl_path)
   200   qed
   201 qed
   202 
   203 declare rtranclp_rtrancl_eq [code del]
   204 declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro]
   205 
   206 code_pred rtranclp
   207   using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
   208 
   209 end