kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma kernel_entry_if_domain_fields:
  "\<lbrace>domain_fields P and K (e \<noteq> Interrupt)\<rbrace>
   kernel_entry_if e tc
   \<lbrace>\<lambda>_. domain_fields P\<rbrace>" apply (simp add: kernel_entry_if_def) apply (wp handle_event_domain_fields | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)) and K (e \<noteq> Interrupt)\<rbrace> kernel_entry_if e tc \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (domain_time s) (domain_index s) (domain_list s)) and (\<lambda>y. e \<noteq> Interrupt)\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc)
od \<lbrace>\<lambda>_ s. P (domain_time s) (domain_index s) (domain_list s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma user_context_of_simp[simp]:
  "user_context_of ((uc,s),mode) = uc" by (simp add: user_context_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. user_context_of ((uc, s), mode) = uc
theory ADT_IF

lemma sys_mode_of_simp[simp]:
  "sys_mode_of ((uc,s),mode) = mode" by (simp add: sys_mode_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sys_mode_of ((uc, s), mode) = mode
theory ADT_IF

lemma exit_idle_context:
  "\<lbrace>ct_idle and invs\<rbrace> kernel_exit_if tc' \<lbrace>\<lambda>tc s. tc = idle_context s\<rbrace>" apply (simp add: kernel_exit_if_def thread_get_def) apply wp apply (subgoal_tac "cur_thread s = idle_thread s") apply (clarsimp simp: cur_thread_idle idle_context_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle and invs\<rbrace> kernel_exit_if tc' \<lbrace>\<lambda>tc s. tc = idle_context s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle and invs\<rbrace> do t' <- gets cur_thread;
tcb <- gets_the (get_tcb t');
return (arch_tcb_context_get (tcb_arch tcb))
od \<lbrace>\<lambda>tc s. tc = idle_context s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_idle and invs) s \<Longrightarrow> get_tcb (cur_thread s) s \<noteq> None \<longrightarrow> arch_tcb_context_get (tcb_arch (the (get_tcb (cur_thread s) s))) = idle_context s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>(ct_idle and invs) s; cur_thread s = idle_thread s\<rbrakk> \<Longrightarrow> get_tcb (cur_thread s) s \<noteq> None \<longrightarrow> arch_tcb_context_get (tcb_arch (the (get_tcb (cur_thread s) s))) = idle_context s
 2. \<And>s. (ct_idle and invs) s \<Longrightarrow> cur_thread s = idle_thread s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma check_active_irq_context:
  "\<lbrace>\<top>\<rbrace> check_active_irq_if tc' \<lbrace>\<lambda>tc s. (snd tc) = tc'\<rbrace>" apply (simp add: check_active_irq_if_def) apply (wp del: no_irq| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> check_active_irq_if tc' \<lbrace>\<lambda>tc s. snd tc = tc'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do irq <- do_machine_op (getActiveIRQ False);
return (irq, tc')
od \<lbrace>\<lambda>tc s. snd tc = tc'\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma kernel_entry_context:
  "\<lbrace>\<top>\<rbrace> kernel_entry_if e tc' \<lbrace>\<lambda>tc s. (snd tc) = tc'\<rbrace>" apply (simp add: kernel_entry_if_def) apply (wp del: no_irq| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> kernel_entry_if e tc' \<lbrace>\<lambda>tc s. snd tc = tc'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set tc' (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, tc')
od \<lbrace>\<lambda>tc s. snd tc = tc'\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma handle_preemption_context:
  "\<lbrace>\<top>\<rbrace> handle_preemption_if tc' \<lbrace>\<lambda>tc s. tc = tc'\<rbrace>" apply (simp add: handle_preemption_if_def) apply (wp del: no_irq| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> handle_preemption_if tc' \<lbrace>\<lambda>tc s. tc = tc'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return tc'
od \<lbrace>\<lambda>tc s. tc = tc'\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma get_tcb_machine_stat_update[simp]:
  "get_tcb t (s\<lparr>machine_state := x\<rparr>) = get_tcb t s" by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb t (s\<lparr>machine_state := x\<rparr>) = get_tcb t s
theory ADT_IF

lemma handle_preemption_globals_equiv[wp]:
  "\<lbrace>globals_equiv st and invs\<rbrace>
   handle_preemption_if a
   \<lbrace>\<lambda>_. globals_equiv st\<rbrace>" apply (simp add: handle_preemption_if_def) apply (wp handle_interrupt_globals_equiv dmo_getActiveIRQ_globals_equiv crunch_wps
         | simp add: crunch_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs\<rbrace> handle_preemption_if a \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv st and invs\<rbrace> do irq <- do_machine_op (getActiveIRQ True);
y <- when (\<exists>y. irq = Some y) (handle_interrupt (the irq));
return a
od \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma schedule_if_globals_equiv_scheduler[wp]:
  "\<lbrace>globals_equiv_scheduler st and invs\<rbrace>
   schedule_if tc
   \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>" apply (simp add: schedule_if_def) apply wp apply (wp globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv) apply (simp add: invs_arch_state invs_valid_idle) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and invs\<rbrace> schedule_if tc \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st and invs\<rbrace> do y <- schedule;
y <- activate_thread;
return tc
od \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B1 y\<rbrace> activate_thread \<lbrace>\<lambda>ya. globals_equiv_scheduler st\<rbrace>
 2. \<lbrace>?Q\<rbrace> schedule \<lbrace>?B1\<rbrace>
 3. \<And>s. (globals_equiv_scheduler st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>y st s. (invs and globals_equiv st) s \<Longrightarrow> (globals_equiv st and valid_arch_state and valid_idle) s
 2. \<lbrace>?Q\<rbrace> schedule \<lbrace>\<lambda>y. invs and globals_equiv_scheduler st\<rbrace>
 3. \<And>s. (globals_equiv_scheduler st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> schedule \<lbrace>\<lambda>y. invs and globals_equiv_scheduler st\<rbrace>
 2. \<And>s. (globals_equiv_scheduler st and invs) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma dmo_user_memory_update_idle_equiv:
  "\<lbrace>idle_equiv st\<rbrace> do_machine_op (user_memory_update um) \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" by (wpsimp wp: dmo_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>idle_equiv st\<rbrace> do_machine_op (user_memory_update um) \<lbrace>\<lambda>_. idle_equiv st\<rbrace>
theory ADT_IF

lemma dmo_device_memory_update_idle_equiv:
  "\<lbrace>idle_equiv st\<rbrace> do_machine_op (device_memory_update um) \<lbrace>\<lambda>_. idle_equiv st\<rbrace>" by (wpsimp wp: dmo_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>idle_equiv st\<rbrace> do_machine_op (device_memory_update um) \<lbrace>\<lambda>_. idle_equiv st\<rbrace>
theory ADT_IF

lemma ct_active_not_idle':
  "ct_active s \<Longrightarrow> \<not> ct_idle s" by (clarsimp simp add: ct_in_state_def st_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_active s \<Longrightarrow> \<not> ct_idle s
theory ADT_IF

lemma Init_Fin_serial_weak_strengthen:
  "\<lbrakk> Init_Fin_serial_weak A s0 I; A [> J; J \<subseteq> I; Init A s0 \<subseteq> J \<rbrakk>
     \<Longrightarrow> Init_Fin_serial_weak A s0 J" by (force simp: Init_Fin_serial_weak_def serial_system_weak_def Init_Fin_serial_weak_axioms_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Init_Fin_serial_weak A s0 I; A [> J; J \<subseteq> I; Init A s0 \<subseteq> J\<rbrakk> \<Longrightarrow> Init_Fin_serial_weak A s0 J
theory ADT_IF

lemma rel_terminate_weaken:
  "\<lbrakk> rel_terminate A s0 R I measuref; J \<subseteq> I \<rbrakk>
     \<Longrightarrow> rel_terminate A s0 R J measuref" by (force simp: rel_terminate_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel_terminate A s0 R I measuref; J \<subseteq> I\<rbrakk> \<Longrightarrow> rel_terminate A s0 R J measuref
theory ADT_IF

lemma domains_distinct:
  "pas_domains_distinct initial_aag" apply (rule pas_wellformed_noninterference_domains_distinct) apply (rule policy_wellformed) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_domains_distinct initial_aag proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference initial_aag proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma current_domains_distinct:
  "pas_domains_distinct (current_aag s)" using domains_distinct by (simp add: current_aag_def pas_domains_distinct_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_domains_distinct (current_aag s) proof (prove)
using this:
pas_domains_distinct initial_aag

goal (1 subgoal):
 1. pas_domains_distinct (current_aag s)
theory ADT_IF

lemma current_aag_initial:
  "current_aag s0_internal = initial_aag" by (simp add: current_aag_def the_subject_of_aag_domain cur_domain_subject_s0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. current_aag s0_internal = initial_aag
theory ADT_IF

lemma invs_if_s0[simp]:
  "invs_if s0" apply (clarsimp simp: s0_def invs_if_def Invs_s0_internal[simplified]
                        ct_running_or_ct_idle_s0_internal domain_time_s0_internal
                        det_inv_s0 cur_thread_context_of_def scheduler_action_s0_internal) using domain_time_s0_internal by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if s0 proof (prove)
goal (1 subgoal):
 1. domain_time s0_internal = 0 \<Longrightarrow> False proof (prove)
using this:
0 < domain_time s0_internal

goal (1 subgoal):
 1. domain_time s0_internal = 0 \<Longrightarrow> False
theory ADT_IF

lemma only_timer_irq_inv_irq_state_update[simp]:
  "only_timer_irq_inv timer_irq s0_internal
     (b\<lparr>machine_state := machine_state b\<lparr>irq_state := Suc (irq_state (machine_state b))\<rparr>\<rparr>) =
   only_timer_irq_inv timer_irq s0_internal b" by (clarsimp simp: only_timer_irq_inv_def only_timer_irq_def irq_is_recurring_def is_irq_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. only_timer_irq_inv timer_irq s0_internal (b\<lparr>machine_state := machine_state b\<lparr>irq_state := Suc (irq_state_of_state b)\<rparr>\<rparr>) = only_timer_irq_inv timer_irq s0_internal b
theory ADT_IF

lemma initial_aag_bak:
  "initial_aag =
   (current_aag s)\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal))\<rparr>" using current_aag_def cur_domain_subject_s0 the_subject_of_aag_domain by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. initial_aag = current_aag s\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal))\<rparr> proof (prove)
using this:
current_aag ?t \<equiv> initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain ?t))\<rparr>
pas_cur_domain initial_aag s0_internal
?l \<in> pasDomainAbs initial_aag ?d \<Longrightarrow> the_elem (pasDomainAbs initial_aag ?d) = ?l

goal (1 subgoal):
 1. initial_aag = current_aag s\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal))\<rparr>
theory ADT_IF

lemma the_label_of_domain_exists[intro, simp]:
  "the_elem (pasDomainAbs initial_aag l) \<in> pasDomainAbs initial_aag l" using domains_distinct[simplified pas_domains_distinct_def] the_subject_of_aag_domain by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_elem (pasDomainAbs initial_aag l) \<in> pasDomainAbs initial_aag l proof (prove)
using this:
\<forall>d. \<exists>l. pasDomainAbs initial_aag d = {l}
?l \<in> pasDomainAbs initial_aag ?d \<Longrightarrow> the_elem (pasDomainAbs initial_aag ?d) = ?l

goal (1 subgoal):
 1. the_elem (pasDomainAbs initial_aag l) \<in> pasDomainAbs initial_aag l
theory ADT_IF

lemma pas_cur_domain_current_aag:
  "pas_cur_domain (current_aag s) s" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_cur_domain (current_aag s) s
theory ADT_IF

lemma subject_current_aag:
  "pasSubject (current_aag s) \<in> pasDomainAbs initial_aag (cur_domain s)" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasSubject (current_aag s) \<in> pasDomainAbs initial_aag (cur_domain s)
theory ADT_IF

lemma pas_wellformed_cur[iff]:
  "pas_wellformed_noninterference (current_aag s)" apply (cut_tac policy_wellformed) apply (simp add: pas_wellformed_noninterference_def current_aag_def pas_domains_distinct_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference (current_aag s) proof (prove)
goal (1 subgoal):
 1. pas_wellformed_noninterference initial_aag \<Longrightarrow> pas_wellformed_noninterference (current_aag s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma current_aag_lift:
  assumes b: "\<And>aag. \<lbrace>P aag\<rbrace> f \<lbrace>\<lambda>r s. Q aag r s\<rbrace>"
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (current_aag s) s\<rbrace> f \<lbrace>\<lambda>r s. Q (current_aag s) r s\<rbrace>" apply (simp add: current_aag_def) apply (rule hoare_lift_Pf3[where f="cur_domain", OF b a]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (current_aag s) s\<rbrace> f \<lbrace>\<lambda>r s. Q (current_aag s) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) s\<rbrace> f \<lbrace>\<lambda>r s. Q (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) r s\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma guarded_pas_domain_cur:
  "guarded_pas_domain (current_aag s) s = guarded_pas_domain initial_aag s" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. guarded_pas_domain (current_aag s) s = guarded_pas_domain initial_aag s
theory ADT_IF

lemma pas_refined_cur:
  "pas_refined (current_aag s) s = pas_refined initial_aag s" apply (rule iffI) apply (subst initial_aag_bak[where s=s]) apply (erule pas_refined_pasSubject_update) apply simp apply (simp add: current_aag_def) apply (subst the_subject_of_aag_domain[where l = "pasSubject initial_aag"]) apply (rule cur_domain_subject_s0) apply (blast intro: cur_domain_subject_s0) apply (simp add: current_aag_def) apply (rule pas_refined_pasSubject_update) apply blast+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pas_refined (current_aag s) s = pas_refined initial_aag s proof (prove)
goal (2 subgoals):
 1. pas_refined (current_aag s) s \<Longrightarrow> pas_refined initial_aag s
 2. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (2 subgoals):
 1. pas_refined (current_aag s) s \<Longrightarrow> pas_refined (current_aag s\<lparr>pasSubject := the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal))\<rparr>) s
 2. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (3 subgoals):
 1. pas_wellformed_noninterference (current_aag s)
 2. the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag s) ?d5
 3. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (2 subgoals):
 1. the_elem (pasDomainAbs (current_aag s) (cur_domain s0_internal)) \<in> pasDomainAbs (current_aag s) ?d5
 2. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (2 subgoals):
 1. the_elem (pasDomainAbs initial_aag (cur_domain s0_internal)) \<in> pasDomainAbs initial_aag ?d5
 2. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (3 subgoals):
 1. pas_cur_domain initial_aag s0_internal
 2. pasSubject initial_aag \<in> pasDomainAbs initial_aag ?d5
 3. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (2 subgoals):
 1. pasSubject initial_aag \<in> pasDomainAbs initial_aag ?d5
 2. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (1 subgoal):
 1. pas_refined initial_aag s \<Longrightarrow> pas_refined (current_aag s) s proof (prove)
goal (1 subgoal):
 1. pas_refined initial_aag s \<Longrightarrow> pas_refined (initial_aag\<lparr>pasSubject := the_elem (pasDomainAbs initial_aag (cur_domain s))\<rparr>) s proof (prove)
goal (3 subgoals):
 1. pas_refined initial_aag s \<Longrightarrow> pas_refined initial_aag s
 2. pas_refined initial_aag s \<Longrightarrow> pas_wellformed_noninterference initial_aag
 3. pas_refined initial_aag s \<Longrightarrow> the_elem (pasDomainAbs initial_aag (cur_domain s)) \<in> pasDomainAbs initial_aag ?d18 proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma pasObjectAbs_current_aag:
  "pasObjectAbs (current_aag x) = pasObjectAbs initial_aag" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasObjectAbs (current_aag x) = pasObjectAbs initial_aag
theory ADT_IF

lemma pasIRQAbs_current_aag:
  "pasIRQAbs (current_aag x) = pasIRQAbs initial_aag" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasIRQAbs (current_aag x) = pasIRQAbs initial_aag
theory ADT_IF

lemma pasASIDAbs_current_aag:
  "pasASIDAbs (current_aag x) = pasASIDAbs initial_aag" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasASIDAbs (current_aag x) = pasASIDAbs initial_aag
theory ADT_IF

lemma pasPolicy_current_aag:
  "pasPolicy (current_aag x) = pasPolicy initial_aag" by (simp add: current_aag_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pasPolicy (current_aag x) = pasPolicy initial_aag
theory ADT_IF

lemma guarded_pas_is_subject_current_aag:
  "\<lbrakk> guarded_pas_domain (current_aag s) s; invs s \<rbrakk>
     \<Longrightarrow> ct_active s \<longrightarrow> is_subject (current_aag s) (cur_thread s)" apply (clarsimp simp add: guarded_pas_domain_def current_aag_def) apply (rule sym) apply (blast intro: the_elemI
                dest: domains_distinct[THEN pas_domains_distinct_inj] ct_active_not_idle) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>guarded_pas_domain (current_aag s) s; invs s\<rbrakk> \<Longrightarrow> ct_active s \<longrightarrow> is_subject (current_aag s) (cur_thread s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs initial_aag (cur_thread s) \<in> pasDomainAbs initial_aag (cur_domain s); invs s; ct_active s\<rbrakk> \<Longrightarrow> pasObjectAbs initial_aag (cur_thread s) = the_elem (pasDomainAbs initial_aag (cur_domain s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cur_thread s \<noteq> idle_thread s \<longrightarrow> pasObjectAbs initial_aag (cur_thread s) \<in> pasDomainAbs initial_aag (cur_domain s); invs s; ct_active s\<rbrakk> \<Longrightarrow> the_elem (pasDomainAbs initial_aag (cur_domain s)) = pasObjectAbs initial_aag (cur_thread s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma handle_event_was_not_Interrupt:
  "\<lbrace>\<top>\<rbrace> handle_event e -,\<lbrace>\<lambda> r s. e \<noteq> Interrupt\<rbrace>" apply (case_tac e) apply (simp | wp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1. e = SyscallEvent x1 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace>
 2. \<And>x2. e = UnknownSyscall x2 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace>
 3. \<And>x31 x32. e = UserLevelFault x31 x32 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace>
 4. e = Interrupt \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace>
 5. \<And>x5. e = VMFaultEvent x5 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace>
 6. \<And>x6. e = HypervisorEvent x6 \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> handle_event e -, \<lbrace>\<lambda>r s. e \<noteq> Interrupt\<rbrace> proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma kernel_entry_if_was_not_Interrupt:
  "(x, ba) \<in> fst (kernel_entry_if e a b)
   \<Longrightarrow> (case fst x of Inr a \<Rightarrow> True | _ \<Rightarrow>  e \<noteq> Interrupt)" apply (simp add: kernel_entry_if_def) apply (erule use_valid) apply wp apply simp apply (rule handle_event_was_not_Interrupt[simplified validE_E_def validE_def]) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, ba) \<in> fst (kernel_entry_if e a b) \<Longrightarrow> case fst x of Inl aa \<Rightarrow> e \<noteq> Interrupt | Inr a \<Rightarrow> True proof (prove)
goal (1 subgoal):
 1. (x, ba) \<in> fst ((do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, a)
od) b) \<Longrightarrow> case fst x of Inl aa \<Rightarrow> e \<noteq> Interrupt | Inr a \<Rightarrow> True proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P\<rbrace> do t <- gets cur_thread;
y <- thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch tcb)\<rparr>) t;
r <- handle_event e;
return (r, a)
od \<lbrace>\<lambda>a aa. case fst a of Inl aa \<Rightarrow> e \<noteq> Interrupt | Inr a \<Rightarrow> True\<rbrace>
 2. ?P b proof (prove)
goal (4 subgoals):
 1. \<And>x xa. \<lbrace>?B5 x xa\<rbrace> handle_event e \<lbrace>\<lambda>xb b. case fst (xb, a) of Inl aa \<Rightarrow> e \<noteq> Interrupt | Inr a \<Rightarrow> True\<rbrace>
 2. \<And>x. \<lbrace>?B4 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch tcb)\<rparr>) x \<lbrace>?B5 x\<rbrace>
 3. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?B4\<rbrace>
 4. ?P b proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrace>?B5 x ()\<rbrace> handle_event e \<lbrace>\<lambda>xb a. case xb of Inl aa \<Rightarrow> e \<noteq> Interrupt | Inr a \<Rightarrow> True\<rbrace>
 2. \<And>x. \<lbrace>?B4 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch tcb)\<rparr>) x \<lbrace>?B5 x\<rbrace>
 3. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?B4\<rbrace>
 4. ?P b proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>?B4 x\<rbrace> thread_set (\<lambda>tcb. tcb\<lparr>tcb_arch := arch_tcb_context_set a (tcb_arch tcb)\<rparr>) x \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<lbrace>?P\<rbrace> gets cur_thread \<lbrace>?B4\<rbrace>
 3. ?P b proof (prove)
goal:
No subgoals!