src/HOL/Relation_Power.thy
author haftmann
Wed Sep 26 20:27:55 2007 +0200 (2007-09-26)
changeset 24728 e2b3a1065676
parent 24304 69d40a562ba4
child 24996 ebd5f4cc7118
permissions -rw-r--r--
moved Finite_Set before Datatype
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
wenzelm@18398
    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*)
haftmann@24304
    18
primrec (unchecked 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
haftmann@21414
    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*)
haftmann@24304
    28
primrec (unchecked 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
haftmann@21414
    38
text {*
haftmann@21414
    39
  Circumvent this problem for code generation:
haftmann@21414
    40
*}
haftmann@21414
    41
haftmann@21414
    42
definition
haftmann@22737
    43
  funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@22737
    44
where
haftmann@21414
    45
  funpow_def: "funpow n f = f ^ n"
haftmann@21414
    46
haftmann@21414
    47
lemmas [code inline] = funpow_def [symmetric]
haftmann@21414
    48
haftmann@21414
    49
lemma [code func]:
haftmann@21414
    50
  "funpow 0 f = id"
haftmann@21414
    51
  "funpow (Suc n) f = f o funpow n f"
haftmann@21414
    52
  unfolding funpow_def by simp_all
haftmann@21414
    53
nipkow@15112
    54
lemma funpow_add: "f ^ (m+n) = f^m o f^n"
wenzelm@18398
    55
  by (induct m) simp_all
nipkow@15112
    56
nipkow@18049
    57
lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)"
nipkow@18049
    58
proof -
nipkow@18049
    59
  have "f((f^n) x) = (f^(n+1)) x" by simp
wenzelm@18398
    60
  also have "\<dots>  = (f^n o f^1) x" by (simp only: funpow_add)
nipkow@18049
    61
  also have "\<dots> = (f^n)(f x)" by simp
nipkow@18049
    62
  finally show ?thesis .
nipkow@18049
    63
qed
nipkow@18049
    64
wenzelm@18398
    65
lemma rel_pow_1 [simp]:
wenzelm@18398
    66
  fixes R :: "('a*'a)set"
wenzelm@18398
    67
  shows "R^1 = R"
wenzelm@18398
    68
  by simp
paulson@15410
    69
paulson@15410
    70
lemma rel_pow_0_I: "(x,x) : R^0"
wenzelm@18398
    71
  by simp
paulson@15410
    72
paulson@15410
    73
lemma rel_pow_Suc_I: "[| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)"
wenzelm@18398
    74
  by auto
paulson@15410
    75
wenzelm@18398
    76
lemma rel_pow_Suc_I2:
wenzelm@18398
    77
    "(x, y) : R \<Longrightarrow> (y, z) : R^n \<Longrightarrow> (x,z) : R^(Suc n)"
wenzelm@20503
    78
  apply (induct n arbitrary: z)
wenzelm@18398
    79
   apply simp
wenzelm@18398
    80
  apply fastsimp
wenzelm@18398
    81
  done
paulson@15410
    82
paulson@15410
    83
lemma rel_pow_0_E: "[| (x,y) : R^0; x=y ==> P |] ==> P"
wenzelm@18398
    84
  by simp
paulson@15410
    85
wenzelm@18398
    86
lemma rel_pow_Suc_E:
wenzelm@18398
    87
    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P"
wenzelm@18398
    88
  by auto
paulson@15410
    89
wenzelm@18398
    90
lemma rel_pow_E:
wenzelm@18398
    91
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
wenzelm@18398
    92
        !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P
paulson@15410
    93
     |] ==> P"
wenzelm@18398
    94
  by (cases n) auto
paulson@15410
    95
wenzelm@18398
    96
lemma rel_pow_Suc_D2:
wenzelm@18398
    97
    "(x, z) : R^(Suc n) \<Longrightarrow> (\<exists>y. (x,y) : R & (y,z) : R^n)"
wenzelm@20503
    98
  apply (induct n arbitrary: x z)
wenzelm@18398
    99
   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
wenzelm@18398
   100
  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
wenzelm@18398
   101
  done
paulson@15410
   102
paulson@15410
   103
lemma rel_pow_Suc_D2':
wenzelm@18398
   104
    "\<forall>x y z. (x,y) : R^n & (y,z) : R --> (\<exists>w. (x,w) : R & (w,z) : R^n)"
wenzelm@18398
   105
  by (induct n) (simp_all, blast)
paulson@15410
   106
wenzelm@18398
   107
lemma rel_pow_E2:
wenzelm@18398
   108
    "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;
wenzelm@18398
   109
        !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P
paulson@15410
   110
     |] ==> P"
wenzelm@18398
   111
  apply (case_tac n, simp)
wenzelm@18398
   112
  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
wenzelm@18398
   113
  done
paulson@15410
   114
paulson@15410
   115
lemma rtrancl_imp_UN_rel_pow: "!!p. p:R^* ==> p : (UN n. R^n)"
wenzelm@18398
   116
  apply (simp only: split_tupled_all)
wenzelm@18398
   117
  apply (erule rtrancl_induct)
wenzelm@18398
   118
   apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
wenzelm@18398
   119
  done
paulson@15410
   120
paulson@15410
   121
lemma rel_pow_imp_rtrancl: "!!p. p:R^n ==> p:R^*"
wenzelm@18398
   122
  apply (simp only: split_tupled_all)
wenzelm@18398
   123
  apply (induct n)
wenzelm@18398
   124
   apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
wenzelm@18398
   125
  apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
wenzelm@18398
   126
  done
paulson@15410
   127
paulson@15410
   128
lemma rtrancl_is_UN_rel_pow: "R^* = (UN n. R^n)"
wenzelm@18398
   129
  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
paulson@15410
   130
paulson@15410
   131
wenzelm@18398
   132
lemma single_valued_rel_pow:
wenzelm@18398
   133
    "!!r::('a * 'a)set. single_valued r ==> single_valued (r^n)"
wenzelm@18398
   134
  apply (rule single_valuedI)
wenzelm@18398
   135
  apply (induct n)
wenzelm@18398
   136
   apply simp
wenzelm@18398
   137
  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
wenzelm@18398
   138
  done
paulson@15410
   139
paulson@15410
   140
ML
paulson@15410
   141
{*
paulson@15410
   142
val funpow_add = thm "funpow_add";
paulson@15410
   143
val rel_pow_1 = thm "rel_pow_1";
paulson@15410
   144
val rel_pow_0_I = thm "rel_pow_0_I";
paulson@15410
   145
val rel_pow_Suc_I = thm "rel_pow_Suc_I";
paulson@15410
   146
val rel_pow_Suc_I2 = thm "rel_pow_Suc_I2";
paulson@15410
   147
val rel_pow_0_E = thm "rel_pow_0_E";
paulson@15410
   148
val rel_pow_Suc_E = thm "rel_pow_Suc_E";
paulson@15410
   149
val rel_pow_E = thm "rel_pow_E";
paulson@15410
   150
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
paulson@15410
   151
val rel_pow_Suc_D2 = thm "rel_pow_Suc_D2";
paulson@15410
   152
val rel_pow_E2 = thm "rel_pow_E2";
paulson@15410
   153
val rtrancl_imp_UN_rel_pow = thm "rtrancl_imp_UN_rel_pow";
paulson@15410
   154
val rel_pow_imp_rtrancl = thm "rel_pow_imp_rtrancl";
paulson@15410
   155
val rtrancl_is_UN_rel_pow = thm "rtrancl_is_UN_rel_pow";
paulson@15410
   156
val single_valued_rel_pow = thm "single_valued_rel_pow";
paulson@15410
   157
*}
paulson@15410
   158
nipkow@10213
   159
end