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

Make all evaluation parametric over value type of expressions

parent 4b3f7f61
......@@ -3,36 +3,61 @@
*)
needs "Infra/tactics.ml";;
(*
Define expressions parametric over some value type V.
Will ease reasoning about different instantiations later.
*)
let exp_INDUCT, exp_REC= define_type
"exp = Var num
| Const real
| Const V
| Plus exp exp
| Sub exp exp
| Mult exp exp
| Div exp exp";;
(*
Since we want to stay with real values for the moment,
show that real valued expressions can be evaluated
by constructing the corresponding function
*)
let exp_eval_EXISTS = prove_general_recursive_function_exists
`?exp_eval.
(!x E. exp_eval (Var x) E = E x) /\
(!r E. exp_eval (Const r) E = r) /\
(!x (E:num->real). exp_eval (Var x) E = E x) /\
(!(v:real) E. exp_eval (Const v) E = v) /\
(!e1 e2 E. exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Mult e1 e2) E = (exp_eval e1) E * (exp_eval e2) E) /\
(!e1 e2 E. exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
(*
Since HOL Light could prove the existence of the evaluation function,
we can define it using the defining equations from the theorem.
*)
let exp_eval_DEF = new_specification ["exp_eval"] exp_eval_EXISTS;;
(*
Toy examples showing how to evaluate terms and functions in HOL Light
*)
`exp_eval (Const (&1)) (\x. &1)`;;
REWRITE_CONV[exp_eval_DEF] it;;
rhs (concl it);;
(* Prove totality of expression evaluation *)
(*
Prove totality of expression evaluation for reals assuming totality of the environment
TODO: Make totality totality on occuring variables
*)
let exp_eval_total =
prove (
`!e (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`,
`!(e:(real)exp) (s:num->real).
(!x:num. ?v:real. s x = v) ==>
?v. exp_eval e s = v`,
MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC THEN MESON_TAC[]);;
(*
More formal proof, to get feeling about tactics.
TODO: Time consumption compared?
g `!e (s:num->real). (!x:num. ?v:real. s x = v) ==> ?v. exp_eval e s = v`;;
e (MATCH_MP_TAC exp_INDUCT THEN REPEAT STRIP_TAC);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
......@@ -56,38 +81,84 @@ e (MESON_TAC[]);;
e (MESON_TAC[]);;
let exp_eval_total = top_thm();; *)
(*
Using the parametric expressions, define boolean expressions for conditionals
*)
let bexp_INDUCT, bexp_REC = define_type
"bexp = leq exp exp
| less exp exp";;
"bexp = leq (V)exp (V)exp
| less (V)exp (V)exp";;
(*
Define evaluation of booleans for reals
*)
let bval_SIMPS = define
`(bval (leq e1 e2) (E:num->real) = (exp_eval e1 E) <= (exp_eval e2 E)) /\
(bval (less e1 e2) E = (exp_eval e1 E) < (exp_eval e2 E))`;;
(* Simplify arithmetic later by making > >= only abbreviations *)
let gr_simps = define
`gr = \e1. \e2. less e2 e1`;;
`gr = \(e1:(V)exp). \(e2:(V)exp). less e2 e1`;;
let greq_simps = define
`greq = \e1. \e2. leq e2 e1`;;
`greq = \(e1:(V)exp). \(e2:(V)exp). leq e2 e1`;;
(*
Next define what a program is.
Currently no loops, only conditionals and assignments
Final return statement
*)
let cmd_INDUCT, cmd_REC = define_type
"cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;
"cmd = Ass num (V)exp cmd
| Ite (V)bexp cmd cmd
| Ret (V)exp";;
(*
Define environment update function for arbitrary type as abbreviation
*)
let upd_env_simps = define
`upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E y)`;;
`upd_env (x:num) (v:V) (E:num->V) =(\y. if y = x then v else E y)`;;
(* Small Step semantics for Daisy Language *)
(*
Small Step semantics for Daisy language, parametric by evaluation function.
*)
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s (upd_env x v env)) /\
(!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
(!c s t env. bval c env = F ==> sstep (Ite c s t) env t env)`;;
`(!x (e:(V)exp) s (env:num->V) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v ==>
sstep (Ass x e s) env eval beval s (upd_env x v env)) /\
(!(c:(V)bexp) s t
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = T ==>
sstep (Ite c s t) env eval beval s env) /\
(!(c:(V)bexp) s t
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = F ==>
sstep (Ite c s t) env eval beval t env)`;;
(*
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function*)
let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
`(!x e s env v. exp_eval e env = v /\ bstep s (upd_env x v env) s ==>
bstep (Ass x e s) env s ) /\
(!c s t env. bval c env = T /\ bstep s env s ==>
bstep (Ite c s t) env s) /\
(!c s t env. bval c env = F /\ bstep s env s
==> bstep (Ite c s t) env t)`;;
`(!x (e:(V)exp) s (env:num->V) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
eval e env = v /\ bstep s (upd_env x v env) eval beval s ==>
bstep (Ass x e s) env eval beval s ) /\
(!(c:(V)bexp) s1 s2 t
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = T /\ bstep s1 env eval beval s2 ==>
bstep (Ite c s1 t) env eval beval s2) /\
(!(c:(V)bexp) s t1 t2
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
beval c env = F /\ bstep t1 env eval beval t2
==> bstep (Ite c s t1) env eval beval t2 )`;;
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