Changeset 1354 for src/RTLabs/RTLabsToRTL.ma
- Timestamp:
- Oct 11, 2011, 2:38:19 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTLabs/RTLabsToRTL.ma
r1352 r1354 128 128 λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. 129 129 130 axiom split_into_bytes: 131 ∀size. 132 ∀int: bvint size. 133 Σbytes: list Byte. |bytes| = size_intsize size. 130 definition split_into_bytes: 131 ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ 132 λsize. 133 match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with 134 [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ]. 135 [ %[@[int]] // 136 | %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) // 137 | %[@(let 〈h1,l〉 ≝ split ? 8 … int in 138 let 〈h2,l〉 ≝ split ? 8 … l in 139 let 〈h3,l〉 ≝ split ? 8 … l in 140 [l;h3;h2;h1])] 141 cases (split ????) #h1 #l normalize 142 cases (split ????) #h2 #l normalize 143 cases (split ????) // ] 144 qed. 134 145 135 146 lemma eqb_implies_eq:
Note: See TracChangeset
for help on using the changeset viewer.