theory GraphRefine

lemma simpl_to_graph_While_lemma:
  assumes ps: "GGamma f = Some gf" "nn = NextNode m" "function_graph gf m = Some (Cond l r cond)"
        "eq_impl nn eqs (\<lambda>gst sst. cond gst = (sst \<in> C)) (I \<inter> P)"
  assumes loop: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) P I eqs out_eqs \<rbrakk>
        \<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c ;; com.While C c) con) (Suc (n + k)) (S # tS) (P \<inter> C) I eqs out_eqs"
  assumes exitloop: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (P \<inter> (- C)) I eqs out_eqs"
  shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS P I eqs out_eqs" apply (rule simpl_to_graph_induct) apply (simp add: ps) apply (rule_tac S=C in simpl_to_graph_cases) apply (rule simpl_to_graph_step[rotated]) apply (rule loop) apply (simp add: ps) apply (frule eq_implD[OF ps(4)], simp+) apply (simp add: exec_graph_step_image_node ps) apply (blast intro: step.intros add_cont_step) apply (rule simpl_to_graph_step[rotated]) apply (rule simpl_to_graph_ge_subset) apply (rule exitloop) apply fastforce apply (frule eq_implD[OF ps(4)], simp+) apply (simp add: exec_graph_step_image_node ps) apply (blast intro: step.intros add_cont_step) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) n tS P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) (Suc n + k) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) (n + k) (S' # tS) P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> C) I eqs out_eqs
 2. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (3 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (?nn'3 S' k) (?com'3 S' k) (Suc (n + k)) (S' # tS) (?P'3 S' k) I (?inp_eqs'3 S' k) out_eqs
 2. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (?com'3 S' k, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(?nn'3 S' k, gst', f)]} \<and> sst' \<in> ?P'3 S' k \<and> sst' \<in> I \<and> ?inp_eqs'3 S' k gst' sst'
 3. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (3 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs
 2. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont (c;;
While C c) con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(l, gst', f)]} \<and> sst' \<in> P \<inter> C \<and> sst' \<in> I \<and> eqs gst' sst'
 3. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont (c;;
While C c) con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(l, gst', f)]} \<and> sst' \<in> P \<inter> C \<and> sst' \<in> I \<and> eqs gst' sst'
 2. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<and> sst \<in> C; sst \<in> I; eqs gst sst; cond gst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont (c;;
While C c) con, Normal sst') \<and> (\<exists>gst'. exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(l, gst', f)]} \<and> sst' \<in> P \<and> sst' \<in> C \<and> sst' \<in> I \<and> eqs gst' sst')
 2. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<and> sst \<in> C; sst \<in> I; eqs gst sst; cond gst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont (c;;
While C c) con, Normal sst') \<and> sst' \<in> P \<and> sst' \<in> C \<and> sst' \<in> I \<and> eqs gst sst'
 2. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (n + k) (S' # tS) (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (?nn'28 S' k) (?com'28 S' k) (Suc (n + k)) (S' # tS) (?P'28 S' k) I (?inp_eqs'28 S' k) out_eqs
 2. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> - C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (?com'28 S' k, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(?nn'28 S' k, gst', f)]} \<and> sst' \<in> ?P'28 S' k \<and> sst' \<in> I \<and> ?inp_eqs'28 S' k gst' sst' proof (prove)
goal (3 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f (?nn'28 S' k) (?com'28 S' k) (?n31 S' k) (?traces'31 S' k) (?P'28 S' k) I (?inp_eqs'28 S' k) out_eqs
 2. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> ?n31 S' k \<le> Suc (n + k) \<and> set (?traces'31 S' k) \<subseteq> set (S' # tS)
 3. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> - C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (?com'28 S' k, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(?nn'28 S' k, gst', f)]} \<and> sst' \<in> ?P'28 S' k \<and> sst' \<in> I \<and> ?inp_eqs'28 S' k gst' sst' proof (prove)
goal (2 subgoals):
 1. \<And>S' k. simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs \<Longrightarrow> Suc n \<le> Suc (n + k) \<and> set tS \<subseteq> set (S' # tS)
 2. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> - C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(r, gst', f)]} \<and> sst' \<in> P \<inter> - C \<and> sst' \<in> I \<and> eqs gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<inter> - C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(r, gst', f)]} \<and> sst' \<in> P \<inter> - C \<and> sst' \<in> I \<and> eqs gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<and> sst \<notin> C; sst \<in> I; eqs gst sst; \<not> cond gst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> (\<exists>gst'. exec_graph_step GGamma `` {[(NextNode m, gst, f)]} \<subseteq> {[(r, gst', f)]} \<and> sst' \<in> P \<and> sst' \<notin> C \<and> sst' \<in> I \<and> eqs gst' sst') proof (prove)
goal (1 subgoal):
 1. \<And>S' k sst gst. \<lbrakk>simpl_to_graph SGamma GGamma f (NextNode m) (add_cont (While C c) con) (Suc (n + k)) (S' # tS) P I eqs out_eqs; sst \<in> P \<and> sst \<notin> C; sst \<in> I; eqs gst sst; \<not> cond gst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (add_cont (While C c) con, Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst') \<and> sst' \<in> P \<and> sst' \<notin> C \<and> sst' \<in> I \<and> eqs gst sst' proof (prove)
goal:
No subgoals!