Changeset 2111 for src/ASM/Status.ma


Ignore:
Timestamp:
Jun 26, 2012, 5:30:41 PM (8 years ago)
Author:
sacerdot
Message:

Cleanup: lemmas/theorems/axioms moved to the right places.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r2055 r2111  
    11301130qed.
    11311131
     1132lemma fetch_pseudo_instruction_vsplit:
     1133 ∀instr_list,ppc,ppc_ok.
     1134  ∃pre,suff,lbl.
     1135   (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
     1136#instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
     1137cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
     1138lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
     1139#EQ %{lbl0} @EQ
     1140qed.
     1141
     1142lemma fetch_pseudo_instruction_append:
     1143 ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
     1144  let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
     1145  fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
     1146  〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
     1147 #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
     1148 cut (|l1| + nat_of_bitvector … ppc < 2^16)
     1149 [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
     1150 -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
     1151 >nat_of_bitvector_bitvector_of_nat_inverse try assumption
     1152 [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
     1153 #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
     1154 #lbl #instr normalize nodelta >add_associative %
     1155qed.
     1156
    11321157definition address_of_word_labels_code_mem ≝
    11331158  λcode_mem : list labelled_instruction.
Note: See TracChangeset for help on using the changeset viewer.