separated funpow, relpow from power on monoids
authorhaftmann
Fri Apr 17 15:57:26 2009 +0200 (2009-04-17)
changeset 3094937f887b55e7f
parent 30948 7f699568a877
child 30950 1435a8f01a41
separated funpow, relpow from power on monoids
NEWS
src/HOL/List.thy
src/HOL/Relation_Power.thy
     1.1 --- a/NEWS	Fri Apr 17 15:14:06 2009 +0200
     1.2 +++ b/NEWS	Fri Apr 17 15:57:26 2009 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
     1.5  div_mult_mult1 is now [simp] by default.  INCOMPATIBILITY.
     1.6  
     1.7 +* Power operation on relations and functions is now a dedicated overloaded constant
     1.8 +funpower with infix syntax "^^".  INCOMPATIBILITY.
     1.9 +
    1.10  New in Isabelle2009 (April 2009)
    1.11  --------------------------------
    1.12  
     2.1 --- a/src/HOL/List.thy	Fri Apr 17 15:14:06 2009 +0200
     2.2 +++ b/src/HOL/List.thy	Fri Apr 17 15:57:26 2009 +0200
     2.3 @@ -198,7 +198,7 @@
     2.4  
     2.5  definition
     2.6    rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     2.7 -  "rotate n = rotate1 ^ n"
     2.8 +  "rotate n = rotate1 ^^ n"
     2.9  
    2.10  definition
    2.11    list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
     3.1 --- a/src/HOL/Relation_Power.thy	Fri Apr 17 15:14:06 2009 +0200
     3.2 +++ b/src/HOL/Relation_Power.thy	Fri Apr 17 15:57:26 2009 +0200
     3.3 @@ -9,132 +9,124 @@
     3.4  imports Power Transitive_Closure Plain
     3.5  begin
     3.6  
     3.7 -instance
     3.8 -  "fun" :: (type, type) power ..
     3.9 -      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    3.10 +consts funpower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80)
    3.11  
    3.12  overloading
    3.13 -  relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
    3.14 +  relpow \<equiv> "funpower \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"
    3.15  begin
    3.16  
    3.17 -text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *}
    3.18 +text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
    3.19  
    3.20  primrec relpow where
    3.21 -  "(R \<Colon> ('a \<times> 'a) set)  ^ 0 = Id"
    3.22 -  | "(R \<Colon> ('a \<times> 'a) set) ^ Suc n = R O (R ^ n)"
    3.23 +    "(R \<Colon> ('a \<times> 'a) set) ^^ 0 = Id"
    3.24 +  | "(R \<Colon> ('a \<times> 'a) set) ^^ Suc n = R O (R ^^ n)"
    3.25  
    3.26  end
    3.27  
    3.28  overloading
    3.29 -  funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
    3.30 +  funpow \<equiv> "funpower \<Colon> ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
    3.31  begin
    3.32  
    3.33 -text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    3.34 +text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    3.35  
    3.36  primrec funpow where
    3.37 -  "(f \<Colon> 'a \<Rightarrow> 'a) ^ 0 = id"
    3.38 -  | "(f \<Colon> 'a \<Rightarrow> 'a) ^ Suc n = f o (f ^ n)"
    3.39 +    "(f \<Colon> 'a \<Rightarrow> 'a) ^^ 0 = id"
    3.40 +  | "(f \<Colon> 'a \<Rightarrow> 'a) ^^ Suc n = f o (f ^^ n)"
    3.41  
    3.42  end
    3.43  
    3.44 -text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
    3.45 -functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
    3.46 -and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
    3.47 -For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
    3.48 -constraints.*}
    3.49 -
    3.50 -text {*
    3.51 -  Circumvent this problem for code generation:
    3.52 -*}
    3.53 -
    3.54 -primrec
    3.55 -  fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    3.56 -where
    3.57 -  "fun_pow 0 f = id"
    3.58 +primrec fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
    3.59 +    "fun_pow 0 f = id"
    3.60    | "fun_pow (Suc n) f = f o fun_pow n f"
    3.61  
    3.62 -lemma funpow_fun_pow [code unfold]: "f ^ n = fun_pow n f"
    3.63 +lemma funpow_fun_pow [code unfold]:
    3.64 +  "f ^^ n = fun_pow n f"
    3.65    unfolding funpow_def fun_pow_def ..
    3.66  
    3.67 -lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    3.68 +lemma funpow_add:
    3.69 +  "f ^^ (m + n) = f ^^ m o f ^^ n"
    3.70    by (induct m) simp_all
    3.71  
    3.72 -lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
    3.73 +lemma funpow_swap1:
    3.74 +  "f ((f ^^ n) x) = (f ^^ n) (f x)"
    3.75  proof -
    3.76 -  have "f((f^n) x) = (f^(n+1)) x" unfolding One_nat_def by simp
    3.77 -  also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
    3.78 -  also have "\<dots> = (f^n)(f x)" unfolding One_nat_def by simp
    3.79 +  have "f ((f ^^ n) x) = (f ^^ (n+1)) x" unfolding One_nat_def by simp
    3.80 +  also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
    3.81 +  also have "\<dots> = (f ^^ n) (f x)" unfolding One_nat_def by simp
    3.82    finally show ?thesis .
    3.83  qed
    3.84  
    3.85  lemma rel_pow_1 [simp]:
    3.86 -  fixes R :: "('a*'a)set"
    3.87 -  shows "R^1 = R"
    3.88 -  unfolding One_nat_def by simp
    3.89 -
    3.90 -lemma rel_pow_0_I: "(x,x) : R^0"
    3.91 +  fixes R :: "('a * 'a) set"
    3.92 +  shows "R ^^ 1 = R"
    3.93    by simp
    3.94  
    3.95 -lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
    3.96 +lemma rel_pow_0_I: 
    3.97 +  "(x, x) \<in> R ^^ 0"
    3.98 +  by simp
    3.99 +
   3.100 +lemma rel_pow_Suc_I:
   3.101 +  "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
   3.102    by auto
   3.103  
   3.104  lemma rel_pow_Suc_I2:
   3.105 -    "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
   3.106 -  apply (induct n arbitrary: z)
   3.107 -   apply simp
   3.108 -  apply fastsimp
   3.109 -  done
   3.110 +  "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
   3.111 +  by (induct n arbitrary: z) (simp, fastsimp)
   3.112  
   3.113 -lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
   3.114 +lemma rel_pow_0_E:
   3.115 +  "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
   3.116    by simp
   3.117  
   3.118  lemma rel_pow_Suc_E:
   3.119 -    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
   3.120 +  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
   3.121    by auto
   3.122  
   3.123  lemma rel_pow_E:
   3.124 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
   3.125 -        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
   3.126 -     |] ==> P"
   3.127 +  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
   3.128 +   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
   3.129 +   \<Longrightarrow> P"
   3.130    by (cases n) auto
   3.131  
   3.132  lemma rel_pow_Suc_D2:
   3.133 -    "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
   3.134 +  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
   3.135    apply (induct n arbitrary: x z)
   3.136     apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
   3.137    apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
   3.138    done
   3.139  
   3.140  lemma rel_pow_Suc_D2':
   3.141 -    "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
   3.142 +  "\<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.143    by (induct n) (simp_all, blast)
   3.144  
   3.145  lemma rel_pow_E2:
   3.146 -    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
   3.147 -        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
   3.148 -     |] ==> P"
   3.149 -  apply (case_tac n, simp)
   3.150 +  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
   3.151 +     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
   3.152 +   \<Longrightarrow> P"
   3.153 +  apply (cases n, simp)
   3.154    apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   3.155    done
   3.156  
   3.157 -lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
   3.158 -  apply (simp only: split_tupled_all)
   3.159 +lemma rtrancl_imp_UN_rel_pow:
   3.160 +  "p \<in> R^* \<Longrightarrow> p \<in> (\<Union>n. R ^^ n)"
   3.161 +  apply (cases p) apply (simp only:)
   3.162    apply (erule rtrancl_induct)
   3.163     apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   3.164    done
   3.165  
   3.166 -lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
   3.167 -  apply (simp only: split_tupled_all)
   3.168 -  apply (induct n)
   3.169 +lemma rel_pow_imp_rtrancl:
   3.170 +  "p \<in> R ^^ n \<Longrightarrow> p \<in> R^*"
   3.171 +  apply (induct n arbitrary: p)
   3.172 +  apply (simp_all only: split_tupled_all)
   3.173     apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   3.174    apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   3.175    done
   3.176  
   3.177 -lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   3.178 +lemma rtrancl_is_UN_rel_pow:
   3.179 +  "R^* = (UN n. R ^^ n)"
   3.180    by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   3.181  
   3.182  lemma trancl_power:
   3.183 -  "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
   3.184 +  "x \<in> r^+ = (\<exists>n > 0. x \<in> r ^^ n)"
   3.185    apply (cases x)
   3.186    apply simp
   3.187    apply (rule iffI)
   3.188 @@ -151,30 +143,12 @@
   3.189    done
   3.190  
   3.191  lemma single_valued_rel_pow:
   3.192 -    "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   3.193 +  fixes R :: "('a * 'a) set"
   3.194 +  shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
   3.195 +  apply (induct n arbitrary: R)
   3.196 +  apply simp_all
   3.197    apply (rule single_valuedI)
   3.198 -  apply (induct n)
   3.199 -   apply simp
   3.200    apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   3.201    done
   3.202  
   3.203 -ML
   3.204 -{*
   3.205 -val funpow_add = thm "funpow_add";
   3.206 -val rel_pow_1 = thm "rel_pow_1";
   3.207 -val rel_pow_0_I = thm "rel_pow_0_I";
   3.208 -val rel_pow_Suc_I = thm "rel_pow_Suc_I";
   3.209 -val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
   3.210 -val rel_pow_0_E = thm "rel_pow_0_E";
   3.211 -val rel_pow_Suc_E = thm "rel_pow_Suc_E";
   3.212 -val rel_pow_E = thm "rel_pow_E";
   3.213 -val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   3.214 -val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   3.215 -val rel_pow_E2 = thm "rel_pow_E2";
   3.216 -val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
   3.217 -val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
   3.218 -val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
   3.219 -val single_valued_rel_pow = thm "single_valued_rel_pow";
   3.220 -*}
   3.221 -
   3.222  end