theory GraphRefine

lemma simpl_to_graph_steps_Fault1:
  "\<forall>s \<in> P \<inter> I. \<exists>com'. SGamma \<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F)
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n Q P I eqs out_eqs" apply (clarsimp simp: simpl_to_graph_def) apply (drule_tac x=sst in bspec, clarsimp+) apply (cut_tac \<Gamma>=SGamma and c="com'" and f=F in steps_Fault) apply (frule_tac c_trace_may_extend_steps, assumption) apply (erule(1) rtranclp_trans) apply assumption apply (clarsimp simp: c_trace_def) apply (rule exI, rule context_conjI) apply (erule(1) nat_trace_rel_final, fastforce simp: final_def) apply (simp add: trace_end_cut trace_end_match_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s\<in>P \<inter> I. \<exists>com'. SGamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F) \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>\<forall>s\<in>P \<inter> I. \<exists>com'. SGamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F); tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; 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 (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F)\<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'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F)\<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 (3 subgoals):
 1. \<And>tr gst sst n' gf' tr' n'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (?com'22 tr gst sst n' gf' tr' n'' com', ?xst'22 tr gst sst n' gf' tr' n'' com')
 2. \<And>tr gst sst n' gf' tr' n'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F)\<rbrakk> \<Longrightarrow> (?y22 tr gst sst n' gf' tr' n'' com', tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss22 tr gst sst n' gf' tr' n'' com')
 3. \<And>tr gst sst n' gf' tr' n'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (?com'22 tr gst sst n' gf' tr' n'' com', ?xst'22 tr gst sst n' gf' tr' n'' com') \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y22 tr gst sst n' gf' tr' n'' com', trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss22 tr gst sst n' gf' tr' n'' com')\<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'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F)\<rbrakk> \<Longrightarrow> (?y22 tr gst sst n' gf' tr' n'' com', tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss22 tr gst sst n' gf' tr' n'' com')
 2. \<And>tr gst sst n' gf' tr' n'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (SKIP, Fault F) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (?y22 tr gst sst n' gf' tr' n'' com', trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (?Ss22 tr gst sst n' gf' tr' n'' com')\<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'' com'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> trace' (n'' + j) = Some (SKIP, Fault F) \<and> trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set Q)\<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'' com' j trace'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault F); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set Q)\<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'' com' j trace'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault F); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set Q)\<rbrakk> \<Longrightarrow> ?tr''30 tr gst sst n' gf' tr' n'' com' j trace' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}
 2. \<And>tr gst sst n' gf' tr' n'' com' j trace'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault F); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); ?tr''30 tr gst sst n' gf' tr' n'' com' j trace' \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> ?tr''30 tr gst sst n' gf' tr' n'' com' j trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (?tr''30 tr gst sst n' gf' tr' n'' com' j trace')) proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n'' com' j trace'. \<lbrakk>tr n' = Some [(nn, 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) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}; tr' n'' = Some (com, Normal sst); SGamma\<turnstile> (com, Normal sst) \<rightarrow>\<^sup>* (com', Fault F); SGamma\<turnstile> (com', Fault F) \<rightarrow>\<^sup>* (SKIP, Fault F); trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y}; trace' (n'' + j) = Some (SKIP, Fault F); trace'|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub>; (tr, trace'|\<^bsub>{..n'' + j}\<^esub>) \<in> suffix_tuple_closure_inter (set Q); trace'|\<^bsub>{..n'' + j}\<^esub> \<in> nat_trace_rel (Not \<circ> final) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'}\<rbrakk> \<Longrightarrow> trace'|\<^bsub>{..n'' + j}\<^esub>|\<^bsub>{..n''}\<^esub> = tr'|\<^bsub>{..n''}\<^esub> \<and> trace_end_match out_eqs I (trace_end tr) (trace_end (trace'|\<^bsub>{..n'' + j}\<^esub>)) proof (prove)
goal:
No subgoals!