Changeset 1646 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jan 16, 2012, 3:04:14 PM (8 years ago)
Author:
mulligan
Message:

finished the block_costs computation, and propagated the changes forward, subject to closing two axioms (an elimination principle, and a lemma on subvectors). moved some code around to its rightful place.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1599 r1646  
    11include "ASM/BitVector.ma".
    22include "ASM/Util.ma".
     3
     4definition addr16_of_addr11: Word → Word11 → Word ≝
     5  λpc: Word.
     6  λa: Word11.
     7  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
     8  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
     9  let 〈b123, b〉 ≝ split … 3 8 a in
     10  let b1 ≝ get_index_v … b123 0 ? in
     11  let b2 ≝ get_index_v … b123 1 ? in
     12  let b3 ≝ get_index_v … b123 2 ? in
     13  let p5 ≝ get_index_v … n2 0 ? in
     14    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
     15  //
     16qed.
    317
    418definition nat_of_bool ≝
Note: See TracChangeset for help on using the changeset viewer.