theory SyscallArgs_C

lemma interpret_excaps_test_null[unfolded array_to_list_def, simplified]:
  "\<lbrakk> length (interpret_excaps excps) \<ge> n;
        n < length (array_to_list (excaprefs_C excps)) \<rbrakk>
     \<Longrightarrow> (index (excaprefs_C excps) n = NULL) = (length (interpret_excaps excps) = n)" apply (simp add: interpret_excaps_def) apply (rule iffI) apply (erule order_antisym[rotated]) apply (rule length_takeWhile_le) apply (simp add: array_to_list_def) apply simp apply (drule length_takeWhile_ge) apply (simp add: array_to_list_def NULL_ptr_val) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length (interpret_excaps excps); n < length (array_to_list (excaprefs_C excps))\<rbrakk> \<Longrightarrow> (excaprefs_C excps.[n] = NULL) = (length (interpret_excaps excps) = n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps))\<rbrakk> \<Longrightarrow> (excaprefs_C excps.[n] = NULL) = (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps)); excaprefs_C excps.[n] = NULL\<rbrakk> \<Longrightarrow> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n
 2. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps)); length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length (array_to_list (excaprefs_C excps)); excaprefs_C excps.[n] = NULL\<rbrakk> \<Longrightarrow> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) \<le> n
 2. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps)); length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < length (array_to_list (excaprefs_C excps)); excaprefs_C excps.[n] = NULL\<rbrakk> \<Longrightarrow> \<not> ptr_val (array_to_list (excaprefs_C excps) ! n) \<noteq> 0
 2. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps)); length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))); n < length (array_to_list (excaprefs_C excps)); length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length (array_to_list (excaprefs_C excps)); length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) = n\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length (array_to_list (excaprefs_C excps)); length (array_to_list (excaprefs_C excps)) = n \<or> n < length (array_to_list (excaprefs_C excps)) \<and> \<not> ptr_val (array_to_list (excaprefs_C excps) ! n) \<noteq> 0\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = NULL proof (prove)
goal:
No subgoals!