Tutorial/Semantics_of_programming_languages_deep.ml

   1 let string_INDUCT,string_RECURSION =
   2   define_type "string = String (int list)";;
   3
   4 let expression_INDUCT,expression_RECURSION = define_type
   5 "expression = Literal num
   6             | Variable string
   7             | Plus expression expression
   8             | Times expression expression";;
   9
  10 let command_INDUCT,command_RECURSION = define_type
  11   "command = Assign string expression
  12            | Sequence command command
  13            | If expression command command
  14            | While expression command";;
  15
  16 parse_as_infix(";;",(18,"right"));;
  17 parse_as_infix(":=",(20,"right"));;
  18 override_interface(";;",`Sequence`);;
  19 override_interface(":=",`Assign`);;
  20 overload_interface("+",`Plus`);;
  21 overload_interface("*",`Times`);;
  22
  23 let value = define
  24  `(value (Literal n) s = n) /\
  25   (value (Variable x) s = s(x)) /\
  26   (value (e1 + e2) s = value e1 s + value e2 s) /\
  27   (value (e1 * e2) s = value e1 s * value e2 s)`;;
  28
  29 let sem_RULES,sem_INDUCT,sem_CASES = new_inductive_definition
  30   `(!x e s s'. s'(x) = value e s /\ (!y. ~(y = x) ==> s'(y) = s(y))
  31                ==> sem (x := e) s s') /\
  32    (!c1 c2 s s' s''. sem(c1) s s' /\ sem(c2) s' s'' ==> sem(c1 ;; c2) s s'') /\
  33    (!e c1 c2 s s'. ~(value e s = 0) /\ sem(c1) s s' ==> sem(If e c1 c2) s s') /\
  34    (!e c1 c2 s s'. value e s = 0 /\ sem(c2) s s' ==> sem(If e c1 c2) s s') /\
  35    (!e c s. value e s = 0 ==> sem(While e c) s s) /\
  36    (!e c s s' s''. ~(value e s = 0) /\ sem(c) s s' /\ sem(While e c) s' s''
  37                    ==> sem(While e c) s s'')`;;
  38
  39 (**** Fails
  40   define
  41    `sem(While e c) s s' <=> if value e s = 0 then (s' = s)
  42                             else ?s''. sem c s s'' /\ sem(While e c) s'' s'`;;
  43 ****)
  44
  45 let DETERMINISM = prove
  46  (`!c s s' s''. sem c s s' /\ sem c s s'' ==> (s' = s'')`,
  47   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  48   MATCH_MP_TAC sem_INDUCT THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
  49   DISCH_TAC THEN ONCE_REWRITE_TAC[sem_CASES] THEN
  50   REWRITE_TAC[distinctness "command"; injectivity "command"] THEN
  51   REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);;
  52
  53 let wlp = new_definition
  54  `wlp c q s <=> !s'. sem c s s' ==> q s'`;;
  55
  56 let terminates = new_definition
  57  `terminates c s <=> ?s'. sem c s s'`;;
  58
  59 let wp = new_definition
  60  `wp c q s <=> terminates c s /\ wlp c q s`;;
  61
  62 let WP_TOTAL = prove
  63  (`!c. (wp c EMPTY = EMPTY)`,
  64   REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; EMPTY] THEN MESON_TAC[]);;
  65
  66 let WP_MONOTONIC = prove
  67  (`q SUBSET r ==> wp c q SUBSET wp c r`,
  68   REWRITE_TAC[SUBSET; IN; wp; wlp; terminates] THEN MESON_TAC[]);;
  69
  70 let WP_DISJUNCTIVE = prove
  71  (`(wp c p) UNION (wp c q) = wp c (p UNION q)`,
  72   REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN
  73   MESON_TAC[DETERMINISM]);;
  74
  75 let WP_SEQ = prove
  76  (`!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2`,
  77   REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN
  78   GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN
  79   REWRITE_TAC[injectivity "command"; distinctness "command"] THEN
  80   MESON_TAC[DETERMINISM]);;
  81
  82 let correct = new_definition
  83  `correct p c q <=> p SUBSET (wp c q)`;;
  84
  85 let CORRECT_PRESTRENGTH = prove
  86  (`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,
  87   REWRITE_TAC[correct; SUBSET_TRANS]);;
  88
  89 let CORRECT_POSTWEAK = prove
  90  (`!p c q q'. correct p c q' /\ q' SUBSET q ==> correct p c q`,
  91   REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;
  92
  93 let CORRECT_SEQ = prove
  94  (`!p q r c1 c2.
  95         correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q`,
  96   REWRITE_TAC[correct; WP_SEQ; o_THM] THEN
  97   MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;