Commit 92b1984f authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix some flaws, simplify big- and small-step relations

parent 81dc70ea
......@@ -23,56 +23,51 @@ let upd_env_simps = define
Small Step semantics for Daisy language, parametric by evaluation function.
*)
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!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).
`(!x (e:(real)exp) s (env:num->real) (v:real)
(eval:(real)exp->(num->real)->real)
(env:num->real).
eval e env = v ==>
sstep (Let 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) /\
(!(e:(V)exp) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
sstep (Let x e s) env eval s (upd_env x v env)) /\
(!(c:(real)bexp) s t
(eval:(real)exp->(num->real)->real)
(env:num->real).
bval c env eval = T ==>
sstep (Ite c s t) env eval s env) /\
(!(c:(real)bexp) s t
(eval:(real)exp->(num->real)->real)
(env:num->real).
bval c env eval = F ==>
sstep (Ite c s t) env eval t env) /\
(!(e:(real)exp) (v:real)
(eval:(real)exp->(num->real)->real)
(env:num->real).
eval e env = v ==>
sstep (Ret e) env eval beval Nop (upd_env (0) v env))`;;
sstep (Ret e) env eval Nop (upd_env (0) v 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:(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 (Let 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 ) /\
(!(e:(V)exp) (v:V)
(eval:(V)exp->(num->V)->V)
(beval:(V)bexp->(num->V)->bool)
(env:num->V).
`(!x (e:(real)exp) s (env:num->real) (v:real)
(eval:(real)exp->(num->real)->real)
(env:num->real)
(env2:num->real).
eval e env = v /\ bstep s (upd_env x v env) eval s env2 ==>
bstep (Let x e s) env eval s env2) /\
(!(c:(real)bexp) s1 s2 t
(eval:(real)exp->(num->real)->real)
(env:num->real)
(env2:num->real).
bval c env eval = T /\ bstep s1 env eval s2 env2 ==>
bstep (Ite c s1 t) env eval s2 env2) /\
(!(c:(real)bexp) s t1 t2
(eval:(real)exp->(num->real)->real)
(env:num->real)
(env2:num->real).
bval c env eval = F /\ bstep t1 env eval t2 env2 ==>
bstep (Ite c s t1) env eval t2 env2) /\
(!(e:(real)exp) (v:real)
(eval:(real)exp->(num->real)->real)
(env:num->real).
eval e env = v ==>
bstep (Ret e) env eval beval Nop)`;;
bstep (Ret e) env eval Nop env)`;;
......@@ -81,9 +81,10 @@ let bexp_INDUCT, bexp_REC = define_type
Define evaluation of booleans for reals
*)
let bval_SIMPS = define
`(bval (leq e1 e2) (E:num->real) (eval:(V)exp->(num->real)->real) =
`(bval (leq e1 e2) (E:num->real) (eval:(real)exp->(num->real)->real) =
(eval e1 E) <= (eval e2 E)) /\
(bval (less e1 e2) E eval = (eval e1 E) < (eval e2 E))`;;
(bval (less e1 e2) (E:num->real) (eval:(real)exp->(num->real)->real) =
(eval e1 E) < (eval e2 E))`;;
(* Simplify arithmetic later by making > >= only abbreviations *)
let gr_simps = define
......
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