Changeset 2028


Ignore:
Timestamp:
Jun 7, 2012, 5:58:26 PM (5 years ago)
Author:
boender
Message:
  • bugfix to Assembly (forgotten sigma)
  • added add_bitvector_of_nat_plus to Arithmetic
  • insert_lookup_opt_miss to BitVectorTrie?
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1963 r2028  
    556556qed.
    557557
     558axiom add_bitvector_of_nat_plus:
     559  ∀n,p,q:nat.
     560    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
     561   
    558562definition sign_bit : ∀n. BitVector n → bool ≝
    559563λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
  • src/ASM/Assembly.ma

    r2022 r2028  
    559559        [ SJMP address ]
    560560    else
    561       let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (lookup_labels jmp) in
     561      let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (sigma (lookup_labels jmp)) in
    562562      let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in
    563563      if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then
  • src/ASM/BitVectorTrie.ma

    r1931 r2028  
    478478qed.
    479479
    480 lemma insert_lookup_opt:
     480lemma insert_lookup_opt_hit:
    481481 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
    482482   lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ (b = c ∧ a = v).
     
    503503qed.
    504504
     505lemma insert_lookup_opt_miss:
     506 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     507   lookup_opt … b (insert … c v t) = None A →
     508     (notb (eq_bv n b c)) = true ∧ lookup_opt … b t = None A.
     509 #A #v #n #c elim c -c; -n;
     510 [ #b #t #Hl normalize in Hl; destruct (Hl)
     511 | #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq
     512   #t cases (BitVectorTrie_Sn … t)
     513   [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
     514     [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% ->%); #Heq3
     515       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_insert_hit #H destruct (H)
     516       |2,4: >lookup_opt_insert_miss in H;
     517         [1,3: #H whd in match eq_bv in Heq3; >Heq3 @conj
     518           [1,3: / by refl/
     519           |2,4: @H
     520           ]
     521         |2,4: >Heq3 / by I/
     522         ]
     523       ]
     524     |2,3: @conj
     525       [1,3: @refl
     526       |2,4: @H
     527       ]
     528     ]
     529   | #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize
     530     [1,4:  lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %); #Heq3
     531       [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X)
     532       |2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H;
     533         [1,3: #X @conj
     534           [1,3: whd in match (eq_bv ???) in Heq3; >Heq3 / by refl/
     535           |2,4: @refl
     536           ]
     537         |2,4: >Heq3 / by I/
     538         ]
     539       ]
     540     |2,3: @conj @refl
     541     ]
     542   ]
     543 ]
     544qed.
     545   
    505546lemma forall_insert_inv1:
    506547  ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset for help on using the changeset viewer.