src/HOL/Relation_Power.thy
author haftmann
Fri Apr 17 15:57:26 2009 +0200 (2009-04-17)
changeset 30949 37f887b55e7f
parent 30079 293b896b9c25
permissions -rw-r--r--
separated funpow, relpow from power on monoids
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
haftmann@30949
    12
consts funpower :: "('a \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'b" (infixr "^^" 80)
nipkow@10213
    13
haftmann@25861
    14
overloading
haftmann@30949
    15
  relpow \<equiv> "funpower \<Colon> ('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a \<times> 'a) set"
haftmann@25861
    16
begin
haftmann@25861
    17
haftmann@30949
    18
text {* @{text "R ^^ n = R O ... O R"}, the n-fold composition of @{text R} *}
nipkow@10213
    19
haftmann@25861
    20
primrec relpow where
haftmann@30949
    21
    "(R \<Colon> ('a \<times> 'a) set) ^^ 0 = Id"
haftmann@30949
    22
  | "(R \<Colon> ('a \<times> 'a) set) ^^ Suc n = R O (R ^^ n)"
haftmann@25861
    23
haftmann@25861
    24
end
nipkow@11305
    25
haftmann@25861
    26
overloading
haftmann@30949
    27
  funpow \<equiv> "funpower \<Colon> ('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a"
haftmann@25861
    28
begin
haftmann@25861
    29
haftmann@30949
    30
text {* @{text "f ^^ n = f o ... o f"}, the n-fold composition of @{text f} *}
haftmann@25861
    31
haftmann@25861
    32
primrec funpow where
haftmann@30949
    33
    "(f \<Colon> 'a \<Rightarrow> 'a) ^^ 0 = id"
haftmann@30949
    34
  | "(f \<Colon> 'a \<Rightarrow> 'a) ^^ Suc n = f o (f ^^ n)"
haftmann@25861
    35
haftmann@25861
    36
end
nipkow@11305
    37
haftmann@30949
    38
primrec fun_pow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where
haftmann@30949
    39
    "fun_pow 0 f = id"
haftmann@25861
    40
  | "fun_pow (Suc n) f = f o fun_pow n f"
haftmann@21414
    41
haftmann@30949
    42
lemma funpow_fun_pow [code unfold]:
haftmann@30949
    43
  "f ^^ n = fun_pow n f"
haftmann@25861
    44
  unfolding funpow_def fun_pow_def ..
haftmann@21414
    45
haftmann@30949
    46
lemma funpow_add:
haftmann@30949
    47
  "f ^^ (m + n) = f ^^ m o f ^^ n"
wenzelm@18398
    48
  by (induct m) simp_all
nipkow@15112
    49
haftmann@30949
    50
lemma funpow_swap1:
haftmann@30949
    51
  "f ((f ^^ n) x) = (f ^^ n) (f x)"
nipkow@18049
    52
proof -
haftmann@30949
    53
  have "f ((f ^^ n) x) = (f ^^ (n+1)) x" unfolding One_nat_def by simp
haftmann@30949
    54
  also have "\<dots>  = (f ^^ n o f ^^ 1) x" by (simp only: funpow_add)
haftmann@30949
    55
  also have "\<dots> = (f ^^ n) (f x)" unfolding One_nat_def by simp
nipkow@18049
    56
  finally show ?thesis .
nipkow@18049
    57
qed
nipkow@18049
    58
wenzelm@18398
    59
lemma rel_pow_1 [simp]:
haftmann@30949
    60
  fixes R :: "('a * 'a) set"
haftmann@30949
    61
  shows "R ^^ 1 = R"
wenzelm@18398
    62
  by simp
paulson@15410
    63
haftmann@30949
    64
lemma rel_pow_0_I: 
haftmann@30949
    65
  "(x, x) \<in> R ^^ 0"
haftmann@30949
    66
  by simp
haftmann@30949
    67
haftmann@30949
    68
lemma rel_pow_Suc_I:
haftmann@30949
    69
  "(x, y) \<in>  R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
wenzelm@18398
    70
  by auto
paulson@15410
    71
wenzelm@18398
    72
lemma rel_pow_Suc_I2:
haftmann@30949
    73
  "(x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ n \<Longrightarrow> (x, z) \<in> R ^^ Suc n"
haftmann@30949
    74
  by (induct n arbitrary: z) (simp, fastsimp)
paulson@15410
    75
haftmann@30949
    76
lemma rel_pow_0_E:
haftmann@30949
    77
  "(x, y) \<in> R ^^ 0 \<Longrightarrow> (x = y \<Longrightarrow> P) \<Longrightarrow> P"
wenzelm@18398
    78
  by simp
paulson@15410
    79
wenzelm@18398
    80
lemma rel_pow_Suc_E:
haftmann@30949
    81
  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<And>y. (x, y) \<in> R ^^ n \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P) \<Longrightarrow> P"
wenzelm@18398
    82
  by auto
paulson@15410
    83
wenzelm@18398
    84
lemma rel_pow_E:
haftmann@30949
    85
  "(x, z) \<in>  R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
haftmann@30949
    86
   \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in>  R ^^ m \<Longrightarrow> (y, z) \<in> R \<Longrightarrow> P)
haftmann@30949
    87
   \<Longrightarrow> P"
wenzelm@18398
    88
  by (cases n) auto
paulson@15410
    89
wenzelm@18398
    90
lemma rel_pow_Suc_D2:
haftmann@30949
    91
  "(x, z) \<in> R ^^ Suc n \<Longrightarrow> (\<exists>y. (x, y) \<in> R \<and> (y, z) \<in> R ^^ n)"
wenzelm@20503
    92
  apply (induct n arbitrary: x z)
wenzelm@18398
    93
   apply (blast intro: rel_pow_0_I elim: rel_pow_0_E rel_pow_Suc_E)
wenzelm@18398
    94
  apply (blast intro: rel_pow_Suc_I elim: rel_pow_0_E rel_pow_Suc_E)
wenzelm@18398
    95
  done
paulson@15410
    96
paulson@15410
    97
lemma rel_pow_Suc_D2':
haftmann@30949
    98
  "\<forall>x y z. (x, y) \<in> R ^^ n \<and> (y, z) \<in> R \<longrightarrow> (\<exists>w. (x, w) \<in> R \<and> (w, z) \<in> R ^^ n)"
wenzelm@18398
    99
  by (induct n) (simp_all, blast)
paulson@15410
   100
wenzelm@18398
   101
lemma rel_pow_E2:
haftmann@30949
   102
  "(x, z) \<in> R ^^ n \<Longrightarrow>  (n = 0 \<Longrightarrow> x = z \<Longrightarrow> P)
haftmann@30949
   103
     \<Longrightarrow> (\<And>y m. n = Suc m \<Longrightarrow> (x, y) \<in> R \<Longrightarrow> (y, z) \<in> R ^^ m \<Longrightarrow> P)
haftmann@30949
   104
   \<Longrightarrow> P"
haftmann@30949
   105
  apply (cases n, simp)
wenzelm@18398
   106
  apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
wenzelm@18398
   107
  done
paulson@15410
   108
haftmann@30949
   109
lemma rtrancl_imp_UN_rel_pow:
haftmann@30949
   110
  "p \<in> R^* \<Longrightarrow> p \<in> (\<Union>n. R ^^ n)"
haftmann@30949
   111
  apply (cases p) apply (simp only:)
wenzelm@18398
   112
  apply (erule rtrancl_induct)
wenzelm@18398
   113
   apply (blast intro: rel_pow_0_I rel_pow_Suc_I)+
wenzelm@18398
   114
  done
paulson@15410
   115
haftmann@30949
   116
lemma rel_pow_imp_rtrancl:
haftmann@30949
   117
  "p \<in> R ^^ n \<Longrightarrow> p \<in> R^*"
haftmann@30949
   118
  apply (induct n arbitrary: p)
haftmann@30949
   119
  apply (simp_all only: split_tupled_all)
wenzelm@18398
   120
   apply (blast intro: rtrancl_refl elim: rel_pow_0_E)
wenzelm@18398
   121
  apply (blast elim: rel_pow_Suc_E intro: rtrancl_into_rtrancl)
wenzelm@18398
   122
  done
paulson@15410
   123
haftmann@30949
   124
lemma rtrancl_is_UN_rel_pow:
haftmann@30949
   125
  "R^* = (UN n. R ^^ n)"
wenzelm@18398
   126
  by (blast intro: rtrancl_imp_UN_rel_pow rel_pow_imp_rtrancl)
paulson@15410
   127
kleing@25295
   128
lemma trancl_power:
haftmann@30949
   129
  "x \<in> r^+ = (\<exists>n > 0. x \<in> r ^^ n)"
kleing@25295
   130
  apply (cases x)
kleing@25295
   131
  apply simp
kleing@25295
   132
  apply (rule iffI)
kleing@25295
   133
   apply (drule tranclD2)
kleing@25295
   134
   apply (clarsimp simp: rtrancl_is_UN_rel_pow)
kleing@25295
   135
   apply (rule_tac x="Suc x" in exI)
kleing@25295
   136
   apply (clarsimp simp: rel_comp_def)
kleing@25295
   137
   apply fastsimp
kleing@25295
   138
  apply clarsimp
kleing@25295
   139
  apply (case_tac n, simp)
kleing@25295
   140
  apply clarsimp
kleing@25295
   141
  apply (drule rel_pow_imp_rtrancl)
kleing@25295
   142
  apply fastsimp
kleing@25295
   143
  done
paulson@15410
   144
wenzelm@18398
   145
lemma single_valued_rel_pow:
haftmann@30949
   146
  fixes R :: "('a * 'a) set"
haftmann@30949
   147
  shows "single_valued R \<Longrightarrow> single_valued (R ^^ n)"
haftmann@30949
   148
  apply (induct n arbitrary: R)
haftmann@30949
   149
  apply simp_all
wenzelm@18398
   150
  apply (rule single_valuedI)
wenzelm@18398
   151
  apply (fast dest: single_valuedD elim: rel_pow_Suc_E)
wenzelm@18398
   152
  done
paulson@15410
   153
nipkow@10213
   154
end