bouned transitive closure
authorhaftmann
Thu Oct 13 23:27:46 2011 +0200 (2011-10-13 ago)
changeset 45140339a8b3c4791
parent 45139 bdcaa3f3a2f4
child 45141 b2eb87bd541b
bouned transitive closure
src/HOL/Enum.thy
src/HOL/Nitpick.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/Enum.thy	Thu Oct 13 23:02:59 2011 +0200
     1.2 +++ b/src/HOL/Enum.thy	Thu Oct 13 23:27:46 2011 +0200
     1.3 @@ -758,69 +758,13 @@
     1.4      unfolding enum_the_def by (auto split: list.split)
     1.5  qed
     1.6  
     1.7 +
     1.8  subsection {* An executable card operator on finite types *}
     1.9  
    1.10 -lemma
    1.11 -  [code]: "card R = length (filter R enum)"
    1.12 -by (simp add: distinct_length_filter[OF enum_distinct] enum_UNIV Collect_def)
    1.13 -
    1.14 -subsection {* An executable (reflexive) transitive closure on finite relations *}
    1.15 -
    1.16 -text {* Definitions could be moved to Transitive Closure theory if they are of more general use. *}
    1.17 -
    1.18 -definition ntrancl :: "('a * 'a => bool) => nat => ('a * 'a => bool)"
    1.19 -where
    1.20 - [code del]: "ntrancl R n = (UN i : {i. 0 < i & i <= (Suc n)}. R ^^ i)"
    1.21 -
    1.22 -lemma [code]:
    1.23 -  "ntrancl (R :: 'a * 'a => bool) 0 = R"
    1.24 -proof
    1.25 -  show "R <= ntrancl R 0"
    1.26 -    unfolding ntrancl_def by fastforce
    1.27 -next
    1.28 -  { 
    1.29 -    fix i have "(0 < i & i <= Suc 0) = (i = 1)" by auto
    1.30 -  }
    1.31 -  from this show "ntrancl R 0 <= R"
    1.32 -    unfolding ntrancl_def by auto
    1.33 -qed
    1.34 -
    1.35  lemma [code]:
    1.36 -  "ntrancl (R :: 'a * 'a => bool) (Suc n) = (ntrancl R n) O (Id Un R)"
    1.37 -proof
    1.38 -  {
    1.39 -    fix a b
    1.40 -    assume "(a, b) : ntrancl R (Suc n)"
    1.41 -    from this obtain i where "0 < i" "i <= Suc (Suc n)" "(a, b) : R ^^ i"
    1.42 -      unfolding ntrancl_def by auto
    1.43 -    have "(a, b) : ntrancl R n O (Id Un R)"
    1.44 -    proof (cases "i = 1")
    1.45 -      case True
    1.46 -      from this `(a, b) : R ^^ i` show ?thesis
    1.47 -        unfolding ntrancl_def by auto
    1.48 -    next
    1.49 -      case False
    1.50 -      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
    1.51 -        by (cases i) auto
    1.52 -      from this `(a, b) : R ^^ i` obtain c where c1: "(a, c) : R ^^ j" and c2:"(c, b) : R"
    1.53 -        by auto
    1.54 -      from c1 j `i <= Suc (Suc n)` have "(a, c): ntrancl R n"
    1.55 -        unfolding ntrancl_def by fastforce
    1.56 -      from this c2 show ?thesis by fastforce
    1.57 -    qed
    1.58 -  }
    1.59 -  from this show "ntrancl R (Suc n) <= ntrancl R n O (Id Un R)" by auto
    1.60 -next
    1.61 -  show "ntrancl R n O (Id Un R) <= ntrancl R (Suc n)"
    1.62 -    unfolding ntrancl_def by fastforce
    1.63 -qed
    1.64 +  "card R = length (filter R enum)"
    1.65 +  by (simp add: distinct_length_filter [OF enum_distinct] enum_UNIV Collect_def)
    1.66  
    1.67 -lemma [code]: "trancl (R :: ('a :: finite) * 'a => bool) = ntrancl R (card R - 1)"
    1.68 -by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
    1.69 -
    1.70 -(* a copy of Nitpick.rtrancl_unfold, should be moved to Transitive_Closure *)
    1.71 -lemma [code]: "r^* = (r^+)^="
    1.72 -by simp
    1.73  
    1.74  subsection {* Closing up *}
    1.75  
     2.1 --- a/src/HOL/Nitpick.thy	Thu Oct 13 23:02:59 2011 +0200
     2.2 +++ b/src/HOL/Nitpick.thy	Thu Oct 13 23:27:46 2011 +0200
     2.3 @@ -63,7 +63,7 @@
     2.4  by (auto simp: mem_def)
     2.5  
     2.6  lemma rtrancl_unfold [nitpick_unfold, no_atp]: "r\<^sup>* \<equiv> (r\<^sup>+)\<^sup>="
     2.7 -by simp
     2.8 +  by (simp only: rtrancl_trancl_reflcl)
     2.9  
    2.10  lemma rtranclp_unfold [nitpick_unfold, no_atp]:
    2.11  "rtranclp r a b \<equiv> (a = b \<or> tranclp r a b)"
     3.1 --- a/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:02:59 2011 +0200
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Oct 13 23:27:46 2011 +0200
     3.3 @@ -576,6 +576,9 @@
     3.4     apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD], fast)
     3.5    done
     3.6  
     3.7 +lemma rtrancl_trancl_reflcl [code]: "r^* = (r^+)^="
     3.8 +  by simp
     3.9 +
    3.10  lemma trancl_empty [simp]: "{}^+ = {}"
    3.11    by (auto elim: trancl_induct)
    3.12  
    3.13 @@ -980,6 +983,65 @@
    3.14  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
    3.15  done
    3.16  
    3.17 +
    3.18 +subsection {* Bounded transitive closure *}
    3.19 +
    3.20 +definition ntrancl :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"
    3.21 +where
    3.22 +  "ntrancl n R = (\<Union>i\<in>{i. 0 < i \<and> i \<le> Suc n}. R ^^ i)"
    3.23 +
    3.24 +lemma ntrancl_Zero [simp, code]:
    3.25 +  "ntrancl 0 R = R"
    3.26 +proof
    3.27 +  show "R \<subseteq> ntrancl 0 R"
    3.28 +    unfolding ntrancl_def by fastforce
    3.29 +next
    3.30 +  { 
    3.31 +    fix i have "0 < i \<and> i \<le> Suc 0 \<longleftrightarrow> i = 1" by auto
    3.32 +  }
    3.33 +  from this show "ntrancl 0 R \<le> R"
    3.34 +    unfolding ntrancl_def by auto
    3.35 +qed
    3.36 +
    3.37 +lemma ntrancl_Suc [simp, code]:
    3.38 +  "ntrancl (Suc n) R = ntrancl n R O (Id \<union> R)"
    3.39 +proof
    3.40 +  {
    3.41 +    fix a b
    3.42 +    assume "(a, b) \<in> ntrancl (Suc n) R"
    3.43 +    from this obtain i where "0 < i" "i \<le> Suc (Suc n)" "(a, b) \<in> R ^^ i"
    3.44 +      unfolding ntrancl_def by auto
    3.45 +    have "(a, b) \<in> ntrancl n R O (Id \<union> R)"
    3.46 +    proof (cases "i = 1")
    3.47 +      case True
    3.48 +      from this `(a, b) \<in> R ^^ i` show ?thesis
    3.49 +        unfolding ntrancl_def by auto
    3.50 +    next
    3.51 +      case False
    3.52 +      from this `0 < i` obtain j where j: "i = Suc j" "0 < j"
    3.53 +        by (cases i) auto
    3.54 +      from this `(a, b) \<in> R ^^ i` obtain c where c1: "(a, c) \<in> R ^^ j" and c2:"(c, b) \<in> R"
    3.55 +        by auto
    3.56 +      from c1 j `i \<le> Suc (Suc n)` have "(a, c) \<in> ntrancl n R"
    3.57 +        unfolding ntrancl_def by fastforce
    3.58 +      from this c2 show ?thesis by fastforce
    3.59 +    qed
    3.60 +  }
    3.61 +  from this show "ntrancl (Suc n) R \<subseteq> ntrancl n R O (Id \<union> R)"
    3.62 +    by auto
    3.63 +next
    3.64 +  show "ntrancl n R O (Id \<union> R) \<subseteq> ntrancl (Suc n) R"
    3.65 +    unfolding ntrancl_def by fastforce
    3.66 +qed
    3.67 +
    3.68 +lemma finnite_trancl_ntranl:
    3.69 +  "finite R \<Longrightarrow> trancl R = ntrancl (card R - 1) R"
    3.70 +  by (cases "card R") (auto simp add: trancl_finite_eq_rel_pow rel_pow_empty ntrancl_def)
    3.71 +
    3.72 +lemma [code]: "trancl (R :: (('a :: finite) \<times> 'a) set) = ntrancl (card R - 1) R"
    3.73 +  by (simp add: finnite_trancl_ntranl)
    3.74 +
    3.75 +
    3.76  subsection {* Acyclic relations *}
    3.77  
    3.78  definition acyclic :: "('a * 'a) set => bool" where