theory GraphRefine

lemma simpl_to_graph_step:
  "(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
        \<Longrightarrow> \<exists>sst' gst'. (step SGamma) (com, Normal sst) (com', Normal sst')
            \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]}
            \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst')
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) com n traces P I inp_eqs out_eqs" apply (rule simpl_to_graph_step_general[rotated, where i=1 and j=1]) apply simp+ apply (simp add: eq_OO) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]} \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst'; simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) com n traces P I inp_eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]} \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst'; simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf ?nn' ?com' (n + min 1 1) traces ?P' I ?inp_eqs' out_eqs
 2. \<And>sst gst. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]} \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst'; simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs; sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 1) (com, Normal sst) (?com', Normal sst') \<and> (exec_graph_step GGamma ^^ 1) `` {[(NextNode m, gst, gf)]} \<subseteq> {[(?nn', gst', gf)]} \<and> (\<forall>k<1. \<forall>st'. ([(NextNode m, gst, gf)], 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>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> (\<exists>gst'. exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]} \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst'); simpl_to_graph SGamma GGamma gf nn' com' (Suc n) traces P' I inp_eqs' out_eqs; sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. ((=) OO step SGamma) (com, Normal sst) (com', Normal sst') \<and> (\<exists>gst'. exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn', gst', gf)]} \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst' sst') proof (prove)
goal:
No subgoals!