theory KHeap_DR

lemma resolve_address_bits_error_branch2:
  "\<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap;cap = cap.CNodeCap oref radix_bits guard\<rbrakk>
   \<Longrightarrow> \<exists>excep. CSpace_A.resolve_address_bits (cap,ref) = throwError excep" unfolding resolve_address_bits_def apply (case_tac cap) apply (simp_all add:CSpace_A.resolve_address_bits'.simps in_terminate_branch_def in_recursive_branch_def) apply (clarsimp | rule conjI)+ apply (clarsimp simp:whenE_def | rule conjI)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> \<exists>excep. CSpace_A.resolve_address_bits (cap, ref) = throwError excep proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep proof (prove)
goal (12 subgoals):
 1. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.NullCap\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 2. \<And>x21 x22 x23 x24. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 3. \<And>x31 x32 x33. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 4. \<And>x41 x42 x43. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 5. \<And>x51 x52 x53. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 6. \<And>x61 x62 x63. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 7. \<And>x7. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 8. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 9. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = IRQControlCap\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
 10. \<And>x10. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; \<not> in_terminate_branch ref cap; \<not> in_recursive_branch ref cap; cap = cap.CNodeCap oref radix_bits guard; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> \<exists>excep. resolve_address_bits' TYPE('a) (cap, ref) = throwError excep
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x61. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; x61 = oref; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> (length ref \<le> radix_bits + length guard \<longrightarrow> (radix_bits = 0 \<and> guard = [] \<longrightarrow> (\<exists>excep. fail = throwError excep)) \<and> (\<exists>excep. doE y <- whenE (\<not> guard \<le> ref) (throwError (GuardMismatch (length ref) guard));
y <- whenE (length ref < radix_bits + length guard) (throwError (DepthMismatch (length ref) (radix_bits + length guard)));
returnOk ((oref, drop (length guard) ref), [])
odE = throwError excep)) \<and> (\<not> length ref \<le> radix_bits + length guard \<longrightarrow> (radix_bits = 0 \<and> guard = [] \<longrightarrow> (\<exists>excep. fail = throwError excep)) \<and> (\<exists>excep. throwError (GuardMismatch (length ref) guard) = throwError excep)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; length ref \<le> radix_bits + length guard\<rbrakk> \<Longrightarrow> \<exists>excep. doE y <- whenE (\<not> guard \<le> ref) (throwError (GuardMismatch (length ref) guard));
y <- whenE (length ref < radix_bits + length guard) (throwError (DepthMismatch (length ref) (radix_bits + length guard)));
returnOk ((oref, drop (length guard) ref), [])
odE = throwError excep
 2. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> \<not> length ref \<le> radix_bits + length guard \<longrightarrow> (radix_bits = 0 \<and> guard = [] \<longrightarrow> (\<exists>excep. fail = throwError excep)) \<and> (\<exists>excep. throwError (GuardMismatch (length ref) guard) = throwError excep) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; cap = cap.CNodeCap oref radix_bits guard; length ref < radix_bits + length guard; \<not> guard \<le> ref\<rbrakk> \<Longrightarrow> \<exists>excep. throwError (GuardMismatch (length ref) guard) = throwError excep
 2. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; cap = cap.CNodeCap oref radix_bits guard; length ref < radix_bits + length guard\<rbrakk> \<Longrightarrow> guard \<le> ref \<longrightarrow> (\<exists>excep. throwError (DepthMismatch (length ref) (radix_bits + length guard)) = throwError excep)
 3. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard; length ref \<le> radix_bits + length guard\<rbrakk> \<Longrightarrow> length ref = radix_bits + length guard \<longrightarrow> (\<exists>excep. throwError (GuardMismatch (radix_bits + length guard) guard) = throwError excep)
 4. \<lbrakk>0 < radix_bits \<or> guard \<noteq> []; length ref = radix_bits + length guard \<longrightarrow> \<not> guard \<le> ref; radix_bits + length guard < length ref \<longrightarrow> \<not> guard \<le> ref; cap = cap.CNodeCap oref radix_bits guard\<rbrakk> \<Longrightarrow> \<not> length ref \<le> radix_bits + length guard \<longrightarrow> (radix_bits = 0 \<and> guard = [] \<longrightarrow> (\<exists>excep. fail = throwError excep)) \<and> (\<exists>excep. throwError (GuardMismatch (length ref) guard) = throwError excep) proof (prove)
goal:
No subgoals!