Changeset 1354


Ignore:
Timestamp:
Oct 11, 2011, 2:38:19 PM (8 years ago)
Author:
sacerdot
Message:

One axiom closed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1352 r1354  
    128128  λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
    129129
    130 axiom split_into_bytes:
    131   ∀size.
    132   ∀int: bvint size.
    133     Σbytes: list Byte. |bytes| = size_intsize size.
     130definition 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 ????) // ]
     144qed.
    134145
    135146lemma eqb_implies_eq:
Note: See TracChangeset for help on using the changeset viewer.