theory GraphProof

lemma stepwise_graph_refine_flip:
  "stepwise_graph_refine Gamma (fns', fns) (nns', nns)
        (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (option_map (\<lambda>x. (snd x, fst x)) otr) N
    = stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N" apply (intro iffI stepwise_graph_refineI) apply (frule_tac i=j and j=i and tr=tr' and tr'=tr in stepwise_graph_refineD) apply simp apply auto[1] apply (frule_tac i=j and j=i and tr=tr' and tr'=tr in stepwise_graph_refineD) apply simp apply auto[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. stepwise_graph_refine Gamma (fns', fns) (nns', nns) (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (map_option (\<lambda>x. (snd x, fst x)) otr) N = stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns', fns) (nns', nns) (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (map_option (\<lambda>x. (snd x, fst x)) otr) N; 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, nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns, 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, fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, fns')))\<rbrakk> \<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'))))
 2. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', fns)))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal (3 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns', fns) (nns', nns) (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (map_option (\<lambda>x. (snd x, fst x)) otr) N; 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, nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns, 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, fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, fns')))\<rbrakk> \<Longrightarrow> N \<le> j \<and> N \<le> i \<and> tr' j \<noteq> None \<and> tr i \<noteq> None \<and> (map fst (the (tr' j)), map fst (the (tr i))) = (nns', nns) \<and> (map (snd \<circ> snd) (the (tr' j)), map (snd \<circ> snd) (the (tr i))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr' j)), map (fst \<circ> snd) (the (tr i))), fst (map (fst \<circ> snd) (the (tr' j)), map (fst \<circ> snd) (the (tr i)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr', tr)) \<and> tr' \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr \<in> exec_trace Gamma (last (snd (fns', fns)))
 2. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns', fns) (nns', nns) (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (map_option (\<lambda>x. (snd x, fst x)) otr) N; 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, nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns, 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, fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, fns'))); (trace_end tr' = None) = (trace_end tr = None) \<and> (trace_end tr' \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr')), hd (the (trace_end tr))), fst (hd (the (trace_end tr')), hd (the (trace_end tr)))))\<rbrakk> \<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'))))
 3. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', fns)))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns', fns) (nns', nns) (\<lambda>x. rel (snd x, fst x)) (\<lambda>x. orel (snd x, fst x)) (map_option (\<lambda>x. (snd x, fst x)) otr) N; 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, nns') \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns, 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, fns'))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns, fns'))); (trace_end tr' = None) = (trace_end tr = None) \<and> (trace_end tr' \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr')), hd (the (trace_end tr))), fst (hd (the (trace_end tr')), hd (the (trace_end tr)))))\<rbrakk> \<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'))))
 2. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', fns)))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', fns)))\<rbrakk> \<Longrightarrow> (trace_end tr = None) = (trace_end tr' = None) \<and> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal (2 subgoals):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', fns)))\<rbrakk> \<Longrightarrow> N \<le> j \<and> N \<le> i \<and> tr' j \<noteq> None \<and> tr i \<noteq> None \<and> (map fst (the (tr' j)), map fst (the (tr i))) = (nns, nns') \<and> (map (snd \<circ> snd) (the (tr' j)), map (snd \<circ> snd) (the (tr i))) = (fns, fns') \<and> rel (map (fst \<circ> snd) (the (tr' j)), map (fst \<circ> snd) (the (tr i))) \<and> (otr \<noteq> None \<longrightarrow> otr = Some (tr', tr)) \<and> tr' \<in> exec_trace Gamma (last (fst (fns, fns'))) \<and> tr \<in> exec_trace Gamma (last (snd (fns, fns')))
 2. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', 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> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal (1 subgoal):
 1. \<And>tr tr' i j. \<lbrakk>stepwise_graph_refine Gamma (fns, fns') (nns, nns') rel orel otr N; 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', nns) \<and> (map (snd \<circ> snd) (the (tr i)), map (snd \<circ> snd) (the (tr' j))) = (fns', fns) \<and> rel (snd (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j))), fst (map (fst \<circ> snd) (the (tr i)), map (fst \<circ> snd) (the (tr' j)))) \<and> (map_option (\<lambda>x. (snd x, fst x)) otr \<noteq> None \<longrightarrow> map_option (\<lambda>x. (snd x, fst x)) otr = Some (tr, tr')) \<and> tr \<in> exec_trace Gamma (last (fst (fns', fns))) \<and> tr' \<in> exec_trace Gamma (last (snd (fns', 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> (trace_end tr \<noteq> None \<longrightarrow> orel (snd (hd (the (trace_end tr)), hd (the (trace_end tr'))), fst (hd (the (trace_end tr)), hd (the (trace_end tr'))))) proof (prove)
goal:
No subgoals!