Changeset 2226 for src/RTLabs/Traces.ma

Timestamp:

Jul 20, 2012, 6:36:34 PM (9 years ago)

Author:

campbell

Message:

Whole program proof.

File:

• src/RTLabs/Traces.ma (modified) (3 diffs)

src/RTLabs/Traces.ma

@@ -1942 +1942 @@
 ] qed.
 
+lemma well_cost_labelled_initial : ∀p,s.
+  make_initial_state p = OK ? s →
+  well_cost_labelled_program p →
+  well_cost_labelled_state s ∧ soundly_labelled_state s.
+#p #s
+@bind_ok #m #Em
+@bind_ok #b #Eb
+@bind_ok #f #Ef
+#E destruct
+whd in ⊢ (% → %);
+#WCL
+@(find_funct_ptr_All ??????? Ef)
+@(All_mp … WCL)
+* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
+qed.
+
+lemma well_cost_labelled_make_global : ∀p.
+  well_cost_labelled_program p →
+  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
+#p whd in ⊢ (% → ?%%);
+#WCL %
+#b #f #FFP
+[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
+| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
+] @(All_mp … WCL)
+* #id * #fn // * /2/
+qed.
+
 theorem program_trace_exists :
   termination_oracle →
   ∀p:RTLabs_program.
+  well_cost_labelled_program p →
   ∀s:state.
   ∀I: make_initial_state p = OK ? s.
@@ -1957 +1986 @@
   trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
 
-#ORACLE #p #s #I
+#ORACLE #p #WCL #s #I
 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
 #NOIO #NW
@@ -1963 +1992 @@
 whd 
 @(whole_structured_trace_exists (make_global p) p ? ORACLE)
-[ 3: @flat_trace | 4: @I
-| *: cases daemon
+[ @(proj1 … (well_cost_labelled_make_global … WCL))
+| @(proj2 … (well_cost_labelled_make_global … WCL))
+| @flat_trace
+| @I
+| @(proj1 ?? (well_cost_labelled_initial … I WCL))
+| @(proj2 ?? (well_cost_labelled_initial … I WCL))
 ] qed.