theory GraphRefine

lemma trace_drop_n_end:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')]
    \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'
    \<Longrightarrow> trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]
    \<Longrightarrow> \<exists>j \<ge> 2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)]" apply (frule trace_end_SomeD, (auto simp: exec_trace_def)[1]) apply clarsimp apply (rename_tac j') apply (drule(4) exec_trace_drop_n_rest[rotated 2, rule_format], simp) apply (frule_tac i="Suc (i + j')" in exec_trace_step_cases) apply (frule(1) exec_trace_invariant) apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_def
                 split: graph_function.split_asm) apply (rule_tac x="Suc (Suc j')" in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; \<exists>n. trace_drop_n (Suc i) (Suc 0) tr n = Some [(Ret, st', fn''')] \<and> trace_drop_n (Suc i) (Suc 0) tr (Suc n) = None \<and> \<not> continuing [(Ret, st', fn''')]\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr na = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc na) = None\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr j' = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc j') = None\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr j' = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc j') = None; tr (Suc i + j') = Some ([(Ret, st', fn''')] @ [(NextNode n, st, fn'')])\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr j' = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc j') = None; tr (Suc i + j') = Some ([(Ret, st', fn''')] @ [(NextNode n, st, fn'')]); tr (Suc (i + j')) = None \<and> tr (Suc (Suc (i + j'))) = None \<or> (\<exists>state. tr (Suc (i + j')) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc (i + j'))) = None) \<or> tr (Suc (i + j')) \<noteq> None \<and> tr (Suc (Suc (i + j'))) \<noteq> None \<and> (the (tr (Suc (i + j'))), the (tr (Suc (Suc (i + j'))))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>j'. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr j' = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc j') = None; tr (Suc i + j') = Some ([(Ret, st', fn''')] @ [(NextNode n, st, fn'')]); tr (Suc (i + j')) = None \<and> tr (Suc (Suc (i + j'))) = None \<or> (\<exists>state. tr (Suc (i + j')) = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc (Suc (i + j'))) = None) \<or> tr (Suc (i + j')) \<noteq> None \<and> tr (Suc (Suc (i + j'))) \<noteq> None \<and> (the (tr (Suc (i + j'))), the (tr (Suc (Suc (i + j'))))) \<in> exec_graph_step Gamma; exec_graph_invariant Gamma fn ([(Ret, st', fn''')] @ [(NextNode n, st, fn'')])\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars (function_outputs gf') outps st' st, fn)] proof (prove)
goal (1 subgoal):
 1. \<And>j' x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); x3 n = Some (node.Call nn fn' inps outps); Gamma fn' = Some (GraphFunction x1a x2a x3a x4a); trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn'; trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr j' = Some [(Ret, st', fn''')]; trace_drop_n (Suc i) (Suc 0) tr (Suc j') = None; tr (Suc (i + j')) = Some [(Ret, st', fn'''), (NextNode n, st, fn)]; fn'' = fn; get_state_function_call Gamma (NextNode n, st, fn) = Some fn'''; gf = GraphFunction x1 x2 x3 x4; gf' = GraphFunction x1a x2a x3a x4a; tr (Suc (Suc (i + j'))) = Some [(nn, return_vars x2a outps st' st, fn)]\<rbrakk> \<Longrightarrow> \<exists>j\<ge>2. tr (i + j) = Some [(nn, return_vars x2a outps st' st, fn)] proof (prove)
goal:
No subgoals!