theory GraphProof

lemma test_restrs_condition:
  "\<lbrakk> graph = [ 1 \<mapsto> Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> Basic (NextNode 3) [], 3 \<mapsto> Basic Ret [] ];
    Gamma ''bar'' = Some (GraphFunction [] [] graph 1);
    tr \<in> exec_trace Gamma ''bar'';
    Gamma ''foo'' = Some (GraphFunction [] [] [ 1 \<mapsto> Basic Ret []] 1) \<rbrakk>
    \<Longrightarrow> restrs_condition tr (restrs_list [(1, [1])]) 5" apply (frule exec_trace_init, elim exE conjE) apply (frule_tac i=0 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases) apply (frule_tac i=1 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) apply (frule_tac i=2 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def TWO return_vars_def) apply (frule_tac i=3 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) apply (frule_tac i=4 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) apply (frule_tac i=5 in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases upd_vars_def save_vals_def init_vars_def) apply (simp add: restrs_condition_def Collect_less_nat Collect_conv_if trace_addr_def
                   restrs_list_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>graph = [1 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; Gamma ''bar'' = Some (GraphFunction [] [] graph 1); tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [1 \<mapsto> node.Basic Ret []] 1)\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(1, [1])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st gf. \<lbrakk>graph = [1 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; Gamma ''bar'' = Some (GraphFunction [] [] graph 1); tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [1 \<mapsto> node.Basic Ret []] 1); Gamma ''bar'' = Some gf; tr 0 = Some [(NextNode (entry_point gf), st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(1, [1])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st y. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; ([(NextNode (Suc 0), st, ''bar'')], y) \<in> exec_graph_step Gamma; tr (Suc 0) = Some y\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), init_vars [] [] st, ''foo''), (NextNode (Suc 0), st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st y. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), init_vars [] [] st, ''foo''), (NextNode (Suc 0), st, ''bar'')]; ([(NextNode (Suc 0), init_vars [] [] st, ''foo''), (NextNode (Suc 0), st, ''bar'')], y) \<in> exec_graph_step Gamma; tr (Suc (Suc 0)) = Some y\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr (Suc (Suc 0)) = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr (Suc (Suc 0)) = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = None \<and> tr 3 = None \<or> (\<exists>a. (\<exists>aa b. tr 2 = Some [(a, aa, b)]) \<and> (a = Ret \<or> a = Err) \<and> tr 3 = None) \<or> (\<exists>y. tr 2 = Some y) \<and> (\<exists>y. tr 3 = Some y) \<and> (the (tr 2), the (tr 3)) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st y. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; ([(NextNode 2, st, ''bar'')], y) \<in> exec_graph_step Gamma; tr 4 = Some y\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; tr 4 = Some [(NextNode 3, st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st y. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; tr 4 = Some [(NextNode 3, st, ''bar'')]; ([(NextNode 3, st, ''bar'')], y) \<in> exec_graph_step Gamma; tr 5 = Some y\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; tr 4 = Some [(NextNode 3, st, ''bar'')]; tr 5 = Some [(Ret, st, ''bar'')]\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; tr 4 = Some [(NextNode 3, st, ''bar'')]; tr 5 = Some [(Ret, st, ''bar'')]; tr 6 = None \<or> (\<exists>y. tr 6 = Some y) \<and> ([(Ret, st, ''bar'')], the (tr 6)) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>graph = [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []]; tr \<in> exec_trace Gamma ''bar''; Gamma ''foo'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Basic Ret []] (Suc 0)); Gamma ''bar'' = Some (GraphFunction [] [] [Suc 0 \<mapsto> node.Call (NextNode 2) ''foo'' [] [], 2 \<mapsto> node.Basic (NextNode 3) [], 3 \<mapsto> node.Basic Ret []] (Suc 0)); tr 0 = Some [(NextNode (Suc 0), st, ''bar'')]; tr (Suc 0) = Some [(NextNode (Suc 0), default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 2 = Some [(Ret, default_state, ''foo''), (NextNode (Suc 0), st, ''bar'')]; tr 3 = Some [(NextNode 2, st, ''bar'')]; tr 4 = Some [(NextNode 3, st, ''bar'')]; tr 5 = Some [(Ret, st, ''bar'')]; tr 6 = None\<rbrakk> \<Longrightarrow> restrs_condition tr (restrs_list [(Suc 0, [Suc 0])]) 5 proof (prove)
goal:
No subgoals!