kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphRefine

lemma simpl_to_graph_Throw_immediate:
  "simpl_to_graph SGamma GGamma f nn (add_cont com.Throw con) n tS P I eqs out_eqs
    \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont com.Throw (Inl c # con)) n tS P I eqs out_eqs"
  "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.Throw (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 THROW con) n tS P I eqs out_eqs \<Longrightarrow> simpl_to_graph SGamma GGamma f nn (add_cont THROW (Inl c # con)) n tS P I eqs out_eqs) &&& (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 THROW (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 THROW (Inl c # con), Normal sst) \<rightarrow> (add_cont THROW con, Normal sst)
 2. \<And>sst gst. \<lbrakk>sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont THROW (Inr c # con), Normal sst) \<rightarrow> (add_cont c con, Normal sst) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_Seq:
  "simpl_to_graph SGamma GGamma f nn (add_cont (c ;; d) con) n tS P I eqs out_eqs
    = simpl_to_graph SGamma GGamma f nn (add_cont c (Inl d # con)) n tS P I eqs out_eqs" by (simp add: add_cont_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma f nn (add_cont (c;;
d) con) n tS P I eqs out_eqs = simpl_to_graph SGamma GGamma f nn (add_cont c (Inl d # con)) n tS P I eqs out_eqs
theory GraphRefine

lemma simpl_to_graph_Catch:
  "simpl_to_graph SGamma GGamma f nn (add_cont (com.Catch c d) con) n tS P I eqs out_eqs
    = simpl_to_graph SGamma GGamma f nn (add_cont c (Inr d # con)) n tS P I eqs out_eqs" by (simp add: add_cont_Cons)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_to_graph SGamma GGamma f nn (add_cont (TRY
  c
CATCH d
END) con) n tS P I eqs out_eqs = simpl_to_graph SGamma GGamma f nn (add_cont c (Inr d # con)) n tS P I eqs out_eqs
theory GraphRefine

lemma no_next_step: "eq_impl nn' eqs (\<lambda>gst' sst'.
        ((exec_graph_step GGamma) ^^ 0) `` {[(nn, gst', fn)]} \<subseteq> {[(nn, gst', fn)]}
        \<and> (\<forall>k < (0 :: nat). \<forall>st'. ([(nn, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
        \<longrightarrow> continuing st')) P" by (simp add: eq_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eq_impl nn' eqs (\<lambda>gst' sst'. (exec_graph_step GGamma ^^ 0) `` {[(nn, gst', fn)]} \<subseteq> {[(nn, gst', fn)]} \<and> (\<forall>k<0. \<forall>st'. ([(nn, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')) P
theory GraphRefine

lemma basic_next_step: "GGamma fn = Some gf \<Longrightarrow> function_graph gf m = Some (Basic nn' upds)
    \<Longrightarrow> eq_impl nn'' eqs (\<lambda>gst' sst'.
        ((exec_graph_step GGamma) ^^ 1) `` {[(NextNode m, gst', fn)]} \<subseteq> {[(nn', upd_vars upds gst', fn)]}
        \<and> (\<forall>k < 1. \<forall>st'. ([(NextNode m, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k
        \<longrightarrow> continuing st')) P" apply (clarsimp simp: eq_impl_def simp del: imp_disjL) apply (clarsimp simp: exec_graph_step_def K_def split: graph_function.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GGamma fn = Some gf; function_graph gf m = Some (node.Basic nn' upds)\<rbrakk> \<Longrightarrow> eq_impl nn'' eqs (\<lambda>gst' sst'. (exec_graph_step GGamma ^^ 1) `` {[(NextNode m, gst', fn)]} \<subseteq> {[(nn', upd_vars upds gst', fn)]} \<and> (\<forall>k<1. \<forall>st'. ([(NextNode m, gst', fn)], st') \<in> exec_graph_step GGamma ^^ k \<longrightarrow> continuing st')) P proof (prove)
goal (1 subgoal):
 1. \<And>gst sst x. \<lbrakk>GGamma fn = Some gf; function_graph gf m = Some (node.Basic nn' upds); eqs gst sst; sst \<in> P; ([(NextNode m, gst, fn)], x) \<in> exec_graph_step GGamma\<rbrakk> \<Longrightarrow> x = [(nn', upd_vars upds gst, fn)] proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma rtranclp_respects_fun:
  assumes respects: "\<And>x y. R x y \<Longrightarrow> R (f x) (f y)"
  shows "R\<^sup>*\<^sup>* x y \<Longrightarrow> R\<^sup>*\<^sup>* (f x) (f y)" apply (induct rule: rtranclp.induct) apply (fastforce intro: respects elim: rtranclp_trans)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* x y \<Longrightarrow> R\<^sup>*\<^sup>* (f x) (f y) proof (prove)
goal (2 subgoals):
 1. \<And>a. R\<^sup>*\<^sup>* (f a) (f a)
 2. \<And>a b c. \<lbrakk>R\<^sup>*\<^sup>* a b; R\<^sup>*\<^sup>* (f a) (f b); R b c\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* (f a) (f c) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma add_cont_steps:
  "\<Gamma> \<turnstile> (com, xs) \<rightarrow>\<^sup>* (com', xs')
    \<Longrightarrow> \<Gamma> \<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs')" apply (drule_tac f="\<lambda>(a, b). (add_cont a con, b)" in rtranclp_respects_fun[rotated]) apply clarsimp apply (erule add_cont_step) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (com, xs) \<rightarrow>\<^sup>* (com', xs') \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs') proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<Gamma>\<turnstile> x \<rightarrow> y \<Longrightarrow> \<Gamma>\<turnstile> (case x of (a, b) \<Rightarrow> (add_cont a con, b)) \<rightarrow> (case y of (a, b) \<Rightarrow> (add_cont a con, b))
 2. \<Gamma>\<turnstile> (case (com, xs) of (a, b) \<Rightarrow> (add_cont a con, b)) \<rightarrow>\<^sup>* (case (com', xs') of (a, b) \<Rightarrow> (add_cont a con, b)) \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs') proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<Gamma>\<turnstile> (a, b) \<rightarrow> (aa, ba) \<Longrightarrow> \<Gamma>\<turnstile> (add_cont a con, b) \<rightarrow> (add_cont aa con, ba)
 2. \<Gamma>\<turnstile> (case (com, xs) of (a, b) \<Rightarrow> (add_cont a con, b)) \<rightarrow>\<^sup>* (case (com', xs') of (a, b) \<Rightarrow> (add_cont a con, b)) \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs') proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (case (com, xs) of (a, b) \<Rightarrow> (add_cont a con, b)) \<rightarrow>\<^sup>* (case (com', xs') of (a, b) \<Rightarrow> (add_cont a con, b)) \<Longrightarrow> \<Gamma>\<turnstile> (add_cont com con, xs) \<rightarrow>\<^sup>* (add_cont com' con, xs') proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_steps_Fault:
  "\<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 (add_cont com con) n Q P I eqs out_eqs" apply (clarsimp intro!: simpl_to_graph_steps_Fault1) apply (drule_tac x=s in bspec, clarsimp+) apply (rule exI) apply (erule add_cont_steps) 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 (add_cont com con) n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s\<in>P \<inter> I. \<exists>com'. SGamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F); s \<in> P; s \<in> I\<rbrakk> \<Longrightarrow> \<exists>com'. SGamma\<turnstile> (add_cont com con, Normal s) \<rightarrow>\<^sup>* (com', Fault ?F) proof (prove)
goal (1 subgoal):
 1. \<And>s com'. \<lbrakk>s \<in> P; s \<in> I; SGamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F)\<rbrakk> \<Longrightarrow> \<exists>com'. SGamma\<turnstile> (add_cont com con, Normal s) \<rightarrow>\<^sup>* (com', Fault ?F) proof (prove)
goal (1 subgoal):
 1. \<And>s com'. \<lbrakk>s \<in> P; s \<in> I; SGamma\<turnstile> (com, Normal s) \<rightarrow>\<^sup>* (com', Fault F)\<rbrakk> \<Longrightarrow> SGamma\<turnstile> (add_cont com con, Normal s) \<rightarrow>\<^sup>* (?com'6 s com', Fault ?F) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma eq_impl_refl:
  "eq_impl nn eqs eqs P" by (simp add: eq_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs eqs P
theory GraphRefine

lemma simpl_to_graph_noop_Basic:
  "\<lbrakk> GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds);
        eq_impl nn eqs (\<lambda>gst sst. eqs2 (upd_vars upds gst) sst) (P \<inter> I);
        simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs" apply (rule simpl_to_graph_step_general[where i=1 and j=0, rotated]) apply simp+ apply (simp add: exec_graph_step_image_node eq_impl_def K_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds); eq_impl nn eqs (\<lambda>gst. eqs2 (upd_vars upds gst)) (P \<inter> I); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs proof (prove)
goal (2 subgoals):
 1. \<lbrakk>GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds); eq_impl nn eqs (\<lambda>gst. eqs2 (upd_vars upds gst)) (P \<inter> I); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf ?nn' ?com' (n + min 1 0) Q ?P' I ?inp_eqs' out_eqs
 2. \<And>sst gst. \<lbrakk>GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds); eq_impl nn eqs (\<lambda>gst. eqs2 (upd_vars upds gst)) (P \<inter> I); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>sst' gst'. (step SGamma ^^ 0) (c, Normal sst) (?com', Normal sst') \<and> (exec_graph_step GGamma ^^ 1) `` {[(NextNode m, gst, gf)]} \<subseteq> {[(?nn', gst', gf)]} \<and> (\<forall>k<1. \<forall>st'. ([(NextNode m, 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>GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn upds); eq_impl nn eqs (\<lambda>gst. eqs2 (upd_vars upds gst)) (P \<inter> I); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs; sst \<in> P; sst \<in> I; eqs gst sst\<rbrakk> \<Longrightarrow> \<exists>gst'. exec_graph_step GGamma `` {[(NextNode m, gst, gf)]} \<subseteq> {[(nn, gst', gf)]} \<and> eqs2 gst' sst proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_noop:
  "\<lbrakk> GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn []);
        simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs;
        eq_impl nn eqs eqs2 (P \<inter> I) \<rbrakk>
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs" apply (erule(1) simpl_to_graph_noop_Basic, simp_all) apply (simp add: upd_vars_def save_vals_def eq_impl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>GGamma gf = Some gfc; function_graph gfc m = Some (node.Basic nn []); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs; eq_impl nn eqs eqs2 (P \<inter> I)\<rbrakk> \<Longrightarrow> simpl_to_graph SGamma GGamma gf (NextNode m) c n Q P I eqs out_eqs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>function_graph gfc m = Some (node.Basic nn []); simpl_to_graph SGamma GGamma gf nn c n Q P I eqs2 out_eqs; eq_impl nn eqs eqs2 (P \<inter> I)\<rbrakk> \<Longrightarrow> eq_impl nn eqs (\<lambda>gst. eqs2 (upd_vars [] gst)) (P \<inter> I) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma eq_impl_triv: "eq_impl nn eqs eqs S" by (simp add: eq_impl_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eq_impl nn eqs eqs S
theory GraphRefine

lemma var_acc_var_upd:
  "var_acc nm (var_upd nm' v st) = (if nm = nm' then v else var_acc nm st)" by (cases st, simp add: var_acc_def var_upd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. var_acc nm (var_upd nm' v st) = (if nm = nm' then v else var_acc nm st)
theory GraphRefine

lemma var_acc_var_upd_same[simp]:
  "var_acc nm (var_upd nm v st) = v" by (simp add: var_acc_var_upd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. var_acc nm (var_upd nm v st) = v
theory GraphRefine

lemma var_acc_var_upd_diff:
  "nm \<noteq> nm' \<Longrightarrow> var_acc nm (var_upd nm' v st) = var_acc nm st" by (simp add: var_acc_var_upd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nm \<noteq> nm' \<Longrightarrow> var_acc nm (var_upd nm' v st) = var_acc nm st
theory GraphRefine

lemma fetch_returned:
  "\<lbrakk> distinct vs; length vs = length xs \<rbrakk>
    \<Longrightarrow> acc_vars vs (save_vals vs xs st) = xs" apply (induct vs arbitrary: xs st) apply (simp add: acc_vars_def) apply (case_tac xs, simp_all add: save_vals_def acc_vars_def) apply (rule_tac P="\<lambda>st. var_acc a st = b" and Q="\<lambda>x. x \<in> set xs" for a b xs
            in fold_invariant, simp) apply simp apply (clarsimp simp: var_acc_var_upd set_zip) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct vs; length vs = length xs\<rbrakk> \<Longrightarrow> acc_vars vs (save_vals vs xs st) = xs proof (prove)
goal (2 subgoals):
 1. \<And>xs st. \<lbrakk>distinct []; length [] = length xs\<rbrakk> \<Longrightarrow> acc_vars [] (save_vals [] xs st) = xs
 2. \<And>x1 vs xs st. \<lbrakk>\<And>xs st. \<lbrakk>distinct vs; length vs = length xs\<rbrakk> \<Longrightarrow> acc_vars vs (save_vals vs xs st) = xs; distinct (x1 # vs); length (x1 # vs) = length xs\<rbrakk> \<Longrightarrow> acc_vars (x1 # vs) (save_vals (x1 # vs) xs st) = xs proof (prove)
goal (1 subgoal):
 1. \<And>x1 vs xs st. \<lbrakk>\<And>xs st. \<lbrakk>distinct vs; length vs = length xs\<rbrakk> \<Longrightarrow> acc_vars vs (save_vals vs xs st) = xs; distinct (x1 # vs); length (x1 # vs) = length xs\<rbrakk> \<Longrightarrow> acc_vars (x1 # vs) (save_vals (x1 # vs) xs st) = xs proof (prove)
goal (1 subgoal):
 1. \<And>x1 vs xs st a list. \<lbrakk>\<And>xs st. length list = length xs \<Longrightarrow> map (\<lambda>v. var_acc v (fold (\<lambda>(x, y). var_upd x y) (zip vs xs) st)) vs = xs; x1 \<notin> set vs \<and> distinct vs; length vs = length list; xs = a # list\<rbrakk> \<Longrightarrow> var_acc x1 (fold (\<lambda>(x, y). var_upd x y) (zip vs list) (var_upd x1 a st)) = a proof (prove)
goal (2 subgoals):
 1. \<And>x1 vs xs st a list. \<lbrakk>\<And>xs st. length list = length xs \<Longrightarrow> map (\<lambda>v. var_acc v (fold (\<lambda>(x, y). var_upd x y) (zip vs xs) st)) vs = xs; x1 \<notin> set vs \<and> distinct vs; length vs = length list; xs = a # list\<rbrakk> \<Longrightarrow> var_acc x1 (var_upd x1 a st) = a
 2. \<And>x1 vs xs st a list x s. \<lbrakk>\<And>xs st. length list = length xs \<Longrightarrow> map (\<lambda>v. var_acc v (fold (\<lambda>(x, y). var_upd x y) (zip vs xs) st)) vs = xs; x1 \<notin> set vs \<and> distinct vs; length vs = length list; xs = a # list; x \<in> set (zip vs list); var_acc x1 s = a\<rbrakk> \<Longrightarrow> var_acc x1 ((case x of (x, xa) \<Rightarrow> var_upd x xa) s) = a proof (prove)
goal (1 subgoal):
 1. \<And>x1 vs xs st a list x s. \<lbrakk>\<And>xs st. length list = length xs \<Longrightarrow> map (\<lambda>v. var_acc v (fold (\<lambda>(x, y). var_upd x y) (zip vs xs) st)) vs = xs; x1 \<notin> set vs \<and> distinct vs; length vs = length list; xs = a # list; x \<in> set (zip vs list); var_acc x1 s = a\<rbrakk> \<Longrightarrow> var_acc x1 ((case x of (x, xa) \<Rightarrow> var_upd x xa) s) = a proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma c_trace_nontermination:
  "tr \<in> c_trace \<Gamma>
    \<Longrightarrow> trace_end tr = None
    \<Longrightarrow> tr 0 = Some (com, st)
    \<Longrightarrow> \<not> terminates \<Gamma> com st" apply (frule trace_end_NoneD, simp add: c_trace_def) apply (erule disjE) apply (clarsimp simp: c_trace_def nat_trace_rel_def)+ apply (drule terminates_impl_no_infinite_trans_computation) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> c_trace \<Gamma>; trace_end tr = None; tr 0 = Some (com, st)\<rbrakk> \<Longrightarrow> \<not> \<Gamma>\<turnstile>com \<down> st proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> c_trace \<Gamma>; trace_end tr = None; tr 0 = Some (com, st); tr = (\<lambda>_. None) \<or> (\<exists>f. tr = Some \<circ> f)\<rbrakk> \<Longrightarrow> \<not> \<Gamma>\<turnstile>com \<down> st proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> c_trace \<Gamma>; trace_end tr = None; tr 0 = Some (com, st); tr = (\<lambda>_. None)\<rbrakk> \<Longrightarrow> \<not> \<Gamma>\<turnstile>com \<down> st
 2. \<lbrakk>tr \<in> c_trace \<Gamma>; trace_end tr = None; tr 0 = Some (com, st); \<exists>f. tr = Some \<circ> f\<rbrakk> \<Longrightarrow> \<not> \<Gamma>\<turnstile>com \<down> st proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. \<Gamma>\<turnstile> f n \<rightarrow> f (Suc n); trace_end (Some \<circ> f) = None; f 0 = (com, st); tr = Some \<circ> f; \<Gamma>\<turnstile>com \<down> st\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>\<forall>n. \<Gamma>\<turnstile> f n \<rightarrow> f (Suc n); trace_end (Some \<circ> f) = None; f 0 = (com, st); tr = Some \<circ> f; \<nexists>f. f 0 = (com, st) \<and> (\<forall>i. \<Gamma>\<turnstile> f i \<rightarrow>\<^sup>+ f (Suc i))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma trace_end_Ret_Err:
  "trace \<in> exec_trace Gamma fname
    \<Longrightarrow> trace_end trace = Some v
    \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> er \<in> {Ret, Err}" apply (frule trace_end_SomeD) apply (clarsimp simp: exec_trace_def, assumption) apply clarsimp apply (frule(1) exec_trace_invariant) apply (auto simp: continuing_def exec_graph_invariant_Cons
             split: list.split_asm next_node.split_asm,
         auto simp: exec_graph_invariant_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v\<rbrakk> \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> er \<in> {Ret, Err} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v\<rbrakk> \<Longrightarrow> trace \<in> nat_trace_rel ?cont ?r
 2. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v; \<exists>n. trace n = Some v \<and> trace (Suc n) = None \<and> \<not> ?cont v\<rbrakk> \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> er \<in> {Ret, Err} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v; \<exists>n. trace n = Some v \<and> trace (Suc n) = None \<and> \<not> continuing v\<rbrakk> \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> er \<in> {Ret, Err} proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v; trace n = Some v; trace (Suc n) = None; \<not> continuing v\<rbrakk> \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> (er = Ret \<or> er = Err) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>trace \<in> exec_trace Gamma fname; trace_end trace = Some v; trace n = Some v; trace (Suc n) = None; \<not> continuing v; exec_graph_invariant Gamma fname v\<rbrakk> \<Longrightarrow> \<exists>gst er. v = [(er, gst, fname)] \<and> (er = Ret \<or> er = Err) proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma simpl_to_graph_name_simpl_state:
  "(\<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces {sst} I inp_eqs out_eqs)
    \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs" by (simp add: simpl_to_graph_def, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>sst. sst \<in> P \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces {sst} I inp_eqs out_eqs) \<Longrightarrow> simpl_to_graph SGamma GGamma gf nn com n traces P I inp_eqs out_eqs
theory GraphRefine

lemma trace_drop_n_init:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')]
    \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0
        = Some [(NextNode (entry_point gf'), init_vars (function_inputs gf') inps st, fn')]" apply (frule(1) exec_trace_invariant) apply (simp add: exec_graph_invariant_Cons) apply (frule_tac tr=tr and i=i in exec_trace_step_cases) apply (clarsimp simp: exec_graph_step_def split: graph_function.split_asm) apply (simp add: trace_drop_n_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point gf'), init_vars (function_inputs gf') inps st, fn')] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn'')]; exec_graph_invariant Gamma fn [(NextNode n, st, fn'')]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point gf'), init_vars (function_inputs gf') inps st, fn')] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn)]; fn'' = fn\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point gf'), init_vars (function_inputs gf') inps st, fn')] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; tr i = Some [(NextNode n, st, fn)]; fn'' = fn; tr i = None \<and> tr (Suc i) = None \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) \<or> tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point gf'), init_vars (function_inputs gf') inps st, fn')] proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4 x1a x2a x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); x3 n = Some (node.Call nn fn' inps outps); Gamma fn' = Some (GraphFunction x1a x2a x3a x4a); tr i = Some [(NextNode n, st, fn)]; fn'' = fn; gf = GraphFunction x1 x2 x3 x4; gf' = GraphFunction x1a x2a x3a x4a; tr (Suc i) = Some [(NextNode x4a, init_vars x1a inps st, fn'), (NextNode n, st, fn)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode x4a, init_vars x1a inps st, fn')] proof (prove)
goal:
No subgoals!