theory GraphProof

lemma stepwise_graph_refine_end_inline_right:
  "stepwise_graph_refine Gamma (f1 # fns, f2 # fns')
        (nn # nns, nn' # nns')
        rel' orel otr (Suc N)
    \<Longrightarrow> Gamma f1 = Some gf1 \<Longrightarrow> Gamma f2 = Some gf2
    \<Longrightarrow> function_graph gf1 n = Some (Basic nn upds)
    \<Longrightarrow> function_graph gf2 n' = Some (Call nn' fname inputs outputs)
    \<Longrightarrow> Gamma fname = Some gf3
    \<Longrightarrow> \<forall>x xs y y' ys. rel (x # xs, y # y' # ys)
        \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys)
    \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, fname # f2 # fns')
        (NextNode n # nns, Ret # 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 (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel' orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys)\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma (f1 # fns, fname # f2 # fns') (NextNode n # nns, Ret # NextNode n' # nns') rel orel otr N proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (f1 # fns, f2 # fns') (nn # nns, nn' # nns') rel' orel otr (Suc N); Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y 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, Ret # NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (f1 # fns, fname # 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, fname # f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, fname # 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.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y 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, Ret # NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (f1 # fns, fname # 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, fname # f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, fname # 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)))) = (nn # nns, nn' # nns') \<and> (map (snd \<circ> snd) (the (tr (Suc i))), map (snd \<circ> snd) (the (tr' (Suc j)))) = (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 (f1 # fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (f1 # fns, f2 # fns'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j aa zs ac ai zsd. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((Ret, ac, fname) # (NextNode n', ai, f2) # zsd); nns = map fst zs; rel (aa # map (fst \<circ> snd) zs, ac # ai # map (fst \<circ> snd) zsd); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); nns' = map fst zsd; 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 zsd = [] then (snd \<circ> snd) (NextNode n', ai, f2) else last (map (snd \<circ> snd) zsd)); fns' = map (snd \<circ> snd) zsd\<rbrakk> \<Longrightarrow> (\<exists>y. tr (Suc i) = Some y) \<and> (\<exists>y. tr' (Suc j) = Some y) \<and> map fst (the (tr (Suc i))) = nn # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsd \<and> map (snd \<circ> snd) (the (tr (Suc i))) = f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsd \<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 ai zsd. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((Ret, ac, fname) # (NextNode n', ai, f2) # zsd); nns = map fst zs; rel (aa # map (fst \<circ> snd) zs, ac # ai # map (fst \<circ> snd) zsd); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); nns' = map fst zsd; 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 zsd = [] then (snd \<circ> snd) (NextNode n', ai, f2) else last (map (snd \<circ> snd) zsd)); fns' = map (snd \<circ> snd) zsd; 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))) = nn # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsd \<and> map (snd \<circ> snd) (the (tr (Suc i))) = f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsd \<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 ai zsd. \<lbrakk>Gamma f1 = Some gf1; Gamma f2 = Some gf2; function_graph gf1 n = Some (node.Basic nn upds); function_graph gf2 n' = Some (node.Call nn' fname inputs outputs); Gamma fname = Some gf3; \<forall>x xs y y' ys. rel (x # xs, y # y' # ys) \<longrightarrow> rel' (upd_vars upds x # xs, return_vars (function_outputs gf3) outputs y y' # ys); N \<le> i; N \<le> j; tr i = Some ((NextNode n, aa, f1) # zs); tr' j = Some ((Ret, ac, fname) # (NextNode n', ai, f2) # zsd); nns = map fst zs; rel (aa # map (fst \<circ> snd) zs, ac # ai # map (fst \<circ> snd) zsd); fns = map (snd \<circ> snd) zs; (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); nns' = map fst zsd; 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 zsd = [] then (snd \<circ> snd) (NextNode n', ai, f2) else last (map (snd \<circ> snd) zsd)); fns' = map (snd \<circ> snd) zsd; 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))) = nn # map fst zs \<and> map fst (the (tr' (Suc j))) = nn' # map fst zsd \<and> map (snd \<circ> snd) (the (tr (Suc i))) = f1 # map (snd \<circ> snd) zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zsd \<and> rel' (map (fst \<circ> snd) (the (tr (Suc i))), map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal:
No subgoals!