Commit 9d635a47 authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix flaw, that epsilon was undefined

parent 1a8c9bc5
......@@ -25,36 +25,36 @@ Definition upd_env (x:nat) (v: R) (E: nat -> R) (y:nat) :R :=
(**
Small Step semantics for Daisy language, parametric by evaluation function.
**)
Inductive sstep : cmd R -> env_ty -> cmd R -> env_ty -> Prop :=
Inductive sstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
let_s x e s env v eps:
eval_exp eps env e v ->
sstep (Let R x e s) env s (upd_env x v env)
sstep (Let R x e s) env eps s (upd_env x v env)
|condtrue_s c s t eps env:
bval eps env c True ->
sstep (Ite R c s t) env s env
sstep (Ite R c s t) env eps s env
|condfalse_s c s t eps env:
(~bval eps env c True) ->
sstep (Ite R c s t) env s env
sstep (Ite R c s t) env eps s env
|ret_s e v eps env:
eval_exp eps env e v ->
sstep (Ret R e) env (Nop R) (upd_env 0 v env).
sstep (Ret R e) env eps (Nop R) (upd_env 0 v env).
(**
Analogously define Big Step semantics for the Daisy language,
parametric by the evaluation function
**)
Inductive bstep : cmd R -> env_ty -> cmd R -> env_ty -> Prop :=
Inductive bstep : cmd R -> env_ty -> R -> cmd R -> env_ty -> Prop :=
let_b x e s env v eps env2:
eval_exp eps env e v ->
bstep s (upd_env x v env) s env2 ->
bstep (Let R x e s) env s env2
bstep s (upd_env x v env) eps s env2 ->
bstep (Let R x e s) env eps s env2
|condtrue_b c s1 s2 t eps env env2:
bval eps env c True ->
bstep s1 env s2 env2 ->
bstep (Ite R c s1 t) env s2 env2
bstep s1 env eps s2 env2 ->
bstep (Ite R c s1 t) env eps s2 env2
|condgalse_b c s t1 t2 eps env env2:
(~ bval eps env c True) ->
bstep t1 env t2 env2 ->
bstep (Ite R c s t1) env t2 env2
bstep t1 env eps t2 env2 ->
bstep (Ite R c s t1) env eps t2 env2
|ret_b e v eps env:
eval_exp eps env e v ->
bstep (Ret R e) env (Nop R) (upd_env 0 v env).
\ No newline at end of file
bstep (Ret R e) env eps (Nop R) (upd_env 0 v env).
\ No newline at end of file
......@@ -26,19 +26,19 @@ let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x (e:(real)exp) s (env:num->real) (v:real) eps
(env:num->real).
eval_exp eps env e v ==>
sstep (Let x e s) env s (upd_env x v env)) /\
sstep (Let x e s) env eps s (upd_env x v env)) /\
(!(c:(real)bexp) s t eps
(env:num->real).
bval eps env c T ==>
sstep (Ite c s t) env s env) /\
sstep (Ite c s t) env eps s env) /\
(!(c:(real)bexp) s t eps
(env:num->real).
bval eps env c F ==>
sstep (Ite c s t) env t env) /\
sstep (Ite c s t) env eps t env) /\
(!(e:(real)exp) (v:real) eps
(env:num->real).
eval_exp eps env e v ==>
sstep (Ret e) env Nop (upd_env (0) v env))`;;
sstep (Ret e) env eps Nop (upd_env (0) v env))`;;
(*
Analogously define Big Step semantics for the Daisy language,
......@@ -47,21 +47,21 @@ let bstep_RULES,bstep_INDUCT,bstep_CASES = new_inductive_definition
`(!x (e:(real)exp) s (env:num->real) (v:real) eps
(env2:num->real).
eval_exp eps env e v /\
bstep s (upd_env x v env) s env2 ==>
bstep (Let x e s) env s env2) /\
bstep s (upd_env x v env) eps s env2 ==>
bstep (Let x e s) env eps s env2) /\
(!(c:(real)bexp) s1 s2 t eps
(env:num->real)
(env2:num->real).
bval eps env c T /\
bstep s1 env s2 env2 ==>
bstep (Ite c s1 t) env s2 env2) /\
bstep s1 env eps s2 env2 ==>
bstep (Ite c s1 t) env eps s2 env2) /\
(!(c:(real)bexp) s t1 t2 eps
(env:num->real)
(env2:num->real).
bval eps env c F /\
bstep t1 env t2 env2 ==>
bstep (Ite c s t1) env t2 env2) /\
bstep t1 env eps t2 env2 ==>
bstep (Ite c s t1) env eps t2 env2) /\
(!(e:(real)exp) (v:real) eps
(env:num->real).
eval_exp eps env e v ==>
bstep (Ret e) env Nop (upd_env 0 v env))`;;
bstep (Ret e) env eps Nop (upd_env 0 v env))`;;
......@@ -154,8 +154,7 @@ e (DISJ2_TAC THEN DISJ2_TAC);;
e (CHEAT_TAC);; (* FIXME: Follows from Asms *)
(* Destruct IH, rewrite then done *)
e (CHEAT_TAC);;
b();;
b();;
let eval_0_det = top_thm();;
(*
Using the parametric expressions, define boolean expressions for conditionals
......
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