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