source: src/joint/lineariseProof.ma @ 2442

Last change on this file since 2442 was 2442, checked in by piccolo, 7 years ago

Traces repaired. (By Paolo)
Statement of lineariseProof in place.

File size: 2.3 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/linearise.ma".
16include "common/StatusSimulation.ma".   
17include "joint/Traces.ma".
18include "joint/SemanticUtils.ma".
19
20definition graph_abstract_status:
21 ∀p:unserialized_params.
22  (∀F.more_sem_unserialized_params p F) →
23    joint_program (mk_graph_params p) →
24     abstract_status
25 ≝
26 λp,p',prog.
27  joint_abstract_status
28   (mk_prog_params
29    (make_sem_graph_params (mk_graph_params p) (p' ?))
30    prog ⊥).
31@daemon (* I/O, TODO *)
32qed.
33
34definition lin_abstract_status:
35 ∀p:unserialized_params.
36  (∀F.more_sem_unserialized_params p F) →
37    joint_program (mk_lin_params p) →
38     abstract_status
39 ≝
40 λp,p',prog.
41  joint_abstract_status
42   (mk_prog_params
43    (make_sem_lin_params (mk_lin_params p) (p' ?))
44    prog ⊥).
45@daemon (* I/O, TODO *)
46qed.
47
48definition linearise_status_rel:
49 ∀p,p',graph_prog.
50  let lin_prog ≝ linearise ? graph_prog in
51   status_rel
52    (graph_abstract_status p p' graph_prog)
53    (lin_abstract_status p p' lin_prog).
54 cases daemon
55qed.
56
57lemma linearise_ok:
58 ∀p,p',graph_prog.
59  let lin_prog ≝ linearise ? graph_prog in
60   status_simulation
61    (graph_abstract_status p p' graph_prog)
62    (lin_abstract_status p p' lin_prog) ≝
63 λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) ….
64 cases daemon
65qed.
Note: See TracBrowser for help on using the repository browser.