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