34 by (unfold moment_def, simp) |
34 by (unfold moment_def, simp) |
35 |
35 |
36 lemma moment_zero [simp]: "moment 0 s = []" |
36 lemma moment_zero [simp]: "moment 0 s = []" |
37 by (simp add:moment_def) |
37 by (simp add:moment_def) |
38 |
38 |
39 lemma p_split_gen: |
39 lemma least_idx: |
40 "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow> |
40 assumes "Q (i::nat)" |
41 (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
41 obtains j where "j \<le> i" "Q j" "\<forall> k < j. \<not> Q k" |
42 proof (induct s, simp) |
42 using assms |
43 fix a s |
43 by (metis ex_least_nat_le le0 not_less0) |
44 assume ih: "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> |
44 |
45 \<Longrightarrow> \<exists>i<length s. k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall>i'>i. Q (moment i' s))" |
45 lemma duration_idx: |
46 and nq: "\<not> Q (moment k (a # s))" and qa: "Q (a # s)" |
46 assumes "\<not> Q (i::nat)" |
47 have le_k: "k \<le> length s" |
47 and "Q j" |
48 proof - |
48 and "i \<le> j" |
49 { assume "length s < k" |
49 obtains k where "i \<le> k" "k < j" "\<not> Q k" "\<forall> i'. k < i' \<and> i' \<le> j \<longrightarrow> Q i'" |
50 hence "length (a#s) \<le> k" by simp |
50 proof - |
51 from moment_ge [OF this] and nq and qa |
51 let ?Q = "\<lambda> t. t \<le> j \<and> \<not> Q (j - t)" |
52 have "False" by auto |
52 have "?Q (j - i)" using assms by (simp add: assms(1)) |
53 } thus ?thesis by arith |
53 from least_idx [of ?Q, OF this] |
54 qed |
54 obtain l |
55 have nq_k: "\<not> Q (moment k s)" |
55 where h: "l \<le> j - i" "\<not> Q (j - l)" "\<forall>k<l. \<not> (k \<le> j \<and> \<not> Q (j - k))" |
56 proof - |
56 by metis |
57 have "moment k (a#s) = moment k s" |
57 let ?k = "j - l" |
58 proof - |
58 have "i \<le> ?k" using assms(3) h(1) by linarith |
59 from moment_app [OF le_k, of "[a]"] show ?thesis by simp |
59 moreover have "?k < j" by (metis assms(2) diff_le_self h(2) le_neq_implies_less) |
60 qed |
60 moreover have "\<not> Q ?k" by (simp add: h(2)) |
61 with nq show ?thesis by simp |
61 moreover have "\<forall> i'. ?k < i' \<and> i' \<le> j \<longrightarrow> Q i'" |
62 qed |
62 by (metis diff_diff_cancel diff_le_self diff_less_mono2 h(3) |
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)))" |
63 less_imp_diff_less not_less) |
64 proof - |
64 ultimately show ?thesis using that by metis |
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 |
65 qed |
133 |
66 |
|
67 lemma p_split_gen: |
|
68 assumes "Q s" |
|
69 and "\<not> Q (moment k s)" |
|
70 shows "(\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
|
71 proof(cases "k \<le> length s") |
|
72 case True |
|
73 let ?Q = "\<lambda> t. Q (moment t s)" |
|
74 have "?Q (length s)" using assms(1) by simp |
|
75 from duration_idx[of ?Q, OF assms(2) this True] |
|
76 obtain i where h: "k \<le> i" "i < length s" "\<not> Q (moment i s)" |
|
77 "\<forall>i'. i < i' \<and> i' \<le> length s \<longrightarrow> Q (moment i' s)" by metis |
|
78 moreover have "(\<forall> i' > i. Q (moment i' s))" using h(4) assms(1) not_less |
|
79 by fastforce |
|
80 ultimately show ?thesis by metis |
|
81 qed (insert assms, auto) |
|
82 |
134 lemma p_split: |
83 lemma p_split: |
135 "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> |
84 assumes qs: "Q s" |
136 (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
85 and nq: "\<not> Q []" |
|
86 shows "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
137 proof - |
87 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 |
88 from nq have "\<not> Q (moment 0 s)" by simp |
141 from p_split_gen [of Q s 0, OF qs this] |
89 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)))" |
90 show ?thesis by auto |
143 by auto |
|
144 qed |
91 qed |
145 |
92 |
146 lemma moment_Suc_tl: |
93 lemma moment_Suc_tl: |
147 assumes "Suc i \<le> length s" |
94 assumes "Suc i \<le> length s" |
148 shows "tl (moment (Suc i) s) = moment i s" |
95 shows "tl (moment (Suc i) s) = moment i s" |
149 using assms unfolding moment_def rev_take |
96 using assms |
150 by (simp, metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
97 by (simp add:moment_def rev_take, |
|
98 metis Suc_diff_le diff_Suc_Suc drop_Suc tl_drop) |
151 |
99 |
152 lemma moment_plus: |
100 lemma moment_plus: |
153 assumes "Suc i \<le> length s" |
101 assumes "Suc i \<le> length s" |
154 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
102 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
155 proof - |
103 proof - |