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