Changeset 1976 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
May 21, 2012, 7:04:21 PM (8 years ago)
Author:
tranquil
Message:
  • monads: just changed some defs, which had to be propagated in some files
  • ASM/CostProof.ma: linked cost as defined there to the one in StructuredTraces? that uses fold
  • added a library for permutations of lists (useful with fold AC ops on lists)
  • first draft of abstract_status implementation for joint languages (file joint/as_semantics.ma)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1964 r1976  
    722722  @nat_of_bitvector_lt_bound
    723723qed.
     724
     725definition ASM_cost_map :
     726  ∀code_memory: BitVectorTrie Byte 16.
     727  ∀cost_labels: BitVectorTrie costlabel 16.
     728  ∀cost_map: identifier_map CostTag nat.
     729  (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k) →
     730  as_cost_map (ASM_abstract_status code_memory cost_labels) ≝
     731  λcode_memory,cost_labels,cost_map,codom_dom,l_sig.
     732  (lookup_present … cost_map (pi1 … l_sig) ?).
     733  cases l_sig #l * #pc @(codom_dom pc)
     734  qed.
     735 
     736include "utilities/permutations.ma".
     737
     738lemma tech_cost_sum_eq_as_cost :
     739  ∀code_memory: BitVectorTrie Byte 16.
     740  ∀cost_labels: BitVectorTrie costlabel 16.
     741  ∀cost_map: identifier_map CostTag nat.
     742  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
     743  ∀trace.
     744  (Σ_{i < |trace|}(tech_cost_of_label cost_labels cost_map codom_dom trace i)) =
     745  (Σ_{l ∈ trace}(ASM_cost_map code_memory … codom_dom l)).
     746#cmem #clab #cmap #codom_dom #trace
     747@(list_elim_left … trace)
     748[ %
     749| #tl #hd #IH >append_length >commutative_plus
     750  >(fold_permute … (hd@[tl]) (tl::hd)) [2: @perm_swap_append ]
     751  whd in ⊢ (??%%); <IH
     752  <tech_cost_of_label_shift [2: %]
     753  cut (∀x,y,z,w.x = y → z = w → x + z = y + w) [ // ] #APP @APP -APP
     754  [ %
     755  | @sym_eq @same_bigop /2 by tech_cost_of_label_prefix/
     756  ]
     757]
     758qed.
Note: See TracChangeset for help on using the changeset viewer.