source: src/joint/lineariseProof.ma @ 2443

Last change on this file since 2443 was 2443, checked in by tranquil, 7 years ago

changed joint's stack pointer and internal stack

File size: 2.1 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.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 p p')
30    prog).
31
32definition lin_abstract_status:
33 ∀p:unserialized_params.
34  (∀F.sem_unserialized_params p F) →
35    joint_program (mk_lin_params p) →
36     abstract_status
37 ≝
38 λp,p',prog.
39  joint_abstract_status
40   (mk_prog_params
41    (make_sem_lin_params p p')
42    prog).
43
44definition linearise_status_rel:
45 ∀p,p',graph_prog.
46  let lin_prog ≝ linearise ? graph_prog in
47   status_rel
48    (graph_abstract_status p p' graph_prog)
49    (lin_abstract_status p p' lin_prog).
50 cases daemon
51qed.
52
53lemma linearise_ok:
54 ∀p,p',graph_prog.
55  let lin_prog ≝ linearise ? graph_prog in
56   status_simulation
57    (graph_abstract_status p p' graph_prog)
58    (lin_abstract_status p p' lin_prog) ≝
59 λp,p',graph_prog. mk_status_simulation … (linearise_status_rel p p' graph_prog) ….
60 cases daemon
61qed.
Note: See TracBrowser for help on using the repository browser.