Commit b3b0e20d authored by Heiko Becker's avatar Heiko Becker
Browse files

prove totality of exp eval to get idea of HOL Light, add .ocamlinit to gitignore

parent 308ec6d5
......@@ -3,3 +3,4 @@ target/
.DS_Store
src/test/resources/range_regression_today.txt
rawdata/*.txt
hol/.ocamlinit
......@@ -19,15 +19,11 @@ let exp_eval = define
(exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
(exp_eval (Div e1 e2) E = (exp_eval e1) E * (exp_eval e2) E)`;;
let s_env_EQ =
define `s_env:num->real = (\x. 1:real)`;;
let test_EQ =
define `test:num = exp_eval (Var 1) s_env`;;
g `test = 1`;;
e (REWRITE_TAC[test_EQ; s_env_EQ; exp_eval]);;
(* Prove totality of expression evaluation *)
let eval_dev =
prove (`!e s. (!x. ?v. s x = v) ==> ?v. exp_eval e s = v`,
MATCH_MP_TAC exp_INDUCT THEN REPEAT DISCH_TAC THEN REPEAT CONJ_TAC THEN REPEAT GEN_TAC
THEN MESON_TAC[]);;
let bexp_INDUCT, bexp_REC = define_type
"bexp = leq exp exp
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment