author | immler |
Wed, 17 Jul 2013 13:34:21 +0200 | |
changeset 52681 | 8cc7f76b827a |
parent 51526 | 155263089e7b |
child 57862 | 8f074e6e22fc |
permissions | -rw-r--r-- |
50087 | 1 |
(* Author: Fabian Immler, TUM *) |
2 |
||
3 |
header {* Sequence of Properties on Subsequences *} |
|
4 |
||
5 |
theory Diagonal_Subsequence |
|
51526 | 6 |
imports Complex_Main |
50087 | 7 |
begin |
8 |
||
9 |
locale subseqs = |
|
10 |
fixes P::"nat\<Rightarrow>(nat\<Rightarrow>nat)\<Rightarrow>bool" |
|
11 |
assumes ex_subseq: "\<And>n s. subseq s \<Longrightarrow> \<exists>r'. subseq r' \<and> P n (s o r')" |
|
12 |
begin |
|
13 |
||
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
14 |
definition reduce where "reduce s n = (SOME r'. subseq r' \<and> P n (s o r'))" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
15 |
|
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
16 |
lemma subseq_reduce[intro, simp]: |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
17 |
"subseq s \<Longrightarrow> subseq (reduce s n)" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
18 |
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) auto |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
19 |
|
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
20 |
lemma reduce_holds: |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
21 |
"subseq s \<Longrightarrow> P n (s o reduce s n)" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
22 |
unfolding reduce_def by (rule someI2_ex[OF ex_subseq]) (auto simp: o_def) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
23 |
|
50087 | 24 |
primrec seqseq where |
25 |
"seqseq 0 = id" |
|
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
26 |
| "seqseq (Suc n) = seqseq n o reduce (seqseq n) n" |
50087 | 27 |
|
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
28 |
lemma subseq_seqseq[intro, simp]: "subseq (seqseq n)" |
50087 | 29 |
proof (induct n) |
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
30 |
case (Suc n) thus ?case by (subst seqseq.simps) (auto simp: subseq_reduce intro!: subseq_o) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
31 |
qed (simp add: subseq_def) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
32 |
|
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
33 |
lemma seqseq_holds: |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
34 |
"P n (seqseq (Suc n))" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
35 |
proof - |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
36 |
have "P n (seqseq n o reduce (seqseq n) n)" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
37 |
by (intro reduce_holds subseq_seqseq) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
38 |
thus ?thesis by simp |
50087 | 39 |
qed |
40 |
||
41 |
definition diagseq where "diagseq i = seqseq i i" |
|
42 |
||
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
43 |
lemma subseq_mono: "subseq f \<Longrightarrow> a \<le> b \<Longrightarrow> f a \<le> f b" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
44 |
by (metis le_eq_less_or_eq subseq_mono) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
45 |
|
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
46 |
lemma subseq_strict_mono: "subseq f \<Longrightarrow> a < b \<Longrightarrow> f a < f b" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
47 |
by (simp add: subseq_def) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
48 |
|
50087 | 49 |
lemma diagseq_mono: "diagseq n < diagseq (Suc n)" |
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
50 |
proof - |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
51 |
have "diagseq n < seqseq n (Suc n)" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
52 |
using subseq_seqseq[of n] by (simp add: diagseq_def subseq_def) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
53 |
also have "\<dots> \<le> seqseq n (reduce (seqseq n) n (Suc n))" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
54 |
by (auto intro: subseq_mono seq_suble) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
55 |
also have "\<dots> = diagseq (Suc n)" by (simp add: diagseq_def) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
56 |
finally show ?thesis . |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
57 |
qed |
50087 | 58 |
|
59 |
lemma subseq_diagseq: "subseq diagseq" |
|
60 |
using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def) |
|
61 |
||
62 |
primrec fold_reduce where |
|
63 |
"fold_reduce n 0 = id" |
|
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
64 |
| "fold_reduce n (Suc k) = fold_reduce n k o reduce (seqseq (n + k)) (n + k)" |
50087 | 65 |
|
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
66 |
lemma subseq_fold_reduce[intro, simp]: "subseq (fold_reduce n k)" |
50087 | 67 |
proof (induct k) |
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
68 |
case (Suc k) from subseq_o[OF this subseq_reduce] show ?case by (simp add: o_def) |
50087 | 69 |
qed (simp add: subseq_def) |
70 |
||
71 |
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k" |
|
72 |
by (induct k) simp_all |
|
73 |
||
74 |
lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n" |
|
75 |
by (induct n) (simp_all) |
|
76 |
||
77 |
lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n" |
|
78 |
using seqseq_fold_reduce by (simp add: diagseq_def) |
|
79 |
||
80 |
lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n" |
|
81 |
by (induct n) simp_all |
|
82 |
||
83 |
lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)" |
|
84 |
proof - |
|
85 |
have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)" |
|
86 |
by (simp add: diagseq_fold_reduce) |
|
87 |
also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)" |
|
88 |
unfolding fold_reduce_add seqseq_fold_reduce .. |
|
89 |
finally show ?thesis . |
|
90 |
qed |
|
91 |
||
92 |
lemma diagseq_sub: |
|
93 |
assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n" |
|
94 |
using diagseq_add[of m "n - m"] assms by simp |
|
95 |
||
96 |
lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))" |
|
97 |
unfolding subseq_Suc_iff fold_reduce.simps o_def |
|
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
98 |
proof |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
99 |
fix n |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
100 |
have "fold_reduce k n (k + n) < fold_reduce k n (k + Suc n)" (is "?lhs < _") |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
101 |
by (auto intro: subseq_strict_mono) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
102 |
also have "\<dots> \<le> fold_reduce k n (reduce (seqseq (k + n)) (k + n) (k + Suc n))" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
103 |
by (rule subseq_mono) (auto intro!: seq_suble subseq_mono) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
104 |
finally show "?lhs < \<dots>" . |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
105 |
qed |
50087 | 106 |
|
107 |
lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))" |
|
108 |
by (auto simp: o_def diagseq_add) |
|
109 |
||
52681
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
110 |
lemma diagseq_holds: |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
111 |
assumes subseq_stable: "\<And>r s n. subseq r \<Longrightarrow> P n s \<Longrightarrow> P n (s o r)" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
112 |
shows "P k (diagseq o (op + (Suc k)))" |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
113 |
unfolding diagseq_seqseq by (intro subseq_stable subseq_diagonal_rest seqseq_holds) |
8cc7f76b827a
tuned definition of seqseq; clarified usage of diagseq via diagseq_holds
immler
parents:
51526
diff
changeset
|
114 |
|
50087 | 115 |
end |
116 |
||
117 |
end |