1 2 3(*****************************************************************************) 4(* Create "ModelTheory" containing definition of models for OBE semantics. *) 5(* PSL version 1.1 *) 6(*****************************************************************************) 7 8(*****************************************************************************) 9(* A model is a quintuple (S,S0,R,P,L), represented as a record, where *) 10(* *) 11(* - S : 'state -> bool is a set of states *) 12(* - S0 : 'state -> bool is a subset of S, the initial states *) 13(* - R : 'state # 'state -> bool is a transition relation *) 14(* - P : 'prop -> bool is a set of atomic proposition *) 15(* - L : 'state -> ('prop -> bool) maps each state to the *) 16(* set of propositions true in that state *) 17(* *) 18(* The type parameters are: ``: ('state,'prop)model`` *) 19(* N.B. terms that follow are not contrained to use type variables 'state *) 20(* and 'prop, but may use 'a, 'b etc or whatever typechecking assigns. *) 21(*****************************************************************************) 22 23(*****************************************************************************) 24(* Load theory of syntax, paths and models *) 25(* (commented out for compilation) *) 26(*****************************************************************************) 27 28(* 29quietdec := true; (* Switch off output *) 30loadPath (* Add path to loadPath *) 31 := 32 "../../path" :: !loadPath; 33map load ["pred_setLib","PSLPathTheory"]; 34open ped_setTheory PSLPathTheory; 35quietdec := false; (* Restore output *) 36*) 37 38(*****************************************************************************) 39(* Boilerplate needed for compilation *) 40(*****************************************************************************) 41 42open HolKernel Parse boolLib bossLib pred_setTheory PSLPathTheory; 43 44(*****************************************************************************) 45(* END BOILERPLATE *) 46(*****************************************************************************) 47 48(*****************************************************************************) 49(* Start a new theory called ModelTheory *) 50(*****************************************************************************) 51 52val _ = new_theory "Model"; 53 54(*****************************************************************************) 55(* Stop ``S`` parsing to the S-combinator *) 56(*****************************************************************************) 57val _ = hide "S"; 58 59(*****************************************************************************) 60(* ``: ('prop,'state)model`` *) 61(*****************************************************************************) 62val model_def = 63 Hol_datatype 64 `model = 65 <| S: 'state -> bool; 66 S0:'state -> bool; 67 R: 'state # 'state -> bool; 68 P: 'prop -> bool; 69 L: 'state -> ('prop -> bool) |>`; 70 71val MODEL_def = 72 Define 73 `MODEL M = 74 M.S0 SUBSET M.S /\ 75 (!s s'. (s,s') IN M.R ==> s IN M.S /\ s' IN M.S) /\ 76 (!s. s IN M.S ==> M.L s SUBSET M.P)`; 77 78(*****************************************************************************) 79(* A letter is either TOP, or BOTTOM *) 80(* or a set of atomic propositions repersenting a state *) 81(*****************************************************************************) 82val letter_def = 83 Hol_datatype 84 `letter = TOP | BOTTOM | STATE of ('prop -> bool)`; 85 86(*****************************************************************************) 87(* PATH M s is true of path p iff p is a computation path of model M *) 88(*****************************************************************************) 89val PATH_def = 90 Define 91 `PATH M s w = 92 (LENGTH w > 0) /\ (s = ELEM w 0) /\ s IN M.S /\ 93 (!n :: (LESS(LENGTH w - 1)). 94 ELEM w n IN M.S /\ ELEM w (SUC n) IN M.S /\ 95 (ELEM w n, ELEM w (SUC n)) IN M.R) /\ 96 (!l. (w = FINITE l) 97 ==> !s. s IN M.S ==> ~((ELEM w (LENGTH l - 1), s) IN M.R))`; 98 99 100(*****************************************************************************) 101(* A computation of M is a path of M starting from an initial state *) 102(*****************************************************************************) 103val COMPUTATION_def = 104 Define 105 `COMPUTATION M w = ?s. s IN M.S0 /\ PATH M s w`; 106 107val _ = export_theory(); 108 109 110