theory GraphRefine

lemma simpl_to_graph_Cond:
  "\<lbrakk> nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (Cond l r cond);
        eq_impl nn eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I);
        eq_impl nn eqs eqs2 (P \<inter> I \<inter> C);
        simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs;
        eq_impl nn eqs eqs3 (P \<inter> I \<inter> (- C));
        simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (com.Cond C c d) con) n Q P I eqs out_eqs" apply clarsimp apply (rule_tac S=C in simpl_to_graph_cases) apply (erule_tac nn'=l in simpl_to_graph_step[rotated]) apply (simp add: exec_graph_step_image_node) apply (fastforce dest: eq_implD intro: step.intros add_cont_step)[1] apply (erule_tac nn'=r in simpl_to_graph_step[rotated]) apply (simp add: exec_graph_step_image_node) apply (fastforce dest: eq_implD intro: step.intros add_cont_step)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl nn eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl nn eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl nn eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (com.Cond C c d) con) n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q (P \<inter> C) I eqs out_eqs
 2. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs; sst \<in> P \<inter> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont c con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(l, gst', gf)]} \<and> sst' \<in> P \<inter> C \<and> sst' \<in> I \<and> eqs2 gst' sst'
 2. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q (P \<inter> - C) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs; sst \<in> P \<and> sst \<in> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> (cond gst \<longrightarrow> (\<exists>sst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont c con, Normal sst') \<and> sst' \<in> P \<and> sst' \<in> C \<and> sst' \<in> I \<and> eqs2 gst sst')) \<and> (\<not> cond gst \<longrightarrow> (\<exists>sst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont c con, Normal sst') \<and> r = l \<and> sst' \<in> P \<and> sst' \<in> C \<and> sst' \<in> I \<and> eqs2 gst sst'))
 2. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q (P \<inter> - C) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); simpl_to_graph SGamma GGamma gf r (add_cont d con) (Suc n) Q (P \<inter> - C) I eqs3 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (com.Cond C c d) con) n Q (P \<inter> - C) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); sst \<in> P \<inter> - C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont d con, Normal sst') \<and> exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(r, gst', gf)]} \<and> sst' \<in> P \<inter> - C \<and> sst' \<in> I \<and> eqs3 gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; GGamma gf = Some gfc; function_graph gfc m = Some (node.Cond l r cond); eq_impl (NextNode m) eqs (\<lambda>gst sst. l \<noteq> r \<longrightarrow> cond gst = (sst \<in> C)) (P \<inter> I); eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> C); simpl_to_graph SGamma GGamma gf l (add_cont c con) (Suc n) Q (P \<inter> C) I eqs2 out_eqs; eq_impl (NextNode m) eqs eqs3 (P \<inter> I \<inter> - C); sst \<in> P \<and> sst \<notin> C; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> (cond gst \<longrightarrow> (\<exists>sst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont d con, Normal sst') \<and> l = r \<and> sst' \<in> P \<and> sst' \<notin> C \<and> sst' \<in> I \<and> eqs3 gst sst')) \<and> (\<not> cond gst \<longrightarrow> (\<exists>sst'. SGamma\<turnstile> (add_cont (com.Cond C c d) con, Normal sst) \<rightarrow> (add_cont d con, Normal sst') \<and> sst' \<in> P \<and> sst' \<notin> C \<and> sst' \<in> I \<and> eqs3 gst sst')) proof (prove)
goal:
No subgoals!