Changeset 2124 for src/ASM/BitVector.ma


Ignore:
Timestamp:
Jun 27, 2012, 4:23:54 PM (7 years ago)
Author:
sacerdot
Message:

Much more shuffling around to proper places

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r2122 r2124  
    236236    String.
    237237
    238 example sub_minus_one_seven_eight:
    239   ∀v: BitVector 7.
    240   false ::: (\fst (sub_7_with_carry v (bitvector_of_nat ? 1) false)) =
    241   \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false).
    242  cases daemon.
    243 qed.
    244 
    245 axiom sub16_with_carry_overflow:
    246   ∀left, right, result: BitVector 16.
    247   ∀flags: BitVector 3.
    248   ∀upper: BitVector 9.
    249   ∀lower: BitVector 7.
    250     sub_16_with_carry left right false = 〈result, flags〉 →
    251       vsplit bool 9 7 result = 〈upper, lower〉 →
    252         get_index_v bool 3 flags 2 ? = true →
    253           upper = [[true; true; true; true; true; true; true; true; true]].
    254   //
    255 qed.
    256 
    257 axiom sub_16_to_add_16_8_0:
    258  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    259   get_index' ? 2 0 flags = false →
    260   sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
    261    v1 = add ? v2 (sign_extension (false:::v3)).
    262 
    263 axiom sub_16_to_add_16_8_1:
    264  ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
    265   get_index' ? 2 0 flags = true →
    266   sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
    267    v1 = add ? v2 (sign_extension (true:::v3)).
     238definition bitvector_3_cases:
     239  ∀b: BitVector 3.
     240    ∃l, c, r: bool.
     241      b ≃ [[l; c; r]].
     242  #b
     243  @(Vector_inv_ind bool 3 b (λn: nat. λv: Vector bool n. ∃l:bool.∃c:bool.∃r:bool. v ≃ [[l; c; r]]))
     244  [1:
     245    #absurd @⊥ -b @(destruct_bug_fix_1 2)
     246    >absurd %
     247  |2:
     248    #n #hd #tl #_ #size_refl #hd_tl_refl %{hd}
     249    cut (n = 2)
     250    [1:
     251      @destruct_bug_fix_2
     252      >size_refl %
     253    |2:
     254      #n_refl >n_refl in tl; #V
     255      @(Vector_inv_ind bool 2 V (λn: nat. λv: Vector bool n. ∃c:bool. ∃r:bool. hd:::v ≃ [[hd; c; r]]))
     256      [1:
     257        #absurd @⊥ -V @(destruct_bug_fix_1 1)
     258        >absurd %
     259      |2:
     260        #n' #hd' #tl' #_ #size_refl' #hd_tl_refl' %{hd'}
     261        cut (n' = 1)
     262        [1:
     263          @destruct_bug_fix_2 >size_refl' %
     264        |2:
     265          #n_refl' >n_refl' in tl'; #V'
     266          @(Vector_inv_ind bool 1 V' (λn: nat. λv: Vector bool n. ∃r: bool. hd:::hd':::v ≃ [[hd; hd'; r]]))
     267          [1:
     268            #absurd @⊥ -V' @(destruct_bug_fix_1 0)
     269            >absurd %
     270          |2:
     271            #n'' #hd'' #tl'' #_ #size_refl'' #hd_tl_refl'' %{hd''}
     272            cut (n'' = 0)
     273            [1:
     274              @destruct_bug_fix_2 >size_refl'' %
     275            |2:
     276              #n_refl'' >n_refl'' in tl''; #tl'''
     277              >(Vector_O … tl''') %
     278            ]
     279          ]
     280        ]
     281      ]
     282    ]
     283  ]
     284qed.
     285
     286lemma bitvector_3_elim_prop:
     287  ∀P: BitVector 3 → Prop.
     288    P [[false;false;false]] → P [[false;false;true]] → P [[false;true;false]] →
     289    P [[false;true;true]] → P [[true;false;false]] → P [[true;false;true]] →
     290    P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
     291  #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9
     292  cases (bitvector_3_cases … H9) #l #assm cases assm
     293  -assm #c #assm cases assm
     294  -assm #r #assm cases assm destruct
     295  cases l cases c cases r assumption
     296qed.
Note: See TracChangeset for help on using the changeset viewer.