Changeset 2226 for src/RTLabs/Traces.ma
- Timestamp:
- Jul 20, 2012, 6:36:34 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
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
Note: See TracChangeset
for help on using the changeset viewer.