Changeset 1613 for src/ASM


Ignore:
Timestamp:
Dec 14, 2011, 4:41:31 PM (8 years ago)
Author:
sacerdot
Message:

Coercion moved to Matita standard lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Assembly.ma

    r1609 r1613  
    640640qed. 
    641641
    642 lemma coerc_pair_sigma:
    643  ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x).
    644 #A #B #P * #a #b #p % [@a | /2/]
    645 qed.
    646 coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x)
    647 ≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)).
    648 
    649642definition create_label_map: ∀program:list labelled_instruction.
    650643  ∀policy:jump_expansion_policy.
     
    20172010    eq_identifier tag l r = false → (l = r → False).
    20182011
     2012include "basics/russell.ma".
     2013
     2014lemma weird: ∀A,B,P. (Σx:A × B. P x) → True.
     2015 #A #B #P #c
     2016 letin H ≝ (let 〈a,b〉 ≝ c in b)
     2017 check H
     2018
    20192019definition build_maps:
    20202020 ∀pseudo_program.∀pol:policy pseudo_program.
     
    20392039                  lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id)))
    20402040                (\snd pseudo_program)
    2041         (λprefix,i,tl,prf,t.
     2041        (λprefix,i,tl,prf,t. ?(*
    20422042          let 〈labels, ppc_pc_costs〉 ≝ t in
    20432043          let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in
     
    20532053          in
    20542054            let construct ≝ construct_costs pseudo_program pol ppc pc costs i' in
    2055               〈labels, 〈S ppc,construct〉〉) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
     2055              〈labels, 〈S ppc,construct〉〉*)) 〈empty_map …, 〈0, 〈0, Stub ? ?〉〉〉
    20562056    in
    20572057      let 〈labels, ppc_pc_costs〉 ≝ result in
    20582058      let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in
    20592059      let 〈pc, costs〉 ≝ pc_costs in
    2060         〈labels, costs〉.
     2060        〈labels, ?(*costs*)〉.
     2061 [2: check result
    20612062 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2
    20622063   generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
Note: See TracChangeset for help on using the changeset viewer.