[STATEMENT]
lemma cfWriteExtendFileSize:
  "[| ~ index < fileSize cfile1;
      cfWrite cfile1 index value = Some cfile2
   |] ==> fileSize cfile2 = Suc index"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfWrite cfile1 index value = Some cfile2\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (simp add: cfWrite_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; (if index div blockSize < numBlocks then if index < fileSize cfile1 then Some (cfWriteNoExtend cfile1 index value) else Some (cfWriteNoExtend (cfExtendFile cfile1 index) index value) else None) = Some cfile2\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (case_tac "index div blockSize < numBlocks", simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfWriteNoExtend (cfExtendFile cfile1 index) index value = cfile2; index div blockSize < numBlocks\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply (simp add: cfWriteNoExtend_def cfExtendFile_def Let_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> index < fileSize cfile1; cfile1\<lparr>fileSize := Suc index, nextFreeBlock := Suc (index div blockSize), data := writeCArray (data cfile1) (index div blockSize) (writeCArray (readCArray (data cfile1) (index div blockSize)) (index mod blockSize) value)\<rparr> = cfile2; index div blockSize < numBlocks\<rbrakk> \<Longrightarrow> fileSize cfile2 = Suc index
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done