Changeset 1976 for src/ASM/CostsProof.ma
- Timestamp:
- May 21, 2012, 7:04:21 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/CostsProof.ma
r1964 r1976 722 722 @nat_of_bitvector_lt_bound 723 723 qed. 724 725 definition 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 736 include "utilities/permutations.ma". 737 738 lemma 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 ] 758 qed.
Note: See TracChangeset
for help on using the changeset viewer.