More fixes for pointer array assertions.

proof/asmrefine/SEL4GraphRefine.thy

@@ -65,7 +65,7 @@ lemma snd_snd_gs_new_frames_new_cnodes[simp]:
   "snd (snd ((if P then f else g) gs)) = (if P then snd (snd (f gs)) else snd (snd (g gs)))"
   by (simp_all add: gs_new_frames_def gs_new_cnodes_def gs_clear_region_def)
 
-ML {* val nm = "Kernel_C.cancelIPC" *}
+ML {* val nm = "Kernel_C.loadCapTransfer" *}
 
 (*
 local_setup {*  define_graph_fun_short funs nm *}
@@ -80,6 +80,7 @@ ML {*
 ML {*
     val v = ProveSimplToGraphGoals.test_graph_refine_proof funs (csenv ()) ctxt nm
 *}
+
 *)
 
 ML {* ProveSimplToGraphGoals.test_all_graph_refine_proofs_after

tools/asmrefine/CommonOpsLemmas.thy

@@ -95,7 +95,7 @@ lemma ptr_add_assertion_sintD:
   "ptr_add_assertion ptr (sint (x :: ('a :: len) word)) strong htd
     \<longrightarrow> (x = 0 \<or> (x <s 0 \<and> array_assertion (ptr +\<^sub>p sint x)
             (unat (- x)) htd)
-        \<or> (0 <s x \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd))"
+        \<or> (x \<noteq> 0 \<and> \<not> x <s 0 \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd))"
   using unat_lt2p[where x=x]
   apply (simp add: ptr_add_assertion_def word_sless_alt
                    sint_uint_sless_0_if[THEN arg_cong[where f="\<lambda>x. - x"]]
@@ -105,7 +105,7 @@ lemma ptr_add_assertion_sintD:
                    word_size
            del: unat_lt2p)
   apply (simp add: array_assertion_shrink_right)
-  apply auto
+  apply (auto simp: linorder_not_less)
   done
 
 end

tools/asmrefine/ProveGraphRefine.thy

@@ -577,6 +577,7 @@ fun dest_ptr_add_assertion ctxt = SUBGOAL (fn (t, i) =>
           THEN_ALL_NEW TRY o REPEAT_ALL_NEW (dresolve_tac ctxt
             @{thms ptr_add_assertion_uintD[rule_format]
                    ptr_add_assertion_sintD[rule_format]})
+          THEN_ALL_NEW TRY o safe_goal_tac ctxt
           THEN_ALL_NEW SUBGOAL (fn (t, i) =>
             if Term.exists_Const (fn (s, _) => s = @{const_name ptr_add_assertion}
                 orelse s = @{const_name ptr_add_assertion'}) t