theory GraphRefine

lemma simpl_to_graph_lvar_nondet_init:
  assumes stg: "simpl_to_graph SGamma GGamma fname nn (add_cont com.Skip con) n traces UNIV I eqs2 out_eqs"
      and eqs: "eq_impl nn eqs (\<lambda>gst sst. \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I) (P \<inter> I)"
  shows "simpl_to_graph SGamma GGamma fname nn
        (add_cont (lvar_nondet_init accf updf) con) n traces P I eqs out_eqs" apply (rule simpl_to_graph_step_R[OF _ stg]) apply (simp add: lvar_nondet_init_def) apply (drule eq_implD[OF eqs], simp) apply (rule exI, rule conjI, rule add_cont_step) apply (rule step.Spec) apply simp apply (rule_tac x=undefined in exI, simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma fname nn (add_cont (lvar_nondet_init accf updf) con) n traces P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (lvar_nondet_init accf updf) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> sst' \<in> UNIV \<and> sst' \<in> I \<and> eqs2 gst sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (Spec {(s, t). \<exists>v. t = updf (\<lambda>_. v) s}) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> sst' \<in> I \<and> eqs2 gst sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (Spec {(s, t). \<exists>v. t = updf (\<lambda>_. v) s}) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> sst' \<in> I \<and> eqs2 gst sst' proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (Spec {(s, t). \<exists>v. t = updf (\<lambda>_. v) s}, Normal sst) \<rightarrow> (SKIP, Normal (?sst'6 sst gst))
 2. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> ?sst'6 sst gst \<in> I \<and> eqs2 gst (?sst'6 sst gst) proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> (sst, ?sst'6 sst gst) \<in> {(s, t). \<exists>v. t = updf (\<lambda>_. v) s}
 2. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> ?sst'6 sst gst \<in> I \<and> eqs2 gst (?sst'6 sst gst) proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> \<exists>v. ?sst'6 sst gst = updf (\<lambda>_. v) sst
 2. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> ?sst'6 sst gst \<in> I \<and> eqs2 gst (?sst'6 sst gst) proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; \<forall>f. eqs2 gst (updf f sst) \<and> updf f sst \<in> I\<rbrakk> \<Longrightarrow> updf (\<lambda>_. undefined) sst \<in> I \<and> eqs2 gst (updf (\<lambda>_. undefined) sst) proof (prove)
goal:
No subgoals!