Changeset 1479
 Timestamp:
 Nov 2, 2011, 8:27:30 AM (10 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1459 r1479 1000 1000 definition jump_expansion': pseudo_assembly_program → policy_type ≝ 1001 1001 λprogram.λpc. 1002 let policy ≝ jump_expansion_internal (\snd program) in1002 let policy ≝ jump_expansion_internal (\snd program) (\snd program) in 1003 1003 let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in 1004 1004 j. 
src/ASM/BitVectorTrie.ma
r1474 r1479 464 464 qed. 465 465 466 lemma insert_lookup_opt: 467 ∀A:Type[0].∀v,a:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 468 lookup_opt … b (insert … c v t) = Some A a → lookup_opt … b t = Some A a ∨ a = v. 469 #A #v #a #n #c elim c c; n; 470 [ #b #t #Hl normalize in Hl; %2 destruct (Hl) @refl 471  #n #hd #tl #Hind #b cases (BitVector_Sn … b) #hd' * #tl' #Heq >Heq 472 #t cases (BitVectorTrie_Sn … t) 473 [ * #l * #r #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize 474 [1,4: @(Hind tl' ? H) 475 2,3: %1 @H 476 ] 477  #Heq2 >Heq2 cases hd cases hd' #H normalize in H; normalize 478 [1,4: lapply (refl ? (eq_bv ? tl' tl)) cases (eq_bv ? tl' tl) in ⊢ (???% → %) #Heq3 479 [1,3: >(eq_bv_eq … Heq3) in H; >lookup_opt_prepare_trie_for_insertion_hit #X destruct (X) %2 // 480 2,4: >(lookup_opt_prepare_trie_for_insertion_miss) in H 481 [1,3: #X %1 // 482 2,4: >Heq3 // 483 ] 484 ] 485 2,3: destruct (H) 486 ] 487 qed. 488 466 489 lemma forall_insert_inv1: 467 490 ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset
for help on using the changeset viewer.