Changeset 1928 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1927 r1928  
    6262
    6363include alias "arithmetics/nat.ma".
    64 
    65 lemma execute_1_ok_clock:
    66   ∀cm.
    67   ∀s.
    68     clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
    69   #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
    70 qed-.
    7164
    7265let rec compute_max_trace_label_label_cost_is_ok
     
    338331include alias "basics/logic.ma".
    339332
    340 lemma and_intro_right:
    341   ∀a, b: Prop.
    342     a → (a → b) → a ∧ b.
    343   #a #b /3/
    344 qed.
    345 
    346 lemma lt_m_n_to_exists_o_plus_m_n:
    347   ∀m, n: nat.
    348     m < n → ∃o: nat. m + o = n.
    349   #m #n
    350   cases m
    351   [1:
    352     #irrelevant
    353     %{n} %
    354   |2:
    355     #m' #lt_hyp
    356     %{(n - S m')}
    357     >commutative_plus in ⊢ (??%?);
    358     <plus_minus_m_m
    359     [1:
    360       %
    361     |2:
    362       @lt_S_to_lt
    363       assumption
    364     ]
    365   ]
    366 qed.
    367 
    368 lemma lt_O_n_to_S_pred_n_n:
    369   ∀n: nat.
    370     0 < n → S (pred n) = n.
    371   #n
    372   cases n
    373   [1:
    374     #absurd
    375     cases(lt_to_not_zero 0 0 absurd)
    376   |2:
    377     #n' #lt_hyp %
    378   ]
    379 qed.
    380 
    381 lemma exists_plus_m_n_to_exists_Sn:
    382   ∀m, n: nat.
    383     m < n → ∃p: nat. S p = n.
    384   #m #n
    385   cases m
    386   [1:
    387     #lt_hyp %{(pred n)}
    388     @(lt_O_n_to_S_pred_n_n … lt_hyp)
    389   |2:
    390     #m' #lt_hyp %{(pred n)}
    391     @(lt_O_n_to_S_pred_n_n)
    392     @(transitive_le … (S m') …)
    393     [1:
    394       //
    395     |2:
    396       @lt_S_to_lt
    397       assumption
    398     ]
    399   ]
    400 qed.
    401 
    402333include alias "arithmetics/bigops.ma".
    403334
     
    513444qed.
    514445
    515 
    516446definition tech_cost_of_label:
    517447 ∀cost_labels: BitVectorTrie costlabel 16.
     
    595525qed.
    596526   
    597 (* XXX: here *)
    598527let rec compute_trace_label_return_using_paid_ok_with_trace
    599528 (cm: ?) (total_program_size: nat) (total_program_size_limit: total_program_size ≤ 2^16)
Note: See TracChangeset for help on using the changeset viewer.