Ignore:
Timestamp:
Mar 16, 2013, 10:42:43 AM (7 years ago)
Author:
piccolo
Message:

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2883 r2891  
    160160
    161161include "joint/StatusSimulationHelper.ma".
     162include alias "basics/lists/listb.ma".
    162163
    163164lemma make_ERTL_To_ERTLptr_good_state_relation :
     
    209210  change with (pc_block (pc … st2)) in match (pc_block ?);
    210211  <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     212| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
     213  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
     214  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
     215  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ)
     216  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
     217  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     218  #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc'
     219  #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc')
     220  -EQst1_no_pc' #EQst1_no_pc'
     221  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
     222  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ)
     223  %{(mk_state_pc ? st2_no_pc'
     224     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt)
     225     (last_pop … st2))} %
     226     [ whd in ⊢ (??%?); >EQst2_no_pc' %
     227     | whd whd in match sigma_state_pc; normalize nodelta >EQfn %
     228     ]
     229  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
     230  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
     231  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     232                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
     233                 return 〈f,fn,stmt1〉)
     234   [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
     235  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
     236  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *]
     237  normalize nodelta #EQ destruct(EQ) * #labels * #registers
     238  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
     239  #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters
     240  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
     241         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     242  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
     243  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
     244   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     245  #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
     246  ]
    211247]
    212248qed.
Note: See TracChangeset for help on using the changeset viewer.