|
1 theory SCT_Misc |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 |
|
6 subsection {* Searching in lists *} |
|
7 |
|
8 fun index_of :: "'a list \<Rightarrow> 'a \<Rightarrow> nat" |
|
9 where |
|
10 "index_of [] c = 0" |
|
11 | "index_of (x#xs) c = (if x = c then 0 else Suc (index_of xs c))" |
|
12 |
|
13 lemma index_of_member: |
|
14 "(x \<in> set l) \<Longrightarrow> (l ! index_of l x = x)" |
|
15 by (induct l) auto |
|
16 |
|
17 lemma index_of_length: |
|
18 "(x \<in> set l) = (index_of l x < length l)" |
|
19 by (induct l) auto |
|
20 |
|
21 |
|
22 |
|
23 subsection {* Some reasoning tools *} |
|
24 |
|
25 lemma inc_induct[consumes 1]: |
|
26 assumes less: "i \<le> j" |
|
27 assumes base: "P j" |
|
28 assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i" |
|
29 shows "P i" |
|
30 using less |
|
31 proof (induct d\<equiv>"j - i" arbitrary: i) |
|
32 case (0 i) |
|
33 with `i \<le> j` have "i = j" by simp |
|
34 with base show ?case by simp |
|
35 next |
|
36 case (Suc d i) |
|
37 hence "i < j" "P (Suc i)" |
|
38 by simp_all |
|
39 thus "P i" by (rule step) |
|
40 qed |
|
41 |
|
42 lemma strict_inc_induct[consumes 1]: |
|
43 assumes less: "i < j" |
|
44 assumes base: "\<And>i. j = Suc i \<Longrightarrow> P i" |
|
45 assumes step: "\<And>i. \<lbrakk>i < j; P (Suc i)\<rbrakk> \<Longrightarrow> P i" |
|
46 shows "P i" |
|
47 using less |
|
48 proof (induct d\<equiv>"j - i - 1" arbitrary: i) |
|
49 case (0 i) |
|
50 with `i < j` have "j = Suc i" by simp |
|
51 with base show ?case by simp |
|
52 next |
|
53 case (Suc d i) |
|
54 hence "i < j" "P (Suc i)" |
|
55 by simp_all |
|
56 thus "P i" by (rule step) |
|
57 qed |
|
58 |
|
59 |
|
60 lemma three_cases: |
|
61 assumes "a1 \<Longrightarrow> thesis" |
|
62 assumes "a2 \<Longrightarrow> thesis" |
|
63 assumes "a3 \<Longrightarrow> thesis" |
|
64 assumes "\<And>R. \<lbrakk>a1 \<Longrightarrow> R; a2 \<Longrightarrow> R; a3 \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
65 shows "thesis" |
|
66 using prems |
|
67 by auto |
|
68 |
|
69 |
|
70 section {* Sequences *} |
|
71 |
|
72 types |
|
73 'a sequence = "nat \<Rightarrow> 'a" |
|
74 |
|
75 subsection {* Increasing sequences *} |
|
76 |
|
77 definition increasing :: "(nat \<Rightarrow> nat) \<Rightarrow> bool" |
|
78 where |
|
79 "increasing s = (\<forall>i j. i < j \<longrightarrow> s i < s j)" |
|
80 |
|
81 lemma increasing_strict: |
|
82 assumes "increasing s" |
|
83 assumes "i < j" |
|
84 shows "s i < s j" |
|
85 using prems |
|
86 unfolding increasing_def by simp |
|
87 |
|
88 lemma increasing_weak: |
|
89 assumes "increasing s" |
|
90 assumes "i \<le> j" |
|
91 shows "s i \<le> s j" |
|
92 using prems increasing_strict[of s i j] |
|
93 by (cases "i<j") auto |
|
94 |
|
95 lemma increasing_inc: |
|
96 assumes [simp]: "increasing s" |
|
97 shows "n \<le> s n" |
|
98 proof (induct n) |
|
99 case (Suc n) |
|
100 with increasing_strict[of s n "Suc n"] |
|
101 show ?case by auto |
|
102 qed auto |
|
103 |
|
104 |
|
105 lemma increasing_bij: |
|
106 assumes [simp]: "increasing s" |
|
107 shows "(s i < s j) = (i < j)" |
|
108 proof |
|
109 assume "s i < s j" |
|
110 show "i < j" |
|
111 proof (rule classical) |
|
112 assume "\<not> ?thesis" |
|
113 hence "j \<le> i" by arith |
|
114 with increasing_weak have "s j \<le> s i" by simp |
|
115 with `s i < s j` show ?thesis by simp |
|
116 qed |
|
117 qed (simp add:increasing_strict) |
|
118 |
|
119 |
|
120 |
|
121 |
|
122 subsection {* Sections induced by an increasing sequence *} |
|
123 |
|
124 abbreviation |
|
125 "section s i == {s i ..< s (Suc i)}" |
|
126 |
|
127 definition |
|
128 "section_of s n = (LEAST i. n < s (Suc i))" |
|
129 |
|
130 |
|
131 lemma section_help: |
|
132 assumes [intro, simp]: "increasing s" |
|
133 shows "\<exists>i. n < s (Suc i)" |
|
134 proof - |
|
135 from increasing_inc have "n \<le> s n" . |
|
136 also from increasing_strict have "\<dots> < s (Suc n)" by simp |
|
137 finally show ?thesis .. |
|
138 qed |
|
139 |
|
140 lemma section_of2: |
|
141 assumes "increasing s" |
|
142 shows "n < s (Suc (section_of s n))" |
|
143 unfolding section_of_def |
|
144 by (rule LeastI_ex) (rule section_help) |
|
145 |
|
146 |
|
147 lemma section_of1: |
|
148 assumes [simp, intro]: "increasing s" |
|
149 assumes "s i \<le> n" |
|
150 shows "s (section_of s n) \<le> n" |
|
151 proof (rule classical) |
|
152 let ?m = "section_of s n" |
|
153 |
|
154 assume "\<not> ?thesis" |
|
155 hence a: "n < s ?m" by simp |
|
156 |
|
157 have nonzero: "?m \<noteq> 0" |
|
158 proof |
|
159 assume "?m = 0" |
|
160 from increasing_weak have "s 0 \<le> s i" by simp |
|
161 also note `\<dots> \<le> n` |
|
162 finally show False using `?m = 0` `n < s ?m` by simp |
|
163 qed |
|
164 with a have "n < s (Suc (?m - 1))" by simp |
|
165 with Least_le have "?m \<le> ?m - 1" |
|
166 unfolding section_of_def . |
|
167 with nonzero show ?thesis by simp |
|
168 qed |
|
169 |
|
170 lemma section_of_known: |
|
171 assumes [simp]: "increasing s" |
|
172 assumes in_sect: "k \<in> section s i" |
|
173 shows "section_of s k = i" (is "?s = i") |
|
174 proof (rule classical) |
|
175 assume "\<not> ?thesis" |
|
176 |
|
177 hence "?s < i \<or> ?s > i" by arith |
|
178 thus ?thesis |
|
179 proof |
|
180 assume "?s < i" |
|
181 hence "Suc ?s \<le> i" by simp |
|
182 with increasing_weak have "s (Suc ?s) \<le> s i" by simp |
|
183 moreover have "k < s (Suc ?s)" using section_of2 by simp |
|
184 moreover from in_sect have "s i \<le> k" by simp |
|
185 ultimately show ?thesis by simp |
|
186 next |
|
187 assume "i < ?s" hence "Suc i \<le> ?s" by simp |
|
188 with increasing_weak have "s (Suc i) \<le> s ?s" by simp |
|
189 moreover |
|
190 from in_sect have "s i \<le> k" by simp |
|
191 with section_of1 have "s ?s \<le> k" by simp |
|
192 moreover from in_sect have "k < s (Suc i)" by simp |
|
193 ultimately show ?thesis by simp |
|
194 qed |
|
195 qed |
|
196 |
|
197 |
|
198 lemma in_section_of: |
|
199 assumes [simp, intro]: "increasing s" |
|
200 assumes "s i \<le> k" |
|
201 shows "k \<in> section s (section_of s k)" |
|
202 using prems |
|
203 by (auto intro:section_of1 section_of2) |
|
204 |
|
205 |
|
206 end |