Changeset 1613
 Timestamp:
 Dec 14, 2011, 4:41:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1609 r1613 640 640 qed. 641 641 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 649 642 definition create_label_map: ∀program:list labelled_instruction. 650 643 ∀policy:jump_expansion_policy. … … 2017 2010 eq_identifier tag l r = false → (l = r → False). 2018 2011 2012 include "basics/russell.ma". 2013 2014 lemma 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 2019 2019 definition build_maps: 2020 2020 ∀pseudo_program.∀pol:policy pseudo_program. … … 2039 2039 lookup_def … labels id (zero …) = sigma pseudo_program pol (address_of_word_labels_code_mem pre id))) 2040 2040 (\snd pseudo_program) 2041 (λprefix,i,tl,prf,t. 2041 (λprefix,i,tl,prf,t. ?(* 2042 2042 let 〈labels, ppc_pc_costs〉 ≝ t in 2043 2043 let 〈ppc, pc_costs〉 ≝ ppc_pc_costs in … … 2053 2053 in 2054 2054 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 ? ?〉〉〉 2056 2056 in 2057 2057 let 〈labels, ppc_pc_costs〉 ≝ result in 2058 2058 let 〈ppc,pc_costs〉 ≝ ppc_pc_costs in 2059 2059 let 〈pc, costs〉 ≝ pc_costs in 2060 〈labels, costs〉. 2060 〈labels, ?(*costs*)〉. 2061 [2: check result 2061 2062 [2: whd generalize in match (pi2 … t); >p >p1 >p2 >p3 * * * #IHn1 #IH0 #IH1 #IH2 2062 2063 generalize in match (refl … construct); cases construct in ⊢ (???% → %); #PC #CODE #JMEQ % [% [%]]
Note: See TracChangeset
for help on using the changeset viewer.