theory GraphProof

lemma visit_extended_pred:
  "\<lbrakk> trace_addr tr i = Some addr; restrs_condition tr restrs i;
        tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen;
        converse (reachable_step' f) `` {addr} \<subseteq> S;
        addr \<noteq> NextNode (entry_point f) \<rbrakk>
    \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S
        \<and> j < i
        \<and> (trace_addr tr ` {Suc j ..< i} \<subseteq> {None})
        \<and> (trace_bottom_addr tr ` {Suc j ..< i} \<subseteq> {Some nn'})
        \<and> restrs_condition tr (pred_restrs nn' restrs) j" apply (frule(5) visit_immediate_pred) apply (clarsimp simp: pred_restrs) apply (frule(4) trace_bottom_addr_trace_addr_prev) apply clarsimp apply (rule_tac x=j in exI, simp) apply (clarsimp split: if_split_asm) apply (simp add: atLeastLessThanSuc_atLeastAtMost) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr i = Some addr; restrs_condition tr restrs i; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f)\<rbrakk> \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S \<and> j < i \<and> trace_addr tr ` {Suc j..<i} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<i} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_addr tr i = Some addr; restrs_condition tr restrs i; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); \<exists>i' nn'. i = Suc i' \<and> nn' \<in> S \<and> trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S \<and> j < i \<and> trace_addr tr ` {Suc j..<i} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<i} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<And>i' nn'. \<lbrakk>trace_addr tr (Suc i') = Some addr; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs) i'; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); i = Suc i'; nn' \<in> S; trace_bottom_addr tr i' = Some nn'\<rbrakk> \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S \<and> j < Suc i' \<and> trace_addr tr ` {Suc j..<Suc i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<Suc i'} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<And>i' nn'. \<lbrakk>trace_addr tr (Suc i') = Some addr; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs) i'; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); i = Suc i'; nn' \<in> S; trace_bottom_addr tr i' = Some nn'; \<exists>j. trace_addr tr j = Some nn' \<and> (i' = j \<or> trace_addr tr i' = None) \<and> trace_addr tr ` {Suc j..i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..i'} \<subseteq> {Some nn'} \<and> j \<le> i' \<and> restrs_condition tr (if i' = j then if trace_addr tr i' = None then restrs else pred_restrs nn' restrs else pred_restrs nn' (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs)) j\<rbrakk> \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S \<and> j < Suc i' \<and> trace_addr tr ` {Suc j..<Suc i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<Suc i'} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' j. \<lbrakk>trace_addr tr (Suc i') = Some addr; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs) i'; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); i = Suc i'; nn' \<in> S; trace_bottom_addr tr i' = Some nn'; trace_addr tr j = Some nn'; i' = j \<or> trace_addr tr i' = None; trace_addr tr ` {Suc j..i'} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..i'} \<subseteq> {Some nn'}; j \<le> i'; restrs_condition tr (if i' = j then if trace_addr tr i' = None then restrs else pred_restrs nn' restrs else pred_restrs nn' (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs)) j\<rbrakk> \<Longrightarrow> \<exists>j nn'. trace_addr tr j = Some nn' \<and> nn' \<in> S \<and> j < Suc i' \<and> trace_addr tr ` {Suc j..<Suc i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<Suc i'} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' j. \<lbrakk>trace_addr tr (Suc i') = Some addr; restrs_condition tr (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs) i'; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); i = Suc i'; nn' \<in> S; trace_bottom_addr tr i' = Some nn'; trace_addr tr j = Some nn'; i' = j \<or> trace_addr tr i' = None; trace_addr tr ` {Suc j..i'} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..i'} \<subseteq> {Some nn'}; j \<le> i'; restrs_condition tr (if i' = j then if trace_addr tr i' = None then restrs else pred_restrs nn' restrs else pred_restrs nn' (if trace_addr tr i' = None then restrs else pred_restrs nn' restrs)) j\<rbrakk> \<Longrightarrow> trace_addr tr ` {Suc j..<Suc i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<Suc i'} \<subseteq> {Some nn'} \<and> restrs_condition tr (pred_restrs nn' restrs) j proof (prove)
goal (1 subgoal):
 1. \<And>i' nn' j. \<lbrakk>trace_addr tr (Suc i') = Some addr; trace_addr tr i' = None; restrs_condition tr restrs i'; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; wf_graph_function f ilen olen; (reachable_step' f)\<inverse> `` {addr} \<subseteq> S; addr \<noteq> NextNode (entry_point f); i = Suc i'; nn' \<in> S; trace_bottom_addr tr i' = Some nn'; trace_addr tr j = Some nn'; trace_addr tr ` {Suc j..i'} \<subseteq> {None}; trace_bottom_addr tr ` {Suc j..i'} \<subseteq> {Some nn'}; j \<le> i'; i' \<noteq> j; restrs_condition tr (pred_restrs nn' restrs) j\<rbrakk> \<Longrightarrow> trace_addr tr ` {Suc j..<Suc i'} \<subseteq> {None} \<and> trace_bottom_addr tr ` {Suc j..<Suc i'} \<subseteq> {Some nn'} proof (prove)
goal:
No subgoals!