theory GraphProof

lemma restr_trace_refine_Err:
  "(\<not> pc Err restrs tr'
        \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr')
    \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr'" apply (clarsimp simp: restr_trace_refine_def) apply (erule impCE) apply simp apply (clarsimp simp: trace_refine2_def trace_refine_def) apply (drule(1) pc_Ret_Err_trace_end[where er=Err, simplified]) apply clarsimp apply (simp split: option.split list.split next_node.split) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> pc Err restrs tr' \<longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' \<Longrightarrow> restr_trace_refine prec Gamma1 fn1 Gamma2 fn2 rs1 rs2 orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>\<not> pc Err restrs tr' \<longrightarrow> (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'; tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf')\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); \<not> \<not> pc Err restrs tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); pc Err restrs tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); pc Err restrs tr'\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> case trace_end tr' of None \<Rightarrow> True | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (init_state fn1 gf xs))), function_outputs_st gf a) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (init_state fn2 gf' ys))), function_outputs_st gf' st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); \<exists>st g. trace_end tr' = Some [(Err, st, g)]\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> case trace_end tr' of None \<Rightarrow> True | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (init_state fn1 gf xs))), function_outputs_st gf a) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (init_state fn2 gf' ys))), function_outputs_st gf' st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (2 subgoals):
 1. \<And>gf gf' xs ys st g. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); trace_end tr' = Some [(Err, st, g)]\<rbrakk> \<Longrightarrow> case trace_end tr of None \<Rightarrow> case trace_end tr' of None \<Rightarrow> True | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # lista) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some [(Ret, a, bb)] \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some ((NextNode nat, b) # list) \<Rightarrow> False | Some [(Ret, st', xa)] \<Rightarrow> orel (switch_val fst (tuple_switch (acc_vars (function_inputs gf) (fst (snd (init_state fn1 gf xs))), function_outputs_st gf a) \<circ> snd) (tuple_switch (acc_vars (function_inputs gf') (fst (snd (init_state fn2 gf' ys))), function_outputs_st gf' st') \<circ> snd)) | Some ((Ret, st', xa) # ab # lista) \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ab # lista) \<Rightarrow> False | Some ((Ret, a, bb) # aa # lista) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # ac # listb) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> False | Some ((_, b) # list) \<Rightarrow> case trace_end tr' of None \<Rightarrow> \<not> prec | Some [] \<Rightarrow> False | Some [(Err, xa, xb)] \<Rightarrow> True | Some ((Err, xa, xb) # aa # listb) \<Rightarrow> False | Some ((_, b) # lista) \<Rightarrow> False
 2. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal (1 subgoal):
 1. \<And>gf gf' xs ys. \<lbrakk>tr \<in> exec_trace Gamma1 fn1; tr' \<in> exec_trace Gamma2 fn2; Gamma1 fn1 = Some gf; Gamma2 fn2 = Some gf'; the (tr 0) = [init_state fn1 gf xs]; length xs = length (function_inputs gf); restrs_eventually_condition tr rs1; restrs_eventually_condition tr' rs2; the (tr' 0) = [init_state fn2 gf' ys]; length ys = length (function_inputs gf'); (\<exists>xsa. init_state fn1 gf xs = init_state fn1 gf xsa \<and> length xsa = length (function_inputs gf)) \<and> (\<exists>ysa. init_state fn2 gf' ys = init_state fn2 gf' ysa \<and> length ysa = length (function_inputs gf')) \<longrightarrow> trace_refine2 prec (gf, gf') orel tr tr'\<rbrakk> \<Longrightarrow> trace_refine2 prec (gf, gf') orel tr tr' proof (prove)
goal:
No subgoals!