# HG changeset patch
# User wenzelm
# Date 1434732081 -7200
# Node ID 84b8e5c2580ed117f7ffa1790e0e13647d69a92c
# Parent  a79f89a36dffc4a757464a73a9d2d4323f6c3f9f
tuned proofs;

diff -r a79f89a36dff -r 84b8e5c2580e src/HOL/Library/Transitive_Closure_Table.thy
--- 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