theory GraphRefine

lemma simpl_to_graph_induct:
  assumes Suc: "\<And>S' k. simpl_to_graph SGamma GGamma gf nn com (Suc n + k) (S' # S) P I inp_eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (n + k) (S' # S) P I inp_eqs out_eqs"
  shows "simpl_to_graph SGamma GGamma gf nn com n S P I inp_eqs out_eqs" apply (rule simpl_to_graphI) apply (cut_tac tr=tr and n=n and S=S in simpl_to_graph_induct_proof) apply (cut_tac S'=S' and k="n'a - n" in Suc) apply simp+ apply (erule simpl_to_graphD) apply (simp add: suffix_tuple_closure_inter_insert) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n S P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. 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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst) \<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'' S' n'a. \<lbrakk>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); n \<le> n'a; simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') (Suc n'a) (S' # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')\<rbrakk> \<Longrightarrow> simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') n'a (S' # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')
 2. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') n ({tr} \<times> UNIV # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')\<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'' S' n'a. \<lbrakk>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); n \<le> n'a; simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') (Suc n'a) (S' # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com (Suc n + (n'a - n)) (S' # S) P I inp_eqs out_eqs
 2. \<And>tr gst sst n' gf' tr' n'' S' n'a. \<lbrakk>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); n \<le> n'a; simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') (Suc n'a) (S' # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n''); simpl_to_graph SGamma GGamma gf nn com (n + (n'a - n)) (S' # S) P I inp_eqs out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') n'a (S' # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')
 3. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); simpl_to_graph (?SGamma2 tr gst sst n' gf' tr' n'') (?GGamma2 tr gst sst n' gf' tr' n'') (?gf2 tr gst sst n' gf' tr' n'') (?nn2 tr gst sst n' gf' tr' n'') (?com2 tr gst sst n' gf' tr' n'') n ({tr} \<times> UNIV # S) (?P2 tr gst sst n' gf' tr' n'') (?I2 tr gst sst n' gf' tr' n'') (?inp_eqs2 tr gst sst n' gf' tr' n'') (?out_eqs2 tr gst sst n' gf' tr' n'')\<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>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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst); simpl_to_graph SGamma GGamma gf nn com n ({tr} \<times> UNIV # S) P I inp_eqs out_eqs\<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''. 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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst) \<Longrightarrow> tr (?n'6 tr gst sst n' gf' tr' n'') = Some [(nn, ?gst6 tr gst sst n' gf' tr' n'', ?gf'6 tr gst sst n' gf' tr' n'')] \<and> ?sst6 tr gst sst n' gf' tr' n'' \<in> P \<and> ?sst6 tr gst sst n' gf' tr' n'' \<in> I \<and> inp_eqs (?gst6 tr gst sst n' gf' tr' n'') (?sst6 tr gst sst n' gf' tr' n'') \<and> n \<le> ?n'6 tr gst sst n' gf' tr' n'' \<and> n \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> suffix_tuple_closure_inter (set ({tr} \<times> UNIV # S)) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal (?sst6 tr gst sst n' gf' tr' n'')) proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. 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 S) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). SGamma\<turnstile> x \<rightarrow> y} \<and> tr' n'' = Some (com, Normal sst) \<Longrightarrow> tr (?n'6 tr gst sst n' gf' tr' n'') = Some [(nn, ?gst6 tr gst sst n' gf' tr' n'', ?gf'6 tr gst sst n' gf' tr' n'')] \<and> ?sst6 tr gst sst n' gf' tr' n'' \<in> P \<and> ?sst6 tr gst sst n' gf' tr' n'' \<in> I \<and> inp_eqs (?gst6 tr gst sst n' gf' tr' n'') (?sst6 tr gst sst n' gf' tr' n'') \<and> n \<le> ?n'6 tr gst sst n' gf' tr' n'' \<and> sst = ?sst6 tr gst sst n' gf' tr' n'' proof (prove)
goal:
No subgoals!