theory GraphProof

lemma graph_function_restr_trace_refine:
  assumes wfs: "wf_graph_function f1 il1 ol1" "wf_graph_function f2 il2 ol2"
     and inps: "converse (reachable_step' f1) `` {NextNode (entry_point f1)} \<subseteq> set []"
               "converse (reachable_step' f2) `` {NextNode (entry_point f2)} \<subseteq> set []"
      and gfs: "Gamma1 fn1 = Some f1" "Gamma2 fn2 = Some f2"
  notes wf_facts = wf_graph_function_init_extract
                   wf_graph_function_init_extract
                   wf_graph_function_length_function_inputs
  shows "graph_function_refine prec Gamma1 fn1 Gamma2 fn2
        (eqs ieqs (Some o ils)) orel
    = (\<forall>tr tr'. related_pair (False, NextNode (entry_point f1), restrs_list [])
            (acc_vars (function_inputs f1))
            (True, NextNode (entry_point f2), restrs_list [])
            (acc_vars (function_inputs f2))
            (eqs ieqs (Some o ils) o tuple_switch) (tr, tr')
            \<and> exec_double_trace Gamma1 fn1 Gamma2 fn2 tr tr'
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2
        (restrs_list [(entry_point f1, [1])]) (restrs_list [(entry_point f2, [1])])
            orel tr tr')" using wfs apply (simp add: graph_function_refine_trace2 gfs) apply (simp add: restr_trace_refine_def gfs
                   restrs_eventually_init
                   restrs_list_def split_def related_pair_def double_visit_def
                   wf_graph_function_init_extract) apply (rule arg_cong[where f=All] ext)+ apply (auto simp: wf_graph_function_init_extract
                    wf_graph_function_length_function_inputs gfs
                    restrs_list_def
              cong: if_cong
             elim!: restrs_eventually_init[where Gamma=Gamma1, OF _ _ inps(1)]
                    restrs_eventually_init[where Gamma=Gamma2, OF _ _ inps(2)];
         metis) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_function_refine prec Gamma1 fn1 Gamma2 fn2 (eqs ieqs (Some \<circ> ils)) orel = (\<forall>tr tr'. related_pair (False, NextNode (entry_point f1), restrs_list []) (acc_vars (function_inputs f1)) (True, NextNode (entry_point f2), restrs_list []) (acc_vars (function_inputs f2)) (eqs ieqs (Some \<circ> ils) \<circ> tuple_switch) (tr, tr') \<and> tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list [(entry_point f1, [1])]) (restrs_list [(entry_point f2, [1])]) orel tr tr') proof (prove)
using this:
wf_graph_function f1 il1 ol1
wf_graph_function f2 il2 ol2

goal (1 subgoal):
 1. graph_function_refine prec Gamma1 fn1 Gamma2 fn2 (eqs ieqs (Some \<circ> ils)) orel = (\<forall>tr tr'. related_pair (False, NextNode (entry_point f1), restrs_list []) (acc_vars (function_inputs f1)) (True, NextNode (entry_point f2), restrs_list []) (acc_vars (function_inputs f2)) (eqs ieqs (Some \<circ> ils) \<circ> tuple_switch) (tr, tr') \<and> tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list [(entry_point f1, [1])]) (restrs_list [(entry_point f2, [1])]) orel tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph_function f1 il1 ol1; wf_graph_function f2 il2 ol2\<rbrakk> \<Longrightarrow> (\<forall>tr tr'. tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<and> (\<exists>xs. the (tr 0) = [init_state fn1 f1 xs] \<and> length xs = length (function_inputs f1) \<and> (\<exists>ys. the (tr' 0) = [init_state fn2 f2 ys] \<and> length ys = length (function_inputs f2) \<and> eqs ieqs (Some \<circ> ils) (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine2 prec (f1, f2) orel tr tr') = (\<forall>tr tr'. related_pair (False, NextNode (entry_point f1), restrs_list []) (acc_vars (function_inputs f1)) (True, NextNode (entry_point f2), restrs_list []) (acc_vars (function_inputs f2)) (eqs ieqs (Some \<circ> ils) \<circ> tuple_switch) (tr, tr') \<and> tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 (restrs_list [(entry_point f1, [Suc 0])]) (restrs_list [(entry_point f2, [Suc 0])]) orel tr tr') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph_function f1 il1 ol1; wf_graph_function f2 il2 ol2\<rbrakk> \<Longrightarrow> (\<forall>tr tr'. tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<and> (\<exists>xs. the (tr 0) = [init_state fn1 f1 xs] \<and> length xs = length (function_inputs f1) \<and> (\<exists>ys. the (tr' 0) = [init_state fn2 f2 ys] \<and> length ys = length (function_inputs f2) \<and> eqs ieqs (Some \<circ> ils) (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine2 prec (f1, f2) orel tr tr') = (\<forall>tr tr'. eqs ieqs (Some \<circ> ils) (tuple_switch (acc_vars (function_inputs f1) (the (visit tr (NextNode (entry_point f1)) (\<lambda>i. UNIV))), acc_vars (function_inputs f2) (the (visit tr' (NextNode (entry_point f2)) (\<lambda>i. UNIV))))) \<and> tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<longrightarrow> (\<exists>xs. the (tr 0) = [init_state fn1 f1 xs] \<and> length xs = length (function_inputs f1)) \<and> (\<exists>ys. the (tr' 0) = [init_state fn2 f2 ys] \<and> length ys = length (function_inputs f2)) \<and> restrs_eventually_condition tr (\<lambda>i. if i = entry_point f1 then set (snd (entry_point f1, [Suc 0])) \<inter> UNIV else UNIV) \<and> restrs_eventually_condition tr' (\<lambda>i. if i = entry_point f2 then set (snd (entry_point f2, [Suc 0])) \<inter> UNIV else UNIV) \<longrightarrow> trace_refine2 prec (f1, f2) orel tr tr') proof (prove)
goal (1 subgoal):
 1. \<And>tr tr'. \<lbrakk>wf_graph_function f1 il1 ol1; wf_graph_function f2 il2 ol2\<rbrakk> \<Longrightarrow> (tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<and> (\<exists>xs. the (tr 0) = [init_state fn1 f1 xs] \<and> length xs = length (function_inputs f1) \<and> (\<exists>ys. the (tr' 0) = [init_state fn2 f2 ys] \<and> length ys = length (function_inputs f2) \<and> eqs ieqs (Some \<circ> ils) (tuple_switch (xs, ys)))) \<longrightarrow> trace_refine2 prec (f1, f2) orel tr tr') = (eqs ieqs (Some \<circ> ils) (tuple_switch (acc_vars (function_inputs f1) (the (visit tr (NextNode (entry_point f1)) (\<lambda>i. UNIV))), acc_vars (function_inputs f2) (the (visit tr' (NextNode (entry_point f2)) (\<lambda>i. UNIV))))) \<and> tr \<in> exec_trace Gamma1 fn1 \<and> tr' \<in> exec_trace Gamma2 fn2 \<longrightarrow> (\<exists>xs. the (tr 0) = [init_state fn1 f1 xs] \<and> length xs = length (function_inputs f1)) \<and> (\<exists>ys. the (tr' 0) = [init_state fn2 f2 ys] \<and> length ys = length (function_inputs f2)) \<and> restrs_eventually_condition tr (\<lambda>i. if i = entry_point f1 then set (snd (entry_point f1, [Suc 0])) \<inter> UNIV else UNIV) \<and> restrs_eventually_condition tr' (\<lambda>i. if i = entry_point f2 then set (snd (entry_point f2, [Suc 0])) \<inter> UNIV else UNIV) \<longrightarrow> trace_refine2 prec (f1, f2) orel tr tr') proof (prove)
goal:
No subgoals!