theory ADT_IF

lemma ADT_A_if_Step_irq_masks:
  "\<lbrakk> (s,s') \<in> data_type.Step (ADT_A_if utf) x; invs_if s \<rbrakk>
     \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state (internal_state_if s)" apply (case_tac s, clarsimp) apply (rename_tac uc i_s mode) apply (case_tac mode) apply (simp_all add: system.Step_def steps_def ADT_A_if_def in_monad rah_simp execution_def
                            global_automaton_if_def check_active_irq_A_if_def do_user_op_A_if_def
                            check_active_irq_if_def kernel_schedule_if_def  kernel_call_A_if_def
                            kernel_handle_preemption_if_def kernel_exit_A_if_def measuref_if_def
              | safe | split if_splits)+ apply (erule use_valid[OF _ do_user_op_if_irq_masks_of_state]
                        use_valid[OF _ dmo_getActiveIRQ_irq_masks]
                        use_valid[OF _ kernel_entry_if_irq_masks]
                  | rule refl)+ apply fastforce apply (subgoal_tac "irq_masks_of_state b = irq_masks_of_state i_s",simp) apply (erule use_valid[OF _ kernel_entry_if_irq_masks]) apply fastforce apply (erule use_valid[OF _ handle_preemption_if_irq_masks]) apply fastforce apply (erule use_valid[OF _ schedule_if_irq_masks]) apply fastforce apply (erule use_valid[OF _ kernel_exit_irq_masks]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> Step (ADT_A_if utf) x; invs_if s\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state (internal_state_if s) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>(((a, b), ba), s') \<in> Step (ADT_A_if utf) (); invs_if ((a, b), ba); s = ((a, b), ba)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state b proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s mode. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode)\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s proof (prove)
goal (6 subgoals):
 1. \<And>uc i_s mode. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = InUserMode\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s
 2. \<And>uc i_s mode. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = InIdleMode\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s
 3. \<And>uc i_s mode x3. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = KernelEntry x3\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s
 4. \<And>uc i_s mode. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = KernelPreempted\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s
 5. \<And>uc i_s mode x5. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = KernelSchedule x5\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s
 6. \<And>uc i_s mode. \<lbrakk>(((uc, i_s), mode), s') \<in> Step (ADT_A_if utf) (); invs_if ((uc, i_s), mode); s = ((uc, i_s), mode); mode = KernelExit\<rbrakk> \<Longrightarrow> irq_masks_of_state (internal_state_if s') = irq_masks_of_state i_s proof (prove)
goal (10 subgoals):
 1. \<And>uc i_s b a ba e. \<lbrakk>invs_if ((uc, i_s), InUserMode); s = ((uc, i_s), InUserMode); step_restrict ((a, ba), KernelEntry e); s' = ((a, ba), KernelEntry e); (None, b) \<in> fst (do_machine_op (getActiveIRQ False) i_s); ((Some e, a), ba) \<in> fst (do_user_op_if utf uc b); e \<noteq> Interrupt\<rbrakk> \<Longrightarrow> irq_masks_of_state ba = irq_masks_of_state i_s
 2. \<And>uc i_s b a ba. \<lbrakk>invs_if ((uc, i_s), InUserMode); s = ((uc, i_s), InUserMode); step_restrict ((a, ba), InUserMode); s' = ((a, ba), InUserMode); (None, b) \<in> fst (do_machine_op (getActiveIRQ False) i_s); ((None, a), ba) \<in> fst (do_user_op_if utf uc b)\<rbrakk> \<Longrightarrow> irq_masks_of_state ba = irq_masks_of_state i_s
 3. \<And>uc i_s b i. \<lbrakk>invs_if ((uc, i_s), InUserMode); s = ((uc, i_s), InUserMode); step_restrict ((uc, b), KernelEntry Interrupt); s' = ((uc, b), KernelEntry Interrupt); (Some i, b) \<in> fst (do_machine_op (getActiveIRQ False) i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 4. \<And>uc i_s b i. \<lbrakk>invs_if ((uc, i_s), InIdleMode); s = ((uc, i_s), InIdleMode); step_restrict ((uc, b), KernelEntry Interrupt); s' = ((uc, b), KernelEntry Interrupt); (Some i, b) \<in> fst (do_machine_op (getActiveIRQ False) i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 5. \<And>uc i_s b. \<lbrakk>invs_if ((uc, i_s), InIdleMode); s = ((uc, i_s), InIdleMode); step_restrict ((uc, b), InIdleMode); (None, b) \<in> fst (do_machine_op (getActiveIRQ False) i_s); s' = ((uc, b), InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 6. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelPreempted); s' = ((a, b), KernelPreempted); x3 \<noteq> Interrupt; ((Inl (), a), b) \<in> fst (kernel_entry_if x3 uc i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 7. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelSchedule (x3 = Interrupt)); s' = ((a, b), KernelSchedule (x3 = Interrupt)); ((Inr (), a), b) \<in> fst (kernel_entry_if x3 uc i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 8. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 9. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 10. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (5 subgoals):
 1. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelPreempted); s' = ((a, b), KernelPreempted); x3 \<noteq> Interrupt\<rbrakk> \<Longrightarrow> ((\<lambda>s. irq_masks_of_state s = irq_masks_of_state i_s) and domain_sep_inv False (?st136 uc i_s x3 a b) and invs) i_s
 2. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelSchedule (x3 = Interrupt)); s' = ((a, b), KernelSchedule (x3 = Interrupt)); ((Inr (), a), b) \<in> fst (kernel_entry_if x3 uc i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 4. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 5. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (4 subgoals):
 1. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelSchedule (x3 = Interrupt)); s' = ((a, b), KernelSchedule (x3 = Interrupt)); ((Inr (), a), b) \<in> fst (kernel_entry_if x3 uc i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 2. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 4. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (4 subgoals):
 1. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelSchedule (x3 = Interrupt)); s' = ((a, b), KernelSchedule (x3 = Interrupt)); ((Inr (), a), b) \<in> fst (kernel_entry_if x3 uc i_s)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 2. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 4. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (4 subgoals):
 1. \<And>uc i_s x3 a b. \<lbrakk>invs_if ((uc, i_s), KernelEntry x3); s = ((uc, i_s), KernelEntry x3); step_restrict ((a, b), KernelSchedule (x3 = Interrupt)); s' = ((a, b), KernelSchedule (x3 = Interrupt))\<rbrakk> \<Longrightarrow> ((\<lambda>s. irq_masks_of_state s = irq_masks_of_state i_s) and domain_sep_inv False (?st150 uc i_s x3 a b) and invs) i_s
 2. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 4. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (3 subgoals):
 1. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); (a, b) \<in> fst (handle_preemption_if uc i_s); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 2. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (3 subgoals):
 1. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelPreempted); s = ((uc, i_s), KernelPreempted); step_restrict ((a, b), KernelSchedule True); s' = ((a, b), KernelSchedule True)\<rbrakk> \<Longrightarrow> ((\<lambda>s. irq_masks_of_state s = irq_masks_of_state i_s) and domain_sep_inv False (?st163 uc i_s a b)) i_s
 2. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 3. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (2 subgoals):
 1. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); (a, b) \<in> fst (schedule_if uc i_s); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s
 2. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (2 subgoals):
 1. \<And>uc i_s x5 a b. \<lbrakk>invs_if ((uc, i_s), KernelSchedule x5); s = ((uc, i_s), KernelSchedule x5); step_restrict ((a, b), KernelExit); s' = ((a, b), KernelExit)\<rbrakk> \<Longrightarrow> ((\<lambda>s. irq_masks_of_state s = irq_masks_of_state i_s) and domain_sep_inv False (?st174 uc i_s x5 a b)) i_s
 2. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); (a, b) \<in> fst (kernel_exit_if uc i_s); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state b = irq_masks_of_state i_s proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s a b. \<lbrakk>invs_if ((uc, i_s), KernelExit); s = ((uc, i_s), KernelExit); step_restrict ((a, b), if ct_running b then InUserMode else InIdleMode); s' = ((a, b), if ct_running b then InUserMode else InIdleMode)\<rbrakk> \<Longrightarrow> irq_masks_of_state i_s = irq_masks_of_state i_s proof (prove)
goal:
No subgoals!