Changeset 2102 for src/ASM/PolicyFront.ma
 Timestamp:
 Jun 20, 2012, 4:51:35 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2101 r2102 767 767 ] 768 768 qed. 769 770 lemma 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 ] 783 qed. 784 785 lemma 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 ] 826 qed.
Note: See TracChangeset
for help on using the changeset viewer.