Commit 4b3f7f61 authored by Heiko Becker's avatar Heiko Becker
Browse files

Basic version of daisy IL working

parent 23427b3b
......@@ -11,15 +11,28 @@ let exp_INDUCT, exp_REC= define_type
| Mult exp exp
| Div exp exp";;
let exp_eval_SIMPS = define
`(exp_eval (Var x) E = E x) /\
(exp_eval (Const r) E = r) /\
(exp_eval (Plus e1 e2) E = (exp_eval e1) E + (exp_eval e2) E) /\
(exp_eval (Sub e1 e2) E = (exp_eval e1) E - (exp_eval e2) E) /\
(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 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) /\
(!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)`;;
let exp_eval_DEF = new_specification ["exp_eval"] exp_eval_EXISTS;;
`exp_eval (Const (&1)) (\x. &1)`;;
REWRITE_CONV[exp_eval_DEF] it;;
rhs (concl it);;
(* Prove totality of expression evaluation *)
let exp_eval_total =
prove (
`!e (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[]);;
(*
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`);;
......@@ -41,7 +54,7 @@ e (EXISTS_TAC `(v1:real) + (v2:real)` THEN ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
e (MESON_TAC[]);;
let exp_eval_total = top_thm();;
let exp_eval_total = top_thm();; *)
let bexp_INDUCT, bexp_REC = define_type
"bexp = leq exp exp
......@@ -62,26 +75,19 @@ let cmd_INDUCT, cmd_REC = define_type
| Ite bexp cmd cmd
| Nop";;
let upd_env_simps1 = define
let upd_env_simps = define
`upd_env (x:num) (v:real) (E:num->real) =(\y. if y = x then v else E y)`;;
(* Small Step semantics for Daisy Language *)
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x e s E v. exp_eval e E = v ==> sstep (Ass x e s) E s (upd_env x v E)) /\
(! c s t E. bval c E = true ==> sstep (Ite c s t) E s E) /\
(! c s t E. bval c E = false ==> sstep (Ite c s t) E t E)`;;
`(!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)`;;
(* Big Step semantics for Daisy Language *)
let bstep_RULES, bstep_INDUCT, bstep_CASES = new_inductive_definition
`(!x e s1 s2 E v.
exp_eval e (E:num->real) = v ==>
bstep (s1:cmd) (upd_env x v E) (s2:cmd) ==>
bstep (Ass x e s1) E s2) /\
(!c s1 s2 t E.
bval c (E:num->real) = true ==>
bstep s1 E s2 ==>
bstep (Ite c s1 t) E s2) /\
(!c s t1 t2 E.
bval c (E:num->real) = false ==>
bstep t1 E t2 ==>
bstep (Ite c s t1) E t2)`;;
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)`;;
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