Tutorial/Semantics_of_programming_languages_shallow.ml

   1 let assign = new_definition
   2   `Assign (f:S->S) (q:S->bool) = q o f`;;
   3
   4 parse_as_infix(";;",(18,"right"));;
   5
   6 let sequence = new_definition
   7  `(c1:(S->bool)->(S->bool)) ;; (c2:(S->bool)->(S->bool)) = c1 o c2`;;
   8
   9 let if_def = new_definition
  10  `If e (c:(S->bool)->(S->bool)) q = {s | if e s then c q s else q s}`;;
  11
  12 let ite_def = new_definition
  13  `Ite e (c1:(S->bool)->(S->bool)) c2 q =
  14     {s | if e s then c1 q s else c2 q s}`;;
  15
  16 let while_RULES,while_INDUCT,while_CASES = new_inductive_definition
  17          `!q s. If e (c ;; while e c) q s ==> while e c q s`;;
  18
  19 let while_def = new_definition
  20  `While e c q =
  21     {s | !w. (!s:S. (if e(s) then c w s else q s) ==> w s) ==> w s}`;;
  22
  23 let monotonic = new_definition
  24  `monotonic c <=> !q q'. q SUBSET q' ==> (c q) SUBSET (c q')`;;
  25
  26 let MONOTONIC_ASSIGN = prove
  27  (`monotonic (Assign f)`,
  28   SIMP_TAC[monotonic; assign; SUBSET; o_THM; IN]);;
  29
  30 let MONOTONIC_IF = prove
  31  (`monotonic c ==> monotonic (If e c)`,
  32   REWRITE_TAC[monotonic; if_def] THEN SET_TAC[]);;
  33
  34 let MONOTONIC_ITE = prove
  35  (`monotonic c1 /\ monotonic c2 ==> monotonic (Ite e c1 c2)`,
  36   REWRITE_TAC[monotonic; ite_def] THEN SET_TAC[]);;
  37
  38 let MONOTONIC_SEQ = prove
  39  (`monotonic c1 /\ monotonic c2 ==> monotonic (c1 ;; c2)`,
  40   REWRITE_TAC[monotonic; sequence; o_THM] THEN SET_TAC[]);;
  41
  42 let MONOTONIC_WHILE = prove
  43  (`monotonic c ==> monotonic(While e c)`,
  44   REWRITE_TAC[monotonic; while_def] THEN SET_TAC[]);;
  45
  46 let WHILE_THM = prove
  47  (`!e c q:S->bool.
  48     monotonic c
  49     ==> (!s. If e (c ;; While e c) q s ==> While e c q s) /\
  50         (!w'. (!s. If e (c ;; (\q. w')) q s ==> w' s)
  51               ==> (!a. While e c q a ==> w' a)) /\
  52         (!s. While e c q s <=> If e (c ;; While e c) q s)`,
  53   REPEAT GEN_TAC THEN DISCH_TAC THEN
  54   (MP_TAC o GEN_ALL o DISCH_ALL o derive_nonschematic_inductive_relations)
  55    `!s:S. (if e s then c w s else q s) ==> w s` THEN
  56   REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM; IMP_IMP] THEN
  57   DISCH_THEN MATCH_MP_TAC THEN
  58   REWRITE_TAC[FUN_EQ_THM; while_def; IN_ELIM_THM] THEN
  59   POP_ASSUM MP_TAC THEN REWRITE_TAC[monotonic] THEN SET_TAC[]);;
  60
  61 let WHILE_FIX = prove
  62  (`!e c. monotonic c ==> (While e c = If e (c ;; While e c))`,
  63   REWRITE_TAC[FUN_EQ_THM] THEN MESON_TAC[WHILE_THM]);;
  64
  65 let correct = new_definition
  66  `correct p c q <=> p SUBSET (c q)`;;
  67
  68 let CORRECT_PRESTRENGTH = prove
  69  (`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,
  70   REWRITE_TAC[correct; SUBSET_TRANS]);;
  71
  72 let CORRECT_POSTWEAK = prove
  73  (`!p c q q'. monotonic c /\ correct p c q' /\ q' SUBSET q ==> correct p c q`,
  74   REWRITE_TAC[correct; monotonic] THEN SET_TAC[]);;
  75
  76 let CORRECT_ASSIGN = prove
  77  (`!p f q. (p SUBSET (q o f)) ==> correct p (Assign f) q`,
  78   REWRITE_TAC[correct; assign]);;
  79
  80 let CORRECT_SEQ = prove
  81  (`!p q r c1 c2.
  82         monotonic c1 /\ correct p c1 r /\ correct r c2 q
  83         ==> correct p (c1 ;; c2) q`,
  84   REWRITE_TAC[correct; sequence; monotonic; o_THM] THEN SET_TAC[]);;
  85
  86 let CORRECT_ITE = prove
  87  (`!p e c1 c2 q.
  88        correct (p INTER e) c1 q /\ correct (p INTER (UNIV DIFF e)) c2 q
  89        ==> correct p (Ite e c1 c2) q`,
  90   REWRITE_TAC[correct; ite_def] THEN SET_TAC[]);;
  91
  92 let CORRECT_IF = prove
  93  (`!p e c q.
  94        correct (p INTER e) c q /\ p INTER (UNIV DIFF e) SUBSET q
  95        ==> correct p (If e c) q`,
  96   REWRITE_TAC[correct; if_def] THEN SET_TAC[]);;
  97
  98 let CORRECT_WHILE = prove
  99  (`!(<<) p c q e invariant.
 100       monotonic c /\
 101       WF(<<) /\
 102       p SUBSET invariant /\
 103       (UNIV DIFF e) INTER invariant SUBSET q /\
 104       (!X:S. correct (invariant INTER e INTER (\s. X = s)) c
 105                      (invariant INTER (\s. s << X)))
 106       ==> correct p (While e c) q`,
 107   REWRITE_TAC[correct; SUBSET; IN_INTER; IN_UNIV; IN_DIFF; IN] THEN
 108   REPEAT GEN_TAC THEN STRIP_TAC THEN
 109   SUBGOAL_THEN `!s:S. invariant s ==> While e c q s` MP_TAC THENL
 110    [ALL_TAC; ASM_MESON_TAC[]] THEN
 111   FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND]) THEN
 112   X_GEN_TAC `s:S` THEN REPEAT DISCH_TAC THEN
 113   FIRST_ASSUM(fun th -> ONCE_REWRITE_TAC[MATCH_MP WHILE_FIX th]) THEN
 114   REWRITE_TAC[if_def; sequence; o_THM; IN_ELIM_THM] THEN
 115   COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
 116   FIRST_X_ASSUM(MP_TAC o SPECL [`s:S`; `s:S`]) THEN ASM_REWRITE_TAC[] THEN
 117   FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [monotonic]) THEN
 118   REWRITE_TAC[SUBSET; IN; RIGHT_IMP_FORALL_THM] THEN
 119   DISCH_THEN MATCH_MP_TAC THEN ASM_SIMP_TAC[INTER; IN_ELIM_THM; IN]);;
 120
 121 let assert_def = new_definition
 122  `assert (p:S->bool) (q:S->bool) = q`;;
 123
 124 let variant_def = new_definition
 125  `variant ((<<):S->S->bool) (q:S->bool) = q`;;
 126
 127 let CORRECT_SEQ_VC = prove
 128  (`!p q r c1 c2.
 129         monotonic c1 /\ correct p c1 r /\ correct r c2 q
 130         ==> correct p (c1 ;; assert r ;; c2) q`,
 131   REWRITE_TAC[correct; sequence; monotonic; assert_def; o_THM] THEN SET_TAC[]);;
 132
 133 let CORRECT_WHILE_VC = prove
 134  (`!(<<) p c q e invariant.
 135       monotonic c /\
 136       WF(<<) /\
 137       p SUBSET invariant /\
 138       (UNIV DIFF e) INTER invariant SUBSET q /\
 139       (!X:S. correct (invariant INTER e INTER (\s. X = s)) c
 140                      (invariant INTER (\s. s << X)))
 141       ==> correct p (While e (assert invariant ;; variant(<<) ;; c)) q`,
 142   REPEAT STRIP_TAC THEN
 143   REWRITE_TAC[sequence; variant_def; assert_def; o_DEF; ETA_AX] THEN
 144   ASM_MESON_TAC[CORRECT_WHILE]);;
 145
 146 let MONOTONIC_ASSERT = prove
 147  (`monotonic (assert p)`,
 148   REWRITE_TAC[assert_def; monotonic]);;
 149
 150 let MONOTONIC_VARIANT = prove
 151  (`monotonic (variant p)`,
 152   REWRITE_TAC[variant_def; monotonic]);;
 153
 154 let MONO_TAC =
 155   REPEAT(MATCH_MP_TAC MONOTONIC_WHILE ORELSE
 156          (MAP_FIRST MATCH_MP_TAC
 157            [MONOTONIC_SEQ; MONOTONIC_IF; MONOTONIC_ITE] THEN CONJ_TAC)) THEN
 158   MAP_FIRST MATCH_ACCEPT_TAC
 159    [MONOTONIC_ASSIGN; MONOTONIC_ASSERT; MONOTONIC_VARIANT];;
 160
 161 let VC_TAC =
 162   FIRST
 163    [MATCH_MP_TAC CORRECT_SEQ_VC THEN CONJ_TAC THENL [MONO_TAC; CONJ_TAC];
 164     MATCH_MP_TAC CORRECT_ITE THEN CONJ_TAC;
 165     MATCH_MP_TAC CORRECT_IF THEN CONJ_TAC;
 166     MATCH_MP_TAC CORRECT_WHILE_VC THEN REPEAT CONJ_TAC THENL
 167      [MONO_TAC; TRY(MATCH_ACCEPT_TAC WF_MEASURE); ALL_TAC; ALL_TAC;
 168       REWRITE_TAC[FORALL_PAIR_THM; MEASURE] THEN REPEAT GEN_TAC];
 169     MATCH_MP_TAC CORRECT_ASSIGN];;
 170
 171 needs "Library/prime.ml";;
 172
 173 (* ------------------------------------------------------------------------- *)
 174 (* x = m, y = n;                                                             *)
 175 (* while (!(x == 0 || y == 0))                                               *)
 176 (*  { if (x < y) y = y - x;                                                  *)
 177 (*    else x = x - y;                                                        *)
 178 (*  }                                                                        *)
 179 (* if (x == 0) x = y;                                                        *)
 180 (* ------------------------------------------------------------------------- *)
 181
 182 g `correct
 183     (\(m,n,x,y). T)
 184     (Assign (\(m,n,x,y). m,n,m,n) ;;         // x,y := m,n
 185      assert (\(m,n,x,y). x = m /\ y = n) ;;
 186      While (\(m,n,x,y). ~(x = 0 \/ y = 0))
 187       (assert (\(m,n,x,y). gcd(x,y) = gcd(m,n)) ;;
 188        variant(MEASURE(\(m,n,x,y). x + y)) ;;
 189        Ite (\(m,n,x,y). x < y)
 190            (Assign (\(m,n,x,y). m,n,x,y - x))
 191            (Assign (\(m,n,x,y). m,n,x - y,y))) ;;
 192      assert (\(m,n,x,y). (x = 0 \/ y = 0) /\ gcd(x,y) = gcd(m,n)) ;;
 193      If (\(m,n,x,y). x = 0) (Assign (\(m,n,x,y). (m,n,y,y))))
 194   (\(m,n,x,y). gcd(m,n) = x)`;;
 195
 196 e(REPEAT VC_TAC);;
 197
 198 b();;
 199 e(REPEAT VC_TAC THEN REWRITE_TAC[SUBSET; FORALL_PAIR_THM] THEN
 200   MAP_EVERY X_GEN_TAC [`m:num`; `n:num`; `x:num`; `y:num`] THEN
 201   REWRITE_TAC[IN; INTER; UNIV; DIFF; o_DEF; IN_ELIM_THM; PAIR_EQ] THEN
 202   CONV_TAC(TOP_DEPTH_CONV GEN_BETA_CONV) THEN SIMP_TAC[]);;
 203
 204 e(SIMP_TAC[GCD_SUB; LT_IMP_LE]);;
 205 e ARITH_TAC;;
 206
 207 e(SIMP_TAC[GCD_SUB; NOT_LT] THEN ARITH_TAC);;
 208
 209 e(MESON_TAC[GCD_0]);;
 210
 211 e(MESON_TAC[GCD_0; GCD_SYM]);;
 212
 213 parse_as_infix("refines",(12,"right"));;
 214
 215 let refines = new_definition
 216  `c2 refines c1 <=> !q. c1(q) SUBSET c2(q)`;;
 217
 218 let REFINES_REFL = prove
 219  (`!c. c refines c`,
 220   REWRITE_TAC[refines; SUBSET_REFL]);;
 221
 222 let REFINES_TRANS = prove
 223  (`!c1 c2 c3. c3 refines c2 /\ c2 refines c1 ==> c3 refines c1`,
 224   REWRITE_TAC[refines] THEN MESON_TAC[SUBSET_TRANS]);;
 225
 226 let REFINES_CORRECT = prove
 227  (`correct p c1 q /\ c2 refines c1 ==> correct p c2 q`,
 228   REWRITE_TAC[correct; refines] THEN MESON_TAC[SUBSET_TRANS]);;
 229
 230 let REFINES_WHILE = prove
 231  (`c' refines c ==> While e c' refines While e c`,
 232   REWRITE_TAC[refines; while_def; SUBSET; IN_ELIM_THM; IN] THEN MESON_TAC[]);;
 233
 234 let specification = new_definition
 235  `specification(p,q) r = if q SUBSET r then p else {}`;;
 236
 237 let REFINES_SPECIFICATION = prove
 238  (`c refines specification(p,q) ==> correct p c q`,
 239   REWRITE_TAC[specification; correct; refines] THEN
 240   MESON_TAC[SUBSET_REFL; SUBSET_EMPTY]);;