let string_INDUCT,string_RECURSION =
  define_type "string = String (int list)";
;


let expression_INDUCT,expression_RECURSION = define_type
"expression = Literal num
            | Variable string
            | Plus expression expression
            | Times expression expression";
;


let command_INDUCT,command_RECURSION = define_type
  "command = Assign string expression
           | Sequence command command
           | If expression command command
           | While expression command";
;

parse_as_infix(";;",(18,"right"));;
parse_as_infix(":=",(20,"right"));;
override_interface(";;",`Sequence`);;
override_interface(":=",`Assign`);;
overload_interface("+",`Plus`);;
overload_interface("*",`Times`);;


let value = define
 `(value (Literal n) s = n) /\
  (value (Variable x) s = s(x)) /\
  (value (e1 + e2) s = value e1 s + value e2 s) /\
  (value (e1 * e2) s = value e1 s * value e2 s)`;;

let sem_RULES,sem_INDUCT,sem_CASES = new_inductive_definition
  `(!x e s s'. s'(x) = value e s /\ (!y. ~(y = x) ==> s'(y) = s(y))
               ==> sem (x := e) s s') /\
   (!c1 c2 s s' s''. sem(c1) s s' /\ sem(c2) s' s'' ==> sem(c1 ;; c2) s s'') /\
   (!e c1 c2 s s'. ~(value e s = 0) /\ sem(c1) s s' ==> sem(If e c1 c2) s s') /\
   (!e c1 c2 s s'. value e s = 0 /\ sem(c2) s s' ==> sem(If e c1 c2) s s') /\
   (!e c s. value e s = 0 ==> sem(While e c) s s) /\
   (!e c s s' s''. ~(value e s = 0) /\ sem(c) s s' /\ sem(While e c) s' s''
                   ==> sem(While e c) s s'')`;;

(**** Fails
  define
   `sem(While e c) s s' <=> if value e s = 0 then (s' = s)
                            else ?s''. sem c s s'' /\ sem(While e c) s'' s'`;;
****)


let DETERMINISM = 
prove
 (`!c s s' s''. sem c s s' /\ sem c s s'' ==> (s' = s'')`,

  REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
  MATCH_MP_TAC sem_INDUCT THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
  DISCH_TAC THEN ONCE_REWRITE_TAC[sem_CASES] THEN
  REWRITE_TAC[distinctness "command";
 injectivity "command"] THEN
  REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]);;


let wlp = new_definition
 `wlp c q s <=> !s'. sem c s s' ==> q s'`;;


let terminates = new_definition
 `terminates c s <=> ?s'. sem c s s'`;;


let wp = new_definition
 `wp c q s <=> terminates c s /\ wlp c q s`;;


let WP_TOTAL = 
prove
 (`!c. (wp c EMPTY = EMPTY)`,

  REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; EMPTY] THEN MESON_TAC[]);;


let WP_MONOTONIC = 
prove
 (`q SUBSET r ==> wp c q SUBSET wp c r`,

  REWRITE_TAC[SUBSET; IN; wp; wlp; terminates] THEN MESON_TAC[]);;


let WP_DISJUNCTIVE = 
prove
 (`(wp c p) UNION (wp c q) = wp c (p UNION q)`,

  REWRITE_TAC[FUN_EQ_THM; IN; wp; wlp; IN_ELIM_THM; UNION; terminates] THEN
  MESON_TAC[DETERMINISM]);;


let WP_SEQ = 
prove
 (`!c1 c2 q. wp (c1 ;; c2) = wp c1 o wp c2`,

  REWRITE_TAC[wp; wlp; terminates; FUN_EQ_THM; o_THM] THEN REPEAT GEN_TAC THEN
  GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [sem_CASES] THEN
  REWRITE_TAC[injectivity "command";
 distinctness "command"] THEN
  MESON_TAC[DETERMINISM]);;


let correct = new_definition
 `correct p c q <=> p SUBSET (wp c q)`;;


let CORRECT_PRESTRENGTH = 
prove
 (`!p p' c q. p SUBSET p' /\ correct p' c q ==> correct p c q`,

  REWRITE_TAC[correct; SUBSET_TRANS]);;


let CORRECT_POSTWEAK = 
prove
 (`!p c q q'. correct p c q' /\ q' SUBSET q ==> correct p c q`,

  REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;


let CORRECT_SEQ = 
prove
 (`!p q r c1 c2.
        correct p c1 r /\ correct r c2 q ==> correct p (c1 ;; c2) q`,

  REWRITE_TAC[correct; WP_SEQ; o_THM] THEN
  MESON_TAC[WP_MONOTONIC; SUBSET_TRANS]);;