theory GraphRefine

lemma simpl_to_graph_ccatchbrk_Return:
  "\<forall>f s. exn_var (exn_upd f s) = f (exn_var s)
    \<Longrightarrow> eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 (ccatchbrk exn_var) con) n tS (upd_range exn_upd Return) I eqs out_eqs" apply (simp add: ccatchbrk_def) apply (rule simpl_to_graph_step_R_unchanged) apply (simp add: upd_range_def) apply (rule add_cont_step step.CondFalse)+ apply clarsimp apply (erule simpl_to_graph_weaken, simp add: eq_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 (ccatchbrk exn_var) con) n tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 (IF \<acute>exn_var = Break THEN
  SKIP
ELSE
  THROW
FI) con) n tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (upd_range exn_upd Return) I eqs2 out_eqs; sst \<in> upd_range exn_upd Return; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (IF \<acute>exn_var = Break THEN
  SKIP
ELSE
  THROW
FI) con, Normal sst) \<rightarrow> (?com', Normal sst)
 2. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 ?com' n tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (range (exn_upd (\<lambda>_. Return)) \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (range (exn_upd (\<lambda>_. Return))) I eqs2 out_eqs; sst \<in> range (exn_upd (\<lambda>_. Return)); sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (IF \<acute>exn_var = Break THEN
  SKIP
ELSE
  THROW
FI) con, Normal sst) \<rightarrow> (?com', Normal sst)
 2. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 ?com' n tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (range (exn_upd (\<lambda>_. Return)) \<inter> I); simpl_to_graph SGamma GGamma f nn (add_cont THROW con) n tS (range (exn_upd (\<lambda>_. Return))) I eqs2 out_eqs; sst \<in> range (exn_upd (\<lambda>_. Return)); sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> sst \<notin> {s. exn_var s = Break}
 2. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>f s. exn_var (exn_upd f s) = f (exn_var s); eq_impl nn eqs eqs2 (upd_range exn_upd Return \<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 tS (upd_range exn_upd Return) I eqs out_eqs proof (prove)
goal:
No subgoals!