kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphRefine

lemma simpl_to_graph_ge_subset:
  "simpl_to_graph SGamma GGamma gf nn com n traces' P I inp_eqs out_eqs
    \<Longrightarrow> n' \<ge> n \<and> set traces' \<subseteq> set traces
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' traces P I inp_eqs out_eqs" apply (simp add: simpl_to_graph_def suffix_tuple_closure_inter_def Ball_def) apply (erule mp[rotated], intro all_mono ex_mono imp_mono conj_mono imp_refl,
      simp_all) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simpl_to_graph SGamma GGamma gf nn com n traces' P I inp_eqs out_eqs; n \<le> n' \<and> set traces' \<subseteq> set traces\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n' traces P I inp_eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>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> (\<forall>x. x \<in> (\<lambda>S. {(y, tr). \<exists>k. (y, tr|\<^bsub>{..k}\<^esub>) \<in> S}) ` set traces' \<longrightarrow> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> x) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<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'')); n \<le> n' \<and> set traces' \<subseteq> set traces\<rbrakk> \<Longrightarrow> \<forall>tr gst sst n'a gf' tr' n''. tr n'a = Some [(nn, gst, gf')] \<and> sst \<in> P \<and> sst \<in> I \<and> inp_eqs gst sst \<and> n' \<le> n'a \<and> n' \<le> n'' \<and> tr \<in> exec_trace GGamma gf \<and> (\<forall>x. x \<in> (\<lambda>S. {(y, tr). \<exists>k. (y, tr|\<^bsub>{..k}\<^esub>) \<in> S}) ` set traces \<longrightarrow> (tr, tr'|\<^bsub>{..n''}\<^esub>) \<in> x) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<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 (1 subgoal):
 1. \<And>x. n \<le> n' \<and> set traces' \<subseteq> set traces \<Longrightarrow> x \<in> (\<lambda>S. {(y, tr). \<exists>k. (y, tr|\<^bsub>{..k}\<^esub>) \<in> S}) ` set traces' \<longrightarrow> x \<in> (\<lambda>S. {(y, tr). \<exists>k. (y, tr|\<^bsub>{..k}\<^esub>) \<in> S}) ` set traces proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma nat_trace_rel_to_relpow:
  "trace \<in> nat_trace_rel cont R
    \<Longrightarrow> trace i = Some x
    \<Longrightarrow> trace (i + j) = Some y
    \<Longrightarrow> (x, y) \<in> R ^^ j" apply (induct j arbitrary: y) apply simp apply atomize apply (clarsimp simp: nat_trace_rel_def) apply (drule_tac x="i + j" in spec, clarsimp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ j proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + 0) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ 0
 2. \<And>j y. \<lbrakk>\<And>y. \<lbrakk>trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ j; trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + Suc j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ Suc j proof (prove)
goal (1 subgoal):
 1. \<And>j y. \<lbrakk>\<And>y. \<lbrakk>trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ j; trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + Suc j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ Suc j proof (prove)
goal (1 subgoal):
 1. \<And>j y. \<lbrakk>\<forall>y. trace \<in> nat_trace_rel cont R \<longrightarrow> trace i = Some x \<longrightarrow> trace (i + j) = Some y \<longrightarrow> (x, y) \<in> R ^^ j; trace \<in> nat_trace_rel cont R; trace i = Some x; trace (i + Suc j) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ Suc j proof (prove)
goal (1 subgoal):
 1. \<And>j y. \<lbrakk>\<forall>y. trace (i + j) = Some y \<longrightarrow> (x, y) \<in> R ^^ j; \<forall>n. (trace n = None \<longrightarrow> trace (Suc n) = None) \<and> ((\<exists>y. trace (Suc n) = Some y) \<longrightarrow> (the (trace n), the (trace (Suc n))) \<in> R) \<and> ((\<exists>y. trace n = Some y) \<and> cont (the (trace n)) \<longrightarrow> (\<exists>y. trace (Suc n) = Some y)); trace i = Some x; trace (Suc (i + j)) = Some y\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ j O R proof (prove)
goal (1 subgoal):
 1. \<And>j y ya. \<lbrakk>(x, ya) \<in> R ^^ j; trace i = Some x; trace (Suc (i + j)) = Some y; (ya, y) \<in> R; trace (i + j) = Some ya\<rbrakk> \<Longrightarrow> (x, y) \<in> R ^^ j O R proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma c_trace_may_extend_steps:
  "trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
    \<Longrightarrow> trace i = Some (com, Normal st)
    \<Longrightarrow> \<Gamma> \<turnstile> (com, Normal st) \<rightarrow>\<^sup>* (com', xst')
    \<Longrightarrow> (y, restrict_map trace {..i}) \<in> suffix_tuple_closure_inter Ss
    \<Longrightarrow> \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma> \<turnstile> x \<rightarrow> y}
      \<and> trace' (i + j) = Some (com', xst')
      \<and> restrict_map trace' {.. i} = restrict_map trace {.. i}
      \<and> (y, restrict_map trace' {.. i + j}) \<in> suffix_tuple_closure_inter Ss" apply (clarsimp simp: rtranclp_power) apply (blast intro: c_trace_may_extend) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); \<Gamma>\<turnstile> (com, Normal st) \<rightarrow>\<^sup>* (com', xst'); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss\<rbrakk> \<Longrightarrow> \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>trace \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y}; trace i = Some (com, Normal st); (y, trace|\<^bsub>{..i}\<^esub>) \<in> suffix_tuple_closure_inter Ss; (step \<Gamma> ^^ n) (com, Normal st) (com', xst')\<rbrakk> \<Longrightarrow> \<exists>j trace'. trace' \<in> nat_trace_rel (\<lambda>x. False) {(x, y). \<Gamma>\<turnstile> x \<rightarrow> y} \<and> trace' (i + j) = Some (com', xst') \<and> trace'|\<^bsub>{..i}\<^esub> = trace|\<^bsub>{..i}\<^esub> \<and> (y, trace'|\<^bsub>{..i + j}\<^esub>) \<in> suffix_tuple_closure_inter Ss proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma restrict_map_prefix_eq: "(restrict_map tr {..n} = restrict_map tr' {..n})
    = (\<forall>i \<le> n. tr i = tr' i)" by (auto simp add: fun_eq_iff restrict_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (tr|\<^bsub>{..n}\<^esub> = tr'|\<^bsub>{..n}\<^esub>) = (\<forall>i\<le>n. tr i = tr' i)
theory GraphRefine

lemma restrict_map_eq_mono:
  "i \<le> j \<Longrightarrow> restrict_map tr {..j} = restrict_map tr' {..j}
    \<Longrightarrow> restrict_map tr {.. (i :: 'a :: linorder)} = restrict_map tr' {..i}" unfolding restrict_map_prefix_eq by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; tr|\<^bsub>{..j}\<^esub> = tr'|\<^bsub>{..j}\<^esub>\<rbrakk> \<Longrightarrow> tr|\<^bsub>{..i}\<^esub> = tr'|\<^bsub>{..i}\<^esub> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; \<forall>i\<le>j. tr i = tr' i\<rbrakk> \<Longrightarrow> \<forall>ia\<le>i. tr ia = tr' ia
theory GraphRefine

lemma simpl_to_graph_step_R:
  "(\<And>sst gst. sst \<in> P \<Longrightarrow> sst \<in> I \<Longrightarrow> inp_eqs gst sst
        \<Longrightarrow> \<exists>sst'. (step SGamma) (com, Normal sst) (com', Normal sst')
            \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst')
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com' n traces P' 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_graph_step_general[rotated, where i=0 and j=1]) apply simp+ apply (simp add: eq_OO) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst'; simpl_to_graph SGamma GGamma gf nn com' n traces P' 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 (2 subgoals):
 1. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst'; simpl_to_graph SGamma GGamma gf nn com' n traces P' I inp_eqs' out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf ?nn' ?com' (n + min 0 1) traces ?P' I ?inp_eqs' out_eqs
 2. \<And>sst gst. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst'; simpl_to_graph SGamma GGamma gf nn com' n traces P' I inp_eqs' out_eqs; sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 1) (com, Normal sst) (?com', Normal sst') \<and> (exec_graph_step GGamma ^^ 0) `` {[(nn, gst, gf)]} \<subseteq> {[(?nn', gst', gf)]} \<and> (\<forall>k<0. \<forall>st'. ([(nn, gst, gf)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st') \<and> sst' \<in> ?P' \<and> sst' \<in> I \<and> ?inp_eqs' gst' sst' proof (prove)
goal (1 subgoal):
 1. \<And>sst gst. \<lbrakk>\<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. SGamma\<turnstile> (com, Normal sst) \<rightarrow> (com', Normal sst') \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst'; simpl_to_graph SGamma GGamma gf nn com' n traces P' I inp_eqs' out_eqs; sst \<in> P; sst \<in> I; inp_eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst'. ((=) OO step SGamma) (com, Normal sst) (com', Normal sst') \<and> sst' \<in> P' \<and> sst' \<in> I \<and> inp_eqs' gst sst' proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma trace_end_None_ge_seq:
  "tr \<in> nat_trace_rel c R
    \<Longrightarrow> \<forall>i. \<exists>j \<ge> i. tr j \<noteq> None
    \<Longrightarrow> trace_end tr = None" apply (clarsimp simp: trace_end_def) apply (drule_tac x=n in spec) apply (drule(1) trace_None_dom_subset) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; \<forall>i. \<exists>j\<ge>i. tr j \<noteq> None\<rbrakk> \<Longrightarrow> trace_end tr = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel c R; \<forall>i. \<exists>j\<ge>i. \<exists>y. tr j = Some y; tr n = None\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel c R; tr n = None; \<exists>j\<ge>n. \<exists>y. tr j = Some y\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> nat_trace_rel c R; \<exists>j\<ge>n. \<exists>y. tr j = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = None proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma restrict_map_eq_Some_le:
  "(restrict_map tr {..n} = restrict_map tr' {..m})
    \<Longrightarrow> tr' (m :: nat) = Some v
    \<Longrightarrow> n \<ge> m \<and> (\<forall>k \<le> m. restrict_map tr {..k} = restrict_map tr' {..k})" apply (frule_tac x=m in fun_cong, simp(no_asm_use) add: restrict_map_def) apply (simp split: if_split_asm) apply (auto simp: fun_eq_iff split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr|\<^bsub>{..n}\<^esub> = tr'|\<^bsub>{..m}\<^esub>; tr' m = Some v\<rbrakk> \<Longrightarrow> m \<le> n \<and> (\<forall>k\<le>m. tr|\<^bsub>{..k}\<^esub> = tr'|\<^bsub>{..k}\<^esub>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. if x \<le> n then tr x else None) = (\<lambda>x. if x \<le> m then tr' x else None); tr' m = Some v; (if m \<le> n then tr m else None) = tr' m\<rbrakk> \<Longrightarrow> m \<le> n \<and> (\<forall>k\<le>m. (\<lambda>x. if x \<le> k then tr x else None) = (\<lambda>x. if x \<le> k then tr' x else None)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<lambda>x. if x \<le> n then tr x else None) = (\<lambda>x. if x \<le> m then tr' x else None); tr' m = Some v; m \<le> n; tr m = Some v\<rbrakk> \<Longrightarrow> \<forall>k\<le>m. (\<lambda>x. if x \<le> k then tr x else None) = (\<lambda>x. if x \<le> k then tr' x else None) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma suffix_tuple_closure_inter_insert:
  "(x, tr) \<in> suffix_tuple_closure_inter (insert S Ss)
    = ((\<exists>k. (x, restrict_map tr {..k}) \<in> S) \<and> (x, tr) \<in> suffix_tuple_closure_inter Ss)" by (simp add: suffix_tuple_closure_inter_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, tr) \<in> suffix_tuple_closure_inter (insert S Ss)) = ((\<exists>k. (x, tr|\<^bsub>{..k}\<^esub>) \<in> S) \<and> (x, tr) \<in> suffix_tuple_closure_inter Ss)
theory GraphRefine

lemma eq_implD:
  "\<lbrakk> eq_impl addr eqs eqs2 S; eqs gst sst; sst \<in> S \<rbrakk>
        \<Longrightarrow> eqs2 gst sst" by (simp add: eq_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl addr eqs eqs2 S; eqs gst sst; sst \<in> S\<rbrakk> \<Longrightarrow> eqs2 gst sst
theory GraphRefine

lemma exec_graph_step_image_node:
  "GGamma f = Some gf \<Longrightarrow> function_graph gf n = Some node
    \<Longrightarrow> exec_graph_step GGamma `` {[(NextNode n, gst, f)]}
      = exec_node GGamma gst node [(NextNode n, gst, f)]" by (cases gf, simp add: exec_graph_step_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GGamma f = Some gf; function_graph gf n = Some node\<rbrakk> \<Longrightarrow> exec_graph_step GGamma `` {[(NextNode n, gst, f)]} = exec_node GGamma gst node [(NextNode n, gst, f)]
theory GraphRefine

lemma add_cont_Cons:
  "add_cont c (Inl d # cont) = add_cont (c ;; d) cont"
  "add_cont c (Inr d # cont) = add_cont (com.Catch c d) cont" by (simp_all add: add_cont_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_cont c (Inl d # cont) = add_cont (c;;
d) cont &&& add_cont c (Inr d # cont) = add_cont (TRY
  c
CATCH d
END) cont
theory GraphRefine

lemma add_cont_Nil:
  "add_cont c [] = c" by (simp add: add_cont_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. add_cont c [] = c
theory GraphRefine

lemma add_cont_step:
  "SGamma \<turnstile> (com, s) \<rightarrow> (com', s')
    \<Longrightarrow> SGamma \<turnstile> (add_cont com con, s) \<rightarrow> (add_cont com' con, s')" apply (induct con rule: rev_induct) apply (simp add: add_cont_def) apply (simp add: add_cont_def step.intros split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SGamma\<turnstile> (com, s) \<rightarrow> (com', s') \<Longrightarrow> SGamma\<turnstile> (add_cont com con, s) \<rightarrow> (add_cont com' con, s') proof (prove)
goal (2 subgoals):
 1. SGamma\<turnstile> (com, s) \<rightarrow> (com', s') \<Longrightarrow> SGamma\<turnstile> (add_cont com [], s) \<rightarrow> (add_cont com' [], s')
 2. \<And>x xs. \<lbrakk>SGamma\<turnstile> (com, s) \<rightarrow> (com', s') \<Longrightarrow> SGamma\<turnstile> (add_cont com xs, s) \<rightarrow> (add_cont com' xs, s'); SGamma\<turnstile> (com, s) \<rightarrow> (com', s')\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont com (xs @ [x]), s) \<rightarrow> (add_cont com' (xs @ [x]), s') proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>SGamma\<turnstile> (com, s) \<rightarrow> (com', s') \<Longrightarrow> SGamma\<turnstile> (add_cont com xs, s) \<rightarrow> (add_cont com' xs, s'); SGamma\<turnstile> (com, s) \<rightarrow> (com', s')\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont com (xs @ [x]), s) \<rightarrow> (add_cont com' (xs @ [x]), s') proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_weaken[rotated]:
  assumes eqs: "\<forall>gst sst. eqs gst sst \<and> sst \<in> P \<and> sst \<in> I
            \<longrightarrow> eqs2 gst sst \<and> sst \<in> Q"
  shows "simpl_to_graph SGamma GGamma gf nn com n tS Q I eqs2 out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs" using eqs apply (clarsimp simp add: simpl_to_graph_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n tS Q I eqs2 out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs proof (prove)
using this:
\<forall>gst sst. eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<longrightarrow> eqs2 gst sst \<and> sst \<in> Q

goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma gf nn com n tS Q I eqs2 out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>tr gst sst n' gf' tr' n''. \<lbrakk>\<forall>tr gst sst n' gf' tr' n''. tr n' = Some [(nn, gst, gf')] \<and> sst \<in> Q \<and> sst \<in> I \<and> eqs2 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 tS) \<and> tr' \<in> nat_trace_rel (\<lambda>x. False) {(cfg, cfg'). SGamma\<turnstile> cfg \<rightarrow> cfg'} \<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'')); \<forall>gst sst. eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<longrightarrow> eqs2 gst sst \<and> sst \<in> Q; 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 tS); 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:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_weaken_eq_impl:
  "eq_impl nn eqs eqs2 (I \<inter> P)
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs2 out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs" apply (erule simpl_to_graph_weaken) apply (simp add: eq_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>eq_impl nn eqs eqs2 (I \<inter> P); simpl_to_graph SGamma GGamma gf nn com n tS P I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n tS P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs eqs2 (I \<inter> P) \<Longrightarrow> \<forall>gst sst. eqs gst sst \<and> sst \<in> P \<and> sst \<in> I \<longrightarrow> eqs2 gst sst \<and> sst \<in> P proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma use_simpl_to_graph_While_assum:
  "\<lbrakk> simpl_to_graph SGamma GGamma f nn com n tS P I eqs out_eqs;
    n \<le> n' \<and> set tS \<subseteq> set tS';
    eq_impl nn eqs (\<lambda>gst sst. sst \<in> P) (Q \<inter> I) \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn com n' tS' Q I eqs out_eqs" apply (erule simpl_to_graph_ge_subset[rotated]) apply (erule simpl_to_graph_weaken) apply (auto simp add: eq_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simpl_to_graph SGamma GGamma f nn com n tS P I eqs out_eqs; n \<le> n' \<and> set tS \<subseteq> set tS'; eq_impl nn eqs (\<lambda>gst sst. sst \<in> P) (Q \<inter> I)\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn com n' tS' Q I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simpl_to_graph SGamma GGamma f nn com n tS P I eqs out_eqs; eq_impl nn eqs (\<lambda>gst sst. sst \<in> P) (Q \<inter> I)\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma f nn com n tS Q I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs (\<lambda>gst sst. sst \<in> P) (Q \<inter> I) \<Longrightarrow> \<forall>gst sst. eqs gst sst \<and> sst \<in> Q \<and> sst \<in> I \<longrightarrow> eqs gst sst \<and> sst \<in> P proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_Skip_immediate:
  "simpl_to_graph SGamma GGamma f nn (add_cont c con) n tS P I eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Skip (Inl c # con)) n tS P I eqs out_eqs"
  "simpl_to_graph SGamma GGamma f nn (add_cont com.Skip con) n tS P I eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Skip (Inr c # con)) n tS P I eqs out_eqs" apply (safe elim!: simpl_to_graph_step_R_unchanged[rotated]) apply (auto simp: add_cont_Cons intro: add_cont_step step.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (simpl_to_graph SGamma GGamma f nn (add_cont c con) n tS P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont SKIP (Inl c # con)) n tS P I eqs out_eqs) &&& (simpl_to_graph SGamma GGamma f nn (add_cont SKIP con) n tS P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont SKIP (Inr c # con)) n tS P I eqs out_eqs) proof (prove)
goal (2 subgoals):
 1. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont SKIP (Inl c # con), Normal sst) \<rightarrow> (add_cont c con, Normal sst)
 2. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont SKIP (Inr c # con), Normal sst) \<rightarrow> (add_cont SKIP con, Normal sst) proof (prove)
goal:
No subgoals!