theory GraphLangLemmas

lemma exec_trace_drop_n_rest_Cons:
  "tr \<in> exec_trace Gamma fn
    \<Longrightarrow> tr i = Some ((NextNode n, st, fn'') # xs)
    \<Longrightarrow> Gamma fn'' = Some gf
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk
     \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs))" proof (induct k) case 0 show ?case using 0 apply (clarsimp simp: trace_drop_n_def) apply (frule_tac i=i in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons
                   split: graph_function.split_asm) done next case (Suc k) have rev_drop_eq: "\<And>xs ys n. length ys = n
    \<Longrightarrow> (xs = rev (drop n (rev xs)) @ ys)
        = (\<exists>zs. xs = zs @ ys)" by auto show ?case using Suc.prems Suc.hyps apply (clarsimp simp: trace_drop_n_def field_simps) apply (frule_tac i="Suc k + i" in exec_trace_step_cases) apply (clarsimp simp: field_simps all_less_Suc_eq rev_drop_eq) apply (clarsimp simp: exec_graph_step_stack_extend) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (state)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some stk \<longrightarrow> tr (Suc i + 0) = Some (stk @ (NextNode n, st, fn'') # xs)
 2. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (state)
this:
tr \<in> exec_trace Gamma fn
tr i = Some ((NextNode n, st, fn'') # xs)
Gamma fn'' = Some gf
function_graph gf n = Some (node.Call nn fn' inps outps)
Gamma fn' = Some gf'

goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some stk \<longrightarrow> tr (Suc i + 0) = Some (stk @ (NextNode n, st, fn'') # xs)
 2. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
goal (1 subgoal):
 1. \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some stk \<longrightarrow> tr (Suc i + 0) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
using this:
tr \<in> exec_trace Gamma fn
tr i = Some ((NextNode n, st, fn'') # xs)
Gamma fn'' = Some gf
function_graph gf n = Some (node.Call nn fn' inps outps)
Gamma fn' = Some gf'

goal (1 subgoal):
 1. \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some stk \<longrightarrow> tr (Suc i + 0) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr (Suc i) = Some z\<rbrakk> \<Longrightarrow> z = rev (drop (Suc (length xs)) (rev z)) @ (NextNode n, st, fn'') # xs proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr (Suc i) = Some z; tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> z = rev (drop (Suc (length xs)) (rev z)) @ (NextNode n, st, fn'') # xs proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr 0 = Some stk \<longrightarrow> tr (Suc i + 0) = Some (stk @ (NextNode n, st, fn'') # xs)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (state)
this:
\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs)
tr \<in> exec_trace Gamma fn
tr i = Some ((NextNode n, st, fn'') # xs)
Gamma fn'' = Some gf
function_graph gf n = Some (node.Call nn fn' inps outps)
Gamma fn' = Some gf'

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys n. length ys = n \<Longrightarrow> (xs = rev (drop n (rev xs)) @ ys) = (\<exists>zs. xs = zs @ ys) proof (state)
this:
length ?ys = ?n \<Longrightarrow> (?xs = rev (drop ?n (rev ?xs)) @ ?ys) = (\<exists>zs. ?xs = zs @ ?ys)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs); tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
goal (1 subgoal):
 1. \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
using this:
tr \<in> exec_trace Gamma fn
tr i = Some ((NextNode n, st, fn'') # xs)
Gamma fn'' = Some gf
function_graph gf n = Some (node.Call nn fn' inps outps)
Gamma fn' = Some gf'
\<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs)

goal (1 subgoal):
 1. \<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs) proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; \<forall>stk. (\<exists>z. tr (Suc (i + k)) = Some z \<and> rev (drop (Suc (length xs)) (rev z)) = stk) \<longrightarrow> tr (Suc (i + k)) = Some (stk @ (NextNode n, st, fn'') # xs); \<forall>j<Suc k. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (Suc (i + k))) = Some z\<rbrakk> \<Longrightarrow> z = rev (drop (Suc (length xs)) (rev z)) @ (NextNode n, st, fn'') # xs proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; \<forall>stk. (\<exists>z. tr (Suc (i + k)) = Some z \<and> rev (drop (Suc (length xs)) (rev z)) = stk) \<longrightarrow> tr (Suc (i + k)) = Some (stk @ (NextNode n, st, fn'') # xs); \<forall>j<Suc k. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i))))))); tr (Suc (Suc (i + k))) = Some z; tr (Suc k + i) = None \<and> tr (Suc (Suc k + i)) = None \<or> (\<exists>state. tr (Suc k + i) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc k + i)) = None) \<or> tr (Suc k + i) \<noteq> None \<and> tr (Suc (Suc k + i)) \<noteq> None \<and> (the (tr (Suc k + i)), the (tr (Suc (Suc k + i)))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> z = rev (drop (Suc (length xs)) (rev z)) @ (NextNode n, st, fn'') # xs proof (prove)
goal (1 subgoal):
 1. \<And>z zs. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some ((NextNode n, st, fn'') # xs); Gamma fn'' = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr (Suc (Suc (i + k))) = Some z; (zs @ (NextNode n, st, fn'') # xs, z) \<in> exec_graph_step Gamma; tr (Suc (i + k)) = Some (zs @ (NextNode n, st, fn'') # xs); continuing zs; \<forall>j<k. (\<exists>y. tr (Suc (j + i)) = Some y) \<and> continuing (rev (drop (Suc (length xs)) (rev (the (tr (Suc (j + i)))))))\<rbrakk> \<Longrightarrow> \<exists>zs. z = zs @ (NextNode n, st, fn'') # xs proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr (Suc k) = Some stk \<longrightarrow> tr (Suc i + Suc k) = Some (stk @ (NextNode n, st, fn'') # xs)

goal:
No subgoals!