Commit 23427b3b authored by Heiko Becker's avatar Heiko Becker
Browse files

Add current state

parent b3b0e20d
(*
Some tactic aliases that ease the use
*)
let INTROS = REPEAT STRIP_TAC;;
let SPECIALIZE v t =
ASSUME_TAC (SPECL [v] (ASSUME t));;
(*
Formalization of the Abstract Syntax Tree of a subset used in the Daisy framework
*)
*)
needs "Infra/tactics.ml";;
(* FIXME: num -> real for Const *)
let exp_INDUCT, exp_REC= define_type
"exp = Var num
| Const real
......@@ -11,29 +11,77 @@ let exp_INDUCT, exp_REC= define_type
| Mult exp exp
| Div exp exp";;
let exp_eval = define
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)`;;
(exp_eval (Div e1 e2) E = (exp_eval e1) E / (exp_eval e2) E)`;;
(* 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[]);;
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`);;
e (SPECIALIZE `a:num` `!(x:num). ?(v:real). (s:num->real) x = v`);;
e (DESTRUCT_TAC "@v. v_def" (ASSUME `?(v:real). (s:num->real) a = v`));;
e (EXISTS_TAC `v:real`);;
e (ASM_REWRITE_TAC[exp_eval_SIMPS]);;
e (EXISTS_TAC `a:real`);;
e (REWRITE_TAC [exp_eval_SIMPS]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`);;
e (SUBGOAL_TAC "val_def_a0" `?v. exp_eval a0 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a0 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (SPECIALIZE `s:num->real` `!s. (!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`);;
e (SUBGOAL_TAC "val_def_a1" `?v. exp_eval a1 s = v` [ALL_TAC]);;
e (MATCH_MP_TAC (ASSUME `(!x. ?v. s x = v) ==> (?v. exp_eval a1 s = v)`) THEN ASM_REWRITE_TAC[]);;
e (DESTRUCT_TAC "@v1. v1_def" (ASSUME `?v. exp_eval a0 s = v`));;
e (DESTRUCT_TAC "@v2. v2_def" (ASSUME `?v. exp_eval a1 s = v`));;
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 bexp_INDUCT, bexp_REC = define_type
"bexp = leq exp exp
| less exp exp";;
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 = `\e1. \e2. less e2 e1`;;
let greq = `\e1. \e2. leq e2 e1`;;
let gr_simps = define
`gr = \e1. \e2. less e2 e1`;;
let greq_simps = define
`greq = \e1. \e2. leq e2 e1`;;
let cmd_INDUCT, cmd_REC = define_type
"cmd = Ass num exp
| Seq cmd cmd
| Ite bexp cmd cmd";;
"cmd = Ass num exp cmd
| Ite bexp cmd cmd
| Nop";;
let upd_env_simps1 = 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)`;;
(* 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)`;;
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