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