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
nipkow@10213
     1
(*  Title:      HOL/Relation_Power.thy
nipkow@10213
     2
    ID:         $Id$
nipkow@10213
     3
    Author:     Tobias Nipkow
nipkow@10213
     4
    Copyright   1996  TU Muenchen
paulson@15410
     5
*)
nipkow@11306
     6
paulson@15410
     7
header{*Powers of Relations and Functions*}
nipkow@10213
     8
nipkow@15131
     9
theory Relation_Power
nipkow@15140
    10
imports Nat
nipkow@15131
    11
begin
nipkow@10213
    12
nipkow@10213
    13
instance
paulson@15410
    14
  set :: (type) power ..  
paulson@15410
    15
      --{* only type @{typ "('a * 'a) set"} should be in class @{text power}!*}
nipkow@10213
    16
paulson@15410
    17
(*R^n = R O ... O R, the n-fold composition of R*)
nipkow@10213
    18
primrec (relpow)
nipkow@10213
    19
  "R^0 = Id"
nipkow@10213
    20
  "R^(Suc n) = R O (R^n)"
nipkow@10213
    21
nipkow@11305
    22
nipkow@11306
    23
instance
paulson@15410
    24
  fun :: (type, type) power ..
paulson@15410
    25
      --{* only type @{typ "'a => 'a"} should be in class @{text power}!*}
nipkow@11305
    26
paulson@15410
    27
(*f^n = f o ... o f, the n-fold composition of f*)
nipkow@11305
    28
primrec (funpow)
nipkow@11305
    29
  "f^0 = id"
nipkow@11305
    30
  "f^(Suc n) = f o (f^n)"
nipkow@11305
    31
paulson@15410
    32
text{*WARNING: due to the limits of Isabelle's type classes, exponentiation on
paulson@15410
    33
functions and relations has too general a domain, namely @{typ "('a * 'b)set"}
paulson@15410
    34
and @{typ "'a => 'b"}.  Explicit type constraints may therefore be necessary.
paulson@15410
    35
For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need
paulson@15410
    36
constraints.*}
paulson@15410
    37
nipkow@15112
    38
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
nipkow@15112
    39
by(induct m) simp_all
nipkow@15112
    40
nipkow@18049
    41
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
nipkow@18049
    42
proof -
nipkow@18049
    43
  have "f((f^n) x) = (f^(n+1)) x" by simp
nipkow@18049
    44
  also have "\<dots>  = (f^n o f^1) x" by (simp only:funpow_add)
nipkow@18049
    45
  also have "\<dots> = (f^n)(f x)" by simp
nipkow@18049
    46
  finally show ?thesis .
nipkow@18049
    47
qed
nipkow@18049
    48
paulson@15410
    49
lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R"
paulson@15410
    50
by simp
paulson@15410
    51
declare rel_pow_1 [simp]
paulson@15410
    52
paulson@15410
    53
lemma rel_pow_0_I: "(x,x) : R^0"
paulson@15410
    54
by simp
paulson@15410
    55
paulson@15410
    56
lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
paulson@15410
    57
apply (auto ); 
paulson@15410
    58
done
paulson@15410
    59
paulson@15410
    60
lemma rel_pow_Suc_I2 [rule_format]:
paulson@15410
    61
     "\<forall>z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)"
paulson@15410
    62
apply (induct_tac "n", simp_all)
paulson@15410
    63
apply blast
paulson@15410
    64
done
paulson@15410
    65
paulson@15410
    66
lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
paulson@15410
    67
by simp
paulson@15410
    68
paulson@15410
    69
lemma rel_pow_Suc_E: 
paulson@15410
    70
     "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
paulson@15410
    71
by auto
paulson@15410
    72
paulson@15410
    73
lemma rel_pow_E: 
paulson@15410
    74
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
paulson@15410
    75
        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P   
paulson@15410
    76
     |] ==> P"
paulson@15410
    77
by (case_tac "n", auto)
paulson@15410
    78
paulson@15410
    79
lemma rel_pow_Suc_D2 [rule_format]:
paulson@15410
    80
     "\<forall>x z. (x,z):R^(Suc n) --> (\<exists>y. (x,y):R & (y,z):R^n)"
paulson@15410
    81
apply (induct_tac "n")
paulson@15410
    82
apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
paulson@15410
    83
apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
paulson@15410
    84
done
paulson@15410
    85
paulson@15410
    86
paulson@15410
    87
lemma rel_pow_Suc_D2':
paulson@15410
    88
     "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
paulson@15410
    89
by (induct_tac "n", simp_all, blast)
paulson@15410
    90
paulson@15410
    91
lemma rel_pow_E2: 
paulson@15410
    92
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;         
paulson@15410
    93
        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P   
paulson@15410
    94
     |] ==> P"
paulson@15410
    95
apply (case_tac "n", simp) 
paulson@15410
    96
apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast) 
paulson@15410
    97
done
paulson@15410
    98
paulson@15410
    99
lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
paulson@15410
   100
apply (simp only: split_tupled_all)
paulson@15410
   101
apply (erule rtrancl_induct)
paulson@15410
   102
apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
paulson@15410
   103
done
paulson@15410
   104
paulson@15410
   105
lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
paulson@15410
   106
apply (simp only: split_tupled_all)
paulson@15410
   107
apply (induct "n")
paulson@15410
   108
apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
paulson@15410
   109
apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
paulson@15410
   110
done
paulson@15410
   111
paulson@15410
   112
lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
paulson@15410
   113
by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
paulson@15410
   114
paulson@15410
   115
paulson@15410
   116
lemma single_valued_rel_pow [rule_format]:
paulson@15410
   117
     "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
paulson@15410
   118
apply (rule single_valuedI)
paulson@15410
   119
apply (induct_tac "n", simp)
paulson@15410
   120
apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
paulson@15410
   121
done
paulson@15410
   122
paulson@15410
   123
ML
paulson@15410
   124
{*
paulson@15410
   125
val funpow_add = thm "funpow_add";
paulson@15410
   126
val rel_pow_1 = thm "rel_pow_1";
paulson@15410
   127
val rel_pow_0_I = thm "rel_pow_0_I";
paulson@15410
   128
val rel_pow_Suc_I = thm "rel_pow_Suc_I";
paulson@15410
   129
val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
paulson@15410
   130
val rel_pow_0_E = thm "rel_pow_0_E";
paulson@15410
   131
val rel_pow_Suc_E = thm "rel_pow_Suc_E";
paulson@15410
   132
val rel_pow_E = thm "rel_pow_E";
paulson@15410
   133
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
paulson@15410
   134
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
paulson@15410
   135
val rel_pow_E2 = thm "rel_pow_E2";
paulson@15410
   136
val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
paulson@15410
   137
val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
paulson@15410
   138
val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
paulson@15410
   139
val single_valued_rel_pow = thm "single_valued_rel_pow";
paulson@15410
   140
*}
paulson@15410
   141
nipkow@10213
   142
end