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