src/HOL/Library/Transitive_Closure_Table.thy
 author blanchet Wed Sep 24 15:45:55 2014 +0200 (2014-09-24) changeset 58425 246985c6b20b parent 56922 d411a81b8356 child 58881 b9556a055632 permissions -rw-r--r--
simpler proof
```     1 (* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
```
```     2
```
```     3 header {* A table-based implementation of the reflexive transitive closure *}
```
```     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 = (\<exists>xs. rtrancl_path r x xs y)"
```
```    16 proof
```
```    17   assume "r\<^sup>*\<^sup>* x y"
```
```    18   then show "\<exists>xs. rtrancl_path r x xs y"
```
```    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 `\<exists>xs. rtrancl_path r z xs y`
```
```    26     obtain xs where "rtrancl_path r z xs y" ..
```
```    27     with `r x z` have "rtrancl_path r x (z # xs) y"
```
```    28       by (rule rtrancl_path.step)
```
```    29     then show ?case ..
```
```    30   qed
```
```    31 next
```
```    32   assume "\<exists>xs. rtrancl_path r x xs y"
```
```    33   then obtain xs where "rtrancl_path r x xs y" ..
```
```    34   then show "r\<^sup>*\<^sup>* x y"
```
```    35   proof induct
```
```    36     case (base x)
```
```    37     show ?case by (rule rtranclp.rtrancl_refl)
```
```    38   next
```
```    39     case (step x y ys z)
```
```    40     from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
```
```    41       by (rule converse_rtranclp_into_rtranclp)
```
```    42   qed
```
```    43 qed
```
```    44
```
```    45 lemma rtrancl_path_trans:
```
```    46   assumes xy: "rtrancl_path r x xs y"
```
```    47   and yz: "rtrancl_path r y ys z"
```
```    48   shows "rtrancl_path r x (xs @ ys) z" using xy yz
```
```    49 proof (induct arbitrary: z)
```
```    50   case (base x)
```
```    51   then show ?case by simp
```
```    52 next
```
```    53   case (step x y xs)
```
```    54   then have "rtrancl_path r y (xs @ ys) z"
```
```    55     by simp
```
```    56   with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
```
```    57     by (rule rtrancl_path.step)
```
```    58   then show ?case by simp
```
```    59 qed
```
```    60
```
```    61 lemma rtrancl_path_appendE:
```
```    62   assumes xz: "rtrancl_path r x (xs @ y # ys) z"
```
```    63   obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
```
```    64 proof (induct xs arbitrary: x)
```
```    65   case Nil
```
```    66   then have "rtrancl_path r x (y # ys) z" by simp
```
```    67   then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
```
```    68     by cases auto
```
```    69   from xy have "rtrancl_path r x [y] y"
```
```    70     by (rule rtrancl_path.step [OF _ rtrancl_path.base])
```
```    71   then have "rtrancl_path r x ([] @ [y]) y" by simp
```
```    72   then show ?thesis using yz by (rule Nil)
```
```    73 next
```
```    74   case (Cons a as)
```
```    75   then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
```
```    76   then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
```
```    77     by cases auto
```
```    78   show ?thesis
```
```    79   proof (rule Cons(1) [OF _ az])
```
```    80     assume "rtrancl_path r y ys z"
```
```    81     assume "rtrancl_path r a (as @ [y]) y"
```
```    82     with xa have "rtrancl_path r x (a # (as @ [y])) y"
```
```    83       by (rule rtrancl_path.step)
```
```    84     then have "rtrancl_path r x ((a # as) @ [y]) y"
```
```    85       by simp
```
```    86     then show ?thesis using `rtrancl_path r y ys z`
```
```    87       by (rule Cons(2))
```
```    88   qed
```
```    89 qed
```
```    90
```
```    91 lemma rtrancl_path_distinct:
```
```    92   assumes xy: "rtrancl_path r x xs y"
```
```    93   obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
```
```    94 proof (induct xs rule: measure_induct_rule [of length])
```
```    95   case (less xs)
```
```    96   show ?case
```
```    97   proof (cases "distinct (x # xs)")
```
```    98     case True
```
```    99     with `rtrancl_path r x xs y` show ?thesis by (rule less)
```
```   100   next
```
```   101     case False
```
```   102     then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
```
```   103       by (rule not_distinct_decomp)
```
```   104     then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
```
```   105       by iprover
```
```   106     show ?thesis
```
```   107     proof (cases as)
```
```   108       case Nil
```
```   109       with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
```
```   110         by auto
```
```   111       from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
```
```   112         by (auto elim: rtrancl_path_appendE)
```
```   113       from xs have "length cs < length xs" by simp
```
```   114       then show ?thesis
```
```   115         by (rule less(1)) (iprover intro: cs less(2))+
```
```   116     next
```
```   117       case (Cons d ds)
```
```   118       with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
```
```   119         by auto
```
```   120       with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
```
```   121         and ay: "rtrancl_path r a (bs @ a # cs) y"
```
```   122         by (auto elim: rtrancl_path_appendE)
```
```   123       from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
```
```   124       with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
```
```   125         by (rule rtrancl_path_trans)
```
```   126       from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
```
```   127       then show ?thesis
```
```   128         by (rule less(1)) (iprover intro: xy less(2))+
```
```   129     qed
```
```   130   qed
```
```   131 qed
```
```   132
```
```   133 inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   134   for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
```
```   135 where
```
```   136   base: "rtrancl_tab r xs x x"
```
```   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"
```
```   138
```
```   139 lemma rtrancl_path_imp_rtrancl_tab:
```
```   140   assumes path: "rtrancl_path r x xs y"
```
```   141   and x: "distinct (x # xs)"
```
```   142   and ys: "({x} \<union> set xs) \<inter> set ys = {}"
```
```   143   shows "rtrancl_tab r ys x y" using path x ys
```
```   144 proof (induct arbitrary: ys)
```
```   145   case base
```
```   146   show ?case by (rule rtrancl_tab.base)
```
```   147 next
```
```   148   case (step x y zs z)
```
```   149   then have "x \<notin> set ys" by auto
```
```   150   from step have "distinct (y # zs)" by simp
```
```   151   moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
```
```   152     by auto
```
```   153   ultimately have "rtrancl_tab r (x # ys) y z"
```
```   154     by (rule step)
```
```   155   with `x \<notin> set ys` `r x y`
```
```   156   show ?case by (rule rtrancl_tab.step)
```
```   157 qed
```
```   158
```
```   159 lemma rtrancl_tab_imp_rtrancl_path:
```
```   160   assumes tab: "rtrancl_tab r ys x y"
```
```   161   obtains xs where "rtrancl_path r x xs y" using tab
```
```   162 proof induct
```
```   163   case base
```
```   164   from rtrancl_path.base show ?case by (rule base)
```
```   165 next
```
```   166   case step show ?case by (iprover intro: step rtrancl_path.step)
```
```   167 qed
```
```   168
```
```   169 lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
```
```   170 proof
```
```   171   assume "r\<^sup>*\<^sup>* x y"
```
```   172   then obtain xs where "rtrancl_path r x xs y"
```
```   173     by (auto simp add: rtranclp_eq_rtrancl_path)
```
```   174   then obtain xs' where xs': "rtrancl_path r x xs' y"
```
```   175     and distinct: "distinct (x # xs')"
```
```   176     by (rule rtrancl_path_distinct)
```
```   177   have "({x} \<union> set xs') \<inter> set [] = {}" by simp
```
```   178   with xs' distinct show "rtrancl_tab r [] x y"
```
```   179     by (rule rtrancl_path_imp_rtrancl_tab)
```
```   180 next
```
```   181   assume "rtrancl_tab r [] x y"
```
```   182   then obtain xs where "rtrancl_path r x xs y"
```
```   183     by (rule rtrancl_tab_imp_rtrancl_path)
```
```   184   then show "r\<^sup>*\<^sup>* x y"
```
```   185     by (auto simp add: rtranclp_eq_rtrancl_path)
```
```   186 qed
```
```   187
```
```   188 declare rtranclp_rtrancl_eq[code del]
```
```   189 declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
```
```   190
```
```   191 code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce
```
```   192
```
`   193 end`