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