Changeset 1354 for src/RTLabs/RTLabsToRTL.ma

Timestamp:

Oct 11, 2011, 2:38:19 PM (8 years ago)

Author:

sacerdot

Message:

One axiom closed.

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (1 diff)

src/RTLabs/RTLabsToRTL.ma

@@ -128 +128 @@
   λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl.
 
-axiom split_into_bytes:
-  ∀size.
-  ∀int: bvint size.
-    Σbytes: list Byte. |bytes| = size_intsize size.
+definition split_into_bytes:
+  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝ 
+λsize.
+ match size return λsize.∀int: bvint size. Σbytes. |bytes| = size_intsize size with
+  [ I8 ⇒ λint. ? | I16 ⇒ λint. ? | I32 ⇒ λint. ? ].
+[ %[@[int]] //
+| %[@(let 〈h,l〉 ≝ split ? 8 … int in [l;h])] cases (split ????) //
+| %[@(let 〈h1,l〉 ≝ split ? 8 … int in
+      let 〈h2,l〉 ≝ split ? 8 … l in
+      let 〈h3,l〉 ≝ split ? 8 … l in
+       [l;h3;h2;h1])]
+  cases (split ????) #h1 #l normalize
+  cases (split ????) #h2 #l normalize
+  cases (split ????) // ]
+qed.
 
 lemma eqb_implies_eq: