|
1 theory Happen_within |
|
2 imports Main Moment |
|
3 begin |
|
4 |
|
5 (* |
|
6 lemma |
|
7 fixes P :: "('a list) \<Rightarrow> bool" |
|
8 and Q :: "('a list) \<Rightarrow> bool" |
|
9 and k :: nat |
|
10 and f :: "('a list) \<Rightarrow> nat" |
|
11 assumes "\<And> s t. \<lbrakk>P s; \<not> Q s; P (t@s); k < length t\<rbrakk> \<Longrightarrow> f (t@s) < f s" |
|
12 shows "\<And> s t. \<lbrakk> P s; P(t @ s); f(s) * k < length t\<rbrakk> \<Longrightarrow> Q (t@s)" |
|
13 sorry |
|
14 *) |
|
15 |
|
16 text {* |
|
17 The following two notions are introduced to improve the situation. |
|
18 *} |
|
19 |
|
20 definition all_future :: "(('a list) \<Rightarrow> bool) \<Rightarrow> (('a list) \<Rightarrow> bool) \<Rightarrow> ('a list) \<Rightarrow> bool" |
|
21 where "all_future G R s = (\<forall> t. G (t@s) \<longrightarrow> R t)" |
|
22 |
|
23 definition happen_within :: "(('a list) \<Rightarrow> bool) \<Rightarrow> (('a list) \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> ('a list) \<Rightarrow> bool" |
|
24 where "happen_within G R k s = all_future G (\<lambda> t. k < length t \<longrightarrow> |
|
25 (\<exists> i \<le> k. R (moment i t @ s) \<and> G (moment i t @ s))) s" |
|
26 |
|
27 lemma happen_within_intro: |
|
28 fixes P :: "('a list) \<Rightarrow> bool" |
|
29 and Q :: "('a list) \<Rightarrow> bool" |
|
30 and k :: nat |
|
31 and f :: "('a list) \<Rightarrow> nat" |
|
32 assumes |
|
33 lt_k: "0 < k" |
|
34 and step: "\<And> s. \<lbrakk>P s; \<not> Q s\<rbrakk> \<Longrightarrow> happen_within P (\<lambda> s'. f s' < f s) k s" |
|
35 shows "\<And> s. P s \<Longrightarrow> happen_within P Q ((f s + 1) * k) s" |
|
36 proof - |
|
37 fix s |
|
38 assume "P s" |
|
39 thus "happen_within P Q ((f s + 1) * k) s" |
|
40 proof(induct n == "f s + 1" arbitrary:s rule:nat_less_induct) |
|
41 fix s |
|
42 assume ih [rule_format]: "\<forall>m<f s + 1. \<forall>x. m = f x + 1 \<longrightarrow> P x |
|
43 \<longrightarrow> happen_within P Q ((f x + 1) * k) x" |
|
44 and ps: "P s" |
|
45 show "happen_within P Q ((f s + 1) * k) s" |
|
46 proof(cases "Q s") |
|
47 case True |
|
48 show ?thesis |
|
49 proof - |
|
50 { fix t |
|
51 from True and ps have "0 \<le> ((f s + 1)*k) \<and> Q (moment 0 t @ s) \<and> P (moment 0 t @ s)" by auto |
|
52 hence "\<exists>i\<le>(f s + 1) * k. Q (moment i t @ s) \<and> P (moment i t @ s)" by auto |
|
53 } thus ?thesis by (auto simp: happen_within_def all_future_def) |
|
54 qed |
|
55 next |
|
56 case False |
|
57 from step [OF ps False] have kk: "happen_within P (\<lambda>s'. f s' < f s) k s" . |
|
58 show ?thesis |
|
59 proof - |
|
60 { fix t |
|
61 assume pts: "P (t @ s)" and ltk: "(f s + 1) * k < length t" |
|
62 from ltk have lt_k_lt: "k < length t" by auto |
|
63 with kk pts obtain i |
|
64 where le_ik: "i \<le> k" |
|
65 and lt_f: "f (moment i t @ s) < f s" |
|
66 and p_m: "P (moment i t @ s)" |
|
67 by (auto simp:happen_within_def all_future_def) |
|
68 from ih [of "f (moment i t @ s) + 1" "(moment i t @ s)", OF _ _ p_m] and lt_f |
|
69 have hw: "happen_within P Q ((f (moment i t @ s) + 1) * k) (moment i t @ s)" by auto |
|
70 have "(\<exists>j\<le>(f s + 1) * k. Q (moment j t @ s) \<and> P (moment j t @ s))" (is "\<exists> j. ?T j") |
|
71 proof - |
|
72 let ?t = "restm i t" |
|
73 have eq_t: "t = ?t @ moment i t" by (simp add:moment_restm_s) |
|
74 have h1: "P (restm i t @ moment i t @ s)" |
|
75 proof - |
|
76 from pts and eq_t have "P ((restm i t @ moment i t) @ s)" by simp |
|
77 thus ?thesis by simp |
|
78 qed |
|
79 moreover have h2: "(f (moment i t @ s) + 1) * k < length (restm i t)" |
|
80 proof - |
|
81 have h: "\<And> x y z. (x::nat) \<le> y \<Longrightarrow> x * z \<le> y * z" by simp |
|
82 from lt_f have "(f (moment i t @ s) + 1) \<le> f s " by simp |
|
83 from h [OF this, of k] |
|
84 have "(f (moment i t @ s) + 1) * k \<le> f s * k" . |
|
85 moreover from le_ik have "\<dots> \<le> ((f s) * k + k - i)" by simp |
|
86 moreover from le_ik lt_k_lt and ltk have "(f s) * k + k - i < length t - i" by simp |
|
87 moreover have "length (restm i t) = length t - i" using length_restm by metis |
|
88 ultimately show ?thesis by simp |
|
89 qed |
|
90 from hw [unfolded happen_within_def all_future_def, rule_format, OF h1 h2] |
|
91 obtain m where le_m: "m \<le> (f (moment i t @ s) + 1) * k" |
|
92 and q_m: "Q (moment m ?t @ moment i t @ s)" |
|
93 and p_m: "P (moment m ?t @ moment i t @ s)" by auto |
|
94 have eq_mm: "moment m ?t @ moment i t @ s = (moment (m+i) t)@s" |
|
95 proof - |
|
96 have "moment m (restm i t) @ moment i t = moment (m + i) t" |
|
97 using moment_plus_split by metis |
|
98 thus ?thesis by simp |
|
99 qed |
|
100 let ?j = "m + i" |
|
101 have "?T ?j" |
|
102 proof - |
|
103 have "m + i \<le> (f s + 1) * k" |
|
104 proof - |
|
105 have h: "\<And> x y z. (x::nat) \<le> y \<Longrightarrow> x * z \<le> y * z" by simp |
|
106 from lt_f have "(f (moment i t @ s) + 1) \<le> f s " by simp |
|
107 from h [OF this, of k] |
|
108 have "(f (moment i t @ s) + 1) * k \<le> f s * k" . |
|
109 with le_m have "m \<le> f s * k" by simp |
|
110 hence "m + i \<le> f s * k + i" by simp |
|
111 with le_ik show ?thesis by simp |
|
112 qed |
|
113 moreover from eq_mm q_m have " Q (moment (m + i) t @ s)" by metis |
|
114 moreover from eq_mm p_m have " P (moment (m + i) t @ s)" by metis |
|
115 ultimately show ?thesis by blast |
|
116 qed |
|
117 thus ?thesis by blast |
|
118 qed |
|
119 } thus ?thesis by (simp add:happen_within_def all_future_def firstn.simps) |
|
120 qed |
|
121 qed |
|
122 qed |
|
123 qed |
|
124 |
|
125 end |
|
126 |