power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
authorhaftmann
Mon Apr 20 09:32:40 2009 +0200 (2009-04-20)
changeset 30954cf50e67bc1d1
parent 30953 d5f5ab29d769
child 30955 ef2319d6b6a5
power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure
src/HOL/IsaMakefile
src/HOL/Nat.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Apr 20 09:32:09 2009 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Mon Apr 20 09:32:40 2009 +0200
     1.3 @@ -218,7 +218,6 @@
     1.4    Nat_Numeral.thy \
     1.5    Presburger.thy \
     1.6    Recdef.thy \
     1.7 -  Relation_Power.thy \
     1.8    SetInterval.thy \
     1.9    $(SRC)/Provers/Arith/assoc_fold.ML \
    1.10    $(SRC)/Provers/Arith/cancel_numeral_factor.ML \
     2.1 --- a/src/HOL/Nat.thy	Mon Apr 20 09:32:09 2009 +0200
     2.2 +++ b/src/HOL/Nat.thy	Mon Apr 20 09:32:40 2009 +0200
     2.3 @@ -1164,6 +1164,37 @@
     2.4  end
     2.5  
     2.6  
     2.7 +subsection {* Natural operation of natural numbers on functions *}
     2.8 +
     2.9 +text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    2.10 +
    2.11 +primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    2.12 +    "funpow 0 f = id"
    2.13 +  | "funpow (Suc n) f = f o funpow n f"
    2.14 +
    2.15 +abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
    2.16 +  "f o^ n \<equiv> funpow n f"
    2.17 +
    2.18 +notation (latex output)
    2.19 +  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    2.20 +
    2.21 +notation (HTML output)
    2.22 +  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    2.23 +
    2.24 +lemma funpow_add:
    2.25 +  "f o^ (m + n) = f o^ m \<circ> f o^ n"
    2.26 +  by (induct m) simp_all
    2.27 +
    2.28 +lemma funpow_swap1:
    2.29 +  "f ((f o^ n) x) = (f o^ n) (f x)"
    2.30 +proof -
    2.31 +  have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
    2.32 +  also have "\<dots>  = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
    2.33 +  also have "\<dots> = (f o^ n) (f x)" by simp
    2.34 +  finally show ?thesis .
    2.35 +qed
    2.36 +
    2.37 +
    2.38  subsection {* Embedding of the Naturals into any
    2.39    @{text semiring_1}: @{term of_nat} *}
    2.40  
     3.1 --- a/src/HOL/Transitive_Closure.thy	Mon Apr 20 09:32:09 2009 +0200
     3.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Apr 20 09:32:40 2009 +0200
     3.3 @@ -630,6 +630,139 @@
     3.4  
     3.5  declare trancl_into_rtrancl [elim]
     3.6  
     3.7 +subsection {* The power operation on relations *}
     3.8 +
     3.9 +text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
    3.10 +
    3.11 +primrec relpow :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (infixr "^^" 80) where
    3.12 +    "R ^^ 0 = Id"
    3.13 +  | "R ^^ Suc n = R O (R ^^ n)"
    3.14 +
    3.15 +notation (latex output)
    3.16 +  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    3.17 +
    3.18 +notation (HTML output)
    3.19 +  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
    3.20 +
    3.21 +lemma rel_pow_1 [simp]:
    3.22 +  "R ^^ 1 = R"
    3.23 +  by simp
    3.24 +
    3.25 +lemma rel_pow_0_I: 
    3.26 +  "(x, x) \<in> R ^^ 0"
    3.27 +  by simp
    3.28 +
    3.29 +lemma rel_pow_Suc_I:
    3.30 +  "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
    3.31 +  by auto
    3.32 +
    3.33 +lemma rel_pow_Suc_I2:
    3.34 +  "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
    3.35 +  by (induct n arbitrary: z) (simp, fastsimp)
    3.36 +
    3.37 +lemma rel_pow_0_E:
    3.38 +  "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
    3.39 +  by simp
    3.40 +
    3.41 +lemma rel_pow_Suc_E:
    3.42 +  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
    3.43 +  by auto
    3.44 +
    3.45 +lemma rel_pow_E:
    3.46 +  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
    3.47 +   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
    3.48 +   \<Longrightarrow> P"
    3.49 +  by (cases n) auto
    3.50 +
    3.51 +lemma rel_pow_Suc_D2:
    3.52 +  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
    3.53 +  apply (induct n arbitrary: x z)
    3.54 +   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    3.55 +  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    3.56 +  done
    3.57 +
    3.58 +lemma rel_pow_Suc_E2:
    3.59 +  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P"
    3.60 +  by (blast dest: rel_pow_Suc_D2)
    3.61 +
    3.62 +lemma rel_pow_Suc_D2':
    3.63 +  "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)"
    3.64 +  by (induct n) (simp_all, blast)
    3.65 +
    3.66 +lemma rel_pow_E2:
    3.67 +  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
    3.68 +     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
    3.69 +   \<Longrightarrow> P"
    3.70 +  apply (cases n, simp)
    3.71 +  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
    3.72 +  done
    3.73 +
    3.74 +lemma rtrancl_imp_UN_rel_pow:
    3.75 +  assumes "p \<in> R^*"
    3.76 +  shows "p \<in> (\<Union>n. R ^^ n)"
    3.77 +proof (cases p)
    3.78 +  case (Pair x y)
    3.79 +  with assms have "(x, y) \<in> R^*" by simp
    3.80 +  then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct
    3.81 +    case base show ?case by (blast intro: rel_pow_0_I)
    3.82 +  next
    3.83 +    case step then show ?case by (blast intro: rel_pow_Suc_I)
    3.84 +  qed
    3.85 +  with Pair show ?thesis by simp
    3.86 +qed
    3.87 +
    3.88 +lemma rel_pow_imp_rtrancl:
    3.89 +  assumes "p \<in> R ^^ n"
    3.90 +  shows "p \<in> R^*"
    3.91 +proof (cases p)
    3.92 +  case (Pair x y)
    3.93 +  with assms have "(x, y) \<in> R ^^ n" by simp
    3.94 +  then have "(x, y) \<in> R^*" proof (induct n arbitrary: x y)
    3.95 +    case 0 then show ?case by simp
    3.96 +  next
    3.97 +    case Suc then show ?case
    3.98 +      by (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
    3.99 +  qed
   3.100 +  with Pair show ?thesis by simp
   3.101 +qed
   3.102 +
   3.103 +lemma rtrancl_is_UN_rel_pow:
   3.104 +  "R^* = (\<Union>n. R ^^ n)"
   3.105 +  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   3.106 +
   3.107 +lemma rtrancl_power:
   3.108 +  "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)"
   3.109 +  by (simp add: rtrancl_is_UN_rel_pow)
   3.110 +
   3.111 +lemma trancl_power:
   3.112 +  "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)"
   3.113 +  apply (cases p)
   3.114 +  apply simp
   3.115 +  apply (rule iffI)
   3.116 +   apply (drule tranclD2)
   3.117 +   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
   3.118 +   apply (rule_tac x="Suc x" in exI)
   3.119 +   apply (clarsimp simp: rel_comp_def)
   3.120 +   apply fastsimp
   3.121 +  apply clarsimp
   3.122 +  apply (case_tac n, simp)
   3.123 +  apply clarsimp
   3.124 +  apply (drule rel_pow_imp_rtrancl)
   3.125 +  apply (drule rtrancl_into_trancl1) apply auto
   3.126 +  done
   3.127 +
   3.128 +lemma rtrancl_imp_rel_pow:
   3.129 +  "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n"
   3.130 +  by (auto dest: rtrancl_imp_UN_rel_pow)
   3.131 +
   3.132 +lemma single_valued_rel_pow:
   3.133 +  fixes R :: "('a * 'a) set"
   3.134 +  shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
   3.135 +  apply (induct n arbitrary: R)
   3.136 +  apply simp_all
   3.137 +  apply (rule single_valuedI)
   3.138 +  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   3.139 +  done
   3.140  
   3.141  subsection {* Setup of transitivity reasoner *}
   3.142