theory GraphRefine

lemma simpl_to_graph_cases:
  "simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs" apply (rule simpl_to_graphI) apply (case_tac "sst \<in> S") apply (clarsimp simp only: simpl_to_graph_def[where P="P \<inter> S"] Compl_iff Int_iff) apply (clarsimp simp only: simpl_to_graph_def[where P="P \<inter> - S"] Compl_iff Int_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs; simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs; simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs; tr n' = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I \<and> inp_eqs gst sst \<and> n \<le> n' \<and> n \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set traces) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (2 subgoals):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs; simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs; tr n' = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I \<and> inp_eqs gst sst \<and> n \<le> n' \<and> n \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set traces) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); sst \<in> S\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'')
 2. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs; simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs; tr n' = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I \<and> inp_eqs gst sst \<and> n \<le> n' \<and> n \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set traces) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); sst \<notin> S\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> S) I inp_eqs out_eqs; simpl_to_graph SGamma GGamma gf nn com n traces (P \<inter> - S) I inp_eqs out_eqs; tr n' = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I \<and> inp_eqs gst sst \<and> n \<le> n' \<and> n \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set traces) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); sst \<notin> S\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> c_trace SGamma \<and> tr''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end tr'') proof (prove)
goal:
No subgoals!