theory GraphRefine

lemma simpl_to_graph_Basic_next_step:
  assumes next_step: "eq_impl nn eqs (\<lambda>gst' sst'.
        ((exec_graph_step GGamma) ^^ steps) `` {[(nn, gst', fn)]} \<subseteq> {[(nn', f gst', fn)]}
        \<and> (\<forall>k < steps. \<forall>st'. ([(nn, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
        \<longrightarrow> continuing st')) (P \<inter> I)"
  shows
  "\<lbrakk> eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I);
        simpl_to_graph SGamma GGamma fn nn' (add_cont com.Skip con) (n + min steps 1) tS Q I eqs2 out_eqs \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma fn nn (add_cont (com.Basic f') con) n tS P I eqs out_eqs" apply (rule simpl_to_graph_step_general[where j=1 and i=steps, rotated -1]) apply simp apply (frule eq_implD[OF next_step], simp) apply (simp add: eq_OO) apply (rule exI, rule conjI, blast intro: add_cont_step step.intros) apply (auto dest: eq_implD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps 1) tS Q I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma fn nn (add_cont (com.Basic f') con) n tS P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps 1) tS Q I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma fn ?nn' ?com' (n + min steps 1) tS ?P' I ?inp_eqs' out_eqs
 2. \<And>sst gst. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps 1) tS Q I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 1) (add_cont (com.Basic f') con, Normal sst) (?com', Normal sst') \<and> (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(?nn', gst', fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], 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>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps 1) tS Q I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 1) (add_cont (com.Basic f') con, Normal sst) (add_cont SKIP con, Normal sst') \<and> (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', gst', fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> Q \<and> sst' \<in> I \<and> eqs2 gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps 1) tS Q I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst; (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', f gst, fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 1) (add_cont (com.Basic f') con, Normal sst) (add_cont SKIP con, Normal sst') \<and> (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', gst', fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> Q \<and> sst' \<in> I \<and> eqs2 gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps (Suc 0)) tS Q I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst; (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', f gst, fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (com.Basic f') con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> (\<exists>gst'. (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', gst', fn)]} \<and> sst' \<in> Q \<and> sst' \<in> I \<and> eqs2 gst' sst') proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>eq_impl nn eqs (\<lambda>gst sst. eqs2 (f gst) (f' sst) \<and> f' sst \<in> I \<and> f' sst \<in> Q) (P \<inter> I); simpl_to_graph SGamma GGamma fn nn' (add_cont SKIP con) (n + min steps (Suc 0)) tS Q I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst; (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', f gst, fn)]} \<and> (\<forall>k<steps. \<forall>st'. ([(nn, gst, fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')\<rbrakk> \<Longrightarrow> \<exists>gst'. (exec_graph_step GGamma ^^ steps) `` {[(nn, gst, fn)]} \<subseteq> {[(nn', gst', fn)]} \<and> f' sst \<in> Q \<and> f' sst \<in> I \<and> eqs2 gst' (f' sst) proof (prove)
goal:
No subgoals!