kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphProof

lemma reachable_trace:
  "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> trace_addr tr i = Some nn
    \<Longrightarrow> trace_addr tr j = Some nn'
    \<Longrightarrow> i < j
    \<Longrightarrow> (nn, nn') \<in> trancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})" apply (frule(3) reachable_trace_induct[where k="j - i" and j=j]) apply simp apply (clarsimp simp: trace_bottom_addr_def dest!: trace_addr_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i < j\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+ proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i < j\<rbrakk> \<Longrightarrow> i + (j - i) \<le> j
 2. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i < j; \<forall>nn'. trace_bottom_addr tr (i + (j - i)) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + (j - i)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (j - i \<noteq> 0 \<and> trace_addr tr (i + (j - i)) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i < j; \<forall>nn'. trace_bottom_addr tr (i + (j - i)) = Some nn' \<longrightarrow> Some nn' \<in> trace_addr tr ` {i..i + (j - i)} \<and> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* \<and> (j - i \<noteq> 0 \<and> trace_addr tr (i + (j - i)) \<noteq> None \<longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+)\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+ proof (prove)
goal:
No subgoals!
theory GraphProof

lemma reachable_trace_eq:
  "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> trace_addr tr i = Some nn
    \<Longrightarrow> trace_addr tr j = Some nn'
    \<Longrightarrow> i \<le> j
    \<Longrightarrow> (nn, nn') \<in> rtrancl (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i ..< j}})" apply (cases "i = j", simp_all) apply (rule trancl_into_rtrancl) apply (fastforce elim: reachable_trace) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i \<le> j\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i \<le> j; i \<noteq> j\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i \<le> j; i \<noteq> j\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+ proof (prove)
goal:
No subgoals!
theory GraphProof

lemma restrs_single_visit:
  "tr \<in> exec_trace Gamma fname \<Longrightarrow> Gamma fname = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> trace_addr tr i = Some nn
    \<Longrightarrow> restrs_condition tr restrs i
    \<Longrightarrow> trace_addr tr j = Some nn
    \<Longrightarrow> restrs_condition tr restrs j
    \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})
    \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})
    \<Longrightarrow> i = j" by (metis restrs_single_visit_neq linorder_neq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; restrs_condition tr restrs i; trace_addr tr j = Some nn; restrs_condition tr restrs j; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+\<rbrakk> \<Longrightarrow> i = j
theory GraphProof

lemma restrs_single_visit2:
  "trace_addr tr i = Some nn
    \<Longrightarrow> trace_addr tr j = Some nn
    \<Longrightarrow> tr \<in> exec_trace Gamma fname
    \<Longrightarrow> Gamma fname = Some f
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> restrs_condition tr restrs i
    \<Longrightarrow> restrs_condition tr restrs j
    \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})
    \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})
    \<Longrightarrow> i = j" by (metis restrs_single_visit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr i = Some nn; trace_addr tr j = Some nn; tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; restrs_condition tr restrs i; restrs_condition tr restrs j; \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}); (nn, nn) \<notin> (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})\<^sup>+\<rbrakk> \<Longrightarrow> i = j
theory GraphProof

lemma not_trancl_converse_step:
  "converse stp `` {y} \<subseteq> S
    \<Longrightarrow> \<forall>z \<in> S. (x, z) \<notin> rtrancl (stp \<inter> constraint)
    \<Longrightarrow> (x, y) \<notin> trancl (stp \<inter> constraint)" using tranclD2 by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>stp\<inverse> `` {y} \<subseteq> S; \<forall>z\<in>S. (x, z) \<notin> (stp \<inter> constraint)\<^sup>*\<rbrakk> \<Longrightarrow> (x, y) \<notin> (stp \<inter> constraint)\<^sup>+ proof (prove)
using this:
(?x, ?y) \<in> ?R\<^sup>+ \<Longrightarrow> \<exists>z. (?x, z) \<in> ?R\<^sup>* \<and> (z, ?y) \<in> ?R

goal (1 subgoal):
 1. \<lbrakk>stp\<inverse> `` {y} \<subseteq> S; \<forall>z\<in>S. (x, z) \<notin> (stp \<inter> constraint)\<^sup>*\<rbrakk> \<Longrightarrow> (x, y) \<notin> (stp \<inter> constraint)\<^sup>+
theory GraphProof

lemma reachable_order_mono:
  "(nn, nn') \<in> rtrancl R
    \<Longrightarrow> (\<forall>(nn, nn') \<in> R. order nn \<le> order nn')
    \<Longrightarrow> order nn \<le> (order nn' :: 'a :: linorder)" apply (induct rule: rtrancl.induct) apply simp apply (blast intro: order_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nn, nn') \<in> R\<^sup>*; \<forall>(nn, nn')\<in>R. order nn \<le> order nn'\<rbrakk> \<Longrightarrow> order nn \<le> order nn' proof (prove)
goal (2 subgoals):
 1. \<And>a. \<forall>(nn, nn')\<in>R. order nn \<le> order nn' \<Longrightarrow> order a \<le> order a
 2. \<And>a b c. \<lbrakk>(a, b) \<in> R\<^sup>*; \<forall>(nn, nn')\<in>R. order nn \<le> order nn' \<Longrightarrow> order a \<le> order b; (b, c) \<in> R; \<forall>(nn, nn')\<in>R. order nn \<le> order nn'\<rbrakk> \<Longrightarrow> order a \<le> order c proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(a, b) \<in> R\<^sup>*; \<forall>(nn, nn')\<in>R. order nn \<le> order nn' \<Longrightarrow> order a \<le> order b; (b, c) \<in> R; \<forall>(nn, nn')\<in>R. order nn \<le> order nn'\<rbrakk> \<Longrightarrow> order a \<le> order c proof (prove)
goal:
No subgoals!
theory GraphProof

lemma Collect_less_nat:
  "(n :: nat) - 1 = m
    \<Longrightarrow> {i. i < n \<and> P i} = (if n = 0 then {} else {i. i < m \<and> P i} \<union> (if P m then {m} else {}))" by (cases n, simp_all add: Collect_less_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n - 1 = m \<Longrightarrow> {i. i < n \<and> P i} = (if n = 0 then {} else {i. i < m \<and> P i} \<union> (if P m then {m} else {}))
theory GraphProof

lemma fst_succ_visit[simp]:
  "fst (succ_visit nn v) = fst v" by (simp add: succ_visit_def split_def split: next_node.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (succ_visit nn v) = fst v
theory GraphProof

lemma wf_graph_function_init_extract:
  "\<lbrakk> wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f;
        the (tr 0) = [init_state fn f xs];
        \<forall>n. 0 \<in> restrs n; length xs = ilen \<rbrakk> \<Longrightarrow>
    acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs" apply (cases f) apply (frule wf_graph_function_length_function_inputs) apply (frule exec_trace_init) apply (clarsimp simp: visit_known restrs_condition_def init_state_def
                        wf_graph_function_acc_vars_save_vals) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; the (tr 0) = [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; length xs = ilen\<rbrakk> \<Longrightarrow> acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; the (tr 0) = [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; length xs = ilen; f = GraphFunction x1 x2 x3 x4\<rbrakk> \<Longrightarrow> acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; the (tr 0) = [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; length xs = ilen; f = GraphFunction x1 x2 x3 x4; length (function_inputs f) = ilen\<rbrakk> \<Longrightarrow> acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. \<lbrakk>wf_graph_function f ilen olen; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; the (tr 0) = [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; length xs = ilen; f = GraphFunction x1 x2 x3 x4; length (function_inputs f) = ilen; \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]\<rbrakk> \<Longrightarrow> acc_vars (function_inputs f) (the (visit tr (NextNode (entry_point f)) restrs)) = xs proof (prove)
goal:
No subgoals!
theory GraphProof

lemma init_pc:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> tr 0 = Some [init_state fn f xs]
    \<Longrightarrow> \<forall>n. 0 \<in> restrs n
    \<Longrightarrow> wf_graph_function f ilen olen
    \<Longrightarrow> pc' (entry_point f) restrs tr" apply (clarsimp simp: pc_def visit_def) apply (rule_tac x=0 in exI) apply (simp add: trace_addr_SomeI init_state_def restrs_condition_def
            split: graph_function.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr 0 = Some [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; wf_graph_function f ilen olen\<rbrakk> \<Longrightarrow> pc' (entry_point f) restrs tr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr 0 = Some [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; wf_graph_function f ilen olen\<rbrakk> \<Longrightarrow> \<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some (NextNode (entry_point f)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; tr 0 = Some [init_state fn f xs]; \<forall>n. 0 \<in> restrs n; wf_graph_function f ilen olen\<rbrakk> \<Longrightarrow> restrs_condition tr restrs 0 \<and> trace_addr tr 0 = Some (NextNode (entry_point f)) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma eqs_eq_conj_len_assert:
  "(eqs xs lens vs) = ((eqs xs lens $ vs)
    \<and> (\<forall>addr. lens addr \<noteq> None \<longrightarrow> length (vs addr) = the (lens addr)))" by (auto simp: eqs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. eqs xs lens vs = ((eqs xs lens $ vs) \<and> (\<forall>addr. lens addr \<noteq> None \<longrightarrow> length (vs addr) = the (lens addr)))
theory GraphProof

lemma length_acc_vars[simp]:
  "length (acc_vars vs st) = length vs" by (simp add: acc_vars_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (acc_vars vs st) = length vs
theory GraphProof

lemma restrs_list_Int:
  "restrs_list rs = (\<lambda>j. \<Inter>(n, xsf) \<in> set rs. (if j = n then set xsf else UNIV))" apply (induct rs rule: rev_induct) apply (simp add: restrs_list_def) apply (clarsimp simp add: restrs_list_def fun_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restrs_list rs = (\<lambda>j. \<Inter>(n, xsf)\<in>set rs. if j = n then set xsf else UNIV) proof (prove)
goal (2 subgoals):
 1. restrs_list [] = (\<lambda>j. \<Inter>a\<in>set []. case a of (n, xsf) \<Rightarrow> if j = n then set xsf else UNIV)
 2. \<And>x xs. restrs_list xs = (\<lambda>j. \<Inter>a\<in>set xs. case a of (n, xsf) \<Rightarrow> if j = n then set xsf else UNIV) \<Longrightarrow> restrs_list (xs @ [x]) = (\<lambda>j. \<Inter>a\<in>set (xs @ [x]). case a of (n, xsf) \<Rightarrow> if j = n then set xsf else UNIV) proof (prove)
goal (1 subgoal):
 1. \<And>x xs. restrs_list xs = (\<lambda>j. \<Inter>a\<in>set xs. case a of (n, xsf) \<Rightarrow> if j = n then set xsf else UNIV) \<Longrightarrow> restrs_list (xs @ [x]) = (\<lambda>j. \<Inter>a\<in>set (xs @ [x]). case a of (n, xsf) \<Rightarrow> if j = n then set xsf else UNIV) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma restrs_list_Int2:
  "restrs_list rs = (\<lambda>j. \<Inter>(_, xsf) \<in> {x \<in> set rs. fst x = j}. set xsf)" by (auto simp add: restrs_list_Int fun_eq_iff set_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restrs_list rs = (\<lambda>j. \<Inter>(uu_, xsf)\<in>{x \<in> set rs. fst x = j}. set xsf)
theory GraphProof

lemma restrs_list_Cons:
  "restrs_list ((n, xs) # rs) = (\<lambda>j.
    if j = n then set xs \<inter> restrs_list rs j else restrs_list rs j)" by (simp add: restrs_list_Int fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restrs_list ((n, xs) # rs) = (\<lambda>j. if j = n then set xs \<inter> restrs_list rs j else restrs_list rs j)
theory GraphProof

lemma restrs_eventually_Cons:
  "restrs_eventually_condition tr ((K UNIV) (n := set xs))
    \<Longrightarrow> restrs_eventually_condition tr (restrs_list rs)
    \<Longrightarrow> restrs_eventually_condition tr (restrs_list ((n, xs) # rs))" apply (clarsimp simp: restrs_eventually_condition_def) apply (rule_tac x="max na naa" in exI) apply (simp add: restrs_condition_def restrs_list_Cons split: if_split_asm) apply (simp add: max_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>restrs_eventually_condition tr ((K UNIV)(n := set xs)); restrs_eventually_condition tr (restrs_list rs)\<rbrakk> \<Longrightarrow> restrs_eventually_condition tr (restrs_list ((n, xs) # rs)) proof (prove)
goal (1 subgoal):
 1. \<And>na naa y ya. \<lbrakk>\<forall>m\<ge>na. restrs_condition tr ((\<lambda>y. UNIV)(n := set xs)) m; tr na = Some y; \<forall>m\<ge>naa. restrs_condition tr (restrs_list rs) m; tr naa = Some ya\<rbrakk> \<Longrightarrow> \<exists>na. (\<exists>y. tr na = Some y) \<and> (\<forall>m\<ge>na. restrs_condition tr (restrs_list ((n, xs) # rs)) m) proof (prove)
goal (1 subgoal):
 1. \<And>na naa y ya. \<lbrakk>\<forall>m\<ge>na. restrs_condition tr ((\<lambda>y. UNIV)(n := set xs)) m; tr na = Some y; \<forall>m\<ge>naa. restrs_condition tr (restrs_list rs) m; tr naa = Some ya\<rbrakk> \<Longrightarrow> (\<exists>y. tr (max na naa) = Some y) \<and> (\<forall>m\<ge>max na naa. restrs_condition tr (restrs_list ((n, xs) # rs)) m) proof (prove)
goal (1 subgoal):
 1. \<And>na naa y ya. \<lbrakk>\<forall>m\<ge>na. card {i. i < m \<and> trace_addr tr i = Some (NextNode n)} \<in> set xs; tr na = Some y; \<forall>m\<ge>naa. \<forall>ma. card {i. i < m \<and> trace_addr tr i = Some (NextNode ma)} \<in> restrs_list rs ma; tr naa = Some ya\<rbrakk> \<Longrightarrow> \<exists>y. tr (max na naa) = Some y proof (prove)
goal:
No subgoals!
theory GraphProof

lemma ex_greatest_nat_le:
  "P j \<Longrightarrow> j \<le> n \<Longrightarrow> \<exists>k \<le> n. (\<forall>i \<in> {Suc k .. n}. \<not> P i) \<and> P k" apply (cases "P n") apply (rule_tac x=n in exI, simp) apply (cut_tac P="\<lambda>j. P (n - j)" and n = "n - j" in ex_least_nat_le, simp+) apply (clarify, rule_tac x="n - k" in exI) apply clarsimp apply (drule_tac x="n - i" in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P j; j \<le> n\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. (\<forall>i\<in>{Suc k..n}. \<not> P i) \<and> P k proof (prove)
goal (2 subgoals):
 1. \<lbrakk>P j; j \<le> n; P n\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. (\<forall>i\<in>{Suc k..n}. \<not> P i) \<and> P k
 2. \<lbrakk>P j; j \<le> n; \<not> P n\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. (\<forall>i\<in>{Suc k..n}. \<not> P i) \<and> P k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P j; j \<le> n; \<not> P n\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. (\<forall>i\<in>{Suc k..n}. \<not> P i) \<and> P k proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P j; j \<le> n; \<not> P n; \<exists>k\<le>n - j. (\<forall>i<k. \<not> P (n - i)) \<and> P (n - k)\<rbrakk> \<Longrightarrow> \<exists>k\<le>n. (\<forall>i\<in>{Suc k..n}. \<not> P i) \<and> P k proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>P j; j \<le> n; \<not> P n; k \<le> n - j; \<forall>i<k. \<not> P (n - i); P (n - k)\<rbrakk> \<Longrightarrow> n - k \<le> n \<and> (\<forall>i\<in>{Suc (n - k)..n}. \<not> P i) \<and> P (n - k) proof (prove)
goal (1 subgoal):
 1. \<And>k i. \<lbrakk>P j; j \<le> n; \<not> P n; k \<le> n - j; \<forall>i<k. \<not> P (n - i); P (n - k); P i; Suc (n - k) \<le> i; i \<le> n\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphProof

lemma set_fill_in_below:
  "set (fill_in_below xs) = {k. \<exists>l. l : set xs \<and> k \<le> l}" apply (induct xs rule: rev_induct, simp_all add: fill_in_below_def) apply (simp add: set_eq_iff less_max_iff_disj less_Suc_eq_le) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (fill_in_below xs) = {k. \<exists>l. l \<in> set xs \<and> k \<le> l} proof (prove)
goal (1 subgoal):
 1. \<And>x xs. {0..<fold max (map Suc xs) 0} = {k. \<exists>l. l \<in> set xs \<and> k \<le> l} \<Longrightarrow> {0..<max (Suc x) (fold max (map Suc xs) 0)} = {k. \<exists>l. (l = x \<or> l \<in> set xs) \<and> k \<le> l} proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<forall>x. (x < fold max (map Suc xs) 0) = (\<exists>l. l \<in> set xs \<and> x \<le> l) \<Longrightarrow> \<forall>xa. (xa \<le> x \<or> (\<exists>l. l \<in> set xs \<and> xa \<le> l)) = (\<exists>l. (l = x \<or> l \<in> set xs) \<and> xa \<le> l) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma last_upd_stack:
  "List.last (upd_stack nn stf xs)
    = (if length xs = 1 then (nn, stf (fst (snd (hd xs))), snd (snd (hd xs)))
        else List.last xs)" by (cases xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. last (upd_stack nn stf xs) = (if length xs = 1 then (nn, stf (fst (snd (hd xs))), snd (snd (hd xs))) else last xs)
theory GraphProof

lemma not_reachable_visits_same:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> trace_addr tr i = Some n
    \<Longrightarrow> (n, m) \<notin> rtrancl (reachable_step' gf)
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> j > i
    \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m}" using reachable_trace_eq[THEN subsetD[OF rtrancl_mono, OF Int_lower1]] apply (safe, simp_all) apply (rule ccontr, clarsimp simp: linorder_not_less) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_addr tr i = Some n; (n, m) \<notin> (reachable_step' gf)\<^sup>*; wf_graph_function gf ilen olen; i < j\<rbrakk> \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m} proof (prove)
using this:
\<lbrakk>?tr3 \<in> exec_trace ?Gamma3 ?fname3; ?Gamma3 ?fname3 = Some ?f3; wf_graph_function ?f3 ?ilen3 ?olen3; trace_addr ?tr3 ?i3 = Some ?nn3; trace_addr ?tr3 ?j3 = Some ?nn'3; ?i3 \<le> ?j3\<rbrakk> \<Longrightarrow> (?nn3, ?nn'3) \<in> (reachable_step' ?f3)\<^sup>*

goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_addr tr i = Some n; (n, m) \<notin> (reachable_step' gf)\<^sup>*; wf_graph_function gf ilen olen; i < j\<rbrakk> \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_addr tr i = Some n; (n, m) \<notin> (reachable_step' gf)\<^sup>*; wf_graph_function gf ilen olen; i < j; x < j; trace_addr tr x = Some m; \<And>tr Gamma fname f ilen olen i nn j nn'. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; trace_addr tr j = Some nn'; i \<le> j\<rbrakk> \<Longrightarrow> (nn, nn') \<in> (reachable_step' f)\<^sup>*\<rbrakk> \<Longrightarrow> x < i proof (prove)
goal:
No subgoals!
theory GraphProof

lemma not_reachable_visits_same_symm:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> trace_addr tr i = Some n
    \<Longrightarrow> trace_addr tr j = Some n
    \<Longrightarrow> (n, m) \<notin> rtrancl (reachable_step' gf)
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m}" using linorder_neq_iff[where x=i and y=j] not_reachable_visits_same by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_addr tr i = Some n; trace_addr tr j = Some n; (n, m) \<notin> (reachable_step' gf)\<^sup>*; wf_graph_function gf ilen olen\<rbrakk> \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m} proof (prove)
using this:
(i \<noteq> j) = (i < j \<or> j < i)
\<lbrakk>?tr \<in> exec_trace ?Gamma ?fn; ?Gamma ?fn = Some ?gf; trace_addr ?tr ?i = Some ?n; (?n, ?m) \<notin> (reachable_step' ?gf)\<^sup>*; wf_graph_function ?gf ?ilen ?olen; ?i < ?j\<rbrakk> \<Longrightarrow> {k. k < ?j \<and> trace_addr ?tr k = Some ?m} = {k. k < ?i \<and> trace_addr ?tr k = Some ?m}

goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; trace_addr tr i = Some n; trace_addr tr j = Some n; (n, m) \<notin> (reachable_step' gf)\<^sup>*; wf_graph_function gf ilen olen\<rbrakk> \<Longrightarrow> {k. k < j \<and> trace_addr tr k = Some m} = {k. k < i \<and> trace_addr tr k = Some m}