Ignore:
Timestamp:
Jul 15, 2011, 12:56:48 PM (8 years ago)
Author:
campbell
Message:

Show that entry and exit labels are in the RTLabs graph.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r1052 r1070  
    358358qed.
    359359
     360lemma lookup_opt_prepare_trie_for_insertion_miss:
     361 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.
     362  (notb (eq_bv ? b c)) → lookup_opt … b (prepare_trie_for_insertion … c v) = None ?.
     363 #A #v #n #c elim c
     364  [ #b >(BitVector_O … b) normalize #abs @⊥ //
     365  | #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     366    cases hd cases hd' normalize
     367    [2,3: #_ cases tl' //
     368    |*: change with (bool_to_Prop (notb (eq_bv ???)) → ?) @IH ]]
     369qed.
     370
    360371lemma lookup_opt_insert_hit:
    361372 ∀A:Type[0].∀v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.
     
    374385 ]
    375386qed.
    376    
     387
     388lemma lookup_opt_insert_miss:
     389 ∀A:Type[0].∀v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.
     390  (notb (eq_bv ? b c)) → lookup_opt … b (insert … c v t) = lookup_opt … b t.
     391 #A #v #n #c elim c -c -n
     392  [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //
     393  | #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ
     394    #t cases(BitVectorTrie_Sn … t)
     395    [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     396     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //
     397    | #JMEQ >JMEQ cases hd cases hd' #H normalize in H;
     398     [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize
     399     [3,4: cases tl' // | *: @lookup_opt_prepare_trie_for_insertion_miss //]]]
     400qed.
     401
    377402lemma forall_insert_inv1:
    378403  ∀A.∀n.∀b.∀a.∀t.∀P.
Note: See TracChangeset for help on using the changeset viewer.