Ignore:
Timestamp:
Jun 20, 2012, 4:51:35 PM (8 years ago)
Author:
boender
Message:
  • some small changes
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/PolicyFront.ma

    r2101 r2102  
    767767 ]
    768768qed.
     769
     770lemma occurs_does_not: ∀tag,A,id,list_instr.
     771  does_not_occur tag A id list_instr = true →
     772  occurs_exactly_once tag A id list_instr = true →
     773  False.
     774 #tag #A #id #list_instr elim list_instr
     775 [ #_ whd in match (occurs_exactly_once ????); #ABS destruct (ABS)
     776 | #h #t #Hind whd in match (does_not_occur ????);
     777   whd in match (occurs_exactly_once ????);
     778   cases (instruction_matches_identifier ?? id h) normalize nodelta
     779   [ #ABS destruct (ABS)
     780   | @Hind
     781   ]
     782 ]
     783qed.
     784 
     785lemma label_in_program: ∀program:(Σl.S (|l|) < 2^16).∀labels:(Σlm.
     786   ∀l.occurs_exactly_once ?? l program →
     787    bitvector_of_nat ? (lookup_def ?? lm l 0) =
     788     address_of_word_labels_code_mem program l).∀x.
     789 occurs_exactly_once ?? x program →   
     790 lookup_def ASMTag ℕ labels x O≤|program|.
     791 #program cases program -program #program #Hprogram #labels #x cases labels
     792 -labels #labels #H lapply (H x) -H
     793 generalize in match (lookup_def … labels x 0);
     794 whd in match address_of_word_labels_code_mem;
     795 whd in match index_of; normalize nodelta elim program in Hprogram;
     796 [ #Hprogram #n cases not_implemented
     797 | #h #t #Hind #Hprogram #n #Hlm #Hocc lapply (Hlm Hocc) -Hlm #Hbv
     798   whd in match (occurs_exactly_once ????) in Hocc;
     799   whd in match (index_of_internal ????) in Hbv;
     800   lapply (refl ? (instruction_matches_identifier … x h))
     801   lapply Hocc; lapply Hbv; -Hocc -Hbv
     802   cases (instruction_matches_identifier … x h) in ⊢ (% → % → ???% → %);
     803   normalize nodelta #Hbv #Hocc #EQ
     804   [ >(bitvector_of_nat_ok 16 n 0)
     805     [ @le_O_n
     806     | >(eq_eq_bv … Hbv) @I
     807     | / by /
     808     | cases daemon
     809     ]
     810   | cases n in Hbv;
     811     [ #_ @le_O_n
     812     | -n #n #Hbv @le_S_S @(Hind … Hocc)
     813       [ @(transitive_lt … Hprogram) @le_n
     814       | #_ lapply (bitvector_of_nat_ok 16 (S n) (index_of_internal ? (instruction_matches_identifier ?? x) t 1) ???)
     815         [ >Hbv >eq_bv_refl @I
     816         | @(transitive_lt … Hprogram) cases daemon
     817         | cases daemon
     818         | #H >(index_of_label_from_internal … Hocc)
     819           <plus_O_n >(index_of_label_from_internal … Hocc) in H;
     820           #H >(injective_S … H) <plus_O_n @refl
     821         ]
     822       ]
     823     ]
     824   ]
     825 ]
     826qed.
Note: See TracChangeset for help on using the changeset viewer.