--- a/src/HOL/Library/Formal_Power_Series.thy Fri Dec 06 09:42:13 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Dec 06 17:33:45 2013 +0100
@@ -53,7 +53,7 @@
lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)"
unfolding fps_one_def by simp
-instantiation fps :: (plus) plus
+instantiation fps :: (plus) plus
begin
definition fps_plus_def:
@@ -89,7 +89,7 @@
lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)"
unfolding fps_uminus_def by simp
-instantiation fps :: ("{comm_monoid_add, times}") times
+instantiation fps :: ("{comm_monoid_add, times}") times
begin
definition fps_times_def:
@@ -312,28 +312,28 @@
lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)"
by (simp add: fps_ext)
-lemma fps_const_add [simp]: "fps_const (c::'a\<Colon>monoid_add) + fps_const d = fps_const (c + d)"
+lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + fps_const d = fps_const (c + d)"
by (simp add: fps_ext)
-lemma fps_const_sub [simp]: "fps_const (c::'a\<Colon>group_add) - fps_const d = fps_const (c - d)"
+lemma fps_const_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
by (simp add: fps_ext)
-lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
+lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)"
by (simp add: fps_eq_iff fps_mult_nth setsum_0')
-lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f =
+lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f =
Abs_fps (\<lambda>n. if n = 0 then c + f$0 else f$n)"
by (simp add: fps_ext)
-lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) =
+lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) =
Abs_fps (\<lambda>n. if n = 0 then f$0 + c else f$n)"
by (simp add: fps_ext)
-lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
+lemma fps_const_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\<lambda>n. c * f$n)"
unfolding fps_eq_iff fps_mult_nth
by (simp add: fps_const_def mult_delta_left setsum_delta)
-lemma fps_const_mult_right: "f * fps_const (c::'a\<Colon>semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
+lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\<lambda>n. f$n * c)"
unfolding fps_eq_iff fps_mult_nth
by (simp add: fps_const_def mult_delta_right setsum_delta')
@@ -357,8 +357,8 @@
proof
fix a b :: "'a fps"
assume a0: "a \<noteq> 0" and b0: "b \<noteq> 0"
- then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0"
- and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0" unfolding fps_nonzero_nth_minimal
+ then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0" and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0"
+ unfolding fps_nonzero_nth_minimal
by blast+
have "(a * b) $ (i+j) = (\<Sum>k=0..i+j. a$k * b$(i+j-k))"
by (rule fps_mult_nth)
@@ -389,13 +389,13 @@
subsection{* The eXtractor series X*}
-lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
+lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)"
by (induct n) auto
definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
lemma X_mult_nth [simp]:
- "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
+ "(X * (f :: 'a::semiring_1 fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
proof (cases "n = 0")
case False
have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
@@ -409,10 +409,10 @@
qed
lemma X_mult_right_nth[simp]:
- "((f :: ('a::comm_semiring_1) fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
+ "((f :: 'a::comm_semiring_1 fps) * X) $n = (if n = 0 then 0 else f $ (n - 1))"
by (metis X_mult_nth mult_commute)
-lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
+lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then 1::'a::comm_ring_1 else 0)"
proof (induct k)
case 0
then show ?case by (simp add: X_def fps_eq_iff)
@@ -420,16 +420,16 @@
case (Suc k)
{
fix m
- have "(X^Suc k) $ m = (if m = 0 then (0::'a) else (X^k) $ (m - 1))"
+ have "(X^Suc k) $ m = (if m = 0 then 0::'a else (X^k) $ (m - 1))"
by (simp del: One_nat_def)
- then have "(X^Suc k) $ m = (if m = Suc k then (1::'a) else 0)"
+ then have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)"
using Suc.hyps by (auto cong del: if_weak_cong)
}
then show ?case by (simp add: fps_eq_iff)
qed
lemma X_power_mult_nth:
- "(X^k * (f :: ('a::comm_ring_1) fps)) $n = (if n < k then 0 else f $ (n - k))"
+ "(X^k * (f :: 'a::comm_ring_1 fps)) $n = (if n < k then 0 else f $ (n - k))"
apply (induct k arbitrary: n)
apply simp
unfolding power_Suc mult_assoc
@@ -438,7 +438,7 @@
done
lemma X_power_mult_right_nth:
- "((f :: ('a::comm_ring_1) fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
+ "((f :: 'a::comm_ring_1 fps) * X^k) $n = (if n < k then 0 else f $ (n - k))"
by (metis X_power_mult_nth mult_commute)
@@ -450,15 +450,15 @@
begin
definition
- dist_fps_def: "dist (a::'a fps) b =
+ dist_fps_def: "dist (a :: 'a fps) b =
(if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
-lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
+lemma dist_fps_ge0: "dist (a :: 'a fps) b \<ge> 0"
by (simp add: dist_fps_def)
-lemma dist_fps_sym: "dist (a::'a fps) b = dist b a"
+lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a"
apply (auto simp add: dist_fps_def)
- apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a $ n \<noteq> b $ n)"])
+ apply (rule cong[OF refl, where x="(\<lambda>n. a $ n \<noteq> b $ n)"])
apply (rule ext)
apply auto
done
@@ -550,18 +550,26 @@
text{* The infinite sums and justification of the notation in textbooks*}
lemma reals_power_lt_ex:
- assumes xp: "x > 0" and y1: "(y::real) > 1"
+ fixes x y :: real
+ assumes xp: "x > 0"
+ and y1: "y > 1"
shows "\<exists>k>0. (1/y)^k < x"
proof -
- have yp: "y > 0" using y1 by simp
+ have yp: "y > 0"
+ using y1 by simp
from reals_Archimedean2[of "max 0 (- log y x) + 1"]
- obtain k::nat where k: "real k > max 0 (- log y x) + 1" by blast
- from k have kp: "k > 0" by simp
- from k have "real k > - log y x" by simp
- then have "ln y * real k > - ln x" unfolding log_def
+ obtain k :: nat where k: "real k > max 0 (- log y x) + 1"
+ by blast
+ from k have kp: "k > 0"
+ by simp
+ from k have "real k > - log y x"
+ by simp
+ then have "ln y * real k > - ln x"
+ unfolding log_def
using ln_gt_zero_iff[OF yp] y1
- by (simp add: minus_divide_left field_simps del:minus_divide_left[symmetric])
- then have "ln y * real k + ln x > 0" by simp
+ by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric])
+ then have "ln y * real k + ln x > 0"
+ by simp
then have "exp (real k * ln y + ln x) > exp 0"
by (simp add: mult_ac)
then have "y ^ k * x > 1"
@@ -569,17 +577,18 @@
by simp
then have "x > (1 / y)^k" using yp
by (simp add: field_simps nonzero_power_divide)
- then show ?thesis using kp by blast
+ then show ?thesis
+ using kp by blast
qed
-lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)" by (simp add: X_def)
-
-lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else (0::'a::comm_ring_1))"
+lemma X_nth[simp]: "X$n = (if n = 1 then 1 else 0)"
+ by (simp add: X_def)
+
+lemma X_power_nth[simp]: "(X^k) $n = (if n = k then 1 else 0::'a::comm_ring_1)"
by (simp add: X_power_iff)
-
lemma fps_sum_rep_nth: "(setsum (\<lambda>i. fps_const(a$i)*X^i) {0..m})$n =
- (if n \<le> m then a$n else (0::'a::comm_ring_1))"
+ (if n \<le> m then a$n else 0::'a::comm_ring_1)"
apply (auto simp add: fps_setsum_nth cond_value_iff cong del: if_weak_cong)
apply (simp add: setsum_delta')
done
@@ -588,13 +597,13 @@
(is "?s ----> a")
proof -
{
- fix r:: real
+ fix r :: real
assume rp: "r > 0"
have th0: "(2::real) > 1" by simp
from reals_power_lt_ex[OF rp th0]
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast
{
- fix n::nat
+ fix n :: nat
assume nn0: "n \<ge> n0"
then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
by (auto intro: power_decreasing)
@@ -612,21 +621,27 @@
by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
from neq have kn: "k > n"
- by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
- then have "dist (?s n) a < (1/2)^n" unfolding dth
- by (auto intro: power_strict_decreasing)
- also have "\<dots> \<le> (1/2)^n0" using nn0
- by (auto intro: power_decreasing)
- also have "\<dots> < r" using n0 by simp
+ by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff
+ split: split_if_asm intro: LeastI2_ex)
+ then have "dist (?s n) a < (1/2)^n"
+ unfolding dth by (auto intro: power_strict_decreasing)
+ also have "\<dots> \<le> (1/2)^n0"
+ using nn0 by (auto intro: power_decreasing)
+ also have "\<dots> < r"
+ using n0 by simp
finally have "dist (?s n) a < r" .
}
- ultimately have "dist (?s n) a < r" by blast
+ ultimately have "dist (?s n) a < r"
+ by blast
}
- then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r " by blast
+ then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r"
+ by blast
}
- then show ?thesis unfolding LIMSEQ_def by blast
+ then show ?thesis
+ unfolding LIMSEQ_def by blast
qed
+
subsection{* Inverses of formal power series *}
declare setsum_cong[fundef_cong]
@@ -650,7 +665,7 @@
end
lemma fps_inverse_zero [simp]:
- "inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0"
+ "inverse (0 :: 'a::{comm_monoid_add,inverse,times,uminus} fps) = 0"
by (simp add: fps_ext fps_inverse_def)
lemma fps_inverse_one [simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1"
@@ -663,7 +678,8 @@
assumes f0: "f$0 \<noteq> (0::'a::field)"
shows "inverse f * f = 1"
proof -
- have c: "inverse f * f = f * inverse f" by (simp add: mult_commute)
+ have c: "inverse f * f = f * inverse f"
+ by (simp add: mult_commute)
from f0 have ifn: "\<And>n. inverse f $ n = natfun_inverse f n"
by (simp add: fps_inverse_def)
from f0 have th0: "(inverse f * f) $ 0 = 1"
@@ -671,8 +687,10 @@
{
fix n :: nat
assume np: "n > 0"
- from np have eq: "{0..n} = {0} \<union> {1 .. n}" by auto
- have d: "{0} \<inter> {1 .. n} = {}" by auto
+ from np have eq: "{0..n} = {0} \<union> {1 .. n}"
+ by auto
+ have d: "{0} \<inter> {1 .. n} = {}"
+ by auto
from f0 np have th0: "- (inverse f $ n) =
(setsum (\<lambda>i. f$i * natfun_inverse f (n - i)) {1..n}) / (f$0)"
by (cases n) (simp_all add: divide_inverse fps_inverse_def)
@@ -683,10 +701,13 @@
unfolding fps_mult_nth ifn ..
also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))"
by (simp add: eq)
- also have "\<dots> = 0" unfolding th1 ifn by simp
- finally have "(inverse f * f)$n = 0" unfolding c .
+ also have "\<dots> = 0"
+ unfolding th1 ifn by simp
+ finally have "(inverse f * f)$n = 0"
+ unfolding c .
}
- with th0 show ?thesis by (simp add: fps_eq_iff)
+ with th0 show ?thesis
+ by (simp add: fps_eq_iff)
qed
lemma fps_inverse_0_iff[simp]: "(inverse f)$0 = (0::'a::division_ring) \<longleftrightarrow> f$0 = 0"
@@ -695,13 +716,16 @@
lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f $0 = 0"
proof -
{
- assume "f$0 = 0"
- then have "inverse f = 0" by (simp add: fps_inverse_def)
+ assume "f $ 0 = 0"
+ then have "inverse f = 0"
+ by (simp add: fps_inverse_def)
}
moreover
{
- assume h: "inverse f = 0" and c: "f $0 \<noteq> 0"
- from inverse_mult_eq_1[OF c] h have False by simp
+ assume h: "inverse f = 0"
+ assume c: "f $0 \<noteq> 0"
+ from inverse_mult_eq_1[OF c] h have False
+ by simp
}
ultimately show ?thesis by blast
qed
@@ -714,7 +738,8 @@
from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0]
have "inverse f * f = inverse f * inverse (inverse f)"
by (simp add: mult_ac)
- then show ?thesis using f0 unfolding mult_cancel_left by simp
+ then show ?thesis
+ using f0 unfolding mult_cancel_left by simp
qed
lemma fps_inverse_unique:
@@ -723,8 +748,11 @@
shows "inverse f = g"
proof -
from inverse_mult_eq_1[OF f0] fg
- have th0: "inverse f * f = g * f" by (simp add: mult_ac)
- then show ?thesis using f0 unfolding mult_cancel_right
+ have th0: "inverse f * f = g * f"
+ by (simp add: mult_ac)
+ then show ?thesis
+ using f0
+ unfolding mult_cancel_right
by (auto simp add: expand_fps_eq)
qed
@@ -733,19 +761,26 @@
apply (rule fps_inverse_unique)
apply simp
apply (simp add: fps_eq_iff fps_mult_nth)
-proof clarsimp
+ apply clarsimp
+proof -
fix n :: nat
assume n: "n > 0"
- let ?f = "\<lambda>i. if n = i then (1\<Colon>'a) else if n - i = 1 then - 1 else 0"
+ let ?f = "\<lambda>i. if n = i then (1::'a) else if n - i = 1 then - 1 else 0"
let ?g = "\<lambda>i. if i = n then 1 else if i=n - 1 then - 1 else 0"
let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
have th1: "setsum ?f {0..n} = setsum ?g {0..n}"
by (rule setsum_cong2) auto
have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}"
- using n apply - by (rule setsum_cong2) auto
- have eq: "{0 .. n} = {0.. n - 1} \<union> {n}" by auto
- from n have d: "{0.. n - 1} \<inter> {n} = {}" by auto
- have f: "finite {0.. n - 1}" "finite {n}" by auto
+ apply (insert n)
+ apply (rule setsum_cong2)
+ apply auto
+ done
+ have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
+ by auto
+ from n have d: "{0.. n - 1} \<inter> {n} = {}"
+ by auto
+ have f: "finite {0.. n - 1}" "finite {n}"
+ by auto
show "setsum ?f {0..n} = 0"
unfolding th1
apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
@@ -754,11 +789,12 @@
done
qed
-subsection{* Formal Derivatives, and the MacLaurin theorem around 0*}
+
+subsection {* Formal Derivatives, and the MacLaurin theorem around 0 *}
definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f $ (n + 1))"
-lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n+1)"
+lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)"
by (simp add: fps_deriv_def)
lemma fps_deriv_linear[simp]:
@@ -767,16 +803,19 @@
unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps)
lemma fps_deriv_mult[simp]:
- fixes f :: "('a :: comm_ring_1) fps"
+ fixes f :: "'a::comm_ring_1 fps"
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g"
proof -
let ?D = "fps_deriv"
- { fix n::nat
+ {
+ fix n :: nat
let ?Zn = "{0 ..n}"
let ?Zn1 = "{0 .. n + 1}"
let ?f = "\<lambda>i. i + 1"
- have fi: "inj_on ?f {0..n}" by (simp add: inj_on_def)
- have eq: "{1.. n+1} = ?f ` {0..n}" by auto
+ have fi: "inj_on ?f {0..n}"
+ by (simp add: inj_on_def)
+ have eq: "{1.. n+1} = ?f ` {0..n}"
+ by auto
let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n - i) +
of_nat (i+1)* f $ (i+1) * g $ (n - i)"
let ?h = "\<lambda>i. of_nat i * g $ i * f $ ((n+1) - i) +
@@ -784,7 +823,8 @@
{
fix k
assume k: "k \<in> {0..n}"
- have "?h (k + 1) = ?g k" using k by auto
+ have "?h (k + 1) = ?g k"
+ using k by auto
}
note th0 = this
have eq': "{0..n +1}- {1 .. n+1} = {0}" by auto
@@ -834,20 +874,23 @@
lemma fps_deriv_X[simp]: "fps_deriv X = 1"
by (simp add: fps_deriv_def X_def fps_eq_iff)
-lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: ('a:: comm_ring_1) fps)) = - (fps_deriv f)"
+lemma fps_deriv_neg[simp]:
+ "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)"
by (simp add: fps_eq_iff fps_deriv_def)
-lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g"
+lemma fps_deriv_add[simp]:
+ "fps_deriv ((f:: 'a::comm_ring_1 fps) + g) = fps_deriv f + fps_deriv g"
using fps_deriv_linear[of 1 f 1 g] by simp
-lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g"
+lemma fps_deriv_sub[simp]:
+ "fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g"
using fps_deriv_add [of f "- g"] by simp
lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
by (simp add: fps_ext fps_deriv_def fps_const_def)
lemma fps_deriv_mult_const_left[simp]:
- "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
+ "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
by simp
lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
@@ -857,11 +900,11 @@
by (simp add: fps_deriv_def fps_eq_iff )
lemma fps_deriv_mult_const_right[simp]:
- "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
+ "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
by simp
lemma fps_deriv_setsum:
- "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
+ "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: 'a::comm_ring_1 fps)) S"
proof (cases "finite S")
case False
then show ?thesis by simp
@@ -871,7 +914,7 @@
qed
lemma fps_deriv_eq_0_iff [simp]:
- "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f$0 :: 'a::{idom,semiring_char_0}))"
+ "fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})"
proof -
{
assume "f = fps_const (f$0)"
@@ -893,22 +936,22 @@
qed
lemma fps_deriv_eq_iff:
- fixes f:: "('a::{idom,semiring_char_0}) fps"
+ fixes f :: "'a::{idom,semiring_char_0} fps"
shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)"
proof -
have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0"
by simp
- also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)"
+ also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f - g) $ 0)"
unfolding fps_deriv_eq_0_iff ..
finally show ?thesis by (simp add: field_simps)
qed
lemma fps_deriv_eq_iff_ex:
- "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
+ "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)"
by (auto simp: fps_deriv_eq_iff)
-fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
+fun fps_nth_deriv :: "nat \<Rightarrow> 'a::semiring_1 fps \<Rightarrow> 'a fps"
where
"fps_nth_deriv 0 f = f"
| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"
@@ -922,15 +965,15 @@
by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
lemma fps_nth_deriv_neg[simp]:
- "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
+ "fps_nth_deriv n (- (f :: 'a::comm_ring_1 fps)) = - (fps_nth_deriv n f)"
by (induct n arbitrary: f) simp_all
lemma fps_nth_deriv_add[simp]:
- "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
+ "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
using fps_nth_deriv_linear[of n 1 f 1 g] by simp
lemma fps_nth_deriv_sub[simp]:
- "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
+ "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
using fps_nth_deriv_add [of n f "- g"] by simp
lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
@@ -952,7 +995,7 @@
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute)
lemma fps_nth_deriv_setsum:
- "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
+ "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: 'a::comm_ring_1 fps)) S"
proof (cases "finite S")
case True
show ?thesis by (induct rule: finite_induct [OF True]) simp_all
@@ -962,15 +1005,16 @@
qed
lemma fps_deriv_maclauren_0:
- "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) $ 0 = of_nat (fact k) * f$(k)"
+ "(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) $ 0 = of_nat (fact k) * f $ k"
by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)
-subsection {* Powers*}
+
+subsection {* Powers *}
lemma fps_power_zeroth_eq_one: "a$0 =1 \<Longrightarrow> a^n $ 0 = (1::'a::semiring_1)"
by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)
-lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)$0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
+lemma fps_power_first_eq: "(a :: 'a::comm_ring_1 fps) $ 0 =1 \<Longrightarrow> a^n $ 1 = of_nat n * a$1"
proof (induct n)
case 0
then show ?case by simp
@@ -988,10 +1032,10 @@
lemma startsby_zero_power:"a $0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n $0 = 0"
by (induct n) (auto simp add: fps_mult_nth)
-lemma startsby_power:"a $0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n $0 = v^n"
+lemma startsby_power:"a $0 = (v::'a::comm_ring_1) \<Longrightarrow> a^n $0 = v^n"
by (induct n) (auto simp add: fps_mult_nth)
-lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a$0 = 0)"
+lemma startsby_zero_power_iff[simp]: "a^n $0 = (0::'a::idom) \<longleftrightarrow> n \<noteq> 0 \<and> a$0 = 0"
apply (rule iffI)
apply (induct n)
apply (auto simp add: fps_mult_nth)
@@ -1002,11 +1046,14 @@
assumes a0: "a $0 = (0::'a::idom)"
shows "\<forall>n < k. a ^ k $ n = 0"
using a0
-proof(induct k rule: nat_less_induct)
+proof (induct k rule: nat_less_induct)
fix k
- assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $0 = (0\<Colon>'a)"
+ assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0"
let ?ths = "\<forall>m<k. a ^ k $ m = 0"
- { assume "k = 0" then have ?ths by simp }
+ {
+ assume "k = 0"
+ then have ?ths by simp
+ }
moreover
{
fix l
@@ -1022,8 +1069,10 @@
moreover
{
assume m0: "m \<noteq> 0"
- have "a ^k $ m = (a^l * a) $m" by (simp add: k mult_commute)
- also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))" by (simp add: fps_mult_nth)
+ have "a ^k $ m = (a^l * a) $m"
+ by (simp add: k mult_commute)
+ also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))"
+ by (simp add: fps_mult_nth)
also have "\<dots> = 0"
apply (rule setsum_0')
apply auto
@@ -1034,31 +1083,36 @@
done
finally have "a^k $ m = 0" .
}
- ultimately have "a^k $ m = 0" by blast
+ ultimately have "a^k $ m = 0"
+ by blast
}
then have ?ths by blast
}
- ultimately show ?ths by (cases k) auto
+ ultimately show ?ths
+ by (cases k) auto
qed
lemma startsby_zero_setsum_depends:
- assumes a0: "a $0 = (0::'a::idom)" and kn: "n \<ge> k"
+ assumes a0: "a $0 = (0::'a::idom)"
+ and kn: "n \<ge> k"
shows "setsum (\<lambda>i. (a ^ i)$k) {0 .. n} = setsum (\<lambda>i. (a ^ i)$k) {0 .. k}"
apply (rule setsum_mono_zero_right)
- using kn apply auto
+ using kn
+ apply auto
apply (rule startsby_zero_power_prefix[rule_format, OF a0])
apply arith
done
lemma startsby_zero_power_nth_same:
- assumes a0: "a$0 = (0::'a::{idom})"
+ assumes a0: "a$0 = (0::'a::idom)"
shows "a^n $ n = (a$1) ^ n"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
- have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)" by (simp add: field_simps)
+ have "a ^ Suc n $ (Suc n) = (a^n * a)$(Suc n)"
+ by (simp add: field_simps)
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {0.. Suc n}"
by (simp add: fps_mult_nth)
also have "\<dots> = setsum (\<lambda>i. a^n$i * a $ (Suc n - i)) {n .. Suc n}"
@@ -1069,18 +1123,24 @@
apply (rule startsby_zero_power_prefix[rule_format, OF a0])
apply arith
done
- also have "\<dots> = a^n $ n * a$1" using a0 by simp
- finally show ?case using Suc.hyps by simp
+ also have "\<dots> = a^n $ n * a$1"
+ using a0 by simp
+ finally show ?case
+ using Suc.hyps by simp
qed
lemma fps_inverse_power:
- fixes a :: "('a::{field}) fps"
+ fixes a :: "'a::field fps"
shows "inverse (a^n) = inverse a ^ n"
proof -
{
assume a0: "a$0 = 0"
- then have eq: "inverse a = 0" by (simp add: fps_inverse_def)
- { assume "n = 0" then have ?thesis by simp }
+ then have eq: "inverse a = 0"
+ by (simp add: fps_inverse_def)
+ {
+ assume "n = 0"
+ then have ?thesis by simp
+ }
moreover
{
assume n: "n > 0"
@@ -1106,7 +1166,7 @@
qed
lemma fps_deriv_power:
- "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
+ "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)"
apply (induct n)
apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add)
apply (case_tac n)
@@ -1114,10 +1174,10 @@
done
lemma fps_inverse_deriv:
- fixes a:: "('a :: field) fps"
+ fixes a :: "'a::field fps"
assumes a0: "a$0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2"
-proof-
+proof -
from inverse_mult_eq_1[OF a0]
have "fps_deriv (inverse a * a) = 0" by simp
then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0"
@@ -1138,7 +1198,7 @@
qed
lemma fps_inverse_mult:
- fixes a::"('a :: field) fps"
+ fixes a :: "'a::field fps"
shows "inverse (a * b) = inverse a * inverse b"
proof -
{
@@ -1168,7 +1228,7 @@
qed
lemma fps_inverse_deriv':
- fixes a:: "('a :: field) fps"
+ fixes a :: "'a::field fps"
assumes a0: "a$0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2"
using fps_inverse_deriv[OF a0]
@@ -1181,7 +1241,7 @@
by (metis mult_commute inverse_mult_eq_1 f0)
lemma fps_divide_deriv:
- fixes a:: "('a :: field) fps"
+ fixes a :: "'a::field fps"
assumes a0: "b$0 \<noteq> 0"
shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b\<^sup>2"
using fps_inverse_deriv[OF a0]
@@ -1189,7 +1249,7 @@
power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
-lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field))) = 1 - X"
+lemma fps_inverse_gp': "inverse (Abs_fps (\<lambda>n. 1::'a::field)) = 1 - X"
by (simp add: fps_inverse_gp fps_eq_iff X_def)
lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)"
@@ -1197,12 +1257,13 @@
lemma fps_inverse_X_plus1:
- "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::{field})) ^ n)" (is "_ = ?r")
-proof-
+ "inverse (1 + X) = Abs_fps (\<lambda>n. (- (1::'a::field)) ^ n)" (is "_ = ?r")
+proof -
have eq: "(1 + X) * ?r = 1"
unfolding minus_one_power_iff
by (auto simp add: field_simps fps_eq_iff)
- show ?thesis by (auto simp add: eq intro: fps_inverse_unique)
+ show ?thesis
+ by (auto simp add: eq intro: fps_inverse_unique)
qed
@@ -1220,8 +1281,10 @@
fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0"
(is "?l = ?r")
proof -
- have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral)
- moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def)
+ have "fps_deriv ?l = fps_deriv ?r"
+ by (simp add: fps_deriv_fps_integral)
+ moreover have "?l$0 = ?r$0"
+ by (simp add: fps_integral_def)
ultimately show ?thesis
unfolding fps_deriv_eq_iff by auto
qed
@@ -1229,26 +1292,26 @@
subsection {* Composition of FPSs *}
-definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
- fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
+definition fps_compose :: "'a::semiring_1 fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55)
+ where "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a$i * (b^i$n)) {0..n})"
lemma fps_compose_nth: "(a oo b)$n = setsum (\<lambda>i. a$i * (b^i$n)) {0..n}"
by (simp add: fps_compose_def)
-lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)"
+lemma fps_compose_X[simp]: "a oo X = (a :: 'a::comm_ring_1 fps)"
by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta')
lemma fps_const_compose[simp]:
- "fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)"
+ "fps_const (a::'a::comm_ring_1) oo b = fps_const a"
by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
-lemma numeral_compose[simp]: "(numeral k::('a::{comm_ring_1}) fps) oo b = numeral k"
+lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k"
unfolding numeral_fps_const by simp
-lemma neg_numeral_compose[simp]: "(- numeral k::('a::{comm_ring_1}) fps) oo b = - numeral k"
+lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k"
unfolding neg_numeral_fps_const by simp
-lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: ('a :: comm_ring_1) fps)"
+lemma X_fps_compose_startby0[simp]: "a$0 = 0 \<Longrightarrow> X oo a = (a :: 'a::comm_ring_1 fps)"
by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta not_le)
@@ -1259,10 +1322,10 @@
lemma fps_power_mult_eq_shift:
"X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) =
- Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}"
+ Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}"
(is "?lhs = ?rhs")
proof -
- { fix n:: nat
+ { fix n :: nat
have "?lhs $ n = (if n < Suc k then 0 else a n)"
unfolding X_power_mult_nth by auto
also have "\<dots> = ?rhs $ n"
@@ -1298,21 +1361,21 @@
(* If f reprents {a_n} and P is a polynomial, then
P(xD) f represents {P(n) a_n}*)
-definition "XD = op * X o fps_deriv"
-
-lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)"
+definition "XD = op * X \<circ> fps_deriv"
+
+lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: 'a::comm_ring_1 fps)"
by (simp add: XD_def field_simps)
lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a"
by (simp add: XD_def field_simps)
lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) =
- fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)"
+ fps_const c * XD a + fps_const d * XD (b :: 'a::comm_ring_1 fps)"
by simp
lemma XDN_linear:
"(XD ^^ n) (fps_const c * a + fps_const d * b) =
- fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
+ fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: 'a::comm_ring_1 fps)"
by (induct n) simp_all
lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)"
@@ -1320,39 +1383,38 @@
lemma fps_mult_XD_shift:
- "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
+ "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def)
-subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
-
-subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
+subsubsection {* Rule 3 is trivial and is given by @{text fps_times_def} *}
+
+subsubsection {* Rule 5 --- summation and "division" by (1 - X) *}
lemma fps_divide_X_minus1_setsum_lemma:
- "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
+ "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
proof -
- let ?X = "X::('a::comm_ring_1) fps"
let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
by simp
{
- fix n:: nat
+ fix n :: nat
{
- assume "n=0"
- then have "a$n = ((1 - ?X) * ?sa) $ n"
+ assume "n = 0"
+ then have "a $ n = ((1 - X) * ?sa) $ n"
by (simp add: fps_mult_nth)
}
moreover
{
assume n0: "n \<noteq> 0"
- then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1}\<union>{2..n} = {1..n}"
- "{0..n - 1}\<union>{n} = {0..n}"
+ then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1} \<union> {2..n} = {1..n}"
+ "{0..n - 1} \<union> {n} = {0..n}"
by (auto simp: set_eq_iff)
- have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}"
- "{0..n - 1}\<inter>{n} ={}" using n0 by simp_all
+ have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" "{0..n - 1} \<inter> {n} = {}"
+ using n0 by simp_all
have f: "finite {0}" "finite {1}" "finite {2 .. n}"
"finite {0 .. n - 1}" "finite {n}" by simp_all
- have "((1 - ?X) * ?sa) $ n = setsum (\<lambda>i. (1 - ?X)$ i * ?sa $ (n - i)) {0 .. n}"
+ have "((1 - X) * ?sa) $ n = setsum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}"
by (simp add: fps_mult_nth)
also have "\<dots> = a$n"
unfolding th0
@@ -1362,24 +1424,29 @@
unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)]
apply simp
done
- finally have "a$n = ((1 - ?X) * ?sa) $ n" by simp
+ finally have "a$n = ((1 - X) * ?sa) $ n"
+ by simp
}
- ultimately have "a$n = ((1 - ?X) * ?sa) $ n" by blast
+ ultimately have "a$n = ((1 - X) * ?sa) $ n"
+ by blast
}
- then show ?thesis unfolding fps_eq_iff by blast
+ then show ?thesis
+ unfolding fps_eq_iff by blast
qed
lemma fps_divide_X_minus1_setsum:
- "a /((1::('a::field) fps) - X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
+ "a /((1::'a::field fps) - X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
proof -
- let ?X = "1 - (X::('a::field) fps)"
- have th0: "?X $ 0 \<noteq> 0" by simp
- have "a /?X = ?X * Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) * inverse ?X"
+ let ?X = "1 - (X::'a fps)"
+ have th0: "?X $ 0 \<noteq> 0"
+ by simp
+ have "a /?X = ?X * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) * inverse ?X"
using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0
by (simp add: fps_divide_def mult_assoc)
- also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n\<Colon>nat. setsum (op $ a) {0..n}) "
+ also have "\<dots> = (inverse ?X * ?X) * Abs_fps (\<lambda>n::nat. setsum (op $ a) {0..n}) "
by (simp add: mult_ac)
- finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0])
+ finally show ?thesis
+ by (simp add: inverse_mult_eq_1[OF th0])
qed
@@ -1396,7 +1463,8 @@
lemma append_natpermute_less_eq:
assumes "xs @ ys \<in> natpermute n k"
- shows "listsum xs \<le> n" and "listsum ys \<le> n"
+ shows "listsum xs \<le> n"
+ and "listsum ys \<le> n"
proof -
from assms have "listsum (xs @ ys) = n"
by (simp add: natpermute_def)
@@ -1554,8 +1622,8 @@
text {* The general form *}
lemma fps_setprod_nth:
fixes m :: nat
- and a :: "nat \<Rightarrow> ('a::comm_ring_1) fps"
- shows "(setprod a {0 .. m})$n =
+ and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
+ shows "(setprod a {0 .. m}) $ n =
setsum (\<lambda>v. setprod (\<lambda>j. (a j) $ (v!j)) {0..m}) (natpermute n (m+1))"
(is "?P m n")
proof (induct m arbitrary: n rule: nat_less_induct)
@@ -1608,7 +1676,7 @@
text{* The special form for powers *}
lemma fps_power_nth_Suc:
fixes m :: nat
- and a :: "('a::comm_ring_1) fps"
+ and a :: "'a::comm_ring_1 fps"
shows "(a ^ Suc m)$n = setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
proof -
have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}"
@@ -1618,14 +1686,14 @@
lemma fps_power_nth:
fixes m :: nat
- and a :: "('a::comm_ring_1) fps"
+ and a :: "'a::comm_ring_1 fps"
shows "(a ^m)$n =
(if m=0 then 1$n else setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m - 1}) (natpermute n m))"
by (cases m) (simp_all add: fps_power_nth_Suc del: power_Suc)
lemma fps_nth_power_0:
fixes m :: nat
- and a :: "('a::{comm_ring_1}) fps"
+ and a :: "'a::comm_ring_1 fps"
shows "(a ^m)$0 = (a$0) ^ m"
proof (cases m)
case 0
@@ -1641,9 +1709,10 @@
qed
lemma fps_compose_inj_right:
- assumes a0: "a$0 = (0::'a::{idom})"
+ assumes a0: "a$0 = (0::'a::idom)"
and a1: "a$1 \<noteq> 0"
- shows "(b oo a = c oo a) \<longleftrightarrow> b = c" (is "?lhs \<longleftrightarrow>?rhs")
+ shows "(b oo a = c oo a) \<longleftrightarrow> b = c"
+ (is "?lhs \<longleftrightarrow>?rhs")
proof
assume ?rhs
then show "?lhs" by simp
@@ -1692,7 +1761,7 @@
declare setprod_cong [fundef_cong]
-function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a"
+function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a::field fps \<Rightarrow> nat \<Rightarrow> 'a"
where
"radical r 0 a 0 = 1"
| "radical r 0 a (Suc n) = 0"
@@ -1767,7 +1836,7 @@
apply (rule setprod_cong)
apply simp
using Suc
- apply (subgoal_tac "replicate k (0::nat) ! x = 0")
+ apply (subgoal_tac "replicate k 0 ! x = 0")
apply (auto intro: nth_replicate simp del: replicate.simps)
done
also have "\<dots> = a$0" using r Suc by (simp add: setprod_constant)
@@ -2040,7 +2109,7 @@
then have thn: "xs!i < n" by presburger
from h[rule_format, OF thn] show "a$(xs !i) = ?r$(xs!i)" .
qed
- have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
+ have th00: "\<And>x::'a. of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
by (simp add: field_simps del: of_nat_Suc)
from H have "b$n = a^Suc k $ n"
by (simp add: fps_eq_iff)
@@ -2076,7 +2145,7 @@
lemma radical_power:
assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
- and a0: "(a$0 ::'a::field_char_0) \<noteq> 0"
+ and a0: "(a$0 :: 'a::field_char_0) \<noteq> 0"
shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
proof -
let ?ak = "a^ Suc k"
@@ -2093,7 +2162,7 @@
qed
lemma fps_deriv_radical:
- fixes a:: "'a::field_char_0 fps"
+ fixes a :: "'a::field_char_0 fps"
assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
and a0: "a$0 \<noteq> 0"
shows "fps_deriv (fps_radical r (Suc k) a) =
@@ -2120,7 +2189,7 @@
qed
lemma radical_mult_distrib:
- fixes a:: "'a::field_char_0 fps"
+ fixes a :: "'a::field_char_0 fps"
assumes k: "k > 0"
and ra0: "r k (a $ 0) ^ k = a $ 0"
and rb0: "r k (b $ 0) ^ k = b $ 0"
@@ -2191,7 +2260,7 @@
qed
*)
-lemma fps_divide_1[simp]: "(a:: ('a::field) fps) / 1 = a"
+lemma fps_divide_1[simp]: "(a :: 'a::field fps) / 1 = a"
by (simp add: fps_divide_def)
lemma radical_divide:
@@ -2252,9 +2321,9 @@
subsection{* Derivative of composition *}
lemma fps_compose_deriv:
- fixes a:: "('a::idom) fps"
+ fixes a :: "'a::idom fps"
assumes b0: "b$0 = 0"
- shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * (fps_deriv b)"
+ shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * fps_deriv b"
proof -
{
fix n
@@ -2305,7 +2374,8 @@
"((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
proof (cases n)
case 0
- then show ?thesis by (simp add: fps_mult_nth )
+ then show ?thesis
+ by (simp add: fps_mult_nth )
next
case (Suc m)
have "((1+X)*a) $n = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0..n}"
@@ -2317,7 +2387,8 @@
finally show ?thesis .
qed
-subsection{* Finite FPS (i.e. polynomials) and X *}
+
+subsection {* Finite FPS (i.e. polynomials) and X *}
lemma fps_poly_sum_X:
assumes z: "\<forall>i > n. a$i = (0::'a::comm_ring_1)"
@@ -2335,7 +2406,7 @@
subsection{* Compositional inverses *}
-fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
where
"compinv a 0 = X$0"
| "compinv a (Suc n) =
@@ -2376,7 +2447,7 @@
qed
-fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::field"
where
"gcompinv b a 0 = b$0"
| "gcompinv b a (Suc n) =
@@ -2474,9 +2545,9 @@
shows "((a oo c) * (b oo d))$n =
setsum (\<lambda>(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r")
proof -
- let ?S = "{(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
+ let ?S = "{(k::nat, m::nat). k + m \<le> n}"
have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
- have f: "finite {(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
+ have f: "finite {(k::nat, m::nat). k + m \<le> n}"
apply (rule finite_subset[OF s])
apply auto
done
@@ -2708,7 +2779,8 @@
lemma fps_X_power_compose:
assumes a0: "a$0=0"
- shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r")
+ shows "X^k oo a = (a::'a::idom fps)^k"
+ (is "?l = ?r")
proof (cases k)
case 0
then show ?thesis by simp
@@ -2752,7 +2824,7 @@
qed
lemma fps_inv_deriv:
- assumes a0:"a$0 = (0::'a::{field})"
+ assumes a0:"a$0 = (0::'a::field)"
and a1: "a$1 \<noteq> 0"
shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
proof -
@@ -2815,7 +2887,7 @@
qed
lemma fps_ginv_deriv:
- assumes a0:"a$0 = (0::'a::{field})"
+ assumes a0:"a$0 = (0::'a::field)"
and a1: "a$1 \<noteq> 0"
shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
proof -
@@ -2858,7 +2930,7 @@
qed
lemma E_unique_ODE:
- "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::field_char_0)"
+ "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)"
(is "?lhs \<longleftrightarrow> ?rhs")
proof
assume d: ?lhs
@@ -2900,7 +2972,7 @@
lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)"
by (simp add: E_def)
-lemma E0[simp]: "E (0::'a::{field}) = 1"
+lemma E0[simp]: "E (0::'a::field) = 1"
by (simp add: fps_eq_iff power_0_left)
lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
@@ -2914,7 +2986,7 @@
lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
by (induct n) auto
-lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
+lemma X_compose_E[simp]: "X oo E (a::'a::field) = E a - 1"
by (simp add: fps_eq_iff X_fps_compose)
lemma LE_compose:
@@ -2937,7 +3009,7 @@
done
lemma inverse_one_plus_X:
- "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
+ "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::field)^n)"
(is "inverse ?l = ?r")
proof -
have th: "?l * ?r = 1"
@@ -2951,7 +3023,7 @@
lemma radical_E:
assumes r: "r (Suc k) 1 = 1"
- shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
+ shows "fps_radical r (Suc k) (E (c::'a::field_char_0)) = E (c / of_nat (Suc k))"
proof -
let ?ck = "(c / of_nat (Suc k))"
let ?r = "fps_radical r (Suc k)"
@@ -2964,7 +3036,7 @@
show ?thesis by auto
qed
-lemma Ec_E1_eq: "E (1::'a::{field_char_0}) oo (fps_const c * X) = E c"
+lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c"
apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib)
apply (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong)
done
@@ -2972,13 +3044,13 @@
text{* The generalized binomial theorem as a consequence of @{thm E_add_mult} *}
lemma gbinomial_theorem:
- "((a::'a::{field_char_0, field_inverse_zero})+b) ^ n =
+ "((a::'a::{field_char_0,field_inverse_zero})+b) ^ n =
(\<Sum>k=0..n. of_nat (n choose k) * a^k * b^(n-k))"
proof -
from E_add_mult[of a b]
have "(E (a + b)) $ n = (E a * E b)$n" by simp
then have "(a + b) ^ n =
- (\<Sum>i\<Colon>nat = 0\<Colon>nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
+ (\<Sum>i::nat = 0::nat..n. a ^ i * b ^ (n - i) * (of_nat (fact n) / of_nat (fact i * fact (n - i))))"
by (simp add: field_simps fps_mult_nth of_nat_mult[symmetric] setsum_right_distrib)
then show ?thesis
apply simp
@@ -3614,7 +3686,7 @@
lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)"
by (simp add: fps_eq_iff fps_const_def)
-lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a:: {comm_ring_1})"
+lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)"
by (fact numeral_fps_const) (* FIXME: duplicate *)
lemma fps_cos_Eii: "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2"
@@ -3649,7 +3721,7 @@
subsection {* Hypergeometric series *}
-definition "F as bs (c::'a::{field_char_0, field_inverse_zero}) =
+definition "F as bs (c::'a::{field_char_0,field_inverse_zero}) =
Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
@@ -3722,7 +3794,7 @@
lemma XDp_nth[simp]: "XDp c a $ n = (c + of_nat n) * a$n"
by (simp add: XDp_def algebra_simps)
-lemma XDp_commute: "XDp b o XDp (c::'a::comm_ring_1) = XDp c o XDp b"
+lemma XDp_commute: "XDp b \<circ> XDp (c::'a::comm_ring_1) = XDp c \<circ> XDp b"
by (auto simp add: XDp_def fun_eq_iff fps_eq_iff algebra_simps)
lemma XDp0 [simp]: "XDp 0 = XD"
@@ -3732,11 +3804,11 @@
by (simp add: fps_eq_iff fps_integral_def)
lemma F_minus_nat:
- "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0, field_inverse_zero}) $ k =
+ "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
(if k \<le> n then
pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k))
else 0)"
- "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0, field_inverse_zero}) $ k =
+ "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field_inverse_zero}) $ k =
(if k \<le> m then
pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
else 0)"
@@ -3751,13 +3823,13 @@
lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
by (cases n) (simp_all add: pochhammer_rec)
-lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c o r) cs (\<lambda>c. XDp c a) c0 $ n =
+lemma XDp_foldr_nth [simp]: "foldr (\<lambda>c r. XDp c \<circ> r) cs (\<lambda>c. XDp c a) c0 $ n =
foldr (\<lambda>c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a$n"
by (induct cs arbitrary: c0) (auto simp add: algebra_simps)
lemma genric_XDp_foldr_nth:
assumes f: "\<forall>n c a. f c a $ n = (of_nat n + k c) * a$n"
- shows "foldr (\<lambda>c r. f c o r) cs (\<lambda>c. g c a) c0 $ n =
+ shows "foldr (\<lambda>c r. f c \<circ> r) cs (\<lambda>c. g c a) c0 $ n =
foldr (\<lambda>c r. (k c + of_nat n) * r) cs (g c0 a $ n)"
by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)
@@ -3794,7 +3866,7 @@
instance fps :: (comm_ring_1) complete_space
proof
- fix X::"nat \<Rightarrow> 'a fps"
+ fix X :: "nat \<Rightarrow> 'a fps"
assume "Cauchy X"
{
fix i
--- a/src/HOL/Library/Permutations.thy Fri Dec 06 09:42:13 2013 +0100
+++ b/src/HOL/Library/Permutations.thy Fri Dec 06 17:33:45 2013 +0100
@@ -8,371 +8,465 @@
imports Parity Fact
begin
-definition permutes (infixr "permutes" 41) where
- "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
-
-(* ------------------------------------------------------------------------- *)
-(* Transpositions. *)
-(* ------------------------------------------------------------------------- *)
+subsection {* Transpositions *}
lemma swapid_sym: "Fun.swap a b id = Fun.swap b a id"
by (auto simp add: fun_eq_iff swap_def fun_upd_def)
-lemma swap_id_refl: "Fun.swap a a id = id" by simp
+
+lemma swap_id_refl: "Fun.swap a a id = id"
+ by simp
+
lemma swap_id_sym: "Fun.swap a b id = Fun.swap b a id"
by (rule ext, simp add: swap_def)
-lemma swap_id_idempotent[simp]: "Fun.swap a b id o Fun.swap a b id = id"
+
+lemma swap_id_idempotent[simp]: "Fun.swap a b id \<circ> Fun.swap a b id = id"
by (rule ext, auto simp add: swap_def)
-lemma inv_unique_comp: assumes fg: "f o g = id" and gf: "g o f = id"
+lemma inv_unique_comp:
+ assumes fg: "f \<circ> g = id"
+ and gf: "g \<circ> f = id"
shows "inv f = g"
using fg gf inv_equality[of g f] by (auto simp add: fun_eq_iff)
lemma inverse_swap_id: "inv (Fun.swap a b id) = Fun.swap a b id"
- by (rule inv_unique_comp, simp_all)
+ by (rule inv_unique_comp) simp_all
lemma swap_id_eq: "Fun.swap a b id x = (if x = a then b else if x = b then a else x)"
by (simp add: swap_def)
-(* ------------------------------------------------------------------------- *)
-(* Basic consequences of the definition. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Basic consequences of the definition *}
+
+definition permutes (infixr "permutes" 41)
+ where "(p permutes S) \<longleftrightarrow> (\<forall>x. x \<notin> S \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)"
lemma permutes_in_image: "p permutes S \<Longrightarrow> p x \<in> S \<longleftrightarrow> x \<in> S"
unfolding permutes_def by metis
-lemma permutes_image: assumes pS: "p permutes S" shows "p ` S = S"
- using pS
+lemma permutes_image: "p permutes S \<Longrightarrow> p ` S = S"
unfolding permutes_def
- apply -
apply (rule set_eqI)
apply (simp add: image_iff)
apply metis
done
-lemma permutes_inj: "p permutes S ==> inj p "
+lemma permutes_inj: "p permutes S \<Longrightarrow> inj p"
unfolding permutes_def inj_on_def by blast
-lemma permutes_surj: "p permutes s ==> surj p"
+lemma permutes_surj: "p permutes s \<Longrightarrow> surj p"
unfolding permutes_def surj_def by metis
-lemma permutes_inv_o: assumes pS: "p permutes S"
- shows " p o inv p = id"
- and "inv p o p = id"
+lemma permutes_inv_o:
+ assumes pS: "p permutes S"
+ shows "p \<circ> inv p = id"
+ and "inv p \<circ> p = id"
using permutes_inj[OF pS] permutes_surj[OF pS]
unfolding inj_iff[symmetric] surj_iff[symmetric] by blast+
-
lemma permutes_inverses:
fixes p :: "'a \<Rightarrow> 'a"
assumes pS: "p permutes S"
shows "p (inv p x) = x"
- and "inv p (p x) = x"
+ and "inv p (p x) = x"
using permutes_inv_o[OF pS, unfolded fun_eq_iff o_def] by auto
-lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T ==> p permutes T"
+lemma permutes_subset: "p permutes S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> p permutes T"
unfolding permutes_def by blast
lemma permutes_empty[simp]: "p permutes {} \<longleftrightarrow> p = id"
- unfolding fun_eq_iff permutes_def apply simp by metis
+ unfolding fun_eq_iff permutes_def by simp metis
lemma permutes_sing[simp]: "p permutes {a} \<longleftrightarrow> p = id"
- unfolding fun_eq_iff permutes_def apply simp by metis
+ unfolding fun_eq_iff permutes_def by simp metis
lemma permutes_univ: "p permutes UNIV \<longleftrightarrow> (\<forall>y. \<exists>!x. p x = y)"
unfolding permutes_def by simp
-lemma permutes_inv_eq: "p permutes S ==> inv p y = x \<longleftrightarrow> p x = y"
- unfolding permutes_def inv_def apply auto
+lemma permutes_inv_eq: "p permutes S \<Longrightarrow> inv p y = x \<longleftrightarrow> p x = y"
+ unfolding permutes_def inv_def
+ apply auto
apply (erule allE[where x=y])
apply (erule allE[where x=y])
- apply (rule someI_ex) apply blast
+ apply (rule someI_ex)
+ apply blast
apply (rule some1_equality)
apply blast
apply blast
done
-lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S ==> Fun.swap a b id permutes S"
- unfolding permutes_def swap_def fun_upd_def by auto metis
+lemma permutes_swap_id: "a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> Fun.swap a b id permutes S"
+ unfolding permutes_def swap_def fun_upd_def by auto metis
-lemma permutes_superset:
- "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
-by (simp add: Ball_def permutes_def) metis
+lemma permutes_superset: "p permutes S \<Longrightarrow> (\<forall>x \<in> S - T. p x = x) \<Longrightarrow> p permutes T"
+ by (simp add: Ball_def permutes_def) metis
+
-(* ------------------------------------------------------------------------- *)
-(* Group properties. *)
-(* ------------------------------------------------------------------------- *)
+subsection {* Group properties *}
-lemma permutes_id: "id permutes S" unfolding permutes_def by simp
+lemma permutes_id: "id permutes S"
+ unfolding permutes_def by simp
-lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S ==> q o p permutes S"
+lemma permutes_compose: "p permutes S \<Longrightarrow> q permutes S \<Longrightarrow> q \<circ> p permutes S"
unfolding permutes_def o_def by metis
-lemma permutes_inv: assumes pS: "p permutes S" shows "inv p permutes S"
+lemma permutes_inv:
+ assumes pS: "p permutes S"
+ shows "inv p permutes S"
using pS unfolding permutes_def permutes_inv_eq[OF pS] by metis
-lemma permutes_inv_inv: assumes pS: "p permutes S" shows "inv (inv p) = p"
+lemma permutes_inv_inv:
+ assumes pS: "p permutes S"
+ shows "inv (inv p) = p"
unfolding fun_eq_iff permutes_inv_eq[OF pS] permutes_inv_eq[OF permutes_inv[OF pS]]
by blast
-(* ------------------------------------------------------------------------- *)
-(* The number of permutations on a finite set. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* The number of permutations on a finite set *}
lemma permutes_insert_lemma:
assumes pS: "p permutes (insert a S)"
- shows "Fun.swap a (p a) id o p permutes S"
+ shows "Fun.swap a (p a) id \<circ> p permutes S"
apply (rule permutes_superset[where S = "insert a S"])
apply (rule permutes_compose[OF pS])
apply (rule permutes_swap_id, simp)
- using permutes_in_image[OF pS, of a] apply simp
+ using permutes_in_image[OF pS, of a]
+ apply simp
apply (auto simp add: Ball_def swap_def)
done
lemma permutes_insert: "{p. p permutes (insert a S)} =
- (\<lambda>(b,p). Fun.swap a b id o p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
-proof-
-
- {fix p
- {assume pS: "p permutes insert a S"
+ (\<lambda>(b,p). Fun.swap a b id \<circ> p) ` {(b,p). b \<in> insert a S \<and> p \<in> {p. p permutes S}}"
+proof -
+ {
+ fix p
+ {
+ assume pS: "p permutes insert a S"
let ?b = "p a"
- let ?q = "Fun.swap a (p a) id o p"
- have th0: "p = Fun.swap a ?b id o ?q" unfolding fun_eq_iff o_assoc by simp
- have th1: "?b \<in> insert a S " unfolding permutes_in_image[OF pS] by simp
+ let ?q = "Fun.swap a (p a) id \<circ> p"
+ have th0: "p = Fun.swap a ?b id \<circ> ?q"
+ unfolding fun_eq_iff o_assoc by simp
+ have th1: "?b \<in> insert a S"
+ unfolding permutes_in_image[OF pS] by simp
from permutes_insert_lemma[OF pS] th0 th1
- have "\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S" by blast}
+ have "\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S" by blast
+ }
moreover
- {fix b q assume bq: "p = Fun.swap a b id o q" "b \<in> insert a S" "q permutes S"
+ {
+ fix b q
+ assume bq: "p = Fun.swap a b id \<circ> q" "b \<in> insert a S" "q permutes S"
from permutes_subset[OF bq(3), of "insert a S"]
- have qS: "q permutes insert a S" by auto
- have aS: "a \<in> insert a S" by simp
+ have qS: "q permutes insert a S"
+ by auto
+ have aS: "a \<in> insert a S"
+ by simp
from bq(1) permutes_compose[OF qS permutes_swap_id[OF aS bq(2)]]
- have "p permutes insert a S" by simp }
- ultimately have "p permutes insert a S \<longleftrightarrow> (\<exists> b q. p = Fun.swap a b id o q \<and> b \<in> insert a S \<and> q permutes S)" by blast}
- thus ?thesis by auto
+ have "p permutes insert a S"
+ by simp
+ }
+ ultimately have "p permutes insert a S \<longleftrightarrow>
+ (\<exists>b q. p = Fun.swap a b id \<circ> q \<and> b \<in> insert a S \<and> q permutes S)"
+ by blast
+ }
+ then show ?thesis
+ by auto
qed
-lemma card_permutations: assumes Sn: "card S = n" and fS: "finite S"
+lemma card_permutations:
+ assumes Sn: "card S = n"
+ and fS: "finite S"
shows "card {p. p permutes S} = fact n"
-using fS Sn proof (induct arbitrary: n)
- case empty thus ?case by simp
+ using fS Sn
+proof (induct arbitrary: n)
+ case empty
+ then show ?case by simp
next
case (insert x F)
- { fix n assume H0: "card (insert x F) = n"
+ {
+ fix n
+ assume H0: "card (insert x F) = n"
let ?xF = "{p. p permutes insert x F}"
let ?pF = "{p. p permutes F}"
let ?pF' = "{(b, p). b \<in> insert x F \<and> p \<in> ?pF}"
let ?g = "(\<lambda>(b, p). Fun.swap x b id \<circ> p)"
from permutes_insert[of x F]
have xfgpF': "?xF = ?g ` ?pF'" .
- have Fs: "card F = n - 1" using `x \<notin> F` H0 `finite F` by auto
- from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)" using `finite F` by auto
- then have "finite ?pF" using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
- then have pF'f: "finite ?pF'" using H0 `finite F`
+ have Fs: "card F = n - 1"
+ using `x \<notin> F` H0 `finite F` by auto
+ from insert.hyps Fs have pFs: "card ?pF = fact (n - 1)"
+ using `finite F` by auto
+ then have "finite ?pF"
+ using fact_gt_zero_nat by (auto intro: card_ge_0_finite)
+ then have pF'f: "finite ?pF'"
+ using H0 `finite F`
apply (simp only: Collect_split Collect_mem_eq)
apply (rule finite_cartesian_product)
apply simp_all
done
have ginj: "inj_on ?g ?pF'"
- proof-
+ proof -
{
- fix b p c q assume bp: "(b,p) \<in> ?pF'" and cq: "(c,q) \<in> ?pF'"
- and eq: "?g (b,p) = ?g (c,q)"
- from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F" "p permutes F" "q permutes F" by auto
- from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x" unfolding permutes_def
+ fix b p c q
+ assume bp: "(b,p) \<in> ?pF'"
+ assume cq: "(c,q) \<in> ?pF'"
+ assume eq: "?g (b,p) = ?g (c,q)"
+ from bp cq have ths: "b \<in> insert x F" "c \<in> insert x F" "x \<in> insert x F"
+ "p permutes F" "q permutes F"
+ by auto
+ from ths(4) `x \<notin> F` eq have "b = ?g (b,p) x"
+ unfolding permutes_def
by (auto simp add: swap_def fun_upd_def fun_eq_iff)
- also have "\<dots> = ?g (c,q) x" using ths(5) `x \<notin> F` eq
+ also have "\<dots> = ?g (c,q) x"
+ using ths(5) `x \<notin> F` eq
by (auto simp add: swap_def fun_upd_def fun_eq_iff)
- also have "\<dots> = c"using ths(5) `x \<notin> F` unfolding permutes_def
+ also have "\<dots> = c"
+ using ths(5) `x \<notin> F`
+ unfolding permutes_def
by (auto simp add: swap_def fun_upd_def fun_eq_iff)
finally have bc: "b = c" .
- hence "Fun.swap x b id = Fun.swap x c id" by simp
- with eq have "Fun.swap x b id o p = Fun.swap x b id o q" by simp
- hence "Fun.swap x b id o (Fun.swap x b id o p) = Fun.swap x b id o (Fun.swap x b id o q)" by simp
- hence "p = q" by (simp add: o_assoc)
- with bc have "(b,p) = (c,q)" by simp
+ then have "Fun.swap x b id = Fun.swap x c id"
+ by simp
+ with eq have "Fun.swap x b id \<circ> p = Fun.swap x b id \<circ> q"
+ by simp
+ then have "Fun.swap x b id \<circ> (Fun.swap x b id \<circ> p) =
+ Fun.swap x b id \<circ> (Fun.swap x b id \<circ> q)"
+ by simp
+ then have "p = q"
+ by (simp add: o_assoc)
+ with bc have "(b, p) = (c, q)"
+ by simp
}
- thus ?thesis unfolding inj_on_def by blast
+ then show ?thesis
+ unfolding inj_on_def by blast
qed
- from `x \<notin> F` H0 have n0: "n \<noteq> 0 " using `finite F` by auto
- hence "\<exists>m. n = Suc m" by presburger
- then obtain m where n[simp]: "n = Suc m" by blast
+ from `x \<notin> F` H0 have n0: "n \<noteq> 0"
+ using `finite F` by auto
+ then have "\<exists>m. n = Suc m"
+ by presburger
+ then obtain m where n[simp]: "n = Suc m"
+ by blast
from pFs H0 have xFc: "card ?xF = fact n"
- unfolding xfgpF' card_image[OF ginj] using `finite F` `finite ?pF`
+ unfolding xfgpF' card_image[OF ginj]
+ using `finite F` `finite ?pF`
apply (simp only: Collect_split Collect_mem_eq card_cartesian_product)
- by simp
- from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF" unfolding xfgpF' by simp
+ apply simp
+ done
+ from finite_imageI[OF pF'f, of ?g] have xFf: "finite ?xF"
+ unfolding xfgpF' by simp
have "card ?xF = fact n"
using xFf xFc unfolding xFf by blast
}
- thus ?case using insert by simp
+ then show ?case
+ using insert by simp
qed
-lemma finite_permutations: assumes fS: "finite S" shows "finite {p. p permutes S}"
+lemma finite_permutations:
+ assumes fS: "finite S"
+ shows "finite {p. p permutes S}"
using card_permutations[OF refl fS] fact_gt_zero_nat
by (auto intro: card_ge_0_finite)
-(* ------------------------------------------------------------------------- *)
-(* Permutations of index set for iterated operations. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Permutations of index set for iterated operations *}
lemma (in comm_monoid_set) permute:
assumes "p permutes S"
- shows "F g S = F (g o p) S"
+ shows "F g S = F (g \<circ> p) S"
proof -
- from `p permutes S` have "inj p" by (rule permutes_inj)
- then have "inj_on p S" by (auto intro: subset_inj_on)
- then have "F g (p ` S) = F (g o p) S" by (rule reindex)
- moreover from `p permutes S` have "p ` S = S" by (rule permutes_image)
- ultimately show ?thesis by simp
+ from `p permutes S` have "inj p"
+ by (rule permutes_inj)
+ then have "inj_on p S"
+ by (auto intro: subset_inj_on)
+ then have "F g (p ` S) = F (g \<circ> p) S"
+ by (rule reindex)
+ moreover from `p permutes S` have "p ` S = S"
+ by (rule permutes_image)
+ ultimately show ?thesis
+ by simp
qed
lemma setsum_permute:
assumes "p permutes S"
- shows "setsum f S = setsum (f o p) S"
+ shows "setsum f S = setsum (f \<circ> p) S"
using assms by (fact setsum.permute)
lemma setsum_permute_natseg:
assumes pS: "p permutes {m .. n}"
- shows "setsum f {m .. n} = setsum (f o p) {m .. n}"
+ shows "setsum f {m .. n} = setsum (f \<circ> p) {m .. n}"
using setsum_permute [OF pS, of f ] pS by blast
lemma setprod_permute:
assumes "p permutes S"
- shows "setprod f S = setprod (f o p) S"
+ shows "setprod f S = setprod (f \<circ> p) S"
using assms by (fact setprod.permute)
lemma setprod_permute_natseg:
assumes pS: "p permutes {m .. n}"
- shows "setprod f {m .. n} = setprod (f o p) {m .. n}"
+ shows "setprod f {m .. n} = setprod (f \<circ> p) {m .. n}"
using setprod_permute [OF pS, of f ] pS by blast
-(* ------------------------------------------------------------------------- *)
-(* Various combinations of transpositions with 2, 1 and 0 common elements. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Various combinations of transpositions with 2, 1 and 0 common elements *}
+
+lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow>
+ Fun.swap a b id \<circ> Fun.swap a c id = Fun.swap b c id \<circ> Fun.swap a b id"
+ by (simp add: fun_eq_iff swap_def)
-lemma swap_id_common:" a \<noteq> c \<Longrightarrow> b \<noteq> c \<Longrightarrow> Fun.swap a b id o Fun.swap a c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
+lemma swap_id_common': "a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow>
+ Fun.swap a c id \<circ> Fun.swap b c id = Fun.swap b c id \<circ> Fun.swap a b id"
+ by (simp add: fun_eq_iff swap_def)
-lemma swap_id_common': "~(a = b) \<Longrightarrow> ~(a = c) \<Longrightarrow> Fun.swap a c id o Fun.swap b c id = Fun.swap b c id o Fun.swap a b id" by (simp add: fun_eq_iff swap_def)
-
-lemma swap_id_independent: "~(a = c) \<Longrightarrow> ~(a = d) \<Longrightarrow> ~(b = c) \<Longrightarrow> ~(b = d) ==> Fun.swap a b id o Fun.swap c d id = Fun.swap c d id o Fun.swap a b id"
+lemma swap_id_independent: "a \<noteq> c \<Longrightarrow> a \<noteq> d \<Longrightarrow> b \<noteq> c \<Longrightarrow> b \<noteq> d \<Longrightarrow>
+ Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap c d id \<circ> Fun.swap a b id"
by (simp add: swap_def fun_eq_iff)
-(* ------------------------------------------------------------------------- *)
-(* Permutations as transposition sequences. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Permutations as transposition sequences *}
+
+inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool"
+where
+ id[simp]: "swapidseq 0 id"
+| comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id \<circ> p)"
+
+declare id[unfolded id_def, simp]
+
+definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
-inductive swapidseq :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> bool" where
- id[simp]: "swapidseq 0 id"
-| comp_Suc: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (Fun.swap a b id o p)"
-
-declare id[unfolded id_def, simp]
-definition "permutation p \<longleftrightarrow> (\<exists>n. swapidseq n p)"
+subsection {* Some closure properties of the set of permutations, with lengths *}
-(* ------------------------------------------------------------------------- *)
-(* Some closure properties of the set of permutations, with lengths. *)
-(* ------------------------------------------------------------------------- *)
+lemma permutation_id[simp]: "permutation id"
+ unfolding permutation_def by (rule exI[where x=0]) simp
-lemma permutation_id[simp]: "permutation id"unfolding permutation_def
- by (rule exI[where x=0], simp)
declare permutation_id[unfolded id_def, simp]
lemma swapidseq_swap: "swapidseq (if a = b then 0 else 1) (Fun.swap a b id)"
apply clarsimp
- using comp_Suc[of 0 id a b] by simp
+ using comp_Suc[of 0 id a b]
+ apply simp
+ done
lemma permutation_swap_id: "permutation (Fun.swap a b id)"
- apply (cases "a=b", simp_all)
- unfolding permutation_def using swapidseq_swap[of a b] by blast
+ apply (cases "a = b")
+ apply simp_all
+ unfolding permutation_def
+ using swapidseq_swap[of a b]
+ apply blast
+ done
-lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q ==> swapidseq (n + m) (p o q)"
- proof (induct n p arbitrary: m q rule: swapidseq.induct)
- case (id m q) thus ?case by simp
- next
- case (comp_Suc n p a b m q)
- have th: "Suc n + m = Suc (n + m)" by arith
- show ?case unfolding th comp_assoc
- apply (rule swapidseq.comp_Suc) using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3) by blast+
+lemma swapidseq_comp_add: "swapidseq n p \<Longrightarrow> swapidseq m q \<Longrightarrow> swapidseq (n + m) (p \<circ> q)"
+proof (induct n p arbitrary: m q rule: swapidseq.induct)
+ case (id m q)
+ then show ?case by simp
+next
+ case (comp_Suc n p a b m q)
+ have th: "Suc n + m = Suc (n + m)"
+ by arith
+ show ?case
+ unfolding th comp_assoc
+ apply (rule swapidseq.comp_Suc)
+ using comp_Suc.hyps(2)[OF comp_Suc.prems] comp_Suc.hyps(3)
+ apply blast+
+ done
qed
-lemma permutation_compose: "permutation p \<Longrightarrow> permutation q ==> permutation(p o q)"
+lemma permutation_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> permutation (p \<circ> q)"
unfolding permutation_def using swapidseq_comp_add[of _ p _ q] by metis
-lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b ==> swapidseq (Suc n) (p o Fun.swap a b id)"
+lemma swapidseq_endswap: "swapidseq n p \<Longrightarrow> a \<noteq> b \<Longrightarrow> swapidseq (Suc n) (p \<circ> Fun.swap a b id)"
apply (induct n p rule: swapidseq.induct)
using swapidseq_swap[of a b]
- by (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
+ apply (auto simp add: comp_assoc intro: swapidseq.comp_Suc)
+ done
-lemma swapidseq_inverse_exists: "swapidseq n p ==> \<exists>q. swapidseq n q \<and> p o q = id \<and> q o p = id"
-proof(induct n p rule: swapidseq.induct)
- case id thus ?case by (rule exI[where x=id], simp)
+lemma swapidseq_inverse_exists: "swapidseq n p \<Longrightarrow> \<exists>q. swapidseq n q \<and> p \<circ> q = id \<and> q \<circ> p = id"
+proof (induct n p rule: swapidseq.induct)
+ case id
+ then show ?case
+ by (rule exI[where x=id]) simp
next
case (comp_Suc n p a b)
- from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
- let ?q = "q o Fun.swap a b id"
+ from comp_Suc.hyps obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+ by blast
+ let ?q = "q \<circ> Fun.swap a b id"
note H = comp_Suc.hyps
- from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)" by simp
- from swapidseq_comp_add[OF q(1) th0] have th1:"swapidseq (Suc n) ?q" by simp
- have "Fun.swap a b id o p o ?q = Fun.swap a b id o (p o q) o Fun.swap a b id" by (simp add: o_assoc)
- also have "\<dots> = id" by (simp add: q(2))
- finally have th2: "Fun.swap a b id o p o ?q = id" .
- have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id o Fun.swap a b id) \<circ> p" by (simp only: o_assoc)
- hence "?q \<circ> (Fun.swap a b id \<circ> p) = id" by (simp add: q(3))
- with th1 th2 show ?case by blast
+ from swapidseq_swap[of a b] H(3) have th0: "swapidseq 1 (Fun.swap a b id)"
+ by simp
+ from swapidseq_comp_add[OF q(1) th0] have th1: "swapidseq (Suc n) ?q"
+ by simp
+ have "Fun.swap a b id \<circ> p \<circ> ?q = Fun.swap a b id \<circ> (p \<circ> q) \<circ> Fun.swap a b id"
+ by (simp add: o_assoc)
+ also have "\<dots> = id"
+ by (simp add: q(2))
+ finally have th2: "Fun.swap a b id \<circ> p \<circ> ?q = id" .
+ have "?q \<circ> (Fun.swap a b id \<circ> p) = q \<circ> (Fun.swap a b id \<circ> Fun.swap a b id) \<circ> p"
+ by (simp only: o_assoc)
+ then have "?q \<circ> (Fun.swap a b id \<circ> p) = id"
+ by (simp add: q(3))
+ with th1 th2 show ?case
+ by blast
qed
+lemma swapidseq_inverse:
+ assumes H: "swapidseq n p"
+ shows "swapidseq n (inv p)"
+ using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
+
+lemma permutation_inverse: "permutation p \<Longrightarrow> permutation (inv p)"
+ using permutation_def swapidseq_inverse by blast
+
-lemma swapidseq_inverse: assumes H: "swapidseq n p" shows "swapidseq n (inv p)"
- using swapidseq_inverse_exists[OF H] inv_unique_comp[of p] by auto
-
-lemma permutation_inverse: "permutation p ==> permutation (inv p)"
- using permutation_def swapidseq_inverse by blast
+subsection {* The identity map only has even transposition sequences *}
-(* ------------------------------------------------------------------------- *)
-(* The identity map only has even transposition sequences. *)
-(* ------------------------------------------------------------------------- *)
-
-lemma symmetry_lemma:"(\<And>a b c d. P a b c d ==> P a b d c) \<Longrightarrow>
- (\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> (a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d) ==> P a b c d)
- ==> (\<And>a b c d. a \<noteq> b --> c \<noteq> d \<longrightarrow> P a b c d)" by metis
+lemma symmetry_lemma:
+ assumes "\<And>a b c d. P a b c d \<Longrightarrow> P a b d c"
+ and "\<And>a b c d. a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
+ a = c \<and> b = d \<or> a = c \<and> b \<noteq> d \<or> a \<noteq> c \<and> b = d \<or> a \<noteq> c \<and> a \<noteq> d \<and> b \<noteq> c \<and> b \<noteq> d \<Longrightarrow>
+ P a b c d"
+ shows "\<And>a b c d. a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow> P a b c d"
+ using assms by metis
-lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow> Fun.swap a b id o Fun.swap c d id = id \<or>
- (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id)"
-proof-
- assume H: "a\<noteq>b" "c\<noteq>d"
-have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
-( Fun.swap a b id o Fun.swap c d id = id \<or>
- (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and> Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id))"
- apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
- apply (simp_all only: swapid_sym)
- apply (case_tac "a = c \<and> b = d", clarsimp simp only: swapid_sym swap_id_idempotent)
- apply (case_tac "a = c \<and> b \<noteq> d")
- apply (rule disjI2)
- apply (rule_tac x="b" in exI)
- apply (rule_tac x="d" in exI)
- apply (rule_tac x="b" in exI)
- apply (clarsimp simp add: fun_eq_iff swap_def)
- apply (case_tac "a \<noteq> c \<and> b = d")
- apply (rule disjI2)
- apply (rule_tac x="c" in exI)
- apply (rule_tac x="d" in exI)
- apply (rule_tac x="c" in exI)
- apply (clarsimp simp add: fun_eq_iff swap_def)
- apply (rule disjI2)
- apply (rule_tac x="c" in exI)
- apply (rule_tac x="d" in exI)
- apply (rule_tac x="b" in exI)
- apply (clarsimp simp add: fun_eq_iff swap_def)
- done
-with H show ?thesis by metis
+lemma swap_general: "a \<noteq> b \<Longrightarrow> c \<noteq> d \<Longrightarrow>
+ Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+ (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
+ Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id)"
+proof -
+ assume H: "a \<noteq> b" "c \<noteq> d"
+ have "a \<noteq> b \<longrightarrow> c \<noteq> d \<longrightarrow>
+ (Fun.swap a b id \<circ> Fun.swap c d id = id \<or>
+ (\<exists>x y z. x \<noteq> a \<and> y \<noteq> a \<and> z \<noteq> a \<and> x \<noteq> y \<and>
+ Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id))"
+ apply (rule symmetry_lemma[where a=a and b=b and c=c and d=d])
+ apply (simp_all only: swapid_sym)
+ apply (case_tac "a = c \<and> b = d")
+ apply (clarsimp simp only: swapid_sym swap_id_idempotent)
+ apply (case_tac "a = c \<and> b \<noteq> d")
+ apply (rule disjI2)
+ apply (rule_tac x="b" in exI)
+ apply (rule_tac x="d" in exI)
+ apply (rule_tac x="b" in exI)
+ apply (clarsimp simp add: fun_eq_iff swap_def)
+ apply (case_tac "a \<noteq> c \<and> b = d")
+ apply (rule disjI2)
+ apply (rule_tac x="c" in exI)
+ apply (rule_tac x="d" in exI)
+ apply (rule_tac x="c" in exI)
+ apply (clarsimp simp add: fun_eq_iff swap_def)
+ apply (rule disjI2)
+ apply (rule_tac x="c" in exI)
+ apply (rule_tac x="d" in exI)
+ apply (rule_tac x="b" in exI)
+ apply (clarsimp simp add: fun_eq_iff swap_def)
+ done
+ with H show ?thesis by metis
qed
lemma swapidseq_id_iff[simp]: "swapidseq 0 p \<longleftrightarrow> p = id"
using swapidseq.cases[of 0 p "p = id"]
by auto
-lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow> (n=0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id o q \<and> swapidseq m q \<and> a\<noteq> b))"
+lemma swapidseq_cases: "swapidseq n p \<longleftrightarrow>
+ n = 0 \<and> p = id \<or> (\<exists>a b q m. n = Suc m \<and> p = Fun.swap a b id \<circ> q \<and> swapidseq m q \<and> a \<noteq> b)"
apply (rule iffI)
apply (erule swapidseq.cases[of n p])
apply simp
@@ -385,124 +479,161 @@
apply auto
apply (rule comp_Suc, simp_all)
done
+
lemma fixing_swapidseq_decrease:
- assumes spn: "swapidseq n p" and ab: "a\<noteq>b" and pa: "(Fun.swap a b id o p) a = a"
- shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id o p)"
+ assumes spn: "swapidseq n p"
+ and ab: "a \<noteq> b"
+ and pa: "(Fun.swap a b id \<circ> p) a = a"
+ shows "n \<noteq> 0 \<and> swapidseq (n - 1) (Fun.swap a b id \<circ> p)"
using spn ab pa
-proof(induct n arbitrary: p a b)
- case 0 thus ?case by (auto simp add: swap_def fun_upd_def)
+proof (induct n arbitrary: p a b)
+ case 0
+ then show ?case
+ by (auto simp add: swap_def fun_upd_def)
next
case (Suc n p a b)
- from Suc.prems(1) swapidseq_cases[of "Suc n" p] obtain
- c d q m where cdqm: "Suc n = Suc m" "p = Fun.swap c d id o q" "swapidseq m q" "c \<noteq> d" "n = m"
+ from Suc.prems(1) swapidseq_cases[of "Suc n" p]
+ obtain c d q m where
+ cdqm: "Suc n = Suc m" "p = Fun.swap c d id \<circ> q" "swapidseq m q" "c \<noteq> d" "n = m"
by auto
- {assume H: "Fun.swap a b id o Fun.swap c d id = id"
-
- have ?case apply (simp only: cdqm o_assoc H)
- by (simp add: cdqm)}
+ {
+ assume H: "Fun.swap a b id \<circ> Fun.swap c d id = id"
+ have ?case by (simp only: cdqm o_assoc H) (simp add: cdqm)
+ }
moreover
- { fix x y z
- assume H: "x\<noteq>a" "y\<noteq>a" "z \<noteq>a" "x \<noteq>y"
- "Fun.swap a b id o Fun.swap c d id = Fun.swap x y id o Fun.swap a z id"
- from H have az: "a \<noteq> z" by simp
+ {
+ fix x y z
+ assume H: "x \<noteq> a" "y \<noteq> a" "z \<noteq> a" "x \<noteq> y"
+ "Fun.swap a b id \<circ> Fun.swap c d id = Fun.swap x y id \<circ> Fun.swap a z id"
+ from H have az: "a \<noteq> z"
+ by simp
- {fix h have "(Fun.swap x y id o h) a = a \<longleftrightarrow> h a = a"
- using H by (simp add: swap_def)}
+ {
+ fix h
+ have "(Fun.swap x y id \<circ> h) a = a \<longleftrightarrow> h a = a"
+ using H by (simp add: swap_def)
+ }
note th3 = this
- from cdqm(2) have "Fun.swap a b id o p = Fun.swap a b id o (Fun.swap c d id o q)" by simp
- hence "Fun.swap a b id o p = Fun.swap x y id o (Fun.swap a z id o q)" by (simp add: o_assoc H)
- hence "(Fun.swap a b id o p) a = (Fun.swap x y id o (Fun.swap a z id o q)) a" by simp
- hence "(Fun.swap x y id o (Fun.swap a z id o q)) a = a" unfolding Suc by metis
- hence th1: "(Fun.swap a z id o q) a = a" unfolding th3 .
+ from cdqm(2) have "Fun.swap a b id \<circ> p = Fun.swap a b id \<circ> (Fun.swap c d id \<circ> q)"
+ by simp
+ then have "Fun.swap a b id \<circ> p = Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)"
+ by (simp add: o_assoc H)
+ then have "(Fun.swap a b id \<circ> p) a = (Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a"
+ by simp
+ then have "(Fun.swap x y id \<circ> (Fun.swap a z id \<circ> q)) a = a"
+ unfolding Suc by metis
+ then have th1: "(Fun.swap a z id \<circ> q) a = a"
+ unfolding th3 .
from Suc.hyps[OF cdqm(3)[ unfolded cdqm(5)[symmetric]] az th1]
- have th2: "swapidseq (n - 1) (Fun.swap a z id o q)" "n \<noteq> 0" by blast+
- have th: "Suc n - 1 = Suc (n - 1)" using th2(2) by auto
- have ?case unfolding cdqm(2) H o_assoc th
+ have th2: "swapidseq (n - 1) (Fun.swap a z id \<circ> q)" "n \<noteq> 0"
+ by blast+
+ have th: "Suc n - 1 = Suc (n - 1)"
+ using th2(2) by auto
+ have ?case
+ unfolding cdqm(2) H o_assoc th
apply (simp only: Suc_not_Zero simp_thms comp_assoc)
apply (rule comp_Suc)
- using th2 H apply blast+
- done}
- ultimately show ?case using swap_general[OF Suc.prems(2) cdqm(4)] by metis
+ using th2 H
+ apply blast+
+ done
+ }
+ ultimately show ?case
+ using swap_general[OF Suc.prems(2) cdqm(4)] by metis
qed
lemma swapidseq_identity_even:
- assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)" shows "even n"
+ assumes "swapidseq n (id :: 'a \<Rightarrow> 'a)"
+ shows "even n"
using `swapidseq n id`
-proof(induct n rule: nat_less_induct)
+proof (induct n rule: nat_less_induct)
fix n
assume H: "\<forall>m<n. swapidseq m (id::'a \<Rightarrow> 'a) \<longrightarrow> even m" "swapidseq n (id :: 'a \<Rightarrow> 'a)"
- {assume "n = 0" hence "even n" by arith}
+ {
+ assume "n = 0"
+ then have "even n" by presburger
+ }
moreover
- {fix a b :: 'a and q m
+ {
+ fix a b :: 'a and q m
assume h: "n = Suc m" "(id :: 'a \<Rightarrow> 'a) = Fun.swap a b id \<circ> q" "swapidseq m q" "a \<noteq> b"
from fixing_swapidseq_decrease[OF h(3,4), unfolded h(2)[symmetric]]
- have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)" by auto
- from h m have mn: "m - 1 < n" by arith
- from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n" apply arith done}
- ultimately show "even n" using H(2)[unfolded swapidseq_cases[of n id]] by auto
+ have m: "m \<noteq> 0" "swapidseq (m - 1) (id :: 'a \<Rightarrow> 'a)"
+ by auto
+ from h m have mn: "m - 1 < n"
+ by arith
+ from H(1)[rule_format, OF mn m(2)] h(1) m(1) have "even n"
+ by presburger
+ }
+ ultimately show "even n"
+ using H(2)[unfolded swapidseq_cases[of n id]] by auto
qed
-(* ------------------------------------------------------------------------- *)
-(* Therefore we have a welldefined notion of parity. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Therefore we have a welldefined notion of parity *}
definition "evenperm p = even (SOME n. swapidseq n p)"
-lemma swapidseq_even_even: assumes
- m: "swapidseq m p" and n: "swapidseq n p"
+lemma swapidseq_even_even:
+ assumes m: "swapidseq m p"
+ and n: "swapidseq n p"
shows "even m \<longleftrightarrow> even n"
-proof-
+proof -
from swapidseq_inverse_exists[OF n]
- obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
-
+ obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+ by blast
from swapidseq_identity_even[OF swapidseq_comp_add[OF m q(1), unfolded q]]
- show ?thesis by arith
+ show ?thesis
+ by arith
qed
-lemma evenperm_unique: assumes p: "swapidseq n p" and n:"even n = b"
+lemma evenperm_unique:
+ assumes p: "swapidseq n p"
+ and n:"even n = b"
shows "evenperm p = b"
unfolding n[symmetric] evenperm_def
apply (rule swapidseq_even_even[where p = p])
apply (rule someI[where x = n])
- using p by blast+
+ using p
+ apply blast+
+ done
-(* ------------------------------------------------------------------------- *)
-(* And it has the expected composition properties. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* And it has the expected composition properties *}
lemma evenperm_id[simp]: "evenperm id = True"
- apply (rule evenperm_unique[where n = 0]) by simp_all
+ by (rule evenperm_unique[where n = 0]) simp_all
lemma evenperm_swap: "evenperm (Fun.swap a b id) = (a = b)"
-apply (rule evenperm_unique[where n="if a = b then 0 else 1"])
-by (simp_all add: swapidseq_swap)
+ by (rule evenperm_unique[where n="if a = b then 0 else 1"]) (simp_all add: swapidseq_swap)
lemma evenperm_comp:
- assumes p: "permutation p" and q:"permutation q"
- shows "evenperm (p o q) = (evenperm p = evenperm q)"
-proof-
- from p q obtain
- n m where n: "swapidseq n p" and m: "swapidseq m q"
+ assumes p: "permutation p"
+ and q:"permutation q"
+ shows "evenperm (p \<circ> q) = (evenperm p = evenperm q)"
+proof -
+ from p q obtain n m where n: "swapidseq n p" and m: "swapidseq m q"
unfolding permutation_def by blast
note nm = swapidseq_comp_add[OF n m]
- have th: "even (n + m) = (even n \<longleftrightarrow> even m)" by arith
+ have th: "even (n + m) = (even n \<longleftrightarrow> even m)"
+ by arith
from evenperm_unique[OF n refl] evenperm_unique[OF m refl]
evenperm_unique[OF nm th]
- show ?thesis by blast
+ show ?thesis
+ by blast
qed
-lemma evenperm_inv: assumes p: "permutation p"
+lemma evenperm_inv:
+ assumes p: "permutation p"
shows "evenperm (inv p) = evenperm p"
-proof-
- from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
+proof -
+ from p obtain n where n: "swapidseq n p"
+ unfolding permutation_def by blast
from evenperm_unique[OF swapidseq_inverse[OF n] evenperm_unique[OF n refl, symmetric]]
show ?thesis .
qed
-(* ------------------------------------------------------------------------- *)
-(* A more abstract characterization of permutations. *)
-(* ------------------------------------------------------------------------- *)
+subsection {* A more abstract characterization of permutations *}
lemma bij_iff: "bij f \<longleftrightarrow> (\<forall>x. \<exists>!y. f y = x)"
unfolding bij_def inj_on_def surj_def
@@ -514,40 +645,50 @@
lemma permutation_bijective:
assumes p: "permutation p"
shows "bij p"
-proof-
- from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
- from swapidseq_inverse_exists[OF n] obtain q where
- q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id" by blast
- thus ?thesis unfolding bij_iff apply (auto simp add: fun_eq_iff) apply metis done
+proof -
+ from p obtain n where n: "swapidseq n p"
+ unfolding permutation_def by blast
+ from swapidseq_inverse_exists[OF n]
+ obtain q where q: "swapidseq n q" "p \<circ> q = id" "q \<circ> p = id"
+ by blast
+ then show ?thesis unfolding bij_iff
+ apply (auto simp add: fun_eq_iff)
+ apply metis
+ done
qed
-lemma permutation_finite_support: assumes p: "permutation p"
+lemma permutation_finite_support:
+ assumes p: "permutation p"
shows "finite {x. p x \<noteq> x}"
-proof-
- from p obtain n where n: "swapidseq n p" unfolding permutation_def by blast
+proof -
+ from p obtain n where n: "swapidseq n p"
+ unfolding permutation_def by blast
from n show ?thesis
- proof(induct n p rule: swapidseq.induct)
- case id thus ?case by simp
+ proof (induct n p rule: swapidseq.induct)
+ case id
+ then show ?case by simp
next
case (comp_Suc n p a b)
let ?S = "insert a (insert b {x. p x \<noteq> x})"
- from comp_Suc.hyps(2) have fS: "finite ?S" by simp
- from `a \<noteq> b` have th: "{x. (Fun.swap a b id o p) x \<noteq> x} \<subseteq> ?S"
+ from comp_Suc.hyps(2) have fS: "finite ?S"
+ by simp
+ from `a \<noteq> b` have th: "{x. (Fun.swap a b id \<circ> p) x \<noteq> x} \<subseteq> ?S"
by (auto simp add: swap_def)
from finite_subset[OF th fS] show ?case .
-qed
+ qed
qed
-lemma bij_inv_eq_iff: "bij p ==> x = inv p y \<longleftrightarrow> p x = y"
- using surj_f_inv_f[of p] inv_f_f[of f] by (auto simp add: bij_def)
+lemma bij_inv_eq_iff: "bij p \<Longrightarrow> x = inv p y \<longleftrightarrow> p x = y"
+ using surj_f_inv_f[of p] by (auto simp add: bij_def)
lemma bij_swap_comp:
- assumes bp: "bij p" shows "Fun.swap a b id o p = Fun.swap (inv p a) (inv p b) p"
+ assumes bp: "bij p"
+ shows "Fun.swap a b id \<circ> p = Fun.swap (inv p a) (inv p b) p"
using surj_f_inv_f[OF bij_is_surj[OF bp]]
by (simp add: fun_eq_iff swap_def bij_inv_eq_iff[OF bp])
-lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id o p)"
-proof-
+lemma bij_swap_ompose_bij: "bij p \<Longrightarrow> bij (Fun.swap a b id \<circ> p)"
+proof -
assume H: "bij p"
show ?thesis
unfolding bij_swap_comp[OF H] bij_swap_iff
@@ -555,16 +696,20 @@
qed
lemma permutation_lemma:
- assumes fS: "finite S" and p: "bij p" and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
+ assumes fS: "finite S"
+ and p: "bij p"
+ and pS: "\<forall>x. x\<notin> S \<longrightarrow> p x = x"
shows "permutation p"
-using fS p pS
-proof(induct S arbitrary: p rule: finite_induct)
- case (empty p) thus ?case by simp
+ using fS p pS
+proof (induct S arbitrary: p rule: finite_induct)
+ case (empty p)
+ then show ?case by simp
next
case (insert a F p)
- let ?r = "Fun.swap a (p a) id o p"
- let ?q = "Fun.swap a (p a) id o ?r "
- have raa: "?r a = a" by (simp add: swap_def)
+ let ?r = "Fun.swap a (p a) id \<circ> p"
+ let ?q = "Fun.swap a (p a) id \<circ> ?r"
+ have raa: "?r a = a"
+ by (simp add: swap_def)
from bij_swap_ompose_bij[OF insert(4)]
have br: "bij ?r" .
@@ -572,136 +717,193 @@
apply (clarsimp simp add: swap_def)
apply (erule_tac x="x" in allE)
apply auto
- unfolding bij_iff apply metis
+ unfolding bij_iff
+ apply metis
done
from insert(3)[OF br th]
have rp: "permutation ?r" .
- have "permutation ?q" by (simp add: permutation_compose permutation_swap_id rp)
- thus ?case by (simp add: o_assoc)
+ have "permutation ?q"
+ by (simp add: permutation_compose permutation_swap_id rp)
+ then show ?case
+ by (simp add: o_assoc)
qed
lemma permutation: "permutation p \<longleftrightarrow> bij p \<and> finite {x. p x \<noteq> x}"
(is "?lhs \<longleftrightarrow> ?b \<and> ?f")
proof
assume p: ?lhs
- from p permutation_bijective permutation_finite_support show "?b \<and> ?f" by auto
+ from p permutation_bijective permutation_finite_support show "?b \<and> ?f"
+ by auto
next
- assume bf: "?b \<and> ?f"
- hence bf: "?f" "?b" by blast+
- from permutation_lemma[OF bf] show ?lhs by blast
+ assume "?b \<and> ?f"
+ then have "?f" "?b" by blast+
+ from permutation_lemma[OF this] show ?lhs
+ by blast
qed
-lemma permutation_inverse_works: assumes p: "permutation p"
- shows "inv p o p = id" "p o inv p = id"
+lemma permutation_inverse_works:
+ assumes p: "permutation p"
+ shows "inv p \<circ> p = id"
+ and "p \<circ> inv p = id"
using permutation_bijective [OF p]
unfolding bij_def inj_iff surj_iff by auto
lemma permutation_inverse_compose:
- assumes p: "permutation p" and q: "permutation q"
- shows "inv (p o q) = inv q o inv p"
-proof-
+ assumes p: "permutation p"
+ and q: "permutation q"
+ shows "inv (p \<circ> q) = inv q \<circ> inv p"
+proof -
note ps = permutation_inverse_works[OF p]
note qs = permutation_inverse_works[OF q]
- have "p o q o (inv q o inv p) = p o (q o inv q) o inv p" by (simp add: o_assoc)
- also have "\<dots> = id" by (simp add: ps qs)
- finally have th0: "p o q o (inv q o inv p) = id" .
- have "inv q o inv p o (p o q) = inv q o (inv p o p) o q" by (simp add: o_assoc)
- also have "\<dots> = id" by (simp add: ps qs)
- finally have th1: "inv q o inv p o (p o q) = id" .
+ have "p \<circ> q \<circ> (inv q \<circ> inv p) = p \<circ> (q \<circ> inv q) \<circ> inv p"
+ by (simp add: o_assoc)
+ also have "\<dots> = id"
+ by (simp add: ps qs)
+ finally have th0: "p \<circ> q \<circ> (inv q \<circ> inv p) = id" .
+ have "inv q \<circ> inv p \<circ> (p \<circ> q) = inv q \<circ> (inv p \<circ> p) \<circ> q"
+ by (simp add: o_assoc)
+ also have "\<dots> = id"
+ by (simp add: ps qs)
+ finally have th1: "inv q \<circ> inv p \<circ> (p \<circ> q) = id" .
from inv_unique_comp[OF th0 th1] show ?thesis .
qed
-(* ------------------------------------------------------------------------- *)
-(* Relation to "permutes". *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Relation to "permutes" *}
lemma permutation_permutes: "permutation p \<longleftrightarrow> (\<exists>S. finite S \<and> p permutes S)"
-unfolding permutation permutes_def bij_iff[symmetric]
-apply (rule iffI, clarify)
-apply (rule exI[where x="{x. p x \<noteq> x}"])
-apply simp
-apply clarsimp
-apply (rule_tac B="S" in finite_subset)
-apply auto
-done
+ unfolding permutation permutes_def bij_iff[symmetric]
+ apply (rule iffI, clarify)
+ apply (rule exI[where x="{x. p x \<noteq> x}"])
+ apply simp
+ apply clarsimp
+ apply (rule_tac B="S" in finite_subset)
+ apply auto
+ done
-(* ------------------------------------------------------------------------- *)
-(* Hence a sort of induction principle composing by swaps. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Hence a sort of induction principle composing by swaps *}
-lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow> (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p ==> P (Fun.swap a b id o p))
- ==> (\<And>p. p permutes S ==> P p)"
-proof(induct S rule: finite_induct)
- case empty thus ?case by auto
+lemma permutes_induct: "finite S \<Longrightarrow> P id \<Longrightarrow>
+ (\<And> a b p. a \<in> S \<Longrightarrow> b \<in> S \<Longrightarrow> P p \<Longrightarrow> P p \<Longrightarrow> permutation p \<Longrightarrow> P (Fun.swap a b id \<circ> p)) \<Longrightarrow>
+ (\<And>p. p permutes S \<Longrightarrow> P p)"
+proof (induct S rule: finite_induct)
+ case empty
+ then show ?case by auto
next
case (insert x F p)
- let ?r = "Fun.swap x (p x) id o p"
- let ?q = "Fun.swap x (p x) id o ?r"
- have qp: "?q = p" by (simp add: o_assoc)
- from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r" by blast
+ let ?r = "Fun.swap x (p x) id \<circ> p"
+ let ?q = "Fun.swap x (p x) id \<circ> ?r"
+ have qp: "?q = p"
+ by (simp add: o_assoc)
+ from permutes_insert_lemma[OF insert.prems(3)] insert have Pr: "P ?r"
+ by blast
from permutes_in_image[OF insert.prems(3), of x]
- have pxF: "p x \<in> insert x F" by simp
- have xF: "x \<in> insert x F" by simp
+ have pxF: "p x \<in> insert x F"
+ by simp
+ have xF: "x \<in> insert x F"
+ by simp
have rp: "permutation ?r"
unfolding permutation_permutes using insert.hyps(1)
- permutes_insert_lemma[OF insert.prems(3)] by blast
+ permutes_insert_lemma[OF insert.prems(3)]
+ by blast
from insert.prems(2)[OF xF pxF Pr Pr rp]
- show ?case unfolding qp .
+ show ?case
+ unfolding qp .
qed
-(* ------------------------------------------------------------------------- *)
-(* Sign of a permutation as a real number. *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Sign of a permutation as a real number *}
definition "sign p = (if evenperm p then (1::int) else -1)"
-lemma sign_nz: "sign p \<noteq> 0" by (simp add: sign_def)
-lemma sign_id: "sign id = 1" by (simp add: sign_def)
-lemma sign_inverse: "permutation p ==> sign (inv p) = sign p"
+lemma sign_nz: "sign p \<noteq> 0"
+ by (simp add: sign_def)
+
+lemma sign_id: "sign id = 1"
+ by (simp add: sign_def)
+
+lemma sign_inverse: "permutation p \<Longrightarrow> sign (inv p) = sign p"
by (simp add: sign_def evenperm_inv)
-lemma sign_compose: "permutation p \<Longrightarrow> permutation q ==> sign (p o q) = sign(p) * sign(q)" by (simp add: sign_def evenperm_comp)
+
+lemma sign_compose: "permutation p \<Longrightarrow> permutation q \<Longrightarrow> sign (p \<circ> q) = sign p * sign q"
+ by (simp add: sign_def evenperm_comp)
+
lemma sign_swap_id: "sign (Fun.swap a b id) = (if a = b then 1 else -1)"
by (simp add: sign_def evenperm_swap)
-lemma sign_idempotent: "sign p * sign p = 1" by (simp add: sign_def)
-(* ------------------------------------------------------------------------- *)
-(* More lemmas about permutations. *)
-(* ------------------------------------------------------------------------- *)
+lemma sign_idempotent: "sign p * sign p = 1"
+ by (simp add: sign_def)
+
+
+subsection {* More lemmas about permutations *}
lemma permutes_natset_le:
- assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i <= i" shows "p = id"
-proof-
- {fix n
+ fixes S :: "'a::wellorder set"
+ assumes p: "p permutes S"
+ and le: "\<forall>i \<in> S. p i \<le> i"
+ shows "p = id"
+proof -
+ {
+ fix n
have "p n = n"
using p le
- proof(induct n arbitrary: S rule: less_induct)
- fix n S assume H: "\<And>m S. \<lbrakk>m < n; p permutes S; \<forall>i\<in>S. p i \<le> i\<rbrakk> \<Longrightarrow> p m = m"
+ proof (induct n arbitrary: S rule: less_induct)
+ fix n S
+ assume H:
+ "\<And>m S. m < n \<Longrightarrow> p permutes S \<Longrightarrow> \<forall>i\<in>S. p i \<le> i \<Longrightarrow> p m = m"
"p permutes S" "\<forall>i \<in>S. p i \<le> i"
- {assume "n \<notin> S"
- with H(2) have "p n = n" unfolding permutes_def by metis}
+ {
+ assume "n \<notin> S"
+ with H(2) have "p n = n"
+ unfolding permutes_def by metis
+ }
moreover
- {assume ns: "n \<in> S"
- from H(3) ns have "p n < n \<or> p n = n" by auto
- moreover{assume h: "p n < n"
- from H h have "p (p n) = p n" by metis
- with permutes_inj[OF H(2)] have "p n = n" unfolding inj_on_def by blast
- with h have False by simp}
- ultimately have "p n = n" by blast }
- ultimately show "p n = n" by blast
- qed}
- thus ?thesis by (auto simp add: fun_eq_iff)
+ {
+ assume ns: "n \<in> S"
+ from H(3) ns have "p n < n \<or> p n = n"
+ by auto
+ moreover {
+ assume h: "p n < n"
+ from H h have "p (p n) = p n"
+ by metis
+ with permutes_inj[OF H(2)] have "p n = n"
+ unfolding inj_on_def by blast
+ with h have False
+ by simp
+ }
+ ultimately have "p n = n"
+ by blast
+ }
+ ultimately show "p n = n"
+ by blast
+ qed
+ }
+ then show ?thesis
+ by (auto simp add: fun_eq_iff)
qed
lemma permutes_natset_ge:
- assumes p: "p permutes (S::'a::wellorder set)" and le: "\<forall>i \<in> S. p i \<ge> i" shows "p = id"
-proof-
- {fix i assume i: "i \<in> S"
- from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S" by simp
- with le have "p (inv p i) \<ge> inv p i" by blast
- with permutes_inverses[OF p] have "i \<ge> inv p i" by simp}
- then have th: "\<forall>i\<in>S. inv p i \<le> i" by blast
+ fixes S :: "'a::wellorder set"
+ assumes p: "p permutes S"
+ and le: "\<forall>i \<in> S. p i \<ge> i"
+ shows "p = id"
+proof -
+ {
+ fix i
+ assume i: "i \<in> S"
+ from i permutes_in_image[OF permutes_inv[OF p]] have "inv p i \<in> S"
+ by simp
+ with le have "p (inv p i) \<ge> inv p i"
+ by blast
+ with permutes_inverses[OF p] have "i \<ge> inv p i"
+ by simp
+ }
+ then have th: "\<forall>i\<in>S. inv p i \<le> i"
+ by blast
from permutes_natset_le[OF permutes_inv[OF p] th]
- have "inv p = inv id" by simp
+ have "inv p = inv id"
+ by simp
then show ?thesis
apply (subst permutes_inv_inv[OF p, symmetric])
apply (rule inv_unique_comp)
@@ -710,134 +912,160 @@
qed
lemma image_inverse_permutations: "{inv p |p. p permutes S} = {p. p permutes S}"
-apply (rule set_eqI)
-apply auto
- using permutes_inv_inv permutes_inv apply auto
+ apply (rule set_eqI)
+ apply auto
+ using permutes_inv_inv permutes_inv
+ apply auto
apply (rule_tac x="inv x" in exI)
apply auto
done
lemma image_compose_permutations_left:
- assumes q: "q permutes S" shows "{q o p | p. p permutes S} = {p . p permutes S}"
-apply (rule set_eqI)
-apply auto
-apply (rule permutes_compose)
-using q apply auto
-apply (rule_tac x = "inv q o x" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
+ assumes q: "q permutes S"
+ shows "{q \<circ> p | p. p permutes S} = {p . p permutes S}"
+ apply (rule set_eqI)
+ apply auto
+ apply (rule permutes_compose)
+ using q
+ apply auto
+ apply (rule_tac x = "inv q \<circ> x" in exI)
+ apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o)
+ done
lemma image_compose_permutations_right:
assumes q: "q permutes S"
- shows "{p o q | p. p permutes S} = {p . p permutes S}"
-apply (rule set_eqI)
-apply auto
-apply (rule permutes_compose)
-using q apply auto
-apply (rule_tac x = "x o inv q" in exI)
-by (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
+ shows "{p \<circ> q | p. p permutes S} = {p . p permutes S}"
+ apply (rule set_eqI)
+ apply auto
+ apply (rule permutes_compose)
+ using q
+ apply auto
+ apply (rule_tac x = "x \<circ> inv q" in exI)
+ apply (simp add: o_assoc permutes_inv permutes_compose permutes_inv_o comp_assoc)
+ done
-lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} ==> 1 <= p i \<and> p i <= n"
-
-apply (simp add: permutes_def)
-apply metis
-done
+lemma permutes_in_seg: "p permutes {1 ..n} \<Longrightarrow> i \<in> {1..n} \<Longrightarrow> 1 \<le> p i \<and> p i \<le> n"
+ by (simp add: permutes_def) metis
-lemma setsum_permutations_inverse: "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+lemma setsum_permutations_inverse:
+ "setsum f {p. p permutes S} = setsum (\<lambda>p. f(inv p)) {p. p permutes S}"
+ (is "?lhs = ?rhs")
+proof -
let ?S = "{p . p permutes S}"
-have th0: "inj_on inv ?S"
-proof(auto simp add: inj_on_def)
- fix q r
- assume q: "q permutes S" and r: "r permutes S" and qr: "inv q = inv r"
- hence "inv (inv q) = inv (inv r)" by simp
- with permutes_inv_inv[OF q] permutes_inv_inv[OF r]
- show "q = r" by metis
-qed
- have th1: "inv ` ?S = ?S" using image_inverse_permutations by blast
- have th2: "?rhs = setsum (f o inv) ?S" by (simp add: o_def)
- from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 .
+ have th0: "inj_on inv ?S"
+ proof (auto simp add: inj_on_def)
+ fix q r
+ assume q: "q permutes S"
+ and r: "r permutes S"
+ and qr: "inv q = inv r"
+ then have "inv (inv q) = inv (inv r)"
+ by simp
+ with permutes_inv_inv[OF q] permutes_inv_inv[OF r] show "q = r"
+ by metis
+ qed
+ have th1: "inv ` ?S = ?S"
+ using image_inverse_permutations by blast
+ have th2: "?rhs = setsum (f \<circ> inv) ?S"
+ by (simp add: o_def)
+ from setsum_reindex[OF th0, of f] show ?thesis unfolding th1 th2 .
qed
lemma setum_permutations_compose_left:
assumes q: "q permutes S"
- shows "setsum f {p. p permutes S} =
- setsum (\<lambda>p. f(q o p)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+ shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(q \<circ> p)) {p. p permutes S}"
+ (is "?lhs = ?rhs")
+proof -
let ?S = "{p. p permutes S}"
- have th0: "?rhs = setsum (f o (op o q)) ?S" by (simp add: o_def)
- have th1: "inj_on (op o q) ?S"
- apply (auto simp add: inj_on_def)
- proof-
+ have th0: "?rhs = setsum (f \<circ> (op \<circ> q)) ?S"
+ by (simp add: o_def)
+ have th1: "inj_on (op \<circ> q) ?S"
+ proof (auto simp add: inj_on_def)
fix p r
- assume "p permutes S" and r:"r permutes S" and rp: "q \<circ> p = q \<circ> r"
- hence "inv q o q o p = inv q o q o r" by (simp add: comp_assoc)
- with permutes_inj[OF q, unfolded inj_iff]
-
- show "p = r" by simp
+ assume "p permutes S"
+ and r: "r permutes S"
+ and rp: "q \<circ> p = q \<circ> r"
+ then have "inv q \<circ> q \<circ> p = inv q \<circ> q \<circ> r"
+ by (simp add: comp_assoc)
+ with permutes_inj[OF q, unfolded inj_iff] show "p = r"
+ by simp
qed
- have th3: "(op o q) ` ?S = ?S" using image_compose_permutations_left[OF q] by auto
- from setsum_reindex[OF th1, of f]
- show ?thesis unfolding th0 th1 th3 .
+ have th3: "(op \<circ> q) ` ?S = ?S"
+ using image_compose_permutations_left[OF q] by auto
+ from setsum_reindex[OF th1, of f] show ?thesis unfolding th0 th1 th3 .
qed
lemma sum_permutations_compose_right:
assumes q: "q permutes S"
- shows "setsum f {p. p permutes S} =
- setsum (\<lambda>p. f(p o q)) {p. p permutes S}" (is "?lhs = ?rhs")
-proof-
+ shows "setsum f {p. p permutes S} = setsum (\<lambda>p. f(p \<circ> q)) {p. p permutes S}"
+ (is "?lhs = ?rhs")
+proof -
let ?S = "{p. p permutes S}"
- have th0: "?rhs = setsum (f o (\<lambda>p. p o q)) ?S" by (simp add: o_def)
- have th1: "inj_on (\<lambda>p. p o q) ?S"
- apply (auto simp add: inj_on_def)
- proof-
+ have th0: "?rhs = setsum (f \<circ> (\<lambda>p. p \<circ> q)) ?S"
+ by (simp add: o_def)
+ have th1: "inj_on (\<lambda>p. p \<circ> q) ?S"
+ proof (auto simp add: inj_on_def)
fix p r
- assume "p permutes S" and r:"r permutes S" and rp: "p o q = r o q"
- hence "p o (q o inv q) = r o (q o inv q)" by (simp add: o_assoc)
- with permutes_surj[OF q, unfolded surj_iff]
-
- show "p = r" by simp
+ assume "p permutes S"
+ and r: "r permutes S"
+ and rp: "p \<circ> q = r \<circ> q"
+ then have "p \<circ> (q \<circ> inv q) = r \<circ> (q \<circ> inv q)"
+ by (simp add: o_assoc)
+ with permutes_surj[OF q, unfolded surj_iff] show "p = r"
+ by simp
qed
- have th3: "(\<lambda>p. p o q) ` ?S = ?S" using image_compose_permutations_right[OF q] by auto
+ have th3: "(\<lambda>p. p \<circ> q) ` ?S = ?S"
+ using image_compose_permutations_right[OF q] by auto
from setsum_reindex[OF th1, of f]
show ?thesis unfolding th0 th1 th3 .
qed
-(* ------------------------------------------------------------------------- *)
-(* Sum over a set of permutations (could generalize to iteration). *)
-(* ------------------------------------------------------------------------- *)
+
+subsection {* Sum over a set of permutations (could generalize to iteration) *}
lemma setsum_over_permutations_insert:
- assumes fS: "finite S" and aS: "a \<notin> S"
- shows "setsum f {p. p permutes (insert a S)} = setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id o q)) {p. p permutes S}) (insert a S)"
-proof-
- have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id o p)) = f o (\<lambda>(b,p). Fun.swap a b id o p)"
+ assumes fS: "finite S"
+ and aS: "a \<notin> S"
+ shows "setsum f {p. p permutes (insert a S)} =
+ setsum (\<lambda>b. setsum (\<lambda>q. f (Fun.swap a b id \<circ> q)) {p. p permutes S}) (insert a S)"
+proof -
+ have th0: "\<And>f a b. (\<lambda>(b,p). f (Fun.swap a b id \<circ> p)) = f \<circ> (\<lambda>(b,p). Fun.swap a b id \<circ> p)"
by (simp add: fun_eq_iff)
- have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}" by blast
- have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q" by blast
+ have th1: "\<And>P Q. P \<times> Q = {(a,b). a \<in> P \<and> b \<in> Q}"
+ by blast
+ have th2: "\<And>P Q. P \<Longrightarrow> (P \<Longrightarrow> Q) \<Longrightarrow> P \<and> Q"
+ by blast
show ?thesis
unfolding permutes_insert
unfolding setsum_cartesian_product
unfolding th1[symmetric]
unfolding th0
- proof(rule setsum_reindex)
+ proof (rule setsum_reindex)
let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
let ?P = "{p. p permutes S}"
- {fix b c p q assume b: "b \<in> insert a S" and c: "c \<in> insert a S"
- and p: "p permutes S" and q: "q permutes S"
- and eq: "Fun.swap a b id o p = Fun.swap a c id o q"
+ {
+ fix b c p q
+ assume b: "b \<in> insert a S"
+ assume c: "c \<in> insert a S"
+ assume p: "p permutes S"
+ assume q: "q permutes S"
+ assume eq: "Fun.swap a b id \<circ> p = Fun.swap a c id \<circ> q"
from p q aS have pa: "p a = a" and qa: "q a = a"
unfolding permutes_def by metis+
- from eq have "(Fun.swap a b id o p) a = (Fun.swap a c id o q) a" by simp
- hence bc: "b = c"
- by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def cong del: if_weak_cong split: split_if_asm)
- from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o p) = (\<lambda>p. Fun.swap a c id o p) (Fun.swap a c id o q)" by simp
- hence "p = q" unfolding o_assoc swap_id_idempotent
+ from eq have "(Fun.swap a b id \<circ> p) a = (Fun.swap a c id \<circ> q) a"
+ by simp
+ then have bc: "b = c"
+ by (simp add: permutes_def pa qa o_def fun_upd_def swap_def id_def
+ cong del: if_weak_cong split: split_if_asm)
+ from eq[unfolded bc] have "(\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> p) =
+ (\<lambda>p. Fun.swap a c id \<circ> p) (Fun.swap a c id \<circ> q)" by simp
+ then have "p = q"
+ unfolding o_assoc swap_id_idempotent
by (simp add: o_def)
- with bc have "b = c \<and> p = q" by blast
+ with bc have "b = c \<and> p = q"
+ by blast
}
then show "inj_on ?f (insert a S \<times> ?P)"
- unfolding inj_on_def
- apply clarify by metis
+ unfolding inj_on_def by clarify metis
qed
qed