Changeset 1575 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 29, 2011, 2:21:39 PM (9 years ago)
Author:
mulligan
Message:

Changes to specifications on execute functions

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1573 r1575  
    249249qed.
    250250
    251 lemma current_instruction_cost_non_zero:
     251axiom current_instruction_cost_non_zero:
    252252  ∀s: Status.
    253253    current_instruction_cost s > 0.
    254   #s
    255   cases s
    256   #code_memory #hi_ram #lo_ram #x_ram #pc #sfr_8051 #sfr_8052 #p1_latch
    257   #p2_latch #clock
    258   change with (\snd  (fetch ? ?)) in ⊢ (?%?);
    259   change with (fetch0 ? ?) in match (fetch ? ?);
    260   change with (
    261      let 〈pc,v〉 ≝ next code_memory pc in 
    262      let 〈b,v0〉 ≝head bool 7 v in
    263        ?) in match (fetch0 ? ?);
    264   normalize nodelta;
    265 
    266   cases(fetch (code_memory … s) (program_counter … s))
    267   #instruction_pc
    268   cases(instruction_pc)
    269   #instruction #pc
    270   cases(instruction)
    271   [ #addr11
    272254
    273255lemma le_monotonic_plus:
    274256  ∀m, n, o: nat.
    275257    m ≤ n → m + o ≤ n + o.
    276   #m #n #o #hyp
    277   elim o
    278   [ //
    279   | #o' #ind_hyp
    280     <plus_n_Sm <plus_n_Sm
    281     @le_S_S
    282     assumption
    283   ]
     258  #m #n #o #hyp /2/
    284259qed.
    285260
     
    296271  ∀m, n, o.
    297272    m - n = o → o > 0 → n ≤ m.
     273(*  #m #n #o #eq_hyp <eq_hyp in ⊢ (% → ?);
     274  normalize in ⊢ (% → ?);
     275  >le_monot *)
    298276
    299277let rec compute_max_trace_label_label_cost_is_ok
Note: See TracChangeset for help on using the changeset viewer.