theory GraphProof

lemma graph_function_refine_trace:
  "graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel
    = (\<forall>tr tr' xs ys gf gf'. exec_double_trace Gamma1 f1 Gamma2 f2 tr tr'
        \<and> tr 0 \<noteq> None \<and> tr' 0 \<noteq> None \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf'
        \<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) o snd)
            (tuple_switch (ys, function_outputs_st gf' st') o snd)
            )) tr tr')" apply (clarsimp simp: graph_function_refine_def) apply (simp only: ex_simps[symmetric] all_simps[symmetric]
              cong: conj_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_function_refine prec Gamma1 f1 Gamma2 f2 irel orel = (\<forall>tr tr' xs ys gf gf'. (tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2) \<and> tr 0 \<noteq> None \<and> tr' 0 \<noteq> None \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<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') proof (prove)
goal (1 subgoal):
 1. (\<forall>xs ys tr tr' gf gf'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> Gamma1 f1 = Some gf \<and> tr 0 = Some [init_state f1 gf xs] \<and> Gamma2 f2 = Some gf' \<and> tr' 0 = Some [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' xs ys gf gf'. 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> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<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') proof (prove)
goal (1 subgoal):
 1. (\<forall>xs ys tr tr' gf gf'. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> Gamma1 f1 = Some gf \<and> tr 0 = Some [init_state f1 gf xs] \<and> Gamma2 f2 = Some gf' \<and> tr' 0 = Some [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' xs ys gf gf' y ya. tr \<in> exec_trace Gamma1 f1 \<and> tr' \<in> exec_trace Gamma2 f2 \<and> tr 0 = Some ya \<and> tr' 0 = Some y \<and> Gamma1 f1 = Some gf \<and> Gamma2 f2 = Some gf' \<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') proof (prove)
goal:
No subgoals!