1(*  Title:      HOL/HOLCF/IOA/ShortExecutions.thy
2    Author:     Olaf M��ller
3*)
4
5theory ShortExecutions
6imports Traces
7begin
8
9text \<open>
10  Some properties about \<open>Cut ex\<close>, defined as follows:
11
12  For every execution ex there is another shorter execution \<open>Cut ex\<close>
13  that has the same trace as ex, but its schedule ends with an external action.
14\<close>
15
16definition oraclebuild :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq \<rightarrow> 'a Seq"
17  where "oraclebuild P =
18    (fix \<cdot>
19      (LAM h s t.
20        case t of
21          nil \<Rightarrow> nil
22        | x ## xs \<Rightarrow>
23            (case x of
24              UU \<Rightarrow> UU
25            | Def y \<Rightarrow>
26                (Takewhile (\<lambda>x. \<not> P x) \<cdot> s) @@
27                (y \<leadsto> (h \<cdot> (TL \<cdot> (Dropwhile (\<lambda>x. \<not> P x) \<cdot> s)) \<cdot> xs)))))"
28
29definition Cut :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> 'a Seq"
30  where "Cut P s = oraclebuild P \<cdot> s \<cdot> (Filter P \<cdot> s)"
31
32definition LastActExtsch :: "('a,'s) ioa \<Rightarrow> 'a Seq \<Rightarrow> bool"
33  where "LastActExtsch A sch \<longleftrightarrow> Cut (\<lambda>x. x \<in> ext A) sch = sch"
34
35axiomatization where
36  Cut_prefixcl_Finite: "Finite s \<Longrightarrow> \<exists>y. s = Cut P s @@ y"
37
38axiomatization where
39  LastActExtsmall1: "LastActExtsch A sch \<Longrightarrow> LastActExtsch A (TL \<cdot> (Dropwhile P \<cdot> sch))"
40
41axiomatization where
42  LastActExtsmall2: "Finite sch1 \<Longrightarrow> LastActExtsch A (sch1 @@ sch2) \<Longrightarrow> LastActExtsch A sch2"
43
44ML \<open>
45fun thin_tac' ctxt j =
46  rotate_tac (j - 1) THEN'
47  eresolve_tac ctxt [thin_rl] THEN'
48  rotate_tac (~ (j - 1))
49\<close>
50
51
52subsection \<open>\<open>oraclebuild\<close> rewrite rules\<close>
53
54lemma oraclebuild_unfold:
55  "oraclebuild P =
56    (LAM s t.
57      case t of
58        nil \<Rightarrow> nil
59      | x ## xs \<Rightarrow>
60          (case x of
61            UU \<Rightarrow> UU
62          | Def y \<Rightarrow>
63            (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@
64            (y \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> xs))))"
65  apply (rule trans)
66  apply (rule fix_eq2)
67  apply (simp only: oraclebuild_def)
68  apply (rule beta_cfun)
69  apply simp
70  done
71
72lemma oraclebuild_UU: "oraclebuild P \<cdot> sch \<cdot> UU = UU"
73  apply (subst oraclebuild_unfold)
74  apply simp
75  done
76
77lemma oraclebuild_nil: "oraclebuild P \<cdot> sch \<cdot> nil = nil"
78  apply (subst oraclebuild_unfold)
79  apply simp
80  done
81
82lemma oraclebuild_cons:
83  "oraclebuild P \<cdot> s \<cdot> (x \<leadsto> t) =
84    (Takewhile (\<lambda>a. \<not> P a) \<cdot> s) @@
85    (x \<leadsto> (oraclebuild P \<cdot> (TL \<cdot> (Dropwhile (\<lambda>a. \<not> P a) \<cdot> s)) \<cdot> t))"
86  apply (rule trans)
87  apply (subst oraclebuild_unfold)
88  apply (simp add: Consq_def)
89  apply (simp add: Consq_def)
90  done
91
92
93subsection \<open>Cut rewrite rules\<close>
94
95lemma Cut_nil: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> Finite s \<Longrightarrow> Cut P s = nil"
96  apply (unfold Cut_def)
97  apply (subgoal_tac "Filter P \<cdot> s = nil")
98  apply (simp add: oraclebuild_nil)
99  apply (rule ForallQFilterPnil)
100  apply assumption+
101  done
102
103lemma Cut_UU: "Forall (\<lambda>a. \<not> P a) s \<Longrightarrow> \<not> Finite s \<Longrightarrow> Cut P s = UU"
104  apply (unfold Cut_def)
105  apply (subgoal_tac "Filter P \<cdot> s = UU")
106  apply (simp add: oraclebuild_UU)
107  apply (rule ForallQFilterPUU)
108  apply assumption+
109  done
110
111lemma Cut_Cons:
112  "P t \<Longrightarrow> Forall (\<lambda>x. \<not> P x) ss \<Longrightarrow> Finite ss \<Longrightarrow>
113    Cut P (ss @@ (t \<leadsto> rs)) = ss @@ (t \<leadsto> Cut P rs)"
114  apply (unfold Cut_def)
115  apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
116  done
117
118
119subsection \<open>Cut lemmas for main theorem\<close>
120
121lemma FilterCut: "Filter P \<cdot> s = Filter P \<cdot> (Cut P s)"
122  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
123  prefer 3
124  apply fast
125  apply (case_tac "Finite s")
126  apply (simp add: Cut_nil ForallQFilterPnil)
127  apply (simp add: Cut_UU ForallQFilterPUU)
128  text \<open>main case\<close>
129  apply (simp add: Cut_Cons ForallQFilterPnil)
130  done
131
132lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
133  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P x" and x1 = "s" in
134    take_lemma_less_induct [THEN mp])
135  prefer 3
136  apply fast
137  apply (case_tac "Finite s")
138  apply (simp add: Cut_nil ForallQFilterPnil)
139  apply (simp add: Cut_UU ForallQFilterPUU)
140  text \<open>main case\<close>
141  apply (simp add: Cut_Cons ForallQFilterPnil)
142  apply (rule take_reduction)
143  apply auto
144  done
145
146lemma MapCut: "Map f\<cdot>(Cut (P \<circ> f) s) = Cut P (Map f\<cdot>s)"
147  apply (rule_tac A1 = "\<lambda>x. True" and Q1 = "\<lambda>x. \<not> P (f x) " and x1 = "s" in
148    take_lemma_less_induct [THEN mp])
149  prefer 3
150  apply fast
151  apply (case_tac "Finite s")
152  apply (simp add: Cut_nil)
153  apply (rule Cut_nil [symmetric])
154  apply (simp add: ForallMap o_def)
155  apply (simp add: Map2Finite)
156  text \<open>case \<open>\<not> Finite s\<close>\<close>
157  apply (simp add: Cut_UU)
158  apply (rule Cut_UU)
159  apply (simp add: ForallMap o_def)
160  apply (simp add: Map2Finite)
161  text \<open>main case\<close>
162  apply (simp add: Cut_Cons MapConc ForallMap FiniteMap1 o_def)
163  apply (rule take_reduction)
164  apply auto
165  done
166
167lemma Cut_prefixcl_nFinite [rule_format]: "\<not> Finite s \<longrightarrow> Cut P s \<sqsubseteq> s"
168  apply (intro strip)
169  apply (rule take_lemma_less [THEN iffD1])
170  apply (intro strip)
171  apply (rule mp)
172  prefer 2
173  apply assumption
174  apply (tactic "thin_tac' @{context} 1 1")
175  apply (rule_tac x = "s" in spec)
176  apply (rule nat_less_induct)
177  apply (intro strip)
178  apply (rename_tac na n s)
179  apply (case_tac "Forall (\<lambda>x. \<not> P x) s")
180  apply (rule take_lemma_less [THEN iffD2, THEN spec])
181  apply (simp add: Cut_UU)
182  text \<open>main case\<close>
183  apply (drule divide_Seq3)
184  apply (erule exE)+
185  apply (erule conjE)+
186  apply hypsubst
187  apply (simp add: Cut_Cons)
188  apply (rule take_reduction_less)
189  text \<open>auto makes also reasoning about Finiteness of parts of \<open>s\<close>!\<close>
190  apply auto
191  done
192
193lemma execThruCut: "is_exec_frag A (s, ex) \<Longrightarrow> is_exec_frag A (s, Cut P ex)"
194  apply (case_tac "Finite ex")
195  apply (cut_tac s = "ex" and P = "P" in Cut_prefixcl_Finite)
196  apply assumption
197  apply (erule exE)
198  apply (rule exec_prefix2closed)
199  apply (erule_tac s = "ex" and t = "Cut P ex @@ y" in subst)
200  apply assumption
201  apply (erule exec_prefixclosed)
202  apply (erule Cut_prefixcl_nFinite)
203  done
204
205
206subsection \<open>Main Cut Theorem\<close>
207
208lemma exists_LastActExtsch:
209  "sch \<in> schedules A \<Longrightarrow> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<Longrightarrow>
210    \<exists>sch. sch \<in> schedules A \<and> tr = Filter (\<lambda>a. a \<in> ext A) \<cdot> sch \<and> LastActExtsch A sch"
211  apply (unfold schedules_def has_schedule_def [abs_def])
212  apply auto
213  apply (rule_tac x = "filter_act \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) (snd ex))" in exI)
214  apply (simp add: executions_def)
215  apply (pair ex)
216  apply auto
217  apply (rule_tac x = "(x1, Cut (\<lambda>a. fst a \<in> ext A) x2)" in exI)
218  apply simp
219
220  text \<open>Subgoal 1: Lemma:  propagation of execution through \<open>Cut\<close>\<close>
221  apply (simp add: execThruCut)
222
223  text \<open>Subgoal 2:  Lemma:  \<open>Filter P s = Filter P (Cut P s)\<close>\<close>
224  apply (simp add: filter_act_def)
225  apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)")
226  apply (rule_tac [2] MapCut [unfolded o_def])
227  apply (simp add: FilterCut [symmetric])
228
229  text \<open>Subgoal 3: Lemma: \<open>Cut\<close> idempotent\<close>
230  apply (simp add: LastActExtsch_def filter_act_def)
231  apply (subgoal_tac "Map fst \<cdot> (Cut (\<lambda>a. fst a \<in> ext A) x2) = Cut (\<lambda>a. a \<in> ext A) (Map fst \<cdot> x2)")
232  apply (rule_tac [2] MapCut [unfolded o_def])
233  apply (simp add: Cut_idemp)
234  done
235
236
237subsection \<open>Further Cut lemmas\<close>
238
239lemma LastActExtimplnil: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = nil \<Longrightarrow> sch = nil"
240  apply (unfold LastActExtsch_def)
241  apply (drule FilternPnilForallP)
242  apply (erule conjE)
243  apply (drule Cut_nil)
244  apply assumption
245  apply simp
246  done
247
248lemma LastActExtimplUU: "LastActExtsch A sch \<Longrightarrow> Filter (\<lambda>x. x \<in> ext A) \<cdot> sch = UU \<Longrightarrow> sch = UU"
249  apply (unfold LastActExtsch_def)
250  apply (drule FilternPUUForallP)
251  apply (erule conjE)
252  apply (drule Cut_UU)
253  apply assumption
254  apply simp
255  done
256
257end
258