Changeset 865


Ignore:
Timestamp:
May 31, 2011, 11:45:21 AM (8 years ago)
Author:
sacerdot
Message:

Renaming.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r864 r865  
    362362 match l with
    363363  [ nil ⇒ true
    364   | cons hd tl ⇒ notb (address_of_word_labels_internal id hd) ∧ does_not_occur id tl].
     364  | cons hd tl ⇒ notb (instruction_matches_identifier id hd) ∧ does_not_occur id tl].
    365365
    366366lemma does_not_occur_None:
     
    376376  [ nil ⇒ false
    377377  | cons hd tl ⇒
    378      if address_of_word_labels_internal id hd then
     378     if instruction_matches_identifier id hd then
    379379      does_not_occur id tl
    380380     else
     
    393393lemma index_of_internal_None: ∀i,id,instr_list,n.
    394394 occurs_exactly_once id (instr_list@[〈None …,i〉]) →
    395   index_of_internal ? (address_of_word_labels_internal id) instr_list n =
    396    index_of_internal ? (address_of_word_labels_internal id) (instr_list@[〈None …,i〉]) n.
     395  index_of_internal ? (instruction_matches_identifier id) instr_list n =
     396   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈None …,i〉]) n.
    397397 #i #id #instr_list elim instr_list
    398398  [ #n #abs whd in abs; cases abs
    399399  | #hd #tl #IH #n whd in ⊢ (% → ??%%); whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?)
    400     cases (address_of_word_labels_internal id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
     400    cases (instruction_matches_identifier id hd) whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ??%%)
    401401    [ #H %
    402402    | #H @IH whd in H; cases (occurs_exactly_once ??) in H ⊢ %
  • src/ASM/Interpret.ma

    r856 r865  
    642642    index_of_internal A eq l 0.
    643643
    644 definition address_of_word_labels_internal
     644definition instruction_matches_identifier
    645645  λy: Identifier.
    646646  λx: labelled_instruction.
     
    653653  λcode_mem.
    654654  λid: Identifier.
    655     bitvector_of_nat 16 (index_of ? (address_of_word_labels_internal id) code_mem).
     655    bitvector_of_nat 16 (index_of ? (instruction_matches_identifier id) code_mem).
    656656
    657657definition address_of_word_labels ≝
Note: See TracChangeset for help on using the changeset viewer.