theory GraphProof

lemma restrs_single_visit_neq:
  "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 \<Longrightarrow> False" apply (frule(5) reachable_trace) apply (erule notE, erule trancl_mono) apply clarsimp apply (case_tac a, simp_all) apply (drule spec, drule(1) mp, clarsimp) apply (clarsimp simp: restrs_condition_def) apply (drule spec, drule(1) subsetD[rotated])+ apply clarsimp apply (frule card_seteq[rotated -1, OF eq_imp_le], simp, clarsimp)[1] apply (blast dest: linorder_not_less[THEN iffD2]) apply (simp add: reachable_step_def)+ 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; 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>+; i < j\<rbrakk> \<Longrightarrow> False 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>+; i < j; (nn, nn) \<in> (reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}})\<^sup>+\<rbrakk> \<Longrightarrow> False 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}); i < j\<rbrakk> \<Longrightarrow> reachable_step' f \<inter> {(x, y). Some x \<in> trace_addr tr ` {i..<j}} \<subseteq> reachable_step' f \<inter> {(x, y). x \<notin> set cuts} proof (prove)
goal (1 subgoal):
 1. \<And>a b x. \<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}); (a, b) \<in> reachable_step' f; Some a = trace_addr tr x; a \<in> set cuts; i \<le> x; x < j\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b x x1. \<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}); (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; a = NextNode x1\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b x x1 y. \<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; (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; restrs x1 \<subseteq> {y}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b x x1 y. \<lbrakk>tr \<in> exec_trace Gamma fname; Gamma fname = Some f; wf_graph_function f ilen olen; trace_addr tr i = Some nn; \<forall>m. card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode m)} \<in> restrs m; trace_addr tr j = Some nn; \<forall>m. card {i. i < j \<and> trace_addr tr i = Some (NextNode m)} \<in> restrs m; (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; restrs x1 \<subseteq> {y}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b x x1 y. \<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; (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; restrs x1 \<subseteq> {y}; card {ia. ia < i \<and> trace_addr tr ia = Some (NextNode x1)} \<in> {y}; card {i. i < j \<and> trace_addr tr i = Some (NextNode x1)} \<in> {y}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b x x1. \<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; (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; restrs x1 \<subseteq> {card {ia. ia < i \<and> trace_addr tr ia = trace_addr tr x}}; card {i. i < j \<and> trace_addr tr i = trace_addr tr x} = card {ia. ia < i \<and> trace_addr tr ia = trace_addr tr x}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>b x x1. \<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; (NextNode x1, b) \<in> reachable_step' f; Some (NextNode x1) = trace_addr tr x; NextNode x1 \<in> set cuts; i \<le> x; x < j; restrs x1 \<subseteq> {card {ia. ia < i \<and> trace_addr tr ia = trace_addr tr x}}; card {i. i < j \<and> trace_addr tr i = trace_addr tr x} = card {ia. ia < i \<and> trace_addr tr ia = trace_addr tr x}; {ia. ia < i \<and> trace_addr tr ia = trace_addr tr x} = {i. i < j \<and> trace_addr tr i = trace_addr tr x}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 3. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b x. \<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}); (Ret, b) \<in> reachable_step' f; Some Ret = trace_addr tr x; Ret \<in> set cuts; i \<le> x; x < j; a = Ret\<rbrakk> \<Longrightarrow> False
 2. \<And>a b x. \<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}); (Err, b) \<in> reachable_step' f; Some Err = trace_addr tr x; Err \<in> set cuts; i \<le> x; x < j; a = Err\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!