theory GraphProof

lemma stepwise_graph_refine_induct:
  assumes Suc: "\<And>n otr. stepwise_graph_refine Gamma fns nns rel orel otr (Suc n)
        \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr n"
  shows "stepwise_graph_refine Gamma fns nns rel orel otr n" proof - have induct: "\<And>n m otr. n \<ge> m
        \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr n
        \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr m" by (erule(1) inc_induct, erule Suc) show ?thesis apply (rule stepwise_graph_refineI) apply (simp add: prod_eq_iff) apply (case_tac "\<exists>N. (\<forall>i \<ge> N. tr i = None) \<or> (\<forall>i \<ge> N. tr' i = None)") apply clarsimp apply (cut_tac n="Suc N" and m="n" and otr="Some (tr, tr')" in induct) apply (rule ccontr, auto)[1] apply (auto simp add: stepwise_graph_refine_def)[1] apply (drule_tac tr=tr and tr'=tr' in stepwise_graph_refineD, (erule conjI)+) apply simp apply simp apply (case_tac "trace_end tr") apply (rule ccontr, clarsimp) apply (frule(1) exec_trace_end_SomeD, clarsimp) apply (frule(1) exec_trace_None_dom_subset) apply (drule_tac x="Suc na" in spec) apply auto[1] apply clarsimp apply (frule(1) exec_trace_end_SomeD, clarsimp) apply (frule(1) exec_trace_None_dom_subset) apply (drule_tac x="Suc na" in spec) apply auto[1] done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. stepwise_graph_refine Gamma fns nns rel orel otr n proof (state)
goal (1 subgoal):
 1. stepwise_graph_refine Gamma fns nns rel orel otr n proof (prove)
goal (1 subgoal):
 1. \<And>n m otr. \<lbrakk>m \<le> n; stepwise_graph_refine Gamma fns nns rel orel otr n\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel otr m proof (state)
this:
\<lbrakk>?m \<le> ?n; stepwise_graph_refine Gamma fns nns rel orel ?otr ?n\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel ?otr ?m

goal (1 subgoal):
 1. stepwise_graph_refine Gamma fns nns rel orel otr n proof (prove)
goal (1 subgoal):
 1. stepwise_graph_refine Gamma fns nns rel orel otr n proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. n \<le> i \<and> n \<le> j \<and> tr i \<noteq> None \<and> tr' j \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' j))) = nns \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)) \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)) \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<exists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 2. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 2. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (4 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> n \<le> Suc N
 2. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel (Some (tr, tr')) (Suc N)
 3. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); stepwise_graph_refine Gamma fns nns rel orel (Some (tr, tr')) n\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 4. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> stepwise_graph_refine Gamma fns nns rel orel (Some (tr, tr')) (Suc N)
 2. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); stepwise_graph_refine Gamma fns nns rel orel (Some (tr, tr')) n\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 3. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); stepwise_graph_refine Gamma fns nns rel orel (Some (tr, tr')) n\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 2. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> tr i \<noteq> None \<and> tr' j \<noteq> None \<and> (map fst (the (tr i)), map fst (the (tr' j))) = nns \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> (Some (tr, tr') \<noteq> None \<longrightarrow> Some (tr, tr') = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns))
 2. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 3. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j N y ya. \<lbrakk>(\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 2. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None)\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = None\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr'))))
 2. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j y ya yb. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = None; trace_end tr' = Some y; n \<le> i; n \<le> j; tr i = Some ya; tr' j = Some yb; map fst ya = fst nns; map fst yb = snd nns; map (snd \<circ> snd) ya = fst fns; map (snd \<circ> snd) yb = snd fns; rel (map (fst \<circ> snd) ya, map (fst \<circ> snd) yb); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> False
 2. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j ya yb na nn st g. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = None; trace_end tr' = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some ya; tr' j = Some yb; map fst ya = fst nns; map fst yb = snd nns; map (snd \<circ> snd) ya = fst fns; map (snd \<circ> snd) yb = snd fns; rel (map (fst \<circ> snd) ya, map (fst \<circ> snd) yb); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr' na = Some [(nn, st, g)]; tr' (Suc na) = None; nn = Ret \<or> nn = Err\<rbrakk> \<Longrightarrow> False
 2. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j ya yb na nn st g. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = None; trace_end tr' = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some ya; tr' j = Some yb; map fst ya = fst nns; map fst yb = snd nns; map (snd \<circ> snd) ya = fst fns; map (snd \<circ> snd) yb = snd fns; rel (map (fst \<circ> snd) ya, map (fst \<circ> snd) yb); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr' na = Some [(nn, st, g)]; tr' (Suc na) = None; nn = Ret \<or> nn = Err; dom tr' \<subseteq> {..<Suc na}\<rbrakk> \<Longrightarrow> False
 2. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j ya yb na nn st g. \<lbrakk>trace_end tr = None; trace_end tr' = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some ya; tr' j = Some yb; map fst ya = fst nns; map fst yb = snd nns; map (snd \<circ> snd) ya = fst fns; map (snd \<circ> snd) yb = snd fns; rel (map (fst \<circ> snd) ya, map (fst \<circ> snd) yb); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr' na = Some [(nn, st, g)]; tr' (Suc na) = None; nn = Ret \<or> nn = Err; dom tr' \<subseteq> {..<Suc na}; (\<exists>i\<ge>Suc na. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>Suc na. \<exists>y. tr' i = Some y)\<rbrakk> \<Longrightarrow> False
 2. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j a. \<lbrakk>n \<le> i \<and> n \<le> j \<and> (\<exists>y. tr i = Some y) \<and> (\<exists>y. tr' j = Some y) \<and> map fst (the (tr i)) = fst nns \<and> map fst (the (tr' j)) = snd nns \<and> map (snd \<circ> snd) (the (tr i)) = fst fns \<and> map (snd \<circ> snd) (the (tr' j)) = snd fns \<and> rel (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))) \<and> ((\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst fns)) \<and> tr' \<in> exec_trace Gamma (last (snd fns)); \<nexists>N. (\<forall>i\<ge>N. tr i = None) \<or> (\<forall>i\<ge>N. tr' i = None); trace_end tr = Some a\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> ((\<exists>y. trace_end tr = Some y) \<longrightarrow> orel (hd (the (trace_end tr)), hd (the (trace_end tr')))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j a y ya. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = Some a; n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns))\<rbrakk> \<Longrightarrow> (\<exists>y. trace_end tr' = Some y) \<and> orel (hd a, hd (the (trace_end tr'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y ya na nn st g. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr na = Some [(nn, st, g)]; tr (Suc na) = None; nn = Ret \<or> nn = Err\<rbrakk> \<Longrightarrow> (\<exists>y. trace_end tr' = Some y) \<and> orel ((nn, st, g), hd (the (trace_end tr'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y ya na nn st g. \<lbrakk>\<forall>N. (\<exists>i\<ge>N. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>N. \<exists>y. tr' i = Some y); trace_end tr = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr na = Some [(nn, st, g)]; tr (Suc na) = None; nn = Ret \<or> nn = Err; dom tr \<subseteq> {..<Suc na}\<rbrakk> \<Longrightarrow> (\<exists>y. trace_end tr' = Some y) \<and> orel ((nn, st, g), hd (the (trace_end tr'))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j y ya na nn st g. \<lbrakk>trace_end tr = Some [(nn, st, g)]; n \<le> i; n \<le> j; tr i = Some y; tr' j = Some ya; map fst y = fst nns; map fst ya = snd nns; map (snd \<circ> snd) y = fst fns; map (snd \<circ> snd) ya = snd fns; rel (map (fst \<circ> snd) y, map (fst \<circ> snd) ya); (\<exists>a b. otr = Some (a, b)) \<longrightarrow> otr = Some (tr, tr'); tr \<in> exec_trace Gamma (last (fst fns)); tr' \<in> exec_trace Gamma (last (snd fns)); tr na = Some [(nn, st, g)]; tr (Suc na) = None; nn = Ret \<or> nn = Err; dom tr \<subseteq> {..<Suc na}; (\<exists>i\<ge>Suc na. \<exists>y. tr i = Some y) \<and> (\<exists>i\<ge>Suc na. \<exists>y. tr' i = Some y)\<rbrakk> \<Longrightarrow> (\<exists>y. trace_end tr' = Some y) \<and> orel ((nn, st, g), hd (the (trace_end tr'))) proof (prove)
goal:
No subgoals! proof (state)
this:
stepwise_graph_refine Gamma fns nns rel orel otr n

goal:
No subgoals!