author | wenzelm |

Fri Jun 19 18:41:21 2015 +0200 (2015-06-19) | |

changeset 60519 | 84b8e5c2580e |

parent 60518 | a79f89a36dff |

child 60520 | 09fc5eaa21ce |

tuned proofs;

1.1 --- a/src/HOL/Library/Transitive_Closure_Table.thy Fri Jun 19 15:02:24 2015 +0200 1.2 +++ b/src/HOL/Library/Transitive_Closure_Table.thy Fri Jun 19 18:41:21 2015 +0200 1.3 @@ -1,4 +1,4 @@ 1.4 -(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) 1.5 +(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *) 1.6 1.7 section \<open>A table-based implementation of the reflexive transitive closure\<close> 1.8 1.9 @@ -12,10 +12,10 @@ 1.10 base: "rtrancl_path r x [] x" 1.11 | step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z" 1.12 1.13 -lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)" 1.14 +lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> (\<exists>xs. rtrancl_path r x xs y)" 1.15 proof 1.16 - assume "r\<^sup>*\<^sup>* x y" 1.17 - then show "\<exists>xs. rtrancl_path r x xs y" 1.18 + show "\<exists>xs. rtrancl_path r x xs y" if "r\<^sup>*\<^sup>* x y" 1.19 + using that 1.20 proof (induct rule: converse_rtranclp_induct) 1.21 case base 1.22 have "rtrancl_path r y [] y" by (rule rtrancl_path.base) 1.23 @@ -28,23 +28,25 @@ 1.24 by (rule rtrancl_path.step) 1.25 then show ?case .. 1.26 qed 1.27 -next 1.28 - assume "\<exists>xs. rtrancl_path r x xs y" 1.29 - then obtain xs where "rtrancl_path r x xs y" .. 1.30 - then show "r\<^sup>*\<^sup>* x y" 1.31 - proof induct 1.32 - case (base x) 1.33 - show ?case by (rule rtranclp.rtrancl_refl) 1.34 - next 1.35 - case (step x y ys z) 1.36 - from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case 1.37 - by (rule converse_rtranclp_into_rtranclp) 1.38 + show "r\<^sup>*\<^sup>* x y" if "\<exists>xs. rtrancl_path r x xs y" 1.39 + proof - 1.40 + from that obtain xs where "rtrancl_path r x xs y" .. 1.41 + then show ?thesis 1.42 + proof induct 1.43 + case (base x) 1.44 + show ?case 1.45 + by (rule rtranclp.rtrancl_refl) 1.46 + next 1.47 + case (step x y ys z) 1.48 + from \<open>r x y\<close> \<open>r\<^sup>*\<^sup>* y z\<close> show ?case 1.49 + by (rule converse_rtranclp_into_rtranclp) 1.50 + qed 1.51 qed 1.52 qed 1.53 1.54 lemma rtrancl_path_trans: 1.55 assumes xy: "rtrancl_path r x xs y" 1.56 - and yz: "rtrancl_path r y ys z" 1.57 + and yz: "rtrancl_path r y ys z" 1.58 shows "rtrancl_path r x (xs @ ys) z" using xy yz 1.59 proof (induct arbitrary: z) 1.60 case (base x) 1.61 @@ -60,7 +62,8 @@ 1.62 1.63 lemma rtrancl_path_appendE: 1.64 assumes xz: "rtrancl_path r x (xs @ y # ys) z" 1.65 - obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz 1.66 + obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" 1.67 + using xz 1.68 proof (induct xs arbitrary: x) 1.69 case Nil 1.70 then have "rtrancl_path r x (y # ys) z" by simp 1.71 @@ -69,13 +72,13 @@ 1.72 from xy have "rtrancl_path r x [y] y" 1.73 by (rule rtrancl_path.step [OF _ rtrancl_path.base]) 1.74 then have "rtrancl_path r x ([] @ [y]) y" by simp 1.75 - then show ?thesis using yz by (rule Nil) 1.76 + then show thesis using yz by (rule Nil) 1.77 next 1.78 case (Cons a as) 1.79 then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp 1.80 then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z" 1.81 by cases auto 1.82 - show ?thesis 1.83 + show thesis 1.84 proof (rule Cons(1) [OF _ az]) 1.85 assume "rtrancl_path r y ys z" 1.86 assume "rtrancl_path r a (as @ [y]) y" 1.87 @@ -83,14 +86,15 @@ 1.88 by (rule rtrancl_path.step) 1.89 then have "rtrancl_path r x ((a # as) @ [y]) y" 1.90 by simp 1.91 - then show ?thesis using \<open>rtrancl_path r y ys z\<close> 1.92 + then show thesis using \<open>rtrancl_path r y ys z\<close> 1.93 by (rule Cons(2)) 1.94 qed 1.95 qed 1.96 1.97 lemma rtrancl_path_distinct: 1.98 assumes xy: "rtrancl_path r x xs y" 1.99 - obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy 1.100 + obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" 1.101 + using xy 1.102 proof (induct xs rule: measure_induct_rule [of length]) 1.103 case (less xs) 1.104 show ?case 1.105 @@ -138,56 +142,68 @@ 1.106 1.107 lemma rtrancl_path_imp_rtrancl_tab: 1.108 assumes path: "rtrancl_path r x xs y" 1.109 - and x: "distinct (x # xs)" 1.110 - and ys: "({x} \<union> set xs) \<inter> set ys = {}" 1.111 - shows "rtrancl_tab r ys x y" using path x ys 1.112 + and x: "distinct (x # xs)" 1.113 + and ys: "({x} \<union> set xs) \<inter> set ys = {}" 1.114 + shows "rtrancl_tab r ys x y" 1.115 + using path x ys 1.116 proof (induct arbitrary: ys) 1.117 case base 1.118 - show ?case by (rule rtrancl_tab.base) 1.119 + show ?case 1.120 + by (rule rtrancl_tab.base) 1.121 next 1.122 case (step x y zs z) 1.123 - then have "x \<notin> set ys" by auto 1.124 - from step have "distinct (y # zs)" by simp 1.125 + then have "x \<notin> set ys" 1.126 + by auto 1.127 + from step have "distinct (y # zs)" 1.128 + by simp 1.129 moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}" 1.130 by auto 1.131 ultimately have "rtrancl_tab r (x # ys) y z" 1.132 by (rule step) 1.133 - with \<open>x \<notin> set ys\<close> \<open>r x y\<close> 1.134 - show ?case by (rule rtrancl_tab.step) 1.135 + with \<open>x \<notin> set ys\<close> \<open>r x y\<close> show ?case 1.136 + by (rule rtrancl_tab.step) 1.137 qed 1.138 1.139 lemma rtrancl_tab_imp_rtrancl_path: 1.140 assumes tab: "rtrancl_tab r ys x y" 1.141 - obtains xs where "rtrancl_path r x xs y" using tab 1.142 + obtains xs where "rtrancl_path r x xs y" 1.143 + using tab 1.144 proof induct 1.145 case base 1.146 - from rtrancl_path.base show ?case by (rule base) 1.147 + from rtrancl_path.base show ?case 1.148 + by (rule base) 1.149 next 1.150 - case step show ?case by (iprover intro: step rtrancl_path.step) 1.151 + case step 1.152 + show ?case 1.153 + by (iprover intro: step rtrancl_path.step) 1.154 qed 1.155 1.156 -lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y" 1.157 +lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y \<longleftrightarrow> rtrancl_tab r [] x y" 1.158 proof 1.159 - assume "r\<^sup>*\<^sup>* x y" 1.160 - then obtain xs where "rtrancl_path r x xs y" 1.161 - by (auto simp add: rtranclp_eq_rtrancl_path) 1.162 - then obtain xs' where xs': "rtrancl_path r x xs' y" 1.163 - and distinct: "distinct (x # xs')" 1.164 - by (rule rtrancl_path_distinct) 1.165 - have "({x} \<union> set xs') \<inter> set [] = {}" by simp 1.166 - with xs' distinct show "rtrancl_tab r [] x y" 1.167 - by (rule rtrancl_path_imp_rtrancl_tab) 1.168 -next 1.169 - assume "rtrancl_tab r [] x y" 1.170 - then obtain xs where "rtrancl_path r x xs y" 1.171 - by (rule rtrancl_tab_imp_rtrancl_path) 1.172 - then show "r\<^sup>*\<^sup>* x y" 1.173 - by (auto simp add: rtranclp_eq_rtrancl_path) 1.174 + show "rtrancl_tab r [] x y" if "r\<^sup>*\<^sup>* x y" 1.175 + proof - 1.176 + from that obtain xs where "rtrancl_path r x xs y" 1.177 + by (auto simp add: rtranclp_eq_rtrancl_path) 1.178 + then obtain xs' where xs': "rtrancl_path r x xs' y" and distinct: "distinct (x # xs')" 1.179 + by (rule rtrancl_path_distinct) 1.180 + have "({x} \<union> set xs') \<inter> set [] = {}" 1.181 + by simp 1.182 + with xs' distinct show ?thesis 1.183 + by (rule rtrancl_path_imp_rtrancl_tab) 1.184 + qed 1.185 + show "r\<^sup>*\<^sup>* x y" if "rtrancl_tab r [] x y" 1.186 + proof - 1.187 + from that obtain xs where "rtrancl_path r x xs y" 1.188 + by (rule rtrancl_tab_imp_rtrancl_path) 1.189 + then show ?thesis 1.190 + by (auto simp add: rtranclp_eq_rtrancl_path) 1.191 + qed 1.192 qed 1.193 1.194 -declare rtranclp_rtrancl_eq[code del] 1.195 -declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro] 1.196 +declare rtranclp_rtrancl_eq [code del] 1.197 +declare rtranclp_eq_rtrancl_tab_nil [THEN iffD2, code_pred_intro] 1.198 1.199 -code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce 1.200 +code_pred rtranclp 1.201 + using rtranclp_eq_rtrancl_tab_nil [THEN iffD1] by fastforce 1.202 1.203 end 1.204 \ No newline at end of file