src/HOL/Transitive_Closure.thy
 changeset 41987 4ad8f1dc2e0b parent 41792 ff3cb0c418b7 child 42795 66fcc9882784
```     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Mar 15 22:04:02 2011 +0100
1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Mar 16 19:50:56 2011 +0100
1.3 @@ -644,7 +644,7 @@
1.4     apply (auto simp add: Field_def)
1.5    done
1.6
1.7 -lemma finite_trancl: "finite (r^+) = finite r"
1.8 +lemma finite_trancl[simp]: "finite (r^+) = finite r"
1.9    apply auto
1.10     prefer 2
1.11     apply (rule trancl_subset_Field2 [THEN finite_subset])
1.12 @@ -833,14 +833,148 @@
1.13    "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n"
1.14    by (auto dest: rtrancl_imp_UN_rel_pow)
1.15
1.16 +text{* By Sternagel/Thiemann: *}
1.17 +lemma rel_pow_fun_conv:
1.18 +  "((a,b) \<in> R ^^ n) = (\<exists>f. f 0 = a \<and> f n = b \<and> (\<forall>i<n. (f i, f(Suc i)) \<in> R))"
1.19 +proof (induct n arbitrary: b)
1.20 +  case 0 show ?case by auto
1.21 +next
1.22 +  case (Suc n)
1.23 +  show ?case
1.24 +  proof (simp add: rel_comp_def Suc)
1.25 +    show "(\<exists>y. (\<exists>f. f 0 = a \<and> f n = y \<and> (\<forall>i<n. (f i,f(Suc i)) \<in> R)) \<and> (y,b) \<in> R)
1.26 +     = (\<exists>f. f 0 = a \<and> f(Suc n) = b \<and> (\<forall>i<Suc n. (f i, f (Suc i)) \<in> R))"
1.27 +    (is "?l = ?r")
1.28 +    proof
1.29 +      assume ?l
1.30 +      then obtain c f where 1: "f 0 = a"  "f n = c"  "\<And>i. i < n \<Longrightarrow> (f i, f (Suc i)) \<in> R"  "(c,b) \<in> R" by auto
1.31 +      let ?g = "\<lambda> m. if m = Suc n then b else f m"
1.32 +      show ?r by (rule exI[of _ ?g], simp add: 1)
1.33 +    next
1.34 +      assume ?r
1.35 +      then obtain f where 1: "f 0 = a"  "b = f (Suc n)"  "\<And>i. i < Suc n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto
1.36 +      show ?l by (rule exI[of _ "f n"], rule conjI, rule exI[of _ f], insert 1, auto)
1.37 +    qed
1.38 +  qed
1.39 +qed
1.40 +
1.41 +lemma rel_pow_finite_bounded1:
1.42 +assumes "finite(R :: ('a*'a)set)" and "k>0"
1.43 +shows "R^^k \<subseteq> (UN n:{n. 0<n & n <= card R}. R^^n)" (is "_ \<subseteq> ?r")
1.44 +proof-
1.45 +  { fix a b k
1.46 +    have "(a,b) : R^^(Suc k) \<Longrightarrow> EX n. 0<n & n <= card R & (a,b) : R^^n"
1.47 +    proof(induct k arbitrary: b)
1.48 +      case 0
1.49 +      hence "R \<noteq> {}" by auto
1.50 +      with card_0_eq[OF `finite R`] have "card R >= Suc 0" by auto
1.51 +      thus ?case using 0 by force
1.52 +    next
1.53 +      case (Suc k)
1.54 +      then obtain a' where "(a,a') : R^^(Suc k)" and "(a',b) : R" by auto
1.55 +      from Suc(1)[OF `(a,a') : R^^(Suc k)`]
1.56 +      obtain n where "n \<le> card R" and "(a,a') \<in> R ^^ n" by auto
1.57 +      have "(a,b) : R^^(Suc n)" using `(a,a') \<in> R^^n` and `(a',b)\<in> R` by auto
1.58 +      { assume "n < card R"
1.59 +        hence ?case using `(a,b): R^^(Suc n)` Suc_leI[OF `n < card R`] by blast
1.60 +      } moreover
1.61 +      { assume "n = card R"
1.62 +        from `(a,b) \<in> R ^^ (Suc n)`[unfolded rel_pow_fun_conv]
1.63 +        obtain f where "f 0 = a" and "f(Suc n) = b"
1.64 +          and steps: "\<And>i. i <= n \<Longrightarrow> (f i, f (Suc i)) \<in> R" by auto
1.65 +        let ?p = "%i. (f i, f(Suc i))"
1.66 +        let ?N = "{i. i \<le> n}"
1.67 +        have "?p ` ?N <= R" using steps by auto
1.68 +        from card_mono[OF assms(1) this]
1.69 +        have "card(?p ` ?N) <= card R" .
1.70 +        also have "\<dots> < card ?N" using `n = card R` by simp
1.71 +        finally have "~ inj_on ?p ?N" by(rule pigeonhole)
1.72 +        then obtain i j where i: "i <= n" and j: "j <= n" and ij: "i \<noteq> j" and
1.73 +          pij: "?p i = ?p j" by(auto simp: inj_on_def)
1.74 +        let ?i = "min i j" let ?j = "max i j"
1.75 +        have i: "?i <= n" and j: "?j <= n" and pij: "?p ?i = ?p ?j"
1.76 +          and ij: "?i < ?j"
1.77 +          using i j ij pij unfolding min_def max_def by auto
1.78 +        from i j pij ij obtain i j where i: "i<=n" and j: "j<=n" and ij: "i<j"
1.79 +          and pij: "?p i = ?p j" by blast
1.80 +        let ?g = "\<lambda> l. if l \<le> i then f l else f (l + (j - i))"
1.81 +        let ?n = "Suc(n - (j - i))"
1.82 +        have abl: "(a,b) \<in> R ^^ ?n" unfolding rel_pow_fun_conv
1.83 +        proof (rule exI[of _ ?g], intro conjI impI allI)
1.84 +          show "?g ?n = b" using `f(Suc n) = b` j ij by auto
1.85 +        next
1.86 +          fix k assume "k < ?n"
1.87 +          show "(?g k, ?g (Suc k)) \<in> R"
1.88 +          proof (cases "k < i")
1.89 +            case True
1.90 +            with i have "k <= n" by auto
1.91 +            from steps[OF this] show ?thesis using True by simp
1.92 +          next
1.93 +            case False
1.94 +            hence "i \<le> k" by auto
1.95 +            show ?thesis
1.96 +            proof (cases "k = i")
1.97 +              case True
1.98 +              thus ?thesis using ij pij steps[OF i] by simp
1.99 +            next
1.100 +              case False
1.101 +              with `i \<le> k` have "i < k" by auto
1.102 +              hence small: "k + (j - i) <= n" using `k<?n` by arith
1.103 +              show ?thesis using steps[OF small] `i<k` by auto
1.104 +            qed
1.105 +          qed
1.106 +        qed (simp add: `f 0 = a`)
1.107 +        moreover have "?n <= n" using i j ij by arith
1.108 +        ultimately have ?case using `n = card R` by blast
1.109 +      }
1.110 +      ultimately show ?case using `n \<le> card R` by force
1.111 +    qed
1.112 +  }
1.113 +  thus ?thesis using gr0_implies_Suc[OF `k>0`] by auto
1.114 +qed
1.115 +
1.116 +lemma rel_pow_finite_bounded:
1.117 +assumes "finite(R :: ('a*'a)set)"
1.118 +shows "R^^k \<subseteq> (UN n:{n. n <= card R}. R^^n)"
1.119 +apply(cases k)
1.120 + apply force
1.121 +using rel_pow_finite_bounded1[OF assms, of k] by auto
1.122 +
1.123 +lemma rtrancl_finite_eq_rel_pow:
1.124 +  "finite R \<Longrightarrow> R^* = (UN n : {n. n <= card R}. R^^n)"
1.125 +by(fastsimp simp: rtrancl_power dest: rel_pow_finite_bounded)
1.126 +
1.127 +lemma trancl_finite_eq_rel_pow:
1.128 +  "finite R \<Longrightarrow> R^+ = (UN n : {n. 0 < n & n <= card R}. R^^n)"
1.130 +apply(auto dest: rel_pow_finite_bounded1)
1.131 +done
1.132 +
1.133 +lemma finite_rel_comp[simp,intro]:
1.134 +assumes "finite R" and "finite S"
1.135 +shows "finite(R O S)"
1.136 +proof-
1.137 +  have "R O S = (UN (x,y) : R. \<Union>((%(u,v). if u=y then {(x,v)} else {}) ` S))"
1.138 +    by(force simp add: split_def)
1.139 +  thus ?thesis using assms by(clarsimp)
1.140 +qed
1.141 +
1.142 +lemma finite_relpow[simp,intro]:
1.143 +  assumes "finite(R :: ('a*'a)set)" shows "n>0 \<Longrightarrow> finite(R^^n)"
1.144 +apply(induct n)
1.145 + apply simp
1.146 +apply(case_tac n)
1.148 +done
1.149 +
1.150  lemma single_valued_rel_pow:
1.151    fixes R :: "('a * 'a) set"
1.152    shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
1.153 -  apply (induct n arbitrary: R)
1.154 -  apply simp_all
1.155 -  apply (rule single_valuedI)
1.156 -  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
1.157 -  done
1.158 +apply (induct n arbitrary: R)
1.159 +apply simp_all
1.160 +apply (rule single_valuedI)
1.161 +apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
1.162 +done
1.163
1.164  subsection {* Setup of transitivity reasoner *}
1.165
```