theory GraphProof

lemma stepwise_graph_refine_nop_right:
  "stepwise_graph_refine Gamma (fns, f2 # fns') (nns, nn' # nns') rel orel otr N
    \<Longrightarrow> Gamma f2 = Some gf2
    \<Longrightarrow> function_graph gf2 n' = Some (Basic nn' [])
    \<Longrightarrow> stepwise_graph_refine Gamma (fns, f2 # fns')
        (nns, NextNode n' # nns') rel orel otr N" apply (rule stepwise_graph_refineI) apply (erule_tac i="i" and j="Suc j" in stepwise_graph_refineD) apply clarsimp 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) apply (simp add: K_def upd_vars_def save_vals_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stepwise_graph_refine Gamma (fns, f2 # fns') (nns, nn' # nns') rel orel otr N; Gamma f2 = Some gf2; function_graph gf2 n' = Some (node.Basic nn' [])\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma (fns, f2 # fns') (nns, NextNode n' # nns') rel orel otr N proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, f2 # fns') (nns, nn' # nns') rel orel otr N; Gamma f2 = Some gf2; function_graph gf2 n' = Some (node.Basic nn' []); 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))) = (nns, NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (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 (fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (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 f2 = Some gf2; function_graph gf2 n' = Some (node.Basic nn' []); 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))) = (nns, NextNode n' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (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 (fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, f2 # fns')))\<rbrakk> \<Longrightarrow> N \<le> i \<and> N \<le> Suc j \<and> tr i \<noteq> None \<and> tr' (Suc j) \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' (Suc j)))) = (nns, nn' # nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' (Suc j)))) = (fns, f2 # fns') \<and> rel (map (fst \<circ> snd) (the (tr 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 (fns, f2 # fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, f2 # fns'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y aa zs. \<lbrakk>Gamma f2 = Some gf2; function_graph gf2 n' = Some (node.Basic nn' []); N \<le> i; N \<le> j; tr i = Some y; tr' j = Some ((NextNode n', aa, f2) # zs); nns = map fst y; fns = map (snd \<circ> snd) y; nns' = map fst zs; rel (map (fst \<circ> snd) y, aa # map (fst \<circ> snd) zs); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zs; tr \<in> exec_trace Gamma (last (map (snd \<circ> snd) y)); tr' \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n', aa, f2) else last (map (snd \<circ> snd) zs))\<rbrakk> \<Longrightarrow> (\<exists>y. tr' (Suc j) = Some y) \<and> map fst (the (tr' (Suc j))) = nn' # map fst zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zs \<and> rel (map (fst \<circ> snd) y, map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y aa zs. \<lbrakk>Gamma f2 = Some gf2; function_graph gf2 n' = Some (node.Basic nn' []); N \<le> i; N \<le> j; tr i = Some y; tr' j = Some ((NextNode n', aa, f2) # zs); nns = map fst y; fns = map (snd \<circ> snd) y; nns' = map fst zs; rel (map (fst \<circ> snd) y, aa # map (fst \<circ> snd) zs); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zs; tr \<in> exec_trace Gamma (last (map (snd \<circ> snd) y)); tr' \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n', aa, f2) else last (map (snd \<circ> snd) zs)); 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 j) = Some y) \<and> map fst (the (tr' (Suc j))) = nn' # map fst zs \<and> map (snd \<circ> snd) (the (tr' (Suc j))) = f2 # map (snd \<circ> snd) zs \<and> rel (map (fst \<circ> snd) y, map (fst \<circ> snd) (the (tr' (Suc j)))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y aa zs x1 x2 x3 x4. \<lbrakk>Gamma f2 = Some (GraphFunction x1 x2 x3 x4); x3 n' = Some (node.Basic nn' []); N \<le> i; N \<le> j; tr i = Some y; tr' j = Some ((NextNode n', aa, f2) # zs); nns = map fst y; fns = map (snd \<circ> snd) y; nns' = map fst zs; rel (map (fst \<circ> snd) y, aa # map (fst \<circ> snd) zs); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); fns' = map (snd \<circ> snd) zs; tr \<in> exec_trace Gamma (last (map (snd \<circ> snd) y)); tr' \<in> exec_trace Gamma (if zs = [] then (snd \<circ> snd) (NextNode n', aa, f2) else last (map (snd \<circ> snd) zs)); gf2 = GraphFunction x1 x2 x3 x4; tr' (Suc j) = Some ((nn', upd_vars [] aa, f2) # zs)\<rbrakk> \<Longrightarrow> rel (map (fst \<circ> snd) y, upd_vars [] aa # map (fst \<circ> snd) zs) proof (prove)
goal:
No subgoals!