Changeset 2111 for src/ASM/Assembly.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r2110 r2111  
    581581    \fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc (λx.zero …) i).
    582582
    583 (*CSC: move elsewhere *)
    584 lemma nth_safe_append:
    585  ∀A,l,n,n_ok.
    586   ∃pre,suff.
    587    (pre @ [nth_safe A n l n_ok]) @ suff = l.
    588 #A #l elim l normalize
    589  [ #n #abs cases (absurd ? abs (not_le_Sn_O ?))
    590  | #hd #tl #IH #n cases n normalize
    591    [ #_ %{[]} /2/
    592    | #m #m_ok cases (IH m ?)
    593      [ #pre * #suff #EQ %{(hd::pre)} %{suff} <EQ in ⊢ (???%); % | skip ]]
    594 qed.
    595 
    596 lemma fetch_pseudo_instruction_vsplit:
    597  ∀instr_list,ppc,ppc_ok.
    598   ∃pre,suff,lbl.
    599    (pre @ [〈lbl,\fst (fetch_pseudo_instruction instr_list ppc ppc_ok)〉]) @ suff = instr_list.
    600 #instr_list #ppc #ppc_ok whd in match (fetch_pseudo_instruction ???);
    601 cases (nth_safe_append … instr_list … ppc_ok) #pre * #suff #EQ %{pre} %{suff}
    602 lapply EQ -EQ cases (nth_safe labelled_instruction ???) #lbl0 #instr normalize nodelta
    603 #EQ %{lbl0} @EQ
    604 qed.
    605 
    606 axiom eqb_succ_injective_Pos:
    607   ∀l, r: Pos.
    608     eqb (succ l) (succ r) = true → eqb l r = true.
    609 
    610 lemma eqb_true_to_refl_Pos:
    611   ∀l, r: Pos.
    612     eqb l r = true → l = r.
    613   #l #r @(pos_elim2 … l r)
    614   [1:
    615     #r cases r
    616     [1:
    617       #_ %
    618     |2,3:
    619       #l normalize in ⊢ (% → ?); #absurd destruct(absurd)
    620     ]
    621   |2:
    622     #l cases l
    623     [1:
    624       normalize in ⊢ (% → ?); #absurd destruct(absurd)
    625     |2,3:
    626       #l' normalize in ⊢ (% → ?); #absurd destruct(absurd)
    627     ]
    628   |3:
    629     #l #r #inductive_hypothesis #relevant @eq_f
    630     @inductive_hypothesis @eqb_succ_injective_Pos
    631     assumption
    632   ]
    633 qed.
    634 
    635 lemma eq_identifier_eq:
    636   ∀tag: String.
    637   ∀l.
    638   ∀r.
    639     eq_identifier tag l r = true → l = r.
    640   #tag #l #r cases l cases r
    641   #pos_l #pos_r
    642   cases pos_l cases pos_r
    643   [1:
    644     #_ %
    645   |2,3,4,7:
    646     #p1_l normalize in ⊢ (% → ?);
    647     #absurd destruct(absurd)
    648   |5,9:
    649     #p1_l #p1_r normalize in ⊢ (% → ?);
    650     #relevant
    651     >(eqb_true_to_refl_Pos … relevant) %
    652   |*:
    653     #p_l #p_r normalize in ⊢ (% → ?);
    654     #absurd destruct(absurd)
    655   ]
    656 qed.
    657 
    658 axiom neq_identifier_neq:
    659   ∀tag: String.
    660   ∀l, r: identifier tag.
    661     eq_identifier tag l r = false → (l = r → False).
    662583 
    663584(* label_map: identifier ↦ pseudo program counter *)
     
    772693qed.
    773694
    774 
    775 (*CSC: move elsewhere; practically equal to shift_nth_safe but for commutation
    776   of addition. One of the two lemmas should disappear. *)
    777 lemma nth_safe_prepend:
    778  ∀A,l1,l2,j.∀H:j<|l2|.∀K:|l1|+j<|(l1@l2)|.
    779   nth_safe A j l2 H =nth_safe A (|l1|+j) (l1@l2) K.
    780  #A #l1 #l2 #j #H >commutative_plus @shift_nth_safe
    781 qed.
    782 
    783 lemma nth_safe_cons:
    784  ∀A,hd,tl,l2,j,j_ok,Sj_ok.
    785   nth_safe A j (tl@l2) j_ok =nth_safe A (1+j) (hd::tl@l2) Sj_ok.
    786 //
    787 qed.
    788 
    789 lemma eq_nth_safe_proof_irrelevant:
    790  ∀A,l,i,i_ok,i_ok'.
    791   nth_safe A l i i_ok = nth_safe A l i i_ok'.
    792 #A #l #i #i_ok #i_ok' %
    793 qed.
    794 
    795 (*CSC: move elsewhere *)
    796 axiom nat_of_bitvector_add:
    797  ∀n,v1,v2.
    798   nat_of_bitvector n v1 + nat_of_bitvector n v2 < 2^n →
    799    nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
    800 
    801 (*CSC: move elsewhere *)
    802 lemma fetch_pseudo_instruction_append:
    803  ∀l1,l2. |l1@l2| ≤ 2^16 → ∀ppc,ppc_ok,ppc_ok'.
    804   let code_newppc ≝ fetch_pseudo_instruction l2 ppc ppc_ok in
    805   fetch_pseudo_instruction (l1@l2) (add … (bitvector_of_nat … (|l1|)) (ppc)) ppc_ok' =
    806   〈\fst code_newppc, add … (bitvector_of_nat … (|l1|)) (\snd code_newppc)〉.
    807  #l1 #l2 #l1l2_ok #ppc #ppc_ok whd in match fetch_pseudo_instruction; normalize nodelta
    808  cut (|l1| + nat_of_bitvector … ppc < 2^16)
    809  [ @(transitive_le … l1l2_ok) >length_append @monotonic_lt_plus_r assumption ]
    810  -l1l2_ok #l1ppc_ok >nat_of_bitvector_add
    811  >nat_of_bitvector_bitvector_of_nat_inverse try assumption
    812  [2,3: @(transitive_le … l1ppc_ok) @le_S_S // ]
    813  #ppc_ok' <nth_safe_prepend try assumption cases (nth_safe labelled_instruction ???)
    814  #lbl #instr normalize nodelta >add_associative %
    815 qed.
    816 
    817695definition sigma_policy_specification ≝
    818696  λprogram: pseudo_assembly_program.
     
    832710      (  (nat_of_bitvector … ppc < |instr_list| → nat_of_bitvector … pc < nat_of_bitvector … next_pc)
    833711       ∨ (nat_of_bitvector … ppc = |instr_list| → next_pc = (zero …))).
    834 
    835 (*CSC: Move elsewhere *)
    836 axiom lt_nat_of_bitvector: ∀n.∀w. nat_of_bitvector n w < 2^n.
    837712
    838713definition assembly:
Note: See TracChangeset for help on using the changeset viewer.