Changeset 2028
 Timestamp:
 Jun 7, 2012, 5:58:26 PM (7 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1963 r2028 556 556 qed. 557 557 558 axiom 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 558 562 definition sign_bit : ∀n. BitVector n → bool ≝ 559 563 λn,v. match v with [ VEmpty ⇒ false  VCons _ h _ ⇒ h ]. 
src/ASM/Assembly.ma
r2022 r2028 559 559 [ SJMP address ] 560 560 else 561 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 ( lookup_labels jmp) in561 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 (sigma (lookup_labels jmp)) in 562 562 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc_plus_jmp_length in 563 563 if eq_bv ? fst_5_addr fst_5_pc ∧ ¬ do_a_long then 
src/ASM/BitVectorTrie.ma
r1931 r2028 478 478 qed. 479 479 480 lemma insert_lookup_opt :480 lemma insert_lookup_opt_hit: 481 481 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 482 482 lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ (b = c ∧ a = v). … … 503 503 qed. 504 504 505 lemma 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 ] 544 qed. 545 505 546 lemma forall_insert_inv1: 506 547 ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset
for help on using the changeset viewer.