theory GraphRefine

lemma simpl_to_graph_creturn_void:
  "eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I)
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn
        (add_cont com.Throw con) n tS (upd_range exn_upd Return) I eqs2 out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn
        (add_cont (creturn_void exn_upd) con) n tS P I eqs out_eqs" apply (simp add: creturn_void_def simpl_to_graph_Seq) apply (rule_tac simpl_to_graph_Basic_triv'[rotated]) apply (rule simpl_to_graph_Skip_immediate) apply simp apply (simp add: upd_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont (creturn_void exn_upd) con) n tS P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont (com.Basic (exn_upd (\<lambda>_. Return))) (Inl THROW # con)) n tS P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont SKIP (Inl THROW # con)) (n + min 0 1) tS ?Q I ?eqs2.0 out_eqs
 2. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> eq_impl nn eqs (\<lambda>gst sst. ?eqs2.0 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I \<and> exn_upd (\<lambda>_. Return) sst \<in> ?Q) (P \<inter> I) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont THROW con) (n + min 0 1) tS ?Q I ?eqs2.0 out_eqs
 2. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> eq_impl nn eqs (\<lambda>gst sst. ?eqs2.0 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I \<and> exn_upd (\<lambda>_. Return) sst \<in> ?Q) (P \<inter> I) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I) (P \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> eq_impl nn eqs (\<lambda>gst sst. eqs2 gst (exn_upd (\<lambda>_. Return) sst) \<and> exn_upd (\<lambda>_. Return) sst \<in> I \<and> exn_upd (\<lambda>_. Return) sst \<in> upd_range exn_upd Return) (P \<inter> I) proof (prove)
goal:
No subgoals!