| (* |
| * 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 TransS |
| imports |
| "../impl/BilbyFs_Shallow_Desugar_Tuples" |
| "../impl/BilbyFs_ShallowConsts_Desugar_Tuples" |
| "../spec/OstoreInvS" |
| begin |
| |
| lemma pTrans_remainder: |
| "prod.fst (pTrans buf) = drop (trans_len buf) buf" |
| apply (induct buf rule:trans_len.induct) |
| apply simp |
| apply (rename_tac v va) |
| apply (case_tac "trans\<^sub>f (pObj (v # va) 0) = bilbyFsTransIn") |
| apply (clarsimp simp: Let_def is_valid_ObjTrans) |
| apply (rule conjI) |
| apply (fastforce simp: trans_len_Cons bilbyFsObjHeaderSize_def ) |
| apply (clarsimp simp: trans_len_Cons drop_n_ge_0 prod.case_eq_if) |
| apply (rule_tac f="\<lambda>a. drop a (v#va)" in arg_cong, fastforce) |
| apply (fastforce simp: Let_def trans_len_Cons bilbyFsObjHeaderSize_def is_valid_ObjTrans) |
| done |
| |
| lemma list_trans_not_Nil_Nil: |
| "xs \<noteq> [] \<Longrightarrow> |
| list_trans xs \<noteq> ([],[])" |
| by (simp split: list.splits prod.splits) |
| |
| lemma prefix_n_takeD: |
| "prefix xs ys \<Longrightarrow> |
| n \<le> length xs \<Longrightarrow> |
| take n ys = take n xs" |
| by (auto simp: prefix_def) |
| |
| 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 take_length_eq: |
| "\<lbrakk>take n xs = take n ys; length xs \<ge> n\<rbrakk> \<Longrightarrow> length ys \<ge> n" |
| by (fastforce dest!: arg_cong[where f=length]) |
| |
| lemma take_drop_eq_bounded: |
| "\<lbrakk>take n xs = take n ys; j + k < n\<rbrakk> |
| \<Longrightarrow> take j (drop k xs) = take j (drop k ys)" |
| apply (case_tac "length xs \<ge> n") |
| apply (subgoal_tac "length ys \<ge> n") |
| prefer 2 |
| apply (erule (1) take_length_eq) |
| apply (rule nth_equalityI) |
| apply simp |
| apply clarsimp |
| apply (simp add: take_n_eq_simp[where xs=ys]) |
| apply (simp add: not_less_eq_eq) |
| done |
| |
| lemma pObjI: |
| "P(pObj ys 0) \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj xs 0)) \<Longrightarrow> |
| take (unat (Obj.len\<^sub>f (pObj xs 0))) xs = take (unat (Obj.len\<^sub>f (pObj xs 0))) ys \<Longrightarrow> |
| P(pObj xs 0)" |
| apply (erule subst[where P=P,rotated]) |
| apply (simp add: pObj_def pObjHeader_simp) |
| apply (subgoal_tac "\<forall>n<bilbyFsObjHeaderSize - 4. ple32 ys n = ple32 xs n") |
| apply (subgoal_tac "\<forall>n<bilbyFsObjHeaderSize - 8. ple64 ys n = ple64 xs n") |
| apply (simp add: pObj_def pObjHeader_simp |
| take_n_and_len'_eq_simp[where xs=ys and ys=xs and len'="unat bilbyFsObjHeaderSize"]) |
| |
| apply (clarsimp simp: ple64_def bilbyFsObjHeaderSize_def) |
| apply (subst take_drop_eq_bounded[where xs=xs and ys=ys and n="unat (ple32 xs 0x10)"]) |
| apply ((simp | unat_arith)+)[3] |
| apply clarsimp |
| apply (subst ple32_def)+ |
| apply (clarsimp simp: bilbyFsObjHeaderSize_def) |
| apply (subst take_drop_eq_bounded[where xs=xs and ys=ys and n="unat (ple32 xs 0x10)"]) |
| apply ((simp | unat_arith)+) |
| done |
| |
| lemma pObjD: |
| "take (unat (Obj.len\<^sub>f (pObj xs 0))) ys = take (unat (Obj.len\<^sub>f (pObj xs 0))) xs \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj xs 0)) \<Longrightarrow> |
| pObj ys 0 = pObj xs 0" |
| by (auto intro: pObjI) |
| |
| lemma length_bilbyFsObjHeaderSize_le_trans: |
| "unat len \<le> length xs \<Longrightarrow> |
| length xs \<le> length ys \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> length ys \<Longrightarrow> |
| bilbyFsObjHeaderSize \<le> len \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> length xs" |
| by unat_arith |
| |
| lemma is_valid_ObjHeader_prefix_eq: |
| "prefix xs ys \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj xs 0)) \<le> length xs \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj xs 0)) \<Longrightarrow> |
| is_valid_ObjHeader (pObj ys 0) ys = is_valid_ObjHeader (pObj xs 0) xs" |
| apply (frule (1) prefix_n_takeD[where n="unat (Obj.len\<^sub>f (pObj xs 0))"]) |
| apply (drule (1) pObjD) |
| apply (frule prefix_n_takeD[where n="length xs" and xs=xs and ys=ys], fastforce) |
| apply (subgoal_tac "take (unat $ Obj.len\<^sub>f $ pObj xs 0) xs = take (unat $ Obj.len\<^sub>f $ pObj xs 0) ys") |
| prefer 2 |
| apply (drule (1) prefix_n_takeD, fastforce) |
| apply (frule prefix_length_le) |
| apply (auto simp: is_valid_ObjHeader_def length_bilbyFsObjHeaderSize_le_trans) |
| done |
| |
| lemma is_valid_ObjHeader_prefix: |
| "is_valid_ObjHeader (pObj xs 0) xs \<Longrightarrow> |
| prefix xs ys \<Longrightarrow> |
| is_valid_ObjHeader (pObj ys 0) ys" |
| apply (frule is_valid_ObjHeader_buf_len) |
| apply (frule is_valid_ObjHeader_len) |
| apply (drule is_valid_ObjHeader_prefix_eq) |
| apply (clarsimp , unat_arith?)+ |
| done |
| |
| lemma is_valid_ObjHeader_prefix_rev: |
| "is_valid_ObjHeader (pObj ys 0) ys \<Longrightarrow> |
| prefix xs ys \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj xs 0)) \<le> length xs \<Longrightarrow> |
| unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj xs 0)) \<Longrightarrow> |
| is_valid_ObjHeader (pObj xs 0) xs" |
| by (drule is_valid_ObjHeader_prefix_eq, auto) |
| |
| lemma is_valid_ObjHeader_data_len: |
| "is_valid_ObjHeader (pObj xs n) (take nb ys) \<Longrightarrow> |
| is_valid_ObjHeader (pObj xs n) ys" |
| by (clarsimp simp: is_valid_ObjHeader_def) |
| |
| lemma is_valid_ObjHeader_trans_len: |
| "is_valid_ObjHeader (pObj xs 0) xs \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj xs 0)) \<le> trans_len xs" |
| by (case_tac "xs") |
| (clarsimp split:if_splits simp: trans_len_Cons)+ |
| |
| lemma valid_trans_valid_ObjHeaderD: |
| "valid_trans ys \<Longrightarrow> is_valid_ObjHeader (pObj ys 0) ys" |
| apply (erule valid_trans.elims) |
| apply (clarsimp split:if_splits simp: is_valid_ObjTrans) |
| done |
| |
| lemma valid_trans_pObj_trans_len: |
| "valid_trans xs \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj xs 0)) \<le> trans_len xs" |
| apply (case_tac "xs") |
| apply (simp) |
| apply (erule valid_trans.elims) |
| apply (clarsimp split:if_splits) |
| done |
| |
| lemma valid_trans_pObj_take_trans_len: |
| "valid_trans (take (trans_len ys) ys) \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj (take (trans_len ys) ys) 0)) \<le> trans_len ys" |
| apply (case_tac "(take (trans_len ys) ys)") |
| apply (clarsimp) |
| apply (erule valid_trans.elims) |
| apply (clarsimp simp:is_valid_ObjTrans split:if_splits ) |
| apply (drule sym, simp only:) |
| apply (drule is_valid_ObjHeader_buf_len) |
| apply simp |
| apply (drule sym, simp only:) |
| apply (drule is_valid_ObjHeader_buf_len) |
| apply simp |
| done |
| |
| lemma valid_trans_take_trans_len_valid_ObjHeaderD: |
| assumes "valid_trans (take (trans_len ys) ys)" |
| shows "is_valid_ObjHeader (pObj ys 0) ys" |
| proof - |
| have tl_take_bound: "unat (Obj.len\<^sub>f (pObj (take (trans_len ys) ys) 0)) \<le> trans_len ys" |
| by (rule valid_trans_pObj_take_trans_len[OF assms]) |
| have "unat bilbyFsObjHeaderSize \<le> length (take (trans_len ys) ys)" |
| using is_valid_ObjHeader_len_facts[OF valid_trans_valid_ObjHeaderD[OF assms]] |
| by (clarsimp simp: is_valid_ObjHeader_def) |
| moreover have "length (take (trans_len ys) ys) \<le> length ys" |
| by simp |
| ultimately have len_eq: "Obj.len\<^sub>f (pObj ys 0) = (Obj.len\<^sub>f (pObj (take (trans_len ys) ys) 0))" |
| by (clarsimp simp: pObj_def pObjHeader_def Let_def Obj.make_def bilbyFsObjHeaderSize_def ple32_take) |
| from tl_take_bound and len_eq |
| have tl_bound: "unat (Obj.len\<^sub>f (pObj ys 0)) \<le> trans_len ys" |
| by simp |
| |
| have valid: "is_valid_ObjHeader (pObj (take (trans_len ys) ys) 0) (take (trans_len ys) ys)" |
| by (rule valid_trans_valid_ObjHeaderD[OF assms]) |
| |
| have len_lower_bound: "unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj ys 0))" |
| using len_eq[symmetric] is_valid_ObjHeader_len[OF valid] by simp unat_arith |
| |
| show ?thesis |
| using tl_bound valid len_eq |
| by - (rule pObjI[where ys="(take (trans_len ys) ys)", OF _ len_lower_bound], simp_all add: is_valid_ObjHeader_def min_absorb1) |
| qed |
| |
| |
| lemma valid_log_buf_fun_imp_valid_ObjHeader: |
| "valid_list_trans ys \<Longrightarrow> is_valid_ObjHeader (pObj ys 0) ys" |
| apply (erule valid_list_trans.elims) |
| apply (clarsimp simp: is_valid_ObjTrans) |
| apply (drule sym[where s=ys], simp) |
| apply (erule valid_trans.elims) |
| apply (rename_tac v va) |
| apply (subgoal_tac "is_valid_ObjHeader (pObj (v#va) 0) (v#va)") |
| apply (erule is_valid_ObjHeader_prefix) |
| apply (drule_tac t="v # va" in sym, fastforce) |
| apply (fastforce simp: is_valid_ObjTrans split: if_splits dest: is_valid_ObjHeader_buf_len)+ |
| done |
| |
| lemma n_idx_in_range: |
| "n < length xs \<Longrightarrow> (xs @ ys) ! n = xs ! n" |
| by (metis nth_append) |
| |
| lemma is_down_32_8[simp]: |
| "is_down (c::(U32 \<Rightarrow> U8))" |
| by (simp add: is_down_def word_size target_size source_size) |
| |
| lemma u32_to_u8_ignored[simp]: |
| "u32_to_u8 (ucast x) = x" |
| by (simp add: u32_to_u8_is_ucast ucast_down_ucast_id) |
| |
| lemma word_rcat_8_32_ucast_last: |
| "list \<noteq> [] \<Longrightarrow> ucast (word_rcat list :: word32) = (last list :: word8)" |
| apply (cases list rule: rev_cases, simp_all) |
| apply (rule word_eqI) |
| apply (simp add: word_size test_bit_rcat[OF _ refl] nth_ucast) |
| done |
| |
| lemma is_valid_ObjHeader_first_byte: |
| assumes "is_valid_ObjHeader (pObj data 0) data" |
| shows |
| "hd data = u32_to_u8 bilbyFsMagic" |
| proof - |
| have len_data: "length data > 4" |
| using is_valid_ObjHeader_len_facts[OF assms] |
| by (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def) |
| have "magic\<^sub>f (pObj data 0) = bilbyFsMagic" |
| using assms unfolding is_valid_ObjHeader_def by simp |
| hence "ple32 data 0 = bilbyFsMagic" |
| by (simp add: pObj_def pObjHeader_def Let_def Obj.make_def) |
| hence "u32_to_u8 (ple32 data 0) = u32_to_u8 bilbyFsMagic" |
| by (simp) |
| thus ?thesis |
| using len_data |
| by (case_tac data) |
| (clarsimp simp: ple32_def u32_to_u8_is_ucast word_rcat_8_32_ucast_last)+ |
| qed |
| |
| lemma is_valid_ObjHeader_not_pad: |
| "is_valid_ObjHeader (pObj data 0) data \<Longrightarrow> hd data \<noteq> bilbyFsPadByte" |
| by (drule is_valid_ObjHeader_first_byte) |
| (simp add: bilbyFsMagic_def bilbyFsPadByte_def u32_to_u8_is_ucast) |
| |
| lemma valid_list_trans_non_empty: |
| "valid_list_trans ys \<Longrightarrow> ys \<noteq> []" |
| by (erule valid_list_trans.elims, simp_all) |
| |
| lemma nopad_not_Nil: |
| "nopad xs \<noteq> [] \<Longrightarrow> xs \<noteq> []" |
| by (case_tac xs) (simp_all add: nopad_def) |
| |
| lemma valid_trans_imp_valid_trans_trans_len: |
| "valid_trans xs \<Longrightarrow> trans_len xs \<le> length xs" |
| apply (induct xs rule: trans_len.induct) |
| apply (simp) |
| apply (erule valid_trans.elims) |
| apply (clarsimp split: if_splits simp add: is_valid_ObjTrans) |
| apply (rename_tac v vs) |
| apply (subgoal_tac "Suc (length vs) \<ge> unat (Obj.len\<^sub>f (pObj (v#vs) 0))") |
| apply (fastforce simp: is_valid_ObjHeader_def)+ |
| done |
| |
| lemma validObjIn_imp_validObjHeader: |
| "is_valid_ObjIn obj buf \<Longrightarrow> is_valid_ObjHeader obj buf" |
| by (simp add: is_valid_ObjTrans) |
| |
| lemma trans_len_induct: |
| "P [] \<Longrightarrow> |
| (\<And>v vs. (is_valid_ObjIn (pObj (v#vs) 0) (v#vs) \<Longrightarrow> |
| P (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs))) \<Longrightarrow> |
| P (v#vs)) \<Longrightarrow> P a0" |
| by (erule trans_len.induct) |
| (fastforce intro: validObjIn_imp_validObjHeader) |
| |
| lemma not_is_valid_ObjHeader_trans_len: |
| "\<not>is_valid_ObjHeader (pObj xs 0) xs \<Longrightarrow> trans_len xs = max (unat bilbyFsObjHeaderSize) (unat (Obj.len\<^sub>f (pObj xs 0)))" |
| by (case_tac xs, simp_all add: trans_len_Cons) |
| |
| lemma trans_len_idempotence: |
| notes notI [rule del] |
| shows |
| "trans_len (take (trans_len xs) xs) = trans_len xs" |
| proof (induction xs rule: trans_len_induct) |
| show "trans_len (take (trans_len []) []) = trans_len []" |
| by simp |
| next |
| fix v vs |
| assume IH: "is_valid_ObjIn (pObj (v#vs) 0) (v#vs) \<Longrightarrow> |
| trans_len (take (trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))) |
| (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v # vs))) = |
| trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))" |
| have hdr_sz_le_tl: "unat bilbyFsObjHeaderSize \<le> trans_len (v#vs)" |
| using hdr_sz_le_trans_len[where xs="v#vs"] . |
| hence hdr_eq: "pObjHeader (take (trans_len (v#vs)) (v#vs)) 0 = pObjHeader (v#vs) 0" |
| by (simp add: pObjHeader_simp ple32_take ple64_take) |
| have len_eq: "unat (Obj.len\<^sub>f (pObj (take (trans_len (v # vs)) (v # vs)) 0)) = unat (Obj.len\<^sub>f (pObj (v # vs) 0))" |
| using hdr_sz_le_trans_len[where xs="v#vs"] ple32_take[where ys="v#vs"] |
| by (simp add: pObjHeader_simp pObj_def) |
| have trans_otype_eq: "\<And>f. f \<in> {Obj.trans\<^sub>f, Obj.otype\<^sub>f} \<Longrightarrow> (f (pObj (take (trans_len (v # vs)) (v # vs)) 0)) = f (pObj (v # vs) 0)" |
| using hdr_sz_le_trans_len[where xs="v#vs"] |
| by (fastforce simp: pObjHeader_simp pObj_def) |
| have magic_eq: "\<And>f. f \<in> {Obj.magic\<^sub>f, Obj.offs\<^sub>f} \<Longrightarrow> (f (pObj (take (trans_len (v # vs)) (v # vs)) 0)) = f (pObj (v # vs) 0)" |
| using hdr_sz_le_trans_len[where xs="v#vs"] ple32_take[where ys="v#vs"] |
| by (fastforce simp: pObjHeader_simp pObj_def) |
| show "trans_len (take (trans_len (v#vs)) (v#vs)) = trans_len (v#vs)" |
| proof (cases) |
| assume valid_in: "is_valid_ObjIn (pObj (v#vs) 0) (v#vs)" |
| hence valid_hdr: "is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| by (simp add: is_valid_ObjTrans) |
| have valid_in': "is_valid_ObjIn (pObj (take (trans_len (v#vs)) (v#vs)) 0) (take (trans_len (v#vs)) (v#vs))" |
| using hdr_eq hdr_sz_le_trans_len[where xs="v#vs"] hdr_sz_le_tl valid_in |
| by (simp add: is_valid_ObjTrans is_valid_ObjHeader_def pObj_def Obj.make_def Let_def |
| ple32_take[where ys="v#vs"] ple64_take[where ys="v#vs"] pObjHeader_def |
| bilbyFsObjHeaderSize_def min_absorb1) (* this takes ages *) |
| let ?olen = "unat (Obj.len\<^sub>f (pObj (v # vs) 0))" |
| let ?dropolen = "drop ?olen (v # vs)" |
| |
| have tl: "trans_len (v#vs) = ?olen + trans_len ?dropolen" |
| using valid_in trans_len_Cons by (simp add: is_valid_ObjTrans) |
| |
| have tl': "trans_len (take (trans_len (v # vs)) (v # vs)) = (unat $ Obj.len\<^sub>f $ pObj (take (trans_len (v # vs)) (v # vs)) 0) + |
| trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (take (trans_len (v # vs)) (v # vs)) 0) (take (trans_len (v # vs)) (v # vs)))" |
| using valid_in' trans_len_Cons by (simp add: is_valid_ObjTrans) |
| |
| have olen_assoc: "?olen + trans_len ?dropolen = trans_len ?dropolen + ?olen" |
| by simp |
| |
| have tl_plus_eq: "trans_len (drop ?olen (take (?olen + trans_len ?dropolen) (v # vs))) = |
| trans_len (take (trans_len ?dropolen) ?dropolen)" |
| by (rule arg_cong[where f="trans_len"]) (simp add: take_drop olen_assoc) |
| |
| have "?olen + trans_len ?dropolen = (unat $ Obj.len\<^sub>f $ pObj (take (trans_len (v # vs)) (v # vs)) 0) + |
| trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (take (trans_len (v # vs)) (v # vs)) 0) |
| (take (trans_len (v # vs)) (v # vs)))" |
| using len_eq IH[OF valid_in,simplified] tl_plus_eq |
| by (simp add: len_eq valid_in valid_hdr trans_len_Cons) |
| thus ?thesis |
| by (simp add: tl[symmetric] tl') |
| next |
| assume not_in: "\<not>is_valid_ObjIn (pObj (v#vs) 0) (v#vs)" |
| thus ?thesis |
| proof (cases) |
| assume valid: "is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| |
| have valid': "is_valid_ObjHeader (pObj (take (trans_len (v#vs)) (v#vs)) 0) (take (trans_len (v#vs)) (v#vs))" |
| using hdr_eq len_eq hdr_sz_le_trans_len[where xs="v#vs"] valid apply (simp only: is_valid_ObjTrans is_valid_ObjHeader_def pObj_def Obj.make_def Let_def |
| pObjHeader_def ) |
| using is_valid_ObjHeader_trans_len[OF valid, simplified pObjHeader_simp pObj_def] |
| by (simp add: ple32_take[where ys="v#vs"] ple64_take[where ys="v#vs"] bilbyFsObjHeaderSize_def |
| min_absorb1) |
| hence not_in': "\<not>is_valid_ObjIn (pObj (take (trans_len (v#vs)) (v#vs)) 0) (take (trans_len (v#vs)) (v#vs))" |
| using valid' valid not_in apply (simp add: is_valid_ObjTrans) |
| apply (drule is_valid_ObjHeader_buf_len)+ |
| apply (simp only: pObjHeader_simp pObj_def) |
| apply clarsimp |
| done |
| thus ?thesis |
| using valid valid' not_in not_in' apply (simp add: trans_len_Cons) |
| apply (case_tac "take (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs)", fastforce) |
| using len_eq apply (clarsimp simp: trans_len_Cons bilbyFsObjHeaderSize_def) |
| done |
| next |
| assume not_valid: "\<not>is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| hence not_valid': "\<not>is_valid_ObjHeader (pObj (take (trans_len (v#vs)) (v#vs)) 0) (take (trans_len (v#vs)) (v#vs))" |
| using len_eq |
| by (fastforce simp: is_valid_ObjHeader_def magic_eq trans_otype_eq)+ |
| |
| have "unat (Obj.len\<^sub>f |
| (pObj (take (max (unat bilbyFsObjHeaderSize) (unat (Obj.len\<^sub>f (pObj (v # vs) 0)))) |
| (v # vs)) |
| 0)) = (unat (Obj.len\<^sub>f (pObj (v # vs) 0)))" |
| using ple32_take[where ys="(v # vs)" and ntake="(max (unat bilbyFsObjHeaderSize) (unat (Obj.len\<^sub>f (pObj (v # vs) 0))))"] |
| by (simp add: pObj_def pObjHeader_simp) |
| thus ?thesis |
| apply (simp add: trans_len_Cons) |
| using not_valid and not_valid' apply simp |
| apply (case_tac "(take (max (unat bilbyFsObjHeaderSize) (unat (Obj.len\<^sub>f (pObj (v # vs) 0)))) (v # vs))") |
| apply (simp add: bilbyFsObjHeaderSize_def) |
| apply (simp add: trans_len_Cons) |
| done |
| qed |
| qed |
| qed |
| |
| lemma trans_len_take_drop_eq: |
| assumes is_in:"is_valid_ObjIn (pObj (v # vs) 0) (v # vs)" |
| and valid_trans: "valid_trans (v#vs)" |
| shows |
| "take (trans_len (drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs))) |
| (drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs)) = |
| drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (take (trans_len (v # vs)) (v # vs))" |
| proof - |
| have "valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))" |
| using valid_trans is_in by - (erule valid_trans.elims, fastforce) |
| let ?lenobj = "unat (Obj.len\<^sub>f (pObj (v # vs) 0))" |
| have "trans_len (drop ?lenobj (v#vs)) + ?lenobj = trans_len (v#vs)" |
| using is_in by (subst trans_len.simps) (clarsimp simp: is_valid_ObjTrans) |
| thus ?thesis |
| by (simp add: take_drop) |
| qed |
| |
| |
| lemma trans_len_take_drop_eq': |
| assumes yys_eq: "y#ys = take (trans_len (v#vs)) (v#vs)" |
| and is_in': "is_valid_ObjIn (pObj (v#vs) 0) (v#vs)" |
| and len_eq: "(unat (Obj.len\<^sub>f (pObj (y#ys) 0))) = (unat (Obj.len\<^sub>f (pObj (v#vs) 0)))" |
| shows |
| "take (trans_len (drop (unat (Obj.len\<^sub>f (pObj (v#vs) 0))) (v#vs))) |
| (drop (unat (Obj.len\<^sub>f (pObj (v#vs) 0))) (v#vs)) = |
| drop (unat (Obj.len\<^sub>f (pObj (v#vs) 0))) (y#ys)" |
| apply (simp add: yys_eq) |
| apply (subst trans_len_Cons) |
| using is_in' apply (clarsimp simp: is_valid_ObjTrans) |
| apply (simp add: take_drop len_eq[simplified yys_eq]) |
| apply (case_tac "(drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs))") |
| apply simp |
| apply (rename_tac x xs) |
| apply (drule_tac t="x#xs" in sym) |
| apply (subgoal_tac "(trans_len (drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs)) + |
| unat (Obj.len\<^sub>f (pObj (v # vs) 0))) = ( unat (Obj.len\<^sub>f (pObj (v # vs) 0)) + |
| trans_len (drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs)))") |
| apply (simp only:)+ |
| done |
| |
| lemma take_trans_len_is_valid_ObjHeader_preserved: |
| assumes hdr: "is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| and trans: "Obj.trans\<^sub>f (pObj (v#vs) 0) = tr" |
| and valid: "valid_trans (v # vs)" |
| and yys_eq:"take (trans_len (v#vs)) (v#vs) = y#ys" |
| shows |
| "is_valid_ObjHeader (pObj (y#ys) 0) (y#ys) \<and> |
| Obj.trans\<^sub>f (pObj (y#ys) 0) = tr \<and> |
| unat (Obj.len\<^sub>f (pObj (y#ys) 0)) = unat (Obj.len\<^sub>f (pObj (v#vs) 0))" |
| proof - |
| have prefix: "prefix (y#ys) (v#vs)" |
| using yys_eq by (metis take_is_prefix) |
| have len_eq: "unat (Obj.len\<^sub>f (pObj (y#ys) 0)) = unat (Obj.len\<^sub>f (pObj (v#vs) 0))" |
| using hdr_sz_le_trans_len[where xs="v#vs"] |
| by (simp only: yys_eq[symmetric] bilbyFsObjHeaderSize_def |
| pObj_def pObjHeader_def Obj.make_def Let_def ple32_take) |
| (simp add: ple32_take) |
| moreover hence len_obj: "unat (Obj.len\<^sub>f (pObj (y#ys) 0)) \<le> length (y#ys)" |
| using yys_eq[symmetric] is_valid_ObjHeader_buf_len[OF hdr] is_valid_ObjHeader_trans_len[OF hdr] |
| by clarsimp |
| have lower_bound: "unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj (y#ys) 0))" |
| using is_valid_ObjHeader_len[OF hdr] len_eq by unat_arith |
| have hdr_yys: "is_valid_ObjHeader (pObj (y # ys) 0) (y # ys)" |
| using is_valid_ObjHeader_prefix_rev[OF hdr prefix len_obj lower_bound] . |
| moreover have "unat bilbyFsObjHeaderSize \<le> length (y#ys)" |
| using is_valid_ObjHeader_buf_len[OF hdr_yys] by clarsimp |
| hence "Obj.trans\<^sub>f (pObj (y#ys) 0) = Obj.trans\<^sub>f (pObj (v#vs) 0)" |
| by (simp only: yys_eq[symmetric] bilbyFsObjHeaderSize_def |
| pObj_def pObjHeader_def Obj.make_def Let_def ple32_def) |
| simp |
| ultimately show "?thesis" |
| using trans by simp |
| qed |
| |
| lemma valid_trans_imp_valid_trans_take_trans_len: |
| assumes valid: "valid_trans xs" |
| shows |
| "valid_trans (take (trans_len xs) xs)" |
| using valid_trans_imp_valid_trans_trans_len[OF valid] valid |
| proof (induction xs rule: trans_len_induct) |
| assume "valid_trans []" |
| hence False by simp |
| thus "valid_trans (take (trans_len []) [])" by simp |
| next |
| fix v vs |
| assume valid: "valid_trans (v # vs)" |
| and tllen: "trans_len (v # vs) \<le> length (v # vs)" |
| and IH:"\<lbrakk> is_valid_ObjIn (pObj (v#vs) 0) (v#vs); |
| trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs)) |
| \<le> length (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs)); |
| valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs)) \<rbrakk> \<Longrightarrow> |
| valid_trans (take (trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs))) (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs)))" |
| thus "valid_trans (take (trans_len (v # vs)) (v # vs))" |
| proof (cases "is_valid_ObjIn (pObj (v#vs) 0) (v#vs)") |
| case True |
| obtain y ys where yys_eq:"take (trans_len (v#vs)) (v#vs) = y#ys" |
| using trans_len_non_zero[where xs="v#vs"] |
| by (drule_tac x=v and y="take (trans_len (v#vs) - 1) vs" in meta_spec2) |
| (case_tac "trans_len (v # vs)", fastforce+) |
| have trans_len_le: "trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs)) |
| \<le> length (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))" |
| using valid True |
| by - (fastforce split: if_splits dest: valid_trans_imp_valid_trans_trans_len) |
| have valid_nxt: "valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))" |
| using valid True by - fastforce |
| have valid_trans_len: "valid_trans (take (trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs))) (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs)))" |
| using IH[OF True trans_len_le valid_nxt] . |
| |
| have "is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| and "Obj.trans\<^sub>f (pObj (v#vs) 0) = bilbyFsTransIn" |
| using True by (simp add: is_valid_ObjTrans)+ |
| |
| hence "is_valid_ObjIn (pObj (y#ys) 0) (y#ys)" |
| and "unat (Obj.len\<^sub>f (pObj (y#ys) 0)) = unat (Obj.len\<^sub>f (pObj (v#vs) 0))" |
| using take_trans_len_is_valid_ObjHeader_preserved[OF _ _ valid yys_eq] |
| by (simp add: is_valid_ObjTrans)+ |
| |
| thus ?thesis |
| using valid_trans_len trans_len_take_drop_eq[OF True valid] |
| by (auto simp: yys_eq[symmetric]) |
| next |
| case False |
| hence validCommit: "is_valid_ObjCommit (pObj (v#vs) 0) (v#vs)" |
| using valid by - (erule valid_trans.elims, simp) |
| thus ?thesis |
| proof (cases "take (trans_len (v # vs)) (v # vs)") |
| case Nil |
| hence False using trans_len_non_zero[where xs="v#vs"] by simp |
| thus ?thesis by simp |
| next |
| case (Cons y ys) |
| |
| have "is_valid_ObjHeader (pObj (v#vs) 0) (v#vs)" |
| and "Obj.trans\<^sub>f (pObj (v#vs) 0) = bilbyFsTransCommit" |
| using validCommit by (simp add: is_valid_ObjTrans)+ |
| |
| hence "is_valid_ObjCommit (pObj (y#ys) 0) (y#ys)" |
| using take_trans_len_is_valid_ObjHeader_preserved[OF _ _ valid Cons] |
| by (simp add: is_valid_ObjTrans) |
| |
| thus ?thesis |
| using Cons by simp |
| qed |
| qed |
| qed |
| |
| lemma drop_append': |
| "drop n (x#xs @ ys) = drop n (x#xs) @ drop (n - length (x#xs)) ys" |
| by (metis append_Cons drop_append) |
| |
| lemma obj_len_append: |
| assumes "unat bilbyFsObjHeaderSize \<le> Suc (length vs)" |
| shows " (Obj.len\<^sub>f (pObj (v # vs @ zs) 0)) = Obj.len\<^sub>f (pObj (v # vs) 0)" |
| using assms by (auto simp: pObj_def pObjHeader_simp n_idx_in_range ple32_def) |
| |
| lemma valid_trans_take_trans_len_imp_valid_trans: |
| assumes valid: "valid_trans (take (trans_len xs) xs)" |
| shows "valid_trans xs" |
| using valid |
| proof (induction "xs" rule: valid_trans.induct) |
| assume "valid_trans (take (trans_len []) [])" |
| hence "False" by simp |
| thus "valid_trans []" by simp |
| next |
| fix v vs |
| assume valid: "valid_trans (take (trans_len (v # vs)) (v # vs))" |
| and IH: "is_valid_ObjIn (pObj (v # vs) 0) (v # vs) \<Longrightarrow> |
| valid_trans (take (trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))) |
| (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))) \<Longrightarrow> |
| valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))" |
| obtain y ys where yys_eq: "y#ys = take (trans_len (v#vs)) (v#vs)" |
| using trans_len_non_zero[where xs="v#vs"] by (cases "take (trans_len (v # vs)) (v # vs)" ,simp+) |
| have len_le_trans_len: "unat (Obj.len\<^sub>f (pObj (y#ys) 0)) \<le> trans_len (y#ys)" |
| using valid_trans_pObj_trans_len[OF valid] yys_eq by simp |
| have valid_obj_xs: "is_valid_ObjHeader (pObj (y#ys) 0) (y#ys)" |
| using valid yys_eq by - (erule valid_trans.elims, clarsimp simp: is_valid_ObjTrans split:if_splits) |
| have trans_len_eq: "trans_len (y#ys) = trans_len (v#vs)" |
| using trans_len_idempotence yys_eq by simp |
| have len_yys: "unat bilbyFsObjHeaderSize \<le> length (y#ys)" |
| using hdr_sz_le_trans_len[where xs="y#ys"] yys_eq[symmetric] |
| valid_trans_imp_valid_trans_trans_len[OF valid] by simp |
| have len_eq: "Obj.len\<^sub>f (pObj (y#ys) 0) = Obj.len\<^sub>f (pObj (v#vs) 0)" |
| using len_yys |
| by (simp add: pObj_def pObjHeader_def Obj.make_def yys_eq |
| ple32_take bilbyFsObjHeaderSize_def Let_def) |
| have min_obj_len_trans_len:"min (unat (Obj.len\<^sub>f (pObj (v#vs) 0))) (trans_len (v#vs)) = unat (Obj.len\<^sub>f (pObj (v#vs) 0))" |
| using len_le_trans_len[simplified trans_len_eq len_eq] by simp |
| have len_lower_bound: "unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj (v#vs) 0))" |
| using is_valid_ObjHeader_len[OF valid_obj_xs] by (simp add: len_eq yys_eq[symmetric]) unat_arith |
| |
| show "valid_trans (v # vs)" |
| proof cases |
| assume is_in: "is_valid_ObjIn (pObj (y#ys) 0) (y#ys)" |
| hence is_in': "is_valid_ObjIn (pObj (v#vs) 0) (v#vs)" |
| apply (clarsimp simp: is_valid_ObjTrans yys_eq ) |
| apply (drule is_valid_ObjHeader_data_len[where ys="v#vs"]) |
| apply (frule is_valid_ObjHeader_len) |
| using len_eq min_obj_len_trans_len |
| by (auto elim: pObjI[OF _ len_lower_bound] simp: bilbyFsObjHeaderSize_def) |
| have "valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (y#ys) 0) (y#ys))" |
| using valid yys_eq[symmetric] by - (erule valid_trans.elims,simp add: is_in) |
| hence valid_take_trans_len_nxt: |
| "valid_trans (take (trans_len (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs))) |
| (drop (unat $ Obj.len\<^sub>f $ pObj (v # vs) 0) (v # vs)))" |
| apply (simp add: yys_eq len_eq[simplified yys_eq]) |
| apply (erule subst[rotated,where P=valid_trans]) |
| using trans_len_take_drop_eq'[OF yys_eq is_in'] len_eq |
| by (simp add: yys_eq) |
| |
| have "valid_trans (drop (unat $ Obj.len\<^sub>f $ pObj (v#vs) 0) (v#vs))" |
| using IH[OF is_in' valid_take_trans_len_nxt] . |
| thus ?thesis |
| using is_in' by (simp add: valid_trans_Cons) |
| next |
| assume is_not_in: "\<not>is_valid_ObjIn (pObj (y#ys) 0) (y#ys)" |
| hence is_commit: "is_valid_ObjCommit (pObj (y#ys) 0) (y#ys)" |
| using valid by - (erule valid_trans.elims, simp add: yys_eq) |
| hence is_commit':"is_valid_ObjCommit (pObj (v#vs) 0) (v#vs)" |
| apply (clarsimp simp: is_valid_ObjTrans yys_eq) |
| apply (drule is_valid_ObjHeader_data_len[where ys="v#vs"]) |
| apply (frule is_valid_ObjHeader_len) |
| using len_eq min_obj_len_trans_len |
| apply (auto elim: pObjI[OF _ len_lower_bound] simp: bilbyFsObjHeaderSize_def) |
| done |
| thus ?thesis |
| using is_commit' by (simp add: valid_trans_Cons is_valid_Obj_diff) |
| qed |
| qed |
| |
| lemma valid_trans_eq_valid_trans_take_trans_len: |
| "valid_trans xs = valid_trans (take (trans_len xs) xs)" |
| apply (rule iffI) |
| apply (erule valid_trans_imp_valid_trans_take_trans_len) |
| apply (erule valid_trans_take_trans_len_imp_valid_trans) |
| done |
| |
| lemma valid_trans_prefixD: |
| "valid_trans xs \<Longrightarrow> |
| prefix xs ys \<Longrightarrow> |
| trans_len ys = trans_len xs" |
| apply (clarsimp simp: prefix_def) |
| apply (rename_tac zs) |
| apply (thin_tac "ys = xs @ zs") |
| apply (induct xs rule: trans_len_induct) |
| apply simp |
| apply (erule valid_trans.elims) |
| apply (rename_tac v vs) |
| apply (case_tac "is_valid_ObjIn (pObj (v#vs) 0) (v#vs)") |
| apply simp |
| apply (case_tac "(v # vs @ zs)") |
| apply (simp add: trans_len_Cons) |
| apply (subst trans_len_Cons) |
| apply (clarsimp simp: is_valid_ObjTrans) |
| apply (rename_tac v) |
| apply (frule_tac ys="(v # vs @ zs)" in is_valid_ObjHeader_prefix) |
| apply (simp) |
| apply simp |
| apply (frule_tac data="(v # vs @ zs)" in is_valid_ObjHeader_len_unat) |
| apply (drule_tac xs="(v # vs @ zs)" and ys="v#vs" in pObjD[rotated]) |
| apply (drule_tac data="(v # vs )" in is_valid_ObjHeader_buf_len) |
| apply clarsimp |
| apply (rule nth_take_lemma) |
| apply (drule_tac is_valid_ObjHeader_buf_len) |
| apply (simp add: pObj_def pObjHeader_simp ple32_append_Cons) |
| apply (simp add: pObj_def pObjHeader_simp ple32_append_Cons) |
| apply (subgoal_tac "unat (Obj.len\<^sub>f (pObj (v # vs @ zs) 0)) = unat (Obj.len\<^sub>f (pObj (v#vs) 0)) ") |
| apply (simp) |
| apply (rename_tac i) |
| apply (case_tac i, simp_all add: nth_append) |
| apply (simp add: pObj_def pObjHeader_simp ple32_append_Cons) |
| apply (drule_tac x=zs in meta_spec) |
| apply (erule_tac P="\<lambda>xs. trans_len xs = |
| trans_len (drop (unat (Obj.len\<^sub>f (pObj (v # vs @ zs) 0))) (v # vs))" in subst[rotated]) |
| apply (subgoal_tac " (unat (Obj.len\<^sub>f (pObj (v # vs @ zs) 0))) \<le> length (v#vs)") |
| apply (simp add: ) |
| apply (subgoal_tac "unat bilbyFsObjHeaderSize \<le> unat (Obj.len\<^sub>f (pObj (v # vs @ zs) 0)) ") |
| apply (simp add: bilbyFsObjHeaderSize_def drop_n_ge_0) |
| apply (drule is_valid_ObjHeader_len, unat_arith) |
| apply (drule is_valid_ObjHeader_buf_len, simp) |
| apply (clarsimp simp: trans_len_Cons is_valid_ObjTrans split: if_splits) |
| apply (frule is_valid_ObjHeader_len) |
| apply (drule is_valid_ObjHeader_buf_len, simp)+ |
| apply (clarsimp simp: pObj_def pObjHeader_simp ple32_append_Cons nth_append max_absorb2) |
| apply unat_arith |
| done |
| |
| lemma valid_trans_prefix_imp: |
| "valid_trans xs \<Longrightarrow> |
| prefix xs ys \<Longrightarrow> |
| valid_trans ys" |
| apply (frule valid_trans_imp_valid_trans_take_trans_len) |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (subgoal_tac "take (trans_len xs) xs = take (trans_len xs) ys") |
| apply simp |
| apply (frule valid_trans_imp_valid_trans_take_trans_len) |
| apply (drule (1) valid_trans_prefixD[THEN sym]) |
| apply simp |
| apply (drule (1) valid_trans_take_trans_len_imp_valid_trans) |
| apply (fastforce simp: prefix_def) |
| done |
| |
| lemma drop_prefixI: |
| "prefix xs ys \<Longrightarrow> |
| prefix (drop n xs) (drop n ys)" |
| by (auto simp: prefix_def) |
| |
| lemma drop_Nil_prefixD: |
| "prefix xs ys \<Longrightarrow> |
| drop n xs \<noteq> [] \<Longrightarrow> (drop n ys) \<noteq> []" |
| by (auto simp: prefix_def) |
| |
| lemma drop_length_append: |
| "drop (length xs) (xs@ys) = ys" |
| by auto |
| |
| lemma drop_trans_len_Nil_eq_length: |
| "drop (trans_len xs) xs = [] \<Longrightarrow> |
| valid_trans xs \<Longrightarrow> |
| trans_len xs = length xs" |
| apply (induct xs rule: trans_len.induct) |
| apply fastforce |
| apply (simp) |
| apply (subst (asm) valid_trans.simps) |
| apply (clarsimp split:if_splits simp:is_valid_ObjTrans) |
| apply (fastforce dest: is_valid_ObjHeader_buf_len)+ |
| done |
| |
| definition valid_obj :: "U8 list \<Rightarrow> bool" |
| where |
| "valid_obj xs \<equiv> is_valid_ObjHeader (pObj xs 0) xs" |
| |
| lemma not_valid_obj_list_trans: |
| "\<not>valid_obj xs \<Longrightarrow> |
| prod.fst (list_trans xs) = xs" |
| by (case_tac xs) |
| (simp add: Let_def valid_obj_def split: list.splits)+ |
| |
| lemma valid_obj_imp_no_pad_byte: |
| "valid_obj xs \<Longrightarrow> xs!0 \<noteq> bilbyFsPadByte" |
| using is_valid_ObjHeader_not_pad[where data=xs] |
| apply (simp add: valid_obj_def) |
| apply (drule is_valid_ObjHeader_buf_len) |
| apply (case_tac xs, simp_all add: bilbyFsObjHeaderSize_def) |
| done |
| |
| lemma valid_trans_imp_valid_obj: |
| "valid_trans xs \<Longrightarrow> valid_obj xs" |
| by (erule valid_trans.elims) |
| (simp add: is_valid_ObjTrans valid_obj_def split:if_splits) |
| |
| lemma nopad_Nil: |
| "\<And>n. nopad xs = [] \<Longrightarrow> nopad (xs@(replicate n bilbyFsPadByte)) = []" |
| by (simp add:nopad_def) |
| |
| lemma list_Cons_append_simp: |
| "b # buf = xs \<Longrightarrow> |
| (b # buf @ ys) = xs @ ys" |
| by simp |
| |
| definition |
| padding :: "nat \<Rightarrow> U8 list" |
| where |
| "padding n = replicate n bilbyFsPadByte" |
| |
| lemma Cons_append: "x # xs @ ys = (x#xs) @ ys" |
| by simp |
| |
| lemma slice_Cons_append: "slice f t (x #xs @ ys) = slice f t (x#xs) @ slice (f - min (length (x#xs)) t) (t - length (x#xs)) ys" |
| by (simp only: Cons_append slice_append ) |
| |
| lemma is_valid_ObjHeader_pObj_eq: |
| "is_valid_ObjHeader (pObj (b # buf @ xs) 0) (b # buf @xs) \<Longrightarrow> |
| is_valid_ObjHeader (pObj (b # buf) 0) (b # buf) \<Longrightarrow> |
| pObj (b # buf @ xs) 0 = pObj (b # buf) 0 " |
| apply (frule is_valid_ObjHeader_len_facts[where data="b # buf"]) |
| apply (frule is_valid_ObjHeader_len_facts[where data="b # buf@xs"]) |
| apply (clarsimp simp: is_valid_ObjHeader_def bilbyFsObjHeaderSize_def pObj_def Let_def pObjHeader_def Obj.make_def) |
| apply (simp add: ple32_eq_slice4 ple64_eq_slice8 slice_Cons_append slice_n_n ) |
| apply (simp only: Cons_append take_append nth_append) |
| apply simp |
| done |
| |
| |
| lemma pTrans_remainderD: |
| "P (prod.fst (pTrans buf)) \<Longrightarrow> P (drop (trans_len buf) buf)" |
| by (simp add: pTrans_remainder) |
| |
| lemma is_valid_ObjHeader_trans_len_le_buf_len: |
| "is_valid_ObjHeader (pObj xs 0) xs \<Longrightarrow> |
| unat (Obj.len\<^sub>f (pObj xs 0)) \<le> length xs" |
| by (clarsimp simp: is_valid_ObjHeader_def) |
| |
| lemma snd_pTrans_append: |
| "valid_trans xs \<Longrightarrow> prod.snd (pTrans (xs @ ys)) = prod.snd (pTrans xs)" |
| apply (induct rule:pTrans.induct) |
| apply simp |
| apply (erule valid_trans.elims) |
| apply (clarsimp split:if_splits simp: is_valid_ObjTrans simp: Let_def) |
| apply (frule is_valid_ObjHeader_pObj_eq[rotated, where xs="ys"]) |
| apply (clarsimp simp: prefix_def is_valid_ObjHeader_prefix) |
| apply (rename_tac v vs) |
| apply (frule_tac ys="(v # vs @ ys)" in is_valid_ObjHeader_prefix) |
| apply simp |
| apply (simp add: prod.case_eq_if) |
| apply (subgoal_tac "(drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs) @ ys) = (drop (unat (Obj.len\<^sub>f (pObj (v # vs) 0))) (v # vs @ ys))") |
| apply simp |
| apply (drule is_valid_ObjHeader_trans_len_le_buf_len) |
| apply (simp add: drop_append' prod.case_eq_if) |
| apply (frule is_valid_ObjHeader_pObj_eq[rotated, where xs="ys"]) |
| apply (clarsimp simp: prefix_def is_valid_ObjHeader_prefix) |
| apply (frule_tac ys="(vb # vaa @ ys)" in is_valid_ObjHeader_prefix, simp) |
| apply (drule is_valid_ObjHeader_trans_len_le_buf_len) |
| apply (simp) |
| done |
| |
| text {* @{term pTrans_valid_non_empty} says that pTrans cannot fail if valid_trans holds *} |
| lemma pTrans_valid_non_empty: |
| "valid_trans xs \<Longrightarrow> prod.snd (pTrans (xs@ys)) \<noteq> []" |
| apply (case_tac "xs@ys") |
| apply simp |
| apply (rename_tac v va ) |
| apply (simp add: Let_def, drule sym, simp) |
| apply (erule valid_trans.elims) |
| apply (rename_tac vb vaa) |
| apply (drule_tac t="vb # vaa" in sym) |
| apply (simp only:) |
| apply (subgoal_tac "is_valid_ObjHeader (pObj (xs @ ys) 0) (xs @ ys)") |
| apply (clarsimp simp: is_valid_ObjTrans split:if_splits) |
| apply (fastforce simp: prod.case_eq_if)+ |
| apply (clarsimp simp: is_valid_ObjTrans split:if_splits) |
| apply (erule is_valid_ObjHeader_prefix, simp_all)+ |
| done |
| |
| lemma valid_trans_pTrans_non_empty_trans: |
| notes notI [rule del] |
| shows |
| "valid_trans xs \<Longrightarrow> |
| prod.snd (pTrans xs) \<noteq> []" |
| using pTrans_valid_non_empty[where ys=Nil] |
| by fastforce |
| |
| text {* Nicer induction lemma (variable renamed) *} |
| lemma list_trans_induct: |
| "(\<And>data. (\<And>data' tx. (data', tx) = pTrans data \<Longrightarrow> data' \<noteq>[] \<Longrightarrow> tx \<noteq> [] \<Longrightarrow> P (nopad data')) \<Longrightarrow> P data) \<Longrightarrow> P a0" |
| apply (rule list_trans.induct) |
| apply (drule_tac x=data in meta_spec) |
| apply (drule meta_mp) |
| apply (drule_tac x=data' and y=tx in meta_spec2) |
| apply (drule_tac x="hd data'" and y="tl data'" in meta_spec2) |
| apply (drule_tac x="hd tx" and y="tl tx" in meta_spec2) |
| apply fastforce |
| apply assumption |
| done |
| |
| lemma snd_list_trans_Nil: |
| "prod.snd (list_trans []) = []" |
| by simp |
| |
| lemma no_pad_Nil: |
| "nopad [] = []" |
| unfolding nopad_def |
| by simp |
| |
| lemma nopad_padding_drop_eq_Nil: |
| "(nopad (drop n (xs @ padding m)) = []) = (nopad (drop n xs) = [])" |
| by (auto simp add: drop_append' nopad_def padding_def) |
| |
| lemma nopad_padding_drop_eq_NilD: |
| "(nopad (drop n xs) = []) \<Longrightarrow> ( nopad (drop n (xs @ padding m)) = [])" |
| using nopad_padding_drop_eq_Nil |
| by auto |
| |
| lemma nopad_padding_drop_eq_Nil': |
| "( nopad (drop n (x # xs @ padding m)) = []) = (nopad (drop n (x # xs)) = [])" |
| using nopad_padding_drop_eq_Nil[where xs="(x # xs)" and n=n and m=m] |
| by (subst Cons_append) auto |
| |
| lemma nopad_padding_append: |
| "nopad xs \<noteq> [] \<Longrightarrow> |
| nopad (xs @ padding m) = nopad xs @ padding m" |
| by (clarsimp simp add: nopad_def padding_def) |
| |
| lemma valid_list_trans_append_padding: |
| "valid_list_trans xs \<Longrightarrow> |
| valid_list_trans (xs @ padding n)" |
| apply (induct xs rule: valid_list_trans.induct) |
| apply simp |
| apply (erule valid_list_trans.elims) |
| apply simp |
| apply (rename_tac b' buf' b buf) |
| apply (clarsimp) |
| apply (frule_tac ys="(b # buf @ padding n)" in valid_trans_prefixD, simp) |
| apply (clarsimp simp add: nopad_padding_drop_eq_Nil' split:if_splits) |
| apply (frule_tac ys="(b # buf @ padding n)" in valid_trans_prefix_imp, simp) |
| apply assumption |
| apply (frule_tac ys="(b # buf @ padding n)" in valid_trans_prefix_imp, simp) |
| apply simp |
| apply (subgoal_tac "(nopad (drop (trans_len (b # buf)) (b # buf)) @ padding n) = (nopad (drop (trans_len (b # buf)) (b # buf @ padding n)))") |
| apply simp |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (simp add: drop_append') |
| apply (case_tac "nopad (drop (trans_len (b # buf)) (b # buf))") |
| apply (simp add: nopad_padding_drop_eq_Nil' nopad_padding_append)+ |
| done |
| |
| lemma snd_list_trans_padding_unchanged: |
| notes list_trans.simps[simp del] |
| and length_drop[simp del] |
| and pTrans.simps[simp del] |
| shows |
| "valid_list_trans xs \<Longrightarrow> |
| prod.snd (list_trans (xs @ padding n)) = prod.snd (list_trans xs)" |
| apply (case_tac n, simp add: padding_def) |
| apply (induct xs rule: list_trans_induct) |
| apply (frule valid_list_trans_append_padding[where n=n]) |
| apply (erule valid_list_trans.elims) |
| apply (erule valid_list_trans.elims) |
| apply clarsimp |
| apply (rename_tac pad_len buf b) |
| apply (clarsimp split: if_splits) |
| apply (subgoal_tac "nopad (drop (trans_len (b # buf @ padding (Suc pad_len))) (b # buf @ padding (Suc pad_len))) = nopad (drop (trans_len (b # buf)) (b # buf))") |
| prefer 2 |
| apply (drule valid_trans_valid_ObjHeaderD,drule is_valid_ObjHeader_trans_len_le_buf_len) |
| apply (simp add: drop_append') |
| apply (subst list_trans.simps) |
| apply (rule sym, subst list_trans.simps, rule sym) |
| apply (frule_tac xs="(b # buf)" and ys="padding (Suc pad_len)" in snd_pTrans_append) |
| apply (simp only: prod.case_eq_if list.case_eq_if pTrans_remainder) |
| apply (case_tac "drop (trans_len (b # buf)) (b # buf)") |
| apply (simp add: snd_list_trans_Nil)+ |
| apply (subst list_trans.simps) |
| apply (rule sym, subst list_trans.simps, rule sym) |
| apply (frule_tac xs="(b # buf)" and ys="padding (Suc pad_len)" in snd_pTrans_append) |
| apply (simp only: prod.case_eq_if list.case_eq_if pTrans_remainder) |
| apply (subgoal_tac "drop (trans_len (b # buf @ padding (Suc pad_len))) (b # buf @ padding (Suc pad_len)) \<noteq> []") |
| prefer 2 |
| apply (frule_tac ys="b # buf @ padding (Suc pad_len)" in valid_trans_prefixD, simp) |
| apply (drule valid_trans_imp_valid_trans_trans_len) |
| apply (simp add: drop_append' padding_def) |
| apply simp |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (simp add: valid_trans_pTrans_non_empty_trans snd_list_trans_Nil) |
| apply (frule_tac ys="(b # buf @ padding (Suc pad_len))" in valid_trans_prefixD, simp) |
| apply (simp add: ) |
| apply (frule_tac m="(Suc pad_len)" in nopad_padding_drop_eq_NilD) |
| apply simp |
| apply (frule_tac ys="(b # buf @ padding (Suc pad_len))" in valid_trans_prefixD, simp) |
| apply (simp add: nopad_padding_drop_eq_Nil') |
| (* last subgoal uses the induction hypothesis *) |
| apply (subst list_trans.simps) |
| apply (rule sym, subst list_trans.simps, rule sym) |
| apply (frule_tac xs="b # buf @ padding (Suc pad_len)" in valid_trans_pTrans_non_empty_trans) |
| apply (frule_tac xs="b # buf" in valid_trans_pTrans_non_empty_trans) |
| apply (frule_tac ys="padding (Suc pad_len)" in snd_pTrans_append) |
| apply (frule nopad_not_Nil) |
| apply (frule_tac ys="(b # buf @ padding (Suc pad_len))" in valid_trans_prefixD, simp) |
| apply (simp add: prod.case_eq_if list.case_eq_if del: drop_eq_Nil) |
| apply (simp add: pTrans_remainder nopad_padding_drop_eq_Nil' drop_append') |
| apply (drule_tac x="prod.fst $ pTrans (b#buf)" and y="prod.snd $ pTrans (b#buf)" in meta_spec2) |
| apply (drule_tac x=pad_len in meta_spec) |
| apply (simp add: pTrans_remainder) |
| apply (erule meta_impE) |
| apply (simp add: prod_eq[symmetric] pTrans_remainder) |
| apply (erule trans[rotated]) |
| apply (rule arg_cong[where f="\<lambda>xs. prod.snd (list_trans xs)"]) |
| apply (simp add: nopad_padding_append) |
| done |
| |
| lemma snd_list_trans_no_pad_padding_unchanged: |
| "valid_list_trans xs \<Longrightarrow> |
| prod.snd (list_trans_no_pad (xs @ padding n)) = prod.snd (list_trans_no_pad xs)" |
| by (fastforce dest: snd_list_trans_padding_unchanged[where n=n] simp: list_trans_no_pad_def prod.case_eq_if simp del: list_trans.simps) |
| |
| lemma valid_list_trans_no_pad_append_padding: |
| "valid_list_trans_no_pad xs \<Longrightarrow> |
| valid_list_trans_no_pad (xs @ padding n)" |
| by (clarsimp simp add: valid_list_trans_no_pad_def |
| valid_list_trans_append_padding[where n=n] |
| snd_list_trans_no_pad_padding_unchanged) |
| |
| |
| lemma snd_list_trans_not_Nil: |
| "valid_list_trans xs \<Longrightarrow> |
| prod.snd (list_trans xs) \<noteq> []" |
| apply (erule valid_list_trans.elims) |
| apply (clarsimp simp del: pTrans.simps) |
| apply (frule valid_trans_pTrans_non_empty_trans) |
| apply (clarsimp simp: prod.case_eq_if simp del: pTrans.simps split:list.splits) |
| done |
| |
| |
| lemma snd_list_trans_nopad_not_Nil: |
| "valid_list_trans_no_pad xs \<Longrightarrow> |
| prod.snd (list_trans_no_pad xs) \<noteq> []" |
| by (simp add: valid_list_trans_no_pad_def) |
| |
| lemma valid_trans_nth_0_neq_pad_byte: |
| "valid_trans xs \<Longrightarrow> xs!0 \<noteq> bilbyFsPadByte" |
| by (fastforce elim: valid_trans.elims dest: is_valid_ObjHeader_not_pad |
| simp: is_valid_ObjTrans split:if_splits) |
| |
| lemma valid_list_trans_nth_0_neq_pad_byte: |
| "valid_list_trans ys \<Longrightarrow> ys!0 \<noteq> bilbyFsPadByte" |
| by (fastforce elim: valid_list_trans.elims dest: valid_trans_nth_0_neq_pad_byte) |
| |
| lemma nopad_drop_trans_len_Nil_append: |
| "valid_list_trans ys \<Longrightarrow> |
| nopad (drop (trans_len xs) xs) = [] \<Longrightarrow> |
| valid_trans xs \<Longrightarrow> |
| nopad (drop (trans_len (xs @ ys)) (xs @ ys)) = ys" |
| apply (frule valid_trans_prefixD[where ys="(xs @ ys)"], simp) |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (simp add: nopad_def) |
| apply (frule valid_list_trans_nth_0_neq_pad_byte) |
| apply (case_tac ys, fastforce+) |
| done |
| |
| lemma nopad_drop_trans_len_Nil_append': |
| "valid_list_trans ys \<Longrightarrow> |
| nopad (drop (trans_len xs) xs) = [] \<Longrightarrow> |
| valid_trans xs \<Longrightarrow> |
| nopad (drop (trans_len xs) (xs @ ys)) = ys" |
| apply (frule valid_trans_prefixD[where ys="(xs @ ys)"], simp) |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (simp add: nopad_def) |
| apply (frule valid_list_trans_nth_0_neq_pad_byte) |
| apply (case_tac ys, fastforce+) |
| done |
| |
| |
| lemma nopad_drop_trans_len_not_Nil_append: |
| "nopad (drop (trans_len xs) xs) \<noteq> [] \<Longrightarrow> |
| valid_trans xs \<Longrightarrow> |
| nopad (drop (trans_len (xs @ ys)) (xs @ ys)) \<noteq> []" |
| apply (frule valid_trans_prefixD[where ys="xs@ys"], simp) |
| apply (frule valid_trans_imp_valid_trans_trans_len) |
| apply (fastforce simp add: nopad_def) |
| done |
| |
| lemma nopad_ys_eq_ys_nopad_append: |
| "nopad ys = ys \<Longrightarrow> |
| nopad (xs @ ys) = nopad xs @ ys" |
| by (metis (no_types, hide_lams) nopad_def append_self_conv dropWhile_append3 |
| dropWhile_eq_Cons_conv valid_list_trans.cases) |
| |
| lemma valid_list_trans_nopad_eq_id: |
| "valid_list_trans xs \<Longrightarrow> nopad xs = xs" |
| by (cases xs) (frule valid_list_trans_nth_0_neq_pad_byte, simp add: nopad_def)+ |
| |
| lemma valid_list_trans_append: |
| assumes val_xs: "valid_list_trans xs" |
| and val_ys: "valid_list_trans ys" |
| shows |
| "valid_list_trans (xs@ys)" |
| proof - |
| obtain y' ys' where ys_cons: "ys = y'#ys'" using val_ys by (case_tac ys, simp) |
| show ?thesis |
| using assms |
| apply (induct xs rule: valid_list_trans.induct) |
| apply simp |
| apply (rename_tac x' xs') |
| apply (clarsimp simp add: split: if_splits) |
| apply (case_tac "nopad (drop (trans_len (x' # xs' @ ys)) (x' # xs' @ ys)) = []") |
| apply simp |
| apply (erule valid_trans_prefix_imp, simp) |
| apply simp |
| apply (frule_tac ys="x'#xs'@ys" in valid_trans_prefix_imp) |
| apply simp |
| apply (simp only: Cons_append) |
| apply (frule (2) nopad_drop_trans_len_Nil_append) |
| apply simp |
| apply (simp only: Cons_append) |
| apply (frule (1) nopad_drop_trans_len_not_Nil_append[where ys="ys"]) |
| apply clarsimp |
| apply (frule_tac ys="x'#xs' @ ys" in valid_trans_prefix_imp, simp) |
| apply (simp) |
| apply (frule_tac ys="(x' # xs' @ ys)" in valid_trans_prefixD, simp) |
| apply simp |
| apply (simp add: drop_append') |
| apply (frule_tac xs="x'#xs'" in valid_trans_imp_valid_trans_trans_len) |
| apply simp |
| apply (frule valid_list_trans_nopad_eq_id) |
| apply (simp add: nopad_ys_eq_ys_nopad_append) |
| done |
| qed |
| |
| lemma trans_len_append: |
| "valid_trans xs \<Longrightarrow> |
| trans_len (xs @ ys) = trans_len xs" |
| apply (induct xs rule:trans_len.induct) |
| apply simp |
| apply (erule valid_trans.elims) |
| apply (simp add: is_valid_ObjTrans) |
| apply (clarsimp split: if_splits) |
| apply (subst trans_len.simps) |
| apply (rename_tac v vs) |
| apply (frule_tac ys="(v#vs @ ys)" in is_valid_ObjHeader_prefix, simp) |
| apply (simp add: is_valid_ObjTrans) |
| apply (frule (1) is_valid_ObjHeader_pObj_eq[where xs=ys] ) |
| apply (simp add: ) |
| apply (erule trans[rotated]) |
| apply (rule arg_cong[where f=trans_len]) |
| apply (frule is_valid_ObjHeader_trans_len_le_buf_len) |
| apply (simp add: drop_append') |
| apply (clarsimp simp add: is_valid_ObjTrans) |
| apply (subst trans_len.simps) |
| apply (simp add: is_valid_ObjTrans) |
| apply (rename_tac v vs) |
| apply (frule_tac ys="(v#vs @ ys)" in is_valid_ObjHeader_prefix, simp) |
| apply (simp add: is_valid_ObjTrans) |
| apply (frule (1) is_valid_ObjHeader_pObj_eq[where xs=ys] ) |
| apply simp |
| done |
| |
| lemma fst_pTrans_append_valid_trans_not_Nil: |
| shows |
| "valid_trans xs \<Longrightarrow> ys \<noteq> [] \<Longrightarrow> |
| prod.fst (pTrans (xs @ ys)) \<noteq> []" |
| apply (subgoal_tac "valid_trans (take (trans_len xs) xs)") |
| prefer 2 |
| apply (simp add: valid_trans_eq_valid_trans_take_trans_len[symmetric]) |
| apply (simp add: pTrans_remainder) |
| apply (subgoal_tac "trans_len (xs @ ys) = trans_len xs \<and> trans_len xs \<le> length xs") |
| apply simp |
| apply (frule valid_trans_imp_valid_trans_trans_len, simp) |
| apply (simp add: trans_len_append) |
| done |
| |
| lemma no_pad_byte_nopad_append: |
| "ys ! 0 \<noteq> bilbyFsPadByte \<Longrightarrow> |
| nopad xs @ ys = nopad (xs @ ys)" |
| apply (simp add: nopad_def) |
| apply (case_tac ys) |
| apply simp |
| apply simp |
| apply (simp add: dropWhile_append3) |
| done |
| |
| lemma list_trans_append: |
| notes list_trans.simps[simp del] |
| and pTrans.simps[simp del] |
| |
| assumes valid_xs: "valid_list_trans xs" |
| and valid_ys: "valid_list_trans ys" |
| |
| shows |
| "prod.snd (list_trans xs) @ prod.snd (list_trans ys) = |
| prod.snd (list_trans (xs@ys))" |
| proof - |
| obtain y' ys' where ys_cons: "ys = y'#ys'" using valid_ys by (case_tac ys, simp) |
| |
| have ys_not_Nil: "ys \<noteq> []" using valid_ys by auto |
| |
| show ?thesis |
| using assms |
| proof (induction xs rule: list_trans_induct) |
| fix data |
| assume IH: |
| "(\<And>data' tx. |
| (data', tx) = pTrans data \<Longrightarrow> |
| data' \<noteq> [] \<Longrightarrow> |
| tx \<noteq> [] \<Longrightarrow> |
| valid_list_trans (nopad data') \<Longrightarrow> |
| valid_list_trans ys \<Longrightarrow> |
| prod.snd (list_trans (nopad data')) @ prod.snd (list_trans ys) = |
| prod.snd (list_trans (nopad data' @ ys)))" |
| and valid_data: "valid_list_trans data" |
| obtain d ds where data_cons: "data = d#ds" using valid_data by (case_tac data, simp) |
| |
| have val_trans_ys: "valid_trans ys" |
| using valid_ys by (simp add: ys_cons) |
| |
| have val_trans_data: "valid_trans data" |
| using valid_data by (simp add: data_cons) |
| |
| show "prod.snd (list_trans data) @ prod.snd (list_trans ys) = prod.snd (list_trans (data @ ys))" |
| proof (cases "nopad (drop (trans_len data) data)") |
| case Nil |
| show ?thesis |
| using Nil |
| apply - |
| apply (subst data_cons, subst list_trans.simps, simp only:data_cons[symmetric]) |
| apply (simp add: prod.case_eq_if) |
| apply (simp add: pTrans_remainder) |
| apply (simp add: list.case_eq_if) |
| using valid_trans_pTrans_non_empty_trans[OF val_trans_data] |
| apply simp |
| using valid_trans_imp_valid_trans_trans_len[OF val_trans_data] |
| apply (simp add: prod.case_eq_if snd_list_trans_Nil) |
| apply (subst list_trans.simps[where data="data@ys"]) |
| apply (simp add: prod.case_eq_if list.case_eq_if) |
| using fst_pTrans_append_valid_trans_not_Nil[OF val_trans_data ys_not_Nil] |
| apply (simp add: pTrans_valid_non_empty[OF val_trans_data] snd_pTrans_append[OF val_trans_data]) |
| apply (simp add: pTrans_remainder trans_len_append[OF val_trans_data] ) |
| using valid_trans_nth_0_neq_pad_byte[OF val_trans_ys] |
| apply (simp add: nopad_def) |
| apply (rule arg_cong[where f=prod.snd]) |
| apply (rule arg_cong[where f=list_trans]) |
| apply (case_tac ys, simp_all) |
| done |
| next |
| case (Cons v vs) |
| show ?thesis |
| using Cons |
| apply (subst list_trans.simps) |
| apply (simp add: prod.case_eq_if list.case_eq_if) |
| apply (simp add: pTrans_remainder) |
| apply (simp add: valid_trans_pTrans_non_empty_trans[OF val_trans_data]) |
| using valid_trans_pTrans_non_empty_trans[OF val_trans_data] |
| apply (case_tac "length data \<le> trans_len data") |
| apply (simp add: nopad_def) |
| apply (simp add: ) |
| using IH[where data'="prod.fst (pTrans data)" and tx="prod.snd (pTrans data)"] |
| apply simp |
| apply (erule meta_impE) |
| apply (simp add: pTrans_remainder nopad_def) |
| apply (simp add: valid_ys) |
| apply (erule meta_impE) |
| apply (simp only: pTrans_remainder) |
| apply (drule sym[where t="v#vs"], simp) |
| apply (cut_tac valid_data[simplified data_cons valid_list_trans.simps, THEN conjunct2]) |
| apply (clarsimp simp add: data_cons[symmetric] split:if_splits) |
| apply (drule sym[where t="v#vs"]) |
| apply simp |
| apply (simp only: pTrans_remainder) |
| apply (thin_tac _)+ |
| apply (rule sym, subst list_trans.simps, rule sym) |
| apply (simp only: prod.case_eq_if) |
| apply (simp only: list.case_eq_if) |
| apply (simp add: fst_pTrans_append_valid_trans_not_Nil[OF val_trans_data ys_not_Nil]) |
| apply (simp add: pTrans_valid_non_empty[OF val_trans_data]) |
| apply (simp add: snd_pTrans_append[OF val_trans_data]) |
| apply (simp only: pTrans_remainder) |
| apply (simp add: valid_trans_prefixD[OF val_trans_data, where ys="data@ys"]) |
| apply (simp add: valid_trans_imp_valid_trans_trans_len[OF val_trans_data]) |
| apply (rule arg_cong[where f=prod.snd]) |
| apply (rule arg_cong[where f=list_trans]) |
| using valid_trans_nth_0_neq_pad_byte[OF val_trans_ys] |
| using valid_trans_imp_valid_trans_trans_len[OF val_trans_data] |
| apply (simp add: no_pad_byte_nopad_append ) |
| done |
| qed |
| qed |
| qed |
| |
| lemma valid_list_trans_no_pad_append: |
| "valid_list_trans_no_pad xs \<Longrightarrow> |
| valid_list_trans_no_pad ys \<Longrightarrow> |
| valid_list_trans_no_pad (xs@ys)" |
| using valid_list_trans_append[where xs=xs and ys=ys] |
| snd_list_trans_not_Nil[where xs=xs] snd_list_trans_not_Nil[where xs=ys] |
| list_trans_append[where xs=xs and ys=ys, symmetric] |
| by (clarsimp simp add: prod.case_eq_if valid_list_trans_no_pad_def |
| list_trans_no_pad_def simp del:list_trans.simps) |
| |
| lemma valid_list_trans_no_pad_imp_valid_list_trans: |
| "valid_list_trans_no_pad xs \<Longrightarrow> valid_list_trans xs" |
| by (simp add: valid_list_trans_no_pad_def) |
| |
| lemma slice_drop: |
| "to \<le> length xs \<Longrightarrow> frm \<le> to \<Longrightarrow> slice frm to xs @ drop to xs = drop frm xs" |
| using drop_append[where xs="take to xs" and ys="drop to xs" and n=frm] |
| by (simp add: slice_def min_absorb1 min_absorb2 unat_arith_simps) |
| |
| lemma list_trans_no_pad_append: |
| notes list_trans.simps[simp del] |
| and pTrans.simps[simp del] |
| assumes valid_slice: "valid_list_trans xs" |
| and valid_drop: "valid_list_trans ys" |
| shows |
| "prod.snd (list_trans_no_pad xs) @ prod.snd (list_trans_no_pad ys) = |
| prod.snd (list_trans_no_pad (xs@ys))" |
| using list_trans_append assms |
| by (clarsimp simp: valid_list_trans_no_pad_def list_trans_no_pad_def |
| prod.case_eq_if filter_append[symmetric] slice_drop min_absorb2) |
| |
| |
| (* Do I need this lemma? |
| It seems that it's not needed it until I start reasoning about pollute_buf. *) |
| (* |
| lemma fst_list_trans: |
| assumes prefixeq: "prefixeq xs ys" |
| and valid_list: "valid_list_trans xs" |
| and no_valid_obj: "\<not>valid_obj (drop (length xs) ys)" |
| (*nopad (drop (length xs) ys) \<noteq> [] \<Longrightarrow>*) |
| shows |
| "fst (list_trans ys) = drop (length xs) ys" |
| proof - |
| from valid_list have "valid_trans xs" |
| by - (erule valid_list_trans.elims, simp) |
| hence valid_ys: "valid_trans ys" |
| using prefixeq by (rule valid_trans_prefixeq_imp) |
| have "snd (pTrans ys) \<noteq> []" |
| using valid_trans_pTrans_non_empty_trans[OF valid_ys] . |
| thus ?thesis |
| using assms |
| proof (induction "ys" arbitrary:xs rule: list_trans_induct) |
| fix xs ys |
| assume snd_pTrans: "snd (pTrans ys) \<noteq> []" |
| and prefixeq: "prefixeq xs ys" |
| and valid_list: "valid_list_trans xs" |
| and not_valid_obj: "\<not> valid_obj (drop (length xs) ys)" |
| and IH: |
| "\<And>data' tx xs. |
| (data', tx) = pTrans ys \<Longrightarrow> |
| data' \<noteq> [] \<Longrightarrow> |
| tx \<noteq> [] \<Longrightarrow> |
| snd (pTrans (nopad data')) \<noteq> [] \<Longrightarrow> |
| prefixeq xs (nopad data') \<Longrightarrow> |
| valid_list_trans xs \<Longrightarrow> |
| \<not> valid_obj (drop (length xs) (nopad data')) \<Longrightarrow> |
| fst (list_trans (nopad data')) = drop (length xs) (nopad data')" |
| show "fst (list_trans ys) = drop (length xs) ys" |
| proof - |
| obtain zs where zsimp: "ys = xs @ zs" |
| using prefixeq by (fastforce simp : prefixeq_def) |
| have valid_trans_xs: "valid_trans xs" |
| using valid_list by - (erule valid_list_trans.elims, simp) |
| hence xs_not_nil: "xs \<noteq> []" |
| using valid_trans_xs by (case_tac xs, simp_all) |
| have valid_trans_ys: "valid_trans (xs@zs)" |
| using valid_trans_prefixeq_imp[OF valid_trans_xs prefixeq, simplified zsimp] . |
| hence ys_not_nil: "(xs@zs) \<noteq> []" |
| using valid_trans_xs by (case_tac "xs@zs", simp_all) |
| have trans_len_eq: "trans_len (xs@zs) = trans_len xs" |
| using valid_trans_prefixeqD[OF valid_trans_xs prefixeq, simplified zsimp] . |
| have trans_len_le_length_xs: "trans_len xs \<le> length xs" |
| using valid_trans_imp_valid_trans_trans_len[OF valid_trans_xs] . |
| have xs_remainder: "fst (pTrans xs) = drop (trans_len xs) xs" |
| using pTrans_remainder[where buf="xs"] . |
| have ys_remainder: "fst (pTrans (xs @ zs)) = drop (trans_len (xs @ zs)) (xs @ zs)" |
| using pTrans_remainder[where buf="xs@zs"] . |
| thus ?thesis |
| proof cases |
| assume length_xs: "trans_len xs = length xs" |
| hence fst_pTrans_ys:"fst (pTrans (xs@zs)) = zs" |
| using ys_remainder trans_len_eq by simp |
| thus ?thesis |
| using snd_pTrans apply (case_tac ys, simp, simp del:pTrans.simps) |
| apply (drule sym[where s=ys], simp add: zsimp prod.case_eq_if) |
| apply (case_tac zs, simp split:list.splits) |
| apply (simp) |
| apply (case_tac " snd (pTrans (xs @ zs))", fastforce) |
| using not_valid_obj_list_trans[OF not_valid_obj[simplified zsimp drop_length_append]] |
| apply (simp del:pTrans.simps list_trans.simps add: prod.case_eq_if) |
| oops |
| next |
| fix tx |
| let ?vs = "drop (trans_len xs) xs" |
| assume length_xs: "trans_len xs \<noteq> length xs" |
| hence vs_not_nil: "?vs \<noteq> []" |
| using trans_len_eq trans_len_le_length_xs by simp |
| obtain data' where data'_pTrans: "data' = fst (pTrans ys)" |
| by simp |
| hence data_eq: "data' = drop (trans_len ys) ys" |
| using zsimp ys_remainder by simp |
| hence data'_not_nil: "data' \<noteq> []" |
| using ys_remainder zsimp trans_len_eq trans_len_le_length_xs length_xs by simp |
| obtain tx where tx_facts: "tx = snd (pTrans ys) \<and> tx \<noteq> []" |
| using snd_pTrans by fastforce |
| |
| hence a1: "(data', tx) = pTrans ys" |
| using data'_pTrans tx_facts by fastforce |
| have a5: "prefixeq ?vs (nopad data')" |
| by (simp add: data_eq trans_len_eq zsimp) |
| have a6: "valid_list_trans ?vs" |
| using valid_list trans_len_le_length_xs length_xs |
| by - (erule valid_list_trans.elims, fastforce) |
| have a4: "snd (pTrans (nopad data')) \<noteq> []" |
| proof - |
| have "valid_trans ?vs" |
| using valid_list a6 length_xs trans_len_le_length_xs |
| by - (fastforce elim: valid_list_trans.elims) |
| hence "valid_trans data'" |
| using a5 by - (drule valid_trans_prefixeq_imp) |
| thus ?thesis |
| by - (drule valid_trans_pTrans_non_empty_trans) |
| qed |
| have a7: "\<not> valid_obj (drop (length ?vs) data')" |
| using trans_len_le_length_xs trans_len_eq not_valid_obj |
| by (simp add: zsimp data_eq) |
| have "fst (list_trans data') = drop (length ?vs) data'" |
| using IH[OF a1 data'_not_nil conjunct2[OF tx_facts] a4 ] |
| using IH[OF a1 data'_not_nil conjunct2[OF tx_facts] a4 a5 a6 a7] oops |
| thus ?thesis |
| apply (simp only:zsimp data_eq) |
| apply (subst list_trans.simps) |
| using ys_remainder snd_pTrans[simplified zsimp] length_xs trans_len_eq |
| apply (simp add: prod.case_eq_if del: list_trans.simps) |
| apply (subgoal_tac "drop (trans_len xs) xs @ drop (trans_len xs - length xs) zs \<noteq> []") |
| using trans_len_le_length_xs |
| apply (clarsimp simp: prod.case_eq_if simp del: list_trans.simps split: list.splits)+ |
| done |
| qed |
| qed |
| qed |
| qed |
| *) |
| end |
