kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF

lemma ct_idle_lift:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>"
  assumes d: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>"
  assumes b: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>_. invs\<rbrace>"
  assumes c: "\<And>s. Q s \<Longrightarrow> invs s"
  shows "\<lbrace>Q and (\<lambda>s. P (ct_idle s))\<rbrace> f \<lbrace>\<lambda>r s. P (ct_idle s)\<rbrace>" apply (rule hoare_add_post[OF b],simp) apply (clarsimp simp: valid_def) apply (drule c) apply (clarsimp simp: cur_thread_idle) apply (rule use_valid[OF _ a],assumption) apply (erule use_valid[OF _ d],simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q and (\<lambda>s. P (ct_idle s))\<rbrace> f \<lbrace>\<lambda>r s. P (ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q and (\<lambda>s. P (ct_idle s))\<rbrace> f \<lbrace>\<lambda>rv s. invs s \<longrightarrow> P (ct_idle s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); Q s; P (ct_idle s); invs b\<rbrakk> \<Longrightarrow> P (ct_idle b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (ct_idle s); invs b; invs s\<rbrakk> \<Longrightarrow> P (ct_idle b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (cur_thread s = idle_thread s); invs b; invs s\<rbrakk> \<Longrightarrow> P (cur_thread b = idle_thread b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); P (cur_thread s = idle_thread s); invs b; invs s\<rbrakk> \<Longrightarrow> P (cur_thread s = idle_thread b) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma idle_equiv_context_equiv:
  "\<lbrakk> idle_equiv s s'; invs s' \<rbrakk> \<Longrightarrow> idle_context s' = idle_context s" apply (clarsimp simp: idle_equiv_def idle_context_def invs_def valid_state_def valid_idle_def) apply (drule pred_tcb_at_tcb_at) apply (clarsimp simp: tcb_at_def2 get_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_equiv s s'; invs s'\<rbrakk> \<Longrightarrow> idle_context s' = idle_context s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_thread s = idle_thread_ptr; valid_pspace s'; \<forall>tcb. kheap s idle_thread_ptr = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap s' idle_thread_ptr = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at idle_thread_ptr s = tcb_at idle_thread_ptr s'; valid_mdb s'; valid_ioc s'; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s'; idle_thread s' = idle_thread_ptr; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_ioports s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch (the (get_tcb idle_thread_ptr s'))) = arch_tcb_context_get (tcb_arch (the (get_tcb idle_thread_ptr s))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_thread s = idle_thread_ptr; valid_pspace s'; \<forall>tcb. kheap s idle_thread_ptr = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap s' idle_thread_ptr = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at idle_thread_ptr s = tcb_at idle_thread_ptr s'; valid_mdb s'; valid_ioc s'; idle_thread s' = idle_thread_ptr; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_ioports s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; cur_tcb s'; tcb_at idle_thread_ptr s'\<rbrakk> \<Longrightarrow> arch_tcb_context_get (tcb_arch (the (get_tcb idle_thread_ptr s'))) = arch_tcb_context_get (tcb_arch (the (get_tcb idle_thread_ptr s))) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma pasMaySendIrqs_current_aag[simp]:
  "pasMaySendIrqs (current_aag s) = False" by (simp add: current_aag_def)

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

lemma Fin_ADT_if:
  "Fin (ADT_A_if utf) = id" by (simp add: ADT_A_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Fin (ADT_A_if utf) = id
theory ADT_IF

lemma Init_ADT_if:
  "Init (ADT_A_if utf) = (\<lambda>s. {s} \<inter> full_invs_if \<inter> {s. step_restrict s})" by (simp add: ADT_A_if_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init (ADT_A_if utf) = (\<lambda>s. {s} \<inter> full_invs_if \<inter> {s. step_restrict s})
theory ADT_IF

lemma handle_preemption_if_valid_sched[wp]:
  "\<lbrace>valid_sched and invs\<rbrace>
   handle_preemption_if irq
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (wpsimp simp: handle_preemption_if_def cong: if_cong) apply (rule_tac Q="\<lambda>rv. valid_sched and invs and K (rv \<notin> Some ` non_kernel_IRQs)"
                in hoare_strengthen_post[rotated]) apply clarsimp apply (wpsimp wp: getActiveIRQ_neq_non_kernel)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched and invs\<rbrace> handle_preemption_if irq \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>irq. if \<exists>y. irq = Some y then valid_sched and invs and (\<lambda>s. the irq \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s) else valid_sched\<rbrace>
 2. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (valid_sched and invs and K (rv \<notin> Some ` non_kernel_IRQs)) s \<Longrightarrow> (if \<exists>y. rv = Some y then valid_sched and invs and (\<lambda>s. the rv \<in> non_kernel_IRQs \<longrightarrow> scheduler_act_sane s \<and> ct_not_queued s) else valid_sched) s
 2. \<lbrace>?Q1\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>rv. valid_sched and invs and K (rv \<notin> Some ` non_kernel_IRQs)\<rbrace>
 3. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> do_machine_op (getActiveIRQ True) \<lbrace>\<lambda>rv. valid_sched and invs and K (rv \<notin> Some ` non_kernel_IRQs)\<rbrace>
 2. \<And>s. (valid_sched and invs) s \<Longrightarrow> ?Q1 s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma execution_restrict:
  assumes e: "s \<in> execution (ADT_A_if utf) s0 js"
  shows "step_restrict s" apply (insert e) apply (induct js arbitrary: s rule: rev_induct) apply (clarsimp simp add: execution_def ADT_A_if_def steps_def) apply (clarsimp simp add: execution_def Fin_ADT_if Init_ADT_if steps_def) apply (simp add: ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. step_restrict s proof (prove)
goal (1 subgoal):
 1. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> step_restrict s proof (prove)
goal (2 subgoals):
 1. \<And>s. s \<in> execution (ADT_A_if utf) s0 [] \<Longrightarrow> step_restrict s
 2. \<And>x xs s. \<lbrakk>\<And>s. s \<in> execution (ADT_A_if utf) s0 xs \<Longrightarrow> step_restrict s; s \<in> execution (ADT_A_if utf) s0 (xs @ [x])\<rbrakk> \<Longrightarrow> step_restrict s proof (prove)
goal (1 subgoal):
 1. \<And>x xs s. \<lbrakk>\<And>s. s \<in> execution (ADT_A_if utf) s0 xs \<Longrightarrow> step_restrict s; s \<in> execution (ADT_A_if utf) s0 (xs @ [x])\<rbrakk> \<Longrightarrow> step_restrict s proof (prove)
goal (1 subgoal):
 1. \<And>xs a b ba aa bb bc. \<lbrakk>\<And>a b ba. ((a, b), ba) \<in> foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) ({s0} \<inter> full_invs_if \<inter> Collect step_restrict) xs \<Longrightarrow> step_restrict ((a, b), ba); (((aa, bb), bc), (a, b), ba) \<in> Step (ADT_A_if utf) (); ((aa, bb), bc) \<in> foldl (\<lambda>S j. Step (ADT_A_if utf) () `` S) ({s0} \<inter> full_invs_if \<inter> Collect step_restrict) xs\<rbrakk> \<Longrightarrow> step_restrict ((a, b), ba) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma Step_ADT_A_if':
  "((s,s') \<in> system.Step (ADT_A_if utf) u) \<Longrightarrow> ((s,s') \<in> Step (ADT_A_if utf) u)" apply (simp add: system.Step_def execution_def steps_def ADT_A_if_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> system.Step (ADT_A_if utf) u \<Longrightarrow> (s, s') \<in> Step (ADT_A_if utf) u proof (prove)
goal (1 subgoal):
 1. s' \<in> (global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}) `` ({s} \<inter> full_invs_if \<inter> Collect step_restrict) \<Longrightarrow> (s, s') \<in> global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<and> step_restrict s' proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma invs_if_full_invs_if:
  "invs_if s \<Longrightarrow> s \<in> full_invs_if" by (clarsimp simp: full_invs_if_def invs_if_def Invs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs_if s \<Longrightarrow> s \<in> full_invs_if
theory ADT_IF

lemma ADT_A_if_Step_system:
  "Step_system (ADT_A_if utf) s0" apply (rule Init_Fin_system_Step_system) apply (rule Init_inv_Fin_system_Init_Fin_system) apply (clarsimp simp: Init_inv_Fin_system_def ADT_A_if_def
                        invs_if_full_invs_if system.reachable_def extras_s0) apply (frule execution_invs[simplified ADT_A_if_def]) apply (frule execution_restrict[simplified ADT_A_if_def]) apply (frule invs_if_full_invs_if,force) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Step_system (ADT_A_if utf) s0 proof (prove)
goal (1 subgoal):
 1. Init_Fin_system (ADT_A_if utf) s0 proof (prove)
goal (1 subgoal):
 1. Init_inv_Fin_system (ADT_A_if utf) s0 proof (prove)
goal (1 subgoal):
 1. \<And>a b ba js. ((a, b), ba) \<in> execution \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> Collect step_restrict, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}\<rparr> s0 js \<Longrightarrow> {((a, b), ba)} \<inter> full_invs_if \<inter> Collect step_restrict = {((a, b), ba)} proof (prove)
goal (1 subgoal):
 1. \<And>a b ba js. \<lbrakk>((a, b), ba) \<in> execution \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> Collect step_restrict, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}\<rparr> s0 js; invs_if ((a, b), ba)\<rbrakk> \<Longrightarrow> {((a, b), ba)} \<inter> full_invs_if \<inter> Collect step_restrict = {((a, b), ba)} proof (prove)
goal (1 subgoal):
 1. \<And>a b ba js. \<lbrakk>((a, b), ba) \<in> execution \<lparr>Init = \<lambda>s. {s} \<inter> full_invs_if \<inter> Collect step_restrict, Fin = id, Step = \<lambda>u. global_automaton_if check_active_irq_A_if (do_user_op_A_if utf) kernel_call_A_if kernel_handle_preemption_if kernel_schedule_if kernel_exit_A_if \<inter> {(s, y). step_restrict y}\<rparr> s0 js; invs_if ((a, b), ba); step_restrict ((a, b), ba)\<rbrakk> \<Longrightarrow> {((a, b), ba)} \<inter> full_invs_if \<inter> Collect step_restrict = {((a, b), ba)} proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma ADT_A_if_Run_reachable:
  "(s0, t) \<in> Run (system.Step (ADT_A_if utf)) as \<Longrightarrow> system.reachable (ADT_A_if utf) s0 t" apply (simp add: system.reachable_def) apply (simp add: Step_system_execution_Run_s0[OF ADT_A_if_Step_system]) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s0, t) \<in> Run (system.Step (ADT_A_if utf)) as \<Longrightarrow> system.reachable (ADT_A_if utf) s0 t proof (prove)
goal (1 subgoal):
 1. (s0, t) \<in> Run (system.Step (ADT_A_if utf)) as \<Longrightarrow> \<exists>js. t \<in> execution (ADT_A_if utf) s0 js proof (prove)
goal (1 subgoal):
 1. (s0, t) \<in> Run (system.Step (ADT_A_if utf)) as \<Longrightarrow> \<exists>js. (s0, t) \<in> Run (system.Step (ADT_A_if utf)) js
theory ADT_IF

lemma Step_ADT_A_if:
  "system.reachable (ADT_A_if utf) s0 s
   \<Longrightarrow> ((s,s') \<in> system.Step (ADT_A_if utf) u) = ((s,s') \<in> Step (ADT_A_if utf) u)" apply (simp add: system.reachable_def) apply (clarsimp) apply (frule execution_invs) apply (frule invs_if_full_invs_if) apply (frule execution_restrict) apply (simp add: system.Step_def execution_def steps_def ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) u) = ((s, s') \<in> Step (ADT_A_if utf) u) proof (prove)
goal (1 subgoal):
 1. \<exists>js. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) ()) = ((s, s') \<in> Step (ADT_A_if utf) ()) proof (prove)
goal (1 subgoal):
 1. \<And>js. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) ()) = ((s, s') \<in> Step (ADT_A_if utf) ()) proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>s \<in> execution (ADT_A_if utf) s0 js; invs_if s\<rbrakk> \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) ()) = ((s, s') \<in> Step (ADT_A_if utf) ()) proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if\<rbrakk> \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) ()) = ((s, s') \<in> Step (ADT_A_if utf) ()) proof (prove)
goal (1 subgoal):
 1. \<And>js. \<lbrakk>s \<in> execution (ADT_A_if utf) s0 js; invs_if s; s \<in> full_invs_if; step_restrict s\<rbrakk> \<Longrightarrow> ((s, s') \<in> system.Step (ADT_A_if utf) ()) = ((s, s') \<in> Step (ADT_A_if utf) ()) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma ADT_A_if_reachable_invs_if:
  "system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> invs_if s" apply (clarsimp simp: system.reachable_def) apply (erule execution_invs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. system.reachable (ADT_A_if utf) s0 s \<Longrightarrow> invs_if s proof (prove)
goal (1 subgoal):
 1. \<And>js. s \<in> execution (ADT_A_if utf) s0 js \<Longrightarrow> invs_if s proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma ADT_A_if_enabled_Step_system:
  "enabled_Step_system (ADT_A_if utf) s0" by (simp add: enabled_Step_system_def ADT_A_if_Step_system ADT_A_if_enabled_system)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. enabled_Step_system (ADT_A_if utf) s0
theory ADT_IF

lemma next_irq_state_Suc:
  "\<lbrakk> irq_at cur masks = None; next_irq_state_dom (cur,masks) \<rbrakk>
     \<Longrightarrow> next_irq_state (Suc cur) masks = next_irq_state cur masks" by (simp add: next_irq_state.psimps split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur masks = None; next_irq_state_dom (cur, masks)\<rbrakk> \<Longrightarrow> next_irq_state (Suc cur) masks = next_irq_state cur masks
theory ADT_IF

lemma next_irq_state_Suc':
  "\<lbrakk> irq_at cur masks = Some i; next_irq_state_dom (cur,masks) \<rbrakk>
     \<Longrightarrow> next_irq_state cur masks = cur" by (simp add: next_irq_state.psimps split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur masks = Some i; next_irq_state_dom (cur, masks)\<rbrakk> \<Longrightarrow> next_irq_state cur masks = cur
theory ADT_IF

lemma is_irq_at_next_irq_state_dom':
  "is_irq_at s irq pos \<Longrightarrow> next_irq_state_dom (pos,irq_masks (machine_state s))" apply (rule next_irq_state.domintros) apply (fastforce simp: is_irq_at_def ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_irq_at s irq pos \<Longrightarrow> next_irq_state_dom (pos, irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_irq_at s irq pos; irq_at pos (irq_masks (machine_state s)) = None\<rbrakk> \<Longrightarrow> next_irq_state_dom (Suc pos, irq_masks (machine_state s)) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma is_irq_at_next_irq_state_dom:
  "\<lbrakk> pos \<le> next; is_irq_at s irq next \<rbrakk>
     \<Longrightarrow> next_irq_state_dom (pos,irq_masks (machine_state s))" apply (induct rule: inc_induct) apply (erule is_irq_at_next_irq_state_dom') apply (rule next_irq_state.domintros) apply (blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pos \<le> next; is_irq_at s irq next\<rbrakk> \<Longrightarrow> next_irq_state_dom (pos, irq_masks (machine_state s)) proof (prove)
goal (2 subgoals):
 1. is_irq_at s irq next \<Longrightarrow> next_irq_state_dom (next, irq_masks (machine_state s))
 2. \<And>n. \<lbrakk>pos \<le> n; n < next; is_irq_at s irq next \<Longrightarrow> next_irq_state_dom (Suc n, irq_masks (machine_state s)); is_irq_at s irq next\<rbrakk> \<Longrightarrow> next_irq_state_dom (n, irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pos \<le> n; n < next; is_irq_at s irq next \<Longrightarrow> next_irq_state_dom (Suc n, irq_masks (machine_state s)); is_irq_at s irq next\<rbrakk> \<Longrightarrow> next_irq_state_dom (n, irq_masks (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>pos \<le> n; n < next; is_irq_at s irq next \<Longrightarrow> next_irq_state_dom (Suc n, irq_masks (machine_state s)); is_irq_at s irq next; irq_at n (irq_masks (machine_state s)) = None\<rbrakk> \<Longrightarrow> next_irq_state_dom (Suc n, irq_masks (machine_state s)) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma is_irq_at_next_irq_state:
  "is_irq_at s irq pos
   \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) = pos" apply (subst next_irq_state.psimps[OF is_irq_at_next_irq_state_dom']) apply assumption apply (fastforce simp: is_irq_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_irq_at s irq pos \<Longrightarrow> next_irq_state pos (irq_masks (machine_state s)) = pos proof (prove)
goal (2 subgoals):
 1. is_irq_at s irq pos \<Longrightarrow> is_irq_at s ?irq pos
 2. is_irq_at s irq pos \<Longrightarrow> (if irq_at pos (irq_masks (machine_state s)) = None then next_irq_state (Suc pos) (irq_masks (machine_state s)) else pos) = pos proof (prove)
goal (1 subgoal):
 1. is_irq_at s irq pos \<Longrightarrow> (if irq_at pos (irq_masks (machine_state s)) = None then next_irq_state (Suc pos) (irq_masks (machine_state s)) else pos) = pos proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma next_irq_state_less:
  "\<lbrakk> irq_at cur masks = None; irq_is_recurring irq s; masks = (irq_masks (machine_state s)) \<rbrakk>
     \<Longrightarrow> cur < next_irq_state cur masks" apply (frule_tac n=cur in recurring_next_irq_state_dom) apply (simp add: next_irq_state.psimps) apply (rule less_le_trans[OF _ next_irq_state_le]) apply simp apply assumption apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur masks = None; irq_is_recurring irq s; masks = irq_masks (machine_state s)\<rbrakk> \<Longrightarrow> cur < next_irq_state cur masks proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur masks = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> cur < next_irq_state cur masks proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> cur < next_irq_state (Suc cur) (irq_masks (machine_state s)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> cur < Suc cur
 2. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> irq_is_recurring ?irq3 ?s3
 3. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) = irq_masks (machine_state ?s3) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> irq_is_recurring ?irq3 ?s3
 2. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) = irq_masks (machine_state ?s3) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>irq_at cur (irq_masks (machine_state s)) = None; irq_is_recurring irq s; masks = irq_masks (machine_state s); next_irq_state_dom (cur, irq_masks (machine_state s))\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) = irq_masks (machine_state s) proof (prove)
goal:
No subgoals!
theory ADT_IF

lemma next_irq_state_Suc_le:
  assumes recur: "irq_is_recurring irq s"
  assumes m: "masks = irq_masks (machine_state s)"
  shows "next_irq_state pos masks \<le> next_irq_state (Suc pos) masks" by (rule next_irq_state_mono[OF _ recur m], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. next_irq_state pos masks \<le> next_irq_state (Suc pos) masks
theory ADT_IF

lemma irq_state_inv_refl:
  "irq_state_inv s s" by (simp add: irq_state_inv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_inv s s