|
1 theory Moment |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
6 where "moment n s = rev (take n (rev s))" |
|
7 |
|
8 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
|
9 value "moment 2 [5, 4, 3, 2, 1, 0::int]" |
|
10 |
|
11 (* |
|
12 lemma length_moment_le: |
|
13 assumes le_k: "k \<le> length s" |
|
14 shows "length (moment k s) = k" |
|
15 using le_k unfolding moment_def by auto |
|
16 *) |
|
17 |
|
18 (* |
|
19 lemma length_moment_ge: |
|
20 assumes le_k: "length s \<le> k" |
|
21 shows "length (moment k s) = (length s)" |
|
22 using assms unfolding moment_def by simp |
|
23 *) |
|
24 |
|
25 lemma moment_app [simp]: |
|
26 assumes ile: "i \<le> length s" |
|
27 shows "moment i (s' @ s) = moment i s" |
|
28 using assms unfolding moment_def by simp |
|
29 |
|
30 lemma moment_eq [simp]: "moment (length s) (s' @ s) = s" |
|
31 unfolding moment_def by simp |
|
32 |
|
33 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
|
34 by (unfold moment_def, simp) |
|
35 |
|
36 lemma moment_zero [simp]: "moment 0 s = []" |
|
37 by (simp add:moment_def) |
|
38 |
|
39 lemma p_split_gen: |
|
40 "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow> |
|
41 (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
42 proof (induct s, simp) |
|
43 fix a s |
|
44 assume ih: "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> |
|
45 \<Longrightarrow> \<exists>i<length s. k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall>i'>i. Q (moment i' s))" |
|
46 and nq: "\<not> Q (moment k (a # s))" and qa: "Q (a # s)" |
|
47 have le_k: "k \<le> length s" |
|
48 proof - |
|
49 { assume "length s < k" |
|
50 hence "length (a#s) \<le> k" by simp |
|
51 from moment_ge [OF this] and nq and qa |
|
52 have "False" by auto |
|
53 } thus ?thesis by arith |
|
54 qed |
|
55 have nq_k: "\<not> Q (moment k s)" |
|
56 proof - |
|
57 have "moment k (a#s) = moment k s" |
|
58 proof - |
|
59 from moment_app [OF le_k, of "[a]"] show ?thesis by simp |
|
60 qed |
|
61 with nq show ?thesis by simp |
|
62 qed |
|
63 show "\<exists>i<length (a # s). k \<le> i \<and> \<not> Q (moment i (a # s)) \<and> (\<forall>i'>i. Q (moment i' (a # s)))" |
|
64 proof - |
|
65 { assume "Q s" |
|
66 from ih [OF this nq_k] |
|
67 obtain i where lti: "i < length s" |
|
68 and nq: "\<not> Q (moment i s)" |
|
69 and rst: "\<forall>i'>i. Q (moment i' s)" |
|
70 and lki: "k \<le> i" by auto |
|
71 have ?thesis |
|
72 proof - |
|
73 from lti have "i < length (a # s)" by auto |
|
74 moreover have " \<not> Q (moment i (a # s))" |
|
75 proof - |
|
76 from lti have "i \<le> (length s)" by simp |
|
77 from moment_app [OF this, of "[a]"] |
|
78 have "moment i (a # s) = moment i s" by simp |
|
79 with nq show ?thesis by auto |
|
80 qed |
|
81 moreover have " (\<forall>i'>i. Q (moment i' (a # s)))" |
|
82 proof - |
|
83 { |
|
84 fix i' |
|
85 assume lti': "i < i'" |
|
86 have "Q (moment i' (a # s))" |
|
87 proof(cases "length (a#s) \<le> i'") |
|
88 case True |
|
89 from True have "moment i' (a#s) = a#s" by simp |
|
90 with qa show ?thesis by simp |
|
91 next |
|
92 case False |
|
93 from False have "i' \<le> length s" by simp |
|
94 from moment_app [OF this, of "[a]"] |
|
95 have "moment i' (a#s) = moment i' s" by simp |
|
96 with rst lti' show ?thesis by auto |
|
97 qed |
|
98 } thus ?thesis by auto |
|
99 qed |
|
100 moreover note lki |
|
101 ultimately show ?thesis by auto |
|
102 qed |
|
103 } moreover { |
|
104 assume ns: "\<not> Q s" |
|
105 have ?thesis |
|
106 proof - |
|
107 let ?i = "length s" |
|
108 have "\<not> Q (moment ?i (a#s))" |
|
109 proof - |
|
110 have "?i \<le> length s" by simp |
|
111 from moment_app [OF this, of "[a]"] |
|
112 have "moment ?i (a#s) = moment ?i s" by simp |
|
113 moreover have "\<dots> = s" by simp |
|
114 ultimately show ?thesis using ns by auto |
|
115 qed |
|
116 moreover have "\<forall> i' > ?i. Q (moment i' (a#s))" |
|
117 proof - |
|
118 { fix i' |
|
119 assume "i' > ?i" |
|
120 hence "length (a#s) \<le> i'" by simp |
|
121 from moment_ge [OF this] |
|
122 have " moment i' (a # s) = a # s" . |
|
123 with qa have "Q (moment i' (a#s))" by simp |
|
124 } thus ?thesis by auto |
|
125 qed |
|
126 moreover have "?i < length (a#s)" by simp |
|
127 moreover note le_k |
|
128 ultimately show ?thesis by auto |
|
129 qed |
|
130 } ultimately show ?thesis by auto |
|
131 qed |
|
132 qed |
|
133 |
|
134 lemma p_split: |
|
135 "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> |
|
136 (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
137 proof - |
|
138 fix s Q |
|
139 assume qs: "Q s" and nq: "\<not> Q []" |
|
140 from nq have "\<not> Q (moment 0 s)" by simp |
|
141 from p_split_gen [of Q s 0, OF qs this] |
|
142 show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
143 by auto |
|
144 qed |
|
145 |
|
146 lemma moment_Suc_tl: |
|
147 assumes "Suc i \<le> length s" |
|
148 shows "tl (moment (Suc i) s) = moment i s" |
|
149 using assms unfolding moment_def rev_take |
|
150 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
|
151 |
|
152 lemma moment_plus: |
|
153 assumes "Suc i \<le> length s" |
|
154 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
|
155 proof - |
|
156 have "(moment (Suc i) s) \<noteq> []" |
|
157 using assms by (auto simp add: moment_def) |
|
158 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
|
159 by auto |
|
160 <<<<<<< local |
|
161 have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" |
|
162 by (simp add: moment_def) |
|
163 with moment_app show ?thesis by auto |
|
164 qed |
|
165 |
|
166 lemma moment_Suc_tl: |
|
167 assumes "Suc i \<le> length s" |
|
168 shows "tl (moment (Suc i) s) = moment i s" |
|
169 using assms unfolding moment_def rev_take |
|
170 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
|
171 |
|
172 lemma moment_plus': |
|
173 assumes "Suc i \<le> length s" |
|
174 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
|
175 proof - |
|
176 have "(moment (Suc i) s) \<noteq> []" |
|
177 using assms length_moment_le by fastforce |
|
178 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
|
179 by auto |
|
180 with moment_Suc_tl[OF assms] |
|
181 show ?thesis by metis |
|
182 qed |
|
183 |
|
184 lemma moment_plus: |
|
185 "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" |
|
186 proof(induct s, simp+) |
|
187 fix a s |
|
188 assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s" |
|
189 and le_i: "i \<le> length s" |
|
190 show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)" |
|
191 proof(cases "i= length s") |
|
192 case True |
|
193 hence "Suc i = length (a#s)" by simp |
|
194 with moment_eq have "moment (Suc i) (a#s) = a#s" by auto |
|
195 moreover have "moment i (a#s) = s" |
|
196 proof - |
|
197 from moment_app [OF le_i, of "[a]"] |
|
198 and True show ?thesis by simp |
|
199 qed |
|
200 ultimately show ?thesis by auto |
|
201 next |
|
202 case False |
|
203 from False and le_i have lti: "i < length s" by arith |
|
204 hence les_i: "Suc i \<le> length s" by arith |
|
205 show ?thesis |
|
206 proof - |
|
207 from moment_app [OF les_i, of "[a]"] |
|
208 have "moment (Suc i) (a # s) = moment (Suc i) s" by simp |
|
209 moreover have "moment i (a#s) = moment i s" |
|
210 proof - |
|
211 from lti have "i \<le> length s" by simp |
|
212 from moment_app [OF this, of "[a]"] show ?thesis by simp |
|
213 qed |
|
214 moreover note ih [OF les_i] |
|
215 ultimately show ?thesis by auto |
|
216 qed |
|
217 qed |
|
218 ======= |
|
219 with moment_Suc_tl[OF assms] |
|
220 show ?thesis by metis |
|
221 >>>>>>> other |
|
222 qed |
|
223 |
|
224 end |
|
225 |