src/HOL/Library/Transitive_Closure_Table.thy

author | wenzelm |

Sat, 31 Oct 2020 21:06:29 +0100 | |

changeset 72526 | a3d096a98b69 |

parent 64632 | 9df24b8b6c0a |

permissions | -rw-r--r-- |

clarified Windows base line;

(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) section \<open>A table-based implementation of the reflexive transitive closure\<close> theory Transitive_Closure_Table imports Main begin inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool" for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where base: "rtrancl_path r x [] x" | step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z" lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)" proof show "\<exists>xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y" using that proof (induct rule: converse_rtranclp_induct) case base have "rtrancl_path r y [] y" by (rule rtrancl_path.base) then show ?case .. next case (step x z) from \<open>\<exists>xs. rtrancl_path r z xs y\<close> obtain xs where "rtrancl_path r z xs y" .. with \<open>r x z\<close> have "rtrancl_path r x (z # xs) y" by (rule rtrancl_path.step) then show ?case .. qed show "r\<^sup>*\<^sup>* x y" if "\<exists>xs. rtrancl_path r x xs y" proof - from that obtain xs where "rtrancl_path r x xs y" .. then show ?thesis proof induct case (base x) show ?case by (rule rtranclp.rtrancl_refl) next case (step x y ys z) from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case by (rule converse_rtranclp_into_rtranclp) qed qed qed lemma rtrancl_path_trans: assumes xy: "rtrancl_path r x xs y" and yz: "rtrancl_path r y ys z" shows "rtrancl_path r x (xs @ ys) z" using xy yz proof (induct arbitrary: z) case (base x) then show ?case by simp next case (step x y xs) then have "rtrancl_path r y (xs @ ys) z" by simp with \<open>r x y\<close> have "rtrancl_path r x (y # (xs @ ys)) z" by (rule rtrancl_path.step) then show ?case by simp qed lemma rtrancl_path_appendE: assumes xz: "rtrancl_path r x (xs @ y # ys) z" obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz proof (induct xs arbitrary: x) case Nil then have "rtrancl_path r x (y # ys) z" by simp then obtain xy: "r x y" and yz: "rtrancl_path r y ys z" by cases auto from xy have "rtrancl_path r x [y] y" by (rule rtrancl_path.step [OF _ rtrancl_path.base]) then have "rtrancl_path r x ([] @ [y]) y" by simp then show thesis using yz by (rule Nil) next case (Cons a as) then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z" by cases auto show thesis proof (rule Cons(1) [OF _ az]) assume "rtrancl_path r y ys z" assume "rtrancl_path r a (as @ [y]) y" with xa have "rtrancl_path r x (a # (as @ [y])) y" by (rule rtrancl_path.step) then have "rtrancl_path r x ((a # as) @ [y]) y" by simp then show thesis using \<open>rtrancl_path r y ys z\<close> by (rule Cons(2)) qed qed lemma rtrancl_path_distinct: assumes xy: "rtrancl_path r x xs y" obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" and "set xs' \<subseteq> set xs" using xy proof (induct xs rule: measure_induct_rule [of length]) case (less xs) show ?case proof (cases "distinct (x # xs)") case True with \<open>rtrancl_path r x xs y\<close> show ?thesis by (rule less) simp next case False then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs" by (rule not_distinct_decomp) then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs" by iprover show ?thesis proof (cases as) case Nil with xxs have x: "x = a" and xs: "xs = bs @ a # cs" by auto from x xs \<open>rtrancl_path r x xs y\<close> have cs: "rtrancl_path r x cs y" "set cs \<subseteq> set xs" by (auto elim: rtrancl_path_appendE) from xs have "length cs < length xs" by simp then show ?thesis by (rule less(1))(blast intro: cs less(2) order_trans del: subsetI)+ next case (Cons d ds) with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)" by auto with \<open>rtrancl_path r x xs y\<close> obtain xa: "rtrancl_path r x (ds @ [a]) a" and ay: "rtrancl_path r a (bs @ a # cs) y" by (auto elim: rtrancl_path_appendE) from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE) with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y" by (rule rtrancl_path_trans) from xs have set: "set ((ds @ [a]) @ cs) \<subseteq> set xs" by auto from xs have "length ((ds @ [a]) @ cs) < length xs" by simp then show ?thesis by (rule less(1))(blast intro: xy less(2) set[THEN subsetD])+ qed qed qed inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where base: "rtrancl_tab r xs x x" | step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z" lemma rtrancl_path_imp_rtrancl_tab: assumes path: "rtrancl_path r x xs y" and x: "distinct (x # xs)" and ys: "({x} \<union> set xs) \<inter> set ys = {}" shows "rtrancl_tab r ys x y" using path x ys proof (induct arbitrary: ys) case base show ?case by (rule rtrancl_tab.base) next case (step x y zs z) then have "x \<notin> set ys" by auto from step have "distinct (y # zs)" by simp moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}" by auto ultimately have "rtrancl_tab r (x # ys) y z" by (rule step) with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case by (rule rtrancl_tab.step) qed lemma rtrancl_tab_imp_rtrancl_path: assumes tab: "rtrancl_tab r ys x y" obtains xs where "rtrancl_path r x xs y" using tab proof induct case base from rtrancl_path.base show ?case by (rule base) next case step show ?case by (iprover intro: step rtrancl_path.step) qed lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y" proof show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y" proof - from that obtain xs where "rtrancl_path r x xs y" by (auto simp add: rtranclp_eq_rtrancl_path) then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')" by (rule rtrancl_path_distinct) have "({x} \<union> set xs') \<inter> set [] = {}" by simp with xs' distinct show ?thesis by (rule rtrancl_path_imp_rtrancl_tab) qed show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y" proof - from that obtain xs where "rtrancl_path r x xs y" by (rule rtrancl_tab_imp_rtrancl_path) then show ?thesis by (auto simp add: rtranclp_eq_rtrancl_path) qed qed declare rtranclp_rtrancl_eq [code del] declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro] code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce lemma rtrancl_path_Range: "\<lbrakk> rtrancl_path R x xs y; z \<in> set xs \<rbrakk> \<Longrightarrow> Rangep R z" by(induction rule: rtrancl_path.induct) auto lemma rtrancl_path_Range_end: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> Rangep R y" by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases) lemma rtrancl_path_nth: "\<lbrakk> rtrancl_path R x xs y; i < length xs \<rbrakk> \<Longrightarrow> R ((x # xs) ! i) (xs ! i)" proof(induction arbitrary: i rule: rtrancl_path.induct) case step thus ?case by(cases i) simp_all qed simp lemma rtrancl_path_last: "\<lbrakk> rtrancl_path R x xs y; xs \<noteq> [] \<rbrakk> \<Longrightarrow> last xs = y" by(induction rule: rtrancl_path.induct)(auto elim: rtrancl_path.cases) lemma rtrancl_path_mono: "\<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" by(induction rule: rtrancl_path.induct)(auto intro: rtrancl_path.intros) end