Changeset 2529 for src/joint/semanticsUtils.ma
- Timestamp:
- Dec 4, 2012, 6:16:25 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/semanticsUtils.ma
r2470 r2529 75 75 mk_sem_params 76 76 g_pars 77 (mk_more_sem_params 78 g_pars 79 (spars ?) 80 (word_of_identifier ?) 81 (an_identifier ?) 82 ? (refl …) 83 ). 77 (spars ?) 78 (word_of_identifier ?) 79 (an_identifier ?) 80 ? (refl …). 84 81 * #p % qed. 85 82 … … 89 86 @pos_elim [%] 90 87 #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. 91 92 88 93 89 definition make_sem_lin_params : … … 99 95 mk_sem_params 100 96 lin_pars 101 (mk_more_sem_params 102 lin_pars 103 (spars ?) 104 succ_pos_of_nat 105 (λp.pred (nat_of_pos p)) 106 ?? 107 ). 108 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 109 | #n >nat_succ_pos % 97 (spars ?) 98 succ_pos_of_nat 99 (λp.pred (nat_of_pos p)) 100 ??. 101 [ #n >nat_succ_pos % 102 | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 110 103 ] qed. 104 105 106 107 108 lemma fetch_statement_eq : ∀p:sem_params.∀g. 109 ∀ge : genv_t (joint_function p g).∀ptr : program_counter. 110 ∀i,fn,s. 111 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → 112 let pt ≝ point_of_pc … ptr in 113 stmt_at … (joint_if_code … fn) pt = Some ? s → 114 fetch_statement … ge ptr = OK … 〈i, fn, s〉. 115 #p #g #ge #ptr #i #f #s #EQ1 #EQ2 116 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind 117 >EQ2 % 118 qed. 119 120 lemma fetch_statement_inv : ∀p:sem_params.∀g. 121 ∀ge : genv_t (joint_function p g).∀ptr : program_counter. 122 ∀i,fn,s. 123 fetch_statement … ge ptr = OK … 〈i, fn, s〉 → 124 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧ 125 let pt ≝ point_of_pc p ptr in 126 stmt_at … (joint_if_code … fn) pt = Some ? s. 127 #p #g #ge #ptr #i #fn #s #H 128 elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H 129 elim (bind_inversion ????? H) #s' * #H 130 lapply (opt_eq_from_res ???? H) -H #EQ2 131 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} 132 qed. 133
Note: See TracChangeset
for help on using the changeset viewer.