equal
deleted
inserted
replaced
35 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need |
35 For example, @{term "range(f^n) = A"} and @{term "Range(R^n) = B"} need |
36 constraints.*} |
36 constraints.*} |
37 |
37 |
38 lemma funpow_add: "f ^ (m+n) = f^m o f^n" |
38 lemma funpow_add: "f ^ (m+n) = f^m o f^n" |
39 by(induct m) simp_all |
39 by(induct m) simp_all |
|
40 |
|
41 lemma funpow_swap1: "f((f^n) x) = (f^n)(f x)" |
|
42 proof - |
|
43 have "f((f^n) x) = (f^(n+1)) x" by simp |
|
44 also have "\<dots> = (f^n o f^1) x" by (simp only:funpow_add) |
|
45 also have "\<dots> = (f^n)(f x)" by simp |
|
46 finally show ?thesis . |
|
47 qed |
40 |
48 |
41 lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R" |
49 lemma rel_pow_1: "!!R:: ('a*'a)set. R^1 = R" |
42 by simp |
50 by simp |
43 declare rel_pow_1 [simp] |
51 declare rel_pow_1 [simp] |
44 |
52 |