theory GraphRefine

lemma simpl_to_graph_While_inst:
  assumes ps: "nn = NextNode m" "GGamma f = Some gf" "function_graph gf m = Some (Cond l r cond)"
        "eq_impl nn eqs (\<lambda>gst sst. cond gst = (sst \<in> C)) (I \<inter> G)"
   and ss_eq: "eq_impl nn eqs eqs2 (I \<inter> G \<inter> C)"
      and ss: "\<And>k S. \<lbrakk> simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) (Suc (n + k)) (S # tS) G 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) (G \<inter> C) I eqs2 out_eqs"
   and ex_eq: "eq_impl nn eqs eqs3 (I \<inter> G \<inter> - C)"
      and ex: "simpl_to_graph SGamma GGamma f r (add_cont com.Skip con) (Suc n) tS (G \<inter> (- C)) I eqs3 out_eqs"
   and in_eq: "eq_impl nn eqs (\<lambda>gst sst. sst \<in> G) (I \<inter> G')"
  shows "simpl_to_graph SGamma GGamma f nn (add_cont (com.While C c) con) n tS G' I eqs out_eqs" apply (rule simpl_to_graph_weaken) apply (rule simpl_to_graph_While_lemma[where P=G], (rule ps)+) apply (rule simpl_to_graph_weaken, erule ss) apply (clarsimp simp: ss_eq[THEN eq_implD]) apply (rule simpl_to_graph_weaken, rule ex) apply (clarsimp simp: ex_eq[THEN eq_implD]) apply (clarsimp simp: in_eq[THEN eq_implD]) 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 G' I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) n tS ?Q I ?eqs2.0 out_eqs
 2. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> ?eqs2.0 gst sst \<and> sst \<in> ?Q proof (prove)
goal (3 subgoals):
 1. \<And>k S. simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f l (add_cont (c;;
While C c) con) (Suc (n + k)) (S # tS) (G \<inter> C) I eqs out_eqs
 2. simpl_to_graph SGamma GGamma f r (add_cont SKIP con) (Suc n) tS (G \<inter> - C) I eqs out_eqs
 3. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> G proof (prove)
goal (3 subgoals):
 1. \<And>k S. simpl_to_graph SGamma GGamma f nn (add_cont (While C c) con) (Suc (n + k)) (S # tS) G I eqs out_eqs \<Longrightarrow> \<forall>gst sst. eqs gst sst \<and> sst \<in> G \<inter> C \<and> sst \<in> I \<longrightarrow> eqs2 gst sst \<and> sst \<in> G \<inter> C
 2. simpl_to_graph SGamma GGamma f r (add_cont SKIP con) (Suc n) tS (G \<inter> - C) I eqs out_eqs
 3. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> G proof (prove)
goal (2 subgoals):
 1. simpl_to_graph SGamma GGamma f r (add_cont SKIP con) (Suc n) tS (G \<inter> - C) I eqs out_eqs
 2. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> G proof (prove)
goal (2 subgoals):
 1. \<forall>gst sst. eqs gst sst \<and> sst \<in> G \<inter> - C \<and> sst \<in> I \<longrightarrow> eqs3 gst sst \<and> sst \<in> G \<inter> - C
 2. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> G proof (prove)
goal (1 subgoal):
 1. \<forall>gst sst. eqs gst sst \<and> sst \<in> G' \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> G proof (prove)
goal:
No subgoals!