theory Plus2_Prefix

lemma fold_parallel_pfx_refn_induct:
  "list_all2 (prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>)) xs ys
    \<Longrightarrow> prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>) x y
    \<Longrightarrow> \<forall>x \<in> set (x # xs). par_tr_fin_principle x
    \<Longrightarrow> \<forall>y \<in> set (y # ys). prefix_closed y
    \<Longrightarrow> prefix_refinement sr sr sr (\<lambda>_ _. True) P Q (\<top>\<top>) (\<top>\<top>)
        (fold parallel (rev xs) x) (fold parallel (rev ys) y)" apply (induct rule: list_all2_induct; simp) apply (rule prefix_refinement_parallel_triv[simplified bipred_disj_top_eq]; simp?) apply (clarsimp simp: fold_parallel_par_tr_fin_principle
                         fold_parallel_prefix_closed)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True)) xs ys; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) x y; \<forall>x\<in>set (x # xs). par_tr_fin_principle x; \<forall>y\<in>set (y # ys). prefix_closed y\<rbrakk> \<Longrightarrow> pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) (fold Trace_Monad.parallel (rev xs) x) (fold Trace_Monad.parallel (rev ys) y) proof (prove)
goal (1 subgoal):
 1. \<And>xa xs ya ys. \<lbrakk>list_all2 (pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True)) xs ys; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) xa ya; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) (fold Trace_Monad.parallel (rev xs) x) (fold Trace_Monad.parallel (rev ys) y); pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) x y; par_tr_fin_principle x \<and> par_tr_fin_principle xa \<and> (\<forall>x\<in>set xs. par_tr_fin_principle x); prefix_closed y \<and> prefix_closed ya \<and> (\<forall>x\<in>set ys. prefix_closed x)\<rbrakk> \<Longrightarrow> pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) (Trace_Monad.parallel xa (fold Trace_Monad.parallel (rev xs) x)) (Trace_Monad.parallel ya (fold Trace_Monad.parallel (rev ys) y)) proof (prove)
goal (2 subgoals):
 1. \<And>xa xs ya ys. \<lbrakk>list_all2 (pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True)) xs ys; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) xa ya; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) (fold Trace_Monad.parallel (rev xs) x) (fold Trace_Monad.parallel (rev ys) y); pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) x y; par_tr_fin_principle x \<and> par_tr_fin_principle xa \<and> (\<forall>x\<in>set xs. par_tr_fin_principle x); prefix_closed y \<and> prefix_closed ya \<and> (\<forall>x\<in>set ys. prefix_closed x)\<rbrakk> \<Longrightarrow> par_tr_fin_principle (fold Trace_Monad.parallel (rev xs) x)
 2. \<And>xa xs ya ys. \<lbrakk>list_all2 (pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True)) xs ys; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) xa ya; pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) (fold Trace_Monad.parallel (rev xs) x) (fold Trace_Monad.parallel (rev ys) y); pfx_refn sr (\<lambda>_ _. True) P Q (\<lambda>_ _. True) (\<lambda>_ _. True) x y; par_tr_fin_principle x \<and> par_tr_fin_principle xa \<and> (\<forall>x\<in>set xs. par_tr_fin_principle x); prefix_closed y \<and> prefix_closed ya \<and> (\<forall>x\<in>set ys. prefix_closed x)\<rbrakk> \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (rev ys) y) proof (prove)
goal:
No subgoals!