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