Changeset 2226
 Timestamp:
 Jul 20, 2012, 6:36:34 PM (7 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/CostSpec.ma
r2218 r2226 76 76 77 77 definition well_cost_labelled_program : RTLabs_program → Prop ≝ 78 λp. All ? (λx. let 〈id,fd〉 ≝ x in 79 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn  _ ⇒ True]) (prog_funct … p). 78 λp. All ? (λx. match \snd x with [ Internal fn ⇒ 79 well_cost_labelled_fn fn ∧ soundly_labelled_fn fn 80  _ ⇒ True]) (prog_funct … p). 80 81 81 82 
src/RTLabs/Traces.ma
r2224 r2226 1942 1942 ] qed. 1943 1943 1944 lemma well_cost_labelled_initial : ∀p,s. 1945 make_initial_state p = OK ? s → 1946 well_cost_labelled_program p → 1947 well_cost_labelled_state s ∧ soundly_labelled_state s. 1948 #p #s 1949 @bind_ok #m #Em 1950 @bind_ok #b #Eb 1951 @bind_ok #f #Ef 1952 #E destruct 1953 whd in ⊢ (% → %); 1954 #WCL 1955 @(find_funct_ptr_All ??????? Ef) 1956 @(All_mp … WCL) 1957 * #id * /3/ #fn * #W #S % [ /2/  whd % // @S ] 1958 qed. 1959 1960 lemma well_cost_labelled_make_global : ∀p. 1961 well_cost_labelled_program p → 1962 well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p). 1963 #p whd in ⊢ (% → ?%%); 1964 #WCL % 1965 #b #f #FFP 1966 [ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f  _ ⇒ True]) FFP) 1967  @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f  _ ⇒ True]) FFP) 1968 ] @(All_mp … WCL) 1969 * #id * #fn // * /2/ 1970 qed. 1971 1944 1972 theorem program_trace_exists : 1945 1973 termination_oracle → 1946 1974 ∀p:RTLabs_program. 1975 well_cost_labelled_program p → 1947 1976 ∀s:state. 1948 1977 ∀I: make_initial_state p = OK ? s. … … 1957 1986 trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I). 1958 1987 1959 #ORACLE #p # s #I1988 #ORACLE #p #WCL #s #I 1960 1989 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p) 1961 1990 #NOIO #NW … … 1963 1992 whd 1964 1993 @(whole_structured_trace_exists (make_global p) p ? ORACLE) 1965 [ 3: @flat_trace  4: @I 1966  *: cases daemon 1994 [ @(proj1 … (well_cost_labelled_make_global … WCL)) 1995  @(proj2 … (well_cost_labelled_make_global … WCL)) 1996  @flat_trace 1997  @I 1998  @(proj1 ?? (well_cost_labelled_initial … I WCL)) 1999  @(proj2 ?? (well_cost_labelled_initial … I WCL)) 1967 2000 ] qed. 1968 2001 
src/common/Globalenvs.ma
r2185 r2226 548 548 ] 549 549 ] qed. 550 551 (* lazy proof *) 552 lemma find_funct_ptr_All : ∀A,V,b,p,f,initV,P. 553 find_funct_ptr … (globalenv A V initV p) b = Some ? f → 554 All ? (λx. P (\snd x)) (prog_funct ?? p) → 555 P f. 556 #A #V #b #p #f #initV #P #FFP #ALL 557 cut (All2 ?? (λx,y. P (\snd x)) (prog_funct ?? p) (prog_funct ?? p)) 558 [ elim (prog_funct … p) in ALL ⊢ %; 559 [ //  #h #t #IH * #Hh #Ht % /2/ ] ] 560 #ALL2 561 cases (find_funct_ptr_All2 A A V V b p f initV initV p ? FFP ALL2) 562 #x * // 563 qed. 564 550 565 551 566 discriminator Prod.
Note: See TracChangeset
for help on using the changeset viewer.