Examples/ste.ml

   1 (* ========================================================================= *)
   2 (* Abstract version of symbolic trajectory evaluation.                       *)
   3 (*                                                                           *)
   4 (* Based on the paper "Symbolic Trajectory Evaluation in a Nutshell"         *)
   5 (* by Tom Melham & Ashish Darbari, 2002 (still unpublished?)                 *)
   6 (* ========================================================================= *)
   7
   8 parse_as_infix("&&",(16,"right"));;
   9 parse_as_infix("<<=",(14,"right"));;
  10 parse_as_infix(">->",(13,"right"));;
  11 parse_as_infix(">~~>",(6,"right"));;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (* Some type of nodes that we don't really care much about.                  *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let node_INDUCT,node_RECURSION = define_type
  18   "node = Node num";;
  19
  20 (* ------------------------------------------------------------------------- *)
  21 (* Also "abstract" propositional formulas (i.e. we never unfold "eval").     *)
  22 (* ------------------------------------------------------------------------- *)
  23
  24 let propform_INDUCT,propform_RECURSION = define_type
  25   "propform = Propform (num->bool)->bool";;
  26
  27 let eval = new_recursive_definition propform_RECURSION
  28   `eval (Propform p) v = p v`;;
  29
  30 (* ------------------------------------------------------------------------- *)
  31 (* Quaternary lattice.                                                       *)
  32 (* ------------------------------------------------------------------------- *)
  33
  34 let quat_INDUCT,quat_RECURSION = define_type
  35  "quat = X | ZERO | ONE | TOP";;
  36
  37 let quat_DISTINCT = prove_constructors_distinct quat_RECURSION;;
  38
  39 (* ------------------------------------------------------------------------- *)
  40 (* Basic lattice operations.                                                 *)
  41 (* ------------------------------------------------------------------------- *)
  42
  43 let qle = new_definition
  44   `x <<= y <=> x = X \/ y = TOP \/ x = y`;;
  45
  46 let qjoin = new_definition
  47   `x && y = if x <<= y then y else if y <<= x then x else TOP`;;
  48
  49 (* ------------------------------------------------------------------------- *)
  50 (* Trivial lemmas about the quaternary lattice.                              *)
  51 (* ------------------------------------------------------------------------- *)
  52
  53 let QLE_REFL = prove
  54  (`!x. x <<= x`,
  55   REWRITE_TAC[qle]);;
  56
  57 let QLE_TRANS = prove
  58  (`!x y z. x <<= y /\ y <<= z ==> x <<= z`,
  59   REPEAT(MATCH_MP_TAC quat_INDUCT THEN REPEAT CONJ_TAC) THEN
  60   REWRITE_TAC[qle; quat_DISTINCT]);;
  61
  62 let QLE_LJOIN = prove
  63  (`!x y z. x && y <<= z <=> x <<= z /\ y <<= z`,
  64   REPEAT(MATCH_MP_TAC quat_INDUCT THEN REPEAT CONJ_TAC) THEN
  65   REWRITE_TAC[qjoin; qle; quat_DISTINCT]);;
  66
  67 let QLE_RJOIN = prove
  68  (`!x y. x <<= x && y /\ y <<= x && y`,
  69   REPEAT(MATCH_MP_TAC quat_INDUCT THEN REPEAT CONJ_TAC) THEN
  70   REWRITE_TAC[qjoin; qle; quat_DISTINCT]);;
  71
  72 (* ------------------------------------------------------------------------- *)
  73 (* Choice expressions.                                                       *)
  74 (* ------------------------------------------------------------------------- *)
  75
  76 let choice = new_definition
  77   `b >-> x = if b then x else X`;;
  78
  79 let QLE_CHOICE = prove
  80  (`(b >-> x) <<= y <=> b ==> x <<= y`,
  81   REPEAT GEN_TAC THEN REWRITE_TAC[choice] THEN
  82   COND_CASES_TAC THEN REWRITE_TAC[] THEN REWRITE_TAC[qle]);;
  83
  84 (* ------------------------------------------------------------------------- *)
  85 (* Basic type of trajectory formulas.                                        *)
  86 (* ------------------------------------------------------------------------- *)
  87
  88 let trajform_INDUCT,trajform_RECURSION = define_type
  89  "trajform = Is_0 node
  90            | Is_1 node
  91            | Andj trajform trajform
  92            | When trajform propform
  93            | Next trajform";;
  94
  95 (* ------------------------------------------------------------------------- *)
  96 (* Semantics.                                                                *)
  97 (* ------------------------------------------------------------------------- *)
  98
  99 let tholds = new_recursive_definition trajform_RECURSION
 100   `(tholds (Is_0 nd) seq v <=> ZERO <<= seq 0 nd v) /\
 101    (tholds (Is_1 nd) seq v <=> ONE <<= seq 0 nd v) /\
 102    (tholds (Andj tf1 tf2) seq v <=> tholds tf1 seq v /\ tholds tf2 seq v) /\
 103    (tholds (When tf1 p) seq v <=> eval p v ==> tholds tf1 seq v) /\
 104    (tholds (Next(tf1)) seq v <=> tholds tf1 (\t. seq(t + 1)) v)`;;
 105
 106 (* ------------------------------------------------------------------------- *)
 107 (* Defining sequence.                                                        *)
 108 (* ------------------------------------------------------------------------- *)
 109
 110 let defseq = new_recursive_definition trajform_RECURSION
 111   `(defseq (Is_0 n) t nd v = ((n = nd) /\ (t = 0)) >-> ZERO) /\
 112    (defseq (Is_1 n) t nd v = ((n = nd) /\ (t = 0)) >-> ONE) /\
 113    (defseq (Andj tf1 tf2) t nd v = defseq tf1 t nd v && defseq tf2 t nd v) /\
 114    (defseq (When tf1 p) t nd v =  eval p v >-> defseq tf1 t nd v) /\
 115    (defseq (Next(tf1)) t nd v = ~(t = 0) >-> defseq tf1 (t - 1) nd v)`;;
 116
 117 (* ------------------------------------------------------------------------- *)
 118 (* Proof of the key property.                                                *)
 119 (* ------------------------------------------------------------------------- *)
 120
 121 let DEFSEQ_MINIMAL = prove
 122  (`!tf seq v. tholds tf seq v <=> !t nd. defseq tf t nd v <<= seq t nd v`,
 123   let cases_lemma = prove
 124    (`(!t. P t) <=> P 0 /\ !t. P(SUC t)`,MESON_TAC[num_CASES]) in
 125   MATCH_MP_TAC trajform_INDUCT THEN REWRITE_TAC[defseq; tholds] THEN
 126   REPEAT CONJ_TAC THENL
 127    [REPEAT GEN_TAC THEN REWRITE_TAC[QLE_CHOICE] THEN MESON_TAC[];
 128     REPEAT GEN_TAC THEN REWRITE_TAC[QLE_CHOICE] THEN MESON_TAC[];
 129     SIMP_TAC[QLE_LJOIN; FORALL_AND_THM];
 130     REWRITE_TAC[QLE_CHOICE] THEN MESON_TAC[];
 131     REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[cases_lemma] THEN
 132     ASM_REWRITE_TAC[QLE_CHOICE; NOT_SUC; ADD1; ADD_SUB]]);;
 133
 134 (* ------------------------------------------------------------------------- *)
 135 (* Notion of a trajectory w.r.t. a next-state function.                      *)
 136 (* ------------------------------------------------------------------------- *)
 137
 138 let trajectory = new_definition
 139   `trajectory next seq v <=> !t nd. next(seq t) nd v <<= seq (t + 1) nd v`;;
 140
 141 (* ------------------------------------------------------------------------- *)
 142 (* Defining trajectory of a formula.                                         *)
 143 (* ------------------------------------------------------------------------- *)
 144
 145 let deftraj = new_recursive_definition num_RECURSION
 146   `(deftraj step tf 0 nd v = defseq tf 0 nd v) /\
 147    (deftraj step tf (SUC t) nd v =
 148         defseq tf (SUC t) nd v && step(deftraj step tf t) nd v)`;;
 149
 150 (* ------------------------------------------------------------------------- *)
 151 (* Obviously this is at least as strong as the defining sequence.            *)
 152 (* ------------------------------------------------------------------------- *)
 153
 154 let DEFTRAJ_DEFSEQ = prove
 155  (`!tf t nd v. defseq tf t nd v <<= deftraj step tf t nd v`,
 156   GEN_TAC THEN INDUCT_TAC THEN
 157   REWRITE_TAC[deftraj; QLE_REFL; QLE_RJOIN]);;
 158
 159 (* ------------------------------------------------------------------------- *)
 160 (* ...and it is indeed a trajectory.                                         *)
 161 (* ------------------------------------------------------------------------- *)
 162
 163 let TRAJECTORY_DEFTRAJ = prove
 164  (`!step tf v. trajectory step (deftraj step tf) v`,
 165   REPEAT GEN_TAC THEN REWRITE_TAC[trajectory] THEN
 166   REWRITE_TAC[GSYM ADD1; deftraj; QLE_RJOIN]);;
 167
 168 (* ------------------------------------------------------------------------- *)
 169 (* Monotonicity of next-state function.                                      *)
 170 (* ------------------------------------------------------------------------- *)
 171
 172 let monotonic = new_definition
 173  `monotonic next v <=>
 174    !s1 s2. (!nd. s1 nd v <<= s2 nd v) ==> !nd. next s1 nd v <<= next s2 nd v`;;
 175
 176 (* ------------------------------------------------------------------------- *)
 177 (* Minimality property of defining trajectory (needs monotonicity).          *)
 178 (* ------------------------------------------------------------------------- *)
 179
 180 let DEFTRAJ_MINIMAL = prove
 181  (`!step v.
 182       monotonic step v
 183       ==> !tf seq. trajectory step seq v
 184                    ==> (tholds tf seq v <=>
 185                         !t nd. deftraj step tf t nd v <<= seq t nd v)`,
 186   REWRITE_TAC[monotonic; trajectory; RIGHT_IMP_FORALL_THM] THEN
 187   REPEAT STRIP_TAC THEN EQ_TAC THENL
 188    [ALL_TAC; MESON_TAC[DEFSEQ_MINIMAL; DEFTRAJ_DEFSEQ; QLE_TRANS]] THEN
 189   DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[deftraj; QLE_LJOIN] THEN
 190   ASM_MESON_TAC[DEFSEQ_MINIMAL; QLE_TRANS; ADD1]);;
 191
 192 (* ------------------------------------------------------------------------- *)
 193 (* Basic semantic notion in STE.                                             *)
 194 (* ------------------------------------------------------------------------- *)
 195
 196 let ste = new_definition
 197   `(A >~~> C) ckt v <=>
 198       !seq. trajectory ckt seq v /\ tholds A seq v ==> tholds C seq v`;;
 199
 200 (* ------------------------------------------------------------------------- *)
 201 (* The "fundamental theorem of STE".                                         *)
 202 (* ------------------------------------------------------------------------- *)
 203
 204 let STE_THM = prove
 205  (`monotonic ckt v
 206    ==> ((A >~~> C) ckt v <=> !t nd. defseq C t nd v <<= deftraj ckt A t nd v)`,
 207   MESON_TAC[ste; DEFTRAJ_MINIMAL; DEFSEQ_MINIMAL; DEFTRAJ_DEFSEQ;
 208             TRAJECTORY_DEFTRAJ; QLE_TRANS]);;