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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2110 r2111  
    33include "ASM/StatusProofs.ma".
    44include alias "arithmetics/nat.ma".
    5 
    6 definition bit_elim_prop: ∀P: bool → Prop. Prop ≝
    7   λP.
    8     P true ∧ P false.
    9  
    10 let rec bitvector_elim_prop_internal
    11   (n: nat) (P: BitVector n → Prop) (m: nat)
    12     on m:
    13       m ≤ n → BitVector (n - m) → Prop ≝
    14   match m return λm. m ≤ n → BitVector (n - m) → Prop with
    15   [ O    ⇒ λprf1. λprefix. P ?
    16   | S n' ⇒ λprf2. λprefix.
    17       bit_elim_prop (λbit. bitvector_elim_prop_internal n P n' …)
    18   ].
    19   try applyS prefix
    20   try (@le_S_to_le assumption)
    21   letin res ≝ (bit ::: prefix)
    22   <minus_S_S >minus_Sn_m
    23   assumption
    24 qed.
    25 
    26 definition bitvector_elim_prop ≝
    27   λn: nat.
    28   λP: BitVector n → Prop.
    29     bitvector_elim_prop_internal n P n ? ?.
    30   try @le_n
    31   <minus_n_n @[[ ]]
    32 qed.
    33 
    34 lemma bool_eq_internal_eq:
    35   ∀b, c.
    36     (λb. λc. (if b then c else (if c then false else true))) b c = true → b = c.
    37   #b #c
    38   cases b cases c normalize nodelta
    39   try (#_ % @I)
    40   #assm destruct %
    41 qed.
    425
    436definition bit_elim: ∀P: bool → bool. bool ≝
     
    6225  try @le_n
    6326  <minus_n_n @[[]]
    64 qed.
    65 
    66 lemma mem_middle_vector:
    67   ∀A: Type[0].
    68   ∀m, o: nat.
    69   ∀eq: A → A → bool.
    70   ∀reflex: ∀a. eq a a = true.
    71   ∀p: Vector A m.
    72   ∀a: A.
    73   ∀r: Vector A o.
    74     mem A eq ? (p@@(a:::r)) a = true.
    75   #A #m #o #eq #reflex #p #a
    76   elim p try (normalize >reflex #H %)
    77   #m' #hd #tl #inductive_hypothesis
    78   normalize
    79   cases (eq ??) normalize nodelta
    80   try (#irrelevant %)
    81   @inductive_hypothesis
    8227qed.
    8328
     
    13681  cases v try %
    13782  #n' #hd #tl %
    138 qed.
    139 
    140 corollary subvector_hd_tl:
    141   ∀A: Type[0].
    142   ∀o: nat.
    143   ∀eq: A → A → bool.
    144   ∀refl: ∀a. eq a a = true.
    145   ∀h: A.
    146   ∀v: Vector A o.
    147     bool_to_Prop (subvector_with A ? ? eq v (h ::: v)).
    148   #A #o #eq #reflex #h #v
    149   >(vector_cons_append … h v)
    150   <(vector_cons_empty … ([[h]] @@ v))
    151   @(subvector_multiple_append … eq reflex [[ ]] v ? [[h]])
    15283qed.
    15384
     
    236167  ]
    237168qed.
    238 
    239 definition product_elim ≝
    240   λm, n: nat.
    241   λv: Vector addressing_mode_tag (S m).
    242   λq: Vector addressing_mode_tag (S n).
    243   λP: (v × q) → bool.
    244     list_addressing_mode_tags_elim ? v (λx. list_addressing_mode_tags_elim ? q (λy. P 〈x, y〉)).
    245 
    246 definition union_elim ≝
    247   λA, B: Type[0].
    248   λelimA: (A → bool) → bool.
    249   λelimB: (B → bool) → bool.
    250   λelimU: A ⊎ B → bool.
    251     elimA (λa. elimB (λb. elimU (inl ? ? a) ∧ elimU (inr ? ? b))).
    252 
    253 (*                           
    254 definition preinstruction_elim: ∀P: preinstruction [[ relative ]] → bool. bool ≝
    255   λP.
    256     list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADD ? ACC_A addr)) ∧
    257     list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (ADDC ? ACC_A addr)) ∧
    258     list_addressing_mode_tags_elim ? [[ registr ; direct ; indirect ; data ]] (λaddr. P (SUBB ? ACC_A addr)) ∧
    259     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ; dptr ]] (λaddr. P (INC ? addr)) ∧
    260     list_addressing_mode_tags_elim ? [[ acc_a ; registr ; direct ; indirect ]] (λaddr. P (DEC ? addr)) ∧
    261     list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (MUL ? ACC_A addr)) ∧
    262     list_addressing_mode_tags_elim ? [[acc_b]] (λaddr. P (DIV ? ACC_A addr)) ∧
    263     list_addressing_mode_tags_elim ? [[ registr ; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    264     list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CLR ? addr)) ∧
    265     list_addressing_mode_tags_elim ? [[ acc_a ; carry ; bit_addr ]] (λaddr. P (CPL ? addr)) ∧
    266     P (DA ? ACC_A) ∧
    267     bitvector_elim 8 (λr. P (JC ? (RELATIVE r))) ∧
    268     bitvector_elim 8 (λr. P (JNC ? (RELATIVE r))) ∧
    269     bitvector_elim 8 (λr. P (JZ ? (RELATIVE r))) ∧
    270     bitvector_elim 8 (λr. P (JNZ ? (RELATIVE r))) ∧
    271     bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    272     bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JNB ? (BIT_ADDR b) (RELATIVE r))))) ∧
    273     bitvector_elim 8 (λr. (bitvector_elim 8 (λb: BitVector 8. P (JBC ? (BIT_ADDR b) (RELATIVE r))))) ∧
    274     list_addressing_mode_tags_elim ? [[ registr; direct ]] (λaddr. bitvector_elim 8 (λr. P (DJNZ ? addr (RELATIVE r)))) ∧
    275     P (RL ? ACC_A) ∧
    276     P (RLC ? ACC_A) ∧
    277     P (RR ? ACC_A) ∧
    278     P (RRC ? ACC_A) ∧
    279     P (SWAP ? ACC_A) ∧
    280     P (RET ?) ∧
    281     P (RETI ?) ∧
    282     P (NOP ?) ∧
    283     bit_elim (λb. P (XCHD ? ACC_A (INDIRECT b))) ∧
    284     list_addressing_mode_tags_elim ? [[ carry; bit_addr ]] (λaddr. P (SETB ? addr)) ∧
    285     bitvector_elim 8 (λaddr. P (PUSH ? (DIRECT addr))) ∧
    286     bitvector_elim 8 (λaddr. P (POP ? (DIRECT addr))) ∧
    287     union_elim ? ? (product_elim ? ? [[ acc_a ]] [[ direct; data ]])
    288                    (product_elim ? ? [[ registr; indirect ]] [[ data ]])
    289                    (λd. bitvector_elim 8 (λb. P (CJNE ? d (RELATIVE b)))) ∧
    290     list_addressing_mode_tags_elim ? [[ registr; direct; indirect ]] (λaddr. P (XCH ? ACC_A addr)) ∧
    291     union_elim ? ? (product_elim ? ? [[acc_a]] [[ data ; registr ; direct ; indirect ]])
    292                    (product_elim ? ? [[direct]] [[ acc_a ; data ]])
    293                    (λd. P (XRL ? d)) ∧
    294     union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
    295                                    (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
    296                    (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
    297                    (λd. P (ANL ? d)) ∧
    298     union_elim ? ? (union_elim ? ? (product_elim ? ? [[acc_a]] [[ registr ; data ; direct ; indirect ]])
    299                                    (product_elim ? ? [[direct]] [[ acc_a ; data ]]))
    300                    (product_elim ? ? [[carry]] [[ bit_addr ; n_bit_addr]])
    301                    (λd. P (ORL ? d)) ∧
    302     union_elim ? ? (product_elim ? ? [[acc_a]] [[ ext_indirect ; ext_indirect_dptr ]])
    303                    (product_elim ? ? [[ ext_indirect ; ext_indirect_dptr ]] [[acc_a]])
    304                    (λd. P (MOVX ? d)) ∧
    305     union_elim ? ? (
    306       union_elim ? ? (
    307         union_elim ? ? (
    308           union_elim ? ? (
    309             union_elim ? ?  (product_elim ? ? [[acc_a]] [[ registr ; direct ; indirect ; data ]])
    310                             (product_elim ? ? [[ registr ; indirect ]] [[ acc_a ; direct ; data ]]))
    311                             (product_elim ? ? [[direct]] [[ acc_a ; registr ; direct ; indirect ; data ]]))
    312                             (product_elim ? ? [[dptr]] [[data16]]))
    313                             (product_elim ? ? [[carry]] [[bit_addr]]))
    314                             (product_elim ? ? [[bit_addr]] [[carry]])
    315                             (λd. P (MOV ? d)).
    316   %
    317 qed.
    318  
    319 definition instruction_elim: ∀P: instruction → bool. bool ≝
    320   λP. (*
    321     bitvector_elim 11 (λx. P (ACALL (ADDR11 x))) ∧
    322     bitvector_elim 16 (λx. P (LCALL (ADDR16 x))) ∧
    323     bitvector_elim 11 (λx. P (AJMP (ADDR11 x))) ∧
    324     bitvector_elim 16 (λx. P (LJMP (ADDR16 x))) ∧ *)
    325     bitvector_elim 8 (λx. P (SJMP (RELATIVE x))). (*  ∧
    326     P (JMP INDIRECT_DPTR) ∧
    327     list_addressing_mode_tags_elim ? [[ acc_dptr; acc_pc ]] (λa. P (MOVC ACC_A a)) ∧
    328     preinstruction_elim (λp. P (RealInstruction p)). *)
    329   %
    330 qed.
    331 
    332 
    333 axiom instruction_elim_complete:
    334  ∀P. instruction_elim P = true → ∀i. P i = true.
    335 *)
    336 (*definition eq_instruction ≝
    337   λi, j: instruction.
    338     true.*)
    339169
    340170definition eq_addressing_mode: addressing_mode → addressing_mode → bool ≝
Note: See TracChangeset for help on using the changeset viewer.