theory Noninterference

lemma interrupt_step:
  assumes interrupt:
    "\<And>r. (r,internal_state_if s')
            \<in> fst (kernel_entry_if Interrupt (user_context_of s) (internal_state_if s))
          \<Longrightarrow> sys_mode_of s = KernelEntry Interrupt \<Longrightarrow> (sys_mode_of s' = KernelSchedule True)
          \<Longrightarrow> snd r = user_context_of s \<Longrightarrow> snd r = user_context_of s'
          \<Longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s)
          \<Longrightarrow> P"
  assumes preemption:
    "\<And>r. (r,internal_state_if s')
            \<in> fst (handle_preemption_if (user_context_of s) (internal_state_if s))
          \<Longrightarrow> sys_mode_of s = KernelPreempted \<Longrightarrow> sys_mode_of s' = KernelSchedule True
          \<Longrightarrow> r = user_context_of s \<Longrightarrow> r = user_context_of s'
          \<Longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s)
          \<Longrightarrow> P"
  shows "\<lbrakk> interrupted_modes (sys_mode_of s); (s,s') \<in> data_type.Step (ADT_A_if utf) () \<rbrakk> \<Longrightarrow> P" apply (insert interrupt preemption) apply atomize apply (case_tac s, clarsimp) apply (rename_tac uc i_s mode) apply (case_tac mode ; clarsimp) subgoal for uc i_s apply (clarsimp simp: system.Step_def execution_def steps_def ADT_A_if_def
                            global_automaton_if_def kernel_call_A_if_def
                            kernel_handle_preemption_if_def del: notI) apply (frule use_valid[OF _ kernel_entry_context] ; clarsimp) apply (frule_tac P1="\<lambda>x. x = cur_domain i_s" in use_valid[OF _ kernel_entry_if_cur_domain]) apply auto done subgoal for uc i_s apply (clarsimp simp: system.Step_def execution_def steps_def ADT_A_if_def
                           global_automaton_if_def kernel_call_A_if_def
                           kernel_handle_preemption_if_def del: notI) apply (frule use_valid[OF _ handle_preemption_context] ; clarsimp) apply (frule_tac P1="\<lambda>x. x = cur_domain i_s" in use_valid[OF _ handle_preemption_if_cur_domain]) apply auto done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>interrupted_modes (sys_mode_of s); (s, s') \<in> data_type.Step (ADT_A_if utf) ()\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>interrupted_modes (sys_mode_of s); (s, s') \<in> data_type.Step (ADT_A_if utf) (); \<And>r. \<lbrakk>(r, internal_state_if s') \<in> fst (kernel_entry_if Interrupt (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelEntry Interrupt; sys_mode_of s' = KernelSchedule True; snd r = user_context_of s; snd r = user_context_of s'; cur_domain (internal_state_if s') = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> P; \<And>r. \<lbrakk>(r, internal_state_if s') \<in> fst (handle_preemption_if (user_context_of s) (internal_state_if s)); sys_mode_of s = KernelPreempted; sys_mode_of s' = KernelSchedule True; r = user_context_of s; r = user_context_of s'; cur_domain (internal_state_if s') = cur_domain (internal_state_if s)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>interrupted_modes (sys_mode_of s); (s, s') \<in> data_type.Step (ADT_A_if utf) (); \<forall>r. (r, internal_state_if s') \<in> fst (kernel_entry_if Interrupt (user_context_of s) (internal_state_if s)) \<longrightarrow> sys_mode_of s = KernelEntry Interrupt \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> snd r = user_context_of s \<longrightarrow> snd r = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s) \<longrightarrow> P; \<forall>r. (r, internal_state_if s') \<in> fst (handle_preemption_if (user_context_of s) (internal_state_if s)) \<longrightarrow> sys_mode_of s = KernelPreempted \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> r = user_context_of s \<longrightarrow> r = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain (internal_state_if s) \<longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>interrupted_modes ba; (((a, b), ba), s') \<in> data_type.Step (ADT_A_if utf) (); (\<exists>aa. ((aa, a), internal_state_if s') \<in> fst (kernel_entry_if Interrupt a b)) \<longrightarrow> ba = KernelEntry Interrupt \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> a = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain b \<longrightarrow> P; (a, internal_state_if s') \<in> fst (handle_preemption_if a b) \<longrightarrow> ba = KernelPreempted \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> a = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain b \<longrightarrow> P; s = ((a, b), ba)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s mode. \<lbrakk>interrupted_modes mode; (((uc, i_s), mode), s') \<in> data_type.Step (ADT_A_if utf) (); (\<exists>a. ((a, uc), internal_state_if s') \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> mode = KernelEntry Interrupt \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; (uc, internal_state_if s') \<in> fst (handle_preemption_if uc i_s) \<longrightarrow> mode = KernelPreempted \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), mode)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>uc i_s. \<lbrakk>(((uc, i_s), KernelEntry Interrupt), s') \<in> data_type.Step (ADT_A_if utf) (); (\<exists>a. ((a, uc), internal_state_if s') \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt)\<rbrakk> \<Longrightarrow> P
 2. \<And>uc i_s. \<lbrakk>(((uc, i_s), KernelPreempted), s') \<in> data_type.Step (ADT_A_if utf) (); (uc, internal_state_if s') \<in> fst (handle_preemption_if uc i_s) \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelPreempted)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(((uc, i_s), KernelEntry Interrupt), s') \<in> data_type.Step (ADT_A_if utf) (); (\<exists>a. ((a, uc), internal_state_if s') \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(\<exists>a. ((a, uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> uc = a \<longrightarrow> cur_domain b = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt); step_restrict ((a, b), KernelSchedule True); s' = ((a, b), KernelSchedule True); ((Inr (), a), b) \<in> fst (kernel_entry_if Interrupt uc i_s)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(\<exists>a. ((a, uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> cur_domain b = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt); step_restrict ((uc, b), KernelSchedule True); s' = ((uc, b), KernelSchedule True); ((Inr (), uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>(\<exists>a. ((a, uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> cur_domain b = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt); step_restrict ((uc, b), KernelSchedule True); s' = ((uc, b), KernelSchedule True); ((Inr (), uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)\<rbrakk> \<Longrightarrow> cur_domain i_s = cur_domain i_s
 2. \<And>b. \<lbrakk>(\<exists>a. ((a, uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s)) \<longrightarrow> cur_domain b = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelEntry Interrupt); step_restrict ((uc, b), KernelSchedule True); s' = ((uc, b), KernelSchedule True); ((Inr (), uc), b) \<in> fst (kernel_entry_if Interrupt uc i_s); cur_domain b = cur_domain i_s\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<And>uc i_s. \<lbrakk>(((uc, i_s), KernelPreempted), s') \<in> data_type.Step (ADT_A_if utf) (); (uc, internal_state_if s') \<in> fst (handle_preemption_if uc i_s) \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelPreempted)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(((uc, i_s), KernelPreempted), s') \<in> data_type.Step (ADT_A_if utf) (); (uc, internal_state_if s') \<in> fst (handle_preemption_if uc i_s) \<longrightarrow> sys_mode_of s' = KernelSchedule True \<longrightarrow> uc = user_context_of s' \<longrightarrow> cur_domain (internal_state_if s') = cur_domain i_s \<longrightarrow> P; s = ((uc, i_s), KernelPreempted)\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(uc, b) \<in> fst (handle_preemption_if uc i_s) \<longrightarrow> uc = a \<longrightarrow> cur_domain b = cur_domain i_s \<longrightarrow> P; 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> P proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>s = ((uc, i_s), KernelPreempted); step_restrict ((uc, b), KernelSchedule True); (uc, b) \<in> fst (handle_preemption_if uc i_s); s' = ((uc, b), KernelSchedule True); cur_domain b \<noteq> cur_domain i_s\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<And>b. \<lbrakk>s = ((uc, i_s), KernelPreempted); step_restrict ((uc, b), KernelSchedule True); (uc, b) \<in> fst (handle_preemption_if uc i_s); s' = ((uc, b), KernelSchedule True); cur_domain b \<noteq> cur_domain i_s\<rbrakk> \<Longrightarrow> cur_domain i_s = cur_domain i_s
 2. \<And>b. \<lbrakk>s = ((uc, i_s), KernelPreempted); step_restrict ((uc, b), KernelSchedule True); (uc, b) \<in> fst (handle_preemption_if uc i_s); s' = ((uc, b), KernelSchedule True); cur_domain b \<noteq> cur_domain i_s; cur_domain b = cur_domain i_s\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!