theory DetSchedDomainTime_AI

lemma call_kernel_domain_time_inv_det_ext:
  "\<lbrace> (\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) \<rbrace>
   (call_kernel e) :: (unit,det_ext) s_monad
   \<lbrace>\<lambda>_ s. 0 < domain_time s \<rbrace>" unfolding call_kernel_def apply (case_tac "e = Interrupt") apply simp apply (rule hoare_pre) apply ((wp schedule_domain_time_left handle_interrupt_valid_domain_time
           | wpc | simp)+)[1] apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" in hoare_strengthen_post) apply wp apply fastforce+ 
  (* now non-interrupt case; may throw but does not touch domain_time in handle_event *)
   apply (wp schedule_domain_time_left without_preemption_wp handle_interrupt_valid_domain_time) apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" in hoare_post_imp) apply fastforce apply (wp handle_event_domain_time_inv)+ apply (rule_tac Q'="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp_R) apply (wp handle_event_domain_time_inv) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> call_kernel e \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (2 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace> do y <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (3 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>?Q3\<rbrace> do y <- liftE (do_machine_op (getActiveIRQ False) >>= case_option (return ()) handle_interrupt);
y <- schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>
 2. \<And>s. \<lbrakk>e = Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (3 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>?Q3\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>x s. (x = None \<longrightarrow> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) \<and> ((\<exists>xa. x = Some xa) \<longrightarrow> valid_domain_list s \<and> 0 < domain_time s)\<rbrace>
 2. \<And>s. \<lbrakk>e = Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (4 subgoals):
 1. e = Interrupt \<Longrightarrow> \<lbrace>?Q3\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 2. \<And>rv s. \<lbrakk>e = Interrupt; 0 < domain_time s \<and> valid_domain_list s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) \<and> ((\<exists>x. rv = Some x) \<longrightarrow> valid_domain_list s \<and> 0 < domain_time s)
 3. \<And>s. \<lbrakk>e = Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> ?Q3 s
 4. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>e = Interrupt; 0 < domain_time s \<and> valid_domain_list s\<rbrakk> \<Longrightarrow> (rv = None \<longrightarrow> valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)) \<and> ((\<exists>x. rv = Some x) \<longrightarrow> valid_domain_list s \<and> 0 < domain_time s)
 2. \<And>s. \<lbrakk>e = Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list) s\<rbrakk> \<Longrightarrow> 0 < domain_time s \<and> valid_domain_list s
 3. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (1 subgoal):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>(\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)\<rbrace> do handle_event e <handle> (\<lambda>_. without_preemption $ do irq <- do_machine_op $ getActiveIRQ True;
when (irq \<noteq> None) $ handle_interrupt (the irq)
od);
schedule;
activate_thread
od \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'77 x\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. if irq \<noteq> None then \<lambda>s. valid_domain_list s \<and> 0 < domain_time s else (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?Q58\<rbrace> handle_event e \<lbrace>\<lambda>x s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>, \<lbrace>\<lambda>x s. True \<and> True \<and> ?P'77 x s\<rbrace>
 3. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> ?Q58 s proof (prove)
goal (4 subgoals):
 1. \<And>x rv s. \<lbrakk>e \<noteq> Interrupt; 0 < domain_time s \<and> valid_domain_list s\<rbrakk> \<Longrightarrow> (if rv \<noteq> None then \<lambda>s. valid_domain_list s \<and> 0 < domain_time s else (\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread))) s
 2. \<And>x. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'77 x\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 3. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?Q58\<rbrace> handle_event e \<lbrace>\<lambda>x s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>, \<lbrace>\<lambda>x s. True \<and> True \<and> ?P'77 x s\<rbrace>
 4. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> ?Q58 s proof (prove)
goal (3 subgoals):
 1. \<And>x. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'77 x\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s\<rbrace>
 2. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?Q58\<rbrace> handle_event e \<lbrace>\<lambda>x s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread)\<rbrace>, \<lbrace>\<lambda>x s. True \<and> True \<and> ?P'77 x s\<rbrace>
 3. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> ?Q58 s proof (prove)
goal (2 subgoals):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'122\<rbrace> handle_event e \<lbrace>\<lambda>rv s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread\<rbrace>, -
 2. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> (True \<and> e \<noteq> Interrupt) \<and> (True \<and> e \<noteq> Interrupt) \<and> (0 < domain_time s \<and> e \<noteq> Interrupt) \<and> valid_domain_list s \<and> valid_domain_list s \<and> ?P'122 s proof (prove)
goal (3 subgoals):
 1. e \<noteq> Interrupt \<Longrightarrow> \<lbrace>?P'122\<rbrace> handle_event e \<lbrace>\<lambda>_ s. 0 < domain_time s\<rbrace>, -
 2. \<And>rv s. \<lbrakk>e \<noteq> Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread
 3. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> (True \<and> e \<noteq> Interrupt) \<and> (True \<and> e \<noteq> Interrupt) \<and> (0 < domain_time s \<and> e \<noteq> Interrupt) \<and> valid_domain_list s \<and> valid_domain_list s \<and> ?P'122 s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>e \<noteq> Interrupt; 0 < domain_time s\<rbrakk> \<Longrightarrow> domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread
 2. \<And>s. \<lbrakk>e \<noteq> Interrupt; ((\<lambda>s. 0 < domain_time s) and valid_domain_list and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s)) s\<rbrakk> \<Longrightarrow> (True \<and> e \<noteq> Interrupt) \<and> (True \<and> e \<noteq> Interrupt) \<and> (0 < domain_time s \<and> e \<noteq> Interrupt) \<and> valid_domain_list s \<and> valid_domain_list s \<and> 0 < domain_time s \<and> e \<noteq> Interrupt proof (prove)
goal:
No subgoals!