 Timestamp:
 Feb 16, 2012, 6:05:56 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1705 r1706 985 985 986 986 inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ 987  stlb_refl : ∀l,n,H. is_cost_label (lookup_present … g l H) → steps_to_label_bound g l (S n)988 987  stlb_step : ∀l,n,H. 989 988 let stmt ≝ lookup_present … g l H in 990 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → steps_to_label_bound g l' n) → 989 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → 990 (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨ 991 steps_to_label_bound g l' n) → 991 992 steps_to_label_bound g l (steps_for_statement stmt + n). 993 994 lemma steps_to_label_bound_inv : ∀g,l,n. 995 steps_to_label_bound g l n → 996 ∀H. let stmt ≝ lookup_present … g l H in 997 ∃n'. n = steps_for_statement stmt + n' ∧ 998 (∀l'. Exists label (λl0. l0 = l') (successors stmt) → 999 (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨ 1000 steps_to_label_bound g l' n'). 1001 #g #l0 #n0 #S inversion S #l #n #H #IH #E1 #E2 #_ destruct #H' 1002 % [2: % [ @refl  #l' #EX cases (IH l' EX) /2/ ]  skip ] 1003 qed. 992 1004 993 1005 discriminator nat. 994 995 lemma steps_to_label_bound_inv_step : ∀g,l,n.996 steps_to_label_bound g l n →997 ∀H.998 let stmt ≝ lookup_present … g l H in999 ¬ (bool_to_Prop (is_cost_label stmt)) →1000 (∀l'. Exists label (λl0. l0 = l') (successors stmt) →1001 ∃n'. n = n' + steps_for_statement stmt ∧1002 steps_to_label_bound g l' n').1003 #g #l0 #n0 #H1 inversion H11004 [ #l #n #H2 #C #E1 #E2 #_ destruct #H3 #H4 @⊥ @(absurd ? C H4)1005  #l #n #H2 #IH #_ #E1 #E2 #_ destruct #H3 #NC #l' #EX1006 % [2: % [ @commutative_plus  @IH // ] ]1007 ] qed.1008 1006 1009 1007 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. … … 1037 1035 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct 1038 1036 inversion H52 1039 [ #H60 #H61 #H62 #H63 #H64 #H65 #H66 destruct 1040  #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 normalize in H74; destruct 1041 ] 1037 #H68 #H69 #H70 #H71 #H72 #H73 #H74 normalize in H73; destruct 1042 1038  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct 1043 1039  #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct … … 1075 1071 state_steps_to_label_bound s (S n) → 1076 1072 eval_statement ge s = Value ??? 〈tr, s'〉 → 1077 RTLabs_cost s = false →1073 RTLabs_cost s' = false → 1078 1074 (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ 1079 1075 state_steps_to_label_bound s' n. … … 1083 1079 [ /3/ 1084 1080  * #l * #S1 #S2 #NC %2 1085 cases (steps_to_label_bound_inv_step … FS … l S2) 1086 [ 2: change with (RTLabs_cost (State f fs m)) in ⊢ (?(?%)); >NC % // ] 1081 cases (steps_to_label_bound_inv … FS ?) [2: @(next_ok f) ] 1087 1082 #n' 1088 1083 inversion (eval_perserves … EVAL) 1089 1084 [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct 1090 >(eval_steps … EVAL) * >commutative_plus #En normalize in En; 1091 whd in S1:(??%?); 1085 >(eval_steps … EVAL) * #En normalize in En; 1092 1086 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1093 %1 @H 1087 whd in S1:(??%?); destruct 1088 %1 cases (H l S2) 1089 [ * #LP 1090 change with (RTLabs_cost (State (mk_frame H1 H7 l H9 H5 H6) fs' m')) in ⊢ (?% → ?); 1091 >NC * 1092  // 1093 ] 1094 1094  #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct 1095 >(eval_steps … EVAL) * >commutative_plus #En normalize in En; 1096 whd in S1:(??%?); 1095 >(eval_steps … EVAL) * #En normalize in En; 1097 1096 #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct 1098 %2 // 1097 %2 whd lapply (H l S2) 1098 @FS // 1099 1099  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 1100 1100 destruct
Note: See TracChangeset
for help on using the changeset viewer.