theory GraphLang

lemma exec_graph_step_n_Err:
  "(((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n)
    \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack))
        \<and> drop n ((Err, st, graph) # stack) \<noteq> []" proof (induct n arbitrary: stack') case 0 show ?case using 0 by (auto simp add: exec_graph_n_def) next case (Suc n) show ?case using Suc.prems apply (clarsimp simp: exec_graph_n_def relcomp_unfold linorder_not_le) apply (drule exec_graph_step_def[THEN eqset_imp_iff, THEN iffD1]) apply (case_tac y, simp_all) apply (drule Suc.hyps[rotated, unfolded exec_graph_n_def]) apply (simp only: neq_Nil_conv) apply (clarsimp simp: linorder_not_le drop_eq_Cons) apply (clarsimp split: list.split_asm) apply (case_tac zs, simp_all) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> [] proof (state)
goal (2 subgoals):
 1. \<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma 0 \<Longrightarrow> stack' = upd_stack Err id (drop 0 ((Err, st, graph) # stack)) \<and> drop 0 ((Err, st, graph) # stack) \<noteq> []
 2. \<And>n stack'. \<lbrakk>\<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []; ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (state)
this:
((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma 0

goal (2 subgoals):
 1. \<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma 0 \<Longrightarrow> stack' = upd_stack Err id (drop 0 ((Err, st, graph) # stack)) \<and> drop 0 ((Err, st, graph) # stack) \<noteq> []
 2. \<And>n stack'. \<lbrakk>\<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []; ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. stack' = upd_stack Err id (drop 0 ((Err, st, graph) # stack)) \<and> drop 0 ((Err, st, graph) # stack) \<noteq> [] proof (prove)
using this:
((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma 0

goal (1 subgoal):
 1. stack' = upd_stack Err id (drop 0 ((Err, st, graph) # stack)) \<and> drop 0 ((Err, st, graph) # stack) \<noteq> [] proof (state)
this:
stack' = upd_stack Err id (drop 0 ((Err, st, graph) # stack)) \<and> drop 0 ((Err, st, graph) # stack) \<noteq> []

goal (1 subgoal):
 1. \<And>n stack'. \<lbrakk>\<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []; ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (state)
goal (1 subgoal):
 1. \<And>n stack'. \<lbrakk>\<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []; ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (state)
this:
((Err, st, graph) # stack, ?stack') \<in> exec_graph_n Gamma n \<Longrightarrow> ?stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []
((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)

goal (1 subgoal):
 1. \<And>n stack'. \<lbrakk>\<And>stack'. ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma n \<Longrightarrow> stack' = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []; ((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (prove)
using this:
((Err, st, graph) # stack, stack') \<in> exec_graph_n Gamma (Suc n)

goal (1 subgoal):
 1. stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>((Err, st, graph) # stack, y) \<in> exec_graph_step Gamma ^^ n; (y, stack') \<in> exec_graph_step Gamma\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop n stack) \<and> n < length stack proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>((Err, st, graph) # stack, y) \<in> exec_graph_step Gamma ^^ n; (y, stack') \<in> {(stack, stack'). case stack of [] \<Rightarrow> False | (NextNode nn, st, fname) # xa \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction x xa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id stack | Some node \<Rightarrow> stack' \<in> exec_node Gamma st node stack | [(Ret, st, x)] \<Rightarrow> False | (Ret, st, x) # (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction x xa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl stack) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma st node (tl stack) | (Ret, st, x) # (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl stack) | [(Err, b)] \<Rightarrow> False | (Err, b) # a # lista \<Rightarrow> stack' = upd_stack Err id (tl stack)}\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop n stack) \<and> n < length stack proof (prove)
goal (1 subgoal):
 1. \<And>y a list. \<lbrakk>((Err, st, graph) # stack, a # list) \<in> exec_graph_step Gamma ^^ n; case a of (NextNode nn, st, fname) \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (a # list) | Some node \<Rightarrow> stack' \<in> exec_node Gamma st node (a # list) | (Ret, st, x) \<Rightarrow> case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (a # list)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma st node (tl (a # list)) | (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl (a # list)) | (Err, b) \<Rightarrow> case list of [] \<Rightarrow> False | aa # lista \<Rightarrow> stack' = upd_stack Err id (tl (a # list)); y = a # list\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop n stack) \<and> n < length stack proof (prove)
goal (1 subgoal):
 1. \<And>y a list. \<lbrakk>case a of (NextNode nn, st, fname) \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (a # list) | Some node \<Rightarrow> stack' \<in> exec_node Gamma st node (a # list) | (Ret, st, x) \<Rightarrow> case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa graph xb) \<Rightarrow> case graph nn of None \<Rightarrow> stack' = upd_stack Err id (tl (a # list)) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma st node (tl (a # list)) | (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl (a # list)) | (Err, b) \<Rightarrow> case list of [] \<Rightarrow> False | aa # lista \<Rightarrow> stack' = upd_stack Err id (tl (a # list)); y = a # list; a # list = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> drop n ((Err, st, graph) # stack) \<noteq> []\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop n stack) \<and> n < length stack proof (prove)
goal (1 subgoal):
 1. \<And>y a list. \<lbrakk>case a of (NextNode nn, sta, fname) \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa grapha xb) \<Rightarrow> case grapha nn of None \<Rightarrow> stack' = upd_stack Err id (upd_stack Err id (drop n ((Err, st, graph) # stack))) | Some node \<Rightarrow> stack' \<in> exec_node Gamma sta node (upd_stack Err id (drop n ((Err, st, graph) # stack))) | (Ret, sta, x) \<Rightarrow> case list of [] \<Rightarrow> False | (NextNode nn, xa, fname) # xb \<Rightarrow> case Gamma fname of None \<Rightarrow> False | Some (GraphFunction xa xaa grapha xb) \<Rightarrow> case grapha nn of None \<Rightarrow> stack' = upd_stack Err id (tl (upd_stack Err id (drop n ((Err, st, graph) # stack)))) | Some node \<Rightarrow> stack' \<in> exec_node_return Gamma sta node (tl (upd_stack Err id (drop n ((Err, st, graph) # stack)))) | (_, b) # xb \<Rightarrow> stack' = upd_stack Err id (tl (upd_stack Err id (drop n ((Err, st, graph) # stack)))) | (Err, b) \<Rightarrow> case list of [] \<Rightarrow> False | a # lista \<Rightarrow> stack' = upd_stack Err id (tl (upd_stack Err id (drop n ((Err, st, graph) # stack)))); y = upd_stack Err id (drop n ((Err, st, graph) # stack)); a # list = upd_stack Err id (drop n ((Err, st, graph) # stack)) \<and> (\<exists>y ys. drop n ((Err, st, graph) # stack) = y # ys)\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop n stack) \<and> n < length stack proof (prove)
goal (1 subgoal):
 1. \<And>aa b list ab zs. \<lbrakk>case list of [] \<Rightarrow> False | a # lista \<Rightarrow> stack' = upd_stack Err id (tl (upd_stack Err id (drop (length zs) ((Err, st, graph) # stack)))); (Err, st, graph) # stack = zs @ (ab, aa, b) # list; n = length zs\<rbrakk> \<Longrightarrow> stack' = upd_stack Err (\<lambda>a. a) (drop (length zs) stack) \<and> length zs < length stack proof (prove)
goal (1 subgoal):
 1. \<And>aa b ab zs a ac ba x22. \<lbrakk>(Err, st, graph) # stack = zs @ (ab, aa, b) # (a, ac, ba) # x22; n = length zs; stack' = (Err, ac, ba) # x22\<rbrakk> \<Longrightarrow> (Err, ac, ba) # x22 = upd_stack Err (\<lambda>a. a) (drop (length zs) stack) \<and> length zs < length stack proof (prove)
goal:
No subgoals! proof (state)
this:
stack' = upd_stack Err id (drop (Suc n) ((Err, st, graph) # stack)) \<and> drop (Suc n) ((Err, st, graph) # stack) \<noteq> []

goal:
No subgoals!