theory GraphProof

lemma stepwise_graph_refine_inline_left:
  "stepwise_graph_refine Gamma (fname # f1 # fns, f2 # fns')
        (NextNode (entry_point gf3) # NextNode n # nns, nn' # nns')
        rel' orel otr (Suc N)
    \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2
    \<Longrightarrow> function_graph gf1 n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' upds)
    \<Longrightarrow> Gamma fname = Some gf3
    \<Longrightarrow> \<forall>x xs y ys. rel (x # xs, y # ys)
        \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys)
    \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns')
        (NextNode n # nns, NextNode n' # nns') rel orel otr N" apply (rule stepwise_graph_refineI) apply (erule_tac i="Suc i" and j="Suc j" in stepwise_graph_refineD) apply clarsimp apply (frule_tac i=i and tr=tr in exec_trace_step_cases) apply (frule_tac i=j and tr=tr' in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons split: graph_function.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stepwise_graph_refine Gamma (fname # f1 # fns, f2 # fns') (NextNode (entry_point gf3) # NextNode n # nns, nn' # nns') rel' orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys)\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (NextNode n # nns, NextNode n' # nns') rel orel otr N proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fname # f1 # fns, f2 # fns') (NextNode (entry_point gf3) # NextNode n # nns, nn' # nns') rel' orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys); N \<le> i \<and> N \<le> j \<and> tr i \<noteq> None \<and> tr' j \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' j))) = (NextNode n # nns, NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (f1 # fns, f2 # fns') \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (f1 # fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, f2 # fns')))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys); N \<le> i \<and> N \<le> j \<and> tr i \<noteq> None \<and> tr' j \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' j))) = (NextNode n # nns, NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (f1 # fns, f2 # fns') \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (f1 # fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, f2 # fns')))\<rbrakk> \<Longrightarrow> Suc N \<le> Suc i \<and> Suc N \<le> Suc j \<and> tr (Suc i) \<noteq> None \<and> tr' (Suc j) \<noteq> None \<and> (map fst (the (tr (Suc i))), map fst (the (tr' (Suc j)))) = (NextNode (entry_point gf3) # NextNode n # nns, nn' # nns') \<and> (map (snd \<circ> snd) (the (tr (Suc i))), map (snd \<circ> snd) (the (tr' (Suc j)))) = (fname # f1 # fns, f2 # fns') \<and> rel' (map (fst \<circ> snd) (the (tr (Suc i))), map (fst \<circ> snd) (the (tr' (Suc j)))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fname # f1 # fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fname # f1 # fns, f2 # fns'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa))\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc i) = Some y) \<and> (\<exists>y. tr' (Suc j) = Some y) \<and> map fst (the (tr (Suc i))) = NextNode (entry_point gf3) # NextNode n # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsa \<and> map (snd \<circ> snd) (the (tr (Suc i))) = fname # f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsa \<and> rel' (map (fst \<circ> snd) (the (tr (Suc i))), map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); 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> (\<exists>y. tr (Suc i) = Some y) \<and> (\<exists>y. tr' (Suc j) = Some y) \<and> map fst (the (tr (Suc i))) = NextNode (entry_point gf3) # NextNode n # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsa \<and> map (snd \<circ> snd) (the (tr (Suc i))) = fname # f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsa \<and> rel' (map (fst \<circ> snd) (the (tr (Suc i))), map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac zsa. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Call nn fname inputs outputs); function_graph gf2 n' = Some (node.Basic nn' upds); Gamma fname = Some gf3; \<forall>x xs y ys. rel (x # xs, y # ys) \<longrightarrow> rel' (init_vars (function_inputs gf3) inputs x # x # xs, upd_vars upds y # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((NextNode n', ac, f2) # zsa); nns = map fst zs; nns' = map fst zsa; rel (aa # map (fst \<circ> snd) zs, ac # map (fst \<circ> snd) zsa); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zsa; tr \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n, aa, f1) else last (map (snd \<circ> snd) zs)); tr' \<in> exec_trace Gamma (if zsa = [] then (snd \<circ> snd) (NextNode n', ac, f2) else last (map (snd \<circ> snd) zsa)); 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; tr' j = None \<and> tr' (Suc j) = None \<or> (\<exists>state. tr' j = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr' (Suc j) = None) \<or> tr' j \<noteq> None \<and> tr' (Suc j) \<noteq> None \<and> (the (tr' j), the (tr' (Suc j))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc i) = Some y) \<and> (\<exists>y. tr' (Suc j) = Some y) \<and> map fst (the (tr (Suc i))) = NextNode (entry_point gf3) # NextNode n # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsa \<and> map (snd \<circ> snd) (the (tr (Suc i))) = fname # f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsa \<and> rel' (map (fst \<circ> snd) (the (tr (Suc i))), map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal:
No subgoals!