theory GraphProof

lemma graph_function_refine_trace2:
  "Gamma1 f1 = Some gf \<Longrightarrow> wf_graph_function gf ilen1 olen1
    \<Longrightarrow> Gamma2 f2 = Some gf' \<Longrightarrow> wf_graph_function gf' ilen2 olen2
    \<Longrightarrow> graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel
    = (\<forall>tr tr'. exec_double_trace Gamma1 f1 Gamma2 f2 tr tr'
        \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf'
        \<and> (\<exists>xs ys. the (tr 0) = [init_state f1 gf xs]
            \<and> length xs = length (function_inputs gf)
            \<and> the (tr' 0) = [init_state f2 gf' ys]
            \<and> length ys = length (function_inputs gf')
            \<and> irel (tuple_switch (xs, ys)))
        \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr')" apply (clarsimp simp: graph_function_refine_trace trace_refine2_def) apply (frule wf_graph_function_length_function_inputs[where f=gf]) apply (frule wf_graph_function_length_function_inputs[where f=gf']) apply (simp add: imp_conjL) apply (rule arg_cong[where f=All] ext imp_cong[OF refl])+ apply (clarsimp dest!: exec_trace_init) apply (safe, simp_all add: init_state_def wf_graph_function_acc_vars_save_vals) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2\<rbrakk> \<Longrightarrow> graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel = (\<forall>tr tr'. (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<and> (\<exists>xs ys. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf) \<and> the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys))) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2\<rbrakk> \<Longrightarrow> (\<forall>tr tr' xs ys. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>y. tr 0 = Some y) \<and> (\<exists>y. tr' 0 = Some y) \<and> the (tr 0) = [init_state f1 gf xs] \<and> the (tr' 0) = [init_state f2 gf' ys] \<and> length xs = length (function_inputs gf) \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr') = (\<forall>tr tr'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (hd (the (tr 0))))), function_outputs_st gf st) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (hd (the (tr' 0))))), function_outputs_st gf' st') \<circ> snd))) tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2; length (function_inputs gf) = ilen1\<rbrakk> \<Longrightarrow> (\<forall>tr tr' xs ys. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>y. tr 0 = Some y) \<and> (\<exists>y. tr' 0 = Some y) \<and> the (tr 0) = [init_state f1 gf xs] \<and> the (tr' 0) = [init_state f2 gf' ys] \<and> length xs = length (function_inputs gf) \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr') = (\<forall>tr tr'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (hd (the (tr 0))))), function_outputs_st gf st) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (hd (the (tr' 0))))), function_outputs_st gf' st') \<circ> snd))) tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2; length (function_inputs gf) = ilen1; length (function_inputs gf') = ilen2\<rbrakk> \<Longrightarrow> (\<forall>tr tr' xs ys. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>y. tr 0 = Some y) \<and> (\<exists>y. tr' 0 = Some y) \<and> the (tr 0) = [init_state f1 gf xs] \<and> the (tr' 0) = [init_state f2 gf' ys] \<and> length xs = length (function_inputs gf) \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr') = (\<forall>tr tr'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = length (function_inputs gf) \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (hd (the (tr 0))))), function_outputs_st gf st) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (hd (the (tr' 0))))), function_outputs_st gf' st') \<circ> snd))) tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2; length (function_inputs gf) = ilen1; length (function_inputs gf') = ilen2\<rbrakk> \<Longrightarrow> (\<forall>tr. tr \<in> exec_trace Gamma1 f1 \<longrightarrow> (\<forall>tr'. tr' \<in> exec_trace Gamma2 f2 \<longrightarrow> (\<exists>y. tr 0 = Some y) \<longrightarrow> (\<exists>y. tr' 0 = Some y) \<longrightarrow> (\<forall>xs. the (tr 0) = [init_state f1 gf xs] \<longrightarrow> (\<forall>ys. the (tr' 0) = [init_state f2 gf' ys] \<longrightarrow> length xs = ilen1 \<longrightarrow> length ys = ilen2 \<longrightarrow> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr')))) = (\<forall>tr. tr \<in> exec_trace Gamma1 f1 \<longrightarrow> (\<forall>tr'. tr' \<in> exec_trace Gamma2 f2 \<longrightarrow> (\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = ilen1 \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = ilen2 \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (hd (the (tr 0))))), function_outputs_st gf st) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (hd (the (tr' 0))))), function_outputs_st gf' st') \<circ> snd))) tr tr')) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr'. \<lbrakk>Gamma1 f1 = Some gf; wf_graph_function gf ilen1 olen1; Gamma2 f2 = Some gf'; wf_graph_function gf' ilen2 olen2; length (function_inputs gf) = ilen1; length (function_inputs gf') = ilen2; tr \<in> exec_trace Gamma1 f1; tr' \<in> exec_trace Gamma2 f2\<rbrakk> \<Longrightarrow> ((\<exists>y. tr 0 = Some y) \<longrightarrow> (\<exists>y. tr' 0 = Some y) \<longrightarrow> (\<forall>xs. the (tr 0) = [init_state f1 gf xs] \<longrightarrow> (\<forall>ys. the (tr' 0) = [init_state f2 gf' ys] \<longrightarrow> length xs = ilen1 \<longrightarrow> length ys = ilen2 \<longrightarrow> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr'))) = ((\<exists>xs. the (tr 0) = [init_state f1 gf xs] \<and> length xs = ilen1 \<and> (\<exists>ys. the (tr' 0) = [init_state f2 gf' ys] \<and> length ys = ilen2 \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (hd (the (tr 0))))), function_outputs_st gf st) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (hd (the (tr' 0))))), function_outputs_st gf' st') \<circ> snd))) tr tr') proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' st sta. \<lbrakk>wf_graph_function gf (length (function_inputs gf)) olen1; wf_graph_function gf' (length (function_inputs gf')) olen2; ilen1 = length (function_inputs gf); ilen2 = length (function_inputs gf'); Gamma1 f1 = Some gf; tr 0 = Some [(NextNode (entry_point gf), st, f1)]; Gamma2 f2 = Some gf'; tr' 0 = Some [(NextNode (entry_point gf'), sta, f2)]\<rbrakk> \<Longrightarrow> (\<forall>xs. (NextNode (entry_point gf), st, f1) = init_state f1 gf xs \<longrightarrow> (\<forall>ys. (NextNode (entry_point gf'), sta, f2) = init_state f2 gf' ys \<longrightarrow> length xs = length (function_inputs gf) \<longrightarrow> length ys = length (function_inputs gf') \<longrightarrow> irel (tuple_switch (xs, ys)) \<longrightarrow> trace_refine prec (\<lambda>st st'. orel (switch_val fst (tuple_switch (xs, function_outputs_st gf st) \<circ> snd) (tuple_switch (ys, function_outputs_st gf' st') \<circ> snd))) tr tr')) = ((\<exists>xs. (NextNode (entry_point gf), st, f1) = init_state f1 gf xs \<and> length xs = length (function_inputs gf) \<and> (\<exists>ys. (NextNode (entry_point gf'), sta, f2) = init_state f2 gf' ys \<and> length ys = length (function_inputs gf') \<and> irel (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine prec (\<lambda>stb st'. orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) st, function_outputs_st gf stb) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') sta, function_outputs_st gf' st') \<circ> snd))) tr tr') proof (prove)
goal:
No subgoals!