src/HOL/Relation_Power.thy
author nipkow
Mon Oct 31 01:43:22 2005 +0100 (2005-10-31)
changeset 18049 156bba334c12
parent 15410 18914688a5fd
child 18398 5d63a8b35688
permissions -rw-r--r--
A few new lemmas
     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 Nat
    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 (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 (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 lemma funpow_add: "f ^ (m+n) = f^m o f^n"
    39 by(induct m) simp_all
    40 
    41 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
    42 proof -
    43   have "f((f^n) x) = (f^(n+1)) x" by simp
    44   also have "\<dots>  = (f^n o f^1) x" by (simp only:funpow_add)
    45   also have "\<dots> = (f^n)(f x)" by simp
    46   finally show ?thesis .
    47 qed
    48 
    49 lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
    50 by simp
    51 declare rel_pow_1 [simp]
    52 
    53 lemma rel_pow_0_I: "(x,x) : R^0"
    54 by simp
    55 
    56 lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
    57 apply (auto ); 
    58 done
    59 
    60 lemma rel_pow_Suc_I2 [rule_format]:
    61      "\<forall>z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)"
    62 apply (induct_tac "n", simp_all)
    63 apply blast
    64 done
    65 
    66 lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
    67 by simp
    68 
    69 lemma rel_pow_Suc_E: 
    70      "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
    71 by auto
    72 
    73 lemma rel_pow_E: 
    74     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
    75         !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P   
    76      |] ==> P"
    77 by (case_tac "n", auto)
    78 
    79 lemma rel_pow_Suc_D2 [rule_format]:
    80      "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>y. (x,y):R & (y,z):R^n)"
    81 apply (induct_tac "n")
    82 apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
    83 apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
    84 done
    85 
    86 
    87 lemma rel_pow_Suc_D2':
    88      "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
    89 by (induct_tac "n", simp_all, blast)
    90 
    91 lemma rel_pow_E2: 
    92     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
    93         !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P   
    94      |] ==> P"
    95 apply (case_tac "n", simp) 
    96 apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) 
    97 done
    98 
    99 lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
   100 apply (simp only: split_tupled_all)
   101 apply (erule rtrancl_induct)
   102 apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
   103 done
   104 
   105 lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
   106 apply (simp only: split_tupled_all)
   107 apply (induct "n")
   108 apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
   109 apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
   110 done
   111 
   112 lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
   113 by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
   114 
   115 
   116 lemma single_valued_rel_pow [rule_format]:
   117      "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
   118 apply (rule single_valuedI)
   119 apply (induct_tac "n", simp)
   120 apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
   121 done
   122 
   123 ML
   124 {*
   125 val funpow_add = thm "funpow_add";
   126 val rel_pow_1 = thm "rel_pow_1";
   127 val rel_pow_0_I = thm "rel_pow_0_I";
   128 val rel_pow_Suc_I = thm "rel_pow_Suc_I";
   129 val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
   130 val rel_pow_0_E = thm "rel_pow_0_E";
   131 val rel_pow_Suc_E = thm "rel_pow_Suc_E";
   132 val rel_pow_E = thm "rel_pow_E";
   133 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   134 val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
   135 val rel_pow_E2 = thm "rel_pow_E2";
   136 val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
   137 val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
   138 val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
   139 val single_valued_rel_pow = thm "single_valued_rel_pow";
   140 *}
   141 
   142 end