theory SyscallArgs_C

lemma interpret_excaps_eq[unfolded array_to_list_def, simplified]:
  "interpret_excaps excps = xs \<Longrightarrow>
   \<forall>n < length xs. (index (excaprefs_C excps) n) = (xs ! n)
         \<and> (length xs < length (array_to_list (excaprefs_C excps))
              \<longrightarrow> index (excaprefs_C excps) (length xs) = NULL)" apply (clarsimp simp: interpret_excaps_def) apply (drule length_takeWhile_gt) apply (clarsimp simp: nth_append) apply (clarsimp simp: array_to_list_def) apply (frule_tac f=length in arg_cong, subst(asm) length_map,
         simp(no_asm_use)) apply (rule conjI) apply (rule trans, erule map_upt_eq_vals_D, simp) apply (simp add: nth_append) apply clarsimp apply (frule nth_length_takeWhile) apply (rule trans, erule map_upt_eq_vals_D, simp) apply (simp add: nth_append NULL_ptr_val) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. interpret_excaps excps = xs \<Longrightarrow> \<forall>n<length xs. excaprefs_C excps.[n] = xs ! n \<and> (length xs < length (array_to_list (excaprefs_C excps)) \<longrightarrow> excaprefs_C excps.[length xs] = NULL) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>xs = takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)); n < length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)))\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)) ! n \<and> (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) < length (array_to_list (excaprefs_C excps)) \<longrightarrow> excaprefs_C excps.[length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)))] = NULL) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>xs = takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)); \<exists>ys zs. length ys = Suc n \<and> array_to_list (excaprefs_C excps) = ys @ zs \<and> takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)) ! n \<and> (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps))) < length (array_to_list (excaprefs_C excps)) \<longrightarrow> excaprefs_C excps.[length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (array_to_list (excaprefs_C excps)))] = NULL) proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; array_to_list (excaprefs_C excps) = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = ys ! n \<and> (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL) proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = ys ! n \<and> (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL) proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = ys ! n \<and> (length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL) proof (prove)
goal (2 subgoals):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> excaprefs_C excps.[n] = ys ! n
 2. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL proof (prove)
goal (2 subgoals):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> (ys @ zs) ! n = ys ! n
 2. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys + length zs = 3\<rbrakk> \<Longrightarrow> length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs \<longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; n + length zs = 2; length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs\<rbrakk> \<Longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; n + length zs = 2; length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs; \<not> ptr_val (zs ! length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs)) \<noteq> 0\<rbrakk> \<Longrightarrow> excaprefs_C excps.[Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs))] = NULL proof (prove)
goal (1 subgoal):
 1. \<And>n ys zs. \<lbrakk>xs = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; length ys = Suc n; map (index (excaprefs_C excps)) [0..<3] = ys @ zs; takeWhile (\<lambda>x. ptr_val x \<noteq> 0) (ys @ zs) = ys @ takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs; n + length zs = 2; length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs) < length zs; \<not> ptr_val (zs ! length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs)) \<noteq> 0\<rbrakk> \<Longrightarrow> (ys @ zs) ! Suc (n + length (takeWhile (\<lambda>x. ptr_val x \<noteq> 0) zs)) = NULL proof (prove)
goal:
No subgoals!