theory GraphRefine

lemma simpl_to_graph_done:
  "\<lbrakk> eq_impl nn eqs out_eqs (P \<inter> I) \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf Ret (add_cont com.Skip []) n Q P I eqs out_eqs" apply (clarsimp simp: c_trace_def add_cont_Nil intro!: simpl_to_graphI) apply (frule_tac i=n' in exec_trace_step_cases) apply (rule exI, rule context_conjI) apply (erule(1) nat_trace_rel_final, simp add: final_def) apply (clarsimp simp: trace_end_cut exec_graph_step_def) apply (clarsimp simp: exec_trace_def trace_end_eq_Some
                        eq_impl_def trace_end_match_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs out_eqs (P \<inter> I) \<Longrightarrow> simpl_to_graph SGamma GGamma gf Ret (add_cont SKIP []) n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst)\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<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>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst); tr n' = None \<and> tr (Suc n') = None \<or> (\<exists>state. tr n' = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc n') = None) \<or> tr n' \<noteq> None \<and> tr (Suc n') \<noteq> None \<and> (the (tr n'), the (tr (Suc n'))) \<in> exec_graph_step GGamma\<rbrakk> \<Longrightarrow> \<exists>tr''. tr'' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<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>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst); tr n' = None \<and> tr (Suc n') = None \<or> (\<exists>state. tr n' = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc n') = None) \<or> tr n' \<noteq> None \<and> tr (Suc n') \<noteq> None \<and> (the (tr n'), the (tr (Suc n'))) \<in> exec_graph_step GGamma\<rbrakk> \<Longrightarrow> ?tr''12 tr gst sst n' gf' tr' n'' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}
 2. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst); tr n' = None \<and> tr (Suc n') = None \<or> (\<exists>state. tr n' = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc n') = None) \<or> tr n' \<noteq> None \<and> tr (Suc n') \<noteq> None \<and> (the (tr n'), the (tr (Suc n'))) \<in> exec_graph_step GGamma; ?tr''12 tr gst sst n' gf' tr' n'' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> ?tr''12 tr gst sst n' gf' tr' n''|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (?tr''12 tr gst sst n' gf' tr' n'')) proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst); tr n' = None \<and> tr (Suc n') = None \<or> (\<exists>state. tr n' = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc n') = None) \<or> tr n' \<noteq> None \<and> tr (Suc n') \<noteq> None \<and> (the (tr n'), the (tr (Suc n'))) \<in> exec_graph_step GGamma; tr'|\<^bsub>{..n''}\<^esub> \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> tr'|\<^bsub>{..n''}\<^esub>|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (tr'|\<^bsub>{..n''}\<^esub>)) proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>eq_impl nn eqs out_eqs (P \<inter> I); tr n' = Some [(Ret, gst, gf')]; sst \<in> P; sst \<in> I; eqs gst sst; n \<le> n'; n \<le> n''; tr \<in> exec_trace GGamma gf; (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; tr' n'' = Some (SKIP, Normal sst); tr (Suc n') = None; tr'|\<^bsub>{..n''}\<^esub> \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> trace_end_match out_eqs I (trace_end tr) (Some (SKIP, Normal sst)) proof (prove)
goal:
No subgoals!