# Changeset 2111 for src/ASM/AssemblyProof.ma

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

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

File:
1 edited

Unmodified
Added
Removed
• ## src/ASM/AssemblyProof.ma

 r2110 include "ASM/StatusProofs.ma". include alias "arithmetics/nat.ma". definition bit_elim_prop: ∀P: bool → Prop. Prop ≝ λP. P true ∧ P false. let rec bitvector_elim_prop_internal (n: nat) (P: BitVector n → Prop) (m: nat) on m: m ≤ n → BitVector (n - m) → Prop ≝ match m return λm. m ≤ n → BitVector (n - m) → Prop with [ O    ⇒ λprf1. λprefix. P ? | S n' ⇒ λprf2. λprefix. bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …) ]. try applyS prefix try (@le_S_to_le assumption) letin res ≝ (bit ::: prefix) minus_Sn_m assumption qed. definition bitvector_elim_prop ≝ λn: nat. λP: BitVector n → Prop. bitvector_elim_prop_internal n P n ? ?. try @le_n reflex #H %) #m' #hd #tl #inductive_hypothesis normalize cases (eq ??) normalize nodelta try (#irrelevant %) @inductive_hypothesis qed. cases v try % #n' #hd #tl % qed. corollary subvector_hd_tl: ∀A: Type[0]. ∀o: nat. ∀eq: A → A → bool. ∀refl: ∀a. eq a a = true. ∀h: A. ∀v: Vector A o. bool_to_Prop (subvector_with A ? ? eq v (h ::: v)). #A #o #eq #reflex #h #v >(vector_cons_append … h v) <(vector_cons_empty … ([[h]] @@ v)) @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]]) qed. ] qed. definition product_elim ≝ λm, n: nat. λv: Vector addressing_mode_tag (S m). λq: Vector addressing_mode_tag (S n). λP: (v × q) → bool. list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)). definition union_elim ≝ λA, B: Type[0]. λelimA: (A → bool) → bool. λelimB: (B → bool) → bool. λelimU: A ⊎ B → bool. elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))). (* definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝ λP. list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧ list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧ list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧ list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧ P (DA ? ACC_A) ∧ bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧ bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧ list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧ P (RL ? ACC_A) ∧ P (RLC ? ACC_A) ∧ P (RR ? ACC_A) ∧ P (RRC ? ACC_A) ∧ P (SWAP ? ACC_A) ∧ P (RET ?) ∧ P (RETI ?) ∧ P (NOP ?) ∧ bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧ list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧ bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧ bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧ union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]]) (product_elim ? ? [[ registr; indirect ]] [[ data ]]) (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧ list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧ union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]]) (λd. P (XRL ? d)) ∧ union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]])) (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) (λd. P (ANL ? d)) ∧ union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]]) (product_elim ? ? [[direct]] [[ acc_a ; data ]])) (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]]) (λd. P (ORL ? d)) ∧ union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]]) (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]]) (λd. P (MOVX ? d)) ∧ union_elim ? ? ( union_elim ? ? ( union_elim ? ? ( union_elim ? ? ( union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]]) (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]])) (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]])) (product_elim ? ? [[dptr]] [[data16]])) (product_elim ? ? [[carry]] [[bit_addr]])) (product_elim ? ? [[bit_addr]] [[carry]]) (λd. P (MOV ? d)). % qed. definition instruction_elim: ∀P: instruction → bool. bool ≝ λP. (* bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧ bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧ bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧ bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *) bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧ P (JMP INDIRECT_DPTR) ∧ list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧ preinstruction_elim (λp. P (RealInstruction p)). *) % qed. axiom instruction_elim_complete: ∀P. instruction_elim P = true → ∀i. P i = true. *) (*definition eq_instruction ≝ λi, j: instruction. true.*) definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
Note: See TracChangeset for help on using the changeset viewer.