theory GraphRefine

lemma simpl_to_graph_Guard:
  "\<lbrakk> nn = NextNode m; eq_impl nn eqs eqs2 (P \<inter> I \<inter> G);
        simpl_to_graph SGamma GGamma gf nn (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (com.Guard F G c) con) n Q P I eqs out_eqs" apply clarsimp apply (rule_tac S=G in simpl_to_graph_cases) apply (rule simpl_to_graph_step_R_unchanged[rotated]) apply (erule simpl_to_graph_weaken) apply (simp add: eq_impl_def) apply (rule add_cont_step) apply (blast intro: step.Guard) apply (rule simpl_to_graph_steps_Fault) apply (blast intro: step.GuardFault) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; eq_impl nn eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf nn (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn (add_cont (Guard F G c) con) n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> G) I eqs out_eqs
 2. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) ?com'2 n Q (P \<inter> G) I eqs out_eqs
 2. \<And>sst gst. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs; sst \<in> P \<inter> G; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (Guard F G c) con, Normal sst) \<rightarrow> (?com'2, Normal sst)
 3. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (3 subgoals):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G)\<rbrakk> \<Longrightarrow> \<forall>gst sst. eqs gst sst \<and> sst \<in> P \<inter> G \<and> sst \<in> I \<longrightarrow> eqs2 gst sst \<and> sst \<in> G \<inter> P
 2. \<And>sst gst. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs; sst \<in> P \<inter> G; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (Guard F G c) con, Normal sst) \<rightarrow> (add_cont c con, Normal sst)
 3. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs; sst \<in> P \<inter> G; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont (Guard F G c) con, Normal sst) \<rightarrow> (add_cont c con, Normal sst)
 2. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs; sst \<in> P \<inter> G; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (Guard F G c, Normal sst) \<rightarrow> (c, Normal sst)
 2. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont (Guard F G c) con) n Q (P \<inter> - G) I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>nn = NextNode m; eq_impl (NextNode m) eqs eqs2 (P \<inter> I \<inter> G); simpl_to_graph SGamma GGamma gf (NextNode m) (add_cont c con) n Q (G \<inter> P) I eqs2 out_eqs\<rbrakk> \<Longrightarrow> \<forall>s\<in>P \<inter> - G \<inter> I. \<exists>com'. SGamma\<turnstile> (Guard F G c, Normal s) \<rightarrow>\<^sup>* (com', Fault ?F28) proof (prove)
goal:
No subgoals!