power operation on functions in theory Nat; power operation on relations in theory Transitive_Closure

--- a/src/HOL/IsaMakefile	Mon Apr 20 09:32:09 2009 +0200
+++ b/src/HOL/IsaMakefile	Mon Apr 20 09:32:40 2009 +0200
@@ -218,7 +218,6 @@
   Nat_Numeral.thy \
   Presburger.thy \
   Recdef.thy \
-  Relation_Power.thy \
   SetInterval.thy \
   $(SRC)/Provers/Arith/assoc_fold.ML \
   $(SRC)/Provers/Arith/cancel_numeral_factor.ML \

--- a/src/HOL/Nat.thy	Mon Apr 20 09:32:09 2009 +0200
+++ b/src/HOL/Nat.thy	Mon Apr 20 09:32:40 2009 +0200
@@ -1164,6 +1164,37 @@
 end
 
 
+subsection {* Natural operation of natural numbers on functions *}
+
+text {* @{text "f o^ n = f o ... o f"}, the n-fold composition of @{text f} *}
+
+primrec funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
+    "funpow 0 f = id"
+  | "funpow (Suc n) f = f o funpow n f"
+
+abbreviation funpower :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "o^" 80) where
+  "f o^ n \<equiv> funpow n f"
+
+notation (latex output)
+  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+notation (HTML output)
+  funpower ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+lemma funpow_add:
+  "f o^ (m + n) = f o^ m \<circ> f o^ n"
+  by (induct m) simp_all
+
+lemma funpow_swap1:
+  "f ((f o^ n) x) = (f o^ n) (f x)"
+proof -
+  have "f ((f o^ n) x) = (f o^ (n + 1)) x" by simp
+  also have "\<dots>  = (f o^ n o f o^ 1) x" by (simp only: funpow_add)
+  also have "\<dots> = (f o^ n) (f x)" by simp
+  finally show ?thesis .
+qed
+
+
 subsection {* Embedding of the Naturals into any
   @{text semiring_1}: @{term of_nat} *}
 

--- a/src/HOL/Transitive_Closure.thy	Mon Apr 20 09:32:09 2009 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Apr 20 09:32:40 2009 +0200
@@ -630,6 +630,139 @@
 
 declare trancl_into_rtrancl [elim]
 
+subsection {* The power operation on relations *}
+
+text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
+
+primrec relpow :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set" (infixr "^^" 80) where
+    "R ^^ 0 = Id"
+  | "R ^^ Suc n = R O (R ^^ n)"
+
+notation (latex output)
+  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+notation (HTML output)
+  relpow ("(_\<^bsup>_\<^esup>)" [1000] 1000)
+
+lemma rel_pow_1 [simp]:
+  "R ^^ 1 = R"
+  by simp
+
+lemma rel_pow_0_I: 
+  "(x, x) \<in> R ^^ 0"
+  by simp
+
+lemma rel_pow_Suc_I:
+  "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
+  by auto
+
+lemma rel_pow_Suc_I2:
+  "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
+  by (induct n arbitrary: z) (simp, fastsimp)
+
+lemma rel_pow_0_E:
+  "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
+  by simp
+
+lemma rel_pow_Suc_E:
+  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
+  by auto
+
+lemma rel_pow_E:
+  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
+   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
+   \<Longrightarrow> P"
+  by (cases n) auto
+
+lemma rel_pow_Suc_D2:
+  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
+  apply (induct n arbitrary: x z)
+   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
+  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
+  done
+
+lemma rel_pow_Suc_E2:
+  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> P) \<Longrightarrow> P"
+  by (blast dest: rel_pow_Suc_D2)
+
+lemma rel_pow_Suc_D2':
+  "\<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)"
+  by (induct n) (simp_all, blast)
+
+lemma rel_pow_E2:
+  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
+     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
+   \<Longrightarrow> P"
+  apply (cases n, simp)
+  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
+  done
+
+lemma rtrancl_imp_UN_rel_pow:
+  assumes "p \<in> R^*"
+  shows "p \<in> (\<Union>n. R ^^ n)"
+proof (cases p)
+  case (Pair x y)
+  with assms have "(x, y) \<in> R^*" by simp
+  then have "(x, y) \<in> (\<Union>n. R ^^ n)" proof induct
+    case base show ?case by (blast intro: rel_pow_0_I)
+  next
+    case step then show ?case by (blast intro: rel_pow_Suc_I)
+  qed
+  with Pair show ?thesis by simp
+qed
+
+lemma rel_pow_imp_rtrancl:
+  assumes "p \<in> R ^^ n"
+  shows "p \<in> R^*"
+proof (cases p)
+  case (Pair x y)
+  with assms have "(x, y) \<in> R ^^ n" by simp
+  then have "(x, y) \<in> R^*" proof (induct n arbitrary: x y)
+    case 0 then show ?case by simp
+  next
+    case Suc then show ?case
+      by (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
+  qed
+  with Pair show ?thesis by simp
+qed
+
+lemma rtrancl_is_UN_rel_pow:
+  "R^* = (\<Union>n. R ^^ n)"
+  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
+
+lemma rtrancl_power:
+  "p \<in> R^* \<longleftrightarrow> (\<exists>n. p \<in> R ^^ n)"
+  by (simp add: rtrancl_is_UN_rel_pow)
+
+lemma trancl_power:
+  "p \<in> R^+ \<longleftrightarrow> (\<exists>n > 0. p \<in> R ^^ n)"
+  apply (cases p)
+  apply simp
+  apply (rule iffI)
+   apply (drule tranclD2)
+   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
+   apply (rule_tac x="Suc x" in exI)
+   apply (clarsimp simp: rel_comp_def)
+   apply fastsimp
+  apply clarsimp
+  apply (case_tac n, simp)
+  apply clarsimp
+  apply (drule rel_pow_imp_rtrancl)
+  apply (drule rtrancl_into_trancl1) apply auto
+  done
+
+lemma rtrancl_imp_rel_pow:
+  "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R ^^ n"
+  by (auto dest: rtrancl_imp_UN_rel_pow)
+
+lemma single_valued_rel_pow:
+  fixes R :: "('a * 'a) set"
+  shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
+  apply (induct n arbitrary: R)
+  apply simp_all
+  apply (rule single_valuedI)
+  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
+  done
 
 subsection {* Setup of transitivity reasoner *}