Changeset 2855


Ignore:
Timestamp:
Mar 12, 2013, 6:51:15 PM (4 years ago)
Author:
piccolo
Message:

little bug fixed in TranslateUtils?.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2851 r2855  
    184184include "joint/semantics_blocks.ma".
    185185include "ASM/Util.ma".
     186include "joint/StatusSimulationHelper.ma".
    186187
    187188lemma eval_cond_ok :
     
    209210bool_to_Prop (taaf_non_empty … taf).
    210211#fix_comp #colour #prog #f_lbls #f_regs #f_bl_r #good #st1 #st2 #st1' #f #fn #a
    211 #ltrue #lfalse #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
     212#ltrue #lfalse #Rst1st2 #EQfetch #EQeval
     213@(general_eval_cond_ok … good … Rst1st2 … EQfetch EQeval)
     214whd #lbl whd #mid1 normalize nodelta
     215letin LTL_prog_params ≝ (mk_prog_params LTL_semantics ??)
     216
     217
     218 whd in match eval_state; normalize nodelta
    212219>EQfetch >m_return_bind
    213220whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
  • src/joint/StatusSimulationHelper.ma

    r2851 r2855  
    3434qed.
    3535
    36 let rec bind_new_arity (B : Type[0]) (b : B) (E : Type[0]) (x : bind_new B E) on x : ℕ ≝
    37 match x with
    38 [bret y ⇒ 0
    39 |bnew f ⇒ 1 + bind_new_arity … b … (f b)
    40 ].
    4136
    42 lemma bcompile_ok : ∀U,R,E,fresh,b.
     37lemma bind_new_bind_new_instantiates :
     38∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P.
     39bind_new_instantiates B X x m l → bind_new_P' ?? P m →
     40P l x.
     41#B #X #m elim m normalize nodelta
     42[#x #y * normalize // #B #l' #P *
     43| #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H)
     44 @Hr
     45]
     46qed.
    4347
    4448
    45 lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     49lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
    4650∀prog : joint_program P_in.
    4751∀stack_sizes.
     
    5660∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
    5761R st1 st2 →
     62let step ≝ (COND P_in ? a ltrue) in
     63bind_new_P' ??
     64 (λregs1.λdata.∀lbl.bind_new_P' ??
     65  (λregs2.λblp.
     66   (∀mid1.∃st2'.
     67     repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? (\fst (\fst blp)) mid1) (st_no_pc … st2)
     68     = return (st_no_pc … st2') ∧
     69     pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
     70     last_pop … st2' = last_pop … st2)
     71   ) (f_step ??? data lbl step)   
     72  ) (init ? fn) →
    5873 fetch_statement P_in …
    5974  (globalenv_noinit ? prog) (pc … st1) =
    60     return 〈f, fn,  sequential … (COND P_in … a ltrue) lfalse〉 →
     75    return 〈f, fn,  sequential … step lfalse〉 →
    6176 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    6277            st1 = return st1' →
    6378as_costed (joint_abstract_status prog_pars_in) st1' →
    64 (*(∀mid1.∃st2'.
    65    repeat_eval_seq_no_pc prog_pars_out f (map_eval ?? blp mid1) (st_no_pc … st2)
    66            = return (st_no_pc … st2') ∧
    67            pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
    68            last_pop … st2' = last_pop … st2)) → *)
    6979∃ st2'. R st1' st2' ∧
    7080∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.
    7181bool_to_Prop (taaf_non_empty … taf).
    7282#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st1 #st1' #st2
    73 #f #fn #a #ltrue #lfalse #R #Rst1st2 #EQfetch whd in match eval_state; normalize nodelta
     83#f #fn #a #ltrue #lfalse #R #Rst1st2 #Hb_graph #EQfetch whd in match eval_state; normalize nodelta
    7484>EQfetch >m_return_bind
    7585whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     
    99109           pc … st2' = (pc_of_point P_out (pc_block (pc … st2)) mid1) ∧
    100110           last_pop … st2' = last_pop … st2)
    101    [2,4: cases daemon (* THE EXTENSIONAL PROOF *) ]
     111   [2,4: assumption ]
    102112#st2_pre_mid ** #res_st2_pre_mid #EQpc_st2_pre_mid #EQlast_pop_st2_pre_mid
    103113>(pc_block_eq_sigma_commute … good … Rst1st2) in EQt_fn1; #EQt_fn1
     
    129139|*: <EQpc_st2_pre_mid <EQlast_pop_st2_pre_mid assumption
    130140]
    131 qed.
     141qed.*)
  • src/joint/TranslateUtils.ma

    r2843 r2855  
    378378[ bret x ⇒ P [ ] x
    379379| bnew f ⇒
    380   ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r)
     380  ∀r.bind_new_P' R X (λl.P (r::l)) (f r)
    381381].
    382382
Note: See TracChangeset for help on using the changeset viewer.