1
2(*****************************************************************************)
3(* Create "RewritesTheory" with rewrites semantics from LRM Version 1.1      *)
4(*****************************************************************************)
5
6(*****************************************************************************)
7(* START BOILERPLATE                                                         *)
8(*****************************************************************************)
9
10(*
11quietdec := true;
12map load
13 ["SyntacticSugarTheory","ClockedSemanticsTheory"];
14quietdec := false;
15*)
16
17(******************************************************************************
18* Boilerplate needed for compilation
19******************************************************************************)
20open HolKernel Parse boolLib bossLib;
21
22(******************************************************************************
23* Open theories
24******************************************************************************)
25open SyntacticSugarTheory ClockedSemanticsTheory;
26
27(*****************************************************************************)
28(* END BOILERPLATE                                                           *)
29(*****************************************************************************)
30
31(******************************************************************************
32* Start a new theory called UnclockedSugarSemantics
33******************************************************************************)
34val _ = new_theory "Rewrites";
35
36(******************************************************************************
37* Version 1.1 rules for compiling clocked SEREs to unclocked SEREs
38******************************************************************************)
39val S_CLOCK_COMP_def =
40 Define
41  `(S_CLOCK_COMP c (S_BOOL b) =
42     (S_CAT (S_REPEAT (S_BOOL (B_NOT c)),S_BOOL(B_AND(c, b)))))
43   /\
44   (S_CLOCK_COMP c (S_CAT(r1,r2)) =
45     S_CAT(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
46   /\
47   (S_CLOCK_COMP c (S_FUSION(r1,r2)) =
48     S_FUSION(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
49   /\
50   (S_CLOCK_COMP c (S_OR(r1,r2)) =
51     S_OR(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
52   /\
53   (S_CLOCK_COMP c (S_AND(r1,r2))  =
54     S_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
55   /\
56   (S_CLOCK_COMP c S_EMPTY =
57     S_EMPTY)
58   /\
59   (S_CLOCK_COMP c (S_REPEAT r) =
60     S_REPEAT(S_CLOCK_COMP c r))
61   /\
62   (S_CLOCK_COMP c (S_CLOCK(r, c1)) =
63     S_CLOCK_COMP c1 r)`;
64
65(******************************************************************************
66* Some abbreviations needed for definition of F_CLOCK_COMP
67******************************************************************************)
68
69(******************************************************************************
70* Strongly on first posedge.
71* Exists a posedge and true on it: [!c U (c /\ f)]
72******************************************************************************)
73val F_U_CLOCK_def =
74 Define
75  `F_U_CLOCK c f = F_UNTIL(F_WEAK_BOOL(B_NOT c),F_AND(F_WEAK_BOOL c, f))`;
76
77(******************************************************************************
78* Weakly on first posedge.
79* On first posedge, if there is a posedge: [!c W (c /\ f)]
80******************************************************************************)
81val F_W_CLOCK_def =
82 Define
83  `F_W_CLOCK c f = F_W(F_WEAK_BOOL(B_NOT c),F_AND(F_WEAK_BOOL c, f))`;
84
85(******************************************************************************
86* Version 1.1 rules for compiling clocked formulas to unclocked formulas
87******************************************************************************)
88val F_CLOCK_COMP_def =
89 Define
90  `(F_CLOCK_COMP c (F_STRONG_BOOL b) =
91     F_U_CLOCK c (F_WEAK_BOOL b))
92   /\
93   (F_CLOCK_COMP c (F_WEAK_BOOL b) =
94     F_W_CLOCK c (F_WEAK_BOOL b))
95   /\
96   (F_CLOCK_COMP c (F_NOT f) =
97     F_NOT(F_CLOCK_COMP c f))
98   /\
99   (F_CLOCK_COMP c (F_AND(f1,f2)) =
100     F_AND(F_CLOCK_COMP c f1, F_CLOCK_COMP c f2))
101   /\
102   (F_CLOCK_COMP c (F_NEXT f) =
103     F_U_CLOCK c (F_NEXT(F_U_CLOCK c (F_CLOCK_COMP c f))))
104   /\
105   (F_CLOCK_COMP c (F_UNTIL(f1,f2)) =
106     F_UNTIL(F_IMPLIES(F_WEAK_BOOL c, F_CLOCK_COMP c f1),
107             F_AND(F_WEAK_BOOL c, F_CLOCK_COMP c f2)))
108   /\
109   (F_CLOCK_COMP c (F_ABORT (f,b)) =
110     F_ABORT(F_CLOCK_COMP c f, b))
111   /\
112   (F_CLOCK_COMP c (F_CLOCK(f,c1)) =
113     F_CLOCK_COMP c1 f)
114   /\
115   (F_CLOCK_COMP c (F_SUFFIX_IMP(r,f)) =
116     F_SUFFIX_IMP(S_CLOCK_COMP c r, F_CLOCK_COMP c f))
117   /\
118   (F_CLOCK_COMP c (F_STRONG_SERE r) =
119     F_STRONG_SERE(S_CLOCK_COMP c r))
120   /\
121   (F_CLOCK_COMP c (F_WEAK_SERE r) =
122     F_WEAK_SERE(S_CLOCK_COMP c r))`;
123
124
125val _ = export_theory();
126
127