kings-crown/FVELER_Isabelle huggingface dataset:
theory CommonOpsLemmas

lemma small_downcasts:
  "unat (x :: 'a :: len word) < 2 ^ LENGTH('b :: len) \<Longrightarrow> unat (UCAST('a \<rightarrow> 'b) x) = unat x" apply (case_tac "LENGTH('a) \<le> LENGTH('b)", simp add: unat_ucast_up_simp) apply (simp add: unat_ucast unat_less_power) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH('b) \<Longrightarrow> unat (UCAST('a \<rightarrow> 'b) x) = unat x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat x < 2 ^ LENGTH('b); \<not> LENGTH('a) \<le> LENGTH('b)\<rbrakk> \<Longrightarrow> unat (UCAST('a \<rightarrow> 'b) x) = unat x proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma exec_graph_invariant_Cons:
  "exec_graph_invariant Gamma fname (x # xs) = (if xs = [] then snd (snd x) = fname
    else (get_state_function_call Gamma (hd xs) = Some (snd (snd x))
        \<and> exec_graph_invariant Gamma fname xs))" by (cases xs, auto simp add: exec_graph_invariant_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. exec_graph_invariant Gamma fname (x # xs) = (if xs = [] then snd (snd x) = fname else get_state_function_call Gamma (hd xs) = Some (snd (snd x)) \<and> exec_graph_invariant Gamma fname xs)
theory GraphLangLemmas

lemma exec_step_invariant:
  "(stack, stack') \<in> exec_graph_step Gamma
    \<Longrightarrow> exec_graph_invariant Gamma gf stack
    \<Longrightarrow> exec_graph_invariant Gamma gf stack'" by (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons
                 get_state_function_call_def
          split: graph_function.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma; exec_graph_invariant Gamma gf stack\<rbrakk> \<Longrightarrow> exec_graph_invariant Gamma gf stack'
theory GraphLangLemmas

lemma exec_trace_Nil:
  "tr \<in> exec_trace Gamma gf \<Longrightarrow> tr i \<noteq> Some []" apply safe apply (drule(1) exec_trace_invariant) apply (simp add: exec_graph_invariant_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr \<in> exec_trace Gamma gf \<Longrightarrow> tr i \<noteq> Some [] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma gf; tr i = Some []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some []; exec_graph_invariant Gamma gf []\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma exec_trace_None_dom_subset:
  "tr n = None \<Longrightarrow> tr \<in> exec_trace Gamma f
    \<Longrightarrow> dom tr \<subseteq> {..< n}" unfolding exec_trace_def by (blast elim: CollectE dest: trace_None_dom_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = None; tr \<in> exec_trace Gamma f\<rbrakk> \<Longrightarrow> dom tr \<subseteq> {..<n} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = None; tr \<in> {trace. \<exists>gf. Gamma f = Some gf \<and> (\<exists>st. trace 0 = Some [(NextNode (entry_point gf), st, f)]) \<and> trace \<in> nat_trace_rel continuing (exec_graph_step Gamma)}\<rbrakk> \<Longrightarrow> dom tr \<subseteq> {..<n}
theory GraphLangLemmas

lemma trace_Some_dom_superset:
  "tr \<in> nat_trace_rel c R
    \<Longrightarrow> tr i = Some v
    \<Longrightarrow> {..i} \<subseteq> dom tr" apply (clarsimp, rule ccontr, clarsimp) 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; tr i = Some v\<rbrakk> \<Longrightarrow> {..i} \<subseteq> dom tr proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; x \<le> i; tr x = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; x \<le> i; dom tr \<subseteq> {..<x}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma trace_end_eq_Some:
  "tr \<in> nat_trace_rel c R
    \<Longrightarrow> tr i = Some v
    \<Longrightarrow> tr (Suc i) = None
    \<Longrightarrow> trace_end tr = Some v" apply (frule(1) trace_Some_dom_superset) apply (frule(1) trace_None_dom_eq) apply (clarsimp simp: le_Suc_eq lessThan_Suc_atMost[symmetric]) apply (simp add: trace_end_def) apply (subst Max_eqI[where x=i], simp_all) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None\<rbrakk> \<Longrightarrow> trace_end tr = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None; {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> trace_end tr = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None; {..i} \<subseteq> dom tr; \<exists>n'\<le>Suc i. dom tr = {..<n'}\<rbrakk> \<Longrightarrow> trace_end tr = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None; dom tr = {..<Suc i}\<rbrakk> \<Longrightarrow> trace_end tr = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None; dom tr = {..<Suc i}\<rbrakk> \<Longrightarrow> ((\<exists>n. tr n = None) \<longrightarrow> tr (Max {..<Suc i}) = Some v) \<and> (\<exists>n. tr n = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; tr (Suc i) = None; dom tr = {..<Suc i}\<rbrakk> \<Longrightarrow> \<exists>n. tr n = None proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma trace_end_cut:
  "tr \<in> nat_trace_rel c R
    \<Longrightarrow> tr i = Some v
    \<Longrightarrow> trace_end (restrict_map tr {.. i}) = Some v" apply (frule(1) trace_Some_dom_superset) apply (simp add: trace_end_def Int_absorb1) apply (subst Max_eqI[where x=i], simp_all) apply (simp add: restrict_map_def) apply (metis Suc_n_not_le_n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v\<rbrakk> \<Longrightarrow> trace_end (tr|\<^bsub>{..i}\<^esub>) = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> trace_end (tr|\<^bsub>{..i}\<^esub>) = Some v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> ((\<exists>n. (tr|\<^bsub>{..i}\<^esub>) n = None) \<longrightarrow> tr (Max {..i}) = Some v) \<and> (\<exists>n. (tr|\<^bsub>{..i}\<^esub>) n = None) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> \<exists>n. (tr|\<^bsub>{..i}\<^esub>) n = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel c R; tr i = Some v; {..i} \<subseteq> dom tr\<rbrakk> \<Longrightarrow> \<exists>n. n \<le> i \<longrightarrow> tr n = None proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma rev_drop_continuing:
  "continuing (rev (drop k (rev stack))) \<Longrightarrow> continuing stack" by (simp add: continuing_def split: list.split next_node.split,
      auto simp: drop_Cons split: nat.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. continuing (rev (drop k (rev stack))) \<Longrightarrow> continuing stack
theory GraphLangLemmas

lemma exec_trace_drop_n:
  assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf"
  shows "tr i = Some [(NextNode n, st, fn'')]
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn'" apply (frule exec_trace_invariant[OF tr(1)]) apply (simp add: exec_graph_invariant_Cons) apply (drule(2) exec_trace_drop_n_Cons[OF tr]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(NextNode n, st, fn'')]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(NextNode n, st, fn'')]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; exec_graph_invariant Gamma fn [(NextNode n, st, fn'')]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr i = Some [(NextNode n, st, fn)]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; fn'' = fn\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; fn'' = fn; trace_drop_n (Suc i) (Suc (length [])) tr \<in> exec_trace Gamma fn'\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fn' proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma exec_trace_drop_n_rest:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')]
    \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps)
    \<Longrightarrow> Gamma fn' = Some gf'
    \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk
     \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]))" apply (frule(1) exec_trace_invariant) apply (clarsimp simp: exec_graph_invariant_Cons) apply (drule(4) exec_trace_drop_n_rest_Cons) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; tr i = Some [(NextNode n, st, fn'')]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; tr i = Some [(NextNode n, st, fn'')]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; exec_graph_invariant Gamma fn [(NextNode n, st, fn'')]\<rbrakk> \<Longrightarrow> \<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]) proof (prove)
goal (1 subgoal):
 1. \<And>stk. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; tr i = Some [(NextNode n, st, fn)]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; fn'' = fn; trace_drop_n (Suc i) (Suc 0) tr k = Some stk\<rbrakk> \<Longrightarrow> tr (Suc (i + k)) = Some (stk @ [(NextNode n, st, fn)]) proof (prove)
goal (1 subgoal):
 1. \<And>stk. \<lbrakk>Gamma fn = Some gf; tr i = Some [(NextNode n, st, fn)]; function_graph gf n = Some (node.Call nn fn' inps outps); Gamma fn' = Some gf'; fn'' = fn; trace_drop_n (Suc i) (Suc 0) tr k = Some stk; \<forall>stka. trace_drop_n (Suc i) (Suc (length [])) tr (?k5 stk) = Some stka \<longrightarrow> tr (Suc i + ?k5 stk) = Some (stka @ [(NextNode n, st, fn)])\<rbrakk> \<Longrightarrow> tr (Suc (i + k)) = Some (stk @ [(NextNode n, st, fn)]) proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma trace_drop_n_init:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> Gamma fname = Some f'
    \<Longrightarrow> tr i = Some [(NextNode n, st, fn')]
    \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'),
            init_vars (function_inputs f') inputs st, fname)]" apply (frule(1) exec_trace_invariant) apply (clarsimp simp: exec_graph_invariant_Cons) apply (frule_tac i=i in exec_trace_step_cases, clarsimp) apply (clarsimp simp: all_exec_graph_step_cases trace_drop_n_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'), init_vars (function_inputs f') inputs st, fname)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn')]; exec_graph_invariant Gamma fn [(NextNode n, st, fn')]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'), init_vars (function_inputs f') inputs st, fname)] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn)]; fn' = fn\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point f'), init_vars (function_inputs f') inputs st, fname)] proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inputs outputs); Gamma fname = Some f'; tr i = Some [(NextNode n, st, fn)]; fn' = fn; ([(NextNode n, st, fn)], y) \<in> exec_graph_step Gamma; tr (Suc i) = Some y\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr 0 = Some [(NextNode (entry_point f'), init_vars (function_inputs f') inputs st, fname)] proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma exec_trace_init:
  "tr \<in> exec_trace Gamma fn
   \<Longrightarrow> \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]" by (clarsimp simp: exec_trace_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr \<in> exec_trace Gamma fn \<Longrightarrow> \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]
theory GraphLangLemmas

lemma dom_Max_None:
  "tr \<in> exec_trace Gamma f \<Longrightarrow> (tr (Max (dom tr)) \<noteq> None)" apply (rule notI) apply (frule(1) exec_trace_None_dom_subset) apply (cases "dom tr = {}") apply (clarsimp dest!: exec_trace_init) apply (drule Max_in[rotated]) apply (simp add: finite_subset) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr \<in> exec_trace Gamma f \<Longrightarrow> tr (Max (dom tr)) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}\<rbrakk> \<Longrightarrow> finite (dom tr)
 2. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; Max (dom tr) \<in> dom tr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; Max (dom tr) \<in> dom tr\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphLangLemmas

lemma trace_end_trace_drop_n_None:
  "trace_end (trace_drop_n i j tr) = None \<Longrightarrow> tr \<in> exec_trace Gamma f
    \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f'
    \<Longrightarrow> trace_end tr = None" apply (clarsimp simp: trace_end_def dom_Max_None split: if_split_asm) apply (rule ccontr, simp) apply (drule(1) exec_trace_None_dom_subset) apply (drule_tac x="n + i + 1" in spec) apply (clarsimp simp: trace_drop_n_def split: if_split_asm) apply auto[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end (trace_drop_n i j tr) = None; tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'\<rbrakk> \<Longrightarrow> trace_end tr = None proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; \<forall>n. \<exists>y. trace_drop_n i j tr n = Some y\<rbrakk> \<Longrightarrow> \<exists>y. tr n = Some y proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; \<forall>n. \<exists>y. trace_drop_n i j tr n = Some y; tr n = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; \<forall>n. \<exists>y. trace_drop_n i j tr n = Some y; dom tr \<subseteq> {..<n}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; trace_drop_n i j tr \<in> exec_trace Gamma f'; dom tr \<subseteq> {..<n}; \<exists>y. trace_drop_n i j tr (n + i + 1) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n z. \<lbrakk>(\<lambda>ia. if \<forall>ja<ia. (\<exists>y. tr (i + ja) = Some y) \<and> continuing (rev (drop j (rev (the (tr (i + ja)))))) then map_option (rev \<circ> drop j \<circ> rev) (tr (ia + i)) else None) \<in> exec_trace Gamma f'; dom tr \<subseteq> {..<n}; tr \<in> exec_trace Gamma f; \<forall>ja<Suc (n + i). (\<exists>y. tr (i + ja) = Some y) \<and> continuing (rev (drop j (rev (the (tr (i + ja)))))); tr (Suc (n + i + i)) = Some z\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ExtraSpecs

lemma simple_simpl_refines_no_fault_execD:
  "\<Gamma> \<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs
    \<Longrightarrow> simple_simpl_refines \<Gamma> com com'
    \<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft)
    \<Longrightarrow> \<Gamma> \<turnstile> \<langle>com', Normal s\<rangle> \<Rightarrow> xs" by (auto simp add: simple_simpl_refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs; simple_simpl_refines \<Gamma> com com'; \<forall>ft. \<not> \<Gamma>\<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> xs
theory ExtraSpecs

lemma simple_simpl_refines_no_fault_terminatesD:
  "simple_simpl_refines \<Gamma> com com'
    \<Longrightarrow> (\<forall>ft. \<not> \<Gamma> \<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft)
    \<Longrightarrow> \<not> terminates \<Gamma> com (Normal s) \<longrightarrow> \<not> terminates \<Gamma> com' (Normal s)" by (auto simp add: simple_simpl_refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simple_simpl_refines \<Gamma> com com'; \<forall>ft. \<not> \<Gamma>\<turnstile> \<langle>com',Normal s\<rangle> \<Rightarrow> Fault ft\<rbrakk> \<Longrightarrow> \<not> \<Gamma>\<turnstile>com \<down> Normal s \<longrightarrow> \<not> \<Gamma>\<turnstile>com' \<down> Normal s
theory ExtraSpecs

lemma simple_simpl_refines_refl:
  "simple_simpl_refines \<Gamma> com com" by (auto simp add: simple_simpl_refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> com com
theory ExtraSpecs

lemma simple_simpl_refines_from_def_eq:
  "body \<equiv> body' \<Longrightarrow> simple_simpl_refines \<Gamma> body' body" 
  (* these are flipped, because the "implementation" is on the rhs of
     definitional equalities, but the lhs of refinement thms. *)
   by (simp add: simple_simpl_refines_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. body \<equiv> body' \<Longrightarrow> simple_simpl_refines \<Gamma> body' body proof (prove)
goal (1 subgoal):
 1. body \<equiv> body' \<Longrightarrow> simple_simpl_refines \<Gamma> body' body
theory ExtraSpecs

lemma simple_simpl_refines_trans:
  "simple_simpl_refines \<Gamma> com com' \<Longrightarrow> simple_simpl_refines \<Gamma> com' com''
    \<Longrightarrow> simple_simpl_refines \<Gamma> com com''" by (simp add: simple_simpl_refines_def, metis)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>simple_simpl_refines \<Gamma> com com'; simple_simpl_refines \<Gamma> com' com''\<rbrakk> \<Longrightarrow> simple_simpl_refines \<Gamma> com com''
theory ExtraSpecs

lemma simple_simpl_refines_drop_Guard:
  "simple_simpl_refines \<Gamma> com (Guard F G com)" apply (clarsimp simp add: simple_simpl_refines_def) apply (case_tac "s \<in> G") apply (auto intro: exec.Guard exec.GuardFault
              elim!: terminates_Normal_elim_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simple_simpl_refines \<Gamma> com (Guard F G com) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>xs. \<Gamma>\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs \<and> \<not> \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> xs) \<or> \<not> \<Gamma>\<turnstile>com \<down> Normal s \<and> \<Gamma>\<turnstile>Guard F G com \<down> Normal s \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(\<exists>xs. \<Gamma>\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs \<and> \<not> \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> xs) \<or> \<not> \<Gamma>\<turnstile>com \<down> Normal s \<and> \<Gamma>\<turnstile>Guard F G com \<down> Normal s; s \<in> G\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> Fault ft
 2. \<And>s. \<lbrakk>(\<exists>xs. \<Gamma>\<turnstile> \<langle>com,Normal s\<rangle> \<Rightarrow> xs \<and> \<not> \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> xs) \<or> \<not> \<Gamma>\<turnstile>com \<down> Normal s \<and> \<Gamma>\<turnstile>Guard F G com \<down> Normal s; s \<notin> G\<rbrakk> \<Longrightarrow> \<exists>ft. \<Gamma>\<turnstile> \<langle>Guard F G com,Normal s\<rangle> \<Rightarrow> Fault ft proof (prove)
goal:
No subgoals!
theory GraphRefine

lemma suffix_tuple_closure_prefixI:
  "(y, restrict_map tr {.. (k :: nat)}) \<in> suffix_tuple_closure_inter Ss
    \<Longrightarrow> (y, tr) \<in> suffix_tuple_closure_inter Ss" by (auto simp add: suffix_tuple_closure_inter_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (y, tr|\<^bsub>{..k}\<^esub>) \<in> suffix_tuple_closure_inter Ss \<Longrightarrow> (y, tr) \<in> suffix_tuple_closure_inter Ss