theory ADT_IF

lemma kernel_entry_if_det_inv':
  "\<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s)
                                         and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>rv s. det_inv (case (fst rv) of Inl irq \<Rightarrow> KernelPreempted
                                   | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace>" apply (case_tac "e = Interrupt") apply simp apply (rule hoare_strengthen_post[OF kernel_entry_if_Interrupt_det_inv]) apply (simp split: sum.splits unit.splits) apply simp apply (rule hoare_weaken_pre[OF hoare_strengthen_post[OF kernel_entry_if_det_inv]]) apply (simp split: sum.splits unit.splits) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry Interrupt) tc and (\<lambda>s. ct_running s \<or> ct_idle s)\<rbrace> kernel_entry_if Interrupt tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>e = Interrupt; case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule True) (cur_context s) s\<rbrakk> \<Longrightarrow> det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and ct_running\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>rv s. det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>e \<noteq> Interrupt; case fst rv of Inl irq \<Rightarrow> det_inv KernelPreempted (cur_context s) s | Inr () \<Rightarrow> det_inv (KernelSchedule False) (cur_context s) s\<rbrakk> \<Longrightarrow> det_inv (case fst rv of Inl irq \<Rightarrow> KernelPreempted | Inr () \<Rightarrow> KernelSchedule (e = Interrupt)) (cur_context s) s
 2. \<And>s. \<lbrakk>e \<noteq> Interrupt; (einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and ct_running) s\<rbrakk> \<Longrightarrow> (einvs and det_inv (KernelEntry e) tc and ct_running and K (e \<noteq> Interrupt)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>e \<noteq> Interrupt; (einvs and det_inv (KernelEntry e) tc and (\<lambda>s. ct_running s \<or> ct_idle s) and ct_running) s\<rbrakk> \<Longrightarrow> (einvs and det_inv (KernelEntry e) tc and ct_running and K (e \<noteq> Interrupt)) s proof (prove)
goal:
No subgoals!