1
2(*****************************************************************************)
3(* Create "RewritesTheory" containing rewrites semantics (LRM B.5)           *)
4(*                                                                           *)
5(* Created Wed Jan 1 2003                                                    *)
6(*****************************************************************************)
7
8(*****************************************************************************)
9(* START BOILERPLATE                                                         *)
10(*****************************************************************************)
11
12(*
13quietdec := true;
14map load
15 ["SyntaxTheory", "SyntacticSugarTheory", "FinitePSLPathTheory", "PSLPathTheory",
16   "UnclockedSemanticsTheory","intLib","res_quanTools"];
17open SyntaxTheory SyntacticSugarTheory FinitePSLPathTheory PSLPathTheory
18     UnclockedSemanticsTheory
19     listTheory rich_listTheory intLib res_quanTools;
20val _ = intLib.deprecate_int();
21quietdec := false;
22*)
23
24(******************************************************************************
25* Boilerplate needed for compilation
26******************************************************************************)
27open HolKernel Parse boolLib bossLib;
28
29(******************************************************************************
30* Open theories
31******************************************************************************)
32open SyntaxTheory FinitePSLPathTheory PSLPathTheory UnclockedSemanticsTheory
33     SyntacticSugarTheory listTheory rich_listTheory intLib res_quanTools;
34
35(******************************************************************************
36* Set default parsing to natural numbers rather than integers
37******************************************************************************)
38val _ = intLib.deprecate_int();
39
40(*****************************************************************************)
41(* END BOILERPLATE                                                           *)
42(*****************************************************************************)
43
44(******************************************************************************
45* A simpset fragment to rewrite away quantifiers restricted with :: (a to b)
46******************************************************************************)
47val resq_SS =
48 simpLib.merge_ss
49  [res_quanTools.resq_SS,
50   rewrites
51    [num_to_def,xnum_to_def,IN_DEF,num_to_def,xnum_to_def,LENGTH_def]];
52
53(******************************************************************************
54* Start a new theory called UnclockedSugarSemantics
55******************************************************************************)
56val _ = new_theory "Rewrites";
57
58(******************************************************************************
59* SEM_1 rules for compiling clocked SEREs to unclocked SEREs
60******************************************************************************)
61val S_CLOCK_COMP_def =
62 Define
63  `(S_CLOCK_COMP c (S_BOOL b) =
64     (S_CAT (S_REPEAT (S_BOOL (B_NOT c)),S_BOOL(B_AND(c, b)))))
65   /\
66   (S_CLOCK_COMP c (S_CAT(r1,r2)) =
67     S_CAT(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
68   /\
69   (S_CLOCK_COMP c (S_FUSION(r1,r2)) =
70     S_FUSION(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
71   /\
72   (S_CLOCK_COMP c (S_OR(r1,r2)) =
73     S_OR(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
74   /\
75   (S_CLOCK_COMP c (S_AND(r1,r2))  =
76     S_AND(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
77   /\
78   (S_CLOCK_COMP c (S_REPEAT r) =
79     S_REPEAT(S_CLOCK_COMP c r))
80   /\
81   (S_CLOCK_COMP c (S_CLOCK(r, c1)) =
82     (S_CAT (S_REPEAT (S_BOOL (B_NOT c1)),
83             S_FUSION(S_BOOL c1, S_CLOCK_COMP c1 r))))`;
84
85(******************************************************************************
86* Some abbreviations needed for definition of F_CLOCK_COMP
87******************************************************************************)
88
89(******************************************************************************
90* Strongly on first posedge.
91* Exists a posedge and true on it: [!c U (c /\ f)]
92******************************************************************************)
93val F_U_CLOCK_def =
94 Define
95  `F_U_CLOCK c f = F_UNTIL(F_BOOL(B_NOT c),F_AND(F_BOOL c, f))`;
96
97(******************************************************************************
98* Weakly on first posedge.
99* On first posedge, if there is a posedge: [!c U (c /\ f)]
100******************************************************************************)
101val F_W_CLOCK_def =
102 Define
103  `F_W_CLOCK c f = F_W(F_BOOL(B_NOT c),F_AND(F_BOOL c, f))`;
104
105(******************************************************************************
106* Non-standard rewrite for abort that avoids need for assuming w_0 |= c
107******************************************************************************)
108val F_INIT_CLOCK_COMP_def =
109 Define
110  `(F_INIT_CLOCK_COMP c (F_BOOL b) =
111     F_BOOL b)
112   /\
113   (F_INIT_CLOCK_COMP c (F_NOT f) =
114     F_NOT(F_INIT_CLOCK_COMP c f))
115   /\
116   (F_INIT_CLOCK_COMP c (F_AND(f1,f2)) =
117     F_AND(F_INIT_CLOCK_COMP c f1, F_INIT_CLOCK_COMP c f2))
118   /\
119   (F_INIT_CLOCK_COMP c (F_NEXT f) =
120     F_NEXT(F_U_CLOCK c (F_INIT_CLOCK_COMP c f)))
121   /\
122   (F_INIT_CLOCK_COMP c (F_UNTIL(f1,f2)) =
123     F_UNTIL(F_IMPLIES(F_BOOL c, F_INIT_CLOCK_COMP c f1),
124             F_AND(F_BOOL c, F_INIT_CLOCK_COMP c f2)))
125   /\
126   (F_INIT_CLOCK_COMP c (F_SUFFIX_IMP(r,f)) =
127     F_SUFFIX_IMP(S_CLOCK_COMP c r, F_U_CLOCK c (F_INIT_CLOCK_COMP c f)))
128(*     F_SUFFIX_IMP(S_CLOCK_COMP c r, F_INIT_CLOCK_COMP c f))  *)
129   /\
130   (F_INIT_CLOCK_COMP c (F_STRONG_IMP(r1,r2)) =
131     F_STRONG_IMP (S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
132   /\
133   (F_INIT_CLOCK_COMP c (F_WEAK_IMP(r1,r2)) =
134     F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
135   /\
136   (F_INIT_CLOCK_COMP c (F_ABORT (f,b)) =
137(*     F_ABORT(F_INIT_CLOCK_COMP c f, B_AND(c,b)))                 *)
138     F_OR(F_BOOL b, F_ABORT(F_INIT_CLOCK_COMP c f, B_AND(c,b))))
139   /\
140   (F_INIT_CLOCK_COMP c (F_STRONG_CLOCK(f,c1)) =
141     F_U_CLOCK c1 (F_INIT_CLOCK_COMP c1 f))`;
142
143(******************************************************************************
144* SEM_1 rules for compiling clocked FL formulas to unclocked formulas
145******************************************************************************)
146val F_CLOCK_COMP_def =
147 Define
148  `(F_CLOCK_COMP c (F_BOOL b) =
149     F_BOOL b)
150   /\
151   (F_CLOCK_COMP c (F_NOT f) =
152     F_NOT(F_CLOCK_COMP c f))
153   /\
154   (F_CLOCK_COMP c (F_AND(f1,f2)) =
155     F_AND(F_CLOCK_COMP c f1, F_CLOCK_COMP c f2))
156   /\
157   (F_CLOCK_COMP c (F_NEXT f) =
158     F_NEXT(F_U_CLOCK c (F_CLOCK_COMP c f)))
159   /\
160   (F_CLOCK_COMP c (F_UNTIL(f1,f2)) =
161     F_UNTIL(F_IMPLIES(F_BOOL c, F_CLOCK_COMP c f1),
162             F_AND(F_BOOL c, F_CLOCK_COMP c f2)))
163   /\
164   (F_CLOCK_COMP c (F_SUFFIX_IMP(r,f)) =
165     F_SUFFIX_IMP(S_CLOCK_COMP c r, F_U_CLOCK c (F_CLOCK_COMP c f)))
166(*     F_SUFFIX_IMP(S_CLOCK_COMP c r, F_CLOCK_COMP c f)) *)
167   /\
168   (F_CLOCK_COMP c (F_STRONG_IMP(r1,r2)) =
169     F_STRONG_IMP (S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
170   /\
171   (F_CLOCK_COMP c (F_WEAK_IMP(r1,r2)) =
172     F_WEAK_IMP(S_CLOCK_COMP c r1, S_CLOCK_COMP c r2))
173   /\
174   (F_CLOCK_COMP c (F_ABORT (f,b)) =
175     F_ABORT(F_CLOCK_COMP c f, B_AND(c,b)))
176(*     F_OR(F_BOOL b, F_ABORT(F_CLOCK_COMP c f, B_AND(c,b)))) *)
177   /\
178   (F_CLOCK_COMP c (F_STRONG_CLOCK(f,c1)) =
179     F_U_CLOCK c1 (F_CLOCK_COMP c1 f))`;
180
181val _ = export_theory();
182
183