theory GraphProof

lemma exec_trace_step_reachable_induct2:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf
    \<Longrightarrow> wf_graph_function gf ilen olen
    \<Longrightarrow> trace_bottom_addr tr (Suc i) = Some addr
    \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf))
        \<and> trace_bottom_addr tr i \<noteq> None
        \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None
            \<or> trace_addr tr (Suc i) = Some addr
                \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf)" apply (induct i arbitrary: addr) apply (frule(2) exec_trace_step_reachable_induct) apply (clarsimp simp: exec_trace_def trace_bottom_addr_def
                         wf_graph_function_def split: graph_function.split_asm) apply (frule(2) exec_trace_step_reachable_induct) apply atomize apply (case_tac "trace_bottom_addr tr (Suc i)", simp_all) apply clarsimp apply (frule_tac i=i in exec_trace_step_reachable_induct, simp) apply clarsimp apply (erule disjE, simp_all) apply (simp add: wf_graph_function_def split: graph_function.split_asm) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf) proof (prove)
goal (2 subgoals):
 1. \<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc 0) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr 0 = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr 0 \<noteq> None \<and> (trace_bottom_addr tr 0 = Some addr \<and> trace_addr tr (Suc 0) = None \<or> trace_addr tr (Suc 0) = Some addr \<and> (the (trace_bottom_addr tr 0), addr) \<in> reachable_step' gf)
 2. \<And>i addr. \<lbrakk>\<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf) proof (prove)
goal (2 subgoals):
 1. \<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc 0) = Some addr; (\<forall>n. trace_bottom_addr tr 0 = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr 0 \<noteq> None \<and> (trace_bottom_addr tr 0 = Some addr \<and> trace_addr tr (Suc 0) = None \<or> trace_addr tr (Suc 0) = Some addr \<and> (the (trace_bottom_addr tr 0), addr) \<in> reachable_step' gf)\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr 0 = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr 0 \<noteq> None \<and> (trace_bottom_addr tr 0 = Some addr \<and> trace_addr tr (Suc 0) = None \<or> trace_addr tr (Suc 0) = Some addr \<and> (the (trace_bottom_addr tr 0), addr) \<in> reachable_step' gf)
 2. \<And>i addr. \<lbrakk>\<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr. \<lbrakk>\<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr. \<lbrakk>\<And>addr. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc i) = Some addr\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf)\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr. \<lbrakk>\<forall>addr. tr \<in> exec_trace Gamma fn \<longrightarrow> Gamma fn = Some gf \<longrightarrow> wf_graph_function gf ilen olen \<longrightarrow> trace_bottom_addr tr (Suc i) = Some addr \<longrightarrow> (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some addr \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some addr \<and> (the (trace_bottom_addr tr i), addr) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf)\<rbrakk> \<Longrightarrow> (\<forall>n. trace_bottom_addr tr (Suc i) = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> trace_bottom_addr tr (Suc i) \<noteq> None \<and> (trace_bottom_addr tr (Suc i) = Some addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (the (trace_bottom_addr tr (Suc i)), addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr a. \<lbrakk>(\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (\<exists>y. trace_bottom_addr tr i = Some y) \<and> (trace_bottom_addr tr i = Some a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (the (trace_bottom_addr tr i), a) \<in> reachable_step' gf); tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf) proof (prove)
goal (2 subgoals):
 1. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y\<rbrakk> \<Longrightarrow> trace_bottom_addr tr (Suc i) = Some (?addr28 i addr a y)
 2. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y; (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some (?addr28 i addr a y) \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some (?addr28 i addr a y) \<and> (the (trace_bottom_addr tr i), ?addr28 i addr a y) \<in> reachable_step' gf)\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf) proof (prove)
goal (2 subgoals):
 1. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y\<rbrakk> \<Longrightarrow> a = ?addr28 i addr a y
 2. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y; (\<forall>n. trace_bottom_addr tr i = Some (NextNode n) \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> trace_bottom_addr tr i \<noteq> None \<and> (trace_bottom_addr tr i = Some (?addr28 i addr a y) \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some (?addr28 i addr a y) \<and> (the (trace_bottom_addr tr i), ?addr28 i addr a y) \<in> reachable_step' gf)\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr a y. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some gf; wf_graph_function gf ilen olen; trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom (function_graph gf); y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf; trace_bottom_addr tr i = Some y; y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step' gf\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom (function_graph gf)) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step' gf) proof (prove)
goal (1 subgoal):
 1. \<And>i addr a y x1 x2 x3 x4. \<lbrakk>trace_bottom_addr tr (Suc (Suc i)) = Some addr; (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom x3) \<longrightarrow> a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step x3; trace_bottom_addr tr (Suc i) = Some a; \<forall>n. y = NextNode n \<longrightarrow> n \<in> dom x3; trace_bottom_addr tr i = Some y; y = a \<and> trace_addr tr (Suc i) = None \<or> trace_addr tr (Suc i) = Some a \<and> (y, a) \<in> reachable_step x3; tr \<in> exec_trace Gamma fn; Gamma fn = Some (GraphFunction x1 x2 x3 x4); gf = GraphFunction x1 x2 x3 x4; distinct x1 \<and> distinct x2 \<and> length x1 = ilen \<and> length x2 = olen \<and> (\<forall>nn i. (nn, NextNode i) \<in> reachable_step x3 \<longrightarrow> i \<in> dom x3) \<and> x4 \<in> dom x3\<rbrakk> \<Longrightarrow> (\<forall>n. a = NextNode n \<longrightarrow> n \<in> dom x3) \<and> (a = addr \<and> trace_addr tr (Suc (Suc i)) = None \<or> trace_addr tr (Suc (Suc i)) = Some addr \<and> (a, addr) \<in> reachable_step x3) proof (prove)
goal:
No subgoals!