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.129 +apply(auto simp add: trancl_power)
   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.147 + apply(simp_all add: assms)
   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