theory ArchEmptyFail_AI

lemma arch_decode_invocation_empty_fail[wp]:
  "empty_fail (arch_decode_invocation label b c d e f)" apply (case_tac "invocation_type label") apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> \<open>-\<close>\<close>) apply (rename_tac alabel) apply (case_tac alabel; simp) apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDControlMakePool_empty_fail\<close>\<close>) apply (find_goal \<open>succeeds \<open>erule arch_decode_ARMASIDPoolAssign_empty_fail\<close>\<close>) apply ((simp add: arch_decode_ARMASIDControlMakePool_empty_fail arch_decode_ARMASIDPoolAssign_empty_fail)+)[2] including no_pre by ((simp add: arch_decode_invocation_def Let_def split: arch_cap.splits cap.splits option.splits | (wp+) | intro conjI impI allI)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (arch_decode_invocation label b c d e f) proof (prove)
goal (2 subgoals):
 1. \<And>x1. invocation_type label = GenInvocationLabel x1 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>x2. invocation_type label = ArchInvocationLabel x2 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f) proof (prove)
goal (2 subgoals):
 1. \<And>x2. invocation_type label = ArchInvocationLabel x2 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>x1. invocation_type label = GenInvocationLabel x1 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f) proof (prove)
goal (2 subgoals):
 1. \<And>alabel. invocation_type label = ArchInvocationLabel alabel \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>x1. invocation_type label = GenInvocationLabel x1 \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f) proof (prove)
goal (17 subgoals):
 1. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDClean_Data; alabel = ARMPDClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDInvalidate_Data; alabel = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 3. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDCleanInvalidate_Data; alabel = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 4. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDUnify_Instruction; alabel = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 5. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; alabel = ARMPageTableMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 6. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableUnmap; alabel = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 7. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; alabel = ARMPageMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 8. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageUnmap; alabel = ARMPageUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 9. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageClean_Data; alabel = ARMPageClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 10. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageInvalidate_Data; alabel = ARMPageInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDControlMakePool; alabel = ARMASIDControlMakePool\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDClean_Data; alabel = ARMPDClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 3. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDInvalidate_Data; alabel = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 4. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDCleanInvalidate_Data; alabel = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 5. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDUnify_Instruction; alabel = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 6. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; alabel = ARMPageTableMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 7. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableUnmap; alabel = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 8. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; alabel = ARMPageMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 9. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageUnmap; alabel = ARMPageUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 10. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageClean_Data; alabel = ARMPageClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
A total of 17 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDPoolAssign; alabel = ARMASIDPoolAssign\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMASIDControlMakePool; alabel = ARMASIDControlMakePool\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 3. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDClean_Data; alabel = ARMPDClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 4. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDInvalidate_Data; alabel = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 5. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDCleanInvalidate_Data; alabel = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 6. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDUnify_Instruction; alabel = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 7. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; alabel = ARMPageTableMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 8. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableUnmap; alabel = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 9. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; alabel = ARMPageMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 10. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageUnmap; alabel = ARMPageUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
A total of 17 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDClean_Data; alabel = ARMPDClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDInvalidate_Data; alabel = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 3. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDCleanInvalidate_Data; alabel = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 4. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDUnify_Instruction; alabel = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 5. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; alabel = ARMPageTableMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 6. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableUnmap; alabel = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 7. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; alabel = ARMPageMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 8. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageUnmap; alabel = ARMPageUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 9. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageClean_Data; alabel = ARMPageClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 10. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageInvalidate_Data; alabel = ARMPageInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDClean_Data; alabel = ARMPDClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 2. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDInvalidate_Data; alabel = ARMPDInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 3. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDCleanInvalidate_Data; alabel = ARMPDCleanInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 4. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPDUnify_Instruction; alabel = ARMPDUnify_Instruction\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 5. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableMap; alabel = ARMPageTableMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 6. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageTableUnmap; alabel = ARMPageTableUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 7. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageMap; alabel = ARMPageMap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 8. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageUnmap; alabel = ARMPageUnmap\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 9. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageClean_Data; alabel = ARMPageClean_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
 10. \<And>alabel. \<lbrakk>invocation_type label = ArchInvocationLabel ARMPageInvalidate_Data; alabel = ARMPageInvalidate_Data\<rbrakk> \<Longrightarrow> empty_fail (arch_decode_invocation label b c d e f)
A total of 15 subgoals...