theory KHeap_AI

lemma valid_irq_states_triv:
  assumes irqs: "\<And>P. f \<lbrace>\<lambda>s. P (interrupt_states s)\<rbrace>"
  assumes ms: "\<And>P. f \<lbrace>\<lambda>s. P (machine_state s)\<rbrace>"
  shows "f \<lbrace>valid_irq_states\<rbrace>" apply(clarsimp simp: valid_def valid_irq_states_def valid_irq_masks_def) apply(case_tac "interrupt_states s irq = IRQInactive") apply(erule use_valid[OF _ ms]) apply blast apply(drule_tac P1="\<lambda>x. x irq \<noteq> IRQInactive" in use_valid[OF _ irqs]) apply assumption by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states\<rbrace> f \<lbrace>\<lambda>_. valid_irq_states\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; (a, b) \<in> fst (f s); interrupt_states b irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; (a, b) \<in> fst (f s); interrupt_states b irq = IRQInactive; interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq
 2. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; (a, b) \<in> fst (f s); interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; interrupt_states b irq = IRQInactive; interrupt_states s irq = IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state s) irq
 2. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; (a, b) \<in> fst (f s); interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; (a, b) \<in> fst (f s); interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq proof (prove)
goal (2 subgoals):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> interrupt_states s irq \<noteq> IRQInactive
 2. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive; interrupt_states b irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq proof (prove)
goal (1 subgoal):
 1. \<And>s a b irq. \<lbrakk>\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks (machine_state s) irq; interrupt_states b irq = IRQInactive; interrupt_states s irq \<noteq> IRQInactive; interrupt_states b irq \<noteq> IRQInactive\<rbrakk> \<Longrightarrow> irq_masks (machine_state b) irq