kings-crown/FVELER_Isabelle huggingface dataset:
theory GraphProof

lemma fold_double_trace_imp:
  "fold double_trace_imp hyps hyp trs
    = ((\<forall>h \<in> set hyps. h trs) \<longrightarrow> hyp trs)" apply (induct hyps arbitrary: hyp, simp_all) apply (auto simp add: double_trace_imp_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold double_trace_imp hyps hyp trs = ((\<forall>h\<in>set hyps. h trs) \<longrightarrow> hyp trs) proof (prove)
goal (1 subgoal):
 1. \<And>x1 hyps hyp. (\<And>hyp. fold double_trace_imp hyps hyp trs = ((\<forall>h\<in>set hyps. h trs) \<longrightarrow> hyp trs)) \<Longrightarrow> ((\<forall>h\<in>set hyps. h trs) \<longrightarrow> double_trace_imp x1 hyp trs) = (x1 trs \<and> (\<forall>h\<in>set hyps. h trs) \<longrightarrow> hyp trs) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma exec_trace_addr_Suc:
  "tr \<in> exec_trace Gamma f \<Longrightarrow> trace_addr tr n = Some (NextNode m) \<Longrightarrow> tr (Suc n) \<noteq> None" apply (drule_tac i=n in exec_trace_step_cases) apply (auto dest!: trace_addr_SomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; trace_addr tr n = Some (NextNode m)\<rbrakk> \<Longrightarrow> tr (Suc n) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr n = Some (NextNode m); tr n = None \<and> tr (Suc n) = None \<or> (\<exists>state. tr n = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc n) = None) \<or> tr n \<noteq> None \<and> tr (Suc n) \<noteq> None \<and> (the (tr n), the (tr (Suc n))) \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> tr (Suc n) \<noteq> None proof (prove)
goal:
No subgoals!
theory GraphProof

lemma ex_least_nat:
  "\<exists>n. P n \<Longrightarrow> \<exists>n :: nat. P n \<and> (\<forall>i < n. \<not> P i)" apply clarsimp apply (case_tac "n = 0") apply fastforce apply (cut_tac P="\<lambda>i. i \<noteq> 0 \<and> P i" in ex_least_nat_le, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>n. P n \<Longrightarrow> \<exists>n. P n \<and> (\<forall>i<n. \<not> P i) proof (prove)
goal (1 subgoal):
 1. \<And>n. P n \<Longrightarrow> \<exists>n. P n \<and> (\<forall>i<n. \<not> P i) proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>P n; n = 0\<rbrakk> \<Longrightarrow> \<exists>n. P n \<and> (\<forall>i<n. \<not> P i)
 2. \<And>n. \<lbrakk>P n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n. P n \<and> (\<forall>i<n. \<not> P i) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>P n; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>n. P n \<and> (\<forall>i<n. \<not> P i) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma exec_trace_end_SomeD:
  "trace_end tr = Some v \<Longrightarrow> tr \<in> exec_trace Gamma f
    \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None
        \<and> (\<exists>nn st g. v = [(nn, st, g)] \<and> nn \<in> {Ret, Err})" apply (frule exec_trace_nat_trace) apply (drule(1) trace_end_SomeD) apply clarsimp apply (frule_tac i=n in exec_trace_Nil) apply (case_tac "fst (hd v)", auto simp add: continuing_def split: list.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end tr = Some v; tr \<in> exec_trace Gamma f\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> (\<exists>nn st g. v = [(nn, st, g)] \<and> nn \<in> {Ret, Err}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end tr = Some v; tr \<in> exec_trace Gamma f; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma)\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> (\<exists>nn st g. v = [(nn, st, g)] \<and> nn \<in> {Ret, Err}) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> \<not> continuing v\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> (\<exists>nn st g. v = [(nn, st, g)] \<and> nn \<in> {Ret, Err}) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr n = Some v; tr (Suc n) = None; \<not> continuing v\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> (\<exists>nn. (\<exists>st g. v = [(nn, st, g)]) \<and> (nn = Ret \<or> nn = Err)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>tr \<in> exec_trace Gamma f; tr \<in> nat_trace_rel continuing (exec_graph_step Gamma); tr n = Some v; tr (Suc n) = None; \<not> continuing v; tr n \<noteq> Some []\<rbrakk> \<Longrightarrow> \<exists>n. tr n = Some v \<and> tr (Suc n) = None \<and> (\<exists>nn. (\<exists>st g. v = [(nn, st, g)]) \<and> (nn = Ret \<or> nn = Err)) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma reachable_from_Ret:
  "((Ret, nn) \<notin> reachable_step' gf)" by (simp add: reachable_step_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Ret, nn) \<notin> reachable_step' gf
theory GraphProof

lemma first_reached_propD:
  "first_reached_prop addrs propn trs
    \<Longrightarrow> \<exists>addr \<in> set addrs. propn addr trs
    \<and> (\<forall>propn. first_reached_prop addrs propn trs = propn addr trs)" by (induct addrs, simp_all split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. first_reached_prop addrs propn trs \<Longrightarrow> \<exists>addr\<in>set addrs. propn addr trs \<and> (\<forall>propn. first_reached_prop addrs propn trs = propn addr trs)
theory GraphProof

lemma double_pc_reds:
  "double_pc (False, nn, restrs) trs = pc nn restrs (fst trs)"
  "double_pc (True, nn, restrs) trs = pc nn restrs (snd trs)" by (simp_all add: double_pc_def pc_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. double_pc (False, nn, restrs) trs = pc nn restrs (fst trs) &&& double_pc (True, nn, restrs) trs = pc nn restrs (snd trs)
theory GraphProof

lemma merge_opt_simps[simp]:
  "merge_opt (Some x) v = Some x"
  "merge_opt None v = v" by (simp_all add: merge_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. merge_opt (Some x) v = Some x &&& merge_opt None v = v
theory GraphProof

lemma fold_merge_opt_Nones_eq:
  "(\<forall>v \<in> set xs. v = None) \<Longrightarrow> fold merge_opt xs v = v" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>v\<in>set xs. v = None \<Longrightarrow> fold merge_opt xs v = v
theory GraphProof

lemma set_zip_rev:
  "length xs = length ys \<Longrightarrow> set (zip xs ys) = set (zip (rev xs) (rev ys))" by (simp add: zip_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> set (zip xs ys) = set (zip (rev xs) (rev ys))
theory GraphProof

lemma pred_restrs:
  "\<lbrakk> tr \<in> exec_trace Gamma f; trace_bottom_addr tr i = Some nn \<rbrakk>
    \<Longrightarrow> restrs_condition tr restrs (Suc i)
        = restrs_condition tr (if trace_addr tr i = None then restrs
            else pred_restrs nn restrs) i" apply (clarsimp simp: restrs_condition_def Collect_less_Suc all_conj_distrib
                        pred_restrs_def
                 split: if_split_asm next_node.split) apply (auto simp: trace_addr_trace_bottom_addr_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; trace_bottom_addr tr i = Some nn\<rbrakk> \<Longrightarrow> restrs_condition tr restrs (Suc i) = restrs_condition tr (if trace_addr tr i = None then restrs else pred_restrs nn restrs) i proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; trace_bottom_addr tr i = Some nn\<rbrakk> \<Longrightarrow> (\<forall>x1. nn = NextNode x1 \<longrightarrow> (\<exists>y. trace_addr tr i = Some y) \<longrightarrow> ((\<forall>m. trace_addr tr i = Some (NextNode m) \<longrightarrow> Suc (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)}) \<in> restrs m) \<and> (\<forall>m. trace_addr tr i \<noteq> Some (NextNode m) \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m)) = (Suc (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode x1)}) \<in> restrs x1 \<and> (\<forall>m. m \<noteq> x1 \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m))) \<and> (nn = Ret \<longrightarrow> (\<exists>y. trace_addr tr i = Some y) \<longrightarrow> ((\<forall>m. trace_addr tr i = Some (NextNode m) \<longrightarrow> Suc (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)}) \<in> restrs m) \<and> (\<forall>m. trace_addr tr i \<noteq> Some (NextNode m) \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m)) = (\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m)) \<and> (nn = Err \<longrightarrow> (\<exists>y. trace_addr tr i = Some y) \<longrightarrow> ((\<forall>m. trace_addr tr i = Some (NextNode m) \<longrightarrow> Suc (card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)}) \<in> restrs m) \<and> (\<forall>m. trace_addr tr i \<noteq> Some (NextNode m) \<longrightarrow> card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m)) = (\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m)) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma visit_inconsistent:
  "restrs i = {} \<Longrightarrow> visit tr nn restrs = None" by (auto simp add: visit_def restrs_condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. restrs i = {} \<Longrightarrow> visit tr nn restrs = None
theory GraphProof

lemma exec_trace_step:
  "tr \<in> exec_trace Gamma f
    \<Longrightarrow> tr i = Some stack
    \<Longrightarrow> continuing stack
    \<Longrightarrow> \<exists>stack'. tr (Suc i) = Some stack' \<and> (stack, stack') \<in> exec_graph_step Gamma" apply (frule_tac i=i in exec_trace_step_cases) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some stack; continuing stack\<rbrakk> \<Longrightarrow> \<exists>stack'. tr (Suc i) = Some stack' \<and> (stack, stack') \<in> exec_graph_step Gamma proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma f; tr i = Some stack; continuing stack; 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> \<exists>stack'. tr (Suc i) = Some stack' \<and> (stack, stack') \<in> exec_graph_step Gamma proof (prove)
goal:
No subgoals!
theory GraphProof

lemma if_x_None_eq_Some:
  "((if P then x else None) = Some y) = (P \<and> x = Some y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then x else None) = Some y) = (P \<and> x = Some y)
theory GraphProof

lemma subtract_le_nat:
  "((a :: nat) \<le> a - b) = (a = 0 \<or> b = 0)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<le> a - b) = (a = 0 \<or> b = 0)
theory GraphProof

lemma bottom_addr_only:
  "trace_addr tr i = None \<Longrightarrow> trace_bottom_addr tr i = Some nn
    \<Longrightarrow> \<exists>x x' xs. tr i = Some (x # x' # xs) \<and> nn = fst (last (x' # xs))" apply (clarsimp simp: trace_addr_def trace_bottom_addr_def
                 split: option.split_asm list.split_asm) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr i = None; trace_bottom_addr tr i = Some nn\<rbrakk> \<Longrightarrow> \<exists>x x' xs. tr i = Some (x # x' # xs) \<and> nn = fst (last (x' # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a aa b ab ac ba x22a. \<lbrakk>nn = fst (last x22a); tr i = Some ((a, aa, b) # (ab, ac, ba) # x22a); x22a \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>ad ae bb af ag bc xs. xs \<noteq> [] \<and> (xs \<noteq> [] \<longrightarrow> a = ad \<and> aa = ae \<and> b = bb \<and> ab = af \<and> ac = ag \<and> ba = bc \<and> x22a = xs \<and> fst (last x22a) = fst (last xs)) proof (prove)
goal:
No subgoals!
theory GraphProof

lemma restrs_condition_no_change:
  "restrs_condition tr restrs i
    \<Longrightarrow> j \<ge> i
    \<Longrightarrow> (\<forall>k \<in> {i ..< j}. trace_addr tr k = None)
    \<Longrightarrow> restrs_condition tr restrs j" apply (clarsimp simp: restrs_condition_def) apply (rule_tac P="\<lambda>S. card S \<in> SS" for SS in subst[rotated]) apply (erule spec) apply (auto intro: linorder_not_le[THEN iffD1, OF notI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>restrs_condition tr restrs i; i \<le> j; \<forall>k\<in>{i..<j}. trace_addr tr k = None\<rbrakk> \<Longrightarrow> restrs_condition tr restrs j proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m; i \<le> j; \<forall>k\<in>{i..<j}. trace_addr tr k = None\<rbrakk> \<Longrightarrow> card {i. i < j \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs m proof (prove)
goal (2 subgoals):
 1. \<And>m. \<lbrakk>\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m; i \<le> j; \<forall>k\<in>{i..<j}. trace_addr tr k = None\<rbrakk> \<Longrightarrow> card (?s1 m) \<in> restrs m
 2. \<And>m. \<lbrakk>\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m; i \<le> j; \<forall>k\<in>{i..<j}. trace_addr tr k = None\<rbrakk> \<Longrightarrow> ?s1 m = {i. i < j \<and> trace_addr tr i = Some (NextNode m)} proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>\<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m; i \<le> j; \<forall>k\<in>{i..<j}. trace_addr tr k = None\<rbrakk> \<Longrightarrow> {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} = {i. i < j \<and> trace_addr tr i = Some (NextNode m)} proof (prove)
goal:
No subgoals!
theory GraphProof

lemma trace_end_exec_SomeI:
  "tr \<in> exec_trace Gamma fn
    \<Longrightarrow> tr i = Some stk
    \<Longrightarrow> tr (Suc i) = None
    \<Longrightarrow> trace_end tr = Some stk" apply (clarsimp simp: trace_end_def exI[where x="Suc i"]) apply (drule(1) exec_trace_None_dom_subset) apply (subst Max_eqI[where x=i], auto elim: finite_subset) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some stk; tr (Suc i) = None\<rbrakk> \<Longrightarrow> trace_end tr = Some stk proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some stk; tr (Suc i) = None\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = Some stk proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; tr i = Some stk; dom tr \<subseteq> {..<Suc i}\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) = Some stk proof (prove)
goal:
No subgoals!
theory GraphProof

lemma function_call_trace_eq:
  assumes tr: "tr \<in> exec_trace Gamma fname"
    "Gamma fname = Some f"
    "wf_graph_function f ilen olen"
  and i: "trace_addr tr i = Some (NextNode n)"
    "restrs_condition tr restrs i"
  and cut: "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})"
    "(NextNode n, NextNode n) \<notin> trancl (reachable_step' f \<inter> {(x, y). x \<notin> set cuts})"
    shows "function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr)" proof - have P: "\<forall>j < i. trace_addr tr j = Some (NextNode n)
       \<longrightarrow> \<not> restrs_condition tr restrs j" using restrs_single_visit[OF tr _ _ i cut] by clarsimp note eq = Least_equality[where x=i, OF _ ccontr, unfolded linorder_not_le] show ?thesis using i apply (clarsimp simp: function_call_trace_def pc_def visit_known P
                   dest!: trace_addr_SomeD) apply (subst eq, auto simp: i P) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (state)
goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (prove)
goal (1 subgoal):
 1. \<forall>j<i. trace_addr tr j = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs j proof (prove)
using this:
\<lbrakk>trace_addr tr ?i = Some (NextNode n); restrs_condition tr restrs ?i\<rbrakk> \<Longrightarrow> ?i = i

goal (1 subgoal):
 1. \<forall>j<i. trace_addr tr j = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs j proof (state)
this:
\<forall>j<i. trace_addr tr j = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs j

goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (state)
this:
\<lbrakk>?P i; \<And>y. \<lbrakk>?P y; y < i\<rbrakk> \<Longrightarrow> False\<rbrakk> \<Longrightarrow> Least ?P = i

goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (prove)
goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (prove)
using this:
trace_addr tr i = Some (NextNode n)
restrs_condition tr restrs i

goal (1 subgoal):
 1. function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr) proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>restrs_condition tr restrs i; tr i = Some [(NextNode n, st, g)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc (LEAST i. trace_addr tr i = Some (NextNode n) \<and> restrs_condition tr restrs i)) (Suc 0) tr = trace_drop_n (Suc i) (Suc 0) tr proof (prove)
goal:
No subgoals! proof (state)
this:
function_call_trace n restrs tr = Some (trace_drop_n (Suc i) 1 tr)

goal:
No subgoals!
theory GraphProof

lemma trace_end_Nil:
  "tr \<in> exec_trace Gamma f
    \<Longrightarrow> trace_end tr \<noteq> Some []" by (auto dest: exec_trace_end_SomeD simp: exec_trace_Nil)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tr \<in> exec_trace Gamma f \<Longrightarrow> trace_end tr \<noteq> Some []
theory GraphProof

lemma visit_Call_loop_lemma:
  "(nn, NextNode n) \<notin> rtrancl (reachable_step' f \<inter> S)
    \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs)
    \<Longrightarrow> converse (reachable_step' f) `` {nn} \<subseteq> {NextNode n}
    \<Longrightarrow> (nn, nn) \<notin> trancl (reachable_step' f \<inter> S)
        \<and> (NextNode n, NextNode n) \<notin> trancl (reachable_step' f \<inter> S)" apply (simp add: not_trancl_converse_step) apply (clarsimp simp: reachable_step_def[THEN eqset_imp_iff] dest!: tranclD) apply (erule disjE, simp_all) apply (erule converse_rtranclE, simp_all add: reachable_step_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nn, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>*; function_graph f n = Some (node.Call nn fname inputs outputs); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}\<rbrakk> \<Longrightarrow> (nn, nn) \<notin> (reachable_step' f \<inter> S)\<^sup>+ \<and> (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(nn, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>*; function_graph f n = Some (node.Call nn fname inputs outputs); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}\<rbrakk> \<Longrightarrow> (NextNode n, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>+ proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>(nn, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>*; function_graph f n = Some (node.Call nn fname inputs outputs); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; (z, NextNode n) \<in> (reachable_step' f \<inter> S)\<^sup>*; z = nn \<or> z = Err; (NextNode n, z) \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>(nn, NextNode n) \<notin> (reachable_step' f \<inter> S)\<^sup>*; function_graph f n = Some (node.Call nn fname inputs outputs); (reachable_step' f)\<inverse> `` {nn} \<subseteq> {NextNode n}; (Err, NextNode n) \<in> (reachable_step' f \<inter> S)\<^sup>*; (NextNode n, Err) \<in> S; z = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphProof

lemma pred_restrs_cut:
  "(\<exists>y. restrs x \<subseteq> {y}) \<Longrightarrow> (\<exists>y. pred_restrs nn restrs x \<subseteq> {y})" apply (clarsimp simp: pred_restrs_def split: next_node.split) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>y. restrs x \<subseteq> {y} \<Longrightarrow> \<exists>y. pred_restrs nn restrs x \<subseteq> {y} proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>restrs x \<subseteq> {y}; nn = NextNode x\<rbrakk> \<Longrightarrow> \<exists>y. {xa. Suc xa \<in> restrs x} \<subseteq> {y} proof (prove)
goal:
No subgoals!
theory GraphProof

lemma pred_restrs_cut2:
  "\<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y})
    \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs nn restrs x \<subseteq> {y})" by (metis pred_restrs_cut)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. restrs x \<subseteq> {y}) \<Longrightarrow> \<forall>x. NextNode x \<in> set cuts \<longrightarrow> (\<exists>y. pred_restrs nn restrs x \<subseteq> {y})
theory GraphProof

lemma not_finite_two:
  "\<not> finite S \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y" apply (case_tac "\<exists>x. x \<in> S") apply (rule ccontr, clarsimp) apply (erule notE, rule_tac B="{x}" in finite_subset) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. infinite S \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<lbrakk>infinite S; \<exists>x. x \<in> S\<rbrakk> \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y
 2. \<lbrakk>infinite S; \<nexists>x. x \<in> S\<rbrakk> \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>infinite S; \<forall>x. x \<in> S \<longrightarrow> (\<forall>y. y \<in> S \<longrightarrow> x = y); x \<in> S\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>infinite S; \<nexists>x. x \<in> S\<rbrakk> \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<forall>x. x \<in> S \<longrightarrow> (\<forall>y. y \<in> S \<longrightarrow> x = y); x \<in> S\<rbrakk> \<Longrightarrow> S \<subseteq> {x}
 2. \<And>x. \<lbrakk>\<forall>x. x \<in> S \<longrightarrow> (\<forall>y. y \<in> S \<longrightarrow> x = y); x \<in> S\<rbrakk> \<Longrightarrow> finite {x}
 3. \<lbrakk>infinite S; \<nexists>x. x \<in> S\<rbrakk> \<Longrightarrow> \<exists>x y. x \<in> S \<and> y \<in> S \<and> x \<noteq> y proof (prove)
goal:
No subgoals!
theory GraphProof

lemma infinite_subset:
  "\<not> finite S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> \<not> finite T" by (metis finite_subset)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>infinite S; S \<subseteq> T\<rbrakk> \<Longrightarrow> infinite T
theory GraphProof

lemma restrs_condition_unique:
  "restrs_condition tr (restrs_list ((n, [x]) # rs)) k
    \<Longrightarrow> restrs_condition tr (restrs_list ((n, [y]) # rs)) k
    \<Longrightarrow> x = y" by (clarsimp simp: restrs_condition_def restrs_list_Cons
              split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>restrs_condition tr (restrs_list ((n, [x]) # rs)) k; restrs_condition tr (restrs_list ((n, [y]) # rs)) k\<rbrakk> \<Longrightarrow> x = y