theory GraphRefine

lemma simpl_to_graph_Err_cond:
  "\<lbrakk> nn = NextNode m; GGamma fname = Some gf;
      function_graph gf m = Some (node.Cond l Err Check);
      eq_impl nn eqs (\<lambda>gst sst. Check gst) (P \<inter> I);
      eq_impl nn eqs eqs2 (P \<inter> I);
      simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma fname nn com n traces P I eqs out_eqs" apply (rule_tac i=1 and j=0 in simpl_to_graph_step_general[rotated -1]) apply simp apply (simp add: exec_graph_step_image_node) apply (auto dest: eq_implD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; GGamma fname = Some gf; function_graph gf m = Some (node.Cond l Err Check); eq_impl nn eqs (\<lambda>gst sst. Check gst) (P \<inter> I); eq_impl nn eqs eqs2 (P \<inter> I); simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma fname nn com n traces P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nn = NextNode m; GGamma fname = Some gf; function_graph gf m = Some (node.Cond l Err Check); eq_impl nn eqs (\<lambda>gst sst. Check gst) (P \<inter> I); eq_impl nn eqs eqs2 (P \<inter> I); simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma fname ?nn' ?com' (n + min 1 0) traces ?P' I ?inp_eqs' out_eqs
 2. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma fname = Some gf; function_graph gf m = Some (node.Cond l Err Check); eq_impl nn eqs (\<lambda>gst sst. Check gst) (P \<inter> I); eq_impl nn eqs eqs2 (P \<inter> I); simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 0) (com, Normal sst) (?com', Normal sst') \<and> (exec_graph_step GGamma ^^ 1) `` {[(nn, gst, fname)]} \<subseteq> {[(?nn', gst', fname)]} \<and> (\<forall>k<1. \<forall>st'. ([(nn, gst, fname)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> ?P' \<and> sst' \<in> I \<and> ?inp_eqs' gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma fname = Some gf; function_graph gf m = Some (node.Cond l Err Check); eq_impl nn eqs (\<lambda>gst sst. Check gst) (P \<inter> I); eq_impl nn eqs eqs2 (P \<inter> I); simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 0) (com, Normal sst) (com, Normal sst') \<and> (exec_graph_step GGamma ^^ 1) `` {[(nn, gst, fname)]} \<subseteq> {[(l, gst', fname)]} \<and> (\<forall>k<1. \<forall>st'. ([(nn, gst, fname)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> P \<and> sst' \<in> I \<and> eqs2 gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma fname = Some gf; function_graph gf m = Some (node.Cond l Err Check); eq_impl (NextNode m) eqs (\<lambda>gst sst. Check gst) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I); simpl_to_graph SGamma GGamma fname l com n traces P I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> (Check gst \<longrightarrow> eqs2 gst sst) \<and> (\<not> Check gst \<longrightarrow> Err = l \<and> eqs2 gst sst) proof (prove)
goal:
No subgoals!