summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 19 Jun 2015 18:41:21 +0200 | |

changeset 60519 | 84b8e5c2580e |

parent 60518 | a79f89a36dff |

child 60520 | 09fc5eaa21ce |

tuned proofs;

--- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Jun 19 15:02:24 2015 +0200 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Jun 19 18:41:21 2015 +0200 @@ -1,4 +1,4 @@ -(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) +(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) section \<open>A table-based implementation of the reflexive transitive closure\<close> @@ -12,10 +12,10 @@ 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 = (\<exists>xs. rtrancl_path r x xs y)" +lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)" proof - assume "r\<^sup>*\<^sup>* x y" - then show "\<exists>xs. rtrancl_path r x xs y" + 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) @@ -28,23 +28,25 @@ by (rule rtrancl_path.step) then show ?case .. qed -next - assume "\<exists>xs. rtrancl_path r x xs y" - then obtain xs where "rtrancl_path r x xs y" .. - then show "r\<^sup>*\<^sup>* x y" - 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) + 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" + 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) @@ -60,7 +62,8 @@ 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 + 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 @@ -69,13 +72,13 @@ 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) + 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 + show thesis proof (rule Cons(1) [OF _ az]) assume "rtrancl_path r y ys z" assume "rtrancl_path r a (as @ [y]) y" @@ -83,14 +86,15 @@ 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> + 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')" using xy + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" + using xy proof (induct xs rule: measure_induct_rule [of length]) case (less xs) show ?case @@ -138,56 +142,68 @@ 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 + 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) + 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 + 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) + 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 + obtains xs where "rtrancl_path r x xs y" + using tab proof induct case base - from rtrancl_path.base show ?case by (rule base) + from rtrancl_path.base show ?case + by (rule base) next - case step show ?case by (iprover intro: step rtrancl_path.step) + case step + show ?case + by (iprover intro: step rtrancl_path.step) qed -lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y" +lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y" proof - assume "r\<^sup>*\<^sup>* x y" - then 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 "rtrancl_tab r [] x y" - by (rule rtrancl_path_imp_rtrancl_tab) -next - assume "rtrancl_tab r [] x y" - then obtain xs where "rtrancl_path r x xs y" - by (rule rtrancl_tab_imp_rtrancl_path) - then show "r\<^sup>*\<^sup>* x y" - by (auto simp add: rtranclp_eq_rtrancl_path) + 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] +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 +code_pred rtranclp + using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce end \ No newline at end of file