50087
|
1 |
(* Author: Fabian Immler, TUM *)
|
|
2 |
|
|
3 |
header {* Sequence of Properties on Subsequences *}
|
|
4 |
|
|
5 |
theory Diagonal_Subsequence
|
|
6 |
imports SEQ
|
|
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 |
|
|
14 |
primrec seqseq where
|
|
15 |
"seqseq 0 = id"
|
|
16 |
| "seqseq (Suc n) = seqseq n o (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
|
|
17 |
|
|
18 |
lemma seqseq_ex:
|
|
19 |
shows "subseq (seqseq n) \<and>
|
|
20 |
(\<exists>r'. seqseq (Suc n) = seqseq n o r' \<and> subseq r' \<and> P n (seqseq n o r'))"
|
|
21 |
proof (induct n)
|
|
22 |
case 0
|
|
23 |
let ?P = "\<lambda>r'. subseq r' \<and> P 0 r'"
|
|
24 |
let ?r = "Eps ?P"
|
|
25 |
have "?P ?r" using ex_subseq[of id 0] by (intro someI_ex[of ?P]) (auto simp: subseq_def)
|
|
26 |
thus ?case by (auto simp: subseq_def)
|
|
27 |
next
|
|
28 |
case (Suc n)
|
|
29 |
then obtain r' where
|
|
30 |
Suc': "seqseq (Suc n) = seqseq n \<circ> r'" "subseq (seqseq n)" "subseq r'"
|
|
31 |
"P n (seqseq n o r')"
|
|
32 |
by blast
|
|
33 |
let ?P = "\<lambda>r'a. subseq (r'a ) \<and> P (Suc n) (seqseq n o r' o r'a)"
|
|
34 |
let ?r = "Eps ?P"
|
|
35 |
have "?P ?r" using ex_subseq[of "seqseq n o r'" "Suc n"] Suc'
|
|
36 |
by (intro someI_ex[of ?P]) (auto intro: subseq_o simp: o_assoc)
|
|
37 |
moreover have "seqseq (Suc (Suc n)) = seqseq n \<circ> r' \<circ> ?r"
|
|
38 |
by (subst seqseq.simps) (simp only: Suc' o_assoc)
|
|
39 |
moreover note subseq_o[OF `subseq (seqseq n)` `subseq r'`]
|
|
40 |
ultimately show ?case unfolding Suc' by (auto simp: o_def)
|
|
41 |
qed
|
|
42 |
|
|
43 |
lemma subseq_seqseq:
|
|
44 |
shows "subseq (seqseq n)" using seqseq_ex[OF assms] by auto
|
|
45 |
|
|
46 |
definition reducer where "reducer n = (SOME r'. subseq r' \<and> P n (seqseq n o r'))"
|
|
47 |
|
|
48 |
lemma subseq_reducer: "subseq (reducer n)" and reducer_reduces: "P n (seqseq n o reducer n)"
|
|
49 |
unfolding atomize_conj unfolding reducer_def using subseq_seqseq
|
|
50 |
by (rule someI_ex[OF ex_subseq])
|
|
51 |
|
|
52 |
lemma seqseq_reducer[simp]:
|
|
53 |
"seqseq (Suc n) = seqseq n o reducer n"
|
|
54 |
by (simp add: reducer_def)
|
|
55 |
|
|
56 |
declare seqseq.simps(2)[simp del]
|
|
57 |
|
|
58 |
definition diagseq where "diagseq i = seqseq i i"
|
|
59 |
|
|
60 |
lemma diagseq_mono: "diagseq n < diagseq (Suc n)"
|
|
61 |
unfolding diagseq_def seqseq_reducer o_def
|
|
62 |
by (metis subseq_mono[OF subseq_seqseq] less_le_trans lessI seq_suble subseq_reducer)
|
|
63 |
|
|
64 |
lemma subseq_diagseq: "subseq diagseq"
|
|
65 |
using diagseq_mono by (simp add: subseq_Suc_iff diagseq_def)
|
|
66 |
|
|
67 |
primrec fold_reduce where
|
|
68 |
"fold_reduce n 0 = id"
|
|
69 |
| "fold_reduce n (Suc k) = fold_reduce n k o reducer (n + k)"
|
|
70 |
|
|
71 |
lemma subseq_fold_reduce: "subseq (fold_reduce n k)"
|
|
72 |
proof (induct k)
|
|
73 |
case (Suc k) from subseq_o[OF this subseq_reducer] show ?case by (simp add: o_def)
|
|
74 |
qed (simp add: subseq_def)
|
|
75 |
|
|
76 |
lemma ex_subseq_reduce_index: "seqseq (n + k) = seqseq n o fold_reduce n k"
|
|
77 |
by (induct k) simp_all
|
|
78 |
|
|
79 |
lemma seqseq_fold_reduce: "seqseq n = fold_reduce 0 n"
|
|
80 |
by (induct n) (simp_all)
|
|
81 |
|
|
82 |
lemma diagseq_fold_reduce: "diagseq n = fold_reduce 0 n n"
|
|
83 |
using seqseq_fold_reduce by (simp add: diagseq_def)
|
|
84 |
|
|
85 |
lemma fold_reduce_add: "fold_reduce 0 (m + n) = fold_reduce 0 m o fold_reduce m n"
|
|
86 |
by (induct n) simp_all
|
|
87 |
|
|
88 |
lemma diagseq_add: "diagseq (k + n) = (seqseq k o (fold_reduce k n)) (k + n)"
|
|
89 |
proof -
|
|
90 |
have "diagseq (k + n) = fold_reduce 0 (k + n) (k + n)"
|
|
91 |
by (simp add: diagseq_fold_reduce)
|
|
92 |
also have "\<dots> = (seqseq k o fold_reduce k n) (k + n)"
|
|
93 |
unfolding fold_reduce_add seqseq_fold_reduce ..
|
|
94 |
finally show ?thesis .
|
|
95 |
qed
|
|
96 |
|
|
97 |
lemma diagseq_sub:
|
|
98 |
assumes "m \<le> n" shows "diagseq n = (seqseq m o (fold_reduce m (n - m))) n"
|
|
99 |
using diagseq_add[of m "n - m"] assms by simp
|
|
100 |
|
|
101 |
lemma subseq_diagonal_rest: "subseq (\<lambda>x. fold_reduce k x (k + x))"
|
|
102 |
unfolding subseq_Suc_iff fold_reduce.simps o_def
|
|
103 |
by (metis subseq_mono[OF subseq_fold_reduce] less_le_trans lessI add_Suc_right seq_suble
|
|
104 |
subseq_reducer)
|
|
105 |
|
|
106 |
lemma diagseq_seqseq: "diagseq o (op + k) = (seqseq k o (\<lambda>x. fold_reduce k x (k + x)))"
|
|
107 |
by (auto simp: o_def diagseq_add)
|
|
108 |
|
|
109 |
end
|
|
110 |
|
|
111 |
end
|