theory Detype_R

lemma createNewObjects_Cons:
  assumes dlength: "length dest < 2 ^ word_bits"
  shows "createNewObjects ty src (dest @ [lt]) ptr us d =
  do createNewObjects ty src dest ptr us d;
     (RetypeDecls_H.createObject ty ((of_nat (length dest) << APIType_capBits ty us) + ptr) us d
       >>= insertNewCap src lt)
  od" proof - from dlength have expand:"dest\<noteq>[] \<longrightarrow> [(0::word32) .e. of_nat (length dest)]
      = [0.e.of_nat (length dest - 1)] @ [of_nat (length dest)]" apply (cases dest) apply clarsimp+ apply (rule upto_enum_inc_1) apply (rule word_of_nat_less) apply (simp add: word_bits_conv minus_one_norm) done have length:"\<lbrakk>length dest < 2 ^ word_bits;dest \<noteq> []\<rbrakk>
      \<Longrightarrow> length [(0::word32) .e. of_nat (length dest - 1)] = length dest" proof (induct dest) case Nil thus ?case by simp next case (Cons x xs) thus ?case by (simp add:unat_of_nat32) qed show ?thesis using dlength apply (case_tac "dest = []") apply (simp add: zipWithM_x_def createNewObjects_def
          sequence_x_def zipWith_def) apply (clarsimp simp:createNewObjects_def) apply (subst expand) apply simp apply (subst zipWithM_x_append1) apply (rule length) apply (simp add:field_simps)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (state)
goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (chain)
picking this:
length dest < 2 ^ word_bits proof (prove)
using this:
length dest < 2 ^ word_bits

goal (1 subgoal):
 1. dest \<noteq> [] \<longrightarrow> [0 .e. word_of_nat (length dest)] = [0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest = []\<rbrakk> \<Longrightarrow> dest \<noteq> [] \<longrightarrow> [0 .e. word_of_nat (length dest)] = [0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)]
 2. \<And>a list. \<lbrakk>length dest < 2 ^ word_bits; dest = a # list\<rbrakk> \<Longrightarrow> dest \<noteq> [] \<longrightarrow> [0 .e. word_of_nat (length dest)] = [0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>Suc (length list) < 2 ^ word_bits; dest = a # list\<rbrakk> \<Longrightarrow> [0 .e. 1 + word_of_nat (length list)] = [0 .e. word_of_nat (length list)] @ [1 + word_of_nat (length list)] proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>Suc (length list) < 2 ^ word_bits; dest = a # list\<rbrakk> \<Longrightarrow> word_of_nat (length list) < 2 ^ word_bits - 1 proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>Suc (length list) < 2 ^ word_bits; dest = a # list\<rbrakk> \<Longrightarrow> length list < unat (2 ^ word_bits - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
dest \<noteq> [] \<longrightarrow> [0 .e. word_of_nat (length dest)] = [0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)]

goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest proof (state)
goal (2 subgoals):
 1. \<lbrakk>length [] < 2 ^ word_bits; [] \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length [] - 1)] = length []
 2. \<And>a dest. \<lbrakk>\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest; length (a # dest) < 2 ^ word_bits; a # dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length (a # dest) - 1)] = length (a # dest) proof (state)
this:
length [] < 2 ^ word_bits
[] \<noteq> []

goal (2 subgoals):
 1. \<lbrakk>length [] < 2 ^ word_bits; [] \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length [] - 1)] = length []
 2. \<And>a dest. \<lbrakk>\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest; length (a # dest) < 2 ^ word_bits; a # dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length (a # dest) - 1)] = length (a # dest) proof (prove)
using this:
length [] < 2 ^ word_bits
[] \<noteq> []

goal (1 subgoal):
 1. length [0 .e. word_of_nat (length [] - 1)] = length [] proof (state)
this:
length [0 .e. word_of_nat (length [] - 1)] = length []

goal (1 subgoal):
 1. \<And>a dest. \<lbrakk>\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest; length (a # dest) < 2 ^ word_bits; a # dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length (a # dest) - 1)] = length (a # dest) proof (state)
goal (1 subgoal):
 1. \<And>a dest. \<lbrakk>\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest; length (a # dest) < 2 ^ word_bits; a # dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length (a # dest) - 1)] = length (a # dest) proof (state)
this:
\<lbrakk>length xs < 2 ^ word_bits; xs \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length xs - 1)] = length xs
length (x # xs) < 2 ^ word_bits
x # xs \<noteq> []

goal (1 subgoal):
 1. \<And>a dest. \<lbrakk>\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest; length (a # dest) < 2 ^ word_bits; a # dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length (a # dest) - 1)] = length (a # dest) proof (prove)
using this:
\<lbrakk>length xs < 2 ^ word_bits; xs \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length xs - 1)] = length xs
length (x # xs) < 2 ^ word_bits
x # xs \<noteq> []

goal (1 subgoal):
 1. length [0 .e. word_of_nat (length (x # xs) - 1)] = length (x # xs) proof (state)
this:
length [0 .e. word_of_nat (length (x # xs) - 1)] = length (x # xs)

goal:
No subgoals! proof (state)
this:
\<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest

goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
using this:
length dest < 2 ^ word_bits

goal (1 subgoal):
 1. createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest = []\<rbrakk> \<Longrightarrow> createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od
 2. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest)] (dest @ [lt]) = do y <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - Suc 0)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> dest \<noteq> []
 2. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) ([0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)]) (dest @ [lt]) = do y <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - Suc 0)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) ([0 .e. word_of_nat (length dest - 1)] @ [word_of_nat (length dest)]) (dest @ [lt]) = do y <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - Suc 0)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length [0 .e. word_of_nat (length dest - 1)] = length dest
 2. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> do _ <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - 1)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od = do y <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - Suc 0)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> length dest < 2 ^ word_bits
 2. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> dest \<noteq> []
 3. \<lbrakk>length dest < 2 ^ word_bits; dest \<noteq> []\<rbrakk> \<Longrightarrow> do _ <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - 1)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od = do y <- zipWithM_x (\<lambda>num slot. global.createObject ty ((num << APIType_capBits ty us) + ptr) us d >>= insertNewCap src slot) [0 .e. word_of_nat (length dest - Suc 0)] dest;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od proof (prove)
goal:
No subgoals! proof (state)
this:
createNewObjects ty src (dest @ [lt]) ptr us d = do createNewObjects ty src dest ptr us d;
global.createObject ty ((word_of_nat (length dest) << APIType_capBits ty us) + ptr) us d >>= insertNewCap src lt
od

goal:
No subgoals!