theory GraphProof

lemma exec_trace_reachable_step:
  "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f
    \<Longrightarrow> trace_addr tr (Suc i) = Some nn'
    \<Longrightarrow> nn' \<noteq> Err
    \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f" apply (clarsimp dest!: trace_addr_SomeD) apply (frule(1) exec_trace_invariant) apply (subgoal_tac "\<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack") prefer 2 apply (metis exec_trace_invariant) apply (frule_tac i=i in exec_trace_step_cases) apply (rule_tac x="the (trace_bottom_addr tr i)" in exI) apply (clarsimp simp: all_exec_graph_step_cases) apply (safe, simp_all add: reachable_step_def)[1] apply (auto simp: exec_graph_invariant_def trace_addr_def
                    get_state_function_call_def trace_bottom_addr_def
             split: graph_function.split_asm next_node.split option.splits node.splits
                    next_node.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; trace_addr tr (Suc i) = Some nn'; nn' \<noteq> Err\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (2 subgoals):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f
 2. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]\<rbrakk> \<Longrightarrow> \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack proof (prove)
goal (2 subgoals):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]\<rbrakk> \<Longrightarrow> \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack
 2. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn stack\<rbrakk> \<Longrightarrow> \<exists>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn 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>nn. (nn, nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; \<forall>stack. tr i = Some stack \<longrightarrow> exec_graph_invariant Gamma fn 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> (the (trace_bottom_addr tr i), nn') \<in> reachable_step' f proof (prove)
goal (1 subgoal):
 1. \<And>st g a aa b x22. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', st, g)]; exec_graph_invariant Gamma fn [(nn', st, g)]; exec_graph_invariant Gamma fn ((a, aa, b) # x22); tr i = Some ((a, aa, b) # x22); (\<exists>x1. a = NextNode x1 \<and> (\<exists>x2. Gamma b = Some x2 \<and> (\<exists>x1a x2a x3. (\<exists>x4. x2 = GraphFunction x1a x2a x3 x4) \<and> (\<exists>x2. x3 x1 = Some x2 \<and> ((\<exists>x12. x2 = node.Basic nn' x12 \<and> st = upd_vars x12 aa \<and> g = b \<and> [] = x22) \<or> (\<exists>x21 x22a x23. x2 = node.Cond x21 x22a x23 \<and> nn' = (if x23 aa then x21 else x22a) \<and> st = aa \<and> g = b \<and> [] = x22)))))) \<or> a = Ret \<and> (\<exists>a ab b x22a. x22 = (a, ab, b) # x22a \<and> (\<exists>x1. a = NextNode x1 \<and> (\<exists>x2. Gamma b = Some x2 \<and> (\<exists>x1a x2a x3. (\<exists>x4. x2 = GraphFunction x1a x2a x3 x4) \<and> (\<exists>x2. x3 x1 = Some x2 \<and> (\<exists>x31 x32 x33 x34. x2 = node.Call x31 x32 x33 x34 \<and> (\<exists>x2. Gamma x32 = Some x2 \<and> (\<exists>x1 x2a. (\<exists>x3 x4. x2 = GraphFunction x1 x2a x3 x4) \<and> nn' = x31 \<and> st = return_vars x2a x34 aa ab \<and> g = b \<and> [] = x22a))))))))\<rbrakk> \<Longrightarrow> (the (trace_bottom_addr tr i), nn') \<in> reachable_step' f proof (prove)
goal (3 subgoals):
 1. \<And>aa b x1 x1a x2a x3 x4 x12. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', upd_vars x12 aa, b)]; exec_graph_invariant Gamma fn [(nn', upd_vars x12 aa, b)]; exec_graph_invariant Gamma fn [(NextNode x1, aa, b)]; tr i = Some [(NextNode x1, aa, b)]; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Basic nn' x12)\<rbrakk> \<Longrightarrow> case the (trace_bottom_addr tr i) of NextNode i \<Rightarrow> case function_graph f i of None \<Rightarrow> False | Some (node.Basic c xa) \<Rightarrow> nn' = c | Some (node.Cond l r xa) \<Rightarrow> nn' = l \<or> nn' = r | Some (node.Call c xa xaa xb) \<Rightarrow> nn' = c \<or> nn' = Err | _ \<Rightarrow> False
 2. \<And>aa b x1 x1a x2a x3 x4 x21 x22a x23. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; (if x23 aa then x21 else x22a) \<noteq> Err; tr (Suc i) = Some [(if x23 aa then x21 else x22a, aa, b)]; exec_graph_invariant Gamma fn [(if x23 aa then x21 else x22a, aa, b)]; exec_graph_invariant Gamma fn [(NextNode x1, aa, b)]; tr i = Some [(NextNode x1, aa, b)]; Gamma b = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Cond x21 x22a x23); nn' = (if x23 aa then x21 else x22a)\<rbrakk> \<Longrightarrow> (x23 aa \<longrightarrow> (case the (trace_bottom_addr tr i) of NextNode i \<Rightarrow> case function_graph f i of None \<Rightarrow> False | Some (node.Basic c xa) \<Rightarrow> x21 = c | Some (node.Cond l r xa) \<Rightarrow> x21 = l \<or> x21 = r | Some (node.Call c xa xaa xb) \<Rightarrow> x21 = c \<or> x21 = Err | _ \<Rightarrow> False)) \<and> (\<not> x23 aa \<longrightarrow> (case the (trace_bottom_addr tr i) of NextNode i \<Rightarrow> case function_graph f i of None \<Rightarrow> False | Some (node.Basic c xa) \<Rightarrow> x22a = c | Some (node.Cond l r xa) \<Rightarrow> x22a = l \<or> x22a = r | Some (node.Call c xa xaa xb) \<Rightarrow> x22a = c \<or> x22a = Err | _ \<Rightarrow> False))
 3. \<And>aa b ac ba x1 x1a x2a x3 x4 x32 x33 x34 x1b x2d x3a x4a. \<lbrakk>tr \<in> exec_trace Gamma fn; Gamma fn = Some f; nn' \<noteq> Err; tr (Suc i) = Some [(nn', return_vars x2d x34 aa ac, ba)]; exec_graph_invariant Gamma fn [(nn', return_vars x2d x34 aa ac, ba)]; exec_graph_invariant Gamma fn [(Ret, aa, b), (NextNode x1, ac, ba)]; tr i = Some [(Ret, aa, b), (NextNode x1, ac, ba)]; Gamma ba = Some (GraphFunction x1a x2a x3 x4); x3 x1 = Some (node.Call nn' x32 x33 x34); Gamma x32 = Some (GraphFunction x1b x2d x3a x4a)\<rbrakk> \<Longrightarrow> case the (trace_bottom_addr tr i) of NextNode i \<Rightarrow> case function_graph f i of None \<Rightarrow> False | Some (node.Basic c xa) \<Rightarrow> nn' = c | Some (node.Cond l r xa) \<Rightarrow> nn' = l \<or> nn' = r | Some (node.Call c xa xaa xb) \<Rightarrow> nn' = c \<or> nn' = Err | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!