|
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 lemma moment_app [simp]: |
|
12 assumes ile: "i \<le> length s" |
|
13 shows "moment i (s' @ s) = moment i s" |
|
14 using assms unfolding moment_def by simp |
|
15 |
|
16 lemma moment_eq [simp]: "moment (length s) (s' @ s) = s" |
|
17 unfolding moment_def by simp |
|
18 |
|
19 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
|
20 by (unfold moment_def, simp) |
|
21 |
|
22 lemma moment_zero [simp]: "moment 0 s = []" |
|
23 by (simp add:moment_def) |
|
24 |
|
25 lemma least_idx: |
|
26 assumes "Q (i::nat)" |
|
27 obtains j where "j \<le> i" "Q j" "\<forall> k < j. \<not> Q k" |
|
28 using assms |
|
29 by (metis ex_least_nat_le le0 not_less0) |
|
30 |
|
31 lemma duration_idx: |
|
32 assumes "\<not> Q (i::nat)" |
|
33 and "Q j" |
|
34 and "i \<le> j" |
|
35 obtains k where "i \<le> k" "k < j" "\<not> Q k" "\<forall> i'. k < i' \<and> i' \<le> j \<longrightarrow> Q i'" |
|
36 proof - |
|
37 let ?Q = "\<lambda> t. t \<le> j \<and> \<not> Q (j - t)" |
|
38 have "?Q (j - i)" using assms by (simp add: assms(1)) |
|
39 from least_idx [of ?Q, OF this] |
|
40 obtain l |
|
41 where h: "l \<le> j - i" "\<not> Q (j - l)" "\<forall>k<l. \<not> (k \<le> j \<and> \<not> Q (j - k))" |
|
42 by metis |
|
43 let ?k = "j - l" |
|
44 have "i \<le> ?k" using assms(3) h(1) by linarith |
|
45 moreover have "?k < j" by (metis assms(2) diff_le_self h(2) le_neq_implies_less) |
|
46 moreover have "\<not> Q ?k" by (simp add: h(2)) |
|
47 moreover have "\<forall> i'. ?k < i' \<and> i' \<le> j \<longrightarrow> Q i'" |
|
48 by (metis diff_diff_cancel diff_le_self diff_less_mono2 h(3) |
|
49 less_imp_diff_less not_less) |
|
50 ultimately show ?thesis using that by metis |
|
51 qed |
|
52 |
|
53 lemma p_split_gen: |
|
54 assumes "Q s" |
|
55 and "\<not> Q (moment k s)" |
|
56 shows "(\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
57 proof(cases "k \<le> length s") |
|
58 case True |
|
59 let ?Q = "\<lambda> t. Q (moment t s)" |
|
60 have "?Q (length s)" using assms(1) by simp |
|
61 from duration_idx[of ?Q, OF assms(2) this True] |
|
62 obtain i where h: "k \<le> i" "i < length s" "\<not> Q (moment i s)" |
|
63 "\<forall>i'. i < i' \<and> i' \<le> length s \<longrightarrow> Q (moment i' s)" by metis |
|
64 moreover have "(\<forall> i' > i. Q (moment i' s))" using h(4) assms(1) not_less |
|
65 by fastforce |
|
66 ultimately show ?thesis by metis |
|
67 qed (insert assms, auto) |
|
68 |
|
69 lemma p_split: |
|
70 assumes qs: "Q s" |
|
71 and nq: "\<not> Q []" |
|
72 shows "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
73 proof - |
|
74 from nq have "\<not> Q (moment 0 s)" by simp |
|
75 from p_split_gen [of Q s 0, OF qs this] |
|
76 show ?thesis by auto |
|
77 qed |
|
78 |
|
79 lemma moment_Suc_tl: |
|
80 assumes "Suc i \<le> length s" |
|
81 shows "tl (moment (Suc i) s) = moment i s" |
|
82 using assms |
|
83 by (simp add:moment_def rev_take, |
|
84 metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
|
85 |
|
86 lemma moment_Suc_hd: |
|
87 assumes "Suc i \<le> length s" |
|
88 shows "hd (moment (Suc i) s) = s!(length s - Suc i)" |
|
89 by (simp add:moment_def rev_take, |
|
90 subst hd_drop_conv_nth, insert assms, auto) |
|
91 |
|
92 lemma moment_plus: |
|
93 assumes "Suc i \<le> length s" |
|
94 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
|
95 proof - |
|
96 have "(moment (Suc i) s) \<noteq> []" using assms |
|
97 by (simp add:moment_def rev_take) |
|
98 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
|
99 by auto |
|
100 with moment_Suc_tl[OF assms] |
|
101 show ?thesis by metis |
|
102 qed |
|
103 |
|
104 end |
|
105 |