| (* |
| * Copyright 2016, NICTA |
| * |
| * This software may be distributed and modified according to the terms of |
| * the GNU General Public License version 2. Note that NO WARRANTY is provided. |
| * See "LICENSE_GPLv2.txt" for details. |
| * |
| * @TAG(NICTA_GPL) |
| *) |
| |
| theory PleSle |
| imports |
| "../impl/BilbyFs_Shallow_Desugar_Tuples" |
| "../adt/WordArrayT" |
| "../adt/ArrayT" |
| "../adt/BufferT" |
| "HOL-Eisbach.Eisbach" |
| begin |
| |
| text{* axioms and lemmas that are *not* specific to 32 word. -> should be refactored.*} |
| axiomatization |
| where |
| u32_to_u8_is_ucast: |
| "u32_to_u8 = ucast" |
| and |
| u64_to_u8_is_ucast: |
| "u64_to_u8 = ucast" |
| and |
| u64_to_u32_is_ucast: |
| "u64_to_u32 = ucast" |
| and |
| u16_to_u8_is_ucast: |
| "u16_to_u8 = ucast" |
| |
| lemmas less_to_le = order_class.order.strict_implies_order |
| |
| lemma test_bit_out_of_bounds: |
| "\<lbrakk>n \<ge> 8\<rbrakk> \<Longrightarrow> ((w :: 8 word) !! n) = False" |
| by (auto dest!: test_bit_size simp:word_size) |
| |
| lemma mod_range_eq: |
| "\<lbrakk>n \<ge> (a::nat)*8; (n::nat) < (a+1)*8\<rbrakk> \<Longrightarrow> n mod 8 = n - (a*8)" |
| by (simp add: div_nat_eqI modulo_nat_def mult.commute) |
| |
| lemma range_le: |
| "\<lbrakk>(n :: nat) \<ge> (a::nat)*8; n < (a+1)*8\<rbrakk> \<Longrightarrow> |
| n - (a*8) < 8" |
| by simp |
| |
| lemma div_range_le: |
| "\<lbrakk>n < (a*8)\<rbrakk> \<Longrightarrow> (n :: nat) div 8 < a" |
| by auto |
| |
| lemma take_decomp: |
| "length l \<ge> n \<Longrightarrow> n > 0 \<Longrightarrow> (take n l) = ((hd l) # (take (n - 1) (tl l)))" |
| by (induct l) (simp add: take_Cons split: nat.split)+ |
| |
| lemma take_drop_decomp: |
| "k < length l \<Longrightarrow> length (drop k l) \<ge> n \<Longrightarrow> n > 0 |
| \<Longrightarrow> take n (drop k l) = (l ! k) # take (n - 1) (drop (k + 1) l)" |
| by (simp add: take_decomp hd_drop_conv_nth drop_Suc[symmetric] drop_tl[symmetric]) |
| |
| lemma elem_take_n: |
| "i<n \<Longrightarrow> (take n xs ! i) = xs ! i" |
| by simp |
| |
| lemma take_n_eq_simp: |
| "take len ys = take len xs \<Longrightarrow> |
| idx < len \<Longrightarrow> |
| ys !idx = xs !idx" |
| by (metis elem_take_n) |
| |
| lemma take_n_and_len'_eq_simp: |
| "take len ys = take len xs \<Longrightarrow> |
| idx < len' \<Longrightarrow> |
| len' \<le> len \<Longrightarrow> |
| ys !idx = xs !idx" |
| by (erule take_n_eq_simp) simp |
| |
| lemma drop_n_then_nth_eq: |
| assumes "n + i \<le> length xs" |
| assumes "n + i \<le> length ys" |
| assumes "ys ! (n + i) = xs ! (n + i)" |
| shows "drop n ys ! (0 + i) = drop n xs ! (0 + i)" |
| using assms by auto |
| |
| lemma drop_n_then_nth_eq_wo_0: |
| assumes "n + i \<le> length xs" |
| assumes "n + i \<le> length ys" |
| assumes "ys ! (n + i) = xs ! (n + i)" |
| shows "drop n ys ! i = drop n xs ! i" |
| using assms by auto |
| |
| lemma plus_no_overflow_unat_lift: |
| "(a::'a::len word ) < a + b \<Longrightarrow> unat (a+b) = unat a + unat b" |
| by unat_arith |
| |
| |
| method handle_wa_mod for offs :: "U32" = |
| (rule wordarray_modify_ret[where index=offs, simplified Let_def], |
| simp_all add: wordarray_make ArrA.defs ElemAO.defs ElemA.defs |
| setu8_def[unfolded tuple_simps sanitizers], unat_arith) |
| |
| lemma take_list_update: |
| "i < length xs |
| \<Longrightarrow> take n (xs[i := x]) = (if i < n then (take n xs)[i := x] else take n xs)" |
| by (induct xs arbitrary: n i, simp_all add: take_Cons split: nat.split) |
| |
| lemma drop_list_update: |
| "i < length xs |
| \<Longrightarrow> drop n (xs[i := x]) = (if i < n then drop n xs else (drop n xs)[i - n := x])" |
| by (induct xs arbitrary: n i, simp_all add: drop_Cons split: nat.split) |
| |
| definition ple16 :: "8 word list \<Rightarrow> 32 word \<Rightarrow> 16 word" |
| where |
| "ple16 data offs \<equiv> word_rcat (rev (take 2 (drop (unat offs) data)))" |
| |
| definition sle16 :: "U16 \<Rightarrow> U8 list" |
| where |
| "sle16 \<equiv> rev \<circ> word_rsplit" |
| |
| lemma deserialise_le16_ret: |
| assumes valid_offs: |
| "unat offs + 1 < length (\<alpha>wa $ data\<^sub>f buf)" |
| assumes no_ovf: |
| "offs < offs + 2" |
| shows |
| "deserialise_le16 (buf, offs) = (ple16 (\<alpha>wa $ data\<^sub>f buf) offs)" |
| using valid_offs |
| apply (subgoal_tac "(\<forall>i\<in>{0..1}. unat (offs+i) < length (\<alpha>wa (data\<^sub>f buf)))") |
| prefer 2 |
| apply unat_arith |
| apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"] ple16_def |
| deserialise_le16_def) |
| apply (subgoal_tac "(unat (offs + 1) > 0)") |
| prefer 2 |
| apply (drule_tac x=1 in bspec, simp) |
| using no_ovf apply unat_arith |
| apply auto[1] |
| apply (subst take_drop_decomp, (simp+))+ |
| apply (subst unatSuc[symmetric], (simp add: unat_gt_0[symmetric] add.commute[where b=offs]))+ |
| apply (rule trans, rule word_rcat_rsplit[symmetric]) |
| apply (rule arg_cong[where f=word_rcat]) |
| apply (subst word_rsplit_upt[where n=2], simp add: word_size) |
| apply simp |
| apply (simp add: upt_rec shiftr_over_or_dist shiftl_shiftr1 shiftl_shiftr2 word_size) |
| apply (safe intro!: word_eqI, simp_all add: word_size word_ops_nth_size nth_ucast |
| nth_shiftr nth_shiftl add.commute[where b=offs] test_bit_out_of_bounds) |
| done |
| |
| lemma serial_le16_helper: |
| "unat offs + 2 < length (\<alpha>wa (data\<^sub>f buf)) \<Longrightarrow> |
| [u16_to_u8 v, u16_to_u8 (v >> 8)] |
| = sle16 v" |
| apply (clarsimp simp: u16_to_u8_is_ucast sle16_def) |
| apply (subst word_rsplit_upt[where n=2]) |
| apply ((simp add: word_size upt_rec)+)[2] |
| apply (simp add: upt_rec) |
| done |
| |
| lemma serialise_le16_ret: |
| assumes no_overflow: "offs < offs + 2" |
| and valid_offs: |
| "unat offs + 2 < length (\<alpha>wa (data\<^sub>f buf))" |
| shows |
| "(serialise_le16 (buf, offs, v)) = |
| buf\<lparr>data\<^sub>f:=WordArrayT.make (buf_sub_slice buf offs (offs+2) (sle16 v))\<rparr>" |
| proof - |
| have unat_plus: |
| "\<And>n. n \<le> 2 \<longrightarrow> unat (offs + n) = unat offs + unat n" |
| using no_overflow valid_offs |
| by clarsimp unat_arith |
| show ?thesis |
| using valid_offs |
| apply (simp add: serialise_le16_def[unfolded sanitizers] serialise_u8_def[unfolded sanitizers] Let_def) |
| apply (handle_wa_mod "offs") |
| apply (handle_wa_mod "offs+1") |
| apply (simp add: serial_le16_helper[OF valid_offs, where v=v,symmetric]) |
| apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"]) |
| apply (rule ext) |
| apply (rule arg_cong[where f="WordArrayT.make"]) |
| |
| apply (simp add: buf_sub_slice_def) |
| apply (rule trans, rule_tac n="unat offs" in append_take_drop_id[symmetric], |
| rule arg_cong2[where f=append]) |
| apply (simp add: unat_plus order_le_less_trans[OF _ valid_offs] take_list_update) |
| apply (simp add: unat_plus) |
| apply (cut_tac valid_offs, simp) |
| apply (simp add: max_absorb1) |
| apply clarsimp |
| apply (simp add: list_eq_iff_nth_eq) |
| apply (rule conjI) |
| using valid_offs |
| apply (simp add: nth_Cons split: nat.split) |
| using valid_offs |
| apply (clarsimp simp only:) |
| apply (subst nth_list_update, unat_arith) + |
| apply clarsimp |
| apply (rule arg_cong[where f="nth (\<alpha>wa (data\<^sub>f buf))"]) |
| apply simp |
| done |
| qed |
| |
| lemma ple16_take: |
| assumes offs:"offs < offs+2" |
| assumes ntake:"unat (offs + 2) \<le> ntake" |
| shows "ple16 (take ntake ys) offs = ple16 ys offs" |
| apply (simp add: ple16_def) |
| apply (rule arg_cong[where f="word_rcat"]) |
| apply (rule arg_cong[where f="rev"]) |
| apply (subst list_eq_iff_nth_eq) |
| using offs ntake less_to_le[OF offs, simplified unat_plus_simple] |
| apply fastforce |
| done |
| |
| lemma ple16_append: |
| assumes no_overflow: "offs < offs + 2" |
| assumes len_ys: "unat (offs + 2) \<le> length ys" |
| shows "ple16 (ys@zs) offs = ple16 ys offs" |
| using plus_no_overflow_unat_lift[OF no_overflow] len_ys |
| by (simp add: ple16_def) |
| |
| lemma ple16_append_Cons: |
| assumes no_overflow: "offs < offs + 2" |
| assumes len_ys: "unat (offs + 2) \<le> length (v#ys)" |
| shows "ple16 (v#ys@zs) offs = ple16 (v#ys) offs" |
| proof - |
| have unat_nth_simp_Cons: "\<And> n xs ys . |
| unat n < Suc (length xs) \<Longrightarrow> (v#xs@ys)!(unat n) = (v#xs)!(unat n)" |
| by (case_tac "0 < unat n") (fastforce simp: nth_append) + |
| show ?thesis |
| apply(subgoal_tac "unat offs < Suc (length ys)") |
| apply(rule ple16_append[where ys = "v#ys" and zs = "zs" and offs="offs", |
| simplified List.append.append_Cons]) |
| using no_overflow apply clarsimp |
| using len_ys apply clarsimp |
| using assms by unat_arith |
| qed |
| |
| definition ple64 :: "8 word list \<Rightarrow> 32 word \<Rightarrow> 64 word" |
| where |
| "ple64 data offs \<equiv> word_rcat (rev (take 8 (drop (unat offs) data)))" |
| |
| definition ple32 :: "8 word list \<Rightarrow> 32 word \<Rightarrow> 32 word" |
| where |
| "ple32 data offs \<equiv> word_rcat (rev (take 4 (drop (unat offs) data)))" |
| |
| definition sle32 :: "U32 \<Rightarrow> U8 list" |
| where |
| "sle32 \<equiv> rev \<circ> word_rsplit" |
| |
| lemma deserialise_le32_ret: |
| assumes valid_offs: |
| "unat offs + 3 < length (\<alpha>wa $ data\<^sub>f buf)" |
| assumes no_ovf: |
| "offs < offs + 3" |
| shows |
| "deserialise_le32 (buf, offs) = (ple32 (\<alpha>wa $ data\<^sub>f buf) offs)" |
| using valid_offs |
| apply (subgoal_tac "(\<forall>i\<in>{0..3}. unat (offs+i) < length (\<alpha>wa (data\<^sub>f buf)))") |
| prefer 2 |
| apply unat_arith |
| apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"] ple32_def |
| deserialise_le32_def) |
| apply (subgoal_tac "\<forall>j\<in>{1..3}. (unat (offs + j) > 0)") |
| prefer 2 |
| apply clarsimp |
| apply (drule_tac x=j in bspec, simp) |
| using no_ovf apply unat_arith |
| apply auto[1] |
| apply (subst take_drop_decomp, (simp+))+ |
| apply (subst unatSuc[symmetric], (simp add: unat_gt_0[symmetric] add.commute[where b=offs]))+ |
| apply simp |
| apply (rule trans, rule word_rcat_rsplit[symmetric]) |
| apply (rule arg_cong[where f=word_rcat]) |
| apply (subst word_rsplit_upt[where n=4], simp add: word_size) |
| apply simp |
| apply (simp add: upt_rec shiftr_over_or_dist shiftl_shiftr1 shiftl_shiftr2 word_size) |
| apply (safe intro!: word_eqI, simp_all add: word_size word_ops_nth_size nth_ucast |
| nth_shiftr nth_shiftl add.commute[where b=offs] test_bit_out_of_bounds) |
| done |
| |
| |
| lemma serial_le32_helper: |
| "unat offs + 4 < length (\<alpha>wa (data\<^sub>f buf)) \<Longrightarrow> |
| [u32_to_u8 v, u32_to_u8 (v >> 8), u32_to_u8 (v >> 16), u32_to_u8 (v >> 24)] |
| = sle32 v" |
| apply (clarsimp simp: u32_to_u8_is_ucast sle32_def) |
| apply (subst word_rsplit_upt[where n=4]) |
| apply ((simp add: word_size upt_rec)+)[2] |
| apply (simp add: upt_rec) |
| done |
| |
| lemma serialise_le32_ret: |
| assumes no_overflow: "offs < offs + 4" |
| and valid_offs: |
| "unat offs + 4 < length (\<alpha>wa (data\<^sub>f buf))" |
| notes wa_modify_ret = wordarray_modify_ret[rotated - 1, simplified Let_def] |
| shows |
| "(serialise_le32 (buf, offs, v)) = |
| buf\<lparr>data\<^sub>f:=WordArrayT.make (buf_sub_slice buf offs (offs+4) (sle32 v))\<rparr>" |
| proof - |
| have unat_plus: |
| "\<And>n. n \<le> 4 \<longrightarrow> unat (offs + n) = unat offs + unat n" |
| using no_overflow valid_offs |
| by unat_arith auto |
| show ?thesis |
| using valid_offs |
| apply (simp add: serialise_le32_def[unfolded sanitizers] serialise_u8_def[unfolded sanitizers] Let_def) |
| apply (handle_wa_mod "offs") |
| apply (handle_wa_mod "offs+1") |
| apply (handle_wa_mod "offs+2") |
| apply (handle_wa_mod "offs+3") |
| apply (simp add: serial_le32_helper[OF valid_offs, where v=v,symmetric]) |
| apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"]) |
| apply (rule ext) |
| apply (rule arg_cong[where f="WordArrayT.make"]) |
| |
| apply (simp add: buf_sub_slice_def) |
| apply (rule trans, rule_tac n="unat offs" in append_take_drop_id[symmetric], |
| rule arg_cong2[where f=append]) |
| apply (simp add: unat_plus order_le_less_trans[OF _ valid_offs] take_list_update) |
| apply (simp add: unat_plus) |
| apply (cut_tac valid_offs, simp) |
| apply (simp add: max_absorb1) |
| apply (simp add: list_eq_iff_nth_eq) |
| apply (rule conjI) |
| using valid_offs |
| apply (simp add: nth_Cons split: nat.split) |
| using valid_offs |
| apply (clarsimp simp only:) |
| apply (subst nth_list_update, unat_arith) + |
| apply force |
| done |
| qed |
| |
| lemma ple32_take: |
| assumes offs:"offs < offs+4" |
| assumes ntake:"unat (offs + 4) \<le> ntake" |
| shows "ple32 (take ntake ys) offs = ple32 ys offs" |
| apply (simp add: ple32_def) |
| apply (rule arg_cong[where f="word_rcat"]) |
| apply (rule arg_cong[where f="rev"]) |
| apply (subst list_eq_iff_nth_eq) |
| using offs ntake less_to_le[OF offs, simplified unat_plus_simple] |
| apply fastforce |
| done |
| |
| lemma plus4_offs_ntake: |
| fixes offs ::U32 |
| assumes "unat (offs + 4) \<le> ntake" |
| assumes offs_overflow: " (offs) < ((offs+4))" |
| assumes "n \<in> {0,1,2,3}" |
| shows "unat (offs+n) < ntake" |
| using assms apply (clarsimp) |
| apply (erule disjE, unat_arith, fastforce?)+ |
| apply simp |
| apply unat_arith |
| done |
| |
| lemma ple32_append: |
| assumes no_overflow: "offs < offs+4" |
| assumes len_ys: "unat (offs + 4) \<le> length ys" |
| shows "ple32 (ys@zs) offs = ple32 ys offs" |
| using plus_no_overflow_unat_lift[OF no_overflow] len_ys |
| by (simp add: ple32_def) |
| |
| lemma ple32_append_Cons: |
| assumes no_overflow: "offs < offs+4" |
| assumes len_ys: "unat (offs + 4) \<le> length (v#ys)" |
| shows "ple32 (v#ys@zs) offs = ple32 (v#ys) offs" |
| proof - |
| have unat_nth_simp_Cons: "\<And> n xs ys . |
| unat n < Suc (length xs) \<Longrightarrow> (v#xs@ys)!(unat n) = (v#xs)!(unat n)" |
| by (case_tac "0 < unat n") (fastforce simp: nth_append) + |
| show ?thesis |
| apply(subgoal_tac "unat offs < Suc (length ys)") |
| apply(rule ple32_append[where ys = "v#ys" and zs = "zs" and offs="offs", simplified List.append.append_Cons]) |
| using no_overflow apply clarsimp |
| using len_ys apply clarsimp |
| using assms by unat_arith |
| qed |
| |
| |
| definition sle64 :: "U64 \<Rightarrow> U8 list" |
| where |
| "sle64 \<equiv> rev \<circ> word_rsplit" |
| |
| lemma deserialise_le64_ret: |
| assumes valid_offs: |
| "unat offs + 8 \<le> length (\<alpha>wa $ data\<^sub>f buf)" |
| assumes no_ovf: |
| "offs \<le> offs + 8" |
| shows |
| "deserialise_le64 (buf, offs) = (ple64 (\<alpha>wa $ data\<^sub>f buf) offs)" |
| using valid_offs |
| apply (subgoal_tac "(\<forall>i\<in>{0..7}. unat (offs+i) < length (\<alpha>wa (data\<^sub>f buf)))") |
| prefer 2 |
| apply unat_arith |
| apply (clarsimp simp: wordarray_get_ret[where arr="data\<^sub>f buf"] ple64_def |
| deserialise_le64_def) |
| apply (subgoal_tac "\<forall>j\<in>{1..7}. (unat (offs + j) > 0)") |
| prefer 2 |
| apply clarsimp |
| apply (drule_tac x=j in bspec, simp) |
| using no_ovf apply unat_arith |
| apply auto[1] |
| apply (subst take_drop_decomp, (simp+))+ |
| apply (subst unatSuc[symmetric], (simp add: unat_gt_0[symmetric] add.commute[where b=offs])[1])+ |
| apply simp |
| apply (rule trans, rule word_rcat_rsplit[symmetric]) |
| apply (rule arg_cong[where f=word_rcat]) |
| apply (subst word_rsplit_upt[where n=8], simp add: word_size) |
| apply simp |
| apply (simp add: upt_rec shiftr_over_or_dist shiftl_shiftr1 shiftl_shiftr2 word_size) |
| apply (safe intro!: word_eqI, simp_all add: word_size word_ops_nth_size nth_ucast |
| nth_shiftr nth_shiftl add.commute[where b=offs] test_bit_out_of_bounds) |
| done |
| |
| lemma serial_le64_helper: |
| "unat offs + 8 < length (\<alpha>wa (data\<^sub>f buf)) \<Longrightarrow> |
| [u64_to_u8 v, u64_to_u8 (v >> 8), u64_to_u8 (v >> 16), u64_to_u8 (v >> 24), |
| u64_to_u8 (v >> 32), u64_to_u8 (v >> 40), u64_to_u8 (v >> 48), u64_to_u8 (v >> 56)] |
| = sle64 v" |
| apply (clarsimp simp: u64_to_u8_is_ucast sle64_def) |
| apply (subst word_rsplit_upt[where n=8]) |
| apply ((simp add: word_size upt_rec)+)[2] |
| apply (simp add: upt_rec) |
| done |
| |
| lemma serialise_le64_ret: |
| assumes no_overflow: "offs < offs + 8" |
| and valid_offs: |
| "unat offs + 8 < length (\<alpha>wa (data\<^sub>f buf))" |
| shows |
| "(serialise_le64 (buf, offs, v)) = |
| buf\<lparr>data\<^sub>f:=WordArrayT.make (buf_sub_slice buf offs (offs+8) (sle64 v))\<rparr>" |
| proof - |
| have unat_plus: |
| "\<And>n. n \<le> 8 \<longrightarrow> unat (offs + n) = unat offs + unat n" |
| using no_overflow valid_offs |
| by unat_arith auto |
| show ?thesis |
| |
| apply (simp add: serialise_le64_def[unfolded sanitizers] serialise_u8_def[unfolded sanitizers] Let_def) |
| using valid_offs apply - |
| apply (handle_wa_mod "offs") |
| apply (handle_wa_mod "offs+1") |
| apply (handle_wa_mod "offs+2") |
| apply (handle_wa_mod "offs+3") |
| apply (handle_wa_mod "offs+4") |
| apply (handle_wa_mod "offs+5") |
| apply (handle_wa_mod "offs+6") |
| apply (handle_wa_mod "offs+7") |
| apply (simp add: serial_le64_helper[OF valid_offs, where v=v,symmetric]) |
| apply (rule arg_cong[where f="\<lambda>v. Buffer.data\<^sub>f_update v buf"]) |
| apply (rule ext) |
| apply (rule arg_cong[where f="WordArrayT.make"]) |
| |
| apply (simp add: buf_sub_slice_def) |
| apply (rule trans, rule_tac n="unat offs" in append_take_drop_id[symmetric], |
| rule arg_cong2[where f=append]) |
| apply (simp add: unat_plus order_le_less_trans[OF _ valid_offs] take_list_update) |
| apply (simp add: unat_plus) |
| apply (cut_tac valid_offs, simp) |
| apply (simp add: max_absorb1) |
| apply (simp add: list_eq_iff_nth_eq) |
| apply (rule conjI) |
| using valid_offs |
| apply (simp add: nth_Cons split: nat.split) |
| using valid_offs |
| apply (clarsimp simp only:) |
| apply (subst nth_list_update, unat_arith) + |
| apply force |
| done |
| qed |
| |
| lemma ple64_take: |
| assumes offs:"offs < offs+8" |
| assumes ntake:"unat (offs + 8) \<le> ntake" |
| shows "ple64 (take ntake ys) offs = ple64 ys offs" |
| apply (simp add: ple64_def) |
| apply (rule arg_cong[where f="word_rcat"]) |
| apply (rule arg_cong[where f="rev"]) |
| apply (subst list_eq_iff_nth_eq) |
| using offs ntake less_to_le[OF offs, simplified unat_plus_simple] |
| apply fastforce |
| done |
| |
| lemma ple64_append: |
| assumes no_overflow: "offs < offs + 8" |
| assumes len_ys: "unat (offs + 8) \<le> length ys" |
| shows "ple64 (ys@zs) offs = ple64 ys offs" |
| using plus_no_overflow_unat_lift[OF no_overflow] len_ys |
| by (simp add: ple64_def) |
| |
| lemma ple64_append_Cons: |
| assumes no_overflow: "offs < offs + 8" |
| assumes len_ys: "unat (offs + 8) \<le> length (v#ys)" |
| shows "ple64 (v#ys@zs) offs = ple64 (v#ys) offs" |
| proof - |
| have unat_nth_simp_Cons: "\<And> n xs ys . |
| unat n < Suc (length xs) \<Longrightarrow> (v#xs@ys)!(unat n) = (v#xs)!(unat n)" |
| by (case_tac "0 < unat n") (fastforce simp: nth_append) + |
| show ?thesis |
| apply(subgoal_tac "unat offs < Suc (length ys)") |
| apply(rule ple64_append[where ys = "v#ys" and zs = "zs" and offs="offs", simplified List.append.append_Cons]) |
| using no_overflow apply clarsimp |
| using len_ys apply clarsimp |
| using assms by unat_arith |
| qed |
| end |
