theory Syscall_S

lemma syscall_bisim:
  assumes bs:
    "bisim (fr \<oplus> r_flt_rel) P P' m_flt m_flt'"
    "\<And>flt flt'. fr flt flt' \<Longrightarrow>
        bisim r (P_flt flt) (P'_flt flt') (h_flt flt) (h_flt' flt')"
    "\<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow>
        bisim (ser \<oplus> r_err_rel rv rv')
               (P_no_flt rv) (P'_no_flt rv')
               (m_err rv) (m_err' rv')"
    "\<And>rv rv' err err'. \<lbrakk>r_flt_rel rv rv'; ser err err'\<rbrakk>
     \<Longrightarrow> bisim r (P_err rv err)
            (P'_err rv' err') (h_err err) (h_err' err')"
    "\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
     \<Longrightarrow> bisim (f \<oplus> r)
           (P_no_err rvf rve) (P'_no_err rvf' rve')
           (m_fin rve) (m_fin' rve')"
  assumes wp:  "\<And>rv.  \<lbrace>Q_no_flt rv\<rbrace>   m_err rv   \<lbrace>P_no_err rv\<rbrace>,  \<lbrace>P_err rv\<rbrace>"
               "\<And>rv'. \<lbrace>Q'_no_flt rv'\<rbrace> m_err' rv' \<lbrace>P'_no_err rv'\<rbrace>,\<lbrace>P'_err rv'\<rbrace>"
               "\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
               "\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"

  shows "bisim (f \<oplus> r) (P and Q) (P' and Q')
           (syscall m_flt  h_flt m_err h_err m_fin)
           (syscall m_flt' h_flt' m_err' h_err' m_fin')" apply (simp add: syscall_def liftE_bindE) apply (rule bisim_split_bind_case_sum) apply (rule bs) apply simp apply (rule bs) apply simp apply (simp add: liftE_bindE) apply (rule bisim_split_bind_case_sum) apply (erule bs) apply simp apply (erule bs) apply simp apply (erule(1) bs) apply (rule wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> r) (P and Q) (P' and Q') (syscall m_flt h_flt m_err h_err m_fin) (syscall m_flt' h_flt' m_err' h_err' m_fin') proof (prove)
goal (1 subgoal):
 1. bisim (f \<oplus> r) (P and Q) (P' and Q') (m_flt >>= case_sum (\<lambda>f. without_preemption $ h_flt f) (\<lambda>a. (without_preemption $ m_err a) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin)) (m_flt' >>= case_sum (\<lambda>f. without_preemption $ h_flt' f) (\<lambda>a. (without_preemption $ m_err' a) >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')) proof (prove)
goal (5 subgoals):
 1. bisim (?lr \<oplus> ?rr) P P' m_flt m_flt'
 2. \<And>rv rv'. ?lr rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?R rv) (?R' rv') (without_preemption $ h_flt rv) (without_preemption $ h_flt' rv')
 3. \<And>rv rv'. ?rr rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((without_preemption $ m_err' rv') >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')
 4. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>?R\<rbrace>
 5. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>?R'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. fr rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?R rv) (?R' rv') (without_preemption $ h_flt rv) (without_preemption $ h_flt' rv')
 2. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((without_preemption $ m_err' rv') >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')
 3. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>?R\<rbrace>
 4. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>?R'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. fr rv rv' \<Longrightarrow> bisim r (?R rv) (?R' rv') (h_flt rv) (h_flt' rv')
 2. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((without_preemption $ m_err' rv') >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')
 3. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>?R\<rbrace>
 4. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>?R'\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. fr rv rv' \<Longrightarrow> fr rv rv'
 2. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((without_preemption $ m_err' rv') >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')
 3. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>P_flt\<rbrace>
 4. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') ((without_preemption $ m_err rv) >>=E case_sum (\<lambda>e. without_preemption $ h_err e) m_fin) ((without_preemption $ m_err' rv') >>=E case_sum (\<lambda>e. without_preemption $ h_err' e) m_fin')
 2. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>P_flt\<rbrace>
 3. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (f \<oplus> r) (?S rv) (?S' rv') (m_err rv >>= case_sum (\<lambda>e. liftE (h_err e)) m_fin) (m_err' rv' >>= case_sum (\<lambda>e. liftE (h_err' e)) m_fin')
 2. \<lbrace>Q\<rbrace> m_flt \<lbrace>?S\<rbrace>, \<lbrace>P_flt\<rbrace>
 3. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>?S'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> bisim (?lr10 rv rv' \<oplus> ?rr10 rv rv') (?P11 rv) (?P'13 rv') (m_err rv) (m_err' rv')
 2. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; ?lr10 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?R10 rv rv' rva) (?R'10 rv rv' rv'a) (liftE (h_err rva)) (liftE (h_err' rv'a))
 3. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; ?rr10 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?S10 rv rv' rva) (?S'10 rv rv' rv'a) (m_fin rva) (m_fin' rv'a)
 4. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>?S10 rv rv'\<rbrace>, \<lbrace>?R10 rv rv'\<rbrace>
 5. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>?S'10 rv rv'\<rbrace>, \<lbrace>?R'10 rv rv'\<rbrace>
 6. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. ?P11 rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 7. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. ?P'13 rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; ser rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?R10 rv rv' rva) (?R'10 rv rv' rv'a) (liftE (h_err rva)) (liftE (h_err' rv'a))
 2. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; r_err_rel rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?S10 rv rv' rva) (?S'10 rv rv' rv'a) (m_fin rva) (m_fin' rv'a)
 3. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>?S10 rv rv'\<rbrace>, \<lbrace>?R10 rv rv'\<rbrace>
 4. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>?S'10 rv rv'\<rbrace>, \<lbrace>?R'10 rv rv'\<rbrace>
 5. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 6. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. P'_no_flt rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; ser rva rv'a\<rbrakk> \<Longrightarrow> bisim r (?R10 rv rv' rva) (?R'10 rv rv' rv'a) (h_err rva) (h_err' rv'a)
 2. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; r_err_rel rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?S10 rv rv' rva) (?S'10 rv rv' rv'a) (m_fin rva) (m_fin' rv'a)
 3. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>?S10 rv rv'\<rbrace>, \<lbrace>?R10 rv rv'\<rbrace>
 4. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>?S'10 rv rv'\<rbrace>, \<lbrace>?R'10 rv rv'\<rbrace>
 5. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 6. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. P'_no_flt rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' rva rv'a. ser rva rv'a \<Longrightarrow> ser rva rv'a
 2. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; r_err_rel rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?S10 rv rv' rva) (?S'10 rv rv' rv'a) (m_fin rva) (m_fin' rv'a)
 3. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>?S10 rv rv'\<rbrace>, \<lbrace>P_err rv\<rbrace>
 4. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>?S'10 rv rv'\<rbrace>, \<lbrace>P'_err rv'\<rbrace>
 5. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 6. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. P'_no_flt rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' rva rv'a. \<lbrakk>r_flt_rel rv rv'; r_err_rel rv rv' rva rv'a\<rbrakk> \<Longrightarrow> bisim (f \<oplus> r) (?S10 rv rv' rva) (?S'10 rv rv' rv'a) (m_fin rva) (m_fin' rv'a)
 2. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>?S10 rv rv'\<rbrace>, \<lbrace>P_err rv\<rbrace>
 3. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>?S'10 rv rv'\<rbrace>, \<lbrace>P'_err rv'\<rbrace>
 4. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 5. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. P'_no_flt rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q12 rv\<rbrace> m_err rv \<lbrace>P_no_err rv\<rbrace>, \<lbrace>P_err rv\<rbrace>
 2. \<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> \<lbrace>?Q'14 rv'\<rbrace> m_err' rv' \<lbrace>P'_no_err rv'\<rbrace>, \<lbrace>P'_err rv'\<rbrace>
 3. \<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and ?Q12 rv\<rbrace>, \<lbrace>P_flt\<rbrace>
 4. \<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv'. P'_no_flt rv' and ?Q'14 rv'\<rbrace>, \<lbrace>P'_flt\<rbrace> proof (prove)
goal:
No subgoals!