theory GraphProof

lemma exec_trace_pc_Call:
  "pc' n restrs tr
    \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> function_graph f n = Some (node.Call nn fname inps outps)
    \<Longrightarrow> Gamma fname = Some g
    \<Longrightarrow> (\<exists>x. restrs_condition tr restrs x \<and> trace_addr tr x = Some (NextNode n)
        \<and> (trace_drop_n (Suc x) 1 tr \<in> exec_trace Gamma fname)
        \<and> visit tr (NextNode n) restrs = Some (fst (snd (hd (the (tr x))))))" apply (clarsimp simp: pc_def visit_eqs elim!: exE[OF ex_least_nat] del: exE) apply (rule exI, rule conjI, assumption, simp) apply (rule conjI[rotated], blast) apply (clarsimp dest!: trace_addr_SomeD) apply (frule(1) exec_trace_invariant) apply (simp add: exec_graph_invariant_def) apply (erule(4) exec_trace_drop_n[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pc' n restrs tr; tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g\<rbrakk> \<Longrightarrow> \<exists>x. restrs_condition tr restrs x \<and> trace_addr tr x = Some (NextNode n) \<and> trace_drop_n (Suc x) 1 tr \<in> exec_trace Gamma fname \<and> visit tr (NextNode n) restrs = Some (fst (snd (hd (the (tr x))))) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; trace_addr tr i = Some (NextNode n); restrs_condition tr restrs i\<rbrakk> \<Longrightarrow> \<exists>x. restrs_condition tr restrs x \<and> trace_addr tr x = Some (NextNode n) \<and> trace_drop_n (Suc x) (Suc 0) tr \<in> exec_trace Gamma fname \<and> (\<exists>i. restrs_condition tr restrs i \<and> trace_addr tr i = Some (NextNode n) \<and> fst (snd (hd (the (tr x)))) = fst (snd (hd (the (tr i)))) \<and> (\<forall>j<i. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n))) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; trace_addr tr i = Some (NextNode n); restrs_condition tr restrs i\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname \<and> (\<exists>ia. restrs_condition tr restrs ia \<and> trace_addr tr ia = Some (NextNode n) \<and> fst (snd (hd (the (tr i)))) = fst (snd (hd (the (tr ia)))) \<and> (\<forall>j<ia. restrs_condition tr restrs j \<longrightarrow> trace_addr tr j \<noteq> Some (NextNode n))) proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; trace_addr tr i = Some (NextNode n); restrs_condition tr restrs i\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname proof (prove)
goal (1 subgoal):
 1. \<And>i st ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; restrs_condition tr restrs i; tr i = Some [(NextNode n, st, ga)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname proof (prove)
goal (1 subgoal):
 1. \<And>i st ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; restrs_condition tr restrs i; tr i = Some [(NextNode n, st, ga)]; exec_graph_invariant Gamma fn [(NextNode n, st, ga)]\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname proof (prove)
goal (1 subgoal):
 1. \<And>i st ga. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; function_graph f n = Some (node.Call nn fname inps outps); Gamma fname = Some g; \<forall>ia<i. trace_addr tr ia = Some (NextNode n) \<longrightarrow> \<not> restrs_condition tr restrs ia; restrs_condition tr restrs i; tr i = Some [(NextNode n, st, fn)]; ga = fn\<rbrakk> \<Longrightarrow> trace_drop_n (Suc i) (Suc 0) tr \<in> exec_trace Gamma fname proof (prove)
goal:
No subgoals!