tuned proofs;
authorwenzelm
Fri Jun 19 18:41:21 2015 +0200 (2015-06-19)
changeset 6051984b8e5c2580e
parent 60518 a79f89a36dff
child 60520 09fc5eaa21ce
tuned proofs;
src/HOL/Library/Transitive_Closure_Table.thy
     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