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