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