src/HOL/Relation_Power.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 26072 f65a7fa2da6c
child 26799 5bd38256ce5b
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title:      HOL/Relation_Power.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1996  TU Muenchen
     5 *)
     6 
     7 header{*Powers of Relations and Functions*}
     8 
     9 theory Relation_Power
    10 imports Power Transitive_Closure
    11 begin
    12 
    13 instance
    14   set :: (type) power ..
    15       --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
    16 
    17 overloading
    18   relpow \<equiv> "power \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"  (unchecked)
    19 begin
    20 
    21 text {* @{text "R ^ n = R O ... O R"}, the n-fold composition of @{text R} *}
    22 
    23 primrec relpow where
    24   "(R \<Colon> ('a \<times> 'a) set)  ^ 0 = Id"
    25   | "(R \<Colon> ('a \<times> 'a) set) ^ Suc n = R O (R ^ n)"
    26 
    27 end
    28 
    29 instance
    30   "fun" :: (type, type) power ..
    31       --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
    32 
    33 overloading
    34   funpow \<equiv> "power \<Colon>  ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" (unchecked)
    35 begin
    36 
    37 text {* @{text "f ^ n = f o ... o f"}, the n-fold composition of @{text f} *}
    38 
    39 primrec funpow where
    40   "(f \<Colon> 'a \<Rightarrow> 'a) ^ 0 = id"
    41   | "(f \<Colon> 'a \<Rightarrow> 'a) ^ Suc n = f o (f ^ n)"
    42 
    43 end
    44 
    45 text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
    46 functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
    47 and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
    48 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
    49 constraints.*}
    50 
    51 text {*
    52   Circumvent this problem for code generation:
    53 *}
    54 
    55 primrec
    56   fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
    57 where
    58   "fun_pow 0 f = id"
    59   | "fun_pow (Suc n) f = f o fun_pow n f"
    60 
    61 lemma funpow_fun_pow [code inline]: "f ^ n = fun_pow n f"
    62   unfolding funpow_def fun_pow_def ..
    63 
    64 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    65   by (induct m) simp_all
    66 
    67 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
    68 proof -
    69   have "f((f^n) x) = (f^(n+1)) x" by simp
    70   also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
    71   also have "\<dots> = (f^n)(f x)" by simp
    72   finally show ?thesis .
    73 qed
    74 
    75 lemma rel_pow_1 [simp]:
    76   fixes R :: "('a*'a)set"
    77   shows "R^1 = R"
    78   by simp
    79 
    80 lemma rel_pow_0_I: "(x,x) : R^0"
    81   by simp
    82 
    83 lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
    84   by auto
    85 
    86 lemma rel_pow_Suc_I2:
    87     "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
    88   apply (induct n arbitrary: z)
    89    apply simp
    90   apply fastsimp
    91   done
    92 
    93 lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
    94   by simp
    95 
    96 lemma rel_pow_Suc_E:
    97     "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
    98   by auto
    99 
   100 lemma rel_pow_E:
   101     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
   102         !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
   103      |] ==> P"
   104   by (cases n) auto
   105 
   106 lemma rel_pow_Suc_D2:
   107     "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
   108   apply (induct n arbitrary: x z)
   109    apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
   110   apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
   111   done
   112 
   113 lemma rel_pow_Suc_D2':
   114     "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
   115   by (induct n) (simp_all, blast)
   116 
   117 lemma rel_pow_E2:
   118     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
   119         !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
   120      |] ==> P"
   121   apply (case_tac n, simp)
   122   apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
   123   done
   124 
   125 lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
   126   apply (simp only: split_tupled_all)
   127   apply (erule rtrancl_induct)
   128    apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   129   done
   130 
   131 lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
   132   apply (simp only: split_tupled_all)
   133   apply (induct n)
   134    apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   135   apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   136   done
   137 
   138 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   139   by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   140 
   141 lemma trancl_power:
   142   "x \<in> r^+ = (\<exists>n > 0. x \<in> r^n)"
   143   apply (cases x)
   144   apply simp
   145   apply (rule iffI)
   146    apply (drule tranclD2)
   147    apply (clarsimp simp: rtrancl_is_UN_rel_pow)
   148    apply (rule_tac x="Suc x" in exI)
   149    apply (clarsimp simp: rel_comp_def)
   150    apply fastsimp
   151   apply clarsimp
   152   apply (case_tac n, simp)
   153   apply clarsimp
   154   apply (drule rel_pow_imp_rtrancl)
   155   apply fastsimp
   156   done
   157 
   158 lemma single_valued_rel_pow:
   159     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   160   apply (rule single_valuedI)
   161   apply (induct n)
   162    apply simp
   163   apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   164   done
   165 
   166 ML
   167 {*
   168 val funpow_add = thm "funpow_add";
   169 val rel_pow_1 = thm "rel_pow_1";
   170 val rel_pow_0_I = thm "rel_pow_0_I";
   171 val rel_pow_Suc_I = thm "rel_pow_Suc_I";
   172 val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
   173 val rel_pow_0_E = thm "rel_pow_0_E";
   174 val rel_pow_Suc_E = thm "rel_pow_Suc_E";
   175 val rel_pow_E = thm "rel_pow_E";
   176 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   177 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   178 val rel_pow_E2 = thm "rel_pow_E2";
   179 val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
   180 val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
   181 val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
   182 val single_valued_rel_pow = thm "single_valued_rel_pow";
   183 *}
   184 
   185 end