theory ADT_IF

lemma irq_state_inv_trivE':
  assumes irq_state:
    "\<And>P. f \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace>"
  assumes irq_masks:
    "\<And>P. \<lbrace>(\<lambda>s. P (irq_masks_of_state s)) and Q\<rbrace> f \<lbrace>\<lambda>_ s. P (irq_masks_of_state s)\<rbrace>"
  assumes no_err:
    "\<And>P. \<lbrace>\<top>\<rbrace> f -, \<lbrace>P\<rbrace>"
  shows
    "\<lbrace>irq_state_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace>" apply (clarsimp simp: validE_def valid_def irq_state_inv_def split: sum.splits) apply (rule use_valid[OF _ irq_state], assumption) apply (rule use_valid[OF _ irq_masks],assumption) apply clarsimp apply (erule use_validE_E[OF _ no_err]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irq_state_inv st and Q\<rbrace> f \<lbrace>\<lambda>_. irq_state_inv st\<rbrace>, \<lbrace>\<lambda>_. irq_state_next st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); Q s\<rbrakk> \<Longrightarrow> ((\<exists>x1. a = Inl x1) \<longrightarrow> irq_state_next st b) \<and> ((\<exists>x2. a = Inr x2) \<longrightarrow> irq_state_of_state st \<le> irq_state_of_state b \<and> irq_masks_of_state b = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state b)) (irq_masks_of_state b) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state b)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); Q s\<rbrakk> \<Longrightarrow> ((\<exists>x1. a = Inl x1) \<longrightarrow> irq_state_next st b) \<and> ((\<exists>x2. a = Inr x2) \<longrightarrow> irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state b = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state b) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state b)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); Q s\<rbrakk> \<Longrightarrow> ((\<lambda>sa. ((\<exists>x1. a = Inl x1) \<longrightarrow> irq_state_next st b) \<and> ((\<exists>x2. a = Inr x2) \<longrightarrow> irq_state_of_state st \<le> irq_state_of_state s \<and> irq_masks_of_state sa = irq_masks_of_state st \<and> next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state sa) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state sa))) and Q) s proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>(Inl x1, b) \<in> fst (f s); irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); Q s\<rbrakk> \<Longrightarrow> irq_state_next st b proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>irq_state_of_state st \<le> irq_state_of_state s; irq_masks_of_state s = irq_masks_of_state st; next_irq_state (Suc (irq_state_of_state s)) (irq_masks_of_state st) = next_irq_state (Suc (irq_state_of_state st)) (irq_masks_of_state st); Q s\<rbrakk> \<Longrightarrow> True proof (prove)
goal:
No subgoals!