1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11theory GraphLangLemmas
12
13imports GraphLang CommonOpsLemmas
14
15begin
16
17definition
18  get_state_function_call :: "(string \<Rightarrow> graph_function option)
19    \<Rightarrow> (next_node \<times> state \<times> string) \<Rightarrow> string option"
20where
21  "get_state_function_call Gamma x \<equiv> case x of (NextNode nn, st, fname) \<Rightarrow>
22        (case Gamma fname of Some gf \<Rightarrow>
23            (case function_graph gf nn of Some (Call _ fname' _ _) \<Rightarrow> Some fname' | _ \<Rightarrow> None)
24          | None \<Rightarrow> None)
25    | _ \<Rightarrow> None"
26
27definition
28  exec_graph_invariant :: "(string \<Rightarrow> graph_function option) \<Rightarrow> string \<Rightarrow> stack \<Rightarrow> bool"
29where
30  "exec_graph_invariant Gamma gf xs = (xs \<noteq> []
31    \<and> (\<forall>frame \<in> set (tl xs). get_state_function_call Gamma frame \<noteq> None)
32    \<and> map (Some o snd o snd) xs = map (get_state_function_call Gamma) (tl xs) @ [Some gf])"
33
34lemma exec_graph_invariant_Cons:
35  "exec_graph_invariant Gamma fname (x # xs) = (if xs = [] then snd (snd x) = fname
36    else (get_state_function_call Gamma (hd xs) = Some (snd (snd x))
37        \<and> exec_graph_invariant Gamma fname xs))"
38  by (cases xs, auto simp add: exec_graph_invariant_def)
39
40lemma exec_step_invariant:
41  "(stack, stack') \<in> exec_graph_step Gamma
42    \<Longrightarrow> exec_graph_invariant Gamma gf stack
43    \<Longrightarrow> exec_graph_invariant Gamma gf stack'"
44  by (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons
45                 get_state_function_call_def
46          split: graph_function.split_asm)
47
48lemma exec_trace_invariant':
49  "tr \<in> exec_trace Gamma gf
50    \<Longrightarrow> (\<forall>stack. tr i = Some stack
51        \<longrightarrow> exec_graph_invariant Gamma gf stack)"
52  apply (induct i)
53   apply (clarsimp simp: exec_trace_def exec_graph_invariant_def)
54   apply (clarsimp split: next_node.split_asm list.split_asm)
55  apply (clarsimp simp: exec_trace_def nat_trace_rel_def)
56  apply (drule_tac x=i in spec, clarsimp)
57  apply (auto elim: exec_step_invariant)
58  done
59
60lemmas exec_trace_invariant = exec_trace_invariant'[rule_format]
61
62lemma exec_trace_Nil:
63  "tr \<in> exec_trace Gamma gf \<Longrightarrow> tr i \<noteq> Some []"
64  apply safe
65  apply (drule(1) exec_trace_invariant)
66  apply (simp add: exec_graph_invariant_def)
67  done
68
69lemma exec_trace_step_cases:
70  assumes exec: "tr \<in> exec_trace Gamma gf"
71  shows "((tr i = None \<and> tr (Suc i) = None))
72        \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None)
73        \<or> (tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma)"
74  using exec exec_trace_Nil[OF exec]
75  apply (clarsimp simp: exec_trace_def nat_trace_rel_def continuing_def Ball_def)
76  apply (drule_tac x=i in spec)+
77  apply (auto split: list.split_asm option.split_asm prod.split_asm next_node.split_asm)[1]
78  done
79
80definition
81  reachable_step :: "(nat \<Rightarrow> node option) \<Rightarrow> (next_node \<times> next_node) set"
82where
83  "reachable_step graph = {(s, t). (case s of NextNode i \<Rightarrow>
84    (case graph i of None \<Rightarrow> False
85        | Some (Cond l r _) \<Rightarrow> (t = l \<or> t = r)
86        | Some (Basic c _) \<Rightarrow> t = c
87        | Some (Call c _ _ _) \<Rightarrow> t = c \<or> t = Err) | _ \<Rightarrow> False)}"
88
89abbreviation
90  "reachable_step' gf \<equiv> reachable_step (function_graph gf)"
91
92lemma exec_trace_None_dom_subset:
93  "tr n = None \<Longrightarrow> tr \<in> exec_trace Gamma f
94    \<Longrightarrow> dom tr \<subseteq> {..< n}"
95  unfolding exec_trace_def
96  by (blast elim: CollectE dest: trace_None_dom_subset)
97
98lemma trace_Some_dom_superset:
99  "tr \<in> nat_trace_rel c R
100    \<Longrightarrow> tr i = Some v
101    \<Longrightarrow> {..i} \<subseteq> dom tr"
102  apply (clarsimp, rule ccontr, clarsimp)
103  apply (drule(1) trace_None_dom_subset)
104  apply auto
105  done
106
107lemma nat_trace_rel_final:
108  "tr \<in> nat_trace_rel c R
109    \<Longrightarrow> tr i = Some v
110    \<Longrightarrow> \<not> c' v
111    \<Longrightarrow> restrict_map tr {.. i} \<in> nat_trace_rel c' R"
112  apply (frule(1) trace_Some_dom_superset)
113  apply (clarsimp simp: nat_trace_rel_def restrict_map_def Suc_le_eq)
114  apply (drule_tac c="Suc n" in subsetD, auto)
115  done
116
117lemma trace_None_dom_eq:
118  "tr n = None \<Longrightarrow> tr \<in> nat_trace_rel cont R
119    \<Longrightarrow> (\<exists>n'. n' \<le> n \<and> dom tr = {..< n'})"
120  apply (cases "\<forall>i. tr i = None")
121   apply (rule_tac x=0 in exI)
122   apply (simp add: fun_eq_iff)
123  apply clarsimp
124  apply (rule_tac x="Suc (Max (dom tr))" in exI)
125  apply (drule(1) nat_trace_Max_dom_None[rotated, simplified, OF exI])
126  apply clarsimp
127  apply (frule(1) trace_None_dom_subset)
128  apply (rule conjI)
129   apply auto[1]
130  apply (rule equalityI)
131   apply (auto simp: less_Suc_eq_le intro!: Max_ge elim: finite_subset)[1]
132  apply (clarsimp, rule ccontr, clarsimp simp: less_Suc_eq_le)
133  apply (drule(1) trace_None_dom_subset)+
134  apply auto
135  done
136
137lemma trace_end_eq_Some:
138  "tr \<in> nat_trace_rel c R
139    \<Longrightarrow> tr i = Some v
140    \<Longrightarrow> tr (Suc i) = None
141    \<Longrightarrow> trace_end tr = Some v"
142  apply (frule(1) trace_Some_dom_superset)
143  apply (frule(1) trace_None_dom_eq)
144  apply (clarsimp simp: le_Suc_eq lessThan_Suc_atMost[symmetric])
145  apply (simp add: trace_end_def)
146  apply (subst Max_eqI[where x=i], simp_all)
147  apply auto
148  done
149
150lemma trace_end_cut:
151  "tr \<in> nat_trace_rel c R
152    \<Longrightarrow> tr i = Some v
153    \<Longrightarrow> trace_end (restrict_map tr {.. i}) = Some v"
154  apply (frule(1) trace_Some_dom_superset)
155  apply (simp add: trace_end_def Int_absorb1)
156  apply (subst Max_eqI[where x=i], simp_all)
157  apply (simp add: restrict_map_def)
158  apply (metis Suc_n_not_le_n)
159  done
160
161definition
162  trace_drop_n :: "nat \<Rightarrow> nat \<Rightarrow> trace \<Rightarrow> trace"
163where
164  "trace_drop_n start n_drop tr = (\<lambda>i. if (\<forall>j < i. tr (start + j) \<noteq> None
165        \<and> continuing (rev (drop n_drop (rev (the (tr (start + j)))))))
166    then option_map (rev o drop n_drop o rev) (tr (i + start)) else None)"
167
168lemma rev_drop_step:
169  "(stack, stack') \<in> exec_graph_step Gamma
170    \<Longrightarrow> continuing (rev (drop k (rev stack)))
171    \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma"
172  apply (subgoal_tac "\<exists>xs ys. stack = xs @ ys \<and> k = length ys")
173   apply clarsimp
174   apply (frule(1) exec_graph_step_stack_extend[THEN iffD1])
175   apply clarsimp
176  apply (rule_tac x="take (length stack - k) stack" in exI)
177  apply (rule_tac x="drop (length stack - k) stack" in exI)
178  apply (cases "length (rev (drop k (rev stack)))")
179   apply simp
180  apply simp
181  done
182
183lemma rev_drop_continuing:
184  "continuing (rev (drop k (rev stack))) \<Longrightarrow> continuing stack"
185  by (simp add: continuing_def split: list.split next_node.split,
186      auto simp: drop_Cons split: nat.split_asm)
187
188lemma all_less_Suc_eq:
189  "(\<forall>x < Suc i. P x) = (P i \<and> (\<forall>x < i. P x))"
190  by (auto simp: less_Suc_eq)
191
192lemma exec_trace_drop_n_Cons:
193  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn'' = Some gf"
194  shows "tr i = Some ((NextNode n, st, fn'') # xs)
195    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
196    \<Longrightarrow> Gamma fn' = Some gf'
197    \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn'"
198  using tr
199  apply (clarsimp simp: exec_trace_def)
200  apply (intro conjI)
201   apply (simp add: trace_drop_n_def)
202   apply (cut_tac exec_trace_step_cases[where i=i, OF tr(1)])
203   apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons
204                  split: graph_function.split_asm)
205  apply (clarsimp simp: nat_trace_rel_def trace_drop_n_def
206                        all_less_Suc_eq
207             split del: if_split)
208  apply (cut_tac i="Suc i + na" in exec_trace_Nil[OF tr(1)])
209  apply (drule_tac x="Suc i + na" in spec)+
210  apply (clarsimp simp: field_simps)
211  apply (safe, simp_all)
212  apply (safe intro!: rev_drop_step)
213  apply (auto dest!: rev_drop_continuing)
214  done
215
216lemma exec_trace_drop_n:
217  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf"
218  shows "tr i = Some [(NextNode n, st, fn'')]
219    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
220    \<Longrightarrow> Gamma fn' = Some gf'
221    \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn'"
222  apply (frule exec_trace_invariant[OF tr(1)])
223  apply (simp add: exec_graph_invariant_Cons)
224  apply (drule(2) exec_trace_drop_n_Cons[OF tr])
225  apply simp
226  done
227
228lemma exec_trace_drop_n_rest_Cons:
229  "tr \<in> exec_trace Gamma fn
230    \<Longrightarrow> tr i = Some ((NextNode n, st, fn'') # xs)
231    \<Longrightarrow> Gamma fn'' = Some gf
232    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
233    \<Longrightarrow> Gamma fn' = Some gf'
234    \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk
235     \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs))"
236proof (induct k)
237  case 0 show ?case using 0
238    apply (clarsimp simp: trace_drop_n_def)
239    apply (frule_tac i=i in exec_trace_step_cases)
240    apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons
241                   split: graph_function.split_asm)
242    done
243next
244  case (Suc k)
245  have rev_drop_eq: "\<And>xs ys n. length ys = n
246    \<Longrightarrow> (xs = rev (drop n (rev xs)) @ ys)
247        = (\<exists>zs. xs = zs @ ys)"
248    by auto
249  show ?case using Suc.prems Suc.hyps
250    apply (clarsimp simp: trace_drop_n_def field_simps)
251    apply (frule_tac i="Suc k + i" in exec_trace_step_cases)
252    apply (clarsimp simp: field_simps all_less_Suc_eq rev_drop_eq)
253    apply (clarsimp simp: exec_graph_step_stack_extend)
254    done
255qed
256
257lemma exec_trace_drop_n_rest:
258  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
259    \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')]
260    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
261    \<Longrightarrow> Gamma fn' = Some gf'
262    \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk
263     \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]))"
264  apply (frule(1) exec_trace_invariant)
265  apply (clarsimp simp: exec_graph_invariant_Cons)
266  apply (drule(4) exec_trace_drop_n_rest_Cons)
267  apply auto
268  done
269
270lemma trace_drop_n_init:
271  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
272    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
273    \<Longrightarrow> Gamma fname = Some f'
274    \<Longrightarrow> tr i = Some [(NextNode n, st, fn')]
275    \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'),
276            init_vars (function_inputs f') inputs st, fname)]"
277  apply (frule(1) exec_trace_invariant)
278  apply (clarsimp simp: exec_graph_invariant_Cons)
279  apply (frule_tac i=i in exec_trace_step_cases, clarsimp)
280  apply (clarsimp simp: all_exec_graph_step_cases trace_drop_n_def)
281  done
282
283lemma exec_trace_init:
284  "tr \<in> exec_trace Gamma fn
285   \<Longrightarrow> \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]"
286  by (clarsimp simp: exec_trace_def)
287
288lemma dom_Max_None:
289  "tr \<in> exec_trace Gamma f \<Longrightarrow> (tr (Max (dom tr)) \<noteq> None)"
290  apply (rule notI)
291  apply (frule(1) exec_trace_None_dom_subset)
292  apply (cases "dom tr = {}")
293   apply (clarsimp dest!: exec_trace_init)
294  apply (drule Max_in[rotated])
295   apply (simp add: finite_subset)
296  apply clarsimp
297  done
298
299lemma trace_end_trace_drop_n_None:
300  "trace_end (trace_drop_n i j tr) = None \<Longrightarrow> tr \<in> exec_trace Gamma f
301    \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f'
302    \<Longrightarrow> trace_end tr = None"
303  apply (clarsimp simp: trace_end_def dom_Max_None split: if_split_asm)
304  apply (rule ccontr, simp)
305  apply (drule(1) exec_trace_None_dom_subset)
306  apply (drule_tac x="n + i + 1" in spec)
307  apply (clarsimp simp: trace_drop_n_def split: if_split_asm)
308  apply auto[1]
309  done
310
311lemma trace_end_trace_drop_n_Some:
312  "trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)]
313    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
314    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
315    \<Longrightarrow> Gamma fname = Some f'
316    \<Longrightarrow> tr i = Some [(NextNode n, st, fn')]
317    \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)]
318"
319  apply (frule(4) exec_trace_drop_n)
320  apply (drule trace_end_SomeD, fastforce simp add: exec_trace_def)
321  apply clarsimp
322  apply (frule(4) exec_trace_drop_n_rest, simp, drule spec, drule(1) mp)
323  apply simp
324  apply (frule(1) exec_trace_invariant[where stack="[a, b]" for a b])
325  apply (clarsimp simp: exec_graph_invariant_Cons get_state_function_call_def)
326  apply (frule_tac i="Suc i + na" in exec_trace_step_cases, clarsimp)
327  apply (clarsimp simp: all_exec_graph_step_cases)
328  apply (metis add_Suc_right)
329  done
330
331end
332